Extract a rename_level0_ssa function

The rename<L0> function will normally be used with ssa symbols, we add
that function to avoid unecessary decision making.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -262,6 +262,15 @@ void goto_symex_statet::set_l2_indices(
   ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
 }
 
+ssa_exprt
+goto_symex_statet::rename_level0_ssa(ssa_exprt ssa, const namespacet &ns)
+{
+  set_l0_indices(ssa, ns);
+  rename(ssa.type(), ssa.get_identifier(), ns, L0);
+  ssa.update_type();
+  return ssa;
+}
+
 void goto_symex_statet::rename(
   exprt &expr,
   const namespacet &ns,
@@ -276,9 +285,7 @@ void goto_symex_statet::rename(
 
     if(level == L0)
     {
-      set_l0_indices(ssa, ns);
-      rename(expr.type(), ssa.get_identifier(), ns, level);
-      ssa.update_type();
+      ssa = rename_level0_ssa(std::move(ssa), ns);
     }
     else if(level == L1)
     {

src/goto-symex/goto_symex_state.h

@@ -180,6 +180,9 @@ class goto_symex_statet final : public goto_statet
   /// A full explanation of SSA (which is why we do this renaming) is in
   /// the SSA section of background-concepts.md.
   void rename(exprt &expr, const namespacet &ns, levelt level=L2);
+
+  ssa_exprt rename_level0_ssa(ssa_exprt ssa, const namespacet &ns);
+
   void rename(
     typet &type,
     const irep_idt &l1_identifier,

src/goto-symex/symex_function_call.cpp

@@ -395,8 +395,8 @@ static void locality(
       it++)
   {
     // get L0 name
-    ssa_exprt ssa(ns.lookup(*it).symbol_expr());
-    state.rename(ssa, ns, goto_symex_statet::L0);
+    ssa_exprt ssa =
+      state.rename_level0_ssa(ssa_exprt(ns.lookup(*it).symbol_expr()), ns);
     const irep_idt l0_name=ssa.get_identifier();
 
     // save old L1 name for popping the frame