module Make: functor (M : Memory.Model) -> functor (C : Code with type loc = M.loc) -> functor (L : Logic with type loc = M.loc) -> sig .. end
functor (
M
:
Memory.Model
) ->
C
Code
with type loc = M.loc
L
Logic
sig
end
Code with type loc = M.loc
Logic with type loc = M.loc
type region = (Ctypes.c_object * M.loc Memory.sloc list) list
(Ctypes.c_object * M.loc Memory.sloc list) list
val vars : region -> Lang.F.Vars.t
region -> Lang.F.Vars.t
val domain : region -> M.Heap.set
region -> M.Heap.set
val assigned : M.sigma Memory.sequence -> region -> Lang.F.pred list
M.sigma Memory.sequence -> region -> Lang.F.pred list