goto-symex: use function and called_function fields

goto_programt::instructionst::instructiont::function is going to go away, use
the fields that are already available within goto-symex.

Author: tautschnig

src/goto-checker/symex_bmc.cpp

@@ -110,7 +110,7 @@ bool symex_bmct::should_stop_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-programs/goto_program.h

@@ -694,9 +694,10 @@ class goto_programt
   void update();
 
   /// Human-readable loop name
-  static irep_idt loop_id(const instructiont &instruction)
+  static irep_idt
+  loop_id(const irep_idt &function_id, const instructiont &instruction)
   {
-    return id2string(instruction.function)+"."+
+    return id2string(function_id) + "." +
            std::to_string(instruction.loop_number);
   }
 

src/goto-symex/goto_symex_state.cpp

@@ -759,7 +759,7 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
     return;
   }
 
-  out << source.pc->function << " " << source.pc->location_number << "\n";
+  out << source.function << " " << source.pc->location_number << "\n";
 
   for(auto stackit = threads[source.thread_nr].call_stack.rbegin(),
            stackend = threads[source.thread_nr].call_stack.rend();
@@ -769,7 +769,7 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
     const auto &frame = *stackit;
     if(frame.calling_location.is_set)
     {
-      out << frame.calling_location.pc->function << " "
+      out << frame.calling_location.function << " "
           << frame.calling_location.pc->location_number << "\n";
     }
   }

src/goto-symex/symex_goto.cpp

@@ -85,8 +85,10 @@ void goto_symext::symex_goto(statet &state)
       return;
     }
 
-    unsigned &unwind=
-      frame.loop_iterations[goto_programt::loop_id(*state.source.pc)].count;
+    const auto loop_id =
+      goto_programt::loop_id(state.source.function, *state.source.pc);
+
+    unsigned &unwind = frame.loop_iterations[loop_id].count;
     unwind++;
 
     if(should_stop_unwind(state.source, state.call_stack(), unwind))

src/goto-symex/symex_main.cpp

@@ -58,7 +58,11 @@ void symex_transition(
       if(i_e->is_goto() && i_e->is_backwards_goto() &&
          (!is_backwards_goto ||
           state.source.pc->location_number>i_e->location_number))
-        frame.loop_iterations[goto_programt::loop_id(*i_e)].count=0;
+      {
+        const auto loop_id =
+          goto_programt::loop_id(state.source.function, *i_e);
+        frame.loop_iterations[loop_id].count = 0;
+      }
   }
 
   state.source.pc=to;
@@ -157,19 +161,18 @@ void goto_symext::initialize_entry_point(
   state.top().calling_location.pc=state.top().end_of_function;
   state.symex_target=⌖
 
-  INVARIANT(
-    !pc->function.empty(), "all symexed instructions should have a function");
-
-  const goto_functiont &entry_point_function = get_goto_function(pc->function);
+  const goto_functiont &entry_point_function =
+    get_goto_function(function_identifier);
 
   state.top().hidden_function = entry_point_function.is_hidden();
 
   auto emplace_safe_pointers_result =
-    state.safe_pointers.emplace(pc->function, local_safe_pointerst{ns});
+    state.safe_pointers.emplace(function_identifier, local_safe_pointerst{ns});
   if(emplace_safe_pointers_result.second)
     emplace_safe_pointers_result.first->second(entry_point_function.body);
 
-  state.dirty.populate_dirty_for_function(pc->function, entry_point_function);
+  state.dirty.populate_dirty_for_function(
+    function_identifier, entry_point_function);
 
   symex_transition(state, state.source.pc, false);
 }