diff --git a/regression/Makefile b/regression/Makefile index ea7e4ee4300..de8c70edd3c 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -1,4 +1,4 @@ -DIRS = ansi-c cbmc cpp +DIRS = ansi-c cbmc cpp goto-instrument test: $(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;) diff --git a/regression/goto-instrument/Makefile b/regression/goto-instrument/Makefile new file mode 100644 index 00000000000..c966780c534 --- /dev/null +++ b/regression/goto-instrument/Makefile @@ -0,0 +1,32 @@ + +default: tests.log + +test: + @if ! ../test.pl -c ../chain.sh ; then \ + ../failed-tests-printer.pl ; \ + exit 1; \ + fi + +tests.log: + @if ! ../test.pl -c ../chain.sh ; then \ + ../failed-tests-printer.pl ; \ + exit 1; \ + fi + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + @for dir in *; do \ + rm -f tests.log; \ + if [ -d "$$dir" ]; then \ + cd "$$dir"; \ + rm -f *.out *.gb; \ + cd ..; \ + fi \ + done + diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh new file mode 100755 index 00000000000..982e784937e --- /dev/null +++ b/regression/goto-instrument/chain.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +SRC=../../../src + +GC=$SRC/goto-cc/goto-cc +GI=$SRC/goto-instrument/goto-instrument + +OPTS=$1 +NAME=${2%.c} + +$GC $NAME.c -o $NAME.gb +$GI $OPTS $NAME.gb + diff --git a/regression/goto-instrument/restore-returns1/ret.c b/regression/goto-instrument/restore-returns1/ret.c new file mode 100644 index 00000000000..46ff87ce934 --- /dev/null +++ b/regression/goto-instrument/restore-returns1/ret.c @@ -0,0 +1,13 @@ + +int foo() +{ + int x; + return x; +} + +int main() +{ + foo(); + return 0; +} + diff --git a/regression/goto-instrument/restore-returns1/test.desc b/regression/goto-instrument/restore-returns1/test.desc new file mode 100644 index 00000000000..aecf983ef22 --- /dev/null +++ b/regression/goto-instrument/restore-returns1/test.desc @@ -0,0 +1,7 @@ +CORE +ret.c +"--escape-analysis --dump-c" +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/restore-returns2/ret.c b/regression/goto-instrument/restore-returns2/ret.c new file mode 100644 index 00000000000..494fb6598a6 --- /dev/null +++ b/regression/goto-instrument/restore-returns2/ret.c @@ -0,0 +1,19 @@ + +int foo() +{ + int x; + int y; + if (x) + { + return 0; + } + int z; + return 1; +} + +int main() +{ + foo(); + return 0; +} + diff --git a/regression/goto-instrument/restore-returns2/test.desc b/regression/goto-instrument/restore-returns2/test.desc new file mode 100644 index 00000000000..aecf983ef22 --- /dev/null +++ b/regression/goto-instrument/restore-returns2/test.desc @@ -0,0 +1,7 @@ +CORE +ret.c +"--escape-analysis --dump-c" +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 4a1320d4731..57f6d989aff 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -316,26 +316,29 @@ bool remove_returnst::restore_returns( // replace "fkt#return_value=x;" by "return x;" code_returnt return_code(assign.rhs()); - // now turn the `return' into `assignment' - i_it->type=RETURN; - i_it->code=return_code; + // the assignment might be a goto target + i_it->make_skip(); + i_it++; - // remove the subsequent goto (and possibly dead) - goto_programt::instructionst::iterator next=i_it; - ++next; - assert(next!=goto_program.instructions.end()); + while(!i_it->is_goto() && !i_it->is_end_function()) + { + assert(i_it->is_dead()); + i_it++; + } - if(next->is_dead()) + if(i_it->is_goto()) { - assert(to_code_dead(next->code).symbol()== - return_code.return_value()); - next=goto_program.instructions.erase(next); - assert(next!=goto_program.instructions.end()); + goto_programt::const_targett target=i_it->get_target(); + assert(target->is_end_function()); + } + else + { + assert(i_it->is_end_function()); + i_it=goto_program.instructions.insert(i_it, *i_it); } - assert(next->is_goto()); - // i_it remains valid - goto_program.instructions.erase(next); + i_it->make_return(); + i_it->code=return_code; } }