Skip to content

Commit 2de787a

Browse files
committed
introduce instructiont::return_value()
This mirrors the change in #5861 by replacing the use of code_returnt by directly returning the return value expression. The client code is simplified considerably.
1 parent a4c81ef commit 2de787a

File tree

5 files changed

+32
-35
lines changed

5 files changed

+32
-35
lines changed

src/goto-instrument/goto_program2code.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -418,14 +418,11 @@ goto_programt::const_targett goto_program2codet::convert_return(
418418
goto_programt::const_targett upper_bound,
419419
code_blockt &dest)
420420
{
421-
const code_returnt &ret = target->get_return();
422-
423421
// add return instruction unless original code was missing a return
424-
if(!ret.has_return_value() ||
425-
ret.return_value().id()!=ID_side_effect ||
426-
to_side_effect_expr(ret.return_value()).get_statement()!=ID_nondet)
422+
if(target->return_value().id()!=ID_side_effect ||
423+
to_side_effect_expr(target->return_value()).get_statement()!=ID_nondet)
427424
{
428-
dest.add(ret);
425+
dest.add(code_returnt{target->return_value()});
429426
}
430427

431428
// all v3 (or later) goto programs have an explicit GOTO after return

src/goto-programs/goto_inline_class.cpp

Lines changed: 3 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -165,31 +165,21 @@ void goto_inlinet::replace_return(
165165
{
166166
if(it->is_return())
167167
{
168-
const auto &code_return = it->get_return();
169-
170168
if(lhs.is_not_nil())
171169
{
172-
if(!code_return.has_return_value())
173-
{
174-
log.warning().source_location = it->code.find_source_location();
175-
log.warning() << "return expects one operand!\n"
176-
<< it->code.pretty() << messaget::eom;
177-
continue;
178-
}
179-
180170
// a typecast may be necessary if the declared return type at the call
181171
// site differs from the defined return type
182172
it->code = code_assignt(
183173
lhs,
184174
typecast_exprt::conditional_cast(
185-
code_return.return_value(), lhs.type()));
175+
it->return_value(), lhs.type()));
186176
it->type=ASSIGN;
187177

188178
it++;
189179
}
190-
else if(code_return.has_return_value())
180+
else
191181
{
192-
it->code = code_expressiont(code_return.return_value());
182+
it->code = code_expressiont(it->return_value());
193183
it->type=OTHER;
194184
it++;
195185
}

src/goto-programs/goto_program.cpp

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -285,8 +285,7 @@ std::list<exprt> expressions_read(
285285
break;
286286

287287
case RETURN:
288-
if(instruction.get_return().return_value().is_not_nil())
289-
dest.push_back(instruction.get_return().return_value());
288+
dest.push_back(instruction.return_value());
290289
break;
291290

292291
case FUNCTION_CALL:
@@ -928,13 +927,9 @@ void goto_programt::instructiont::transform(
928927

929928
case RETURN:
930929
{
931-
auto new_return_value = f(get_return().return_value());
930+
auto new_return_value = f(return_value());
932931
if(new_return_value.has_value())
933-
{
934-
auto new_return = get_return();
935-
new_return.return_value() = *new_return_value;
936-
set_return(new_return);
937-
}
932+
return_value() = *new_return_value;
938933
}
939934
break;
940935

@@ -1037,7 +1032,7 @@ void goto_programt::instructiont::apply(
10371032
break;
10381033

10391034
case RETURN:
1040-
f(get_return().return_value());
1035+
f(return_value());
10411036
break;
10421037

10431038
case ASSIGN:

src/goto-programs/goto_program.h

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
1818
#include <sstream>
1919
#include <string>
2020

21+
#include <util/deprecate.h>
2122
#include <util/invariant.h>
2223
#include <util/namespace.h>
2324
#include <util/source_location.h>
@@ -231,19 +232,39 @@ class goto_programt
231232
code = std::move(c);
232233
}
233234

235+
#if 0
234236
/// Get the return statement for READ
237+
DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
235238
const code_returnt &get_return() const
236239
{
237240
PRECONDITION(is_return());
238241
return to_code_return(code);
239242
}
243+
#endif
240244

245+
/// Get the return value of a RETURN instruction
246+
const exprt &return_value() const
247+
{
248+
PRECONDITION(is_return());
249+
return to_code_return(code).return_value();
250+
}
251+
252+
/// Get the return value of a RETURN instruction
253+
exprt &return_value()
254+
{
255+
PRECONDITION(is_return());
256+
return to_code_return(code).return_value();
257+
}
258+
259+
#if 0
241260
/// Set the return statement for READ
261+
DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
242262
void set_return(code_returnt c)
243263
{
244264
PRECONDITION(is_return());
245265
code = std::move(c);
246266
}
267+
#endif
247268

248269
/// Get the function call for FUNCTION_CALL
249270
const code_function_callt &get_function_call() const

src/pointer-analysis/goto_program_dereference.cpp

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -228,13 +228,7 @@ void goto_program_dereferencet::dereference_instruction(
228228
}
229229
else if(i.is_return())
230230
{
231-
auto r = i.get_return();
232-
233-
if(r.return_value().is_not_nil())
234-
{
235-
dereference_expr(r.return_value(), checks_only);
236-
i.set_return(r);
237-
}
231+
dereference_expr(i.return_value(), checks_only);
238232
}
239233
else if(i.is_other())
240234
{

0 commit comments

Comments
 (0)