		Search-engine friendly clone of the ACL2 documentation.

Valid-desiniter-list

Validate a list of zero or more initializers with optional designations.

Signature
(valid-desiniter-list desiniters target-type lifetime table ienv) → (mv erp new-desiniters return-types new-table)
Arguments: desiniters — Guard (desiniter-listp desiniters).; target-type — Guard (typep target-type).; lifetime — Guard (lifetimep lifetime).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-desiniters — Type (desiniter-listp new-desiniters).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

The target type passed as argument is the type that each list of designators must be applicable to. Currently, we do not support fine-grained type-checking of aggregates or unions with an element/member type which is also an aggregate or union type (this condition is checked precisely for the array type, but conservatively includes all struct and unions types since out approximate types do not yet include member types). In such contexts, when an initializer lacks a designator, the type of the initializer may be either the type of the element/member, or the type of an element/member of that element/member (which member depends on the order of the initializers) [C17:6.7.9/20]. For now, we fall back to the unknown type in these cases as opposed to dealing with this complexity.