Merge pull request #3126 from diffblue/goto-instruction-function

remove goto_programt::instructiont::function member [blocks: #3113]

Author: tautschnig

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;
     }
 

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();
   }
 }
 

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)
   {

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);

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

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;
     }
   }
 }

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++;
 

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)
   {

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()));
 }

src/goto-instrument/branch.cpp

@@ -54,15 +54,13 @@ 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());
 
         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);
       }