Module Eval_terms

module Eval_terms: sig .. end

Evaluation of terms and predicates


type predicate_status = Abstract_interp.Comp.result = 
| True
| False
| Unknown

Evaluating a predicate. Unknown is the Top of the lattice

val pretty_predicate_status : Stdlib.Format.formatter -> predicate_status -> unit
val join_predicate_status : predicate_status ->
predicate_status -> predicate_status
type logic_evaluation_error = 
| Unsupported of string
| UnsupportedLogicVar of Cil_types.logic_var
| AstError of string
| NoEnv of Cil_types.logic_label
| NoResult
| 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 labels_states = Cvalue.Model.t Cil_datatype.Logic_label.Map.t 
type eval_env 

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

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

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

val env_current_state : eval_env -> Cvalue.Model.t
type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t 

Dependencies needed to evaluate a term or a predicate

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

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

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

val eval_tlval_as_zone_under_over : alarm_mode:alarm_mode ->
Locations.access ->
eval_env -> Cil_types.term -> Locations.Zone.t * Locations.Zone.t

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

type 'a eval_result = {
   etype : Cil_types.typ;
   eunder : 'a;
   eover : 'a;
   empty : bool;
   ldeps : logic_deps;
}
val eval_term : alarm_mode:alarm_mode ->
eval_env -> Cil_types.term -> Cvalue.V.t eval_result
val eval_tlval_as_location : alarm_mode:alarm_mode ->
eval_env -> Cil_types.term -> Locations.location
val eval_tlval_as_zone : alarm_mode:alarm_mode ->
Locations.access -> eval_env -> Cil_types.term -> Locations.Zone.t
val eval_predicate : eval_env -> Cil_types.predicate -> predicate_status
val predicate_deps : eval_env -> 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.

val reduce_by_predicate : eval_env -> bool -> Cil_types.predicate -> eval_env
val annot_predicate_deps : pre:Cvalue.Model.t ->
here:Cvalue.Model.t -> Cil_types.predicate -> Locations.Zone.t option

annot_predicate_deps ~pre ~here p computes the logic dependencies needed to evaluate the predicate p in a code annotation in cvalue state here, in a function whose pre-state is pre. Returns None on either an evaluation error or on unsupported construct.