module type Cfg =sig
..end
module S:Wp.Sigs.Sigma
module Node:sig
..end
typenode =
Node.t
val node : unit -> node
module C:sig
..end
module P:sig
..end
module T:sig
..end
module E:sig
..end
type
cfg
val dump_env : name:string -> cfg -> unit
val output_dot : Pervasives.out_channel ->
?checks:P.t Bag.t -> cfg -> unit
val nop : cfg
nop
is an empty execution trace.
Hence, nop
actually denotes all possible execution traces.
This is the neutral element of concat
.
Formally: all interpretations I verify nop: | nop |
_I
val add_tmpnode : node -> cfg
val concat : cfg -> cfg -> cfg
concat
is associative, commutative,
has nop
as neutral element.
Formally: | concat g1 g2 |
_I iff | g1 |
_I and | g2 |
_I
val meta : ?stmt:Cil_types.stmt ->
?descr:string -> node -> cfg
nop
.val goto : node -> node -> cfg
T
such that, if T
contains node a
,
T
also contains node b
and memory states at a
and b
are equal.
Formally: | goto a b |
_I iff (I(a) iff I(b))
val branch : node ->
C.t ->
node -> node -> cfg
P
shall reads only memory state at label Here
.
Formally: | branch n P a b |
_I iff ( (I(n) iff (I(a) \/ I(b)))
/\ (I(n) implies (if P(I(n)) then I(a) else I(b))) )
val guard : node ->
C.t -> node -> cfg
P
shall reads only memory state at label Here
.
Formally: | guard n P a |
_I iff ( (I(n) iff I(a))
/\ (I(n) implies | P |
_I ) )
val guard' : node ->
C.t -> node -> cfg
val either : node ->
node list -> cfg
either
is associative and commutative. either a []
is
very special, since it denotes a cfg with no trace. Technically,
it is equivalent to attaching an assert \false
annotation to node a
.
Formally: | either n [a_1;...;a_n] } |
_I iff ( I(n) iff (I(a_1) \/ ... I(a_n)))
val implies : node ->
(C.t * node) list ->
cfg
Formally: | either n [P_1,a_1;...;P_n,a_n] } |
_I iff ( I(n) iff (I(a_1) \/ ... I(a_n))
/\ I(n) implies | P_k |
_I implies I(a_k)
val effect : node ->
E.t -> node -> cfg
T
such that, if T
contains node a
,
then T
also contains b
with the given effect on corresponding
memory states.
Formally: | effect a e b |
_I iff (( I(a) iff I(b) ) /\ | e |
_I )
val assume : P.t -> cfg
T
such that, if T
contains
every node points in the label-map, then the condition holds over the
corresponding memory states. If the node-map is empty,
the condition must hold over all possible execution path.
Formally: | assume P |
_I iff | P |
_I
val havoc : node ->
effects:node Wp.Sigs.sequence ->
node -> cfg
a
and b
, correspondings
to all the written memory chunks accessible in execution paths delimited
by the effects
sequence of nodes.
Formally: | havoc a s b |
_I is verified if there is no path between s.pre and s.path,
otherwise if (I(a) iff I(b) and if I(a) is defined then I(a) and I(b) are equal
for all the chunks that are not in the written domain of an effect that can be found
between s.pre
to s.post
.
Note: the effects are collected in the final control-flow,
when Wp.CfgCompiler.Cfg.compile
is invoked. The portion of the sub-graph in the sequence
shall be concatenated to the cfg
before compiling-it, otherwize it would be
considered empty and havoc
would be a nop (no connection between a and b).
The compilation of cfg control-flow into path predicate
is performed by allocating fresh environments with optimized variable
allocation. Only the relevant path between the nodes
is extracted. Other paths in the cfg are pruned out.
Extract the nodes that are between the start node and the final
nodes and returns how to observe a collection of states indexed
by nodes. The returned maps gives, for each reachable node, a
predicate representing paths that reach the node and the memory
state at this node.
Nodes absent from the map are unreachable. Whenever possible,
predicate F.ptrue
is returned for inconditionally accessible
nodes.
~name: identifier used for debugging
val compile : ?name:string ->
?mode:Wp.CfgCompiler.mode ->
node ->
Node.Set.t ->
S.domain Node.Map.t ->
cfg ->
Wp.Lang.F.pred Node.Map.t *
S.t Node.Map.t * Wp.Conditions.sequence