Missing source location for DFCC instrumentation

[feliperodri]

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]

@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]

This issue is on the Viewer side, so replacing it with model-checking/cbmc-viewer#133.