module Make:
Parameters: |
|
typestate =
Abstract.Dom.t
type
store
type
tank
type
flow
type
widening
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
val pretty_store : Format.formatter -> store -> unit
val pretty_flow : 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
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
empty_tank
val fill : into:tank -> flow -> unit
into
inplace.val transfer : (state -> state list) ->
flow -> flow
val join : (Partition.branch * flow) list ->
store -> flow
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