Invariant violation parsing simple C program #6566
Description
CBMC version: 5.48.0 (cbmc-5.48.0-4-g169dc1865c)
Operating system: Linux Mint 20 Ulyana
Exact command line resulting in the issue: cbmc --function f problem.c
What behaviour did you expect: CBMC parses the program and reports no error
What happened instead: invariant check failed
CBMC version 5.48.0 (cbmc-5.48.0-4-g169dc1865c) 64-bit x86_64 linux
Parsing problem.c
Converting
Type-checking problem
--- begin invariant violation report ---
Invariant check failed
File: ../src/ansi-c/c_nondet_symbol_factory.cpp:222 function: c_nondet_symbol_factory
Condition: !moving_symbol_failed
Reason: Check return value
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x51) [0x55661fdec0a8]
cbmc(get_backtrace[abi:cxx11]()+0x44) [0x55661fdec2b4]
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&)+0x52) [0x55661f5b96cd]
cbmc(+0x897d9b) [0x55661f5b8d9b]
cbmc(c_nondet_symbol_factory(code_blockt&, symbol_tablet&, dstringt, typet const&, source_locationt const&, c_object_factory_parameterst const&, lifetimet)+0x2a9) [0x55661f8cd38f]
cbmc(build_function_environment(std::vector<code_typet::parametert, std::allocator<code_typet::parametert> > const&, code_blockt&, symbol_tablet&, c_object_factory_parameterst const&)+0x1ba) [0x55661f8b909a]
cbmc(generate_ansi_c_start_function(symbolt const&, symbol_tablet&, message_handlert&, c_object_factory_parameterst const&)+0x21e7) [0x55661f8bbaf5]
cbmc(ansi_c_entry_point(symbol_tablet&, message_handlert&, c_object_factory_parameterst const&)+0x54f) [0x55661f8b9875]
cbmc(ansi_c_languaget::generate_support_functions(symbol_tablet&)+0x41) [0x55661f8bfe49]
cbmc(+0xca44a8) [0x55661f9c54a8]
cbmc(initialize_goto_model(std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > const&, message_handlert&, optionst const&)+0xaad) [0x55661f9c61b3]
cbmc(cbmc_parse_optionst::get_goto_program(goto_modelt&, optionst const&, cmdlinet const&, ui_message_handlert&)+0xc3) [0x55661f5c3daf]
cbmc(cbmc_parse_optionst::doit()+0x7e6) [0x55661f5c228e]
cbmc(parse_options_baset::main()+0x113) [0x55661fe12c87]
cbmc(main+0x59) [0x55661f5b8ac2]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f05f114c0b3]
cbmc(_start+0x2e) [0x55661f5b89ae]
--- end invariant violation report ---
fish: “cbmc --function f problem.c” terminated by signal SIGABRT (Abort)
the problematic file contains only:
void f(int* b, int tmp) {}This was found in a larger program and reduced with the help of c-reduce.