Integer-format-templates
Templates for formats of integer objects.
The formats of integer objects of different types
differ but follow a common template.
The unsigned, signed, and plain char types
follow more restricted rules, and are formalized in
uchar-formats, schar-formats, and char-formats.
The other integer types (short, int, etc.)
follow the more general templates formalized here.
Subtopics
- Integer-format
- Fixtype of formats of (signed and unsigned) integer objects.
- Uinteger-sinteger-bit-roles-wfp
- Check if a list of roles of unsigned integer bits
and a list of roles of signed integer bits
are mutually consistent.
- Sinteger-format
- Fixtype of formats of signed integer objects.
- Uinteger-format
- Fixtype of formats of unsigned integer objects.
- Sinteger-format->min
- The ACL2 integer value of
the minimum value representable in a signed integer format.
- Integer-format-inc-sign-tcnpnt
- The unsigned and signed integer format defined by
a size greater than 1,
increasing value bits,
a sign bit at the end (for the signed format),
two's complement signed format,
no padding bits,
and no trap representations.
- Sinteger-bit-role
- Fixtype of roles of integer bits in signed integers.
- Sinteger-bit-roles-wfp
- Check if a list of roles of signed integer bits is well-formed.
- Uinteger-bit-role
- Fixtype of roles of integer bits in unsigned integers.
- Uinteger-bit-roles-wfp
- Check if a list of roles of unsigned integer bits is well-formed.
- Uinteger+sinteger-format
- Fixtype of pairs consisting of
a format of unsigned integer objects
and a format of signed integer objects.
- Sinteger-bit-roles-value-count
- Number of value bit roles in
a list of roles of signed integer bits.
- Uinteger-bit-roles-value-count
- Number of value bit roles in
a list of roles of unsigned integer bits.
- Sinteger-bit-roles-inc-n-and-sign
- List of n signed integer value bit roles,
starting with exponent 0, in increasing exponent order,
and with a sign bit added at the end.
- Uinteger-bit-roles-inc-n
- List of n unsigned integer value bit roles,
starting with exponent 0, in increasing exponent order.
- Sinteger-format-inc-sign-tcnpnt
- The signed integer format defined by
n increasing value bits,
a sign bit at the end,
two's complement signed format,
no padding bits,
and no trap representations.
- Sinteger-bit-roles-inc-n
- List of n signed integer value bit roles,
starting with exponent 0, in increasing exponent order.
- Uinteger-bit-roles-exponents
- Exponents of a list of roles of unsigned integer bits.
- Sinteger-bit-roles-exponents
- Exponents of a list of roles of signed integer bits.
- Sinteger-format->max
- The ACL2 integer value of
the maximum value representable in a signed integer format.
- Integer-format->bit-size
- Number of bits of an integer format.
- Uinteger-format->max
- The ACL2 integer value of
the maximum value representable in an unsigned integer format.
- Sinteger-bit-roles-sign-count
- Number of sign bit roles in a list of roles of signed integer bits.
- Integer-format->signed-min
- The ACL2 integer value of
the minimum signed value representable in an integer format.
- Uinteger-format-inc-npnt
- The unsigned integer format defined by
n increasing value bits,
no padding bits,
and no trap representations.
- Integer-format->unsigned-max
- The ACL2 integer value of
the maximum unsigned value representable in an integer format.
- Integer-format->signed-max
- The ACL2 integer value of
the maximum signed value representable in an integer format.
- Uinteger-bit-role-list
- Fixtype of lists of roles of integer bits in unsigned integers.
- Sinteger-bit-role-list
- Fixtype of lists of roles of integer bits in signed integers.
- Uinteger-sinteger-bit-roles-wfp-of-inc-n-and-sign
- Mutual well-formedness of the lists of bit roles
from uinteger-bit-roles-inc-n
and sinteger-bit-roles-inc-n-and-sign.
