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

@@ -72,6 +72,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())
@@ -95,6 +99,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);
+  }
 }
 
 /*******************************************************************\
@@ -219,7 +227,6 @@ void _rw_set_loct::read_write_rec(
   else if(expr.id()==ID_address_of)
   {
     assert(expr.operands().size()==1);
-
   }
   else if(expr.id()==ID_if)
   {

src/util/std_code.h

@@ -751,12 +751,18 @@ class code_returnt:public codet
 static 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);
 }
 
 static 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);
 }