		Search-engine friendly clone of the ACL2 documentation.

Valid-struct-declon

Validate a structure declaration.

Signature
(valid-struct-declon structdeclon previous table ienv) → (mv erp new-structdeclon new-previous return-types new-table)
Arguments: structdeclon — Guard (struct-declonp structdeclon).; previous — Guard (ident-listp previous).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-structdeclon — Type (struct-declonp new-structdeclon).; new-previous — Type (ident-listp new-previous).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

The previous input consists of the names of the members that precede this structure declaration in the structure or union specifier being validated. The new-previous output consists of the extension of previous with the names of the members declared by this structure declaration.

If the structure declaration declares members, first we validate the list of specifiers and qualifiers, obtaining a type if the validation is successful. Then we use a separate validation function for the structure declarators, which also returns a possibly extended list of member names.

If the structure declaration consists of a static assertion declaration, we validate it using a separate validation function. The list of member names is unchanged.

If the structure declaration is empty (i.e. a semicolon), which is a GCC extension, the list of member names and the validation table are unchanged.