sig
  type t
  val backward_location :
    Domain_builder.LeafDomain.t ->
    Cil_types.lval ->
    Cil_types.typ -> 'loc -> '-> ('loc * 'v) Eval.or_bottom
  val reduce_further :
    Domain_builder.LeafDomain.t ->
    Cil_types.exp -> '-> (Cil_types.exp * 'v) list
  val evaluate_predicate :
    Domain_builder.LeafDomain.t Abstract_domain.logic_environment ->
    Domain_builder.LeafDomain.t -> Cil_types.predicate -> Alarmset.status
  val reduce_by_predicate :
    Domain_builder.LeafDomain.t Abstract_domain.logic_environment ->
    Domain_builder.LeafDomain.t ->
    Cil_types.predicate -> bool -> Domain_builder.LeafDomain.t Eval.or_bottom
  val interpret_acsl_extension :
    Cil_types.acsl_extension ->
    Domain_builder.LeafDomain.t Abstract_domain.logic_environment ->
    Domain_builder.LeafDomain.t -> Domain_builder.LeafDomain.t
  val enter_loop :
    Cil_types.stmt ->
    Domain_builder.LeafDomain.t -> Domain_builder.LeafDomain.t
  val incr_loop_counter :
    Cil_types.stmt ->
    Domain_builder.LeafDomain.t -> Domain_builder.LeafDomain.t
  val leave_loop :
    Cil_types.stmt ->
    Domain_builder.LeafDomain.t -> Domain_builder.LeafDomain.t
  val filter :
    Cil_types.kernel_function ->
    [ `Post | `Pre ] ->
    Base.Hptset.t ->
    Domain_builder.LeafDomain.t -> Domain_builder.LeafDomain.t
  val reuse :
    Cil_types.kernel_function ->
    Base.Hptset.t ->
    current_input:Domain_builder.LeafDomain.t ->
    previous_output:Domain_builder.LeafDomain.t ->
    Domain_builder.LeafDomain.t
  val show_expr :
    '->
    Domain_builder.LeafDomain.t ->
    Stdlib.Format.formatter -> Cil_types.exp -> unit
  val post_analysis :
    Domain_builder.LeafDomain.t Lattice_bounds.or_bottom -> unit
  module Store :
    sig
      val register_global_state : bool -> t Eval.or_bottom -> unit
      val register_initial_state : Value_types.callstack -> t -> unit
      val register_state_before_stmt :
        Value_types.callstack -> Cil_types.stmt -> t -> unit
      val register_state_after_stmt :
        Value_types.callstack -> Cil_types.stmt -> t -> unit
      val get_global_state : unit -> t Eval.or_bottom
      val get_initial_state : Cil_types.kernel_function -> t Eval.or_bottom
      val get_initial_state_by_callstack :
        ?selection:Eval.callstack list ->
        Cil_types.kernel_function ->
        t Value_types.Callstack.Hashtbl.t Eval.or_top_bottom
      val get_stmt_state : after:bool -> Cil_types.stmt -> t Eval.or_bottom
      val get_stmt_state_by_callstack :
        ?selection:Eval.callstack list ->
        after:bool ->
        Cil_types.stmt ->
        t Value_types.Callstack.Hashtbl.t Eval.or_top_bottom
      val mark_as_computed : unit -> unit
      val is_computed : unit -> bool
    end
  val key : Domain_builder.LeafDomain.t Abstract_domain.key
end