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
=
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 =
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 =
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 = {
}
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