Noisy errors and warnings on simple function verification

[rod-chapman]

I am trying to use the starter kit with CBMC 5.84 to verify a few simple functions, but using the function contracts, DFCC, and loop invariant support that was recently introduced. I have followed the instructions here to create a cbmc/proofs/X subdirectory for function X, with a suitable Makefile, which (amongst other things) contains:

PROOF_UID = X

HARNESS_ENTRY = harness
HARNESS_FILE = $(PROOF_UID)_harness

APPLY_LOOP_CONTRACTS = 1
USE_DYNAMIC_FRAMES = 1
CHECK_FUNCTION_CONTRACTS ?= $(PROOF_UID)

When I run "make" the analysis seems to run OK and produce a sensible-looking report, but I get several warnings and errors on screen that I don't understand or know how to get rid of. Specifically, I get:

rodchap@f4d4889dcf6d X_Init % make
Running litani init
Report will be rendered at file:///var/folders/83/zx9jk1g53wjcr2xvycvs7xjh0000gr/T/litani/runs/latest/html/index.html
Running litani add-job
Running litani build
[9/16] X_Init: checking function contracts                                                                                        file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value

symbol '__CPROVER_alloca_object' already has an initial value

symbol '__CPROVER_new_object' already has an initial value

file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value

no body for function '__CPROVER_assignable'

no body for function '__CPROVER_assignable'

[16/16] X_Init: generating report                                                                                                 WARNING: Skipping malformed coverage data in /Users/rodchap/Desktop/rod/projects/crypto/brazil/src/AWS-LC/third-party-src/crypto/x/cbmc/proofs/X_Init/logs/coverage.xml.

WARNING: Use the --verbose to see what coverage data was skipped.

WARNING: Skipping redefinition of symbol name: X_Init

WARNING:   Old symbol X_Init: file third-party-src/crypto/x/x.c, line 29

WARNING:   New symbol X_Init: file MISSING, line 0

WARNING: Skipping redefinition of symbol name: X_Final

WARNING:   Old symbol X_Final: file third-party-src/crypto/x/x.c, line 43

WARNING:   New symbol X_Final: file third-party-src/include/openssl/x.h, line 47

WARNING: Skipping redefinition of symbol name: X_Init

WARNING:   Old symbol X_Init: file third-party-src/crypto/x/x.c, line 29

WARNING:   New symbol X_Init: file third-party-src/include/openssl/x.h, line 32

WARNING: Skipping redefinition of symbol name: X_Update

WARNING:   Old symbol X_Update: file third-party-src/crypto/x/x.c, line 37

WARNING:   New symbol X_Update: file third-party-src/include/openssl/x.h, line 39

WARNING: Skipping redefinition of symbol name: x_block_data_order

WARNING:   Old symbol x_block_data_order: file third-party-src/crypto/x/internal.h, line 24

WARNING:   New symbol x_block_data_order: file third-party-src/crypto/x/x.c, line 119

WARNING: Skipping source file annotation: wrapped functions for code contracts


Report was rendered at file:///var/folders/83/zx9jk1g53wjcr2xvycvs7xjh0000gr/T/litani/runs/latest/html/index.html

What did I do wrong?

[feliperodri]

Thanks for the report, @rod-chapman!

These are generic CBMC errors, not specific to contracts. They do not affect your analysis.

symbol '__CPROVER_alloca_object' already has an initial value

symbol '__CPROVER_new_object' already has an initial value

file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value

These are spurious warnings resulted from the combination of temporary variables created during contract instrumentation and other passes over the GOTO binary. You’re doing the right thing. We need to find a way to solve these warnings on our side and they do not affect your analysis as well.

no body for function '__CPROVER_assignable'

no body for function '__CPROVER_assignable'

These are emitted by the Python function that generates the final HTML report. We have an issue tracking these model-checking/cbmc-viewer#133. If you find them noise, you can also post your feedback on that issue.

WARNING: Use the --verbose to see what coverage data was skipped.

WARNING: Skipping redefinition of symbol name: X_Init

WARNING:   Old symbol X_Init: file third-party-src/crypto/x/x.c, line 29

WARNING:   New symbol X_Init: file MISSING, line 0

WARNING: Skipping redefinition of symbol name: X_Final

WARNING:   Old symbol X_Final: file third-party-src/crypto/x/x.c, line 43

WARNING:   New symbol X_Final: file third-party-src/include/openssl/x.h, line 47

WARNING: Skipping redefinition of symbol name: X_Init

WARNING:   Old symbol X_Init: file third-party-src/crypto/x/x.c, line 29

WARNING:   New symbol X_Init: file third-party-src/include/openssl/x.h, line 32

WARNING: Skipping redefinition of symbol name: X_Update

WARNING:   Old symbol X_Update: file third-party-src/crypto/x/x.c, line 37

WARNING:   New symbol X_Update: file third-party-src/include/openssl/x.h, line 39

WARNING: Skipping redefinition of symbol name: x_block_data_order

WARNING:   Old symbol x_block_data_order: file third-party-src/crypto/x/internal.h, line 24

WARNING:   New symbol x_block_data_order: file third-party-src/crypto/x/x.c, line 119

WARNING: Skipping source file annotation: wrapped functions for code contracts

[rod-chapman]

In general, an analysis tool like this should never issue a warning or an error that the user doesn't understand and/or doesn't know how to fix.

Issuing spurious warning and errors is a complete trust-breaker for new users.