Merge pull request #2457 from tautschnig/vs-goto-convert

Remove unused parameters in goto_convert

Author: kroening

src/goto-programs/builtin_functions.cpp

@@ -320,7 +320,6 @@ void goto_convertt::do_scanf(
 }
 
 void goto_convertt::do_input(
-  const exprt &lhs,
   const exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
@@ -341,7 +340,6 @@ void goto_convertt::do_input(
 }
 
 void goto_convertt::do_output(
-  const exprt &lhs,
   const exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
@@ -846,12 +844,26 @@ void goto_convertt::do_function_call_symbol(
   else if(identifier==CPROVER_PREFIX "input" ||
           identifier=="__CPROVER::input")
   {
-    do_input(lhs, function, arguments, dest);
+    if(lhs.is_not_nil())
+    {
+      error().source_location=function.find_source_location();
+      error() << identifier << " expected not to have LHS" << eom;
+      throw 0;
+    }
+
+    do_input(function, arguments, dest);
   }
   else if(identifier==CPROVER_PREFIX "output" ||
           identifier=="__CPROVER::output")
   {
-    do_output(lhs, function, arguments, dest);
+    if(lhs.is_not_nil())
+    {
+      error().source_location=function.find_source_location();
+      error() << identifier << " expected not to have LHS" << eom;
+      throw 0;
+    }
+
+    do_output(function, arguments, dest);
   }
   else if(identifier==CPROVER_PREFIX "atomic_begin" ||
           identifier=="__CPROVER::atomic_begin" ||

src/goto-programs/goto_convert_class.h

@@ -126,17 +126,15 @@ class goto_convertt:public messaget
     bool result_is_used);
   void remove_cpp_delete(
     side_effect_exprt &expr,
-    goto_programt &dest,
-    bool result_is_used);
+    goto_programt &dest);
   void remove_malloc(
     side_effect_exprt &expr,
     goto_programt &dest,
     const irep_idt &mode,
     bool result_is_used);
   void remove_temporary_object(
     side_effect_exprt &expr,
-    goto_programt &dest,
-    bool result_is_used);
+    goto_programt &dest);
   void remove_statement_expression(
     side_effect_exprt &expr,
     goto_programt &dest,
@@ -631,12 +629,10 @@ class goto_convertt:public messaget
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_input(
-    const exprt &lhs,
     const exprt &rhs,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_output(
-    const exprt &lhs,
     const exprt &rhs,
     const exprt::operandst &arguments,
     goto_programt &dest);

src/goto-programs/goto_convert_side_effect.cpp

@@ -452,8 +452,7 @@ void goto_convertt::remove_cpp_new(
 
 void goto_convertt::remove_cpp_delete(
   side_effect_exprt &expr,
-  goto_programt &dest,
-  bool result_is_used)
+  goto_programt &dest)
 {
   assert(expr.operands().size()==1);
 
@@ -507,8 +506,7 @@ void goto_convertt::remove_malloc(
 
 void goto_convertt::remove_temporary_object(
   side_effect_exprt &expr,
-  goto_programt &dest,
-  bool result_is_used)
+  goto_programt &dest)
 {
   const irep_idt &mode = expr.get(ID_mode);
   if(expr.operands().size()!=1 &&
@@ -666,11 +664,11 @@ void goto_convertt::remove_side_effect(
     remove_cpp_new(expr, dest, result_is_used);
   else if(statement==ID_cpp_delete ||
           statement==ID_cpp_delete_array)
-    remove_cpp_delete(expr, dest, result_is_used);
+    remove_cpp_delete(expr, dest);
   else if(statement==ID_allocate)
     remove_malloc(expr, dest, mode, result_is_used);
   else if(statement==ID_temporary_object)
-    remove_temporary_object(expr, dest, result_is_used);
+    remove_temporary_object(expr, dest);
   else if(statement==ID_statement_expression)
     remove_statement_expression(expr, dest, mode, result_is_used);
   else if(statement==ID_nondet)

src/goto-programs/parameter_assignments.cpp

@@ -31,13 +31,11 @@ class parameter_assignmentst
   symbol_tablet &symbol_table;
 
   void do_function_calls(
-    goto_functionst &goto_functions,
     goto_programt &goto_program);
 };
 
 /// turns x=f(...) into f(...); lhs=f#return_value;
 void parameter_assignmentst::do_function_calls(
-  goto_functionst &goto_functions,
   goto_programt &goto_program)
 {
   Forall_goto_program_instructions(i_it, goto_program)
@@ -93,7 +91,7 @@ void parameter_assignmentst::do_function_calls(
 void parameter_assignmentst::operator()(goto_functionst &goto_functions)
 {
   Forall_goto_functions(it, goto_functions)
-    do_function_calls(goto_functions, it->second.body);
+    do_function_calls(it->second.body);
 }
 
 /// removes returns

src/goto-programs/remove_returns.cpp

@@ -52,7 +52,6 @@ class remove_returnst
     goto_functionst::function_mapt::iterator f_it);
 
   void undo_function_calls(
-    goto_functionst &goto_functions,
     goto_programt &goto_program);
 
   symbol_exprt get_or_create_return_value_symbol(const irep_idt &function_id);
@@ -366,7 +365,6 @@ bool remove_returnst::restore_returns(
 
 /// turns f(...); lhs=f#return_value; into lhs=f(...)
 void remove_returnst::undo_function_calls(
-  goto_functionst &goto_functions,
   goto_programt &goto_program)
 {
   namespacet ns(symbol_table);
@@ -436,7 +434,7 @@ void remove_returnst::restore(goto_functionst &goto_functions)
   if(!unmodified)
   {
     Forall_goto_functions(it, goto_functions)
-      undo_function_calls(goto_functions, it->second.body);
+      undo_function_calls(it->second.body);
   }
 }