Skip to content

Commit 0e85e07

Browse files
Code readability
1 parent 95ed595 commit 0e85e07

File tree

1 file changed

+35
-40
lines changed

1 file changed

+35
-40
lines changed

cbmc/src/goto-programs/remove_returns.cpp

+35-40
Original file line numberDiff line numberDiff line change
@@ -56,59 +56,54 @@ void remove_returnst::replace_returns(
5656

5757
const irep_idt function_id=f_it->first;
5858

59-
// returns something but void?
60-
bool has_return_value=return_type!=empty_typet();
59+
// Nothing to do if this function returns void
60+
if(return_type==empty_typet())
61+
return;
6162

62-
if(has_return_value)
63-
{
64-
// look up the function symbol
65-
symbol_tablet::symbolst::iterator s_it=
66-
symbol_table.symbols.find(function_id);
63+
// look up the function symbol
64+
symbol_tablet::symbolst::iterator s_it=
65+
symbol_table.symbols.find(function_id);
6766

68-
assert(s_it!=symbol_table.symbols.end());
69-
symbolt &function_symbol=s_it->second;
70-
71-
// make the return type 'void'
72-
f_it->second.type.return_type()=empty_typet();
73-
function_symbol.type=f_it->second.type;
74-
75-
// add return_value symbol to symbol_table
76-
auxiliary_symbolt new_symbol;
77-
new_symbol.is_static_lifetime=true;
78-
new_symbol.module=function_symbol.module;
79-
new_symbol.base_name=
80-
id2string(function_symbol.base_name)+RETURN_VALUE_SUFFIX;
81-
new_symbol.name=id2string(function_symbol.name)+RETURN_VALUE_SUFFIX;
82-
new_symbol.mode=function_symbol.mode;
83-
new_symbol.type=return_type;
84-
85-
symbol_table.add(new_symbol);
86-
}
67+
assert(s_it!=symbol_table.symbols.end());
68+
symbolt &function_symbol=s_it->second;
69+
70+
// make the return type 'void'
71+
f_it->second.type.return_type()=empty_typet();
72+
function_symbol.type=f_it->second.type;
73+
74+
// add return_value symbol to symbol_table
75+
auxiliary_symbolt new_symbol;
76+
new_symbol.is_static_lifetime=true;
77+
new_symbol.module=function_symbol.module;
78+
new_symbol.base_name=
79+
id2string(function_symbol.base_name)+RETURN_VALUE_SUFFIX;
80+
new_symbol.name=id2string(function_symbol.name)+RETURN_VALUE_SUFFIX;
81+
new_symbol.mode=function_symbol.mode;
82+
new_symbol.type=return_type;
83+
84+
symbol_table.add(new_symbol);
8785

8886
goto_programt &goto_program=f_it->second.body;
8987

9088
if(goto_program.empty())
9189
return;
9290

93-
if(has_return_value)
91+
Forall_goto_program_instructions(i_it, goto_program)
9492
{
95-
Forall_goto_program_instructions(i_it, goto_program)
93+
if(i_it->is_return())
9694
{
97-
if(i_it->is_return())
98-
{
99-
assert(i_it->code.operands().size()==1);
95+
assert(i_it->code.operands().size()==1);
10096

101-
// replace "return x;" by "fkt#return_value=x;"
102-
symbol_exprt lhs_expr;
103-
lhs_expr.set_identifier(id2string(function_id)+RETURN_VALUE_SUFFIX);
104-
lhs_expr.type()=return_type;
97+
// replace "return x;" by "fkt#return_value=x;"
98+
symbol_exprt lhs_expr;
99+
lhs_expr.set_identifier(id2string(function_id)+RETURN_VALUE_SUFFIX);
100+
lhs_expr.type()=return_type;
105101

106-
code_assignt assignment(lhs_expr, i_it->code.op0());
102+
code_assignt assignment(lhs_expr, i_it->code.op0());
107103

108-
// now turn the `return' into `assignment'
109-
i_it->type=ASSIGN;
110-
i_it->code=assignment;
111-
}
104+
// now turn the `return' into `assignment'
105+
i_it->type=ASSIGN;
106+
i_it->code=assignment;
112107
}
113108
}
114109
}

0 commit comments

Comments
 (0)