Script to auto-check whether benchmark files compile using GCC #2
Conversation
I think this should be integrated. What is the idea of the Also, what are the reasons for the auto-blacklisted warnings? |
The blacklist file is/was helpful to easily add all the files failing the test to the for-loop that skips over known-bad ones and is included in the script. The reasons for auto-blacklisting were simply such that I did not manually have to ack each and every reported error. In the near term, all the auto-blacklisting should go away, and indeed the files should be fixed instead. See #3 for some first progress towards this goal. Best, |
I have added a few changes to the script in https://github.com/PhilippWendler/sv-benchmarks/tree/checking, maybe you want to include them in this pull request? |
because it only handles C files.
Default is now 32bit as most files in SV-Comp are for 32bit. This will also set 32bit to files for which nothing has been defined yet (e.g., when running the script on new files that should be added).
Thanks a lot, added those improvements! |
Script to auto-check whether benchmark files compile using GCC
The script produces warnings for the file ldv-memsafety/memleaks_test17_2_true-valid-memsafety.i. |
@mutilin |
@delcypher |
As previously stated on the mailing list, I have created a script to check whether benchmark files can at all be compiled using GCC, with crucial warnings enabled. That is, with comments:
Turn on warnings and make them fatal
-Wall -Werror
The rules say "GNU C or ANSI C", but a few benchmarks use C99-for-scoping
-std=c99
The following shouldn't affect the semantics
-Wno-unused-label -Wno-unused-function
-Wno-unused-but-set-variable -Wno-unused-variable -Wno-unused-value
These are a bit weird, but probably ok
-Wno-unknown-pragmas -Wno-attributes -Wno-parentheses
We've had discussions about these:
-Wno-maybe-uninitialized -Wno-uninitialized
A case-by-case question to see whether these are actually well-defined
-Wno-pointer-to-int-cast -Wno-int-to-pointer-cast -Wno-pointer-sign
The following should be fixed in the benchmarks triggering these
-Wno-return-local-addr -Wno-return-type
-Wno-main -Wno-sequence-point
The remaining warnings/errors can't be silenced once -Werror is in effect, so I
arrived at a huge blacklist, which is included in the file. Over time, these should be cleaned up.
Best,
Michael