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

kroening · web-flow · commit d65c6558c610 · 2018-06-26T17:43:29.000+01:00
printf does not and should not have a left-hand side
diff --git a/src/goto-symex/goto_symex.h b/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 &);
 
diff --git a/src/goto-symex/symex_assign.cpp b/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
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/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())
diff --git a/src/goto-symex/symex_other.cpp b/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)
   {

Original file line number	Diff line number	Diff line change
`@@ -311,7 +311,6 @@ irep_idt get_string_argument(const exprt &src, const namespacet &ns)`
`311`	`311`
`312`	`312`	`void goto_symext::symex_printf(`
`313`	`313`	`statet &state,`
`314`		`- const exprt &lhs,`
`315`	`314`	`const exprt &rhs)`
`316`	`315`	`{`
`317`	`316`	`if(rhs.operands().empty())`
Original file line number	Diff line number	Diff line change
`@@ -101,7 +101,7 @@ void goto_symext::symex_other(`
`101`	`101`	`{`
`102`	`102`	`codet clean_code=code;`
`103`	`103`	`clean_expr(clean_code, state, false);`
`104`		`- symex_printf(state, nil_exprt(), clean_code);`
	`104`	`+ symex_printf(state, clean_code);`
`105`	`105`	`}`
`106`	`106`	`else if(statement==ID_input)`
`107`	`107`	`{`