cbmc-viewer
cbmc-viewer copied to clipboard
model-checking
Suppress unhelpful warnings for better user experience
CBMC version: 5.69.1 (cbmc-5.59.0-676-gb4a4122dee)
Viewer version: 2.9
Operating system: N/A
Exact command line resulting in the issue:
First, clone my fork for coreJSON. Then, navigate to the proof located at coreJSON/verification/cbmc/proofs/skipString/. Finally, run the proof using make veryclean; time make.
What behaviour did you expect: No warnings.
What happened instead: I keep getting the following warnings without any source location.
WARNING: Skipping redefinition of symbol name: JSON_Iterate
WARNING: Old symbol JSON_Iterate: file verification/cbmc/proofs/skipString/core_json.c, line 1774
WARNING: New symbol JSON_Iterate: file source/include/core_json.h, line 326
WARNING: Skipping redefinition of symbol name: JSON_Validate
WARNING: Old symbol JSON_Validate: file verification/cbmc/proofs/skipString/core_json.c, line 1129
WARNING: New symbol JSON_Validate: file source/include/core_json.h, line 91
WARNING: Skipping redefinition of symbol name: skipAnyScalar
WARNING: Old symbol skipAnyScalar: file verification/cbmc/include/core_json_annex.h, line 120
WARNING: New symbol skipAnyScalar: file verification/cbmc/proofs/skipString/core_json.c, line 848
WARNING: Skipping redefinition of symbol name: skipCollection
WARNING: Old symbol skipCollection: file verification/cbmc/include/core_json_annex.h, line 95
WARNING: New symbol skipCollection: file verification/cbmc/proofs/skipString/core_json.c, line 1049
WARNING: Skipping redefinition of symbol name: skipScalars
WARNING: Old symbol skipScalars: file verification/cbmc/include/core_json_annex.h, line 106
WARNING: New symbol skipScalars: file verification/cbmc/proofs/skipString/core_json.c, line 1012
WARNING: Skipping redefinition of symbol name: skipSpace
WARNING: Old symbol skipSpace: file verification/cbmc/include/core_json_annex.h, line 132
WARNING: New symbol skipSpace: file verification/cbmc/proofs/skipString/core_json.c, line 72
WARNING: Skipping redefinition of symbol name: skipString
WARNING: Old symbol skipString: file verification/cbmc/include/core_json_annex.h, line 143
WARNING: New symbol skipString: file verification/cbmc/proofs/skipString/core_json.c, line 509
WARNING: Skipping redefinition of symbol name: skipString
WARNING: Old symbol skipString: file verification/cbmc/include/core_json_annex.h, line 143
WARNING: New symbol skipString: file MISSING, line 0
WARNING: Skipping source file annotation: wrapped functions for code contracts
Also, what does these warnings mean?
If this doesn't compromise the coverage report, then it should only be INFO instead of warnings.
@markrtuttle points out that we have various conflicting sources of data about where a symbol is defined, and that is (to an extent) unavoidable (because we use ctags as well as CBMC) and we have to pick one and when it is unavoidable then perhaps we shouldn't bother the user with a warning. But... looking at these warnings I have the following thoughts:
WARNING: Skipping redefinition of symbol name: JSON_Iterate WARNING: Old symbol JSON_Iterate: file verification/cbmc/proofs/skipString/core_json.c, line 1774 WARNING: New symbol JSON_Iterate: file source/include/core_json.h, line 326
If I have to pick one of two possible definitions, I would think I would prefer the one on the .c file and not the one in the header. If I was being pedantic (which is my natural inclination) I would say that the one in the header was a "declaration" not a "definition" and so there really was no choice here as to which to choose as the site of the definition ... choose the definition not the declaration.
In most of these examples I think I would:
- Choose the location of a definition over the location of a declaration.
- Choose data from cbmc over data from ctags
If ctags provides multiple equally preferable locations then just pick one silently. If cbmc provides multiple equally preferable locations then that should be a warning.
But, then there is this:
WARNING: Skipping redefinition of symbol name: skipString WARNING: Old symbol skipString: file verification/cbmc/include/core_json_annex.h, line 143 WARNING: New symbol skipString: file MISSING, line 0
This is very much not OK. This is exactly why I like to keep warnings around, to surface things like this and force them to be fixed. We just sunk a whole bunch of @nwetzler into making sure this doesn't happen, so if that data came from CBMC then let's get it fixed.
@markrtuttle : please don't make this particular warning go away. Can you confirm that the bad data is coming from CBMC, and if so assign to @nwetzler to fix.
