Compustate
Fixtype of computation states.
This is a product type introduced by fty::defprod.
Fields
- static — scope
- frames — frame-list
- heap — heap
A computation state consists of:
- A scope for static storage [C:6.2.4].
Our current C subset only has one translation unit
(i.e. a single .c file, with an optional .h file;
together they form a single translation unit, see preprocess),
so the static storage corresponds to
the variables declared at the top-level in the translation unit,
which form a scope.
- A stack of frames.
The variables there are in automatic storage [C:6.2.4].
- A heap.
This is allocated storage [C:6.2.4].
More components may be added,
and some components may be refined,
as our modeling coverage of C increases.
The stack grows leftward and shrinks rightward,
i.e. push is cons, pop is cdr, and top is car.
Subtopics
- Compustatep
- Recognizer for compustate structures.
- Compustate-fix
- Fixing function for compustate structures.
- Compustate-equiv
- Basic equivalence relation for compustate structures.
- Make-compustate
- Basic constructor macro for compustate structures.
- Compustate->frames
- Get the frames field from a compustate.
- Change-compustate
- Modifying constructor for compustate structures.
- Compustate->static
- Get the static field from a compustate.
- Compustate->heap
- Get the heap field from a compustate.
