package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/CfgCompiler/Cfg/index.html

Module `CfgCompiler.Cfg`Source

Parameters

module S : Sigs.Sigma

Signature

Sourcemodule S = S

The memory model used.

Sourcemodule Node : sig ... end

Program point along a trace.

Sourcetype node = Node.t

Sourceval node : unit -> node

fresh node

Relocatable Formulae

Can be created once with fresh environment, and used several times on different memory states.

Sourcemodule C : sig ... end

Relocatable condition

Sourcemodule P : sig ... end

Relocatable predicate

Sourcemodule T : sig ... end

Relocatable term

Sourcemodule E : sig ... end

Relocatable effect (a predicate that depend on two states).

Sourcetype cfg

Structured collection of traces.

Sourceval dump_env : name:string -> cfg -> unit

Sourceval output_dot : out_channel -> ?checks:P.t Frama_c_kernel.Bag.t -> cfg -> unit

Sourceval 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

Sourceval add_tmpnode : node -> cfg

Set a node as temporary. Information about its path predicate or sigma can be discarded during compilation

Sourceval concat : cfg -> cfg -> cfg

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

Sourceval meta : ?stmt:Frama_c_kernel.Cil_types.stmt -> ?descr:string -> node -> cfg

Attach meta informations to a node. Formally, it is equivalent to nop.

Sourceval goto : node -> node -> cfg

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))

Sourceval branch : node -> C.t -> node -> node -> cfg

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))) )

Sourceval guard : node -> C.t -> node -> cfg

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 ) )

Sourceval guard' : node -> C.t -> node -> cfg

Same than guard but the condition is negated

Sourceval either : node -> node list -> cfg

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)))

Sourceval implies : node -> (C.t * node) list -> cfg

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)

Sourceval effect : node -> E.t -> node -> cfg

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 )

Sourceval assume : P.t -> cfg

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

Sourceval 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

Source

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

On This Page

Parameters
Signature
1. Relocatable Formulae
2. Path-Predicates