Return statements always have one operand

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -415,12 +415,10 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
   }
   else if(statement==ID_return)
   {
-    if(code.operands().size()==1)
-    {
-      code_blockt block;
-      add_expr_instrumentation(block, code.op0());
-      prepend_instrumentation(code, block);
-    }
+    code_blockt block;
+    code_returnt &code_return = to_code_return(code);
+    add_expr_instrumentation(block, code_return.return_value());
+    prepend_instrumentation(code, block);
   }
   else if(statement==ID_function_call)
   {

jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp

@@ -52,8 +52,8 @@ void java_bytecode_typecheckt::typecheck_code(codet &code)
   }
   else if(statement==ID_return)
   {
-    if(code.operands().size()==1)
-      typecheck_expr(code.op0());
+    code_returnt &code_return = to_code_return(code);
+    typecheck_expr(code_return.return_value());
   }
   else if(statement==ID_function_call)
   {

src/ansi-c/c_typecheck_base.h

@@ -138,7 +138,7 @@ class c_typecheck_baset:
   virtual void typecheck_gcc_computed_goto(codet &code);
   virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &);
   virtual void typecheck_gcc_local_label(codet &code);
-  virtual void typecheck_return(codet &code);
+  virtual void typecheck_return(code_returnt &code);
   virtual void typecheck_switch(code_switcht &code);
   virtual void typecheck_while(code_whilet &code);
   virtual void typecheck_dowhile(code_dowhilet &code);

src/ansi-c/c_typecheck_code.cpp

@@ -68,7 +68,7 @@ void c_typecheck_baset::typecheck_code(codet &code)
   else if(statement==ID_continue)
     typecheck_continue(code);
   else if(statement==ID_return)
-    typecheck_return(code);
+    typecheck_return(to_code_return(code));
   else if(statement==ID_decl)
     typecheck_decl(code);
   else if(statement==ID_assign)
@@ -630,49 +630,40 @@ void c_typecheck_baset::typecheck_start_thread(codet &code)
   typecheck_code(to_code(code.op0()));
 }
 
-void c_typecheck_baset::typecheck_return(codet &code)
+void c_typecheck_baset::typecheck_return(code_returnt &code)
 {
-  if(code.operands().empty())
+  if(code.has_return_value())
   {
-    if(
-      return_type.id() != ID_empty && return_type.id() != ID_constructor &&
-      return_type.id() != ID_destructor)
-    {
-      // gcc doesn't actually complain, it just warns!
-      warning().source_location = code.source_location();
-      warning() << "non-void function should return a value" << eom;
-
-      code.copy_to_operands(
-        side_effect_expr_nondett(return_type, code.source_location()));
-    }
-  }
-  else if(code.operands().size()==1)
-  {
-    typecheck_expr(code.op0());
+    typecheck_expr(code.return_value());
 
     if(return_type.id() == ID_empty)
     {
       // gcc doesn't actually complain, it just warns!
-      if(code.op0().type().id() != ID_empty)
+      if(code.return_value().type().id() != ID_empty)
       {
         warning().source_location=code.source_location();
 
         warning() << "function has return void ";
         warning() << "but a return statement returning ";
-        warning() << to_string(code.op0().type());
+        warning() << to_string(code.return_value().type());
         warning() << eom;
 
-        code.op0() = typecast_exprt(code.op0(), return_type);
+        code.return_value() = typecast_exprt(code.return_value(), return_type);
       }
     }
     else
-      implicit_typecast(code.op0(), return_type);
+      implicit_typecast(code.return_value(), return_type);
   }
-  else
+  else if(
+    return_type.id() != ID_empty && return_type.id() != ID_constructor &&
+    return_type.id() != ID_destructor)
   {
-    error().source_location = code.source_location();
-    error() << "return expected to have 0 or 1 operands" << eom;
-    throw 0;
+    // gcc doesn't actually complain, it just warns!
+    warning().source_location = code.source_location();
+    warning() << "non-void function should return a value" << eom;
+
+    code.return_value() =
+      side_effect_expr_nondett(return_type, code.source_location());
   }
 }
 

src/ansi-c/expr2c.cpp

