Frama-C API - Cfg
Parameters
module S : Sigs.Sigma
Signature
module S = S
The memory model used.
module Node : sig ... end
Program point along a trace.
type node = Node.t
val node : unit -> node
fresh node
Relocatable Formulae
Can be created once with fresh environment, and used several times on different memory states.
module C : sig ... end
Relocatable condition
module P : sig ... end
Relocatable predicate
module T : sig ... end
Relocatable term
module E : sig ... end
Relocatable effect (a predicate that depend on two states).
val dump_env : name:string -> cfg -> unit
val output_dot : Stdlib.out_channel -> ?checks:P.t Frama_c_kernel.Bag.t -> cfg -> unit
val nop : cfg
Structurally, 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
Set a node as temporary. Information about its path predicate or sigma can be discarded during compilation
The concatenation is the intersection of all possible collection of traces from each cfg.
concat
is associative, commutative, has nop
as neutral element.
Formally: | concat g1 g2 |
_I iff | g1 |
_I and | g2 |
_I
val meta : ?stmt:Frama_c_kernel.Cil_types.stmt -> ?descr:string -> node -> cfg
Attach meta informations to a node. Formally, it is equivalent to nop
.
Represents all execution traces 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))
Structurally corresponds to an if-then-else control-flow. The predicate 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))) )
Structurally corresponds to an assume control-flow. The predicate 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 ) )
Structurally corresponds to an arbitrary choice among the different possible executions.
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)))
implies is the dual of either. Instead of being a non-deterministic choice, it takes the choices that verify its predicate.
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)
Represents all execution trace 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 )
Represents execution traces 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 Sigs.sequence -> node -> cfg
Inserts an assigns effect between nodes 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 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).
Path-Predicates
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:mode -> node -> Node.Set.t -> S.domain Node.Map.t -> cfg -> Lang.F.pred Node.Map.t * S.t Node.Map.t * Conditions.sequence