Atc-static-variable-pointer-rules
Rules about pointers to variables in static storage.
When exec-ident is applied to a variable that contains an array,
it is rewritten into a pointer to the variable,
which must be in static storage:
this produces a term of the form
(value-pointer (pointer-valid (objdesign-static ...))
(value-array->elemtype ...))
This differs from the pointers to heap objects,
which are ACL2 variables.
This pointer term must be showed valid,
which we do via value-pointer-validp-of-value-pointer,
which produces
(pointer-case (pointer-valid (objdesign-static ...)) :valid),
which we resolve to t via return-type-of-pointer-valid.
The type is extracted from the pointer,
via value-pointer->reftype-of-value-pointer),
which generates a term @('(type-fix ...),
where ... is a term that constructs a type (e.g. (type-sint)),
so we use type-fix-when-typep,
along with rules saying that type-sint and similar constructors
return types.
After establishing the non-nullness of the pointer,
its designator is extracted, via value-pointer->designator.
The rule value-pointer->designator-of-value-pointer does that,
but leaves an objdesign-fix that needs to be removed,
which we do via objdesign-fix-when-objdesignp
and return-type-of-objdesign-static.
The rule return-type-of-value-pointer is used
to establish that the pointer is in fact a value,
which is needed to discharge certain conditions.