Functor Trace_partitioning.Make

module Make: 
functor (Abstract : Abstractions.Eva-> 
functor (Kf : sig
val kf : Cil_types.kernel_function
end-> sig .. end
Parameters:
Abstract : Abstractions.Eva
Kf : sig val kf: Cil_types.kernel_function end

type state = 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.