Module `Core.Flow`Source

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.

Source

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

Source

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

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

Source

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

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

Source

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

Source

val 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

Source

val add_alarm : 
  ?force:bool ->
  ?warning:bool ->
  Alarm.alarm ->
  'a Lattice.lattice ->
  'a flow ->
  'a flow

Source

val 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

Source

val add_warning_check : 
  Alarm.check ->
  Mopsa_utils.Location.range ->
  'a flow ->
  'a flow

Source

val add_safe_check : 
  Alarm.check ->
  Mopsa_utils.Location.range ->
  'a flow ->
  'a flow

Source

val 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

Source

val 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 get_callstack : 'a flow -> Mopsa_utils.Callstack.callstack

Sourceval set_callstack : Mopsa_utils.Callstack.callstack -> 'a flow -> 'a flow

Source

val 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/core/Core/Flow/index.html

Module `Core.Flow`Source

package mopsa

Install

Dune Dependency

Authors

Maintainers

Sources

doc/core/Core/Flow/index.html

Module Core.FlowSource

Module `Core.Flow`Source