diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index 4ae7ae42741..0eb5f36b47d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/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) { diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp index ce58aa6f1f2..52ac8490fbe 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp +++ b/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) { diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 6a860384f0d..0f232d7906e 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/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); diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 4e3eba58117..849940bbbc7 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/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()); } } diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 083ce0d26f8..a20ce849331 100644 --- a/src/ansi-c/expr2c.cpp +++ b/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); diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index a45f582aa8a..25e63ffdc80 100644 --- a/src/ansi-c/parser.y +++ b/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); } ; diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 7bf53207e2f..f1eca6260a1 100644 --- a/src/cpp/parse.cpp +++ b/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; diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index d108947794e..486b0e1b365 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/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) diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 58ec4e51d9c..4a65e3d9729 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/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) diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h index c9a5cd0f114..d919c554ad1 100644 --- a/src/pointer-analysis/value_set_fi.h +++ b/src/pointer-analysis/value_set_fi.h @@ -24,6 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com #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, diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index b13aa2da58b..2deb17e0105 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/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) diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h index 3bf9a0004ad..adb95534526 100644 --- a/src/pointer-analysis/value_set_fivr.h +++ b/src/pointer-analysis/value_set_fivr.h @@ -24,6 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com #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(); diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 9ea66c0f2bc..1c0bbb93063 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/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) diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h index 7e371b738a1..d89196e68a9 100644 --- a/src/pointer-analysis/value_set_fivrns.h +++ b/src/pointer-analysis/value_set_fivrns.h @@ -25,6 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com #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(); diff --git a/src/util/std_code.h b/src/util/std_code.h index a364d8e8b03..b986986fbdb 100644 --- a/src/util/std_code.h +++ b/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(); }