Skip to content

Commit 49333eb

Browse files
committed
Make restore_returns handle simplified programs
The static simplifier may have removed useless goto statements, leaving programs in a form not previously expected by restore_returns, while it actually is still safe to use restore_returns on those.
1 parent 9fe432b commit 49333eb

File tree

1 file changed

+2
-31
lines changed

1 file changed

+2
-31
lines changed

src/goto-programs/remove_returns.cpp

+2-31
Original file line numberDiff line numberDiff line change
@@ -352,38 +352,9 @@ bool remove_returnst::restore_returns(
352352
continue;
353353

354354
// replace "fkt#return_value=x;" by "return x;"
355-
code_returnt return_code(assign.rhs());
356-
357-
// the assignment might be a goto target
358-
i_it->make_skip();
359-
i_it++;
360-
361-
while(!i_it->is_goto() && !i_it->is_end_function())
362-
{
363-
INVARIANT(
364-
i_it->is_dead(),
365-
"only dead statements should appear between "
366-
"a return and the next goto or function end");
367-
i_it++;
368-
}
369-
370-
if(i_it->is_goto())
371-
{
372-
INVARIANT(
373-
i_it->get_target()->is_end_function(),
374-
"GOTO following return should target end of function");
375-
}
376-
else
377-
{
378-
INVARIANT(
379-
i_it->is_end_function(),
380-
"control-flow after assigning return value should lead directly "
381-
"to end of function");
382-
i_it=goto_program.instructions.insert(i_it, *i_it);
383-
}
384-
355+
const exprt rhs = assign.rhs();
385356
i_it->make_return();
386-
i_it->code=return_code;
357+
i_it->code = code_returnt(rhs);
387358
}
388359
}
389360

0 commit comments

Comments
 (0)