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

Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c.kernel/Frama_c_kernel/Interpreted_automata/index.html

Module `Frama_c_kernel.Interpreted_automata`

An interpreted automaton is a convenient formalization of programs for abstract interpretation. It is a control flow graph where states are control point and edges are transitions. It keeps track of conditions on which a transition can be taken (guards) as well as actions which are computed when a transition is taken. It can then be interpreted w.r.t. the operational semantics to reproduce the behavior of the program or w.r.t. to the collection semantics to compute a set of reachable states.

This intermediate representation abstracts almost completely the notion of statement in CIL. Edges are either CIL expressions for guards, CIL instructions for actions or a return Edge. Thus, it saves the higher abstraction layers from interpreting CIL statements and from attaching guards to statement successors.

type vertex_info =

| NoneInfo
| LoopHead of {
1. stmt : Cil_types.stmt;
2. level : int;
}

type 'a control =

| Edges
(*
control flow is only given by vertex edges.
*)
| Loop of 'a
(*
start of a Loop stmt, with breaking vertex.
*)
| If of {
1. cond : Cil_types.exp;
2. vthen : 'a;
3. velse : 'a;
}
(*
edges are guaranteed to be two guards `Then` else `Else` with the given condition and successor vertices.
*)
| Switch of {
1. value : Cil_types.exp;
2. cases : (Cil_types.exp * 'a) list;
3. default : 'a;
}
(*
edges are guaranteed to be issued from a `switch()` statement with the given cases and default vertices.
*)

Control flow informations for outgoing edges, if any.

Vertices are control points. When a vertice is the *start* of a statement, this statement is kept in vertex_start_of.

type vertex = private {

vertex_kf : Cil_types.kernel_function;
vertex_key : int;
vertex_blocks : Cil_types.block list;
mutable vertex_start_of : Cil_types.stmt option;
mutable vertex_end_of : Cil_types.stmt list;
mutable vertex_info : vertex_info;
mutable vertex_control : vertex control;

}

type assert_kind =

| Invariant
| Assert
| Check
| Assume

type 'vertex labels = 'vertex Cil_datatype.Logic_label.Map.t

Maps binding the labels from an annotation to the vertices they refer to in the graph.

type 'vertex annotation = {

kind : assert_kind;
predicate : Cil_types.identified_predicate;
labels : 'vertex labels;
property : Property.t;

}

type 'vertex transition =

| Skip
| Return of Cil_types.exp option * Cil_types.stmt
| Guard of Cil_types.exp * guard_kind * Cil_types.stmt
| Prop of 'vertex annotation * Cil_types.stmt
| Instr of Cil_types.instr * Cil_types.stmt
| Enter of Cil_types.block
| Leave of Cil_types.block

Each transition can either be a skip (do nothing), a return, a guard represented by a Cil expression, a Cil instruction, an ACSL annotation or entering/leaving a block. The edge is annotated with the statement from which the transition has been generated. This is currently used to choose alarms locations.

and guard_kind =

| Then
| Else

type 'vertex edge = private {

edge_kf : Cil_types.kernel_function;
edge_key : int;
edge_kinstr : Cil_types.kinstr;
edge_transition : 'vertex transition;
edge_loc : Cil_types.location;

}

module G : 
  Graph.Sig.G
    with type V.t = vertex
     and type E.t = vertex * vertex edge * vertex
     and type V.label = vertex
     and type E.label = vertex edge

type graph = G.t

type wto = vertex Wto.partition

Weak Topological Order is given by a list (in topological order) of components of the graph, which are themselves WTOs

module Vertex : Datatype.S_with_collections with type t = vertex

Datatype for vertices

module Edge : Datatype.S_with_collections with type t = vertex edge

Datatype for edges

type automaton = {

graph : graph;
entry_point : vertex;
return_point : vertex;
exit_points : vertex list;
stmt_table : (vertex * vertex) Cil_datatype.Stmt.Hashtbl.t;

}

An interpreted automaton for a given function is a graph whose edges are guards and commands.

graph is the control flow graph
entry_point: each execution of the function starts at this vertex
return_point: return statements link to this vertex
exit_points: each call to a non-returning function (declared with the C attribute "noreturn") leads to a vertex from this list, with no successor
stmt_table: this table links statements to their starting and ending vertex

module Automaton : Datatype.S with type t = automaton

Datatype for automata

module WTO : Wto.S with type node = vertex

Datatype for WTOs

val build_automaton : 
  annotations:bool ->
  Cil_types.kernel_function ->
  automaton

Build an interpreted automaton for the given kernel_function. If annotations is true, the automaton includes Prop transitions for assertions and loop invariants of the function body. Note that the automata construction may lead to the build of new Cil expressions which will be different at each call: you may need to memoize the results of this function.

val build_wto : ?pref:WTO.pref -> automaton -> wto

Build a wto for the given automaton. The pref function is a comparison function used to determine what is the best vertex to use as a Wto component head. See Wto.Make for more details.

val get_automaton : Cil_types.kernel_function -> automaton

Get the automaton for the given kernel_function. This is the memoized version of build_automaton ~annotations:false

val exit_strategy : automaton -> vertex Wto.component -> wto

Extract an exit strategy from a component, i.e. a sub-wto where all vertices lead outside the wto without passing through the head.

val output_to_dot : 
  ?pp_vertex:vertex Pretty_utils.formatter ->
  ?pp_edge:vertex edge Pretty_utils.formatter ->
  ?wto:wto ->
  out_channel ->
  automaton ->
  unit

Output the automaton in dot format.

type wto_index = vertex list

the position of a statement in a wto given as the list of component heads

module WTOIndex : sig ... end

Dataflow computation: simple data-flow analysis using interpreted automata. See tests/misc/interpreted_automata_dataflow.ml for a complete example using this dataflow computation.

type 'a widening =

| Fixpoint
(*
The analysis of the loop has reached a fixpoint.
*)
| Widening of 'a
(*
The analysis of the loop has not reached a fixpoint yet, and must continue through a new iteration with the given state, widened if termination requires it.
*)

module type Domain = sig ... end

Input domain for a simple dataflow analysis.

module type DataflowAnalysis = sig ... end

Simple dataflow analysis

module ForwardAnalysis (D : Domain) : DataflowAnalysis with type state = D.t

Forward dataflow analysis. The domain must provide a forward transfer function that computes the state after a transition from the state before.

module BackwardAnalysis (D : Domain) : DataflowAnalysis with type state = D.t

Backward dataflow analysis. The domain must provide a backward transfer function that computes the state before a transition from the state after.

module type Graph = sig ... end

Generic control flow graphs

module MakeGraph
  (Vertex : Datatype.S_with_hashtbl)
  (Edge : Datatype.S) : 
  Graph
    with type V.t = Vertex.t
     and type E.t = Vertex.t * Edge.t * Vertex.t
     and type V.label = Vertex.t
     and type E.label = Edge.t
     and module VTable = Vertex.Hashtbl

This functor can be used to build generic control flow graphs

module UnrollUnnatural : sig ... end

Control flow graphs where unnatural loops are modified such that all paths entering a loop enters it by its head.