cbmc-starter-kit
cbmc-starter-kit copied to clipboard
model-checking
Noisy errors and warnings on simple function verification
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?
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 https://github.com/model-checking/cbmc-viewer/issues/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
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.