diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index b040ca51b8d..07bca6524af 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -191,8 +191,7 @@ void constant_propagator_domaint::transform( } else if(from->is_dead()) { - const auto &code_dead = from->get_dead(); - values.set_to_top(code_dead.symbol()); + values.set_to_top(from->dead_symbol()); } else if(from->is_function_call()) { diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 833c001d1d7..9639d03d3f8 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -304,14 +304,11 @@ void custom_bitvector_domaint::transform( break; case DEAD: - { - const code_deadt &code_dead=to_code_dead(instruction.code); - assign_lhs(code_dead.symbol(), vectorst()); + assign_lhs(instruction.dead_symbol(), vectorst()); - // is it a pointer? - if(code_dead.symbol().type().id()==ID_pointer) - assign_lhs(dereference_exprt(code_dead.symbol()), vectorst()); - } + // is it a pointer? + if(instruction.dead_symbol().type().id() == ID_pointer) + assign_lhs(dereference_exprt(instruction.dead_symbol()), vectorst()); break; case FUNCTION_CALL: diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 81f5b89621b..dc7335e0426 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -210,11 +210,8 @@ void escape_domaint::transform( break; case DEAD: - { - const code_deadt &code_dead=to_code_dead(instruction.code); - aliases.isolate(code_dead.get_identifier()); - assign_lhs_cleanup(code_dead.symbol(), std::set()); - } + aliases.isolate(instruction.dead_symbol().get_identifier()); + assign_lhs_cleanup(instruction.dead_symbol(), std::set()); break; case FUNCTION_CALL: @@ -487,14 +484,14 @@ void escape_analysist::instrument( } else if(instruction.type == DEAD) { - const code_deadt &code_dead = to_code_dead(instruction.code); + const auto &dead_symbol = instruction.dead_symbol(); std::set cleanup_functions1; const escape_domaint &d = operator[](i_it); const escape_domaint::cleanup_mapt::const_iterator m_it = - d.cleanup_map.find("&" + id2string(code_dead.get_identifier())); + d.cleanup_map.find("&" + id2string(dead_symbol.get_identifier())); // does it have a cleanup function for the object? if(m_it != d.cleanup_map.end()) @@ -506,22 +503,12 @@ void escape_analysist::instrument( std::set cleanup_functions2; - d.check_lhs(code_dead.symbol(), cleanup_functions2); + d.check_lhs(dead_symbol, cleanup_functions2); insert_cleanup( - gf_entry.second, - i_it, - code_dead.symbol(), - cleanup_functions1, - true, - ns); + gf_entry.second, i_it, dead_symbol, cleanup_functions1, true, ns); insert_cleanup( - gf_entry.second, - i_it, - code_dead.symbol(), - cleanup_functions2, - false, - ns); + gf_entry.second, i_it, dead_symbol, cleanup_functions2, false, ns); for(const auto &c : cleanup_functions1) { diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 72ae9fe7760..444224bc1f6 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -127,11 +127,8 @@ void global_may_alias_domaint::transform( } case DEAD: - { - const code_deadt &code_dead = to_code_dead(instruction.code); - aliases.isolate(code_dead.get_identifier()); + aliases.isolate(instruction.dead_symbol().get_identifier()); break; - } case FUNCTION_CALL: // Probably safe case GOTO: // Ignoring the guard is a valid over-approximation diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 056564e221e..ca56e0d1bf7 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -815,10 +815,7 @@ void goto_rw( case DEAD: rw_set.get_objects_rec( - function, - target, - rw_range_sett::get_modet::LHS_W, - to_code_dead(target->code).symbol()); + function, target, rw_range_sett::get_modet::LHS_W, target->dead_symbol()); break; case DECL: diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 96514e4355b..953120582df 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -75,7 +75,7 @@ void interval_domaint::transform( break; case DEAD: - havoc_rec(to_code_dead(instruction.code).symbol()); + havoc_rec(instruction.dead_symbol()); break; case ASSIGN: diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 17f635e54ec..fe81c619267 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -293,15 +293,12 @@ void local_bitvector_analysist::build() } case DEAD: - { - const code_deadt &code_dead = to_code_dead(instruction.code); assign_lhs( - code_dead.symbol(), + instruction.dead_symbol(), exprt(ID_uninitialized), loc_info_src, loc_info_dest); break; - } case FUNCTION_CALL: { diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index 5198b1cbb15..233c32a90e0 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -390,11 +390,9 @@ void local_may_aliast::build(const goto_functiont &goto_function) } case DEAD: - { - const code_deadt &code_dead = to_code_dead(instruction.code); - assign_lhs(code_dead.symbol(), nil_exprt(), loc_info_src, loc_info_dest); + assign_lhs( + instruction.dead_symbol(), nil_exprt(), loc_info_src, loc_info_dest); break; - } case FUNCTION_CALL: { diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index e370467220a..4cdb96f6565 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -169,7 +169,7 @@ void rd_range_domaint::transform_dead( const namespacet &, locationt from) { - const irep_idt &identifier = to_code_dead(from->code).get_identifier(); + const irep_idt &identifier = from->dead_symbol().get_identifier(); valuest::iterator entry=values.find(identifier); diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index 768b2d47083..6626aa88bd7 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -55,16 +55,10 @@ void variable_sensitivity_domaint::transform( break; case DEAD: - { // Remove symbol from map, the only time this occurs now (keep TOP.) // It should be the case that DEAD only provides symbols for deletion. - const exprt &expr = to_code_dead(instruction.code).symbol(); - if(expr.id() == ID_symbol) - { - abstract_state.erase(to_symbol_expr(expr)); - } - } - break; + abstract_state.erase(instruction.dead_symbol()); + break; case ASSIGN: { diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp index eaabbd0a356..43dea082cdf 100644 --- a/src/goto-diff/change_impact.cpp +++ b/src/goto-diff/change_impact.cpp @@ -84,7 +84,7 @@ void full_slicert::operator()( } else if(instruction->is_dead()) { - const auto &s=to_code_dead(instruction->code).symbol(); + const auto &s=instruction->dead_symbol(); decl_dead[s.get_identifier()].push(instruction_node_index); } } diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index bed5c47be44..7a881f57a75 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -290,7 +290,7 @@ void full_slicert::operator()( } else if(instruction->is_dead()) { - const auto &s = to_code_dead(instruction->code).symbol(); + const auto &s = instruction->dead_symbol(); decl_dead[s.get_identifier()].push(instruction_node_index); } } diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 379414c0bb3..915ae297352 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -94,7 +94,7 @@ void goto_program2codet::build_dead_map() { if(instruction.is_dead()) { - dead_map[instruction.get_dead().get_identifier()] = + dead_map[instruction.dead_symbol().get_identifier()] = instruction.location_number; } } diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index c74bad5cd0b..39c837c09be 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -884,9 +884,9 @@ void goto_programt::instructiont::validate( source_location); DATA_CHECK_WITH_DIAGNOSTICS( vm, - !ns.lookup(get_dead().get_identifier(), table_symbol), + !ns.lookup(dead_symbol().get_identifier(), table_symbol), "removed symbols should be known", - id2string(get_dead().get_identifier()), + id2string(dead_symbol().get_identifier()), source_location); break; case FUNCTION_CALL: @@ -966,13 +966,9 @@ void goto_programt::instructiont::transform( case DEAD: { - auto new_symbol = f(get_dead().symbol()); + auto new_symbol = f(dead_symbol()); if(new_symbol.has_value()) - { - auto new_dead = get_dead(); - new_dead.symbol() = to_symbol_expr(*new_symbol); - set_dead(new_dead); - } + dead_symbol() = to_symbol_expr(*new_symbol); } break; @@ -1050,7 +1046,7 @@ void goto_programt::instructiont::apply( break; case DEAD: - f(get_dead().symbol()); + f(dead_symbol()); break; case FUNCTION_CALL: diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index b461b7f0c6f..93ca639f1ed 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -218,13 +219,29 @@ class goto_programt } /// Get the dead statement for DEAD + DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead")) const code_deadt &get_dead() const { PRECONDITION(is_dead()); return to_code_dead(code); } + /// Get the symbol for DEAD + const symbol_exprt &dead_symbol() const + { + PRECONDITION(is_dead()); + return to_code_dead(code).symbol(); + } + + /// Get the symbol for DEAD + symbol_exprt &dead_symbol() + { + PRECONDITION(is_dead()); + return to_code_dead(code).symbol(); + } + /// Set the dead statement for DEAD + DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead")) void set_dead(code_deadt c) { PRECONDITION(is_dead()); diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index f6897ebf33b..e18642bff6f 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -19,9 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com void goto_symext::symex_dead(statet &state) { const goto_programt::instructiont &instruction=*state.source.pc; - - const code_deadt &code = instruction.get_dead(); - symex_dead(state, code.symbol()); + symex_dead(state, instruction.dead_symbol()); } void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)