sig
  module type Forward_Evaluation =
    sig
      type value
      type valuation
      type context
      val evaluate :
        Subdivided_evaluation.Forward_Evaluation.context ->
        Subdivided_evaluation.Forward_Evaluation.valuation ->
        Cil_types.exp ->
        (Subdivided_evaluation.Forward_Evaluation.valuation *
         Subdivided_evaluation.Forward_Evaluation.value)
        Eval.evaluated
    end
  module Make :
    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 context
        val evaluate :
          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
end