Make symex_target take a level1t lhs

Author: romainbrenguier

src/goto-symex/symex_decl.cpp

@@ -81,10 +81,11 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
 
   target.decl(
     state.guard.as_expr(),
-    ssa.expr,
+    ssa,
     state.source,
-    hidden ? symex_targett::assignment_typet::HIDDEN
-           : symex_targett::assignment_typet::STATE);
+    hidden?
+      symex_targett::assignment_typet::HIDDEN:
+      symex_targett::assignment_typet::STATE);
 
   if(state.dirty(ssa.expr.get_object_name()) && state.atomic_section_id == 0)
     target.shared_write(

src/goto-symex/symex_target.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_H
 #define CPROVER_GOTO_SYMEX_SYMEX_TARGET_H
 
+#include "renaming_level.h"
 #include <goto-programs/goto_program.h>
 
 class ssa_exprt;
@@ -128,9 +129,9 @@ class symex_targett
   ///  assignments (some may be hidden for the further analysis)
   virtual void decl(
     const exprt &guard,
-    const ssa_exprt &ssa_lhs,
+    const level1t<ssa_exprt> &ssa_lhs,
     const sourcet &source,
-    assignment_typet assignment_type)=0;
+    assignment_typet assignment_type) = 0;
 
   /// Remove a variable from the scope.
   /// \param guard: Precondition for removal of this variable

src/goto-symex/symex_target_equation.cpp

@@ -141,19 +141,19 @@ void symex_target_equationt::assignment(
 
 void symex_target_equationt::decl(
   const exprt &guard,
-  const ssa_exprt &ssa_lhs,
+  const level1t<ssa_exprt> &ssa_lhs,
   const sourcet &source,
   assignment_typet assignment_type)
 {
-  PRECONDITION(ssa_lhs.is_not_nil());
+  PRECONDITION(ssa_lhs.expr.is_not_nil());
 
   SSA_steps.emplace_back(source, goto_trace_stept::typet::DECL);
   SSA_stept &SSA_step=SSA_steps.back();
 
   SSA_step.guard=guard;
-  SSA_step.ssa_lhs=ssa_lhs;
-  SSA_step.ssa_full_lhs=ssa_lhs;
-  SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
+  SSA_step.ssa_lhs = ssa_lhs.expr;
+  SSA_step.ssa_full_lhs = ssa_lhs.expr;
+  SSA_step.original_full_lhs = ssa_lhs.expr.get_original_expr();
   SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
 
   // the condition is trivially true, and only

src/goto-symex/symex_target_equation.h

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/prop/literal.h>
 
+#include "renaming_level.h"
 #include "symex_target.h"
 
 class decision_proceduret;
@@ -66,7 +67,7 @@ class symex_target_equationt:public symex_targett
   /// \copydoc symex_targett::decl()
   virtual void decl(
     const exprt &guard,
-    const ssa_exprt &ssa_lhs,
+    const level1t<ssa_exprt> &ssa_lhs,
     const sourcet &source,
     assignment_typet assignment_type);