Frama-C:
Plug-ins:
Libraries:

Frama-C API - Results

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

type state
type value
type location

Access to abstract states inferred by the analysis

val get_global_state : unit -> state Eval.or_top_bottom

Return the abstract state computed at the start of the analysis, as entry point of the main function, after the initialization of global variables and main arguments.

val get_stmt_state : after:bool -> Frama_c_kernel.Cil_types.stmt -> state Eval.or_top_bottom

Return the abstract state inferred before or after a given statement. This is the join of the states inferred for each callstack.

val get_stmt_state_by_callstack : ?selection:Callstack.t list -> after:bool -> Frama_c_kernel.Cil_types.stmt -> state Callstack.Hashtbl.t Eval.or_top_bottom

Return the abstract state inferred before or after a given statement, for each callstack in which the analysis has reached the statement. The optional argument selection allows selecting only some callstacks: it is more efficient to select fewer callstacks, if not all are needed.

Return the abstract state inferred at start of a given function. This is the join of states inferred for each callstack.

val get_initial_state_by_callstack : ?selection:Callstack.t list -> Frama_c_kernel.Cil_types.kernel_function -> state Callstack.Hashtbl.t Eval.or_top_bottom

Return the abstract state inferred as entry point of the given function, for each callstack in which the function has been analyzed. The optional argument selection allows selecting only some callstacks: it is more efficient to select fewer callstacks, if not all are needed.

Shortcuts for the evaluation in an abstract state

val eval_expr : state -> Eval.exp -> value Eval.evaluated

Evaluates the value of an expression in the given state.

Evaluates the value of an lvalue in the given state, with possible indeterminateness: non-initialization or escaping addresses.

val eval_lval_to_loc : state -> Eval.lval -> location Eval.evaluated

Evaluates the location of an lvalue in the given state, for a read access (invalid location for a read access are ignored).

Evaluates the function argument of a Call constructor.

val assume_cond : pos:Position.t -> state -> Eval.exp -> bool -> state Eval.or_bottom

assume_cond ~pos state expr b reduces the given abstract state by assuming exp evaluates to:

  • a non-zero value if b is true;
  • zero if b is false.