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