Integer-formats
Formats of integer objects.
We use the templates formalized in integer-format-templates
to formalize the possible formats of the integer types
other than unsigned, signed, and plain char types,
namely short, int, and larger types.
We also put these together with
our formalization of the possible formats of
the unsigned, signed, and plain char types,
to form data structures for the possible formats of most integer types
(we plan to add the remaining ones at some point).
Subtopics
- Integer-format-llong-wfp
- Check if an integer format is well-formed
when used for (signed and unsigned) long long.
- Integer-format-short-wfp
- Check if an integer format is well-formed
when used for (signed and unsigned) short.
- Integer-format-long-wfp
- Check if an integer format is well-formed
when used for (signed and unsigned) long.
- Integer-format-int-wfp
- Check if an integer format is well-formed
when used for (signed and unsigned) int.
- Char+short+int+long+llong+bool-format
- Fixtype of formats of
(unsigned, signed, and plain) char objects,
(unsigned and signed) short objects,
(unsigned and signed) int objects,
(unsigned and signed) long objects,
(unsigned and signed) long long objects, and
_Bool objects.
- Char+short+int+long+llong+bool-format-wfp
- Check if the formats of
char,
short,
int,
long,
long long,
and _Bool
objects
are well-formed.
- Llong-format-64tcnt
- The (unsigned and signed) long long format defined by
64 bits with increasing values,
two's complement,
and no trap representations.
- Short-format-16tcnt
- The (unsigned and signed) short format defined by
16 bits with increasing values,
two's complement,
and no trap representations.
- Long-format-32tcnt
- The (unsigned and signed) long format defined by
32 bits with increasing values,
two's complement,
and no trap representations.
- Int-format-16tcnt
- The (unsigned and signed) int format defined by
16 bits with increasing values,
two's complement,
and no trap representations.
- Integer-format-short/int/long/llong-wfp-of-inc-sign-tcnpnt
- Theorems about the well-formedness of
shorts, ints, longs, and long longs
specified via integer-format-inc-sign-tcnpnt.
- Char8+short16+int16+long32+llong64+bool0-tcnt
- The
char,
short,
int,
long,
long long, and
_Bool
integer formats defined by
the minimal number of bits with increasing values,
two's complement,
no trap representations,
unsigned plain chars,
and one-byte _Bool objects
with value in the least significant bit.
