sig
  module type Code =
    sig
      type loc
      val equal_obj :
        Ctypes.c_object ->
        LogicAssigns.Code.loc Memory.value ->
        LogicAssigns.Code.loc Memory.value -> Lang.F.pred
    end
  module type Logic =
    sig
      type loc
      val vars : LogicAssigns.Logic.loc Memory.sloc list -> Lang.F.Vars.t
      val pp_logic :
        Format.formatter -> LogicAssigns.Logic.loc Memory.logic -> unit
      val pp_sloc :
        Format.formatter -> LogicAssigns.Logic.loc Memory.sloc -> unit
      val pp_region :
        Format.formatter -> LogicAssigns.Logic.loc Memory.sloc list -> unit
    end
  module Make :
    functor
      (M : Memory.Model) (C : sig
                                type loc = M.loc
                                val equal_obj :
                                  Ctypes.c_object ->
                                  loc Memory.value ->
                                  loc Memory.value -> Lang.F.pred
                              end) (L : sig
                                          type loc = M.loc
                                          val vars :
                                            loc Memory.sloc list ->
                                            Lang.F.Vars.t
                                          val pp_logic :
                                            Format.formatter ->
                                            loc Memory.logic -> unit
                                          val pp_sloc :
                                            Format.formatter ->
                                            loc Memory.sloc -> unit
                                          val pp_region :
                                            Format.formatter ->
                                            loc Memory.sloc list -> unit
                                        end->
      sig
        type region = (Ctypes.c_object * M.loc Memory.sloc list) list
        val vars : LogicAssigns.Make.region -> Lang.F.Vars.t
        val domain : LogicAssigns.Make.region -> M.Heap.set
        val assigned :
          M.sigma Memory.sequence ->
          LogicAssigns.Make.region -> Lang.F.pred list
      end
end