		Search-engine friendly clone of the ACL2 documentation.

Validation-information

Types

C types used by the validator.

We introduce a model of C types, along with some operations over those types.

Subtopics

Type-compatiblep: Check that two types are compatible [C17:6.2.7].
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 [C17:6.3.1.8].
Type-uaconvert: Perform the usual arithmetic conversions on two arithmetic types [C17:6.3.1.8].
Type-integer-promote: Perform integer promotions on an arithmetic type [C17:6.3.1.1/2].
Type-params-compatiblep: Check that parameter portions of two function types are compatible [C17:6.2.7].
Type-option: Fixtype of optional types.
Type-formalp: Check if a type is supported in our formal semantics of C.
Ldm-type: Map a type in type to a type in the language definition.
Make-pointers-to: Derive a pointer type for each type qualifier and attribute specifier list.
Type-list-default-arg-promote: Perform default argument promotion on each type in a list.
Type-uaconvert-unsigned: Convert two promoted unsigned integer types to their common type, according to the usual arithmetic conversions [C17:6.3.1.8].
Type-uaconvert-signed: Convert two promoted signed integer types to their common type, according to the usual arithmetic conversions [C17:6.3.1.8].
Type-default-arg-promote: Perform default argument promotion on a type [C17:6.5.2.2/6].
Type-default-arg-promotedp: Check if type is a default argument promoted type.
Type-params-composite: Construct a composite of the type-params portion of a function type.
Type-integer-promotedp: Check if an arithmetic type is a promoted one.
Ldm-type-option-set: Map a set of optional types in type-option-set to a set of optional types in the language definition.
Type-unsigned-integerp: Check if a type is an unsigned integer type [C17:6.2.5/6].
Type-standard-unsigned-integerp: Check if a type is a standard unsigned integer type [C17:6.2.5/6].
Type-signed-integerp: Check if a type is a signed integer type [C17:6.2.5/4].
Type-to-value-kind: Map a type to the corresponding c::value kind.
Type-standard-signed-integerp: Check if a type is a standard signed integer type [C17:6.2.5/4].
Ildm-type: Map a type in the language formalization to a type in type.
Type-arithmeticp: Check if a type is an arithmetic type [C17:6.2.5/18].
Ldm-type-set: Map a set of types in type-set to a set of types in the language definition.
Ldm-type-option: Map an optional type in type-option to an optional type in the language definition.
Type-standard-integerp: Check if a type is a standard integer type [C17:6.2.5/7].
Type-option-set-formalp: Check if all the optional types in a set are supported in our formal semantics of C.
Type-real-floatingp: Check if a type is a real floating type [C17:6.2.5/10].
Type-option-formalp: Check if an optional type is supported in our formal semantics of C.
Type-integerp: Check if a type is an integer type [C17:6.2.5/17].
Type-characterp: Check if a type is a character type [C17:6.2.5/15].
Type-basicp: Check if a type is a basic type [C17:6.2.5/14].
Type-aggregatep: Check if a type is an aggregate type [C17:6.2.5/21].
Type-scalarp: Check if a type is a scalar type [C17:6.2.5/21].
Type-realp: Check if a type is a real type [C17:6.2.5/17].
Type-fpconvert: Convert function types to pointer types.
Type-floatingp: Check if a type is a floating type [C17:6.2.5/11].
Type-complexp: Check if a type is a complex type [C17:6.2.5/11].
Type-set-formalp: Check if all the types in a set are supported in our formal semantics of C.
Type-apconvert: Convert array types to pointer types.
Type-composite: Construct a composite type [C17:6.2.7/3].
Ident-type-map: Fixtype of omaps from identifiers to types.
Type-set: Fixtype of sets of types.
Type-option-type-alist: Fixtype of alists from optional types to types.
Type-option-set: Fixtype of sets of optional types.
Type-list-compatiblep: Check that two type-lists are compatible [C17:6.2.7].
Irr-type-params: An irrelevant type-params.
Irr-type: An irrelevant type.
Type-list-composite: Construct a composite type-list.
Type/type-params/type-list