Module Region_separation.Make

Lifts 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)

Parameters

module Sub : Memory_sig.OFFSET_AND_MAKE_BLOCK

Signature

module Scalar = Sub.Scalar

module Address : Memory_sig.FIXED_SIZE_VALUE_DOMAIN with module Scalar = Scalar

module Make_Memory (Block : Memory_sig.BLOCK with module Scalar = Scalar) : Memory_sig.MEMORY with module Scalar = Scalar and module Address := Address and module Block := Block