		Search-engine friendly clone of the ACL2 documentation.

Syntax-for-tools

Validation-information

Information calculated and used by the validator.

The validator calculates and uses information, such as types, and annotates the abstract syntax with some of this information. Here we introduce fixtypes for this information, and operations on those fixtypes.

We also introduce predicates over the abstract syntax, to check that the annotations from the validator are present. This is not the same as saying that the constructs are validated; the predicates just say that information of the right type is present.

Subtopics

Type: Fixtype of C types [C:6.2.5].
Abstract-syntax-annop: Definition of the predicates that check whether the abstract syntax is annotated with validation information.
Type-uaconvert-signed-unsigned: Convert a promoted signed integer type and a promoted unsigned integer type to their common type, according to the usual arithmetic conversions [C:6.3.1.8].
Type-uaconvert: Perform the usual arithmetic conversions on two arithmetic types [C:6.3.1.8].
Valid-ord-info: Fixtype of validation information about ordinary identifiers.
Lifetime: Fixtype of lifetimes.
Type-promote: Perform integer promotions on an arithmetic type [C:6.3.1.1/2].
Valid-defstatus: Fixtype of definition statuses for validation.
Valid-table: Fixtype of validation tables.
Valid-ord-info-option: Fixtype of optional validation information about ordinary identifiers.
Linkage-option: Fixtype of optional linkages.
Linkage: Fixtype of linkages.
Lifetime-option: Fixtype of optional lifetimes.
Var-info: Fixtype of validation information for variables.
Type-option: Fixtype of optional types.
Valid-scope: Fixtype of validation scopes.
Type-uaconvert-unsigned: Convert two promoted unsigned integer types to their common type, according to the usual arithmetic conversions [C:6.3.1.8].
Type-uaconvert-signed: Convert two promoted signed integer types to their common type, according to the usual arithmetic conversions [C:6.3.1.8].
Transunit-info: Fixtype of validation information for translation units.
Type-unsigned-integerp: Check if a type is an unsigned integer type [C:6.2.5/6].
Type-fpconvert: Convert function types to pointer types.
Type-signed-integerp: Check if a type is a signed integer type [C:6.2.5/4].
Type-promotedp: Check if an arithmetic type is a promoted one.
Type-arithmeticp: Check if a type is an arithmetic type [C:6.2.5/18].
Type-apconvert: Convert array types to pointer types.
Valid-ord-scope: Fixtype of validation scopes of ordinary identifiers.
Type-standard-unsigned-integerp: Check if a type is a standard unsigned integer type [C:6.2.5/6].
Type-standard-signed-integerp: Check if a type is a standard signed integer type [C:6.2.5/4].
Type-aggregatep: Check if a type is an aggregate type [C:6.2.5/21].
Type-standard-integerp: Check if a type is a standard integer type [C:6.2.5/7].
Type-real-floatingp: Check if a type is a real floating type [C:6.2.5/10].
Type-integerp: Check if a type is an integer type [C:6.2.5/17].
Type-floatingp: Check if a type is a floating type [C:6.2.5/11].
Type-complexp: Check if a type is a complex type [C:6.2.5/11].
Type-characterp: Check if a type is a character type [C:6.2.5/15].
Type-basicp: Check if a type is a basic type [C:6.2.5/14].
Type-scalarp: Check if a type is a scalar type [C:6.2.5/21].
Type-realp: Check if a type is a real type [C:6.2.5/17].
Coerce-transunit-info: Coerce a value to transunit-info.
Coerce-var-info: Coerce a value to var-info.
Irr-transunit-info: An irrelevant validation information for translation units.
Irr-var-info: An irrelevant validation information for variables.
Irr-valid-table: An irrelevant validation table.
Valid-scope-list: Fixtype of lists of validation scopes.
Type-set: Fixtype of sets of types.
Type-option-type-alist: Fixtype of alists from optional types to types.
Irr-linkage: An irrelevant linkage.
Irr-lifetime: An irrelevant lifetime.
Type-list: Fixtype of lists of types.
Irr-type: An irrelevant type.