A representation of C integer conversions in ACL2.

This is part of the shallow embedding.

We define ACL2 functions that convert between values of different C integer types.

Conversions between C types are described in [C:6.3]. Here we define conversions among the integer types supported by our model; these conversions are described in [C:6.3.1.3].

For the case of a conversion to a signed integer that cannot represent the original value, we use a guard that rules out that case. This way, in order to use the conversion, it must be provably the case that the value is representable in the new signed integer type.

For the case of a conversion to an unsigned integer,
we use `mod` (via the modular constructor) to make it fit.
If the original value fits, the `mod` has no effect.
Otherwise, the `mod` corresponds to the
repeated addition or subtraction described in [C:6.3.1.3].

- Def-integer-conversion
- Event to generate the conversion between C integer types.
- Integer-conversions-signed-from-unsigned-okp
- Theorems about certain conversions from unsigned to signed being always allowed for certain integer type sizes.
- Def-integer-conversions-loop-outer
- Events to generate the conversions between each of a list of source types and each of a list of destination types.
- Def-integer-conversions-loop-inner
- Events to generate the conversions between a source type and each of a list of destination types.
- Sshort-from-ullong-okp
- Check if a conversion from type
unsigned long long to typesigned short is well-defined. - Sllong-from-ushort-okp
- Check if a conversion from type
unsigned short to typesigned long long is well-defined. - Sllong-from-ullong-okp
- Check if a conversion from type
unsigned long long to typesigned long long is well-defined. - Sshort-from-ushort-okp
- Check if a conversion from type
unsigned short to typesigned short is well-defined. - Sshort-from-ulong-okp
- Check if a conversion from type
unsigned long to typesigned short is well-defined. - Sshort-from-uint-okp
- Check if a conversion from type
unsigned int to typesigned short is well-defined. - Sshort-from-uchar-okp
- Check if a conversion from type
unsigned char to typesigned short is well-defined. - Sshort-from-slong-okp
- Check if a conversion from type
signed long to typesigned short is well-defined. - Sshort-from-sllong-okp
- Check if a conversion from type
signed long long to typesigned short is well-defined. - Sshort-from-sint-okp
- Check if a conversion from type
signed int to typesigned short is well-defined. - Slong-from-ushort-okp
- Check if a conversion from type
unsigned short to typesigned long is well-defined. - Slong-from-ulong-okp
- Check if a conversion from type
unsigned long to typesigned long is well-defined. - Slong-from-ullong-okp
- Check if a conversion from type
unsigned long long to typesigned long is well-defined. - Slong-from-uint-okp
- Check if a conversion from type
unsigned int to typesigned long is well-defined. - Slong-from-uchar-okp
- Check if a conversion from type
unsigned char to typesigned long is well-defined. - Slong-from-sllong-okp
- Check if a conversion from type
signed long long to typesigned long is well-defined. - Sllong-from-ulong-okp
- Check if a conversion from type
unsigned long to typesigned long long is well-defined. - Sllong-from-uint-okp
- Check if a conversion from type
unsigned int to typesigned long long is well-defined. - Sllong-from-uchar-okp
- Check if a conversion from type
unsigned char to typesigned long long is well-defined. - Sint-from-ushort-okp
- Check if a conversion from type
unsigned short to typesigned int is well-defined. - Sint-from-ulong-okp
- Check if a conversion from type
unsigned long to typesigned int is well-defined. - Sint-from-ullong-okp
- Check if a conversion from type
unsigned long long to typesigned int is well-defined. - Sint-from-uchar-okp
- Check if a conversion from type
unsigned char to typesigned int is well-defined. - Sint-from-slong-okp
- Check if a conversion from type
signed long to typesigned int is well-defined. - Sint-from-sllong-okp
- Check if a conversion from type
signed long long to typesigned int is well-defined. - Schar-from-ushort-okp
- Check if a conversion from type
unsigned short to typesigned char is well-defined. - Schar-from-ulong-okp
- Check if a conversion from type
unsigned long to typesigned char is well-defined. - Schar-from-ullong-okp
- Check if a conversion from type
unsigned long long to typesigned char is well-defined. - Schar-from-uint-okp
- Check if a conversion from type
unsigned int to typesigned char is well-defined. - Schar-from-uchar-okp
- Check if a conversion from type
unsigned char to typesigned char is well-defined. - Schar-from-sshort-okp
- Check if a conversion from type
signed short to typesigned char is well-defined. - Schar-from-slong-okp
- Check if a conversion from type
signed long to typesigned char is well-defined. - Schar-from-sllong-okp
- Check if a conversion from type
signed long long to typesigned char is well-defined. - Schar-from-sint-okp
- Check if a conversion from type
signed int to typesigned char is well-defined. - Ushort-from-ulong
- Convert from type
unsigned long to typeunsigned short . - Ushort-from-ullong
- Convert from type
unsigned long long to typeunsigned short . - Ushort-from-uint
- Convert from type
unsigned int to typeunsigned short . - Ushort-from-uchar
- Convert from type
unsigned char to typeunsigned short . - Ushort-from-sshort
- Convert from type
signed short to typeunsigned short . - Ushort-from-slong
- Convert from type
signed long to typeunsigned short . - Ushort-from-sllong
- Convert from type
signed long long to typeunsigned short . - Ushort-from-sint
- Convert from type
signed int to typeunsigned short . - Ushort-from-schar
- Convert from type
signed char to typeunsigned short . - Ulong-from-ushort
- Convert from type
unsigned short to typeunsigned long . - Ulong-from-ullong
- Convert from type
unsigned long long to typeunsigned long . - Ulong-from-uchar
- Convert from type
unsigned char to typeunsigned long . - Ulong-from-sshort
- Convert from type
signed short to typeunsigned long . - Ulong-from-slong
- Convert from type
signed long to typeunsigned long . - Ulong-from-sllong
- Convert from type
signed long long to typeunsigned long . - Ulong-from-schar
- Convert from type
signed char to typeunsigned long . - Ullong-from-ushort
- Convert from type
unsigned short to typeunsigned long long . - Ullong-from-ulong
- Convert from type
unsigned long to typeunsigned long long . - Ullong-from-uint
- Convert from type
unsigned int to typeunsigned long long . - Ullong-from-uchar
- Convert from type
unsigned char to typeunsigned long long . - Ullong-from-sshort
- Convert from type
signed short to typeunsigned long long . - Ullong-from-slong
- Convert from type
signed long to typeunsigned long long . - Ullong-from-sllong
- Convert from type
signed long long to typeunsigned long long . - Ullong-from-sint
- Convert from type
signed int to typeunsigned long long . - Ullong-from-schar
- Convert from type
signed char to typeunsigned long long . - Uint-from-ushort
- Convert from type
unsigned short to typeunsigned int . - Uint-from-ullong
- Convert from type
unsigned long long to typeunsigned int . - Uint-from-sshort
- Convert from type
signed short to typeunsigned int . - Uint-from-sllong
- Convert from type
signed long long to typeunsigned int . - Uchar-from-ushort
- Convert from type
unsigned short to typeunsigned char . - Uchar-from-ulong
- Convert from type
unsigned long to typeunsigned char . - Uchar-from-ullong
- Convert from type
unsigned long long to typeunsigned char . - Uchar-from-sshort
- Convert from type
signed short to typeunsigned char . - Uchar-from-slong
- Convert from type
signed long to typeunsigned char . - Uchar-from-sllong
- Convert from type
signed long long to typeunsigned char . - Uchar-from-schar
- Convert from type
signed char to typeunsigned char . - Sshort-from-ushort
- Convert from type
unsigned short to typesigned short . - Sshort-from-ulong
- Convert from type
unsigned long to typesigned short . - Sshort-from-ullong
- Convert from type
unsigned long long to typesigned short . - Sshort-from-uint
- Convert from type
unsigned int to typesigned short . - Sshort-from-uchar
- Convert from type
unsigned char to typesigned short . - Sshort-from-slong
- Convert from type
signed long to typesigned short . - Sshort-from-sllong
- Convert from type
signed long long to typesigned short . - Sshort-from-sint
- Convert from type
signed int to typesigned short . - Sshort-from-schar
- Convert from type
signed char to typesigned short . - Slong-from-ushort
- Convert from type
unsigned short to typesigned long . - Slong-from-ulong
- Convert from type
unsigned long to typesigned long . - Slong-from-ullong
- Convert from type
unsigned long long to typesigned long . - Slong-from-uint
- Convert from type
unsigned int to typesigned long . - Slong-from-uchar
- Convert from type
unsigned char to typesigned long . - Slong-from-sshort
- Convert from type
signed short to typesigned long . - Slong-from-sllong
- Convert from type
signed long long to typesigned long . - Sllong-from-ushort
- Convert from type
unsigned short to typesigned long long . - Sllong-from-ulong
- Convert from type
unsigned long to typesigned long long . - Sllong-from-ullong
- Convert from type
unsigned long long to typesigned long long . - Sllong-from-uint
- Convert from type
unsigned int to typesigned long long . - Sllong-from-uchar
- Convert from type
unsigned char to typesigned long long . - Sllong-from-sshort
- Convert from type
signed short to typesigned long long . - Sllong-from-slong
- Convert from type
signed long to typesigned long long . - Sllong-from-sint
- Convert from type
signed int to typesigned long long . - Sllong-from-schar
- Convert from type
signed char to typesigned long long . - Sint-from-ushort
- Convert from type
unsigned short to typesigned int . - Sint-from-ulong
- Convert from type
unsigned long to typesigned int . - Sint-from-ullong
- Convert from type
unsigned long long to typesigned int . - Sint-from-uint-okp
- Check if a conversion from type
unsigned int to typesigned int is well-defined. - Sint-from-uchar
- Convert from type
unsigned char to typesigned int . - Sint-from-sshort
- Convert from type
signed short to typesigned int . - Sint-from-slong
- Convert from type
signed long to typesigned int . - Sint-from-sllong
- Convert from type
signed long long to typesigned int . - Schar-from-ushort
- Convert from type
unsigned short to typesigned char . - Schar-from-ulong
- Convert from type
unsigned long to typesigned char . - Schar-from-ullong
- Convert from type
unsigned long long to typesigned char . - Schar-from-uint
- Convert from type
unsigned int to typesigned char . - Schar-from-uchar
- Convert from type
unsigned char to typesigned char . - Schar-from-sshort
- Convert from type
signed short to typesigned char . - Schar-from-slong
- Convert from type
signed long to typesigned char . - Schar-from-sllong
- Convert from type
signed long long to typesigned char . - Schar-from-sint
- Convert from type
signed int to typesigned char . - Ulong-from-uint
- Convert from type
unsigned int to typeunsigned long . - Ulong-from-sint
- Convert from type
signed int to typeunsigned long . - Uint-from-ulong
- Convert from type
unsigned long to typeunsigned int . - Uint-from-uchar
- Convert from type
unsigned char to typeunsigned int . - Uint-from-slong
- Convert from type
signed long to typeunsigned int . - Uint-from-sint
- Convert from type
signed int to typeunsigned int . - Uint-from-schar
- Convert from type
signed char to typeunsigned int . - Uchar-from-uint
- Convert from type
unsigned int to typeunsigned char . - Uchar-from-sint
- Convert from type
signed int to typeunsigned char . - Slong-from-sint
- Convert from type
signed int to typesigned long . - Slong-from-schar
- Convert from type
signed char to typesigned long . - Sint-from-uint
- Convert from type
unsigned int to typesigned int . - Sint-from-schar
- Convert from type
signed char to typesigned int .