		Search-engine friendly clone of the ACL2 documentation.

Valid-align-spec

Validate an alignment specifier.

Signature
(valid-align-spec align table ienv) → (mv erp new-align return-types new-table)
Arguments: align — Guard (align-specp align).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-align — Type (align-specp new-align).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

For now we just validate the type name or expression, possibly extending the validation table, but we do not check whether the alignment specifier is appropriate for the place where it occurs [C17:6.7.5].

In the version with the expression, the latter must have integer type [C17:6.7.5/3]. The version with the type name is equivalent to _Alignas(_Alignof(typename)), and thus we perform the same checks as in the :alignof case of valid-expr, including valid-sizeof/alignof.