package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

type 'a flow

A flow is a flow map augmented with an context

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

Empty set of flows

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

Set of all possible flows

val 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

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

Emptiness test

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

top test

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

Inclusion test

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

Abstraction union operator.

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

Union over a list of flows

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

Abstract intersection operator

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

Intersection over a list of flows.

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

Widening operator.

val print : (Print.printer -> 'a -> unit) -> Print.printer -> 'a flow -> unit
val 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.

val 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.

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

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

val 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

val 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

val 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

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

remove tk flow removes token tk from the map of flow

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

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

val partition : (Token.token -> 'a -> bool) -> 'a flow -> 'a flow * 'a flow
val map : (Token.token -> 'a -> 'a) -> 'a flow -> 'a flow
val fold : ('b -> Token.token -> 'a -> 'b) -> 'b -> 'a flow -> 'b
val 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
val merge : 'a Lattice.lattice -> merge_report:(Alarm.report -> Alarm.report -> Alarm.report) -> 'a flow -> ('a flow * Effect.teffect) -> ('a flow * Effect.teffect) -> 'a flow
val get_ctx : 'a flow -> 'a Context.ctx

get_all_ctx flow retrieves the context pool from flow

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

set_all_ctx ctx flow set the context pool of flow to ctx

val 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

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

Empty set of flows

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct