Make symex_target take a level1t lhs

Author: romainbrenguier

src/goto-symex/symex_decl.cpp

@@ -80,7 +80,7 @@ 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:

src/goto-symex/symex_target.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_GOTO_SYMEX_SYMEX_TARGET_H
 
 #include <goto-programs/goto_program.h>
+#include "renaming_level.h"
 
 class ssa_exprt;
 class symbol_exprt;
@@ -128,7 +129,7 @@ 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;
 

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

@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/prop/literal.h>
 
 #include "symex_target.h"
+#include "renaming_level.h"
 
 class decision_proceduret;
 class namespacet;
@@ -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);