		Search-engine friendly clone of the ACL2 documentation.

Language

Types

A model of C types.

Here we define the semantic notion of type, which is related to, but distinct from, the syntactic notion of type name [C17:6.7.7]. Specifically, different type names may denote the same type, if they use syntactically different but equivalent type specifier sequences (e.g. int and signed int).

Subtopics

Type: Fixtype of types [C17:6.2.5].
Type-name-list-to-type-list: Lift tyname-to-type to lists.
Tyname-to-type: Turn a type name into a type.
Member-type-list->name-list: Lift member-type->name to lists.
Type-completep: Check if a type is complete [C17:6.2.5].
Member-type: Fixtype of member types.
Member-type-add-first: Add a member type at the beginning of a list of member types.
Member-type-add-last: Add a member at the end of a list of member types.
Init-type: Fixtype of initializer types.
Type-option: Fixtype of optional types.
Member-type-lookup: Look up a member by name in a list of member types.
Tyspecseq-to-type: Turn a type specifier sequence into a type.
Member-type-list-option: Fixtype of optional lists of member types.
Type-promoted-arithmeticp: Check if a type is a promoted arithmetic type.
Type-list-result: Fixtype of errors and lists of types.
Member-type-list-result: Fixtype of errors and lists of member types.
Integer-type-bits-nulfun: Name of the nullary function that defines the size in bits of a C integer type.
Init-type-result: Fixtype of errors and initializer types.
Type-result: Fixtype of errors and types.
Type-nonchar-integerp: Check if a (supported) type is an integer type except for the plain char type.
Type-nonchar-integer-listp: Check if a list of types consists of all integer types except the plain char type.
Type-arithmetic-listp: Check if a list of types consists of all arithmetic types.
Type-integer-listp: Check if a list of types consists of all integer types.
Integer-type-xdoc-string: Documentation (sub)string that describes a C integer type.
Type-unsigned-integerp: Check if a type is an 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].
Integer-type-minbits: Minimum number of bits that forms a value of a C integer type.
Integer-type-bits: Number of bits that forms a value of a C integer type.
Type-scalarp: Check if a type is a scalar type [C17:6.2.5/21].
Type-integerp: Check if a type is an integer type [C17:6.2.5/17].
Type-arithmeticp: Check if a type is an arithmetic type [C17:6.2.5/18].
Type-realp: Check if a type is a real type [C17:6.2.5/18].
Type-list: Fixtype of lists of types.
*nonchar-integer-types*: List of the (supported) C integer types except plain char.
Member-type-list: Fixtype of lists of member types.
Ident-type-map: Fixtype of maps from identifiers to types.
Type-set: Fixtype of sets of types.
Type-option-set: Fixtype of sets of optional types.
Symbol-type-alist: Fixtype of alists from symbols to types.
Type-option-list: Fixtype of lists of optional types.