goto_unwindt now takes function identifier

We are working towards removing the "function" field from
goto_programt::instructionst::instructiont, and thus need to pass the identifier
of the function whenever it actually is required.

Author: Daniel Kroening

src/goto-instrument/k_induction.cpp

@@ -24,21 +24,25 @@ Author: Daniel Kroening, [email protected]
 class k_inductiont
 {
 public:
-  typedef goto_functionst::goto_functiont goto_functiont;
-
   k_inductiont(
+    const irep_idt &_function_id,
     goto_functiont &_goto_function,
-    bool _base_case, bool _step_case,
-    unsigned _k):
-    goto_function(_goto_function),
-    local_may_alias(_goto_function),
-    natural_loops(_goto_function.body),
-    base_case(_base_case), step_case(_step_case), k(_k)
+    bool _base_case,
+    bool _step_case,
+    unsigned _k)
+    : function_id(_function_id),
+      goto_function(_goto_function),
+      local_may_alias(_goto_function),
+      natural_loops(_goto_function.body),
+      base_case(_base_case),
+      step_case(_step_case),
+      k(_k)
   {
     k_induction();
   }
 
 protected:
+  const irep_idt &function_id;
   goto_functiont &goto_function;
   local_may_aliast local_may_alias;
   natural_loops_mutablet natural_loops;
@@ -70,8 +74,13 @@ void k_inductiont::process_loop(
   {
     // now unwind k times
     goto_unwindt goto_unwind;
-    goto_unwind.unwind(goto_function.body, loop_head, loop_exit, k,
-                       goto_unwindt::unwind_strategyt::PARTIAL);
+    goto_unwind.unwind(
+      function_id,
+      goto_function.body,
+      loop_head,
+      loop_exit,
+      k,
+      goto_unwindt::unwind_strategyt::PARTIAL);
 
     // assume the loop condition has become false
     goto_programt::instructiont assume(ASSUME);
@@ -96,10 +105,11 @@ void k_inductiont::process_loop(
 
     goto_unwindt goto_unwind;
     goto_unwind.unwind(
+      function_id,
       goto_function.body,
       loop_head,
       loop_exit,
-      k+1,
+      k + 1,
       goto_unwindt::unwind_strategyt::PARTIAL,
       iteration_points);
 
@@ -155,5 +165,5 @@ void k_induction(
   unsigned k)
 {
   Forall_goto_functions(it, goto_model.goto_functions)
-    k_inductiont(it->second, base_case, step_case, k);
+    k_inductiont(it->first, it->second, base_case, step_case, k);
 }

src/goto-instrument/unwind.cpp

@@ -80,18 +80,26 @@ void goto_unwindt::copy_segment(
 }
 
 void goto_unwindt::unwind(
+  const irep_idt &function_id,
   goto_programt &goto_program,
   const goto_programt::const_targett loop_head,
   const goto_programt::const_targett loop_exit,
   const unsigned k,
   const unwind_strategyt unwind_strategy)
 {
   std::vector<goto_programt::targett> iteration_points;
-  unwind(goto_program, loop_head, loop_exit, k, unwind_strategy,
-         iteration_points);
+  unwind(
+    function_id,
+    goto_program,
+    loop_head,
+    loop_exit,
+    k,
+    unwind_strategy,
+    iteration_points);
 }
 
 void goto_unwindt::unwind(
+  const irep_idt &function_id,
   goto_programt &goto_program,
   const goto_programt::const_targett loop_head,
   const goto_programt::const_targett loop_exit,
@@ -258,6 +266,7 @@ void goto_unwindt::unwind(
 }
 
 void goto_unwindt::unwind(
+  const irep_idt &function_id,
   goto_programt &goto_program,
   const unwindsett &unwindset,
   const unwind_strategyt unwind_strategy)
@@ -278,11 +287,9 @@ void goto_unwindt::unwind(
       continue;
     }
 
-    const irep_idt func=i_it->function;
-    assert(!func.empty());
-
-    const irep_idt loop_id=
-      id2string(func) + "." + std::to_string(i_it->loop_number);
+    PRECONDITION(!function_id.empty());
+    const irep_idt loop_id =
+      id2string(function_id) + "." + std::to_string(i_it->loop_number);
 
     auto limit=unwindset.get_limit(loop_id, 0);
 
@@ -298,7 +305,8 @@ void goto_unwindt::unwind(
     loop_exit++;
     assert(loop_exit!=goto_program.instructions.end());
 
-    unwind(goto_program, loop_head, loop_exit, *limit, unwind_strategy);
+    unwind(
+      function_id, goto_program, loop_head, loop_exit, *limit, unwind_strategy);
 
     // necessary as we change the goto program in the previous line
     i_it=loop_exit;
@@ -323,7 +331,7 @@ void goto_unwindt::operator()(
 
     goto_programt &goto_program=goto_function.body;
 
-    unwind(goto_program, unwindset, unwind_strategy);
+    unwind(it->first, goto_program, unwindset, unwind_strategy);
   }
 }
 

src/goto-instrument/unwind.h

@@ -28,13 +28,15 @@ class goto_unwindt
   // unwind loop
 
   void unwind(
+    const irep_idt &function_id,
     goto_programt &goto_program,
     const goto_programt::const_targett loop_head,
     const goto_programt::const_targett loop_exit,
     const unsigned k, // bound for given loop
     const unwind_strategyt unwind_strategy);
 
   void unwind(
+    const irep_idt &function_id,
     goto_programt &goto_program,
     const goto_programt::const_targett loop_head,
     const goto_programt::const_targett loop_exit,
@@ -45,9 +47,10 @@ class goto_unwindt
   // unwind function
 
   void unwind(
+    const irep_idt &function_id,
     goto_programt &goto_program,
     const unwindsett &unwindset,
-    const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL);
+    const unwind_strategyt unwind_strategy = unwind_strategyt::PARTIAL);
 
   // unwind all functions
   void operator()(