Closed
Description
CBMC version: 5.29.0
Operating system: Ubuntu20
Exact command line resulting in the issue: See below
What behaviour did you expect: Test passes
What happened instead: Test fails
The modifications proposed in #6077 have shown the existence of a bug in CBMC. Currently, CBMC does not support calling __CPROVER_w_ok() by passing a char object as a parameter.
This bug causes problems in the regression/contracts/assigns_replace_03 test. Running the test outputs the following invariant violation report:
--- begin invariant violation report ---
Invariant check failed
File: ../../src/solvers/flattening/boolbv_width.cpp:197 function: get_entry
Condition: false
Reason: Unimplemented
Backtrace:
../../../build/bab/bin/cbmc(print_backtrace(std::ostream&)+0x3e) [0x129aedd]
../../../build/bab/bin/cbmc(get_backtrace[abi:cxx11]()+0x36) [0x129b088]
../../../build/bab/bin/cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x3c) [0xba91c7]
../../../build/bab/bin/cbmc() [0xba8a7f]
../../../build/bab/bin/cbmc(boolbv_widtht::get_entry(typet const&) const+0x121b) [0x109bc75]
../../../build/bab/bin/cbmc(boolbv_widtht::operator()(typet const&) const+0x23) [0xc0008b]
../../../build/bab/bin/cbmc(bv_pointerst::bv_pointers_widtht::operator()(typet const&) const+0x53) [0x10a1437]
../../../build/bab/bin/cbmc(bv_pointerst::boolbv_width(typet const&) const+0x2c) [0xc00b7e]
../../../build/bab/bin/cbmc(boolbvt::type_conversion(typet const&, std::vector<literalt, std::allocator<literalt> > const&, typet const&, std::vector<literalt, std::allocator<literalt> >&)+0x1a0) [0x109445c]
../../../build/bab/bin/cbmc(boolbvt::convert_bv_typecast(typecast_exprt const&)+0xb5) [0x109423d]
../../../build/bab/bin/cbmc(boolbvt::convert_bitvector(exprt const&)+0x47f) [0x1060265]
../../../build/bab/bin/cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x18e7) [0x10a773d]
../../../build/bab/bin/cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xef) [0x105f82d]
../../../build/bab/bin/cbmc(boolbvt::convert_bv_typecast(typecast_exprt const&)+0x61) [0x10941e9]
../../../build/bab/bin/cbmc(boolbvt::convert_bitvector(exprt const&)+0x47f) [0x1060265]
../../../build/bab/bin/cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x18e7) [0x10a773d]
../../../build/bab/bin/cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0xef) [0x105f82d]
../../../build/bab/bin/cbmc(boolbvt::convert_bv_rel(binary_relation_exprt const&)+0xf0) [0x106d9d2]
../../../build/bab/bin/cbmc(boolbvt::convert_rest(exprt const&)+0x4cc) [0x10628ba]
../../../build/bab/bin/cbmc(bv_pointerst::convert_rest(exprt const&)+0x8ab) [0x10a2177]
../../../build/bab/bin/cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x1507) [0x10e5b75]
../../../build/bab/bin/cbmc(prop_conv_solvert::convert(exprt const&)+0x181) [0x10e4597]
../../../build/bab/bin/cbmc(prop_conv_solvert::convert_bool(exprt const&)+0xef2) [0x10e5560]
../../../build/bab/bin/cbmc(prop_conv_solvert::convert(exprt const&)+0x181) [0x10e4597]
../../../build/bab/bin/cbmc(prop_conv_solvert::convert_bool(exprt const&)+0xb2e) [0x10e519c]
../../../build/bab/bin/cbmc(prop_conv_solvert::convert(exprt const&)+0x181) [0x10e4597]
../../../build/bab/bin/cbmc(prop_conv_solvert::convert_bool(exprt const&)+0xef2) [0x10e5560]
../../../build/bab/bin/cbmc(prop_conv_solvert::convert(exprt const&)+0x181) [0x10e4597]
../../../build/bab/bin/cbmc(prop_conv_solvert::set_equality_to_true(equal_exprt const&)+0x9c) [0x10e60a8]
../../../build/bab/bin/cbmc(prop_conv_solvert::add_constraints_to_prop(exprt const&, bool)+0x565) [0x10e6695]
../../../build/bab/bin/cbmc(prop_conv_solvert::set_to(exprt const&, bool)+0x43) [0x10e70e7]
../../../build/bab/bin/cbmc(boolbvt::set_to(exprt const&, bool)+0x18e) [0x10645c0]
../../../build/bab/bin/cbmc(decision_proceduret::set_to_true(exprt const&)+0x2c) [0x104fff6]
../../../build/bab/bin/cbmc(symex_target_equationt::convert_assignments(decision_proceduret&)+0x130) [0xdfbcbe]
../../../build/bab/bin/cbmc(symex_target_equationt::convert_without_assertions(decision_proceduret&)+0x69) [0xdfb9cd]
../../../build/bab/bin/cbmc(symex_target_equationt::convert(decision_proceduret&)+0x2f) [0xdfba91]
../../../build/bab/bin/cbmc(convert_symex_target_equation(symex_target_equationt&, decision_proceduret&, message_handlert&)+0x80) [0xbd5f86]
../../../build/bab/bin/cbmc(prepare_property_decider(std::unordered_map<dstringt, property_infot, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&, symex_target_equationt&, goto_symex_property_decidert&, ui_message_handlert&)+0xeb) [0xbd71aa]
../../../build/bab/bin/cbmc(multi_path_symex_checkert::prepare_property_decider(std::unordered_map<dstringt, property_infot, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&)+0x40) [0xbe8ef6]
../../../build/bab/bin/cbmc(multi_path_symex_checkert::operator()(std::unordered_map<dstringt, property_infot, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&)+0x1c2) [0xbe8dd2]
../../../build/bab/bin/cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator()()+0x45) [0xbc5f2d]
../../../build/bab/bin/cbmc(cbmc_parse_optionst::doit()+0x192e) [0xbb3384]
../../../build/bab/bin/cbmc(parse_options_baset::main()+0x106) [0x12bf8fc]
../../../build/bab/bin/cbmc(main+0x46) [0xba87fd]
/lib64/libc.so.6(__libc_start_main+0xea) [0x7fd80685d0ba]
../../../build/bab/bin/cbmc(_start+0x2a) [0xba871a]
--- end invariant violation report ---
Note 1: If we change type of the char variable to int and re-run the test, the test passes.
Note 2: if we change the char ** to char *, the pass still fails and outputs the same error.