functor
  (Domain : Abstract_domain.Transfer) (Eva : sig
                                               type state = Domain.state
                                               type value = Domain.value
                                               type origin
                                               type loc = Domain.location
                                               module Valuation :
                                                 sig
                                                   type t = Domain.valuation
                                                   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 filter :
                                                     (Cil_types.exp ->
                                                      (value, origin)
                                                      Eval.record_val -> 
                                                      bool) ->
                                                     (Cil_types.lval ->
                                                      loc Eval.record_loc ->
                                                      bool) ->
                                                     t -> t
                                                 end
                                               val evaluate :
                                                 ?valuation:Valuation.t ->
                                                 ?indeterminate:bool ->
                                                 ?reduction:bool ->
                                                 state ->
                                                 Cil_types.exp ->
                                                 (Valuation.t * 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 loc_size :
                                                 loc -> Int_Base.t
                                               val reinterpret :
                                                 Cil_types.exp ->
                                                 Cil_types.typ ->
                                                 value ->
                                                 value Eval.evaluated
                                               val do_promotion :
                                                 src_typ:Cil_types.typ ->
                                                 dst_typ:Cil_types.typ ->
                                                 Cil_types.exp ->
                                                 value ->
                                                 value Eval.evaluated
                                               val split_by_evaluation :
                                                 Cil_types.exp ->
                                                 Integer.t list ->
                                                 state list ->
                                                 (Integer.t * state list *
                                                  bool)
                                                 list * state list
                                               val check_copy_lval :
                                                 Cil_types.lval * loc ->
                                                 Cil_types.lval * loc ->
                                                 bool Eval.evaluated
                                               val check_non_overlapping :
                                                 state ->
                                                 Cil_types.lval list ->
                                                 Cil_types.lval list ->
                                                 unit Eval.evaluated
                                               val eval_function_exp :
                                                 Cil_types.exp ->
                                                 state ->
                                                 (Kernel_function.t *
                                                  Valuation.t)
                                                 list Eval.evaluated
                                             end->
  sig
    type state = Domain.state
    type value = Domain.value
    type summary = Domain.summary
    val assign :
      with_alarms:CilE.warn_mode ->
      state ->
      Cil_types.kernel_function ->
      Cil_types.stmt ->
      Cil_types.lval -> Cil_types.exp -> state Eval.or_bottom
    val assume :
      with_alarms:CilE.warn_mode ->
      state ->
      Cil_types.stmt -> Cil_types.exp -> bool -> state Eval.or_bottom
    val call :
      with_alarms:CilE.warn_mode ->
      Cil_types.stmt ->
      Cil_types.lval option ->
      Cil_types.exp ->
      Cil_types.exp list ->
      state -> state list Eval.or_bottom * Value_types.cacheable
    val return :
      with_alarms:CilE.warn_mode ->
      Cil_types.kernel_function ->
      Cil_types.stmt ->
      Cil_types.lval option ->
      state -> (state, summary, value) Eval.return Eval.or_bottom
    val split_final_states :
      Cil_types.kernel_function ->
      Cil_types.exp -> Integer.t list -> state list -> state list list
    val check_unspecified_sequence :
      with_alarms:CilE.warn_mode ->
      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
    type res =
        (state, summary, value) Eval.call_result * Value_types.cacheable
    val compute_call_ref :
      (Cil_types.kinstr -> value Eval.call -> state -> res) ref
  end