cil
cil copied to clipboard
"Cannot represent the integer" errors in Concrat benchmarks
Running Goblint on https://github.com/goblint/bench/pull/53 reveals many parsing errors of the following kind:
- [ ] brubeck:
18446744073709551615,Unimplemented: Cannot represent the integer 18446744073709551615. - [ ] Cello:
14313749767032793493,Unimplemented: Cannot represent the integer 14313749767032793493. - [ ] Cello:
18446744073709551615,Unimplemented: Cannot represent the integer 18446744073709551615. - [ ] Chipmunk2D:
18446744070364630559,Unimplemented: Cannot represent the integer 18446744070364630559. - [ ] ... and many more.
For reference, GCC is fine with these and simply warns with "warning: integer constant is so large that it is unsigned" and seems to use a wraparound value in the assembly output.
Apparently we have some special logic for this that allows these constants, but only in the non-default C90 mode: https://github.com/goblint/cil/blob/4ef5a0865ce81c740c93da73e20a4f26daab3f1b/src/cil.ml#L64-L73
That's confusing because with GCC it's fine with C11, etc as well: https://godbolt.org/z/nav1qxa79.
Concrat benchmarks have been merged with Goblint CIL 1.8.2 and that has, for example, parsed 0x8000000000000000ULL and printed 9223372036854775808 into the merged file. Goblint CIL 2.0.0 no longer does that, probably since #53, which started putting all original integer constant strings into CInt, instead of converting the bigint to string for constants too large for OCaml's int63.