Merge pull request diffblue#2484 from tautschnig/vs-printf

printf does not and should not have a left-hand side

Author: Daniel Kroening

src/goto-symex/goto_symex.h

@@ -455,7 +455,7 @@ class goto_symext
   virtual void symex_fkt(statet &, const code_function_callt &);
   virtual void symex_macro(statet &, const code_function_callt &);
   virtual void symex_trace(statet &, const code_function_callt &);
-  virtual void symex_printf(statet &, const exprt &lhs, const exprt &rhs);
+  virtual void symex_printf(statet &, const exprt &rhs);
   virtual void symex_input(statet &, const codet &);
   virtual void symex_output(statet &, const codet &);
 

src/goto-symex/symex_assign.cpp

@@ -54,7 +54,11 @@ void goto_symext::symex_assign(
     else if(statement==ID_allocate)
       symex_allocate(state, lhs, side_effect_expr);
     else if(statement==ID_printf)
-      symex_printf(state, lhs, side_effect_expr);
+    {
+      if(lhs.is_not_nil())
+        throw "printf: unexpected assignment";
+      symex_printf(state, side_effect_expr);
+    }
     else if(statement==ID_gcc_builtin_va_arg_next)
       symex_gcc_builtin_va_arg_next(state, lhs, side_effect_expr);
     else

src/goto-symex/symex_builtin_functions.cpp

@@ -311,7 +311,6 @@ irep_idt get_string_argument(const exprt &src, const namespacet &ns)
 
 void goto_symext::symex_printf(
   statet &state,
-  const exprt &lhs,
   const exprt &rhs)
 {
   if(rhs.operands().empty())

src/goto-symex/symex_other.cpp

@@ -101,7 +101,7 @@ void goto_symext::symex_other(
   {
     codet clean_code=code;
     clean_expr(clean_code, state, false);
-    symex_printf(state, nil_exprt(), clean_code);
+    symex_printf(state, clean_code);
   }
   else if(statement==ID_input)
   {