module Make:functor (
Abstract
:
Abstractions.Eva
) ->
Parameters: |
|
typestate =
Abstract.Dom.t
The states being partitioned
type
store
The storage of all states ever met at a control point
type
tank
The set of states that remains to propagate from a control point.
type
flow
A set of states which are currently propagated
type
widening
Widening information
val empty_store : stmt:Cil_types.stmt option -> store
val empty_flow : flow
val empty_tank : unit -> tank
val empty_widening : stmt:Cil_types.stmt option -> widening
val initial_tank : state list -> tank
Build the initial tank for the entry point of a function.
val pretty_store : Stdlib.Format.formatter -> store -> unit
val pretty_flow : Stdlib.Format.formatter -> flow -> unit
val expanded : store -> state list
val smashed : store ->
state Bottom.Type.or_bottom
val contents : flow -> state list
val is_empty_store : store -> bool
val is_empty_flow : flow -> bool
val is_empty_tank : tank -> bool
val store_size : store -> int
val flow_size : flow -> int
val tank_size : tank -> int
val reset_store : store -> unit
val reset_tank : tank -> unit
val reset_widening : widening -> unit
val reset_widening_counter : widening -> unit
Resets (or just delays) the widening counter. Used on nested loops, to postpone the widening of the inner loop when iterating on the outer loops. This is especially useful when the inner loop fixpoint does not depend on the outer loop.
val enter_loop : flow ->
Cil_types.stmt -> flow
val leave_loop : flow ->
Cil_types.stmt -> flow
val next_loop_iteration : flow ->
Cil_types.stmt -> flow
val split_return : flow ->
Cil_types.exp option -> flow
val drain : tank -> flow
Remove all states from the tank, leaving it empty as if it was just
created by empty_tank
val fill : into:tank -> flow -> unit
Fill the states of the flow into the tank, modifying into
inplace.
val transfer : (state -> state list) ->
flow -> flow
Apply a transfer function to all the states of a propagation.
val join : (Partition.branch * flow) list ->
store -> flow
Join all incoming propagations into the given store. This function returns a set of states which still need to be propagated past the store.
If a state from the propagations is included in another state which has already been propagated, it may be removed from the output propagation. Likewise, if a state from a propagation is included in a state from another propagation of the list (coming from another edge or iteration), it may also be removed.
This function also interprets partitioning annotations at the store vertex (slevel, splits, merges, ...) which will generally change the current partitioning.
val widen : widening ->
flow -> flow
Widen a flow. The widening object keeps track of the previous widenings and previous propagated states to ensure termination.