goto-analyzer fails with an irep.data nullptr

[rurban]

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]

Thanks for the bug report. I will try to fix when I have time.