sig
type predicate_status = True | False | Unknown
val pretty_predicate_status :
Format.formatter -> Eval_terms.predicate_status -> unit
val join_predicate_status :
Eval_terms.predicate_status ->
Eval_terms.predicate_status -> Eval_terms.predicate_status
val join_list_predicate_status :
Eval_terms.predicate_status list -> Eval_terms.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
val pretty_logic_evaluation_error :
Format.formatter -> Eval_terms.logic_evaluation_error -> unit
exception LogicEvalError of Eval_terms.logic_evaluation_error
type labels_states = Cvalue.Model.t Cil_datatype.Logic_label.Map.t
type eval_env
val env_pre_f : pre:Cvalue.Model.t -> unit -> Eval_terms.eval_env
val env_annot :
?c_labels:Eval_terms.labels_states ->
pre:Cvalue.Model.t -> here:Cvalue.Model.t -> unit -> Eval_terms.eval_env
val env_post_f :
?c_labels:Eval_terms.labels_states ->
pre:Cvalue.Model.t ->
post:Cvalue.Model.t ->
result:Cil_types.varinfo option -> unit -> Eval_terms.eval_env
val env_assigns : pre:Cvalue.Model.t -> Eval_terms.eval_env
val env_only_here : Cvalue.Model.t -> Eval_terms.eval_env
val env_current_state : Eval_terms.eval_env -> Cvalue.Model.t
type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
val eval_tlval_as_zone_under_over :
with_alarms:CilE.warn_mode ->
for_writing:bool ->
Eval_terms.eval_env ->
Cil_types.term -> Locations.Zone.t * Locations.Zone.t
type 'a eval_result = {
etype : Cil_types.typ;
eunder : 'a;
eover : 'a;
ldeps : Eval_terms.logic_deps;
}
val eval_term :
with_alarms:CilE.warn_mode ->
Eval_terms.eval_env ->
Cil_types.term -> Cvalue.V.t Eval_terms.eval_result
val eval_tlval :
with_alarms:CilE.warn_mode ->
Eval_terms.eval_env ->
Cil_types.term -> Locations.Location_Bits.t Eval_terms.eval_result
val eval_tlval_as_location :
with_alarms:CilE.warn_mode ->
Eval_terms.eval_env -> Cil_types.term -> Locations.location
val eval_tlval_as_zone :
with_alarms:CilE.warn_mode ->
for_writing:bool ->
Eval_terms.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_terms.eval_env ->
Cil_types.term -> Cil_datatype.Typ.t * Locations.location
val eval_predicate :
Eval_terms.eval_env ->
Cil_types.predicate Cil_types.named -> Eval_terms.predicate_status
val predicate_deps :
Eval_terms.eval_env ->
Cil_types.predicate Cil_types.named -> Eval_terms.logic_deps
val reduce_by_predicate :
Eval_terms.eval_env ->
bool -> Cil_types.predicate Cil_types.named -> Eval_terms.eval_env
val split_disjunction_and_reduce :
reduce:bool ->
env:Eval_terms.eval_env ->
Cvalue.Model.t * Trace.t ->
slevel:int ->
Cil_types.predicate Cil_types.named -> Property.t -> State_set.t
end