diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index e7e88fe0116..3219e74a88b 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -47,12 +47,6 @@ static void unreachable_instructions( it!=dominators.cfg.entry_map.end(); ++it) { - if(it->first->is_dead() || - (it->first->is_assign() && - to_code_assign(it->first->code).lhs().get(ID_identifier)== - "__CPROVER_dead_object")) - continue; - const cfg_dominatorst::cfgt::nodet &n=dominators.cfg[it->second]; if(n.dominators.empty()) dest.insert(std::make_pair(it->first->location_number, @@ -78,11 +72,7 @@ static void all_unreachable( dead_mapt &dest) { forall_goto_program_instructions(it, goto_program) - if(!it->is_end_function() && - !it->is_dead() && - !(it->is_assign() && - to_code_assign(it->code).lhs().get(ID_identifier)== - "__CPROVER_dead_object")) + if(!it->is_end_function()) dest.insert(std::make_pair(it->location_number, it)); } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index ea16e9c8547..4afea029858 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -419,8 +419,6 @@ void goto_convertt::convert( const codet &code, goto_programt &dest) { - std::size_t old_tmp_symbols_size=tmp_symbols.size(); - const irep_idt &statement=code.get_statement(); if(statement==ID_block) @@ -542,19 +540,6 @@ void goto_convertt::convert( else copy(code, OTHER, dest); - // We only need to kill the temporaries if control - // can get to the end of the block. - #if 0 - if(!dest.empty() && - dest.instructions.back().is_goto() && - dest.instructions.back().guard.is_true()) - tmp_symbols.resize(old_tmp_symbols_size); - else - kill_tmp_symbols(old_tmp_symbols_size, dest); - #else - kill_tmp_symbols(old_tmp_symbols_size, dest); - #endif - // make sure dest is never empty if(dest.instructions.empty()) { @@ -566,31 +551,6 @@ void goto_convertt::convert( /*******************************************************************\ -Function: goto_convertt::kill_tmp_symbols - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void goto_convertt::kill_tmp_symbols( - std::size_t final_size, - goto_programt &dest) -{ - while(tmp_symbols.size()>final_size) - { - symbol_exprt symbol=tmp_symbols.back(); - tmp_symbols.pop_back(); - dest.add_instruction(DEAD); - dest.instructions.back().code=code_deadt(symbol); - } -} - -/*******************************************************************\ - Function: goto_convertt::convert_block Inputs: @@ -617,7 +577,8 @@ void goto_convertt::convert_block( convert(b_code, dest); } - // see if we need to do any destructors + // see if we need to do any destructors -- may have been processed + // in a prior break/continue/return already, don't create dead code if(!dest.empty() && dest.instructions.back().is_goto() && dest.instructions.back().guard.is_true()) @@ -2564,11 +2525,10 @@ symbolt &goto_convertt::new_tmp_symbol( new_symbol.location=source_location; } while(symbol_table.move(new_symbol, symbol_ptr)); - tmp_symbols.push_back(symbol_ptr->symbol_expr()); - - goto_programt::targett t=dest.add_instruction(DECL); - t->code=code_declt(symbol_ptr->symbol_expr()); - t->source_location=source_location; + code_declt decl; + decl.symbol()=symbol_ptr->symbol_expr(); + decl.add_source_location()=source_location; + convert_decl(decl, dest); return *symbol_ptr; } diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index c14ef4f32be..fe9115530f8 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -63,9 +63,6 @@ class goto_convertt:public message_streamt symbol_exprt make_compound_literal( const exprt &expr, goto_programt &dest); - - typedef std::list tmp_symbolst; - tmp_symbolst tmp_symbols; // // translation of C expressions (with side effects) @@ -87,8 +84,6 @@ class goto_convertt:public message_streamt exprt &expr, const std::string &suffix, goto_programt &); - - void kill_tmp_symbols(std::size_t, goto_programt &); void rewrite_boolean(exprt &dest); diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 1a0909bdc82..0d6da6daa09 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -417,8 +417,6 @@ void goto_convertt::remove_function_call( new_name(new_symbol); - tmp_symbols.push_back(new_symbol.symbol_expr()); - { code_declt decl; decl.symbol()=new_symbol.symbol_expr(); @@ -488,7 +486,11 @@ void goto_convertt::remove_cpp_new( new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); new_name(new_symbol); - tmp_symbols.push_back(new_symbol.symbol_expr()); + + code_declt decl; + decl.symbol()=new_symbol.symbol_expr(); + decl.add_source_location()=new_symbol.location; + convert_decl(decl, dest); call=code_assignt(new_symbol.symbol_expr(), expr); @@ -560,7 +562,6 @@ void goto_convertt::remove_malloc( new_symbol.location=expr.source_location(); new_name(new_symbol); - tmp_symbols.push_back(new_symbol.symbol_expr()); code_declt decl; decl.symbol()=new_symbol.symbol_expr(); @@ -703,15 +704,9 @@ void goto_convertt::remove_statement_expression( id2string(last.get(ID_statement))+"'"; { - // this likely needs to be a proper stack - tmp_symbolst old_tmp_symbols; - old_tmp_symbols.swap(tmp_symbols); - goto_programt tmp; convert(code, tmp); dest.destructive_append(tmp); - - old_tmp_symbols.swap(tmp_symbols); } static_cast(expr)=tmp_symbol_expr;