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 evaluate :
                                                 ?valuation:Valuation.t ->
                                                 ?reduction:bool ->
                                                 state ->
                                                 Cil_types.exp ->
                                                 (Valuation.t * value)
                                                 Eval.evaluated
                                               val copy_lvalue :
                                                 ?valuation:Valuation.t ->
                                                 state ->
                                                 Cil_types.lval ->
                                                 (Valuation.t *
                                                  value Eval.flagged_value)
                                                 Eval.evaluated
                                               val lvaluate :
                                                 ?valuation:Valuation.t ->
                                                 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 :
                                                 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 location
                                                                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 *
                                                                  Value_types.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 :
                                                                    Value_types.cacheable;
                                                                  builtin :
                                                                    bool;
                                                                }
                                                                val compute_call_ref :
                                                                  (Cil_types.stmt ->
                                                                   (location,
                                                                    value)
                                                                   Eval.call ->
                                                                   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