-
Notifications
You must be signed in to change notification settings - Fork 246
Open
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 withMetadata
Metadata
Assignees
Labels
No labels