Merge pull request #294 from danpoe/remove-returns

Restore returns fix

Author: Daniel Kroening

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;)

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
+

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
+

regression/goto-instrument/restore-returns1/ret.c

@@ -0,0 +1,13 @@
+
+int foo()
+{
+  int x;
+  return x;
+}
+
+int main()
+{
+  foo();
+  return 0;
+}
+

regression/goto-instrument/restore-returns1/test.desc

@@ -0,0 +1,7 @@
+CORE
+ret.c
+"--escape-analysis --dump-c"
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

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;
+}
+

regression/goto-instrument/restore-returns2/test.desc

@@ -0,0 +1,7 @@
+CORE
+ret.c
+"--escape-analysis --dump-c"
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

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;
     }
   }