Repository navigation
Default flags in cargo-rmc cause CBMC inviariant violation #289
Description
Running the regression with the new default flags feature from #263 causes the following error:
CBMC version 5.30.1 (cbmc-5.30.1) 64-bit x86_64 linux
Reading GOTO program from file
Reading: /home/ubuntu/rmc-rebase-3/build/x86_64-unknown-linux-gnu/test/cargo-rmc/simple-lib/test_one_plus_two/target/cbmc.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
--- begin invariant violation report ---
Invariant check failed
File: ../src/util/namespace.h:47 function: lookup
Condition: !not_found
Reason: we are assuming that a name exists in the namespace when this function is called - identifier __CPROVER_dead_object was not found
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x5632a23794b0]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x5632a2379a59]
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&)+0x48) [0x5632a1c6bc78]
cbmc(namespace_baset::lookup(dstringt const&) const+0xf3) [0x5632a1d404e3]
cbmc(goto_checkt::goto_check(dstringt const&, goto_functiont&)+0x2658) [0x5632a210bea8]
cbmc(goto_check(namespacet const&, optionst const&, goto_functionst&)+0x60) [0x5632a210d530]
cbmc(goto_check(optionst const&, goto_modelt&)+0x4e) [0x5632a210d74e]
cbmc(process_goto_program(goto_modelt&, optionst const&, messaget&)+0x527) [0x5632a1ffd327]
cbmc(cbmc_parse_optionst::process_goto_program(goto_modelt&, optionst const&, messaget&)+0x139) [0x5632a1c6d489]
cbmc(cbmc_parse_optionst::get_goto_program(goto_modelt&, optionst const&, cmdlinet const&, ui_message_handlert&)+0x5df) [0x5632a1c6e1bf]
cbmc(cbmc_parse_optionst::doit()+0x5af) [0x5632a1c72b8f]
cbmc(parse_options_baset::main()+0x8f) [0x5632a1c69e3f]
cbmc(main+0x39) [0x5632a1c594e9]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f44c72740b3]
cbmc(_start+0x2e) [0x5632a1c6b68e]
--- end invariant violation report ---
------------------------------------------
stderr:
------------------------------------------
------------------------------------------
failures:
[cargo-rmc] cargo-rmc/simple-lib/test_one_plus_two.expected
[cargo-rmc] cargo-rmc/simple-lib/test_sum.expected
test result: FAILED. 0 passed; 2 failed; 1 ignored; 0 measured; 0 filtered out; finished in 0.75s
Because of that, we call RMC with --no-default-checks but the goal is to remove this argument when running the tests.
Activity
adpaco commentedon Jul 7, 2021
More specifically, the failure can be avoided with
--no-memory-safety-checks. I suppose one of the CBMC memory-safety flags used by default is adding some verification condition that calls__CPROVER_dead_objectwhich is not found.adpaco commentedon Jul 7, 2021
I think the root cause is issue 2 from #105. The
cargo-rmcprocess is missing agoto-ccinvocation that includes all JSON files and an empty C file so that some (CProver) builtins are included, like we do in the case of the balloon demo: nchong-at-aws/firecracker@5e07037