remove goto_programt::instructiont::function member

Author: Daniel Kroening

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();
 }
@@ -351,7 +349,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
         symbol_typet type(stack_catch[i][j].first);
@@ -376,7 +373,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)
@@ -385,7 +381,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;
   }
 }
 
@@ -467,7 +462,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;
     }
 

src/analyses/flow_insensitive_analysis.cpp

@@ -212,12 +212,10 @@ bool flow_insensitive_analysis_baset::do_function_call(
     goto_programt::targett r=temp.add_instruction();
     r->make_return();
     r->code=code_returnt(rhs);
-    r->function=f_it->first;
     r->location_number=0;
 
     goto_programt::targett t=temp.add_instruction(END_FUNCTION);
     t->code.set(ID_identifier, code.function());
-    t->function=f_it->first;
     t->location_number=1;
 
     locationt l_next=l_call; l_next++;
@@ -238,9 +236,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

@@ -1770,9 +1770,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/cbmc/symex_bmc.cpp

@@ -110,7 +110,7 @@ bool symex_bmct::get_unwind(
   const goto_symex_statet::call_stackt &context,
   unsigned unwind)
 {
-  const irep_idt id=goto_programt::loop_id(*source.pc);
+  const irep_idt id = goto_programt::loop_id(source.function, *source.pc);
 
   tvt abort_unwind_decision;
   unsigned this_loop_limit=std::numeric_limits<unsigned>::max();

src/goto-instrument/aggressive_slicer.cpp

@@ -46,8 +46,8 @@ void aggressive_slicert::get_all_functions_containing_properties()
       for(const auto &ins : fct.second.body.instructions)
         if(ins.is_assert())
         {
-          if(functions_to_keep.insert(ins.function).second)
-            note_functions_to_keep(ins.function);
+          if(functions_to_keep.insert(fct.first).second)
+            note_functions_to_keep(fct.first);
         }
     }
   }

src/goto-instrument/branch.cpp

@@ -53,15 +53,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);
       }

src/goto-instrument/code_contracts.cpp

@@ -111,7 +111,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");
   }
@@ -123,7 +122,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;
   }
 
@@ -134,7 +132,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
@@ -145,7 +142,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);
@@ -215,7 +211,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);
@@ -294,7 +289,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;
@@ -303,7 +297,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
@@ -314,7 +307,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=
@@ -335,7 +327,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=
@@ -357,7 +348,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
@@ -367,13 +357,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
@@ -382,7 +370,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

src/goto-instrument/cover_instrument.h

@@ -73,7 +73,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);
-    t->function = function;
   }
 
   bool is_non_cover_assertion(goto_programt::const_targett t) const

src/goto-instrument/cover_instrument_mcdc.cpp

@@ -668,7 +668,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);
-      i_it->function = function;
 
       std::string comment_f = description + " `" + p_string + "' false";
       goto_program.insert_before_swap(i_it);
@@ -678,7 +677,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);
-      i_it->function = function;
     }
 
     std::set<exprt> controlling;
@@ -705,7 +703,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);
-      i_it->function = function;
     }
 
     for(std::size_t i = 0; i < both.size() * 2 + controlling.size(); i++)

src/goto-instrument/cover_instrument_other.cpp

@@ -87,5 +87,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);
-  if_it->function = function;
 }

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

src/goto-instrument/havoc_loops.cpp

@@ -96,7 +96,6 @@ void havoc_loopst::build_havoc_code(
       side_effect_expr_nondett(lhs.type(), loop_head->source_location);
 
     goto_programt::targett t=dest.add_instruction(ASSIGN);
-    t->function=loop_head->function;
     t->source_location=loop_head->source_location;
     t->code=code_assignt(lhs, rhs);
     t->code.add_source_location()=loop_head->source_location;

src/goto-instrument/interrupt.cpp

@@ -104,11 +104,9 @@ 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);
 
@@ -132,11 +130,9 @@ 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
     }

src/goto-instrument/loop_utils.cpp

@@ -49,7 +49,6 @@ void build_havoc_code(
       side_effect_expr_nondett(lhs.type(), loop_head->source_location);
 
     goto_programt::targett t=dest.add_instruction(ASSIGN);
-    t->function=loop_head->function;
     t->source_location=loop_head->source_location;
     t->code=code_assignt(lhs, rhs);
     t->code.add_source_location()=loop_head->source_location;

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("<built-in-library>");
-    it->function=goto_model.goto_functions.entry_point();
-  }
 
   goto_functionst::function_mapt::iterator start_entry=
     goto_model.goto_functions.function_map.find(

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

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

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