Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eva_automata

Eva automata are Interpreted_automata where transitions have been translated to the Eva AST and where useless transitions have been replaced by Skip. As such, it essentially differs by its simpler vertex, edge and transitions types.

type vertex = private {
  1. vertex_kf : Frama_c_kernel.Cil_types.kernel_function;
  2. vertex_key : int;
  3. vertex_start_of : Frama_c_kernel.Cil_types.stmt option;
  4. vertex_info : vertex_info;
  5. mutable vertex_wto_index : vertex list;
}
type guard_kind =
  1. | Then
  2. | Else
type edge = private {
  1. edge_kf : Frama_c_kernel.Cil_types.kernel_function;
  2. edge_key : int;
  3. edge_kinstr : Frama_c_kernel.Cil_types.kinstr;
  4. edge_transition : transition;
  5. edge_loc : Frama_c_kernel.Cil_types.location;
}
module G : Graph.Sig.I with type V.t = vertex and type E.t = vertex * edge * vertex and type V.label = vertex and type E.label = edge
type graph = G.t
type automaton = {
  1. graph : graph;
  2. wto : wto;
  3. entry_point : vertex;
  4. return_point : vertex;
  5. stmt_table : (vertex * vertex) Frama_c_kernel.Cil_datatype.Stmt.Hashtbl.t;
}
val output_to_dot : Stdlib.out_channel -> automaton -> unit
val wto_index_diff : vertex -> vertex -> vertex list * vertex list
val is_wto_head : vertex -> bool
val is_back_edge : (vertex * vertex) -> bool
type loop = {
  1. graph : graph;
    (*

    The complete graph of the englobing function.

    *)
  2. head : vertex;
    (*

    The head of the loop.

    *)
  3. wto : wto;
    (*

    The wto for the loop body (without the loop head).

    *)
  4. stmt : Frama_c_kernel.Cil_types.stmt;
    (*

    The statement at the loop head.

    *)
}
val find_loop : automaton -> vertex -> loop option

Builds the loop type for the englobing loop of vertex.

Dataflow analysis

type 'a widening =
  1. | Fixpoint
  2. | Widening of 'a
module type Domain = sig ... end

Abstract domain for the dataflow analysis. See Interpreted_automata.Domain.

module ForwardAnalysis (D : Domain) : sig ... end

Forward Dataflow analysis. See Interpreted_automata.ForwardAnalysis.

module BackwardAnalysis (D : Domain) : sig ... end

Backward Dataflow analysis. See Interpreted_automata.BackwardAnalysis.