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