diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index 08e29037c70..ebda62896dd 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -12,6 +12,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include +#include #include #include #include @@ -169,6 +170,10 @@ bool static_simplifier( goto_model.goto_functions.update(); } + // restore return types before writing the binary + restore_returns(goto_model); + goto_model.goto_functions.update(); + m.status() << "Writing goto binary" << messaget::eom; return write_goto_binary(out, ns.get_symbol_table(), diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 5257c83ea0a..71d2761dc5c 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -352,38 +352,9 @@ bool remove_returnst::restore_returns( continue; // replace "fkt#return_value=x;" by "return x;" - code_returnt return_code(assign.rhs()); - - // the assignment might be a goto target - i_it->make_skip(); - i_it++; - - while(!i_it->is_goto() && !i_it->is_end_function()) - { - INVARIANT( - i_it->is_dead(), - "only dead statements should appear between " - "a return and the next goto or function end"); - i_it++; - } - - if(i_it->is_goto()) - { - INVARIANT( - i_it->get_target()->is_end_function(), - "GOTO following return should target end of function"); - } - else - { - INVARIANT( - i_it->is_end_function(), - "control-flow after assigning return value should lead directly " - "to end of function"); - i_it=goto_program.instructions.insert(i_it, *i_it); - } - + const exprt rhs = assign.rhs(); i_it->make_return(); - i_it->code=return_code; + i_it->code = code_returnt(rhs); } }