From 22373c11359e5a3cc03b37d2a426abad26145d34 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Jan 2019 14:03:19 +0000 Subject: [PATCH 1/3] Remove validation of instructiont::function as it is going away This member is being removed, there is nothing to validate about it. --- src/goto-programs/goto_program.cpp | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index e86093907bd..acef5c04bcd 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -680,13 +680,6 @@ void goto_programt::instructiont::validate( validate_full_code(code, ns, vm); validate_full_expr(guard, ns, vm); - const symbolt *table_symbol; - DATA_CHECK_WITH_DIAGNOSTICS( - vm, - !ns.lookup(function, table_symbol), - id2string(function) + " not found", - source_location); - auto expr_symbol_finder = [&](const exprt &e) { find_symbols_sett typetags; find_type_symbols(e.type(), typetags); @@ -704,12 +697,13 @@ void goto_programt::instructiont::validate( auto ¤t_source_location = source_location; auto type_finder = - [&ns, vm, &table_symbol, ¤t_source_location](const exprt &e) { + [&ns, vm, ¤t_source_location](const exprt &e) { if(e.id() == ID_symbol) { const auto &goto_symbol_expr = to_symbol_expr(e); const auto &goto_id = goto_symbol_expr.get_identifier(); + const symbolt *table_symbol; if(!ns.lookup(goto_id, table_symbol)) { bool symbol_expr_type_matches_symbol_table = @@ -783,6 +777,7 @@ void goto_programt::instructiont::validate( } }; + const symbolt *table_symbol; switch(type) { case NO_INSTRUCTION_TYPE: From c9c872e2675f81f62dfb81b0d1f25193142c2b27 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 9 Oct 2018 08:51:17 +0100 Subject: [PATCH 2/3] remove goto_programt::instructiont::function member --- jbmc/src/java_bytecode/remove_exceptions.cpp | 6 -- jbmc/src/jbmc/jbmc_parse_options.cpp | 3 - jbmc/src/jdiff/java_syntactic_diff.cpp | 15 --- src/analyses/flow_insensitive_analysis.cpp | 6 -- src/analyses/goto_check.cpp | 3 - src/analyses/interval_analysis.cpp | 1 - src/assembler/remove_asm.cpp | 3 - src/goto-diff/syntactic_diff.cpp | 15 --- src/goto-diff/unified_diff.cpp | 2 +- src/goto-instrument/branch.cpp | 2 - src/goto-instrument/code_contracts.cpp | 13 --- src/goto-instrument/cover_instrument.h | 1 - src/goto-instrument/cover_instrument_mcdc.cpp | 3 - .../cover_instrument_other.cpp | 1 - src/goto-instrument/function.cpp | 3 - .../generate_function_bodies.cpp | 4 - src/goto-instrument/interrupt.cpp | 4 - src/goto-instrument/loop_utils.cpp | 1 - src/goto-instrument/model_argc_argv.cpp | 3 - src/goto-instrument/nondet_static.cpp | 1 - src/goto-instrument/skip_loops.cpp | 1 - src/goto-instrument/stack_depth.cpp | 4 - .../thread_instrumentation.cpp | 2 - src/goto-instrument/unwind.cpp | 5 - src/goto-instrument/wmm/weak_memory.cpp | 1 - src/goto-programs/goto_convert_functions.cpp | 3 - src/goto-programs/goto_function.h | 8 -- src/goto-programs/goto_functions.h | 11 --- src/goto-programs/goto_inline_class.cpp | 11 +-- src/goto-programs/goto_inline_class.h | 1 - src/goto-programs/goto_model.h | 7 -- src/goto-programs/goto_program.h | 91 ++----------------- .../instrument_preconditions.cpp | 2 - src/goto-programs/link_goto_model.cpp | 3 - src/goto-programs/mm_io.cpp | 4 - src/goto-programs/parameter_assignments.cpp | 1 - src/goto-programs/read_bin_goto_object.cpp | 2 +- src/goto-programs/remove_calls_no_body.cpp | 2 - .../remove_function_pointers.cpp | 1 - src/goto-programs/remove_returns.cpp | 2 - .../remove_virtual_functions.cpp | 1 - src/goto-programs/string_abstraction.cpp | 15 --- src/goto-programs/write_goto_binary.cpp | 2 +- unit/goto-programs/goto_program_assume.cpp | 1 - unit/goto-programs/goto_program_dead.cpp | 1 - .../goto_program_declaration.cpp | 1 - .../goto_program_function_call.cpp | 1 - .../goto_program_goto_target.cpp | 2 - ..._program_symbol_type_table_consistency.cpp | 1 - .../goto_program_table_consistency.cpp | 1 - 50 files changed, 14 insertions(+), 264 deletions(-) diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index fe398d686b8..654b02dd988 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -237,7 +237,6 @@ void remove_exceptionst::instrument_exception_handler( t_null->code=code_assignt( thrown_global_symbol, null_voidptr); - t_null->function=instr_it->function; // add the assignment exc = @inflight_exception (before the null assignment) goto_programt::targett t_exc=goto_program.insert_after(instr_it); @@ -246,7 +245,6 @@ void remove_exceptionst::instrument_exception_handler( t_exc->code=code_assignt( thrown_exception_local, typecast_exprt(thrown_global_symbol, thrown_exception_local.type())); - t_exc->function=instr_it->function; } instr_it->make_skip(); } @@ -352,7 +350,6 @@ void remove_exceptionst::add_exception_dispatch_sequence( goto_programt::targett t_exc=goto_program.insert_after(instr_it); t_exc->make_goto(new_state_pc); t_exc->source_location=instr_it->source_location; - t_exc->function=instr_it->function; // use instanceof to check that this is the correct handler struct_tag_typet type(stack_catch[i][j].first); @@ -377,7 +374,6 @@ void remove_exceptionst::add_exception_dispatch_sequence( default_dispatch->make_goto(default_target); default_dispatch->source_location=instr_it->source_location; - default_dispatch->function=instr_it->function; // add dead instructions for(const auto &local : locals) @@ -386,7 +382,6 @@ void remove_exceptionst::add_exception_dispatch_sequence( t_dead->make_dead(); t_dead->code=code_deadt(local); t_dead->source_location=instr_it->source_location; - t_dead->function=instr_it->function; } } @@ -466,7 +461,6 @@ bool remove_exceptionst::instrument_function_call( goto_programt::targett t_null=goto_program.insert_after(instr_it); t_null->make_goto(next_it); t_null->source_location=instr_it->source_location; - t_null->function=instr_it->function; t_null->guard=no_exception_currently_in_flight; } diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 28c0ab81a9c..484cb8b3a22 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -840,9 +840,6 @@ void jbmc_parse_optionst::process_goto_function( function.compute_location_numbers(); goto_function.body.compute_loop_numbers(); } - - // update the function member in each instruction - function.update_instructions_function(); } } diff --git a/jbmc/src/jdiff/java_syntactic_diff.cpp b/jbmc/src/jdiff/java_syntactic_diff.cpp index f040e983fa4..b99707a1f4c 100644 --- a/jbmc/src/jdiff/java_syntactic_diff.cpp +++ b/jbmc/src/jdiff/java_syntactic_diff.cpp @@ -75,21 +75,6 @@ bool java_syntactic_difft::operator()() modified_functions.insert(it->first); continue; } - - goto_programt::instructionst::const_iterator i_it1 = - it->second.body.instructions.begin(); - for(goto_programt::instructionst::const_iterator - i_it2 = f_it->second.body.instructions.begin(); - i_it1 != it->second.body.instructions.end() && - i_it2 != f_it->second.body.instructions.end(); - ++i_it1, ++i_it2) - { - if(i_it1->function != i_it2->function) - { - modified_functions.insert(it->first); - break; - } - } } forall_goto_functions(it, goto_model2.goto_functions) { diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp index a628d26f75a..07898d65928 100644 --- a/src/analyses/flow_insensitive_analysis.cpp +++ b/src/analyses/flow_insensitive_analysis.cpp @@ -212,12 +212,9 @@ bool flow_insensitive_analysis_baset::do_function_call( goto_programt::targett r = temp.add(goto_programt::make_return(code_returnt( side_effect_expr_nondett(code.lhs().type(), l_call->source_location)))); - - r->function=f_it->first; r->location_number=0; goto_programt::targett t = temp.add(goto_programt::make_end_function()); - t->function=f_it->first; t->location_number=1; locationt l_next=l_call; l_next++; @@ -242,9 +239,6 @@ bool flow_insensitive_analysis_baset::do_function_call( // get the state at the beginning of the function locationt l_begin=goto_function.body.instructions.begin(); - DATA_INVARIANT( - l_begin->function == f_it->first, "function names have to match"); - // do the edge from the call site to the beginning of the function new_data = state.transform(ns, calling_function, l_call, f_it->first, l_begin); diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 952dd414e67..c055e6698a6 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1900,9 +1900,6 @@ void goto_checkt::goto_check( i_it->source_location.set_java_bytecode_index( it->source_location.get_java_bytecode_index()); } - - if(i_it->function.empty()) - i_it->function=it->function; } // insert new instructions -- make sure targets are not moved diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp index f748eb2b20d..5bfa08a36ed 100644 --- a/src/analyses/interval_analysis.cpp +++ b/src/analyses/interval_analysis.cpp @@ -82,7 +82,6 @@ void instrument_intervals( t->make_assumption(conjunction(assertion)); i_it++; // goes to original instruction t->source_location=i_it->source_location; - t->function=i_it->function; } } } diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp index 3e618544626..22c6a6f604d 100644 --- a/src/assembler/remove_asm.cpp +++ b/src/assembler/remove_asm.cpp @@ -493,9 +493,6 @@ void remove_asmt::process_function( it->make_skip(); did_something = true; - for(auto &instruction : tmp_dest.instructions) - instruction.function = it->function; - goto_programt::targett next = it; next++; diff --git a/src/goto-diff/syntactic_diff.cpp b/src/goto-diff/syntactic_diff.cpp index c572ca7934d..cf86872c4c6 100644 --- a/src/goto-diff/syntactic_diff.cpp +++ b/src/goto-diff/syntactic_diff.cpp @@ -74,21 +74,6 @@ bool syntactic_difft::operator()() modified_functions.insert(it->first); continue; } - - goto_programt::instructionst::const_iterator - i_it1=it->second.body.instructions.begin(); - for(goto_programt::instructionst::const_iterator - i_it2=f_it->second.body.instructions.begin(); - i_it1!=it->second.body.instructions.end() && - i_it2!=f_it->second.body.instructions.end(); - ++i_it1, ++i_it2) - { - if(i_it1->function != i_it2->function) - { - modified_functions.insert(it->first); - break; - } - } } forall_goto_functions(it, goto_model2.goto_functions) { diff --git a/src/goto-diff/unified_diff.cpp b/src/goto-diff/unified_diff.cpp index ce74bcae5df..b08ccba2d51 100644 --- a/src/goto-diff/unified_diff.cpp +++ b/src/goto-diff/unified_diff.cpp @@ -392,7 +392,7 @@ bool unified_difft::instructions_equal( const goto_programt::instructiont &ins1, const goto_programt::instructiont &ins2) { - return ins1.equals(ins2) && ins1.function == ins2.function && + return ins1.equals(ins2) && (ins1.targets.empty() || instructions_equal(*ins1.get_target(), *ins2.get_target())); } diff --git a/src/goto-instrument/branch.cpp b/src/goto-instrument/branch.cpp index 378a64d0b4e..03d6ab1d57c 100644 --- a/src/goto-instrument/branch.cpp +++ b/src/goto-instrument/branch.cpp @@ -54,7 +54,6 @@ void branch( goto_programt::targett t1=body.insert_after(i_it); t1->make_function_call( function_to_call(goto_model.symbol_table, id, "taken")); - t1->function=f_it->first; goto_programt::targett t2=body.insert_after(t1); t2->make_goto(i_it->get_target()); @@ -62,7 +61,6 @@ void branch( goto_programt::targett t3=body.insert_after(t2); t3->make_function_call( function_to_call(goto_model.symbol_table, id, "not-taken")); - t3->function=f_it->first; i_it->targets.clear(); i_it->targets.push_back(t3); } diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 98408f6accd..47caa7848a8 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -112,7 +112,6 @@ static void check_apply_invariants( { goto_programt::targett a=havoc_code.add_instruction(ASSERT); a->guard=invariant; - a->function=loop_head->function; a->source_location=loop_head->source_location; a->source_location.set_comment("Loop invariant violated before entry"); } @@ -124,7 +123,6 @@ static void check_apply_invariants( { goto_programt::targett assume=havoc_code.add_instruction(ASSUME); assume->guard=invariant; - assume->function=loop_head->function; assume->source_location=loop_head->source_location; } @@ -135,7 +133,6 @@ static void check_apply_invariants( jump->guard = side_effect_expr_nondett(bool_typet(), loop_head->source_location); jump->targets.push_back(loop_end); - jump->function=loop_head->function; } // Now havoc at the loop head. Use insert_swap to @@ -146,7 +143,6 @@ static void check_apply_invariants( { goto_programt::instructiont a(ASSERT); a.guard=invariant; - a.function=loop_end->function; a.source_location=loop_end->source_location; a.source_location.set_comment("Loop invariant not preserved"); goto_function.body.insert_before_swap(loop_end, a); @@ -216,7 +212,6 @@ void code_contractst::apply_contract( { goto_programt::instructiont a(ASSERT); a.guard=requires; - a.function=target->function; a.source_location=target->source_location; goto_program.insert_before_swap(target, a); @@ -295,7 +290,6 @@ void code_contractst::add_contract_check( // build skip so that if(nondet) can refer to it goto_programt tmp_skip; goto_programt::targett skip=tmp_skip.add_instruction(SKIP); - skip->function=dest.instructions.front().function; skip->source_location=ensures.source_location(); goto_programt check; @@ -304,7 +298,6 @@ void code_contractst::add_contract_check( goto_programt::targett g=check.add_instruction(); g->make_goto( skip, side_effect_expr_nondett(bool_typet(), skip->source_location)); - g->function=skip->function; g->source_location=skip->source_location; // prepare function call including all declarations @@ -315,7 +308,6 @@ void code_contractst::add_contract_check( if(gf.type.return_type()!=empty_typet()) { goto_programt::targett d=check.add_instruction(DECL); - d->function=skip->function; d->source_location=skip->source_location; symbol_exprt r= @@ -336,7 +328,6 @@ void code_contractst::add_contract_check( ++p_it) { goto_programt::targett d=check.add_instruction(DECL); - d->function=skip->function; d->source_location=skip->source_location; symbol_exprt p= @@ -358,7 +349,6 @@ void code_contractst::add_contract_check( { goto_programt::targett a=check.add_instruction(); a->make_assumption(requires); - a->function=skip->function; a->source_location=requires.source_location(); // rewrite any use of parameters @@ -368,13 +358,11 @@ void code_contractst::add_contract_check( // ret=function(parameter1, ...) goto_programt::targett f=check.add_instruction(); f->make_function_call(call); - f->function=skip->function; f->source_location=skip->source_location; // assert(ensures) goto_programt::targett a=check.add_instruction(); a->make_assertion(ensures); - a->function=skip->function; a->source_location=ensures.source_location(); // rewrite any use of __CPROVER_return_value @@ -383,7 +371,6 @@ void code_contractst::add_contract_check( // assume(false) goto_programt::targett af=check.add_instruction(); af->make_assumption(false_exprt()); - af->function=skip->function; af->source_location=ensures.source_location(); // prepend the new code to dest diff --git a/src/goto-instrument/cover_instrument.h b/src/goto-instrument/cover_instrument.h index c29cf5bbab3..1b92818a19c 100644 --- a/src/goto-instrument/cover_instrument.h +++ b/src/goto-instrument/cover_instrument.h @@ -74,7 +74,6 @@ class cover_instrumenter_baset t->source_location.set(ID_coverage_criterion, coverage_criterion); t->source_location.set_property_class(property_class); t->source_location.set_function(function_id); - t->function = function_id; } bool is_non_cover_assertion(goto_programt::const_targett t) const diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp index 1513c7cd734..225b5786a56 100644 --- a/src/goto-instrument/cover_instrument_mcdc.cpp +++ b/src/goto-instrument/cover_instrument_mcdc.cpp @@ -667,7 +667,6 @@ void cover_mcdc_instrumentert::instrument( i_it->source_location.set(ID_coverage_criterion, coverage_criterion); i_it->source_location.set_property_class(property_class); i_it->source_location.set_function(function_id); - i_it->function = function_id; std::string comment_f = description + " `" + p_string + "' false"; goto_program.insert_before_swap(i_it); @@ -677,7 +676,6 @@ void cover_mcdc_instrumentert::instrument( i_it->source_location.set(ID_coverage_criterion, coverage_criterion); i_it->source_location.set_property_class(property_class); i_it->source_location.set_function(function_id); - i_it->function = function_id; } std::set controlling; @@ -704,7 +702,6 @@ void cover_mcdc_instrumentert::instrument( i_it->source_location.set(ID_coverage_criterion, coverage_criterion); i_it->source_location.set_property_class(property_class); i_it->source_location.set_function(function_id); - i_it->function = function_id; } for(std::size_t i = 0; i < both.size() * 2 + controlling.size(); i++) diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-instrument/cover_instrument_other.cpp index 4a139f71b87..7e71feafe49 100644 --- a/src/goto-instrument/cover_instrument_other.cpp +++ b/src/goto-instrument/cover_instrument_other.cpp @@ -86,5 +86,4 @@ void cover_instrument_end_of_function( if_it->source_location.set_comment(comment); if_it->source_location.set_property_class("reachability_constraint"); if_it->source_location.set_function(function_id); - if_it->function = function_id; } diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp index c5066c5e0d9..23f810e7218 100644 --- a/src/goto-instrument/function.cpp +++ b/src/goto-instrument/function.cpp @@ -91,7 +91,6 @@ void function_enter( body.insert_before(body.instructions.begin()); t->make_function_call( function_to_call(goto_model.symbol_table, id, f_it->first)); - t->function=f_it->first; } } @@ -123,7 +122,6 @@ void function_exit( if(i_it->is_return()) { goto_programt::instructiont call; - call.function=f_it->first; call.make_function_call( function_to_call(goto_model.symbol_table, id, f_it->first)); body.insert_before_swap(i_it, call); @@ -154,7 +152,6 @@ void function_exit( goto_programt::instructiont call; call.make_function_call( function_to_call(goto_model.symbol_table, id, f_it->first)); - call.function=f_it->first; body.insert_before_swap(last, call); } } diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index b7ce2a17019..244f77decc5 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -76,7 +76,6 @@ class assume_false_generate_function_bodiest : public generate_function_bodiest // NOLINTNEXTLINE auto add_instruction = [&]() { auto instruction = function.body.add_instruction(); - instruction->function = function_name; instruction->source_location = function_symbol.location; return instruction; }; @@ -99,7 +98,6 @@ class assert_false_generate_function_bodiest : public generate_function_bodiest // NOLINTNEXTLINE auto add_instruction = [&]() { auto instruction = function.body.add_instruction(); - instruction->function = function_name; instruction->source_location = function_symbol.location; instruction->source_location.set_function(function_name); return instruction; @@ -130,7 +128,6 @@ class assert_false_then_assume_false_generate_function_bodiest // NOLINTNEXTLINE auto add_instruction = [&]() { auto instruction = function.body.add_instruction(); - instruction->function = function_name; instruction->source_location = function_symbol.location; instruction->source_location.set_function(function_name); return instruction; @@ -212,7 +209,6 @@ class havoc_generate_function_bodiest : public generate_function_bodiest // NOLINTNEXTLINE auto add_instruction = [&]() { auto instruction = function.body.add_instruction(); - instruction->function = function_name; instruction->source_location = function_symbol.location; return instruction; }; diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp index a6b0bc48f5f..dea3f205ed8 100644 --- a/src/goto-instrument/interrupt.cpp +++ b/src/goto-instrument/interrupt.cpp @@ -110,11 +110,9 @@ static void interrupt( t_goto->make_goto(t_orig); t_goto->source_location=source_location; t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location); - t_goto->function=original_instruction.function; t_call->make_function_call(isr_call); t_call->source_location=source_location; - t_call->function=original_instruction.function; t_orig->swap(original_instruction); @@ -138,11 +136,9 @@ static void interrupt( t_goto->make_goto(t_orig); t_goto->source_location=source_location; t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location); - t_goto->function=i_it->function; t_call->make_function_call(isr_call); t_call->source_location=source_location; - t_call->function=i_it->function; i_it=t_call; // the for loop already counts us up } diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp index ee0f34ca10e..efb14b4aaf8 100644 --- a/src/goto-instrument/loop_utils.cpp +++ b/src/goto-instrument/loop_utils.cpp @@ -50,7 +50,6 @@ void build_havoc_code( goto_programt::targett t = dest.add(goto_programt::make_assignment( code_assignt(std::move(lhs), std::move(rhs)), loop_head->source_location)); - t->function=loop_head->function; t->code.add_source_location()=loop_head->source_location; } } diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp index d91743cfa6c..49f8662a7dc 100644 --- a/src/goto-instrument/model_argc_argv.cpp +++ b/src/goto-instrument/model_argc_argv.cpp @@ -152,10 +152,7 @@ bool model_argc_argv( main_symbol.mode); Forall_goto_program_instructions(it, init_instructions) - { it->source_location.set_file(""); - it->function=goto_model.goto_functions.entry_point(); - } goto_functionst::function_mapt::iterator start_entry= goto_model.goto_functions.function_map.find( diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp index e42ac41903c..922f48b7977 100644 --- a/src/goto-instrument/nondet_static.cpp +++ b/src/goto-instrument/nondet_static.cpp @@ -97,7 +97,6 @@ void nondet_static( side_effect_expr_nondett( sym.type(), original_instruction.source_location)); i_it->source_location = original_instruction.source_location; - i_it->function = original_instruction.function; } } else if(instruction.is_function_call()) diff --git a/src/goto-instrument/skip_loops.cpp b/src/goto-instrument/skip_loops.cpp index c28f2f80fe9..8c48da5a301 100644 --- a/src/goto-instrument/skip_loops.cpp +++ b/src/goto-instrument/skip_loops.cpp @@ -48,7 +48,6 @@ static bool skip_loops( goto_programt::targett g=goto_program.insert_before(loop_head); g->make_goto(next, true_exprt()); g->source_location=loop_head->source_location; - g->function=loop_head->function; ++l_it; } diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 7783ceda830..8fd929c3939 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -54,7 +54,6 @@ void stack_depth( goto_programt::targett assert_ins=goto_program.insert_before(first); assert_ins->make_assertion(guard); assert_ins->source_location=first->source_location; - assert_ins->function=first->function; assert_ins->source_location.set_comment( "Stack depth exceeds "+std::to_string(i_depth)); @@ -65,7 +64,6 @@ void stack_depth( plus_ins->code=code_assignt(symbol, plus_exprt(symbol, from_integer(1, symbol.type()))); plus_ins->source_location=first->source_location; - plus_ins->function=first->function; goto_programt::targett last=--goto_program.instructions.end(); assert(last->is_end_function()); @@ -75,7 +73,6 @@ void stack_depth( minus_ins.code=code_assignt(symbol, minus_exprt(symbol, from_integer(1, symbol.type()))); minus_ins.source_location=last->source_location; - minus_ins.function=last->function; goto_program.insert_before_swap(last, minus_ins); } @@ -108,7 +105,6 @@ void stack_depth( it->make_assignment(); it->code=code_assignt(sym, from_integer(0, sym.type())); // no suitable value for source location -- omitted - it->function = INITIALIZE_FUNCTION; // update counters etc. goto_model.goto_functions.update(); diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp index 50a4bee2a81..e75765e7f25 100644 --- a/src/goto-instrument/thread_instrumentation.cpp +++ b/src/goto-instrument/thread_instrumentation.cpp @@ -35,7 +35,6 @@ void thread_exit_instrumentation(goto_programt &goto_program) assert(end->is_end_function()); source_locationt source_location=end->source_location; - irep_idt function=end->function; goto_program.insert_before_swap(end); @@ -51,7 +50,6 @@ void thread_exit_instrumentation(goto_programt &goto_program) end->source_location=source_location; end->source_location.set_comment("mutexes must not be locked on thread exit"); - end->function=function; } void thread_exit_instrumentation(goto_modelt &goto_model) diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index a14803a9431..88aba2f444e 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -120,7 +120,6 @@ void goto_unwindt::unwind( t->make_skip(); t->source_location=loop_head->source_location; - t->function=loop_head->function; t->location_number=loop_head->location_number; } else if(unwind_strategy==unwind_strategyt::CONTINUE) @@ -155,7 +154,6 @@ void goto_unwindt::unwind( UNREACHABLE; new_t->source_location=loop_head->source_location; - new_t->function=loop_head->function; new_t->location_number=loop_head->location_number; unwind_log.insert(new_t, loop_head->location_number); } @@ -181,7 +179,6 @@ void goto_unwindt::unwind( t_goto->make_goto(goto_program.const_cast_target(loop_exit)); t_goto->source_location=loop_exit->source_location; - t_goto->function=loop_exit->function; t_goto->guard=true_exprt(); t_goto->location_number=loop_exit->location_number; } @@ -193,7 +190,6 @@ void goto_unwindt::unwind( t_skip->make_skip(); t_skip->source_location=loop_head->source_location; - t_skip->function=loop_head->function; t_skip->location_number=loop_head->location_number; // where to go for the next iteration @@ -236,7 +232,6 @@ void goto_unwindt::unwind( t_skip->make_skip(); t_skip->source_location=loop_head->source_location; - t_skip->function=loop_head->function; t_skip->location_number=loop_head->location_number; // redirect gotos into loop body diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp index f3f3b24fff1..8f29c9bca29 100644 --- a/src/goto-instrument/wmm/weak_memory.cpp +++ b/src/goto-instrument/wmm/weak_memory.cpp @@ -91,7 +91,6 @@ void introduce_temporaries( new_i.make_assignment(); new_i.code=code_assignt(symbol_expr, instruction.guard); new_i.source_location=instruction.source_location; - new_i.function=instruction.function; // replace guard instruction.guard=symbol_expr; diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 0eb23ed2692..9ce3938a759 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -204,9 +204,6 @@ void goto_convert_functionst::convert_function( // add "end of function" f.body.destructive_append(tmp_end_function); - // do function tags (they are empty at this point) - f.update_instructions_function(identifier); - f.body.update(); if(hide(f.body)) diff --git a/src/goto-programs/goto_function.h b/src/goto-programs/goto_function.h index c3634675a58..22ac0e92c7b 100644 --- a/src/goto-programs/goto_function.h +++ b/src/goto-programs/goto_function.h @@ -72,14 +72,6 @@ class goto_functiont parameter_identifiers.clear(); } - /// update the function member in each instruction - /// \param function_id: the `function_id` used for assigning empty function - /// members - void update_instructions_function(const irep_idt &function_id) - { - body.update_instructions_function(function_id); - } - void swap(goto_functiont &other) { body.swap(other.body); diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index f03933466ea..7f3663456f8 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -78,23 +78,12 @@ class goto_functionst void compute_target_numbers(); void compute_incoming_edges(); - /// update the function member in each instruction by setting it to - /// the goto function's identifier - void update_instructions_function() - { - for(auto &func : function_map) - { - func.second.update_instructions_function(func.first); - } - } - void update() { compute_incoming_edges(); compute_target_numbers(); compute_location_numbers(); compute_loop_numbers(); - update_instructions_function(); } /// Get the identifier of the entry point to a goto model diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index f715e5127c7..7021f971dc0 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -64,7 +64,6 @@ void goto_inlinet::parameter_assignments( goto_programt::targett decl = dest.add( goto_programt::make_decl(symbol.symbol_expr(), source_location)); decl->code.add_source_location()=source_location; - decl->function=adjust_function?target->function:function_name; } // this is the actual parameter @@ -127,8 +126,6 @@ void goto_inlinet::parameter_assignments( dest.add_instruction(ASSIGN); dest.instructions.back().source_location=source_location; dest.instructions.back().code.swap(assignment); - dest.instructions.back().function= - adjust_function?target->function:function_name; } if(it1!=arguments.end()) @@ -143,7 +140,6 @@ void goto_inlinet::parameter_assignments( void goto_inlinet::parameter_destruction( const goto_programt::targett target, - const irep_idt &function_name, // name of called function const code_typet &code_type, // type of called function goto_programt &dest) { @@ -170,7 +166,6 @@ void goto_inlinet::parameter_destruction( goto_programt::targett dead = dest.add( goto_programt::make_dead(symbol.symbol_expr(), source_location)); dead->code.add_source_location()=source_location; - dead->function=adjust_function?target->function:function_name; } } } @@ -277,10 +272,6 @@ void goto_inlinet::insert_function_body( "final instruction of a function must be an END_FUNCTION"); end.type=LOCATION; - if(adjust_function) - for(auto &instruction : body.instructions) - instruction.function=target->function; - // make sure the inlined function does not introduce hiding if(goto_function.is_hidden()) { @@ -299,7 +290,7 @@ void goto_inlinet::insert_function_body( tmp1); goto_programt tmp2; - parameter_destruction(target, identifier, goto_function.type, tmp2); + parameter_destruction(target, goto_function.type, tmp2); goto_programt tmp; tmp.destructive_append(tmp1); // par assignment diff --git a/src/goto-programs/goto_inline_class.h b/src/goto-programs/goto_inline_class.h index 6adaa313329..5ab42271d6b 100644 --- a/src/goto-programs/goto_inline_class.h +++ b/src/goto-programs/goto_inline_class.h @@ -184,7 +184,6 @@ class goto_inlinet:public messaget void parameter_destruction( const goto_programt::targett target, - const irep_idt &function_name, const code_typet &code_type, goto_programt &dest); diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index 3dd6e434679..a640dc5885f 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -194,13 +194,6 @@ class goto_model_functiont goto_functions.compute_location_numbers(goto_function.body); } - /// Updates the empty function member of each instruction by setting them - /// to `function_id` - void update_instructions_function() - { - goto_function.update_instructions_function(function_id); - } - /// Get symbol table /// \return journalling symbol table that (a) wraps the global symbol table, /// and (b) has recorded all symbol mutations (insertions, updates and diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 6b2f8c60f6f..2733b39ad8d 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -264,9 +264,6 @@ class goto_programt return code; } - /// The function this instruction belongs to - irep_idt function; - /// The location of the instruction in the source file source_locationt source_location; @@ -436,13 +433,11 @@ class goto_programt /// Constructor that can set all members, passed by value instructiont( codet _code, - irep_idt _function, source_locationt _source_location, goto_program_instruction_typet _type, exprt _guard, targetst _targets) : code(std::move(_code)), - function(_function), source_location(std::move(_source_location)), type(_type), guard(std::move(_guard)), @@ -459,7 +454,6 @@ class goto_programt swap(instruction.type, type); swap(instruction.guard, guard); swap(instruction.targets, targets); - swap(instruction.function, function); } /// Uniquely identify an invalid target or location @@ -535,42 +529,6 @@ class goto_programt return t; } - /// Get the id of the function that contains the instruction pointed-to by the - /// given instruction iterator. - /// - /// \param l: instruction iterator - /// \return id of the function that contains the pointed-to goto instruction - static const irep_idt get_function_id( - const_targett l) - { - // The field `function` of an instruction may not always contain the id of - // the function it is currently in, due to goto program modifications such - // as inlining. For example, if an instruction in a function `f` is inlined - // into a function `g`, the instruction may, depending on the arguments to - // the inliner, retain the original value of `f` in the function field. - // However, instructions of type END_FUNCTION are never inlined into other - // functions, hence they contain the id of the function they are in. Thus, - // this function takes the END_FUNCTION instruction of the goto program and - // returns the value of its function field. - - while(!l->is_end_function()) - ++l; - - return l->function; - } - - /// Get the id of the function that contains the given goto program. - /// - /// \param p: the goto program - /// \return id of the function that contains the goto program - static const irep_idt get_function_id( - const goto_programt &p) - { - PRECONDITION(!p.empty()); - - return get_function_id(--p.instructions.end()); - } - template std::list get_successors(Target target) const; @@ -695,22 +653,6 @@ class goto_programt } } - /// Sets the `function` member of each instruction if not yet set - /// Note that a goto program need not be a goto function and therefore, - /// we cannot do this in update(), but only at the level of - /// of goto_functionst where goto programs are guaranteed to be - /// named functions. - void update_instructions_function(const irep_idt &function_id) - { - for(auto &instruction : instructions) - { - if(instruction.function.empty()) - { - instruction.function = function_id; - } - } - } - /// Compute location numbers void compute_location_numbers() { @@ -811,14 +753,14 @@ class goto_programt static instructiont make_return(const source_locationt &l = source_locationt::nil()) { - return instructiont(code_returnt(), irep_idt(), l, RETURN, nil_exprt(), {}); + return instructiont(code_returnt(), l, RETURN, nil_exprt(), {}); } static instructiont make_return( code_returnt c, const source_locationt &l = source_locationt::nil()) { - return instructiont(std::move(c), irep_idt(), l, RETURN, nil_exprt(), {}); + return instructiont(std::move(c), l, RETURN, nil_exprt(), {}); } static instructiont @@ -826,7 +768,6 @@ class goto_programt { return instructiont( static_cast(get_nil_irep()), - irep_idt(), l, SKIP, nil_exprt(), @@ -837,7 +778,6 @@ class goto_programt { return instructiont( static_cast(get_nil_irep()), - irep_idt(), l, LOCATION, nil_exprt(), @@ -849,7 +789,6 @@ class goto_programt { return instructiont( static_cast(get_nil_irep()), - irep_idt(), l, THROW, nil_exprt(), @@ -861,7 +800,6 @@ class goto_programt { return instructiont( static_cast(get_nil_irep()), - irep_idt(), l, CATCH, nil_exprt(), @@ -874,7 +812,6 @@ class goto_programt { return instructiont( static_cast(get_nil_irep()), - irep_idt(), l, ASSERT, exprt(g), @@ -886,29 +823,26 @@ class goto_programt const source_locationt &l = source_locationt::nil()) { return instructiont( - static_cast(get_nil_irep()), irep_idt(), l, ASSUME, g, {}); + static_cast(get_nil_irep()), l, ASSUME, g, {}); } static instructiont make_other(const codet &_code) { - return instructiont( - _code, irep_idt(), source_locationt::nil(), OTHER, nil_exprt(), {}); + return instructiont(_code, source_locationt::nil(), OTHER, nil_exprt(), {}); } static instructiont make_decl( const symbol_exprt &symbol, const source_locationt &l = source_locationt::nil()) { - return instructiont( - code_declt(symbol), irep_idt(), l, DECL, nil_exprt(), {}); + return instructiont(code_declt(symbol), l, DECL, nil_exprt(), {}); } static instructiont make_dead( const symbol_exprt &symbol, const source_locationt &l = source_locationt::nil()) { - return instructiont( - code_deadt(symbol), irep_idt(), l, DEAD, nil_exprt(), {}); + return instructiont(code_deadt(symbol), l, DEAD, nil_exprt(), {}); } static instructiont @@ -916,7 +850,6 @@ class goto_programt { return instructiont( static_cast(get_nil_irep()), - irep_idt(), l, ATOMIC_BEGIN, nil_exprt(), @@ -928,7 +861,6 @@ class goto_programt { return instructiont( static_cast(get_nil_irep()), - irep_idt(), l, ATOMIC_END, nil_exprt(), @@ -940,7 +872,6 @@ class goto_programt { return instructiont( static_cast(get_nil_irep()), - irep_idt(), l, END_FUNCTION, nil_exprt(), @@ -951,7 +882,7 @@ class goto_programt const code_gotot &_code, const source_locationt &l = source_locationt::nil()) { - return instructiont(_code, irep_idt(), l, INCOMPLETE_GOTO, nil_exprt(), {}); + return instructiont(_code, l, INCOMPLETE_GOTO, nil_exprt(), {}); } static instructiont make_goto( @@ -960,7 +891,6 @@ class goto_programt { return instructiont( static_cast(get_nil_irep()), - irep_idt(), l, GOTO, true_exprt(), @@ -974,7 +904,6 @@ class goto_programt { return instructiont( static_cast(get_nil_irep()), - irep_idt(), l, GOTO, g, @@ -985,21 +914,21 @@ class goto_programt const code_assignt &_code, const source_locationt &l = source_locationt::nil()) { - return instructiont(_code, irep_idt(), l, ASSIGN, nil_exprt(), {}); + return instructiont(_code, l, ASSIGN, nil_exprt(), {}); } static instructiont make_decl( const code_declt &_code, const source_locationt &l = source_locationt::nil()) { - return instructiont(_code, irep_idt(), l, DECL, nil_exprt(), {}); + return instructiont(_code, l, DECL, nil_exprt(), {}); } static instructiont make_function_call( const code_function_callt &_code, const source_locationt &l = source_locationt::nil()) { - return instructiont(_code, irep_idt(), l, FUNCTION_CALL, nil_exprt(), {}); + return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {}); } }; diff --git a/src/goto-programs/instrument_preconditions.cpp b/src/goto-programs/instrument_preconditions.cpp index 47ea3ff2972..9bfffe8c315 100644 --- a/src/goto-programs/instrument_preconditions.cpp +++ b/src/goto-programs/instrument_preconditions.cpp @@ -110,7 +110,6 @@ void instrument_preconditions( goto_model.goto_functions); source_locationt source_location=it->source_location; - irep_idt function=it->function; replace_symbolt r=actuals_replace_map(call, ns); @@ -121,7 +120,6 @@ void instrument_preconditions( exprt instance=p->guard; r(instance); it->make_assertion(instance); - it->function=function; it->source_location=source_location; it->source_location.set_property_class(ID_precondition_instance); it->source_location.set_comment(p->source_location.get_comment()); diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index dd77454fe84..d2c069b540c 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -34,9 +34,6 @@ static void rename_symbols_in_function( { rename_symbol(iit->code); rename_symbol(iit->guard); - // we need to update the instruction's function field as - // well, with the new symbol for the function - iit->function=new_function_name; } } diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 8ed131144ad..febbd53c864 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -54,7 +54,6 @@ void mm_io( { const dereference_exprt &d=*deref_expr_r.begin(); source_locationt source_location=it->source_location; - irep_idt function=it->function; const code_typet &ct=to_code_type(mm_io_r.type()); irep_idt identifier=to_symbol_expr(mm_io_r).get_identifier(); @@ -72,7 +71,6 @@ void mm_io( goto_function.body.insert_before_swap(it); it->make_function_call(fc); it->source_location=source_location; - it->function=function; it++; } } @@ -83,7 +81,6 @@ void mm_io( { const dereference_exprt &d=to_dereference_expr(a.lhs()); source_locationt source_location=it->source_location; - irep_idt function=it->function; const code_typet &ct=to_code_type(mm_io_w.type()); const typet &pt=ct.parameters()[0].type(); const typet &st=ct.parameters()[1].type(); @@ -97,7 +94,6 @@ void mm_io( goto_function.body.insert_before_swap(it); it->make_function_call(fc); it->source_location=source_location; - it->function=function; it++; } } diff --git a/src/goto-programs/parameter_assignments.cpp b/src/goto-programs/parameter_assignments.cpp index f0bb21b1144..2f9ceb31255 100644 --- a/src/goto-programs/parameter_assignments.cpp +++ b/src/goto-programs/parameter_assignments.cpp @@ -76,7 +76,6 @@ void parameter_assignmentst::do_function_calls( if(rhs.type()!=lhs.type()) rhs.make_typecast(lhs.type()); t->code=code_assignt(lhs, rhs); - t->function=i_it->function; } } diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index a64c33fb8e7..6bf63367ee5 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -100,7 +100,7 @@ static bool read_bin_goto_object_v4( goto_programt::instructiont &instruction=*itarget; irepconverter.reference_convert(in, instruction.code); - instruction.function = irepconverter.read_string_ref(in); + irepconverter.read_string_ref(in); // former function irepconverter.reference_convert(in, instruction.source_location); instruction.type = (goto_program_instruction_typet) irepconverter.read_gb_word(in); diff --git a/src/goto-programs/remove_calls_no_body.cpp b/src/goto-programs/remove_calls_no_body.cpp index 2db01a7c59b..7861117f7b6 100644 --- a/src/goto-programs/remove_calls_no_body.cpp +++ b/src/goto-programs/remove_calls_no_body.cpp @@ -38,7 +38,6 @@ void remove_calls_no_bodyt::remove_call_no_body( goto_programt::targett t = tmp.add_instruction(); t->make_other(code_expressiont(argument)); t->source_location = target->source_location; - t->function = target->function; } // return value @@ -51,7 +50,6 @@ void remove_calls_no_bodyt::remove_call_no_body( goto_programt::targett t = tmp.add_instruction(ASSIGN); t->source_location = target->source_location; - t->function = target->function; t->code.swap(code); } diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 87c9aa3ba88..343473b623a 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -422,7 +422,6 @@ void remove_function_pointerst::remove_function_pointer( irep_idt property_class=it->source_location.get_property_class(); irep_idt comment=it->source_location.get_comment(); it->source_location=target->source_location; - it->function=target->function; if(!property_class.empty()) it->source_location.set_property_class(property_class); if(!comment.empty()) diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index f45aa2dea7f..6979d63ff0e 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -210,7 +210,6 @@ void remove_returnst::do_function_calls( t_a->make_assignment(); t_a->source_location=i_it->source_location; t_a->code=code_assignt(function_call.lhs(), rhs); - t_a->function=i_it->function; // fry the previous assignment function_call.lhs().make_nil(); @@ -221,7 +220,6 @@ void remove_returnst::do_function_calls( t_d->make_dead(); t_d->source_location=i_it->source_location; t_d->code = code_deadt(*return_value); - t_d->function=i_it->function; } } } diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index aa4863629c2..19e1bea9850 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -328,7 +328,6 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( const irep_idt property_class=it->source_location.get_property_class(); const irep_idt comment=it->source_location.get_comment(); it->source_location=target->source_location; - it->function=target->function; if(!property_class.empty()) it->source_location.set_property_class(property_class); if(!comment.empty()) diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index fc9a84751af..62c51152c3a 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -285,7 +285,6 @@ void string_abstractiont::make_decl_and_def(goto_programt &dest, goto_programt::targett decl1 = dest.add(goto_programt::make_decl(sym_expr, ref_instr->source_location)); - decl1->function=ref_instr->function; decl1->code.add_source_location()=ref_instr->source_location; exprt val=symbol.value; @@ -302,7 +301,6 @@ void string_abstractiont::make_decl_and_def(goto_programt &dest, goto_programt::targett assignment1=dest.add_instruction(); assignment1->make_assignment(); assignment1->source_location=ref_instr->source_location; - assignment1->function=ref_instr->function; assignment1->code=code_assignt(sym_expr, val); assignment1->code.add_source_location()=ref_instr->source_location; } @@ -362,7 +360,6 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest, goto_programt::targett assignment1=dest.add_instruction(); assignment1->make_assignment(); assignment1->source_location=ref_instr->source_location; - assignment1->function=ref_instr->function; assignment1->code=code_assignt(member, sym_expr); assignment1->code.add_source_location()=ref_instr->source_location; } @@ -410,7 +407,6 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value( goto_programt::targett decl=dest.add_instruction(); decl->make_decl(); decl->source_location=ref_instr->source_location; - decl->function=ref_instr->function; decl->code=code_declt(sym_expr); decl->code.add_source_location()=ref_instr->source_location; @@ -436,7 +432,6 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value( goto_programt::targett assignment1=dest.add_instruction(); assignment1->make_assignment(); assignment1->source_location=ref_instr->source_location; - assignment1->function=ref_instr->function; assignment1->code=code_assignt(sym_expr, new_symbol.value); assignment1->code.add_source_location()=ref_instr->source_location; } @@ -1085,7 +1080,6 @@ goto_programt::targett string_abstractiont::abstract_pointer_assign( goto_programt::instructiont assignment; assignment.make_assignment(); assignment.source_location=target->source_location; - assignment.function=target->function; assignment.code=code_assignt(new_lhs, new_rhs); assignment.code.add_source_location()=target->source_location; dest.insert_before_swap(target, assignment); @@ -1181,14 +1175,12 @@ goto_programt::targett string_abstractiont::char_assign( goto_programt::targett assignment1=tmp.add_instruction(); assignment1->make_assignment(); assignment1->source_location=target->source_location; - assignment1->function=target->function; assignment1->code=code_assignt(i1, true_exprt()); assignment1->code.add_source_location()=target->source_location; goto_programt::targett assignment2=tmp.add_instruction(); assignment2->make_assignment(); assignment2->source_location=target->source_location; - assignment2->function=target->function; assignment2->code=code_assignt(lhs, rhs); assignment2->code.add_source_location()=target->source_location; @@ -1263,18 +1255,14 @@ goto_programt::targett string_abstractiont::value_assignments_if( goto_programt::targett else_target=tmp.add_instruction(SKIP); goto_programt::targett out_target=tmp.add_instruction(SKIP); - goto_else->function=target->function; goto_else->source_location=target->source_location; goto_else->make_goto(else_target, boolean_negate(rhs.cond())); - goto_out->function=target->function; goto_out->source_location=target->source_location; goto_out->make_goto(out_target, true_exprt()); - else_target->function=target->function; else_target->source_location=target->source_location; - out_target->function=target->function; out_target->source_location=target->source_location; value_assignments(tmp, goto_out, lhs, rhs.true_case()); @@ -1302,7 +1290,6 @@ goto_programt::targett string_abstractiont::value_assignments_string_struct( member(lhs, whatt::IS_ZERO), member(rhs, whatt::IS_ZERO)); assignment->code.add_source_location()=target->source_location; - assignment->function=target->function; assignment->source_location=target->source_location; } @@ -1312,7 +1299,6 @@ goto_programt::targett string_abstractiont::value_assignments_string_struct( member(lhs, whatt::LENGTH), member(rhs, whatt::LENGTH)); assignment->code.add_source_location()=target->source_location; - assignment->function=target->function; assignment->source_location=target->source_location; } @@ -1322,7 +1308,6 @@ goto_programt::targett string_abstractiont::value_assignments_string_struct( member(lhs, whatt::SIZE), member(rhs, whatt::SIZE)); assignment->code.add_source_location()=target->source_location; - assignment->function=target->function; assignment->source_location=target->source_location; } diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp index fdebda05b43..5b42fce4e5e 100644 --- a/src/goto-programs/write_goto_binary.cpp +++ b/src/goto-programs/write_goto_binary.cpp @@ -97,7 +97,7 @@ bool write_goto_binary_v4( const goto_programt::instructiont &instruction = *i_it; irepconverter.reference_convert(instruction.code, out); - irepconverter.write_string_ref(out, instruction.function); + irepconverter.write_string_ref(out, fct.first); irepconverter.reference_convert(instruction.source_location, out); write_gb_word(out, (long)instruction.type); irepconverter.reference_convert(instruction.guard, out); diff --git a/unit/goto-programs/goto_program_assume.cpp b/unit/goto-programs/goto_program_assume.cpp index aa4ef524fd8..5663d750659 100644 --- a/unit/goto-programs/goto_program_assume.cpp +++ b/unit/goto-programs/goto_program_assume.cpp @@ -39,7 +39,6 @@ SCENARIO( symbol_table.insert(fun_symbol); namespacet ns(symbol_table); instructions.back().make_assertion(x_le_10); - instructions.back().function = fun_name; WHEN("Instruction has no targets") { diff --git a/unit/goto-programs/goto_program_dead.cpp b/unit/goto-programs/goto_program_dead.cpp index b57ad6ca7c6..cdc56690b4e 100644 --- a/unit/goto-programs/goto_program_dead.cpp +++ b/unit/goto-programs/goto_program_dead.cpp @@ -37,7 +37,6 @@ SCENARIO( code_deadt removal(var_a); instructions.back().make_dead(); instructions.back().code = removal; - instructions.back().function = fun_name; symbol_table.insert(fun_symbol); WHEN("Removing known symbol") diff --git a/unit/goto-programs/goto_program_declaration.cpp b/unit/goto-programs/goto_program_declaration.cpp index e273ffd3129..c1379b95e4a 100644 --- a/unit/goto-programs/goto_program_declaration.cpp +++ b/unit/goto-programs/goto_program_declaration.cpp @@ -36,7 +36,6 @@ SCENARIO( instructions.emplace_back(goto_program_instruction_typet::DECL); code_declt declaration(var_a); instructions.back().make_decl(declaration); - instructions.back().function = fun_name; symbol_table.insert(fun_symbol); WHEN("Declaring known symbol") diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp index 3407fc0f069..2fb8687dc68 100644 --- a/unit/goto-programs/goto_program_function_call.cpp +++ b/unit/goto-programs/goto_program_function_call.cpp @@ -42,7 +42,6 @@ SCENARIO( goto_functiont goto_function; auto &instructions = goto_function.body.instructions; instructions.emplace_back(goto_program_instruction_typet::FUNCTION_CALL); - instructions.back().function = fun_symbol_name; var_symbol.type = type1; var_symbol2.type = type2; diff --git a/unit/goto-programs/goto_program_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp index bc0349fe200..84aae2cbebd 100644 --- a/unit/goto-programs/goto_program_goto_target.cpp +++ b/unit/goto-programs/goto_program_goto_target.cpp @@ -35,11 +35,9 @@ SCENARIO( auto &instructions = goto_function.body.instructions; instructions.emplace_back(goto_program_instruction_typet::ASSERT); instructions.back().make_assertion(x_le_10); - instructions.back().function = fun_name; instructions.emplace_back(goto_program_instruction_typet::GOTO); instructions.back().make_goto(instructions.begin()); - instructions.back().function = fun_name; symbol.type = type1; symbol_table.insert(symbol); diff --git a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp index 07090357cfd..32c636ee7f6 100644 --- a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp +++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp @@ -36,7 +36,6 @@ SCENARIO( auto &instructions = goto_function.body.instructions; instructions.emplace_back(goto_program_instruction_typet::ASSERT); instructions.back().make_assertion(x_le_10); - instructions.back().function = function_symbol.name; symbol_table.insert(function_symbol); WHEN("Symbol table has the right symbol type") diff --git a/unit/goto-programs/goto_program_table_consistency.cpp b/unit/goto-programs/goto_program_table_consistency.cpp index d33ea824671..40bf9c5e5e4 100644 --- a/unit/goto-programs/goto_program_table_consistency.cpp +++ b/unit/goto-programs/goto_program_table_consistency.cpp @@ -35,7 +35,6 @@ SCENARIO( auto &instructions = goto_function.body.instructions; instructions.emplace_back(goto_program_instruction_typet::ASSERT); instructions.back().make_assertion(x_le_10); - instructions.back().function = function_symbol.name; symbol_table.insert(function_symbol); WHEN("Symbol table has the right symbol") From 8ddd9ba7f72588bf45440872eb821c4e785866ef Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Jan 2019 12:36:27 +0000 Subject: [PATCH 3/3] goto_inline: replace source location if adjust_function is set We no longer need to change an instruction's function member, but should update the source location instead. --- src/goto-programs/goto_inline_class.cpp | 32 ++++--------------------- 1 file changed, 5 insertions(+), 27 deletions(-) diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 7021f971dc0..f50b23d62e2 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -315,37 +315,15 @@ void goto_inlinet::insert_function_body( call_location_number, identifier); -#if 0 - if(goto_function.is_hidden()) + if(adjust_function) { - source_locationt new_source_location= - function.find_source_location(); - - if(new_source_location.is_not_nil()) + Forall_goto_program_instructions(it, tmp) { - new_source_location.set_hide(); - - Forall_goto_program_instructions(it, tmp) - { - if(it->function==identifier) - { - // don't hide assignment to lhs - if(it->is_assign() && it->get_assign().lhs()==lhs) - { - } - else - { - replace_location(it->source_location, new_source_location); - replace_location(it->guard, new_source_location); - replace_location(it->code, new_source_location); - } - - it->function=target->function; - } - } + replace_location(it->source_location, target->source_location); + replace_location(it->guard, target->source_location); + replace_location(it->code, target->source_location); } } -#endif // kill call target->type=LOCATION;