Add goto-destructor test

This checks that (a) the loop iterator 'i' gets killed before
function exit and (b) there aren't too may basic blocks (indicated
by 'GOTO 10' appearing, which would indicate the second loop's
guarded goto statements are being unnecessarily disrupted.

(For example, producing 'if(j==5) goto 2; goto end; 2: ...'
 instead of the simpler 'if(j==5) goto end; ...', which is necessary
 for the i-loop to accomodate the 'dead i;' statement, but not for
 the j-loop)

Author: smowton

regression/cbmc-java/destructor1/Break.class

@@ -0,0 +1,14 @@
+
+public class Break {
+
+  public static void main() {
+
+    int j = 0;
+    ++j;
+    for(int i = 0; i < 10; ++i)
+      if(i == 5) break;
+    for(j = 0; j < 10; ++j)
+      if(j == 5) break;
+  }
+
+}

regression/cbmc-java/destructor1/Break.java

@@ -0,0 +1,8 @@
+CORE
+Break.class
+--show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+dead i;
+--
+GOTO 10