Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"Cannot represent the integer" errors in Concrat benchmarks #132

Open
5 tasks
Tracked by #53
sim642 opened this issue Feb 20, 2023 · 2 comments
Open
5 tasks
Tracked by #53

"Cannot represent the integer" errors in Concrat benchmarks #132

sim642 opened this issue Feb 20, 2023 · 2 comments
Labels

Comments

@sim642
Copy link
Member

sim642 commented Feb 20, 2023

Running Goblint on goblint/bench#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 sim642 added the bug label Feb 20, 2023
@sim642 sim642 self-assigned this Feb 21, 2023
@sim642
Copy link
Member Author

sim642 commented Feb 21, 2023

Apparently we have some special logic for this that allows these constants, but only in the non-default C90 mode:

cil/src/cil.ml

Lines 64 to 73 in 4ef5a08

let cstd = ref C99
let gnu89inline = ref false
let c99Mode () = !cstd <> C90 (* True to handle ISO C 99 vs 90 changes.
c99mode only affects parsing of decimal integer constants without suffix
a) on machines where long and long long do not have the same size
(e.g. 32 Bit machines, 64 Bit Windows, not 64 Bit MacOS or (most? all?) 64 Bit Linux):
giving constants that are bigger than max long type long long in c99mode vs. unsigned long
if c99mode is off.
b) for constants bigger than long long producing a "Unimplemented: Cannot represent the integer"
warning in C99 mode vs. unsigned long long if c99mode is off. *)

That's confusing because with GCC it's fine with C11, etc as well: https://godbolt.org/z/nav1qxa79.

@sim642 sim642 removed their assignment May 12, 2023
@sim642
Copy link
Member Author

sim642 commented Oct 9, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant