|
|
|---|
|
|
|
|---|
Fixtype of object designators.
This is a tagged union type, introduced by fty::deftagsum.
An object designator is a named variable in static storage, or a named variable in automatic storage, or an address in allocated storage (i.e. the heap), or a (structure) member of an object designator, or an (array) element of an object designator. For a variable in automatic storage, we need not only the name, but also an indication of which scope in which frame the variable is in: we use natural numbers for this purpose, meant to be indices in the frame stack and scope stack. For both frames and scopes, index 0 refers to the bottom of the stack; this is the opposite order in which the stacks of frames and scopes are indexed as ACL2 lists (via nth), but we need this opposite order in order for the indices to be stable against frames and scopes being pushed and popped.
Also see object-designators.