Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eval_terms

Evaluation of terms and predicates

type predicate_status = Frama_c_kernel.Abstract_interp.Comp.result =
  1. | True
  2. | False
  3. | Unknown

Evaluating a predicate. Unknown is the Top of the lattice

val join_predicate_status : predicate_status -> predicate_status -> predicate_status
type logic_evaluation_error =
  1. | Unsupported of string
  2. | UnsupportedLogicVar of Frama_c_kernel.Cil_types.logic_var
  3. | AstError of string
  4. | NoEnv of Frama_c_kernel.Cil_types.logic_label
  5. | NoResult
  6. | CAlarm

Error during the evaluation of a term or a predicate

val pretty_logic_evaluation_error : Stdlib.Format.formatter -> logic_evaluation_error -> unit
exception LogicEvalError of logic_evaluation_error
type eval_env

Evaluation environment. Currently available are function Pre and Post, or the environment to evaluate an annotation.

val env_pre_f : pre:Frama_c_kernel.Cvalue.Model.t -> unit -> eval_env
val env_annot : ?c_labels:labels_states -> pre:Frama_c_kernel.Cvalue.Model.t -> here:Frama_c_kernel.Cvalue.Model.t -> unit -> eval_env
val env_post_f : ?c_labels:labels_states -> pre:Frama_c_kernel.Cvalue.Model.t -> post:Frama_c_kernel.Cvalue.Model.t -> result:Frama_c_kernel.Cil_types.varinfo option -> unit -> eval_env
val env_assigns : pre:Frama_c_kernel.Cvalue.Model.t -> eval_env

Used by auxiliary plugins, that do not supply the other states

val env_current_state : eval_env -> Frama_c_kernel.Cvalue.Model.t

Dependencies needed to evaluate a term or a predicate

type alarm_mode =
  1. | Ignore
  2. | Fail
  3. | Track of bool Stdlib.ref

Three modes to handle the alarms when evaluating a logical term.

Return a pair of (under-approximating, over-approximating) zones.

type 'a eval_result = {
  1. etype : Frama_c_kernel.Cil_types.typ;
  2. eunder : 'a;
  3. eover : 'a;
  4. empty : bool;
  5. ldeps : logic_deps;
}
val predicate_deps : eval_env -> Frama_c_kernel.Cil_types.predicate -> logic_deps option

predicate_deps env p computes the logic dependencies needed to evaluate p in the given evaluation environment env. Returns None on either an evaluation error or on unsupported construct.

tlval_deps env t computes the logic dependencies needed to evaluate the address of lvalue term t in the given evaluation environment env.

  • raises LogicEvalError

    on evaluation errors, unsupported constructs, or if t is not an lvalue term.

val reduce_by_predicate : eval_env -> bool -> Frama_c_kernel.Cil_types.predicate -> eval_env