search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
842 stars 262 forks source link

Missing source location for DFCC instrumentation #7350

Closed feliperodri closed 1 year ago

feliperodri commented 1 year ago

CBMC version: 5.69.1 (cbmc-5.59.0-676-gb4a4122dee) 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?

tautschnig commented 1 year ago

@feliperodri Can you clarify which of the warnings you are referring to? Most of the ones you list have a source location, relate to linking, and need to be investigated in the context of the project under verification (it seems the file core_json.c file is generated at build time, but perhaps is inconsistent with the declaration?!). Then there is file MISSING, which I don't know where it might originate from. Finally, there is the "Skipping source file annotation: wrapped functions for code contracts?!"

feliperodri commented 1 year ago

This issue is on the Viewer side, so replacing it with https://github.com/model-checking/cbmc-viewer/issues/133.