Frama-C API - `X`

The four abstractions: values, locations, states and evaluation context, plus the evaluation engine for these abstractions.

module Ctx : sig ... end

module Val : sig ... end

module Loc : sig ... end

module Dom : sig ... end

module Eval : sig ... end

module Compute : sig ... end

module Interferences : sig ... end

Access to abstract states inferred by the analysis

val get_global_state : unit -> Dom.state Eva.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 Eva.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:Eva.Callstack.t list -> after:bool -> Frama_c_kernel.Cil_types.stmt -> Dom.state Eva.Callstack.Hashtbl.t Eva.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.

val get_initial_state : Frama_c_kernel.Cil_types.kernel_function -> Dom.state Eva.Eval.or_top_bottom

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:Eva.Callstack.t list -> Frama_c_kernel.Cil_types.kernel_function -> Dom.state Eva.Callstack.Hashtbl.t Eva.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 : Dom.state -> Eva.Eval.exp -> Val.t Eva.Eval.evaluated

Evaluates the value of an expression in the given state.

val copy_lvalue : Dom.state -> Eva.Eval.lval -> Val.t Eva.Eval.flagged_value Eva.Eval.evaluated

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 -> Eva.Eval.lval -> Loc.location Eva.Eval.evaluated

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

val eval_function_exp : Dom.state -> ?args:Eva.Eval.exp list -> Eva.Eval.exp -> Frama_c_kernel.Cil_types.kernel_function list Eva.Eval.evaluated

Evaluates the function argument of a Call constructor.

val assume_cond : Frama_c_kernel.Cil_types.stmt -> Dom.state -> Eva.Eval.exp -> bool -> Dom.state Eva.Eval.or_bottom

assume_cond stmt 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.

Frama-C API - X

Access to abstract states inferred by the analysis

Shortcuts for the evaluation in an abstract state

Frama-C API - `X`