sig
  type predicate_status =
    Abstract_interp.Comp.result =
      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
  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 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 Pervasives.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