Repository navigation
Omod missing cast in Ceval.ml #565
Description
CompCert 3.16 master branch
gcc 13.3.0
clang 18.1.3
int main() {
switch (-1 % 7u) {
case -1 % 7u:
return 0;
default:
return 1;
}
}$ ccomp omod-missing-cast.c && ./a.out; echo $?
1$ gcc omod-missing-cast.c && ./a.out; echo $?
0$ clang omod-missing-cast.c && ./a.out; echo $?
0My understanding is this:
- Case label
-1 % 7uis computed by the constant expression evaluator incparser/Ceval.ml. - Since the RHS is unsigned, the whole operation is unsigned, so the LHS should be promoted to unsigned.
- The Omod case in
Ceval.ml:binopdoesn't perform this cast so the LHS value is not normalized to 32-bit unsigned before the operation.
Is this intended? If not, proposed fix is to replace in the Omod case
begin match v1, v2 withwith
begin match cast env tyop v1, cast env tyop v2 with
Activity
Ceval.binop: add missing casts to `tyop`
Ceval.unop: wrong cast of result value
xavierleroy commentedon Dec 30, 2025
Well spotted, thanks! Your analysis is correct. Proposed fix in #567. I added casts to
tyopfor all operations, even though they may not be needed for, say, bitwise and.Ceval.unop: wrong cast of result value
Ceval.binop: add missing casts to `tyop`