module Eval_terms: sig
.. end
Evaluation of terms and predicates
Truth values for a predicate analyzed by the value analysis
type
predicate_status =
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
val join_list_predicate_status : predicate_status list -> 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 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
val eval_tlval_as_zone_under_over : with_alarms:CilE.warn_mode ->
for_writing:bool ->
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 : with_alarms:CilE.warn_mode ->
eval_env -> Cil_types.term -> Cvalue.V.t eval_result
val eval_tlval : with_alarms:CilE.warn_mode ->
eval_env ->
Cil_types.term -> Locations.Location_Bits.t eval_result
val eval_tlval_as_location : with_alarms:CilE.warn_mode ->
eval_env -> Cil_types.term -> Locations.location
val eval_tlval_as_zone : with_alarms:CilE.warn_mode ->
for_writing:bool -> eval_env -> Cil_types.term -> Locations.Zone.t
exception Not_an_exact_loc
val eval_term_as_exact_locs : with_alarms:CilE.warn_mode ->
eval_env ->
Cil_types.term -> Cil_datatype.Typ.t * Locations.location
val eval_predicate : eval_env ->
Cil_types.predicate Cil_types.named -> predicate_status
val predicate_deps : eval_env ->
Cil_types.predicate Cil_types.named -> logic_deps
val reduce_by_predicate : eval_env ->
bool -> Cil_types.predicate Cil_types.named -> eval_env
val split_disjunction_and_reduce : reduce:bool ->
env:eval_env ->
Cvalue.Model.t * Trace.t ->
slevel:int ->
Cil_types.predicate Cil_types.named -> Property.t -> State_set.t
If reduce
is true, reduce in all cases. Otherwise, reduce only
when p
is a disjunction, ie. split by this disjunction.
The Property is the one in which is p
.