Implementation-environments
Implementation environments for the C syntax for tools.
These are similar to the implementation environments that are part of our C language formalization,
but they are simpler and meant for efficient execution.
The implementation environments in the language formalization
are richer, and meant for specification;
in particular, in the future they may include data
that may be inefficient to construct in execution.
We provide a mapping from these simplified implementation environments
to the more complex ones in the language formalization.
We also prove that
the operations on implementation environments defined here
are consistent with
the corresponding operations in the language formalization,
according to the aforementioned mapping.
The implementation environments we define here
parameterize some aspects of our C syntax for use by tools.
Subtopics
- Ienv
- Fixtype of implementation environments.
- Ldm-ienv
- Map an implementation environment of type ienv
to one in the language formalization of type c::ienv.
- 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-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-uint-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type unsigned int.
- Ienv-char-rangep
- Check if an ACl2 integer is
in the range of (i.e. representable in) type char.
- Ienv->uchar-max
- The ACL2 integer value of UCHAR_MAX [C17:5.2.4.2.1/1].
- 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->ushort-max
- The ACL2 integer value of USHRT_MAX [C17:5.2.4.2.1].
- Ienv->ulong-max
- The ACL2 integer value of ULONG_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-max
- The ACL2 integer value of SHRT_MAX [C17:5.2.4.2.1].
- Ienv->slong-max
- The ACL2 integer value of LONG_MAX [C17:5.2.4.2.1].
- Ienv->sllong-max
- The ACL2 integer value of LLONG_MAX [C17:5.2.4.2.1].
- Ienv->uint-max
- The ACL2 integer value of UINT_MAX [C17:5.2.4.2.1].
- Ienv->sint-max
- The ACL2 integer value of INT_MAX [C17:5.2.4.2.1].
- Ienv->sshort-min
- The ACL2 integer value of SHRT_MIN [C17:5.2.4.2.1].
- Ienv->slong-min
- The ACL2 integer value of LONG_MIN [C17:5.2.4.2.1].
- Ienv->sllong-min
- The ACL2 integer value of LLONG_MIN [C17:5.2.4.2.1].
- Ienv->sint-min
- The ACL2 integer value of INT_MIN [C17:5.2.4.2.1].
- Ienv->char-min
- The ACL2 integer value of CHAR_MAX [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->std
- Numeric version of the C standard (regardless of GCC extensions).
- Ienv->gcc
- Flag saying whether GCC extensions are enabled or not.
- Ienv-default
- A default implementation environment.
