Add a rename_level1 function

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -320,6 +320,45 @@ void goto_symex_statet::rename_level0(exprt &expr, const namespacet &ns)
   }
 }
 
+void goto_symex_statet::rename_level1(exprt &expr, const namespacet &ns)
+{
+  // rename all the symbols with their last known value
+  if(auto ssa = expr_try_dynamic_cast<ssa_exprt>(expr))
+  {
+    set_l1_indices(level0, level1, *ssa, source.thread_nr, ns);
+    rename(expr.type(), ssa->get_identifier(), ns, L1);
+    ssa->update_type();
+  }
+  else if(expr.id() == ID_symbol)
+  {
+    // we never rename function symbols
+    if(expr.type().id() == ID_code)
+    {
+      rename(expr.type(), to_symbol_expr(expr).get_identifier(), ns, L1);
+      return;
+    }
+
+    expr = ssa_exprt(expr);
+    rename_level1(expr, ns);
+  }
+  else if(auto address_of_expr = expr_try_dynamic_cast<address_of_exprt>(expr))
+  {
+    rename_address(address_of_expr->object(), ns, L1);
+    to_pointer_type(expr.type()).subtype() = address_of_expr->object().type();
+  }
+  else
+  {
+    // this could go wrong, but we would have to re-typecheck ...
+    rename(expr.type(), irep_idt(), ns, L1);
+
+    // do this recursively
+    for(auto &op : expr.operands())
+      rename_level1(op, ns);
+
+    fix_type(expr);
+  }
+}
+
 void goto_symex_statet::rename(
   exprt &expr,
   const namespacet &ns,

src/goto-symex/goto_symex_state.h

@@ -73,6 +73,7 @@ class goto_symex_statet final
   // performs renaming _up to_ the given level
   void rename(exprt &expr, const namespacet &ns, levelt level=L2);
   void rename_level0(exprt &expr, const namespacet &ns);
+  void rename_level1(exprt &expr, const namespacet &ns);
   void rename(
     typet &type,
     const irep_idt &l1_identifier,