Closed
Description
CBMC version: 6.0.0-alpha (build 24th May 2024)
Exact command line resulting in the issue: make TARGET=ctcc
What behaviour did you expect: It should work!
What happened instead:
CBMC crashes on verification of the "ctcc" function in the latest version of code here:
https://github.com/rod-chapman/cbmc-examples/tree/main/arrays
The on-screen output ends with:
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: /Users/rodchap/Desktop/rod/tools/src/cbmc/src/util/lower_byte_operators.cpp:403 function: bv_to_expr
Condition: Precondition
Reason: false
Backtrace:
0 cbmc 0x0000000102d67928 _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 124
1 cbmc 0x0000000102d67db4 _Z13get_backtracev + 160
2 cbmc 0x0000000102896568 _Z29invariant_violated_structuredI34invariant_with_diagnostics_failedtJRNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEES7_EENS1_9enable_ifIXsr3std10is_base_ofI17invariant_failedtT_EE5valueEvE4typeERKS7_SF_iSF_DpOT0_ + 60
3 cbmc 0x0000000102d8343c _Z24report_invariant_failureIJRA33_KcRKNSt3__112basic_stringIcNS3_11char_traitsIcEENS3_9allocatorIcEEEEEEvSB_SB_iS9_S9_DpOT_ + 88
4 cbmc 0x0000000102d78ddc _ZL10bv_to_exprRK5exprtRK5typetRK15endianness_maptRK10namespacet + 1500
5 cbmc 0x0000000102d81778 _ZL17bv_to_struct_exprRK5exprtRK12struct_typetRK15endianness_maptRK10namespacet + 424
6 cbmc 0x0000000102d78afc _ZL10bv_to_exprRK5exprtRK5typetRK15endianness_maptRK10namespacet + 764
7 cbmc 0x0000000102d74058 _Z18lower_byte_extractRK18byte_extract_exprtRK10namespacet + 3364
8 cbmc 0x0000000102d7a944 _ZL17lower_byte_updateRK17byte_update_exprtRK5exprtRKNSt3__18optionalIS2_EERK10namespacet + 2884
9 cbmc 0x0000000102d79680 _Z17lower_byte_updateRK17byte_update_exprtRK10namespacet + 1880
10 cbmc 0x0000000102d83d0c _ZL40lower_byte_update_array_vector_non_constRK17byte_update_exprtRK5typetRK5exprtRKNSt3__18optionalIS5_EERK10namespacet + 1020
11 cbmc 0x0000000102d7a34c _ZL17lower_byte_updateRK17byte_update_exprtRK5exprtRKNSt3__18optionalIS2_EERK10namespacet + 1356
12 cbmc 0x0000000102d79680 _Z17lower_byte_updateRK17byte_update_exprtRK10namespacet + 1880
13 cbmc 0x0000000102c410f4 _ZN10smt2_convt20lower_byte_operatorsERK5exprt + 544
14 cbmc 0x0000000102c30e0c _ZN10smt2_convt24prepare_for_convert_exprERK5exprt + 64
15 cbmc 0x0000000102c4086c _ZN10smt2_convt6set_toERK5exprtb + 964
16 cbmc 0x00000001029d5a84 _ZN22symex_target_equationt19convert_assignmentsER19decision_proceduret + 268
17 cbmc 0x00000001029d5654 _ZN22symex_target_equationt26convert_without_assertionsER19decision_proceduret + 224
18 cbmc 0x00000001029d6f48 _ZN22symex_target_equationt7convertER19decision_proceduret + 48
19 cbmc 0x000000010286d450 _Z29convert_symex_target_equationR22symex_target_equationtR19decision_proceduretR16message_handlert + 264
20 cbmc 0x000000010286eb2c _Z24prepare_property_deciderRNSt3__13mapI8dstringt14property_infotNS_4lessIS1_EENS_9allocatorINS_4pairIKS1_S2_EEEEEER22symex_target_equationtR28goto_symex_property_decidertR19ui_message_handlert + 380
21 cbmc 0x000000010287a9a4 _ZN25multi_path_symex_checkertclERNSt3__13mapI8dstringt14property_infotNS0_4lessIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 236
22 cbmc 0x000000010286b4d4 _ZN43all_properties_verifier_with_trace_storagetI25multi_path_symex_checkertEclEv + 84
23 cbmc 0x0000000102862fc4 _ZN19cbmc_parse_optionst4doitEv + 3060
24 cbmc 0x0000000102d91fc4 _ZN19parse_options_baset4mainEv + 180
25 cbmc 0x0000000102857474 main + 40
26 dyld 0x0000000182407f28 start + 2236
Diagnostics:
<< EXTRA DIAGNOSTICS >>
bv_to_expr does not yet support
bool
<< END EXTRA DIAGNOSTICS >>
--- end invariant violation report ---
Can you reproduce and confirm please?