Failure to supply sources for function under verification causes unhelpful crash

[rod-chapman]

CBMC version: 6.3.1
Operating system: macOS
Exact command line resulting in the issue: "make"
What behaviour did you expect: Failure with an understandable error message
What happened instead: Crash/stackdump/unhelpful error message

Problem: I tried to create a new proof for a function using contracts, but I forgot to change the definition of PROJECT_SOURCES in the Makefile to include the source file that contains that function. This causes goto-instrument to crash with a non-obvious error message.

For example:

[9/13] cmov_int16: checking function contracts                                                                                                                         FAILED: /Users/rodchap/Desktop/rod/projects/crypto/pqcp/pqcp/cbmc/proofs/cmov_int16/gotos/cmov_int16_harness0600.goto /tmp/nix-shell.uejkGk/litani/runs/49a29b0a-2979-4326-b204-e8a1bf76b495/status/e7c1849b-9c7b-498d-92a3-c99fb5c02cca.json 

/nix/store/8siznzd0h4w83hjqczx3j186nkbshlgn-litani-8002c240ef4f424039ed3cc32e076c0234d01768/bin/litani exec --command 'goto-instrument   --dfcc harness    --enforce-contract PQCP_MLKEM_NATIVE_MLKEM768_cmov_int16  --apply-loop-contracts /Users/rodchap/Desktop/rod/projects/crypto/pqcp/pqcp/cbmc/proofs/cmov_int16/gotos/cmov_int16_harness0500.goto /Users/rodchap/Desktop/rod/projects/crypto/pqcp/pqcp/cbmc/proofs/cmov_int16/gotos/cmov_int16_harness0600.goto' --pipeline-name cmov_int16 --ci-stage build --job-id e7c1849b-9c7b-498d-92a3-c99fb5c02cca --stdout-file /Users/rodchap/Desktop/rod/projects/crypto/pqcp/pqcp/cbmc/proofs/cmov_int16/logs/check_function_contracts-log.txt --description 'cmov_int16: checking function contracts' --status-file /tmp/nix-shell.uejkGk/litani/runs/49a29b0a-2979-4326-b204-e8a1bf76b495/status/e7c1849b-9c7b-498d-92a3-c99fb5c02cca.json --profile-memory-interval 10 --inputs /Users/rodchap/Desktop/rod/projects/crypto/pqcp/pqcp/cbmc/proofs/cmov_int16/gotos/cmov_int16_harness0500.goto --outputs /Users/rodchap/Desktop/rod/projects/crypto/pqcp/pqcp/cbmc/proofs/cmov_int16/gotos/cmov_int16_harness0600.goto

--- begin invariant violation report ---

Invariant check failed

File: /tmp/nix-build-cbmc-6.3.1.drv-0/source/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp:206 function: check_transform_goto_model_preconditions

Condition: Precondition

Reason: dfcc_utilst::function_symbol_with_body_exists(goto_model, pair.first)

Backtrace:

0   goto-instrument                     0x0000000100b4d710 _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 124

1   goto-instrument                     0x0000000100b4dbb0 _Z13get_backtracev + 180

2   goto-instrument                     0x0000000100bda6f0 _Z29invariant_violated_structuredI34invariant_with_diagnostics_failedtJRNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEES7_EENS1_9enable_ifIXsr3std10is_base_ofI17invariant_failedtT_EE5valueEvE4typeERKS7_SF_iSF_DpOT0_ + 76

3   goto-instrument                     0x000000010066b02c _Z24report_invariant_failureIJNSt3__112basic_stringIcNS0_11char_traitsIcEENS0_9allocatorIcEEEEEEvRKS6_S8_iS6_S6_DpOT_ + 100

4   goto-instrument                     0x000000010066a794 _ZN5dfcct40check_transform_goto_model_preconditionsEv + 1292

5   goto-instrument                     0x000000010066a004 _ZN5dfcct20transform_goto_modelEv + 24

6   goto-instrument                     0x0000000100669ecc _ZN5dfcctC2ERK8optionstR11goto_modeltRK8dstringtRKNSt3__18optionalINS8_4pairIS5_S5_EEEEbRKNS8_3mapIS5_S5_NS8_4lessIS5_EENS8_9allocatorINSA_IS6_S5_EEEEEE21loop_contract_configtR16message_handlertRKNS8_3setINS8_12basic_stringIcNS8_11char_traitsIcEENSI_IcEEEENSG_ISW_EENSI_ISW_EEEE + 560

7   goto-instrument                     0x0000000100669598 _Z4dfccRK8optionstR11goto_modeltRK8dstringtRKNSt3__18optionalIS4_EEbRKNS7_3setIS4_NS7_4lessIS4_EENS7_9allocatorIS4_EEEE21loop_contract_configtRKNSC_INS7_12basic_stringIcNS7_11char_traitsIcEENSF_IcEEEENSD_ISP_EENSF_ISP_EEEER16message_handlert + 404

8   goto-instrument                     0x00000001006ec37c _ZN30goto_instrument_parse_optionst23instrument_goto_programEv + 8080

9   goto-instrument                     0x00000001006e7adc _ZN30goto_instrument_parse_optionst4doitEv + 660

10  goto-instrument                     0x0000000100b7b160 _ZN19parse_options_baset4mainEv + 220

11  goto-instrument                     0x000000010062e258 main + 56

12  dyld                                0x000000018bd97154 start + 2476



Diagnostics:

<< EXTRA DIAGNOSTICS >>

Function to check 'PQCP_MLKEM_NATIVE_MLKEM768_cmov_int16' either not found or has no body

<< END EXTRA DIAGNOSTICS >>



--- end invariant violation report ---

Please get rid of the stack-trace/crash report. A simple error message such as

Verification of function XXX requested, but source code of that function has not been supplied"

might be better.