unop result type mismatch in Ceval.ml

[bagnalla]

Similar to #565.

CompCert 3.16 master branch
gcc 13.3.0
clang 18.1.3

int main(void) {
  switch (~(unsigned short)0) {
    case ~(unsigned short)0:
      return 0;
    default:
      return 1;
  }
}

ccomp unop-result-type-mismatch.c && ./a.out; echo $?
1

gcc unop-result-type-mismatch.c && ./a.out; echo $?
0

clang unop-result-type-mismatch.c && ./a.out; echo $?
0

cparser/Ceval.ml:unop casts its result to ty instead of tyres, so the constant-evaluated ~(unsigned short)0 casts its result back to unsigned short instead of keeping it promoted to int.

If not intended, proposed fix is to replace in cparser/Ceval.ml:unop

in cast env ty res

with

in cast env tyres res

[xavierleroy]

Well spotted, thanks! Proposed fix applied in #567.