goto-analyzer fails with an irep.data nullptr
Opened this issue · 1 comments
rurban commented
CBMC version: latest develop 6.0.0-preview (cbmc-6.0.0-alpha-324-g08b2f2f2dce)
Operating system: Fedora fc39
Exact command line resulting in the issue:
build cbmc as Debug and copy the goto-analyzer to goto-analyzer-debug
git clone https://github.com/rurban/smart
cd smart
gdb --args goto-analyzer-debug --verify --recursive-interprocedural --vsd --vsd-values intervals --vsd-structs every-field --vsd-arrays smash --vsd-pointers value-set source/algos/sbndm-w6.c
Program received signal SIGSEGV, Segmentation fault.
0x0000000000429b2c in sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::sharing_treet (this=0x7fffffffa6a8, irep=...)
at /home/rurban/Software/cbmc/src/util/irep.h:173
173 PRECONDITION(data->ref_count != 0);
(gdb) p data
$1 = (sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::dt *) 0x0
(gdb) l
168 // copy constructor
169 sharing_treet(const sharing_treet &irep) : data(irep.data)
170 {
171 if(data!=&empty_d)
172 {
173 PRECONDITION(data->ref_count != 0);
174 data->ref_count++;
175 #ifdef IREP_DEBUG
176 std::cout << "COPY " << data << " " << data->ref_count << '\n';
177 #endif
(gdb) bt
#0 0x0000000000429b2c in sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >::sharing_treet (this=0x7fffffffa6a8, irep=...)
at /home/rurban/Software/cbmc/src/util/irep.h:173
#1 0x0000000000427d25 in irept::irept (this=0x7fffffffa6a8) at /home/rurban/Software/cbmc/src/util/irep.h:347
#2 0x0000000000427ed5 in exprt::exprt (this=0x7fffffffa6a8) at /home/rurban/Software/cbmc/src/util/expr.h:55
#3 0x000000000084dd21 in value_set_pointer_abstract_objectt::ptr_comparison_expr (this=0x17693d0, expr=...,
operands=std::vector of length 2, capacity 2 = {...}, environment=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp:186
#4 0x0000000000855e63 in abstract_pointer_objectt::eval_ptr_comparison (this=0x17693d0, expr=...,
operands=std::vector of length 2, capacity 2 = {...}, environment=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/variable-sensitivity/abstract_pointer_object.cpp:113
#5 0x0000000000855b38 in abstract_pointer_objectt::expression_transform (this=0x17693d0, expr=...,
operands=std::vector of length 2, capacity 2 = {...}, environment=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/variable-sensitivity/abstract_pointer_object.cpp:53
#6 0x00000000007e4d46 in context_abstract_objectt::expression_transform (this=0x17c8c50, expr=...,
operands=std::vector of length 2, capacity 2 = {...}, environment=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/variable-sensitivity/context_abstract_object.cpp:104
#7 0x00000000007b79cd in abstract_environmentt::eval (this=0x17c13a8, expr=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/variable-sensitivity/abstract_environment.cpp:116
#8 0x00000000007ba644 in eval_operands (expr=..., env=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/variable-sensitivity/abstract_environment.cpp:552
#9 0x00000000007b9ca1 in abstract_environmentt::eval_expression (this=0x17c13a8, e=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/variable-sensitivity/abstract_environment.cpp:473
#10 0x00000000007b7b31 in abstract_environmentt::eval (this=0x17c13a8, expr=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/variable-sensitivity/abstract_environment.cpp:131
#11 0x000000000080c27f in variable_sensitivity_domaint::ai_simplify (this=0x17c13a0, condition=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp:245
#12 0x000000000080d86b in variable_sensitivity_domaint::assume (this=0x17c13a0, expr=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp:454
#13 0x000000000080b61c in variable_sensitivity_domaint::transform (this=0x17c13a0, function_from=...,
trace_from=std::shared_ptr<const ai_history_baset> (use count 6, weak count 0) = {...}, function_to=...,
trace_to=std::shared_ptr<const ai_history_baset> (use count 3, weak count 0) = {...}, ai=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp:84
#14 0x0000000000750df2 in ai_baset::visit_edge (this=0x15bbda0, function_id=...,
p=std::shared_ptr<const ai_history_baset> (use count 6, weak count 0) = {...}, to_function_id=..., to_l=...,
caller_history=std::shared_ptr<const ai_history_baset> (empty) = {...}, ns=..., working_set=std::set with 2 elements = {...})
at /home/rurban/Software/cbmc/src/analyses/ai.cpp:368
--Type <RET> for more, q to quit, c to continue without paging--
#15 0x00000000007507be in ai_baset::visit (this=0x15bbda0, function_id=...,
p=std::shared_ptr<const ai_history_baset> (use count 6, weak count 0) = {...}, working_set=std::set with 2 elements = {...},
goto_program=..., goto_functions=..., ns=...) at /home/rurban/Software/cbmc/src/analyses/ai.cpp:314
#16 0x000000000074fe51 in ai_baset::fixedpoint (this=0x15bbda0,
start_trace=std::shared_ptr<const ai_history_baset> (use count 3, weak count 0) = {...}, function_id=..., goto_program=...,
goto_functions=..., ns=...) at /home/rurban/Software/cbmc/src/analyses/ai.cpp:248
#17 0x000000000075216d in ai_recursive_interproceduralt::visit_edge_function_call (this=0x15bbda0, calling_function_id=...,
p_call=std::shared_ptr<const ai_history_baset> (use count 6, weak count 0) = {...}, l_return=..., callee_function_id=...,
working_set=std::set with 0 elements, callee=..., goto_functions=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/ai.cpp:576
#18 0x00000000007518c4 in ai_baset::visit_function_call (this=0x15bbda0, calling_function_id=...,
p_call=std::shared_ptr<const ai_history_baset> (use count 6, weak count 0) = {...}, working_set=std::set with 0 elements,
caller=..., goto_functions=..., ns=...) at /home/rurban/Software/cbmc/src/analyses/ai.cpp:483
#19 0x00000000007504cd in ai_baset::visit (this=0x15bbda0, function_id=...,
p=std::shared_ptr<const ai_history_baset> (use count 6, weak count 0) = {...}, working_set=std::set with 0 elements,
goto_program=..., goto_functions=..., ns=...) at /home/rurban/Software/cbmc/src/analyses/ai.cpp:293
#20 0x000000000074fe51 in ai_baset::fixedpoint (this=0x15bbda0,
start_trace=std::shared_ptr<const ai_history_baset> (use count 5, weak count 0) = {...}, function_id=..., goto_program=...,
goto_functions=..., ns=...) at /home/rurban/Software/cbmc/src/analyses/ai.cpp:248
#21 0x000000000075006d in ai_baset::fixedpoint (this=0x15bbda0,
start_trace=std::shared_ptr<const ai_history_baset> (use count 5, weak count 0) = {...}, goto_functions=..., ns=...)
at /home/rurban/Software/cbmc/src/analyses/ai.cpp:264
#22 0x000000000041865b in ai_baset::operator() (this=0x15bbda0, goto_model=...) at /home/rurban/Software/cbmc/src/analyses/ai.h:172
#23 0x0000000000415dec in goto_analyzer_parse_optionst::perform_analysis (this=0x7fffffffd630, options=...)
at /home/rurban/Software/cbmc/src/goto-analyzer/goto_analyzer_parse_options.cpp:629
#24 0x0000000000414ca7 in goto_analyzer_parse_optionst::doit (this=0x7fffffffd630)
at /home/rurban/Software/cbmc/src/goto-analyzer/goto_analyzer_parse_options.cpp:458
#25 0x000000000092e26a in parse_options_baset::main (this=0x7fffffffd630) at /home/rurban/Software/cbmc/src/util/parse_options.cpp:97
#26 0x000000000040a44c in main (argc=13, argv=0x7fffffffdac8)
at /home/rurban/Software/cbmc/src/goto-analyzer/goto_analyzer_main.cpp:28
(gdb) up
(gdb) up
(gdb) p comparisons
$2 = std::set with 0 elements
(gdb) p comparisons.cbegin()
$3 = {<irept> = {<sharing_treet<irept, forward_list_as_mapt<dstringt, irept> >> = {data = 0x0, static empty_d = {<ref_count_ift<true>> = {ref_count = 1}, data = {no = 0}, named_sub = {<std::forward_list<std::pair<dstringt, irept>, std::allocator<std::pair<dstringt, irept> > >> = empty std::forward_list, <No data fields>}, sub = std::vector of length 0, capacity 0, hash_code = 0}}, <No data fields>}, <No data fields>}
What behaviour did you expect:
no SEGV
What happened instead:
SEGV
I tried to check for the nullptr, but data=0x0 should not happen at all, I believe.
martin-cs commented
Thanks for the bug report. I will try to fix when I have time.