Pin C standard to C17 #4055
Pin C standard to C17 #4055
Conversation
|
I disagree with the proposed fix: #4052 (comment) is a problem we should fix by not using „bool“ in the first place. There is no need for using that particular name, and we could just use __kani_bool or whatever instead. |
|
I think there are issues other than the |
Compiling our file with some GCC version with -std=c23 or -std=c2x might do the trick. |
|
I tried that yesterday and it didn't complain about the $ which goto-cc
/usr/bin/goto-cc
$ goto-cc --version
gcc (goto-cc 6.6.0 (cbmc-6.6.0)) 11.4.0
Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger
CBMC version: 6.6.0 (cbmc-6.6.0)
Architecture: x86_64
OS: linux
gcc: 11.4.0
$ goto-cc -std=gnu2x library/kani/kani_lib.c
$ goto-cc -std=gnu23 library/kani/kani_lib.c
gcc: error: unrecognized command-line option ‘-std=gnu23’; did you mean ‘-std=gnu2x’?
preprocessing has failed
$ goto-cc -std=c23 library/kani/kani_lib.c
gcc: error: unrecognized command-line option ‘-std=c23’; did you mean ‘-std=c2x’?
preprocessing has failed
$ goto-cc -std=c2x library/kani/kani_lib.c
$ gcc --version
gcc (Ubuntu 11.4.0-1ubuntu1~22.04) 11.4.0
Copyright (C) 2021 Free Software Foundation, Inc.
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.Not sure if the GCC version I have is too old. So I thought I'd play it safe and pin the language version (since our code in its current form might not be C23-compatible). |
|
I just tried via Compiler Explorer. I believe we really should just remove that line |
|
For the record, I am willing to test if that also fixes things on my end. |
Thanks! I created another PR with the alternative fix: #4058. Kindly let us know if this also fixes the issue. |
|
Closing in favor of #4058 |
This is a proposed alternative fix to #4052 where the new GCC version (v15) switched from C17 to C23 by default and complains about errors in https://github.com/model-checking/kani/blob/main/library/kani/kani_lib.c. The first proposed fix in #4055 pinned the version to C17. This PR instead removes the typedef that causes an error with C23. Resolves #4052 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
3 participants
GCC 15 (which was released a week ago) changed the default language version from C17 to C23:
https://gcc.gnu.org/gcc-15/changes.html#c
With C23, some of the code in https://github.com/model-checking/kani/blob/main/library/kani/kani_lib.c doesn't compile (see #4052). To allow Kani to run in environments with the newer GCC version, this PR pins the language version to C17.
Resolves #4052
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.