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 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) (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 eval_function_exp :
      Cil_types.exp ->
      ?args:Cil_types.exp list ->
      state -> (Kernel_function.t * Valuation.t) list Eval.evaluated
    val interpret_truth :
      alarm:(unit -> Alarms.t) ->
      '-> 'Abstract_value.truth -> 'Eval.evaluated
  end