Remove unused parameters in goto_convert

tautschnig · tautschnig · commit 7dbf60aa8ef1 · 2018-06-25T13:31:37.000+01:00
diff --git a/src/goto-programs/builtin_functions.cpp b/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" ||
diff --git a/src/goto-programs/goto_convert_class.h b/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);
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/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)
diff --git a/src/goto-programs/parameter_assignments.cpp b/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
diff --git a/src/goto-programs/remove_returns.cpp b/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);
   }
 }
 

Original file line number	Diff line number	Diff line change
`@@ -31,13 +31,11 @@ class parameter_assignmentst`
`31`	`31`	`symbol_tablet &symbol_table;`
`32`	`32`
`33`	`33`	`void do_function_calls(`
`34`		`- goto_functionst &goto_functions,`
`35`	`34`	`goto_programt &goto_program);`
`36`	`35`	`};`
`37`	`36`
`38`	`37`	`/// turns x=f(...) into f(...); lhs=f#return_value;`
`39`	`38`	`void parameter_assignmentst::do_function_calls(`
`40`		`- goto_functionst &goto_functions,`
`41`	`39`	`goto_programt &goto_program)`
`42`	`40`	`{`
`43`	`41`	`Forall_goto_program_instructions(i_it, goto_program)`
`@@ -93,7 +91,7 @@ void parameter_assignmentst::do_function_calls(`
`93`	`91`	`void parameter_assignmentst::operator()(goto_functionst &goto_functions)`
`94`	`92`	`{`
`95`	`93`	`Forall_goto_functions(it, goto_functions)`
`96`		`- do_function_calls(goto_functions, it->second.body);`
	`94`	`+ do_function_calls(it->second.body);`
`97`	`95`	`}`
`98`	`96`
`99`	`97`	`/// removes returns`
Original file line number	Diff line number	Diff line change
`@@ -52,7 +52,6 @@ class remove_returnst`
`52`	`52`	`goto_functionst::function_mapt::iterator f_it);`
`53`	`53`
`54`	`54`	`void undo_function_calls(`
`55`		`- goto_functionst &goto_functions,`
`56`	`55`	`goto_programt &goto_program);`
`57`	`56`
`58`	`57`	`symbol_exprt get_or_create_return_value_symbol(const irep_idt &function_id);`
`@@ -366,7 +365,6 @@ bool remove_returnst::restore_returns(`
`366`	`365`
`367`	`366`	`/// turns f(...); lhs=f#return_value; into lhs=f(...)`
`368`	`367`	`void remove_returnst::undo_function_calls(`
`369`		`- goto_functionst &goto_functions,`
`370`	`368`	`goto_programt &goto_program)`
`371`	`369`	`{`
`372`	`370`	`namespacet ns(symbol_table);`
`@@ -436,7 +434,7 @@ void remove_returnst::restore(goto_functionst &goto_functions)`
`436`	`434`	`if(!unmodified)`
`437`	`435`	`{`
`438`	`436`	`Forall_goto_functions(it, goto_functions)`
`439`		`- undo_function_calls(goto_functions, it->second.body);`
	`437`	`+ undo_function_calls(it->second.body);`
`440`	`438`	`}`
`441`	`439`	`}`
`442`	`440`