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 replace_base : Base.substitution -> location -> location
           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 context
           val evaluate :
             subdivided:bool ->
             context ->
             Valuation.t ->
             Cil_types.exp -> (Valuation.t * Value.t) Eval.evaluated
         end)
  ->
  sig
    val evaluate :
      Eva.context ->
      Valuation.t ->
      subdivnb:int -> Cil_types.exp -> (Valuation.t * Value.t) Eval.evaluated
    val reduce_by_enumeration :
      Eva.context ->
      Valuation.t -> Cil_types.exp -> bool -> Valuation.t Eval.or_bottom
  end