package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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

Signature

module Scalar = Sub.Scalar
module Offset = Sub.Offset
module 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