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 -> state list Eval.or_bottom * 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 : state list Eval.or_bottom;
                  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