		Search-engine friendly clone of the ACL2 documentation.

Valid-structdecl

Validate a structure declaration.

Signature
(valid-structdecl structdecl previous table ienv) → (mv erp new-structdecl new-previous return-types new-table)
Arguments: structdecl — Guard (structdeclp structdecl).; previous — Guard (ident-listp previous).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: new-structdecl — Type (structdeclp new-structdecl).; 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.