Module Eval_terms

module Eval_terms: sig .. end
Truth values for a predicate analyzed by the value analysis

Evaluation of terms and predicates



Truth values for a predicate analyzed by the value analysis
type predicate_status = 
| True
| False
| Unknown
Evaluating a predicate. Unknown is the Top of the lattice
val string_of_predicate_status : predicate_status -> string
val pretty_predicate_status : Format.formatter -> predicate_status -> unit
val join_predicate_status : predicate_status ->
predicate_status -> predicate_status
exception Stop
val join_list_predicate_status : predicate_status list -> 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
val unsupported : string -> 'a
val unsupported_lvar : Cil_types.logic_var -> 'a
val ast_error : string -> 'a
val no_env : Cil_types.logic_label -> 'a
val no_result : unit -> 'a
val c_alarm : unit -> 'a
val display_evaluation_error : logic_evaluation_error -> unit
val warn_raise_mode : CilE.warn_mode

Evaluation environments. Used to evaluate predicate on \at nodes
type labels_states = Cvalue.Model.t Cil_datatype.Logic_label.Map.t 
val join_label_states : Cvalue.Model.t Cil_datatype.Logic_label.Map.t ->
Cvalue.Model.t Cil_datatype.Logic_label.Map.t ->
Cvalue.Model.t Cil_datatype.Logic_label.Map.t
type eval_env = {
   e_cur : Cil_types.logic_label;
   e_states : labels_states;
   result : Cil_types.varinfo option;
}
Evaluation environment. Currently available are function Pre and Post, or the environment to evaluate an annotation
val join_env : eval_env -> eval_env -> eval_env
val env_state : eval_env -> Cil_datatype.Logic_label.Map.key -> Cvalue.Model.t
val env_current_state : eval_env -> Cvalue.Model.t
val overwrite_state : eval_env ->
Cvalue.Model.t -> Cil_datatype.Logic_label.Map.key -> eval_env
val overwrite_current_state : eval_env -> Cvalue.Model.t -> eval_env
val lbl_here : Cil_types.logic_label
val add_logic : Cil_datatype.Logic_label.Map.key ->
Cvalue.Model.t -> labels_states -> labels_states
val add_here : Cvalue.Model.t -> labels_states -> labels_states
val add_pre : Cvalue.Model.t -> labels_states -> labels_states
val add_post : Cvalue.Model.t -> labels_states -> labels_states
val add_old : Cvalue.Model.t -> labels_states -> labels_states
val add_init : labels_states -> labels_states
val env_pre_f : ?c_labels:labels_states ->
pre: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_annot : ?c_labels:labels_states ->
pre:Cvalue.Model.t -> here:Cvalue.Model.t -> 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 supported_logic_var : Cil_types.logic_var -> Base.t * Cil_types.typ
val bind_logic_vars : eval_env -> Cil_types.logic_var list -> eval_env
val unbind_logic_vars : eval_env -> Cil_types.logic_var list -> eval_env
val lop_to_cop : Cil_types.relation -> Cil_types.binop
val isLogicNonCompositeType : Cil_types.logic_type -> bool
val infer_type : Cil_types.logic_type -> Cil_types.typ
val same_etype : Cil_datatype.Typ.t -> Cil_datatype.Typ.t -> bool
val real_mode : Ival.Float_abstract.rounding_mode
val infer_binop_res_type : Cil_types.binop -> Cil_types.typ -> Cil_types.typ
type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t 
Dependencies needed to evaluate a term or a predicate
val deps_at : Cil_datatype.Logic_label.Map.key -> logic_deps -> Locations.Zone.t
val add_deps : Cil_datatype.Logic_label.Map.key ->
logic_deps -> Locations.Zone.t -> logic_deps
val join_logic_deps : logic_deps -> logic_deps -> logic_deps
val empty_logic_deps : Locations.Zone.t Cil_datatype.Logic_label.Map.t
type 'a eval_result = {
   etype : Cil_types.typ;
   eunder : 'a;
   eover : 'a;
   ldeps : logic_deps;
}
val under_from_over : Cvalue.V.t -> Cvalue.V.t
val is_noop_cast : src_typ:Cil_types.logic_type -> dst_typ:Cil_types.typ -> bool
val einteger : Cvalue.V.t -> Cvalue.V.t eval_result
val ereal : Cvalue.V.t -> Cvalue.V.t eval_result
val eval_term : with_alarms:CilE.warn_mode ->
eval_env -> Cil_types.term -> Cvalue.V.t eval_result
val eval_binop : with_alarms:CilE.warn_mode ->
eval_env ->
Cil_types.binop ->
Cil_types.term -> Cil_types.term -> Cvalue.V.t eval_result
val eval_tlhost : with_alarms:CilE.warn_mode ->
eval_env ->
Cil_types.term_lhost -> Locations.Location_Bits.t eval_result
val eval_toffset : with_alarms:CilE.warn_mode ->
eval_env ->
Cil_types.typ -> Cil_types.term_offset -> Ival.t eval_result
val eval_thost_toffset : with_alarms:CilE.warn_mode ->
eval_env ->
Cil_types.term_lhost ->
Cil_types.term_offset -> Locations.Location_Bits.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_location_with_deps : with_alarms:CilE.warn_mode ->
eval_env ->
Cil_types.term -> Locations.location * logic_deps
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.
val eval_tlval_as_zone : with_alarms:CilE.warn_mode ->
for_writing:bool -> eval_env -> Cil_types.term -> Locations.Zone.t
val pass_logic_cast : exn -> Cil_types.logic_type -> Cil_types.term -> unit
exception Not_an_exact_loc
val eval_term_as_exact_loc : with_alarms:CilE.warn_mode ->
eval_env -> Cil_types.term -> Cil_types.typ * Locations.location
exception DoNotReduce
exception Reduce_to_bottom
val is_same_term_coerce : Cil_types.term -> Cil_types.term -> bool
val reduce_by_predicate : eval_env ->
bool -> Cil_types.predicate Cil_types.named -> eval_env
val reduce_by_predicate_content : eval_env -> bool -> Cil_types.predicate -> eval_env
val reduce_by_valid : eval_env ->
bool -> for_writing:bool -> Cil_types.term -> eval_env
val reduce_by_relation : eval_env ->
bool ->
Cil_types.term -> Cil_types.relation -> Cil_types.term -> eval_env
val reduce_by_left_relation : eval_env ->
bool ->
Cil_types.term -> Cil_types.relation -> Cil_types.term -> eval_env
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
exception Does_not_improve
val fold_on_disjunction : (Cil_types.predicate Cil_types.named -> 'a -> 'a) ->
Cil_types.predicate Cil_types.named -> 'a -> 'a
val count_disjunction : Cil_types.predicate Cil_types.named -> int
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.