Integer-formats
C integer formats.
[C] provides constraints on the formats of the integer types [C:6.2.5],
but not a complete definition of the formats (unlike Java).
A general formalization of C should be parameterized over these formats;
we plan to do that in our formalization of C.
However, for now we define the formats, but we do so in a way that
should make it easy to change and swap some aspects of the definitions.
[C:6.2.6.2/2] allows padding bits, which we disallow for now.
[C:6.2.6.2/2] allows signed integers to be
two's complement, ones' complement, or sign and magnitude;
for now we assume two's complement.
The exact number of bits in a byte is also implementation-dependent
[C:5.2.4.2.1/1] [C:6.2.6.1/3],
so we introduce a nullary function for the number of bits in a byte,
i.e. in a char (unsigned, signed, or plain).
We define it to be 8 for now, because that is the most frequent case.
A step towards generalizing this is in bytes,
which we plan to use for a future more general version of
our formalization of the integer formats.
We also introduce nullary functions for the number of bits that form
(signed and unsigned)
shorts, ints, long, and long longs.
Given the above current choice of no padding bits,
these numbers of bits have to be multiples of the number of bits in a byte,
because those integers have to take a whole number of bytes.
Recall that each unsigned/signed integer type
takes the same storage as the corresponding signed/unsigned type
[C:6.2.5/6].
We prove some theorems about the nullary functions.
We disable the definitions of the nullary functions,
including executable counterparts.
This way, we minimize the dependencies from the exact definitions,
and we define the integer values, conversions, and operations
as independently from the exact sizes as possible.
Thus, it may not be difficult to replace this file
with another one with different definitions,
or to replace the definitions with a parameterization.
The definitions that we pick here are consistent with gcc
on (at least some versions of) macOS and Linux, namely:
char is 8 bits,
short is 16 bits (2 bytes),
int is 32 bits (4 bytes),
long is 64 bits (8 bytes), and
long long is also 64 bits (8 bytes).
These are all consistent with the ranges in [C:5.2.4.2.1]:
char must be at least 8 bits,
short must be at least 16 bits,
int must be at least 16 bits,
long must be at least 32 bits, and
long long must be at least 64 bits.
Furthermore, the ranges must be non-decreasing [C:6.2.5/8].
For now we only define formats for
the standard signed and unsigned integer types except _Bool.
Note that the plain char type is not covered yet;
it is an integer type,
but not a standard integer type in C's terminology.
Subtopics
- Short-bits
- Size of signed and unsigned short values, in bits.
- Long-bits
- Size of signed and unsigned long values, in bits.
- Int-bits
- Size of signed and unsigned int values, in bits.
- Def-integer-bits-linear-rule
- Macro to generate linear rules about
the sizes in bits of C integer types.
- Llong-bits
- Size of signed and unsigned llong values, in bits.
- Def-integer-bits
- Macro to generate the nullary functions, and some theorems about them,
for the size in bits of the C integer types.
- Char-bits
- Size of signed, unsigned, and plain char values, in bits.
