		Search-engine friendly clone of the ACL2 documentation.

Valid-stmt

Validate a statement.

Signature
(valid-stmt stmt table ienv) → (mv erp new-stmt return-types last-expr-type? new-table)
Arguments: stmt — Guard (stmtp stmt).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: new-stmt — Type (stmtp new-stmt).; return-types — Type (type-setp return-types).; last-expr-type? — Type (type-optionp last-expr-type?).; new-table — Type (valid-tablep new-table).

If validation is successful, we return, besides an updated validation table, also two pieces of type information.

The first piece is the set of types returned by the statement, via return statements, with or without expressions. This is a set because a statement may contain multiple return sub-statements. A return statement with an expression contributes the type of the expression to the set; a return statement without an expression contributes the type void to the set.

The second piece of information is as follows. If the statement is either a (possibly labeled) expression statement, or is a (possibly labeled) compound one whose last block item is an expression statement, the second piece of information is the type of that expression. If the statement is not an expression or compound, or it is compound but does not end in an expression statement (including the case in which the compound statement has no block items), the second piece of information is nil. The reason for having this second piece of information is to support the validation of https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html.

To validate a labeled statement, we validate its label, and then the enclosed statement. We return the union of the return types, and the optional type from the statement. For now we do not check the requirements in [C17:6.8.1/2] and [C17:6.8.1/3].

To validate a compound statement, we push a new scope for the block, and we validate the list of block items. We pop the scope and we return the same results coming from the validation of the block items.

To validate an expression statement, we validate the expression if present, and return its type as the second result; this is nil if there is no expression. The return types are the same as the ones of the expression.

A selection statement and its sub-statements are blocks [C17:6.8.4/3], so we push and pop scopes accordingly. We check that the test of if has scalar type [C17:6.8.4.1/1] and that the target of switch has integer type [C17:6.8.4.2/1]. No type is returned as the last-expr-type? result, because a selection statement is not an expression statement (see criterion above for that result of this validation function).

An iteration statement and its sub-statements are blocks [C17:6.8.5/5], so we push and pop scopes accordingly. We check that the test expression has scalar type. No type is returned as the last-expr-type? result, because an iteraion statement is not an expression statement (see criterion above for that result of this validation function). For now we do not enforce that the declaration in a for only uses the storage class specifiers auto and register.

For now we do not check constraints on the label of a goto [C17:6.8.6.1/1], the occurrence of continue [C17:6.8.6.2/2], and the occurrence of break [C17:6.8.6.3/1].

A return statement explicitly adds a type to the return types, either the type of the expression, or void is there is no expression. We check the constraints on occurrences [C17:6.8.6.4/1] in the validation function for function definitions.

For now we do not check any constraints on assembler statements.