		Search-engine friendly clone of the ACL2 documentation.

Language

Values

A model of C values.

Here we define fixtypes for values and related entities, and some basic ACL2 operations on them (these are not C operations, which are defined separately; they are just ACL2 operations on our model of values).

Subtopics

Pointer: Fixtype of pointers.
Member-types-of-member-values: Lift member-type-of-member-value to lists.
Member-value-list->value-list: Lift member-value->value to lists.
Member-value-list->name-list: Lift member-value->name to lists.
Expr-value: Fixtype of expression values.
Type-list-of-value-list: Lift type-of-value to lists.
Type-of-value: Type of a value.
Value-option: Fixtype of optional values.
Init-value: Fixtype of initializer values.
Value-result: Fixtype of values and errors.
Type-of-value-option: Type of an optional value.
Value-list-result: Fixtype of lists of values and errors.
Member-value-list-result: Fixtype of lists of member values and errors.
Init-value-result: Fixtype of initialization values and errors.
Expr-value-result: Fixtype of expression values and errors.
Value-option-result: Fixtype of optional values and errors.
Signed/unsigned-byte-p-of-integer-values: Theorems saying that the integer values satisfy signed-byte-p and unsigned-byte-p.
Member-type-of-member-value: Member type of a member value.
Bounds-of-integer-values: Linear rules about the bounds of the integer values.
Value-promoted-arithmeticp: Check if a value is a promoted arithmetic value.
Init-type-of-init-value: Initialization type of an initialization value.
Value-unsigned-integerp: Check if a value is an unsigned integer [C17:6.2.5/6].
Value-signed-integerp: Check if a value is a signed integer [C17:6.2.5/4].
Value-integerp: Check if a value is an integer [C17:6.2.5/17].
Value-arithmeticp: Check if a value is arithmetic [C17:6.2.5/18].
Value-scalarp: Check if a value is scalar [C17:6.2.5/21].
Value-realp: Check if a value is a real [C17:6.2.5/18].
Values/membervalues: Fixtypes of values and member values.