Make restore_from take symex_level1t

This ensures we don't accidentaly mix maps from different levels.

Author: romainbrenguier

src/goto-symex/frame.h

@@ -32,7 +32,7 @@ struct framet
   exprt return_value = nil_exprt();
   bool hidden_function = false;
 
-  symex_renaming_levelt old_level1;
+  symex_level1t old_level1;
 
   std::set<irep_idt> local_objects;
 

src/goto-symex/goto_symex_state.cpp

@@ -803,8 +803,8 @@ ssa_exprt goto_symex_statet::add_object(
   if(const auto old_value = level1.insert_or_replace(renamed, l1_index))
   {
     // save old L1 name
-    if(!frame.old_level1.has_key(l0_name))
-      frame.old_level1.insert(l0_name, *old_value);
+    if(!frame.old_level1.has(renamed))
+      frame.old_level1.insert(renamed, old_value->second);
   }
 
   const ssa_exprt ssa = rename_ssa<L1>(renamed.get(), ns).get();

src/goto-symex/renaming_level.cpp

@@ -116,10 +116,10 @@ operator()(renamedt<ssa_exprt, L1> l1_expr) const
   return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
 }
 
-void symex_level1t::restore_from(const symex_renaming_levelt &other)
+void symex_level1t::restore_from(const symex_level1t &other)
 {
   symex_renaming_levelt::delta_viewt delta_view;
-  other.get_delta_view(current_names, delta_view, false);
+  other.current_names.get_delta_view(current_names, delta_view, false);
 
   for(const auto &delta_item : delta_view)
   {

src/goto-symex/renaming_level.h

@@ -74,7 +74,7 @@ struct symex_level1t
   renamedt<ssa_exprt, L1> operator()(renamedt<ssa_exprt, L0> l0_expr) const;
 
   /// Insert the content of \p other into this renaming
-  void restore_from(const symex_renaming_levelt &other);
+  void restore_from(const symex_level1t &other);
 
 private:
   symex_renaming_levelt current_names;