module Eval_terms:sig
..end
Evaluation of terms and predicates
typepredicate_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 |
| |
UnsupportedLogicVar of |
| |
AstError of |
| |
NoEnv of |
| |
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
typelabels_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
typelogic_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 |
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 : |
|
eunder : |
|
eover : |
|
empty : |
|
ldeps : |
}
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
val reduce_by_predicate : eval_env -> bool -> Cil_types.predicate -> eval_env