Skip to content

Commit c0819f9

Browse files
tautschnigtautschnig
authored
Merge pull request #4175 from tautschnig/return-has-an-operand
Return statements always have one operand
2 parents 67f2e0c + ac150b5 commit c0819f9

15 files changed

+72
-84
lines changed

‎jbmc/src/java_bytecode/java_bytecode_instrument.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -415,12 +415,10 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
415415
}
416416
else if(statement==ID_return)
417417
{
418-
if(code.operands().size()==1)
419-
{
420-
code_blockt block;
421-
add_expr_instrumentation(block, code.op0());
422-
prepend_instrumentation(code, block);
423-
}
418+
code_blockt block;
419+
code_returnt &code_return = to_code_return(code);
420+
add_expr_instrumentation(block, code_return.return_value());
421+
prepend_instrumentation(code, block);
424422
}
425423
else if(statement==ID_function_call)
426424
{

‎jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -52,8 +52,8 @@ void java_bytecode_typecheckt::typecheck_code(codet &code)
5252
}
5353
else if(statement==ID_return)
5454
{
55-
if(code.operands().size()==1)
56-
typecheck_expr(code.op0());
55+
code_returnt &code_return = to_code_return(code);
56+
typecheck_expr(code_return.return_value());
5757
}
5858
else if(statement==ID_function_call)
5959
{

‎src/ansi-c/c_typecheck_base.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@ class c_typecheck_baset:
138138
virtual void typecheck_gcc_computed_goto(codet &code);
139139
virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &);
140140
virtual void typecheck_gcc_local_label(codet &code);
141-
virtual void typecheck_return(codet &code);
141+
virtual void typecheck_return(code_returnt &code);
142142
virtual void typecheck_switch(code_switcht &code);
143143
virtual void typecheck_while(code_whilet &code);
144144
virtual void typecheck_dowhile(code_dowhilet &code);

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 17 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ void c_typecheck_baset::typecheck_code(codet &code)
6868
else if(statement==ID_continue)
6969
typecheck_continue(code);
7070
else if(statement==ID_return)
71-
typecheck_return(code);
71+
typecheck_return(to_code_return(code));
7272
else if(statement==ID_decl)
7373
typecheck_decl(code);
7474
else if(statement==ID_assign)
@@ -630,49 +630,40 @@ void c_typecheck_baset::typecheck_start_thread(codet &code)
630630
typecheck_code(to_code(code.op0()));
631631
}
632632

633-
void c_typecheck_baset::typecheck_return(codet &code)
633+
void c_typecheck_baset::typecheck_return(code_returnt &code)
634634
{
635-
if(code.operands().empty())
635+
if(code.has_return_value())
636636
{
637-
if(
638-
return_type.id() != ID_empty && return_type.id() != ID_constructor &&
639-
return_type.id() != ID_destructor)
640-
{
641-
// gcc doesn't actually complain, it just warns!
642-
warning().source_location = code.source_location();
643-
warning() << "non-void function should return a value" << eom;
644-
645-
code.copy_to_operands(
646-
side_effect_expr_nondett(return_type, code.source_location()));
647-
}
648-
}
649-
else if(code.operands().size()==1)
650-
{
651-
typecheck_expr(code.op0());
637+
typecheck_expr(code.return_value());
652638

653639
if(return_type.id() == ID_empty)
654640
{
655641
// gcc doesn't actually complain, it just warns!
656-
if(code.op0().type().id() != ID_empty)
642+
if(code.return_value().type().id() != ID_empty)
657643
{
658644
warning().source_location=code.source_location();
659645

660646
warning() << "function has return void ";
661647
warning() << "but a return statement returning ";
662-
warning() << to_string(code.op0().type());
648+
warning() << to_string(code.return_value().type());
663649
warning() << eom;
664650

665-
code.op0() = typecast_exprt(code.op0(), return_type);
651+
code.return_value() = typecast_exprt(code.return_value(), return_type);
666652
}
667653
}
668654
else
669-
implicit_typecast(code.op0(), return_type);
655+
implicit_typecast(code.return_value(), return_type);
670656
}
671-
else
657+
else if(
658+
return_type.id() != ID_empty && return_type.id() != ID_constructor &&
659+
return_type.id() != ID_destructor)
672660
{
673-
error().source_location = code.source_location();
674-
error() << "return expected to have 0 or 1 operands" << eom;
675-
throw 0;
661+
// gcc doesn't actually complain, it just warns!
662+
warning().source_location = code.source_location();
663+
warning() << "non-void function should return a value" << eom;
664+
665+
code.return_value() =
666+
side_effect_expr_nondett(return_type, code.source_location());
676667
}
677668
}
678669