@@ -2587,8 +2587,7 @@ std::string expr2ct::convert_code_return(
   const codet &src,
   unsigned indent)
 {
-  if(!src.operands().empty() &&
-     src.operands().size()!=1)
+  if(src.operands().size() != 1)
   {
     unsigned precedence;
     return convert_norep(src, precedence);

src/ansi-c/parser.y

@@ -2426,7 +2426,11 @@ jump_statement:
         | TOK_BREAK ';'
         { $$=$1; statement($$, ID_break); }
         | TOK_RETURN ';'
-        { $$=$1; statement($$, ID_return); }
+        {
+          $$=$1;
+          statement($$, ID_return);
+          stack($$).operands().push_back(nil_exprt());
+        }
         | TOK_RETURN comma_expression ';'
         { $$=$1; statement($$, ID_return); mto($$, $2); }
         ;

src/cpp/parse.cpp

@@ -7344,7 +7344,7 @@ bool Parser::rStatement(codet &statement)
 
     lex.get_token(tk1);
 
-    statement=codet(ID_return);
+    statement = code_returnt();
     set_location(statement, tk1);
 
     if(lex.LookAhead(0)==';')
@@ -7375,7 +7375,7 @@ bool Parser::rStatement(codet &statement)
       if(lex.get_token(tk2)!=';')
         return false;
 
-      statement.add_to_operands(std::move(exp));
+      to_code_return(statement).return_value() = std::move(exp);
     }
 
     return true;

src/pointer-analysis/value_set.cpp

@@ -1510,11 +1510,13 @@ void value_sett::apply_code_rec(
   }
   else if(statement==ID_return)
   {
+    const code_returnt &code_return = to_code_return(code);
     // this is turned into an assignment
-    if(code.operands().size()==1)
+    if(code_return.has_return_value())
     {
-      symbol_exprt lhs("value_set::return_value", code.op0().type());
-      assign(lhs, code.op0(), ns, false, false);
+      symbol_exprt lhs(
+        "value_set::return_value", code_return.return_value().type());
+      assign(lhs, code_return.return_value(), ns, false, false);
     }
   }
   else if(statement==ID_array_set)

src/pointer-analysis/value_set_fi.cpp

@@ -1310,16 +1310,14 @@ void value_set_fit::do_end_function(
   assign(lhs, rhs, ns);
 }
 
-void value_set_fit::apply_code(
-  const exprt &code,
-  const namespacet &ns)
+void value_set_fit::apply_code(const codet &code, const namespacet &ns)
 {
   const irep_idt &statement=code.get(ID_statement);
 
   if(statement==ID_block)
   {
-    forall_operands(it, code)
-      apply_code(*it, ns);
+    for(const auto &stmt : to_code_block(code).statements())
+      apply_code(stmt, ns);
   }
   else if(statement==ID_function_call)
   {
@@ -1372,12 +1370,13 @@ void value_set_fit::apply_code(
   }
   else if(statement==ID_return)
   {
+    const code_returnt &code_return = to_code_return(code);
     // this is turned into an assignment
-    if(code.operands().size()==1)
+    if(code_return.has_return_value())
     {
       std::string rvs="value_set::return_value"+std::to_string(from_function);
-      symbol_exprt lhs(rvs, code.op0().type());
-      assign(lhs, code.op0(), ns);
+      symbol_exprt lhs(rvs, code_return.return_value().type());
+      assign(lhs, code_return.return_value(), ns);
     }
   }
   else if(statement==ID_fence)

src/pointer-analysis/value_set_fi.h

@@ -24,6 +24,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "object_numbering.h"
 
+class codet;
+
 class value_set_fit
 {
 public:
@@ -271,9 +273,7 @@ class value_set_fit
     return make_union(new_values.values);
   }
 
-  void apply_code(
-    const exprt &code,
-    const namespacet &ns);
+  void apply_code(const codet &code, const namespacet &ns);
 
   void assign(
     const exprt &lhs,

src/pointer-analysis/value_set_fivr.cpp

@@ -1460,16 +1460,14 @@ void value_set_fivrt::do_end_function(
   assign(lhs, rhs, ns);
 }
 
-void value_set_fivrt::apply_code(
-  const exprt &code,
-  const namespacet &ns)
+void value_set_fivrt::apply_code(const codet &code, const namespacet &ns)
 {
   const irep_idt &statement=code.get(ID_statement);
 
   if(statement==ID_block)
   {
-    forall_operands(it, code)
-      apply_code(*it, ns);
+    for(const auto &stmt : to_code_block(code).statements())
+      apply_code(stmt, ns);
   }
   else if(statement==ID_function_call)
   {
@@ -1522,12 +1520,14 @@ void value_set_fivrt::apply_code(
   }
   else if(statement==ID_return)
   {
+    const code_returnt &code_return = to_code_return(code);
     // this is turned into an assignment
-    if(code.operands().size()==1)
+    if(code_return.has_return_value())
     {
-      std::string rvs="value_set::return_value" + std::to_string(from_function);
-      symbol_exprt lhs(rvs, code.op0().type());
-      assign(lhs, code.op0(), ns);
+      std::string rvs =
+        "value_set::return_value" + std::to_string(from_function);
+      symbol_exprt lhs(rvs, code_return.return_value().type());
+      assign(lhs, code_return.return_value(), ns);
     }
   }
   else if(statement==ID_input || statement==ID_output)

src/pointer-analysis/value_set_fivr.h

@@ -24,6 +24,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "object_numbering.h"
 
+class codet;
+
 class value_set_fivrt
 {
 public:
@@ -307,9 +309,7 @@ class value_set_fivrt
     object_mapt &dest,
     const object_mapt &src) const;
 
-  void apply_code(
-    const exprt &code,
-    const namespacet &ns);
+  void apply_code(const codet &code, const namespacet &ns);
 
   bool handover();
 

src/pointer-analysis/value_set_fivrns.cpp

@@ -1123,16 +1123,14 @@ void value_set_fivrnst::do_end_function(
   assign(lhs, rhs, ns);
 }
 
-void value_set_fivrnst::apply_code(
-  const exprt &code,
-  const namespacet &ns)
+void value_set_fivrnst::apply_code(const codet &code, const namespacet &ns)
 {
   const irep_idt &statement=code.get(ID_statement);
 
   if(statement==ID_block)
   {
-    forall_operands(it, code)
-      apply_code(*it, ns);
+    for(const auto &stmt : to_code_block(code).statements())
+      apply_code(stmt, ns);
   }
   else if(statement==ID_function_call)
   {
@@ -1185,14 +1183,15 @@ void value_set_fivrnst::apply_code(
   }
   else if(statement==ID_return)
   {
+    const code_returnt &code_return = to_code_return(code);
     // this is turned into an assignment
-    if(code.operands().size()==1)
+    if(code_return.has_return_value())
     {
-      irep_idt rvs = std::string("value_set::return_value") +
-                     std::to_string(from_function);
+      std::string rvs =
+        "value_set::return_value" + std::to_string(from_function);
       add_var(rvs);
-      symbol_exprt lhs(rvs, code.op0().type());
-      assign(lhs, code.op0(), ns);
+      symbol_exprt lhs(rvs, code_return.return_value().type());
+      assign(lhs, code_return.return_value(), ns);
     }
   }
   else if(statement==ID_input || statement==ID_output)

src/pointer-analysis/value_set_fivrns.h

@@ -25,6 +25,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "object_numbering.h"
 
+class codet;
+
 class value_set_fivrnst
 {
 public:
@@ -304,9 +306,7 @@ class value_set_fivrnst
     object_mapt &dest,
     const object_mapt &src) const;
 
-  void apply_code(
-    const exprt &code,
-    const namespacet &ns);
+  void apply_code(const codet &code, const namespacet &ns);
 
   bool handover();
 

src/util/std_code.h

@@ -1255,10 +1255,8 @@ inline void validate_expr(const code_function_callt &x)
 class code_returnt:public codet
 {
 public:
-  code_returnt():codet(ID_return)
+  code_returnt() : codet(ID_return, {nil_exprt()})
   {
-    operands().resize(1);
-    op0().make_nil();
   }
 
   explicit code_returnt(const exprt &_op) : codet(ID_return, {_op})
@@ -1277,8 +1275,6 @@ class code_returnt:public codet
 
   bool has_return_value() const
   {
-    if(operands().empty())
-      return false; // backwards compatibility
     return return_value().is_not_nil();
   }