Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make

Parameters

module _ : sig ... end

Signature

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:Frama_c_kernel.Cil_types.stmt option -> is_loop_head:bool -> store
val empty_flow : flow
val empty_tank : unit -> tank
val empty_widening : stmt:Frama_c_kernel.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 -> (Partition.key * state) list
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 add_disjunction_keys : Frama_c_kernel.Cil_types.stmt -> Partition.key -> 'state list -> (Partition.key * 'state) list
val enter_loop : flow -> Eva_automata.loop -> flow
val leave_loop : flow -> Eva_automata.loop -> flow
val next_loop_iteration : flow -> Frama_c_kernel.Cil_types.stmt -> flow
val split_return : flow -> Eva_ast.exp option -> flow
val call_return : caller:Partition.key -> Engine_sig.call_kind -> (Partition.key * state) list -> (Partition.key * state) list

After the analysis of a function call, recombines callee partitioning keys with the caller key.

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 : ((Partition.key * state) -> (Partition.key * state) list) -> flow -> flow

Apply a transfer function to all the states of a propagation.

val join : (int * 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.