Frama-C:
Plug-ins:
Libraries:

Frama-C API - Engine

include Engine_abstractions_sig.S
module Dom : Engine_abstractions_sig.Domain with type value = Val.t and type location = Loc.location and type context = Ctx.t
module Eval : Evaluation_sig.S with type state = Dom.t and type context = Ctx.t and type value = Val.t and type loc = Loc.location and type origin = Dom.origin
include Engine_sig.Results with type state := Dom.state and type value := Val.t and type location := Loc.location

Access to abstract states inferred by the analysis

val get_global_state : unit -> Dom.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 -> Dom.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 -> Dom.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.

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 : Dom.state -> Eval.exp -> Val.t 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 : Dom.state -> Eval.lval -> Loc.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 -> Dom.state -> Eval.exp -> bool -> Dom.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.