rw_set: handle return and other

When calculating the set of touched symbols, also consider the symbols that are
passed to return statements. Furthermore, continue with reading symbols that
are in code labelled with "other".

Added a check to test whether return statements have at most one argument.

Author: Norbert Manthey

src/goto-instrument/rw_set.cpp

@@ -51,6 +51,10 @@ void _rw_set_loct::compute()
     assert(target->code.operands().size()==2);
     assign(target->code.op0(), target->code.op1());
   }
+  else if(target->is_return())
+  {
+    read(to_code_return(target->code));
+  }
   else if(target->is_goto() ||
           target->is_assume() ||
           target->is_assert())
@@ -74,6 +78,10 @@ void _rw_set_loct::compute()
     if(code_function_call.lhs().is_not_nil())
       write(code_function_call.lhs());
   }
+  else if(target->is_other())
+  {
+    read(target->code);
+  }
 }
 
 void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs)

src/util/std_code.h

@@ -933,12 +933,18 @@ template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
 inline const code_returnt &to_code_return(const codet &code)
 {
   assert(code.get_statement()==ID_return);
+  assert(
+    code.operands().size() <= 1 &&
+    "there should be at most one operand in an return statement");
   return static_cast<const code_returnt &>(code);
 }
 
 inline code_returnt &to_code_return(codet &code)
 {
   assert(code.get_statement()==ID_return);
+  assert(
+    code.operands().size() <= 1 &&
+    "there should be at most one operand in an return statement");
   return static_cast<code_returnt &>(code);
 }