package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install 

dune-project
 Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (3)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.1.tar.gz
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500

doc/core/Core/Flow/index.html

Module Core.FlowSource

Abstraction of control flows.

Flows represent a trace partitioning the collect environments depending on the kind of the control flow. Not only reaching environments are concerned, but also environments of traces suspended at previous control points are kept in the flow map. In addition, flow insensitive contexts are also maintained in the flow abstraction.

Sourcetype 'a flow

A flow is a flow map augmented with an context

Sourceval bottom : 'a Context.ctx -> Alarm.report -> 'a flow

Empty set of flows

Sourceval top : 'a Context.ctx -> 'a flow

Set of all possible flows

Sourceval singleton : 'a Context.ctx -> Token.token -> 'a -> 'a flow

singleton ctx tk e returns a flow with a context ctx and a map with a single binding tk to environment e

Sourceval is_bottom : 'a Lattice.lattice -> 'a flow -> bool

Emptiness test

Sourceval is_top : 'a Lattice.lattice -> 'a flow -> bool

top test

Sourceval is_empty : 'a flow -> bool
Sourceval is_singleton : 'a flow -> bool
Sourceval subset : 'a Lattice.lattice -> 'a flow -> 'a flow -> bool

Inclusion test

Sourceval join : 'a Lattice.lattice -> 'a flow -> 'a flow -> 'a flow

Abstraction union operator.

Sourceval join_list : 'a Lattice.lattice -> empty:(unit -> 'a flow) -> 'a flow list -> 'a flow

Union over a list of flows

Sourceval meet : 'a Lattice.lattice -> 'a flow -> 'a flow -> 'a flow

Abstract intersection operator

Sourceval meet_list : 'a Lattice.lattice -> empty:'a flow -> 'a flow list -> 'a flow

Intersection over a list of flows.

Sourceval widen : 'a Lattice.lattice -> 'a flow -> 'a flow -> 'a flow

Widening operator.

Sourceval print : (Print.printer -> 'a -> unit) -> Print.printer -> 'a flow -> unit
Sourceval get : Token.token -> 'a Lattice.lattice -> 'a flow -> 'a

get tk lat flow returns the abstract element associated to token tk in flow. Returns lat.bottom if the binding is not found.

Sourceval set : Token.token -> 'a -> 'a Lattice.lattice -> 'a flow -> 'a flow

set tk a lat flow overwrites the binding of token tk in flow with the abstract element a.

Sourceval set_bottom : Token.token -> 'a flow -> 'a flow

set_bottom tk lat flow overwrites the binding of token tk in flow with a ⊥ environment.

Sourceval copy : Token.token -> Token.token -> 'a Lattice.lattice -> 'a flow -> 'a flow -> 'a flow

copy tk1 tk2 lat flow1 flow2 copies the environment at token tk1 in flow1 into token tk2 in flow2

Sourceval add : Token.token -> 'a -> 'a Lattice.lattice -> 'a flow -> 'a flow

add tk a lat flow appends (by union) a to the existing binding of tk in flow. It is equivalent to set tk (lat.join a (get tk lat flow)) flow

Sourceval rename : Token.token -> Token.token -> 'a Lattice.lattice -> 'a flow -> 'a flow

rename tki tko flow appends (by union) the environment of tki to the existing binding of tka in flow. It is equivalent to add tko (get tki flow) flow

Sourceval remove : Token.token -> 'a flow -> 'a flow

remove tk flow removes token tk from the map of flow

Sourceval mem : Token.token -> 'a flow -> bool
Sourceval filter : (Token.token -> 'a -> bool) -> 'a flow -> 'a flow

filter f flow keeps in flow all tokens tk verifying f tk = true

Sourceval partition : (Token.token -> 'a -> bool) -> 'a flow -> 'a flow * 'a flow
Sourceval map : (Token.token -> 'a -> 'a) -> 'a flow -> 'a flow
Sourceval fold : ('b -> Token.token -> 'a -> 'b) -> 'b -> 'a flow -> 'b
Sourceval map2zo : (Token.token -> 'a -> 'a) -> (Token.token -> 'a -> 'a) -> (Token.token -> 'a -> 'a -> 'a) -> (Alarm.report -> Alarm.report -> Alarm.report) -> 'a flow -> 'a flow -> 'a flow
Sourceval merge : 'a Lattice.lattice -> merge_report:(Alarm.report -> Alarm.report -> Alarm.report) -> 'a flow -> ('a flow * Change.change_map) -> ('a flow * Change.change_map) -> 'a flow
Sourceval get_ctx : 'a flow -> 'a Context.ctx

get_all_ctx flow retrieves the context pool from flow

Sourceval set_ctx : 'a Context.ctx -> 'a flow -> 'a flow

set_all_ctx ctx flow set the context pool of flow to ctx

Sourceval map_ctx : ('a Context.ctx -> 'a Context.ctx) -> 'a flow -> 'a flow

map_all_ctx f flow set the context of flow to be the image of the initial context of flow by f

Sourceval copy_ctx : 'a flow -> 'a flow -> 'a flow
Sourceval get_token_map : 'a flow -> 'a Token.TokenMap.t
Sourceval add_alarm : ?force:bool -> ?warning:bool -> Alarm.alarm -> 'a Lattice.lattice -> 'a flow -> 'a flow
Sourceval raise_alarm : ?force:bool -> ?bottom:bool -> ?warning:bool -> Alarm.alarm -> 'a Lattice.lattice -> 'a flow -> 'a flow
Sourceval add_diagnostic : Alarm.diagnostic -> 'a flow -> 'a flow
Sourceval add_warning_check : Alarm.check -> Mopsa_utils.Location.range -> 'a flow -> 'a flow
Sourceval add_safe_check : Alarm.check -> Mopsa_utils.Location.range -> 'a flow -> 'a flow
Sourceval add_unreachable_check : Alarm.check -> Mopsa_utils.Location.range -> 'a flow -> 'a flow
Sourceval add_assumption : Alarm.assumption -> 'a flow -> 'a flow
Sourceval add_global_assumption : Alarm.assumption_kind -> 'a flow -> 'a flow
Sourceval add_local_assumption : Alarm.assumption_kind -> Mopsa_utils.Location.range -> 'a flow -> 'a flow
Sourceval get_report : 'a flow -> Alarm.report
Sourceval set_report : Alarm.report -> 'a flow -> 'a flow
Sourceval copy_report : 'a flow -> 'a flow -> 'a flow
Sourceval remove_report : 'a flow -> 'a flow
Sourceval create : 'a Context.ctx -> Alarm.report -> 'a Token.TokenMap.t -> 'a flow
Sourceval set_callstack : Mopsa_utils.Callstack.callstack -> 'a flow -> 'a flow
Sourceval push_callstack : string -> ?uniq:string -> Mopsa_utils.Location.range -> 'a flow -> 'a flow
Sourceval pop_callstack : 'a flow -> Mopsa_utils.Callstack.callsite * 'a flow
Sourceval bottom_from : 'a flow -> 'a flow

Empty set of flows