Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make

Parameters

module _ : sig ... end

Signature

val widening_delay : int
val widening_period : int
val history_size : int
val universal_splits : Partition.action list
val flow_actions : Eva_automata.vertex -> Partition.action list * bool

Returns the partitioning actions to be applied on the analysis flow at the given vertex and a boolean indicating whether the propagated states must be stored (and duplicate states filtered out).

val call_return_policy : Partition.call_return_policy