sig
  module type S =
    sig
      type state
      val initial_state :
        lib_entry:bool -> Initialization.S.state Bottom.Type.or_bottom
      val initial_state_with_formals :
        lib_entry:bool ->
        Cil_types.kernel_function ->
        Initialization.S.state Bottom.Type.or_bottom
      val initialize_local_variable :
        Cil_types.stmt ->
        Cil_types.varinfo ->
        Cil_types.init ->
        Initialization.S.state ->
        Initialization.S.state Bottom.Type.or_bottom
    end
  module Make :
    functor (Domain : Abstract.Domain.External)
      (Eva : sig
               type state = Domain.state
               type value
               type origin
               type loc = Domain.location
               module Valuation :
                 sig
                   type t
                   type value = value
                   type origin = origin
                   type loc = loc
                   val empty : t
                   val find :
                     t ->
                     Cil_types.exp ->
                     (value, origin) Eval.record_val Eval.or_top
                   val add :
                     t ->
                     Cil_types.exp -> (value, origin) Eval.record_val -> t
                   val fold :
                     (Cil_types.exp ->
                      (value, origin) Eval.record_val -> '-> 'a) ->
                     t -> '-> 'a
                   val find_loc :
                     t -> Cil_types.lval -> loc Eval.record_loc Eval.or_top
                   val remove : t -> Cil_types.exp -> t
                   val remove_loc : t -> Cil_types.lval -> t
                 end
               val to_domain_valuation :
                 Valuation.t ->
                 (value, loc, origin) Abstract_domain.valuation
               val evaluate :
                 ?valuation:Valuation.t ->
                 ?reduction:bool ->
                 ?subdivnb:int ->
                 state ->
                 Cil_types.exp -> (Valuation.t * value) Eval.evaluated
               val copy_lvalue :
                 ?valuation:Valuation.t ->
                 ?subdivnb:int ->
                 state ->
                 Cil_types.lval ->
                 (Valuation.t * value Eval.flagged_value) Eval.evaluated
               val lvaluate :
                 ?valuation:Valuation.t ->
                 ?subdivnb:int ->
                 for_writing:bool ->
                 state ->
                 Cil_types.lval ->
                 (Valuation.t * loc * Cil_types.typ) Eval.evaluated
               val reduce :
                 ?valuation:Valuation.t ->
                 state -> Cil_types.exp -> bool -> Valuation.t Eval.evaluated
               val assume :
                 ?valuation:Valuation.t ->
                 state ->
                 Cil_types.exp -> value -> Valuation.t Eval.or_bottom
               val eval_function_exp :
                 ?subdivnb:int ->
                 Cil_types.exp ->
                 ?args:Cil_types.exp list ->
                 state ->
                 (Kernel_function.t * Valuation.t) list Eval.evaluated
               val interpret_truth :
                 alarm:(unit -> Alarms.t) ->
                 '-> 'Abstract_value.truth -> 'Eval.evaluated
             end)
      (Transfer : sig
                    type state = Domain.t
                    type value
                    type loc
                    val assign :
                      state ->
                      Cil_types.kinstr ->
                      Cil_types.lval -> Cil_types.exp -> state Eval.or_bottom
                    val assume :
                      state ->
                      Cil_types.stmt ->
                      Cil_types.exp -> bool -> state Eval.or_bottom
                    val call :
                      Cil_types.stmt ->
                      Cil_types.lval option ->
                      Cil_types.exp ->
                      Cil_types.exp list ->
                      state -> (Partition.key * state) list * Eval.cacheable
                    val check_unspecified_sequence :
                      Cil_types.stmt ->
                      state ->
                      (Cil_types.stmt * Cil_types.lval list *
                       Cil_types.lval list * Cil_types.lval list *
                       Cil_types.stmt ref list)
                      list -> unit Eval.or_bottom
                    val enter_scope :
                      Cil_types.kernel_function ->
                      Cil_types.varinfo list -> state -> state
                    type call_result = {
                      states : (Partition.key * state) list;
                      cacheable : Eval.cacheable;
                      builtin : bool;
                    }
                    val compute_call_ref :
                      (Cil_types.stmt ->
                       (loc, value) Eval.call ->
                       Eval.recursion option -> state -> call_result)
                      ref
                  end)
      ->
      sig
        val initial_state : lib_entry:bool -> Domain.t Bottom.Type.or_bottom
        val initial_state_with_formals :
          lib_entry:bool ->
          Cil_types.kernel_function -> Domain.t Bottom.Type.or_bottom
        val initialize_local_variable :
          Cil_types.stmt ->
          Cil_types.varinfo ->
          Cil_types.init -> Domain.t -> Domain.t Bottom.Type.or_bottom
      end
end