Frama-C:
Plug-ins:
Libraries:

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.

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

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.

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:Eva__.Position.t -> Dom.state -> Eva.Eval.exp -> bool -> Dom.state Eva.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.