clean up symex_assign vs. symex_assign_rec

Author: Daniel Kroening

src/goto-symex/auto_objects.cpp

@@ -76,7 +76,7 @@ void goto_symext::initialize_auto_object(
         address_of_expr);
 
       code_assignt assignment(expr, rhs);
-      symex_assign_rec(state, assignment);
+      symex_assign(state, assignment);
     }
   }
 }

src/goto-symex/goto_symex.h

@@ -305,8 +305,7 @@ class goto_symext
   virtual void do_simplify(exprt &expr);
 
   // virtual void symex_block(statet &state, const codet &code);
-  void symex_assign_rec(statet &state, const code_assignt &code);
-  virtual void symex_assign(statet &state, const code_assignt &code);
+  void symex_assign(statet &state, const code_assignt &code);
 
   // havocs the given object
   void havoc_rec(statet &, const guardt &, const exprt &);

src/goto-symex/symex_assign.cpp

@@ -20,27 +20,15 @@ Author: Daniel Kroening, [email protected]
 
 // #define USE_UPDATE
 
-void goto_symext::symex_assign_rec(
-  statet &state,
-  const code_assignt &code)
-{
-  code_assignt deref_code=code;
-
-  clean_expr(deref_code.lhs(), state, true);
-  clean_expr(deref_code.rhs(), state, false);
-
-  symex_assign(state, deref_code);
-}
-
 void goto_symext::symex_assign(
   statet &state,
   const code_assignt &code)
 {
   exprt lhs=code.lhs();
   exprt rhs=code.rhs();
 
-  replace_nondet(lhs);
-  replace_nondet(rhs);
+  clean_expr(lhs, state, true);
+  clean_expr(rhs, state, false);
 
   if(rhs.id()==ID_side_effect)
   {

src/goto-symex/symex_builtin_functions.cpp

@@ -151,7 +151,7 @@ void goto_symext::symex_allocate(
       code_assignt assignment(size_symbol.symbol_expr(), size);
       size=assignment.lhs();
 
-      symex_assign_rec(state, assignment);
+      symex_assign(state, assignment);
     }
   }
 
@@ -187,7 +187,7 @@ void goto_symext::symex_allocate(
     if(zero_value.is_not_nil())
     {
       code_assignt assignment(value_symbol.symbol_expr(), zero_value);
-      symex_assign_rec(state, assignment);
+      symex_assign(state, assignment);
     }
     else
       throw "failed to zero initialize dynamic object";
@@ -212,7 +212,7 @@ void goto_symext::symex_allocate(
   if(rhs.type()!=lhs.type())
     rhs.make_typecast(lhs.type());
 
-  symex_assign_rec(state, code_assignt(lhs, rhs));
+  symex_assign(state, code_assignt(lhs, rhs));
 }
 
 irep_idt get_symbol(const exprt &src)
@@ -276,7 +276,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
     }
   }
 
-  symex_assign_rec(state, code_assignt(lhs, rhs));
+  symex_assign(state, code_assignt(lhs, rhs));
 }
 
 irep_idt get_string_argument_rec(const exprt &src)
@@ -458,7 +458,7 @@ void goto_symext::symex_cpp_new(
   else
     rhs.copy_to_operands(symbol.symbol_expr());
 
-  symex_assign_rec(state, code_assignt(lhs, rhs));
+  symex_assign(state, code_assignt(lhs, rhs));
 }
 
 void goto_symext::symex_cpp_delete(

src/goto-symex/symex_function_call.cpp

@@ -130,7 +130,7 @@ void goto_symext::parameter_assignments(
         }
       }
 
-      symex_assign_rec(state, code_assignt(lhs, rhs));
+      symex_assign(state, code_assignt(lhs, rhs));
     }
 
     if(it1!=arguments.end())
@@ -162,7 +162,7 @@ void goto_symext::parameter_assignments(
 
       symbol_exprt lhs=symbol_exprt(id, it1->type());
 
-      symex_assign_rec(state, code_assignt(lhs, *it1));
+      symex_assign(state, code_assignt(lhs, *it1));
     }
   }
   else if(it1!=arguments.end())
@@ -275,7 +275,7 @@ void goto_symext::symex_function_call_code(
       side_effect_expr_nondett rhs(call.lhs().type());
       rhs.add_source_location()=call.source_location();
       code_assignt code(call.lhs(), rhs);
-      symex_assign_rec(state, code);
+      symex_assign(state, code);
     }
 
     symex_transition(state);
@@ -455,7 +455,7 @@ void goto_symext::return_assignment(statet &state)
           "assignment.lhs().type():\n"+assignment.lhs().type().pretty()+"\n"+
           "assignment.rhs().type():\n"+assignment.rhs().type().pretty();
 
-      symex_assign_rec(state, assignment);
+      symex_assign(state, assignment);
     }
   }
   else

src/goto-symex/symex_main.cpp

@@ -293,7 +293,7 @@ void goto_symext::symex_step(
 
   case ASSIGN:
     if(!state.guard.is_false())
-      symex_assign_rec(state, to_code_assign(instruction.code));
+      symex_assign(state, to_code_assign(instruction.code));
 
     symex_transition(state);
     break;