‎src/ansi-c/expr2c.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2587,8 +2587,7 @@ std::string expr2ct::convert_code_return(
25872587
const codet &src,
25882588
unsigned indent)
25892589
{
2590-
if(!src.operands().empty() &&
2591-
src.operands().size()!=1)
2590+
if(src.operands().size() != 1)
25922591
{
25932592
unsigned precedence;
25942593
return convert_norep(src, precedence);

‎src/ansi-c/parser.y

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2426,7 +2426,11 @@ jump_statement:
24262426
| TOK_BREAK ';'
24272427
{ $$=$1; statement($$, ID_break); }
24282428
| TOK_RETURN ';'
2429-
{ $$=$1; statement($$, ID_return); }
2429+
{
2430+
$$=$1;
2431+
statement($$, ID_return);
2432+
stack($$).operands().push_back(nil_exprt());
2433+
}
24302434
| TOK_RETURN comma_expression ';'
24312435
{ $$=$1; statement($$, ID_return); mto($$, $2); }
24322436
;

‎src/cpp/parse.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7344,7 +7344,7 @@ bool Parser::rStatement(codet &statement)
73447344

73457345
lex.get_token(tk1);
73467346

7347-
statement=codet(ID_return);
7347+
statement = code_returnt();
73487348
set_location(statement, tk1);
73497349

73507350
if(lex.LookAhead(0)==';')
@@ -7375,7 +7375,7 @@ bool Parser::rStatement(codet &statement)
73757375
if(lex.get_token(tk2)!=';')
73767376
return false;
73777377

7378-
statement.add_to_operands(std::move(exp));
7378+
to_code_return(statement).return_value() = std::move(exp);
73797379
}
73807380

73817381
return true;

‎src/pointer-analysis/value_set.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1510,11 +1510,13 @@ void value_sett::apply_code_rec(
15101510
}
15111511
else if(statement==ID_return)
15121512
{
1513+
const code_returnt &code_return = to_code_return(code);
15131514
// this is turned into an assignment
1514-
if(code.operands().size()==1)
1515+
if(code_return.has_return_value())
15151516
{
1516-
symbol_exprt lhs("value_set::return_value", code.op0().type());
1517-
assign(lhs, code.op0(), ns, false, false);
1517+
symbol_exprt lhs(
1518+
"value_set::return_value", code_return.return_value().type());
1519+
assign(lhs, code_return.return_value(), ns, false, false);
15181520
}
15191521
}
15201522
else if(statement==ID_array_set)

‎src/pointer-analysis/value_set_fi.cpp

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1310,16 +1310,14 @@ void value_set_fit::do_end_function(
13101310
assign(lhs, rhs, ns);
13111311
}
13121312

1313-
void value_set_fit::apply_code(
1314-
const exprt &code,
1315-
const namespacet &ns)
1313+
void value_set_fit::apply_code(const codet &code, const namespacet &ns)
13161314
{
13171315
const irep_idt &statement=code.get(ID_statement);
13181316

13191317
if(statement==ID_block)
13201318
{
1321-
forall_operands(it, code)
1322-
apply_code(*it, ns);
1319+
for(const auto &stmt : to_code_block(code).statements())
1320+
apply_code(stmt, ns);
13231321
}
13241322
else if(statement==ID_function_call)
13251323
{
@@ -1372,12 +1370,13 @@ void value_set_fit::apply_code(
13721370
}
13731371
else if(statement==ID_return)
13741372
{
1373+
const code_returnt &code_return = to_code_return(code);
13751374
// this is turned into an assignment
1376-
if(code.operands().size()==1)
1375+
if(code_return.has_return_value())
13771376
{
13781377
std::string rvs="value_set::return_value"+std::to_string(from_function);
1379-
symbol_exprt lhs(rvs, code.op0().type());
1380-
assign(lhs, code.op0(), ns);
1378+
symbol_exprt lhs(rvs, code_return.return_value().type());
1379+
assign(lhs, code_return.return_value(), ns);
13811380
}
13821381
}
13831382
else if(statement==ID_fence)

‎src/pointer-analysis/value_set_fi.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ Author: Daniel Kroening, [email protected]
2424

2525
#include "object_numbering.h"
2626

27+
class codet;
28+
2729
class value_set_fit
2830
{
2931
public:
@@ -271,9 +273,7 @@ class value_set_fit
271273
return make_union(new_values.values);
272274
}
273275

274-
void apply_code(
275-
const exprt &code,
276-
const namespacet &ns);
276+
void apply_code(const codet &code, const namespacet &ns);
277277

278278
void assign(
279279
const exprt &lhs,

‎src/pointer-analysis/value_set_fivr.cpp

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1460,16 +1460,14 @@ void value_set_fivrt::do_end_function(
14601460
assign(lhs, rhs, ns);
14611461
}
14621462

1463-
void value_set_fivrt::apply_code(
1464-
const exprt &code,
1465-
const namespacet &ns)
1463+
void value_set_fivrt::apply_code(const codet &code, const namespacet &ns)
14661464
{
14671465
const irep_idt &statement=code.get(ID_statement);
14681466

14691467
if(statement==ID_block)
14701468
{
1471-
forall_operands(it, code)
1472-
apply_code(*it, ns);
1469+
for(const auto &stmt : to_code_block(code).statements())
1470+
apply_code(stmt, ns);
14731471
}
14741472
else if(statement==ID_function_call)
14751473
{
@@ -1522,12 +1520,14 @@ void value_set_fivrt::apply_code(
15221520
}
15231521
else if(statement==ID_return)
15241522
{
1523+
const code_returnt &code_return = to_code_return(code);
15251524
// this is turned into an assignment
1526-
if(code.operands().size()==1)
1525+
if(code_return.has_return_value())
15271526
{
1528-
std::string rvs="value_set::return_value" + std::to_string(from_function);
1529-
symbol_exprt lhs(rvs, code.op0().type());
1530-
assign(lhs, code.op0(), ns);
1527+
std::string rvs =
1528+
"value_set::return_value" + std::to_string(from_function);
1529+
symbol_exprt lhs(rvs, code_return.return_value().type());
1530+
assign(lhs, code_return.return_value(), ns);
15311531
}
15321532
}
15331533
else if(statement==ID_input || statement==ID_output)

‎src/pointer-analysis/value_set_fivr.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ Author: Daniel Kroening, [email protected]
2424

2525
#include "object_numbering.h"
2626

27+
class codet;
28+
2729
class value_set_fivrt
2830
{
2931
public:
@@ -307,9 +309,7 @@ class value_set_fivrt
307309
object_mapt &dest,
308310
const object_mapt &src) const;
309311

310-
void apply_code(
311-
const exprt &code,
312-
const namespacet &ns);
312+
void apply_code(const codet &code, const namespacet &ns);
313313

314314
bool handover();
315315

‎src/pointer-analysis/value_set_fivrns.cpp

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1123,16 +1123,14 @@ void value_set_fivrnst::do_end_function(
11231123
assign(lhs, rhs, ns);
11241124
}
11251125

1126-
void value_set_fivrnst::apply_code(
1127-
const exprt &code,
1128-
const namespacet &ns)
1126+
void value_set_fivrnst::apply_code(const codet &code, const namespacet &ns)
11291127
{
11301128
const irep_idt &statement=code.get(ID_statement);
11311129

11321130
if(statement==ID_block)
11331131
{
1134-
forall_operands(it, code)
1135-
apply_code(*it, ns);
1132+
for(const auto &stmt : to_code_block(code).statements())
1133+
apply_code(stmt, ns);
11361134
}
11371135
else if(statement==ID_function_call)
11381136
{
@@ -1185,14 +1183,15 @@ void value_set_fivrnst::apply_code(
11851183
}
11861184
else if(statement==ID_return)
11871185
{
1186+
const code_returnt &code_return = to_code_return(code);
11881187
// this is turned into an assignment
1189-
if(code.operands().size()==1)
1188+
if(code_return.has_return_value())
11901189
{
1191-
irep_idt rvs = std::string("value_set::return_value") +
1192-
std::to_string(from_function);
1190+
std::string rvs =
1191+
"value_set::return_value" + std::to_string(from_function);
11931192
add_var(rvs);
1194-
symbol_exprt lhs(rvs, code.op0().type());
1195-
assign(lhs, code.op0(), ns);
1193+
symbol_exprt lhs(rvs, code_return.return_value().type());
1194+
assign(lhs, code_return.return_value(), ns);
11961195
}
11971196
}
11981197
else if(statement==ID_input || statement==ID_output)

‎src/pointer-analysis/value_set_fivrns.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,8 @@ Author: Daniel Kroening, [email protected]
2525

2626
#include "object_numbering.h"
2727

28+
class codet;
29+
2830
class value_set_fivrnst
2931
{
3032
public:
@@ -304,9 +306,7 @@ class value_set_fivrnst
304306
object_mapt &dest,
305307
const object_mapt &src) const;
306308

307-
void apply_code(
308-
const exprt &code,
309-
const namespacet &ns);
309+
void apply_code(const codet &code, const namespacet &ns);
310310

311311
bool handover();
312312

‎src/util/std_code.h

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1255,10 +1255,8 @@ inline void validate_expr(const code_function_callt &x)
12551255
class code_returnt:public codet
12561256
{
12571257
public:
1258-
code_returnt():codet(ID_return)
1258+
code_returnt() : codet(ID_return, {nil_exprt()})
12591259
{
1260-
operands().resize(1);
1261-
op0().make_nil();
12621260
}
12631261

12641262
explicit code_returnt(const exprt &_op) : codet(ID_return, {_op})
@@ -1277,8 +1275,6 @@ class code_returnt:public codet
12771275

12781276
bool has_return_value() const
12791277
{
1280-
if(operands().empty())
1281-
return false; // backwards compatibility
12821278
return return_value().is_not_nil();
12831279
}
12841280

0 commit comments

Comments
 (0)