module A:LogicAssigns.Make
(
M
)
(
C
)
(
L
)
module Hmap: M.Heap.Map
module Dom: M.Heap.Set
typeregion =
(Ctypes.c_object * M.loc Memory.sloc list) list
val vars : region -> Lang.F.Vars.t
val dsloc : Ctypes.c_object -> M.loc Memory.sloc -> M.Heap.set
val domain : region -> Dom.t
val assigned_seq : Lang.F.pred Bag.t ->
M.sigma Memory.sequence ->
(Ctypes.c_object * M.loc Memory.sloc) list -> Lang.F.pred Bag.t
val assigned : M.sigma Memory.sequence -> region -> Lang.F.pred list