Abstract data types to be used in specifications
This module provides functions for dynamic storage allocation.
Its operations are
significantly faster than the C function
The use of the module requires an initializing call of the function
The module does not have generic parameters. It is used by writing
All entities exported by this module can be used in specifications
The functions can be used in a C module in the following way:
#include "DynSpace.h" void *MySpace; /* ... */ MySpace = InitDynSpace (); /* ... */ p = (TypeX*) DynAlloc (MySpace, sizeof (TypeX)); /* ... */ DynClear (MySpace); /* ... */
Note: Neither the cast nor the call of sizeof can be part of a LIDO computation, since type identifiers are not allowed in computations. Hence the calls of this module must reside in a C module (that implements the type of the allocated objects).