Add tests for local variable live ranges with holes

Both of these feature local variables that are declared in the class file LVT with two or more live ranges, because of initialisation by a try/catch or the cases of a switch statement. The tests assert that the initialisation is as expected, to catch cases where the two live ranges are erroneously treated seperately and so the variable read in the assertion is an effective nondet.

Author: smowton

regression/cbmc-java/LocalVarTable3/live_range_with_holes.class

@@ -0,0 +1,26 @@
+
+public class live_range_with_holes {
+
+  public static void main(int arg) {
+
+    int x;
+    int y;
+    switch(arg) {
+      case 1:
+        x = 1;
+        y = 1;
+        break;
+      case 2:
+        x = 2;
+        y = 2;
+        break;
+      default:
+        x = 0;
+        y = 0;
+        break;
+    }
+    assert(x >= 0 && x <= 2);
+
+  }
+
+}

regression/cbmc-java/LocalVarTable3/live_range_with_holes.java

@@ -0,0 +1,7 @@
+CORE
+live_range_with_holes.class
+--function live_range_with_holes.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc-java/LocalVarTable3/test.desc

@@ -0,0 +1,18 @@
+
+public class live_range_exception {
+  public static void main() {
+    int x;
+    int y;
+    try
+    {
+      x = 0;
+      y = 0;
+    }
+    catch(Exception e)
+    {
+      x = 1;
+      y = 1;
+    }
+    assert(x==0 || x==1);
+  }
+}

regression/cbmc-java/LocalVarTable4/live_range_exception.class

@@ -0,0 +1,7 @@
+CORE
+live_range_exception.class
+--function live_range_exception.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--