Module `Memory_domains.Region_separation`

module Make
  (Sub : Memory_sig.OFFSET_AND_MAKE_BLOCK) : 
  Memory_sig.WHOLE_MEMORY_DOMAIN with module Scalar = Sub.Scalar

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)

Module Memory_domains.Region_separation

Module `Memory_domains.Region_separation`