sig type region = (Ctypes.c_object * M.loc Memory.sloc list) list val vars : region -> Lang.F.Vars.t val domain : region -> M.Heap.set val assigned : M.sigma Memory.sequence -> region -> Lang.F.pred list end