Make symex_level0t::operator() return a renamedt

This makes it explicit that the expresssion has been renamed.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -237,7 +237,9 @@ void goto_symex_statet::set_l0_indices(
   ssa_exprt &ssa_expr,
   const namespacet &ns)
 {
-  ssa_expr = level0(std::move(ssa_expr), ns, source.thread_nr);
+  renamedt<ssa_exprt, L0> renamed =
+    level0(std::move(ssa_expr), ns, source.thread_nr);
+  ssa_expr = renamed.get();
 }
 
 void goto_symex_statet::set_l1_indices(
@@ -248,8 +250,9 @@ void goto_symex_statet::set_l1_indices(
     return;
   if(!ssa_expr.get_level_1().empty())
     return;
-  ssa_exprt l0 = level0(std::move(ssa_expr), ns, source.thread_nr);
-  ssa_expr = level1(std::move(l0));
+  renamedt<ssa_exprt, L0> l0 =
+    level0(std::move(ssa_expr), ns, source.thread_nr);
+  ssa_expr = level1(l0.get());
 }
 
 void goto_symex_statet::set_l2_indices(
@@ -258,8 +261,9 @@ void goto_symex_statet::set_l2_indices(
 {
   if(!ssa_expr.get_level_2().empty())
     return;
-  ssa_exprt l0 = level0(std::move(ssa_expr), ns, source.thread_nr);
-  ssa_exprt l1 = level1(std::move(l0));
+  renamedt<ssa_exprt, L0> l0 =
+    level0(std::move(ssa_expr), ns, source.thread_nr);
+  ssa_exprt l1 = level1(l0.get());
   ssa_expr = level2(std::move(l1));
 }
 

src/goto-symex/renaming_level.cpp

@@ -17,30 +17,30 @@ Author: Romain Brenguier, [email protected]
 
 #include "goto_symex_state.h"
 
-ssa_exprt symex_level0t::
+renamedt<ssa_exprt, L0> symex_level0t::
 operator()(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) const
 {
   // already renamed?
   if(!ssa_expr.get_level_0().empty())
-    return std::move(ssa_expr);
+    return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
 
   const irep_idt &obj_identifier = ssa_expr.get_object_name();
 
   // guards are not L0-renamed
   if(obj_identifier == goto_symex_statet::guard_identifier())
-    return std::move(ssa_expr);
+    return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
 
   const symbolt *s;
   const bool found_l0 = !ns.lookup(obj_identifier, s);
   INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
 
   // don't rename shared variables or functions
   if(s->type.id() == ID_code || s->is_shared())
-    return std::move(ssa_expr);
+    return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
 
   // rename!
   ssa_expr.set_level_0(thread_nr);
-  return ssa_expr;
+  return renamedt<ssa_exprt, L0>{ssa_expr};
 }
 
 ssa_exprt symex_level1t::operator()(ssa_exprt ssa_expr) const

src/goto-symex/renaming_level.h

@@ -93,7 +93,7 @@ class renamedt
 /// The renaming is built for one particular interleaving.
 struct symex_level0t : public symex_renaming_levelt
 {
-  ssa_exprt operator()(
+  renamedt<ssa_exprt, L0> operator()(
     ssa_exprt ssa_expr,
     const namespacet &ns,
     unsigned thread_nr) const;