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 replace_base : Base.substitution -> location -> location
           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 :
                oracle:(Cil_types.exp -> value Eval.evaluated) ->
                Abstract_domain.evaluation_context ->
                state ->
                Cil_types.exp -> (value * origin option) Eval.evaluated
              val extract_lval :
                oracle:(Cil_types.exp -> value Eval.evaluated) ->
                Abstract_domain.evaluation_context ->
                state ->
                Cil_types.lval ->
                Cil_types.typ ->
                location -> (value * origin option) 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 to_domain_valuation :
      Valuation.t -> (value, loc, origin) Abstract_domain.valuation
    val evaluate :
      ?valuation:Valuation.t ->
      ?reduction:bool ->
      ?subdivnb:int ->
      state -> Cil_types.exp -> (Valuation.t * value) Eval.evaluated
    val copy_lvalue :
      ?valuation:Valuation.t ->
      ?subdivnb:int ->
      state ->
      Cil_types.lval ->
      (Valuation.t * value Eval.flagged_value) Eval.evaluated
    val lvaluate :
      ?valuation:Valuation.t ->
      ?subdivnb:int ->
      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 :
      ?subdivnb:int ->
      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