functor
  (Value : Abstract_value.External) (Loc : sig
                                             type value = Value.t
                                             type location
                                             type offset
                                             val top : location
                                             val equal_loc :
                                               location -> location -> bool
                                             val equal_offset :
                                               offset -> offset -> bool
                                             val pretty_loc :
                                               Format.formatter ->
                                               location -> unit
                                             val pretty_offset :
                                               Format.formatter ->
                                               offset -> unit
                                             val to_value : location -> value
                                             val size :
                                               location -> Int_Base.t
                                             val assume_no_overlap :
                                               partial:bool ->
                                               location ->
                                               location ->
                                               (location * location)
                                               Abstract_location.truth
                                             val assume_valid_location :
                                               for_writing:bool ->
                                               bitfield:bool ->
                                               location ->
                                               location
                                               Abstract_location.truth
                                             val no_offset : offset
                                             val forward_field :
                                               Cil_types.typ ->
                                               Cil_types.fieldinfo ->
                                               offset -> offset
                                             val forward_index :
                                               Cil_types.typ ->
                                               value -> offset -> offset
                                             val forward_variable :
                                               Cil_types.typ ->
                                               Cil_types.varinfo ->
                                               offset ->
                                               location Eval.or_bottom
                                             val forward_pointer :
                                               Cil_types.typ ->
                                               value ->
                                               offset ->
                                               location Eval.or_bottom
                                             val eval_varinfo :
                                               Cil_types.varinfo -> location
                                             val backward_variable :
                                               Cil_types.varinfo ->
                                               location ->
                                               offset Eval.or_bottom
                                             val backward_pointer :
                                               value ->
                                               offset ->
                                               location ->
                                               (value * offset)
                                               Eval.or_bottom
                                             val backward_field :
                                               Cil_types.typ ->
                                               Cil_types.fieldinfo ->
                                               offset ->
                                               offset Eval.or_bottom
                                             val backward_index :
                                               Cil_types.typ ->
                                               index:value ->
                                               remaining:offset ->
                                               offset ->
                                               (value * offset)
                                               Eval.or_bottom
                                           end) (Valuation : sig
                                                               type t
                                                               type value =
                                                                   Value.t
                                                               type origin
                                                               type loc =
                                                                   Loc.location
                                                               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) (Eva : 
  sig
    type state
    val evaluate :
      ?valuation:Valuation.t ->
      fuel:int ->
      state -> Cil_types.exp -> (Valuation.t * Value.t) Eval.evaluated
  end->
  sig
    val evaluate :
      ?valuation:Valuation.t ->
      fuel:int ->
      Eva.state -> Cil_types.exp -> (Valuation.t * Value.t) Eval.evaluated
    val reduce_by_enumeration :
      Valuation.t ->
      Eva.state -> Cil_types.exp -> bool -> Valuation.t Eval.or_bottom
  end