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
- Schar-format
- Fixtype of formats of signed char objects.
- Uinteger-sinteger-bit-roles-wfp
- Check if a list of roles of unsigned integer bits
and a list of roles of signed integer bits
are mutually consistent.
- Uinteger-format
- Fixtype of formats of unsigned integer objects.
- Uchar-format
- Fixtype of formats of unsigned char objects.
- Sinteger-bit-role
- Fixtype of roles of integer bits in signed integers.
- Signed-format
- Fixtype of signed formats.
- Uinteger-bit-role
- Fixtype of roles of integer bits in unsigned integers.
- Ienv
- Fixtype of implementation environments.
- Sinteger-bit-roles-wfp
- Check if a list of roles of signed integer bits is well-formed.
- Ienv->schar-min
- The ACL2 integer value of SCHAR_MIN [C17:5.2.4.2.1/1].
- Uinteger-bit-roles-wfp
- Check if a list of roles of unsigned integer bits is well-formed.
- Char-format
- Fixtype of formats of char objects.
- Uinteger-bit-roles-value-count
- Number of value bit roles in
a list of roles of unsigned integer bits.
- Uinteger-bit-roles-exponents
- Exponents of a list of roles of unsigned integer bits.
- Sinteger-bit-roles-value-count
- Number of value bit roles in
a list of roles of signed integer bits.
- Sinteger-bit-roles-exponents
- Exponents of a list of roles of signed integer bits.
- Ienv->uchar-max
- The ACL2 integer value of UCHAR_MAX [C17:5.2.4.2.1/1].
- Sinteger-bit-roles-sign-count
- Number of sign bit roles in a list of roles of signed integer bits.
- Ienv->char-min
- The ACL2 integer value of CHAR_MIN [C17:5.2.4.2.1/1].
- Ienv->char-bits
- The ACL2 integer value of CHAR_BIT [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-max
- The ACL2 integer value of CHAR_MIN [C17:5.2.4.2.1/1].
- Uinteger-bit-role-list
- Fixtype of lists of roles of integer bits in unsigned integers.
- Sinteger-value-bits-leq-uinteger-value-bits
- The number of signed integer value bits
is less than or equal to
the number of unsigned integer value bits.
- Sinteger-bit-role-list
- Fixtype of lists of roles of integer bits in signed integers.
