cil icon indicating copy to clipboard operation
cil copied to clipboard

"Cannot represent the integer" errors in Concrat benchmarks

Open sim642 opened this issue 2 years ago • 2 comments

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.

sim642 avatar Feb 20 '23 14:02 sim642

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.

sim642 avatar Feb 21 '23 09:02 sim642

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.

sim642 avatar Oct 09 '23 14:10 sim642