Ienv
Fixtype of implementation environments.
This is a product type introduced by fty::defprod.
Fields
- short-bytes — posp
- int-bytes — posp
- long-bytes — posp
- llong-bytes — posp
- plain-char-signedp — booleanp
Additional Requirements
The following invariant is enforced on the fields:
(and (<= short-bytes int-bytes)
(<= int-bytes long-bytes)
(<= long-bytes llong-bytes)
(<= 2 short-bytes)
(<= 4 int-bytes)
(<= 8 long-bytes)
(<= 8 llong-bytes))
For now we only need to capture
certain characteristics of the integer types.
We assume that bytes are 8 bits,
that signed integers use two's complement,
and that there are no padding bits
or trap representations.
Therefore, the characteristics of the integer types
are mainly defined by four numbers,
i.e. the numbers of bytes of (signed and unsigned)
short, int, long, and long long.
These correspond to the integer formats of our C formalization:
see that topic for more information,
also on the allowed ranges and relative constraints.
We also need a flag saying whether the plain char type
has the same range as signed char or not [C:6.2.5/15];
if the flag is false, it has the same range as unsigned char.
Subtopics
- Ienvp
- Recognizer for ienv structures.
- Ienv-fix
- Fixing function for ienv structures.
- Make-ienv
- Basic constructor macro for ienv structures.
- Ienv->short-bytes
- Get the short-bytes field from a ienv.
- Ienv->llong-bytes
- Get the llong-bytes field from a ienv.
- Ienv-equiv
- Basic equivalence relation for ienv structures.
- Ienv->long-bytes
- Get the long-bytes field from a ienv.
- Ienv->int-bytes
- Get the int-bytes field from a ienv.
- Ienv->plain-char-signedp
- Get the plain-char-signedp field from a ienv.
- Change-ienv
- Modifying constructor for ienv structures.
