Module Eval_terms

module Eval_terms: sig .. end
Evaluation of terms and predicates

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


type predicate_status = Abstract_interp.Comp.result = 
| True
| False
| Unknown
Evaluating a predicate. Unknown is the Top of the lattice
val pretty_predicate_status : 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 : 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 Pervasives.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;
   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
val reduce_by_predicate : eval_env -> bool -> Cil_types.predicate -> eval_env