search

model-checking / cbmc-viewer

CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.
https://model-checking.github.io/cbmc-viewer/
Apache License 2.0
32 stars 11 forks source link

Suppress unhelpful warnings for better user experience #133

Open feliperodri opened 1 year ago

feliperodri commented 1 year ago

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.

feliperodri commented 1 year ago

cc. @jimgrundy

jimgrundy commented 1 year ago

@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: 1) Choose the location of a definition over the location of a declaration. 2) 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.