|
|
|---|
|
|
|
|---|
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].