Heap
Fixtype of heaps.
The heap is the memory area manipulated by malloc and free.
[C17] does not actually use the term `heap';
in fact, [C17] does not appear to use a specific term for this memory area.
However, `heap' is sufficiently commonly used
that it seems adequate to use it here.
For now we model the heap just as a finite map from addresses to values.
Subtopics
- Heap-fix
- (heap-fix x) is a usual ACL2::fty omap fixing function.
- Heapp
- Recognizer for heap.
- Heap-equiv
- Basic equivalence relation for heap structures.
