Schar-formats
Formats of signed char objects.
We formalize the possible formats of signed char objects,
along with some operations on them.
Subtopics
- Schar-format
- Fixtype of formats of signed char objects.
- Schar-format->min
- The ACL2 integer value of SCHAR_MIN [C17:5.2.4.2.1/1].
- Schar-format->max
- The ACL2 integer value of SCHAR_MAX [C17:5.2.4.2.1/1].
- Schar-format-8tcnt
- The signed char format defined by
8 bits, two's complement, and no trap representations.
