sig
  module Make :
    functor
      (Value : Abstract_value.External) (Eva : sig
                                                 type state
                                                 type value = Value.t
                                                 type origin
                                                 type loc
                                                 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 can_copy :
                                                   ?valuation:Valuation.t ->
                                                   is_ret:bool ->
                                                   state ->
                                                   Kernel_function.t ->
                                                   Cil_types.lval ->
                                                   Cil_types.exp ->
                                                   (Cil_types.lval option *
                                                    Valuation.t)
                                                   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 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 = Eva.state
        type value = Value.t
        type origin = Eva.origin
        type loc = Eva.loc
        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 can_copy :
          ?valuation:Valuation.t ->
          is_ret:bool ->
          state ->
          Kernel_function.t ->
          Cil_types.lval ->
          Cil_types.exp ->
          (Cil_types.lval option * Valuation.t) 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 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
end