Noisy errors and warnings on simple function verification #198
Description
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?