goto_unwindt now takes function identifier

Author: Daniel Kroening

src/goto-instrument/k_induction.cpp

@@ -24,12 +24,12 @@ Author: Daniel Kroening, [email protected]
 class k_inductiont
 {
 public:
-  typedef goto_functionst::goto_functiont goto_functiont;
-
   k_inductiont(
+    const irep_idt &_function_identifier,
     goto_functiont &_goto_function,
     bool _base_case, bool _step_case,
     unsigned _k):
+    function_identifier(_function_identifier),
     goto_function(_goto_function),
     local_may_alias(_goto_function),
     natural_loops(_goto_function.body),
@@ -39,6 +39,7 @@ class k_inductiont
   }
 
 protected:
+  const irep_idt &function_identifier;
   goto_functiont &goto_function;
   local_may_aliast local_may_alias;
   natural_loops_mutablet natural_loops;
@@ -70,7 +71,8 @@ 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_unwind.unwind(function_identifier,
+                       goto_function.body, loop_head, loop_exit, k,
                        goto_unwindt::unwind_strategyt::PARTIAL);
 
     // assume the loop condition has become false
@@ -96,6 +98,7 @@ void k_inductiont::process_loop(
 
     goto_unwindt goto_unwind;
     goto_unwind.unwind(
+      function_identifier,
       goto_function.body,
       loop_head,
       loop_exit,
@@ -155,5 +158,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

@@ -77,18 +77,20 @@ void goto_unwindt::copy_segment(
 }
 
 void goto_unwindt::unwind(
+  const irep_idt &function_identifier,
   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,
+  unwind(function_identifier, goto_program, loop_head, loop_exit, k, unwind_strategy,
          iteration_points);
 }
 
 void goto_unwindt::unwind(
+  const irep_idt &function_identifier,
   goto_programt &goto_program,
   const goto_programt::const_targett loop_head,
   const goto_programt::const_targett loop_exit,
@@ -257,6 +259,7 @@ void goto_unwindt::unwind(
 }
 
 void goto_unwindt::unwind(
+  const irep_idt &function_identifier,
   goto_programt &goto_program,
   const unwindsett &unwindset,
   const unwind_strategyt unwind_strategy)
@@ -277,7 +280,7 @@ void goto_unwindt::unwind(
       continue;
     }
 
-    const irep_idt func=i_it->function;
+    const irep_idt func=function_identifier;
     assert(!func.empty());
 
     const irep_idt loop_id=
@@ -297,7 +300,7 @@ 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_identifier, goto_program, loop_head, loop_exit, *limit, unwind_strategy);
 
     // necessary as we change the goto program in the previous line
     i_it=loop_exit;
@@ -322,7 +325,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

@@ -29,13 +29,15 @@ class goto_unwindt
   // unwind loop
 
   void unwind(
+    const irep_idt &function_identifier,
     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_identifier,
     goto_programt &goto_program,
     const goto_programt::const_targett loop_head,
     const goto_programt::const_targett loop_exit,
@@ -46,6 +48,7 @@ class goto_unwindt
   // unwind function
 
   void unwind(
+    const irep_idt &function_identifier,
     goto_programt &goto_program,
     const unwindsett &unwindset,
     const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL);