Implementation-environments
Implementation environments for C.
Some aspects of the syntax and semantics of C are implementation-dependent.
[C17:5] introduces the notion of translation and execution environments,
which specify those aspects.
In our formalization, we introduce a notion of implementation environment,
which puts together the translation and execution environments in [C17].
That is, an implementation environment
specifies the implementation-dependent aspects of C.
We prefer to formalize one (implementation) environment,
instead of two (translation and execution) environments,
because the latter two share several aspects (e.g. integer sizes),
and therefore it seems simpler to have one notion.
We start by capturing some aspects of the C implementation environment.
More will be added in the future.
Initially, our formalization of implementation environments
is not used in other parts of the C formalization;
furthermore, it captures notions already captured elsewhere,
such as the integer formats. But we plan to update the rest of the formalization to use this,
also removing those then-redundant parts.
Subtopics
- Integer-format-templates
- Templates for formats of integer objects.
- Ienv
- Fixtype of implementation environments.
- Integer-formats
- Formats of integer objects.
- Ienv-ushort-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type unsigned short.
- Ienv-ulong-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type unsigned long.
- Ienv-ullong-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type unsigned long long.
- Ienv-uint-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type unsigned int.
- Ienv-uchar-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type unsigned char.
- Ienv-sshort-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type signed short.
- Ienv-slong-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type signed long.
- Ienv-sllong-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type signed long long.
- Ienv-sint-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type signed int.
- Ienv-schar-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type signed char.
- Ienv-char-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type char.
- Ienv->schar-min
- The ACL2 integer value of SCHAR_MIN [C17:5.2.4.2.1/1].
- Ienv->schar-max
- The ACL2 integer value of SCHAR_MAX [C17:5.2.4.2.1/1].
- Ienv->char-size
- The ACL2 integer value of CHAR_BIT [C17:5.2.4.2.1/1].
- Ienv->char-min
- The ACL2 integer value of CHAR_MIN [C17:5.2.4.2.1/1].
- Ienv->char-max
- The ACL2 integer value of CHAR_MAX [C17:5.2.4.2.1/1].
- Ienv->uchar-max
- The ACL2 integer value of UCHAR_MAX [C17:5.2.4.2.1/1].
- Ienv->short-bit-size
- Number of bits of unsigned and signed short objects.
- Ienv->long-bit-size
- Number of bits of unsigned and signed long objects.
- Ienv->llong-bit-size
- Number of bits of unsigned and signed long long objects.
- Ienv->int-bit-size
- Number of bits of unsigned and signed int objects.
- Ienv->short-byte-size
- Number of bytes of unsigned and signed short objects.
- Ienv->long-byte-size
- Number of bytes of unsigned and signed long objects.
- Ienv->llong-byte-size
- Number of bytes of unsigned and signed long long objects.
- Ienv->int-byte-size
- Number of bytes of unsigned and signed int objects.
- Versions
- Versions of C.
- Ienv->ushort-max
- The ACL2 integer value of USHRT_MAX [C17:5.2.4.2.1].
- Ienv->ullong-max
- The ACL2 integer value of ULLONG_MAX [C17:5.2.4.2.1].
- Ienv->sshort-min
- The ACL2 integer value of SHRT_MIN [C17:5.2.4.2.1].
- Ienv->sllong-min
- The ACL2 integer value of LLONG_MIN [C17:5.2.4.2.1].
- Ienv->sllong-max
- The ACL2 integer value of LLONG_MAX [C17:5.2.4.2.1].
- Ienv->bool-byte-size
- Number of bytes of _Bool objects.
- Ienv->bool-bit-size
- Number of bits of _Bool objects.
- Ienv->ulong-max
- The ACL2 integer value of ULONG_MAX [C17:5.2.4.2.1].
- Ienv->uint-max
- The ACL2 integer value of UINT_MAX [C17:5.2.4.2.1].
- Ienv->sshort-max
- The ACL2 integer value of SHRT_MAX [C17:5.2.4.2.1].
- Ienv->slong-min
- The ACL2 integer value of LONG_MIN [C17:5.2.4.2.1].
- Ienv->slong-max
- The ACL2 integer value of LONG_MAX [C17:5.2.4.2.1].
- Ienv->sint-min
- The ACL2 integer value of INT_MIN [C17:5.2.4.2.1].
- Ienv->sint-max
- The ACL2 integer value of INT_MAX [C17:5.2.4.2.1].
- Schar-formats
- Formats of signed char objects.
- Char-formats
- Formats of (plain) char objects.
- Uchar-formats
- Formats of unsigned char objects.
- Signed-formats
- Formats of signed integers.
- Bool-formats
- Formats of _Bool objects.
