		Search-engine friendly clone of the ACL2 documentation.

Valid-dirdeclor

Validate a direct declarator.

Signature
(valid-dirdeclor dirdeclor fundef-params-p type table ienv) → (mv erp new-dirdeclor new-type ident return-types new-table)
Arguments: dirdeclor — Guard (dirdeclorp dirdeclor).; fundef-params-p — Guard (booleanp fundef-params-p).; type — Guard (typep type).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-dirdeclor — Type (dirdeclorp new-dirdeclor).; new-type — Type (typep new-type).; ident — Type (identp ident).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

The type passed as input is the one resulting from the validation of the list of declaration specifiers or the list of specifiers and qualifiers that precedes the declarator of which the direct declarator is part. This type is refined according to the direct declarator, and we return the refined type, along with the declared identifier.

The meaning of the fundef-params-p flag passed as input is the same as in valid-declor: see that function's documentation.

If the direct declarator is just an identifier, the type is not further refined by this direct declarator.

If the direct declarator is a parenthesized declarator, we recursively validate the declarator.

If the direct declarator is one of the array kinds, we refine the type to an array type [C17:6.7.6.2/3] derived from the input type, and we recursively validate the enclosed direct declarator. Then we validate the index expression (if present), ensuring that it has integer type. For now we do not check that, if these expressions are constant, their values are greater than 0 [C17:6.7.6.2/1]. Currently we do not need to do anything with type qualifiers and attributes. The fundef-params-p flag is threaded through.

If the direct declarator is one of the function kinds, we ensure that the input type, which is the function return type, is not a function or array type [C17:6.7.6.3/1]. We refine the input type to a function type (which in our current type system means we override it), and we validate the declarator. Then things differ between the kinds of function declarators.

In a function declarator with a parameter type list, we push a new scope for the parameters. If fundef-params-p is t, we then check whether the parameters of the current direct declarator are in fact the ones of the function. If so, we validate the parameters with a fundef-params-p value of t. Otherwise, we use a value of nil. Validating the parameters adds them to the new scope. We then pop the scope if the parameters are not those of our function definition. Finally, we validate the enclosed direct declarator, returning the refined type.

To check whether the parameter type list in the current direct declarator represents the parameters of the current function definition, we check if the enclosed direct declarator contains function parameters. If so, this enclosed direct declarator contains the definition parameters; the parameter type list of the outer direct declarator does not correspond to the definition. To make things clearer, consider a function definition

void (*f(int x, int y))(int z) { ... }

which defines a function f with parameters x and y, which returns a pointer to a function that has a parameter z and returns void. When we validate the full declarator of this function definition, fundef-params-p is t. When we encounter the outer function declarator, first we check whether the inner direct declarator ((*f(int x, int y))) contains function parameters. Since it does, we determine that the outer parameter type list ((int z)) does not correspond the function definition, and we recursively process the inner direct declarator with fundef-params-p t.

In any case, when the current function declarator is the one whose parameters are for the function definition, after validating the parameters, which pushes a new scope with them, we return the validation table as such, so that when we later validate the function body, we already have the top-level scope for the body. If instead fundef-params-p is nil, the parameters form a function prototype scope [C17:6.2.1/4], which is therefore popped.

For the function declarator with a parameter type list, we handle the special case of a single void [C17:6.7.6.3/10].

A function declarator with a non-empty name list can only occur as the parameters of a function being defined [C17:6.7.6.3/3] Thus, we raise an error when the list is nonempty and fundef-params-p is nil (i.e. we are not validating the parameters of a defined function). Otherwise, we ensure that the names have no duplicates, and we push a new scope for the parameters and the function body, but we do not add the parameters to the new scope, because their types are specified by the declarations that must occur between the end of the whole function declarator and the beginning of the defined function's body. Note, in the case that we have a nonempty list of names, we currently return an imprecise type for the function. Since the type of each parameter is unknowable until the later declarations, we currently approximate the function type by assigning the unknown type to each function parameter.