sig
type predicate_status =
Abstract_interp.Comp.result =
True
| False
| Unknown
val pretty_predicate_status :
Stdlib.Format.formatter -> Eval_terms.predicate_status -> unit
val join_predicate_status :
Eval_terms.predicate_status ->
Eval_terms.predicate_status -> 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 :
Stdlib.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 make_env :
Cvalue.Model.t Abstract_domain.logic_environment ->
Cvalue.Model.t -> Eval_terms.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
type alarm_mode = Ignore | Fail | Track of bool Stdlib.ref
val eval_tlval_as_zone_under_over :
alarm_mode:Eval_terms.alarm_mode ->
Locations.access ->
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 :
alarm_mode:Eval_terms.alarm_mode ->
Eval_terms.eval_env ->
Cil_types.term -> Cvalue.V.t Eval_terms.eval_result
val eval_tlval_as_location :
alarm_mode:Eval_terms.alarm_mode ->
Eval_terms.eval_env -> Cil_types.term -> Locations.location
val eval_tlval_as_zone :
alarm_mode:Eval_terms.alarm_mode ->
Locations.access ->
Eval_terms.eval_env -> Cil_types.term -> Locations.Zone.t
val eval_predicate :
Eval_terms.eval_env -> Cil_types.predicate -> Eval_terms.predicate_status
val predicate_deps :
Eval_terms.eval_env -> Cil_types.predicate -> Eval_terms.logic_deps
val reduce_by_predicate :
Eval_terms.eval_env -> bool -> Cil_types.predicate -> Eval_terms.eval_env
end