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