Merge pull request #442 from smowton/add_lvt_tests

Add tests for local variable live ranges with holes

Author: Daniel Kroening

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$
+--