Region_separation.MakeLifts a memory domain into a memory domain that separates each malloc call into a distinct memory region, separated by the others, where each memory region is handled by Sub.Memory (and pointers by Sub.Address)
module Sub : Memory_sig.OFFSET_AND_MAKE_BLOCKmodule Scalar = Sub.Scalarmodule Offset = Sub.Offsetmodule Address : Memory_sig.FIXED_SIZE_VALUE_DOMAIN with module Scalar = Scalarmodule Make_Memory
(Block :
Memory_sig.BLOCK with module Scalar = Scalar and module Offset = Offset) :
Memory_sig.MEMORY
with module Scalar = Scalar
and module Address := Address
and module Block := Block