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 -> 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   val split_disjunction_and_reduce :     reduce:bool ->     env:Eval_terms.eval_env ->     Cvalue.Model.t * Trace.t ->     slevel:int -> Cil_types.predicate -> Property.t -> State_set.t end