Frama-C:
Plug-ins:
Libraries:

Frama-C API - Engine_sig

type call_kind = [
  1. | `Body
  2. | `Spec
  3. | `Builtin
  4. | `Internal
  5. | `Bottom
]

Kind of function that is analyzed: a body, a specification, a builtin, an internal Frama_C_ (not builtin) function, or nothing. Note that if several functions may be called, preceding values have priority.

type 'state call_result = {
  1. states : (Partition.key * 'state) list;
  2. cacheable : Eval.cacheable;
  3. kind : call_kind;
}

Results of the analysis of a function call:

  • the list of computed abstract states at the return statement of the called function, associated with their partition key;
  • whether the results can safely be stored in the memexec cache;
  • the kind of analyzed function.
module type Transfer_inout = sig ... end

Helper module to register read and written memory zones to Inout_access, built by Transfer_inout.Make.

module type Transfer_stmt = sig ... end

Interpretation of statements, built by functor Transfer_stmt.Make.

module type Transfer_logic = sig ... end

Interpretation of logic assertions, built by functor Transfer_logic.Make.

module type Transfer_specification = sig ... end

Interpretation of function specification, built by functor Transfer_specification.Make.

module type Initialization = sig ... end

Initialization of variables, built by functor Initialization.Make.

module type Iterator = sig ... end

Analysis of a function body by iteration over its interpreted automata, built by the functor Iterator.Make.

module type Compute = sig ... end

Complete analysis of functions, built by the functor Compute_functions.Make.

module type Interferences = sig ... end
module type S = sig ... end
module type Results = sig ... end

Access to analysis results, built by Analysis and used by Results, which defines the final and complete API to access Eva results.

module type S_with_results = sig ... end