functor
  (Value : Value) (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 partially_overlap :
                             location -> location -> bool
                           val check_non_overlapping :
                             (Cil_types.lval * location) list ->
                             (Cil_types.lval * location) list ->
                             unit Eval.evaluated
                           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 reduce_index_by_array_size :
                             size_expr:Cil_types.exp ->
                             index_expr:Cil_types.exp ->
                             Integer.t -> value -> value Eval.evaluated
                           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 reduce_loc_by_validity :
                             for_writing:bool ->
                             bitfield:bool ->
                             Cil_types.lval ->
                             location -> location Eval.evaluated
                           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) (Domain : sig
                                          type state
                                          type value = Value.t
                                          type location = Loc.location
                                          type origin
                                          val extract_expr :
                                            (Cil_types.exp ->
                                             value Eval.evaluated) ->
                                            state ->
                                            Cil_types.exp ->
                                            (value * origin) Eval.evaluated
                                          val extract_lval :
                                            (Cil_types.exp ->
                                             value Eval.evaluated) ->
                                            state ->
                                            Cil_types.lval ->
                                            Cil_types.typ ->
                                            location ->
                                            (value * origin) Eval.evaluated
                                          val backward_location :
                                            state ->
                                            Cil_types.lval ->
                                            Cil_types.typ ->
                                            location ->
                                            value ->
                                            (location * value) Eval.or_bottom
                                          val reduce_further :
                                            state ->
                                            Cil_types.exp ->
                                            value ->
                                            (Cil_types.exp * value) list
                                          type t = state
                                          val ty : t Type.t
                                          val name : string
                                          val descr : t Descr.t
                                          val packed_descr :
                                            Structural_descr.pack
                                          val reprs : t list
                                          val equal : t -> t -> bool
                                          val compare : t -> t -> int
                                          val hash : t -> int
                                          val pretty_code :
                                            Format.formatter -> t -> unit
                                          val internal_pretty_code :
                                            Type.precedence ->
                                            Format.formatter -> t -> unit
                                          val pretty :
                                            Format.formatter -> t -> unit
                                          val varname : t -> string
                                          val mem_project :
                                            (Project_skeleton.t -> bool) ->
                                            t -> bool
                                          val copy : t -> t
                                        end->
  sig
    type state = Domain.state
    type value = Value.t
    type origin = Domain.origin
    type loc = Loc.location
    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 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_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