Add java address space limits tests

Author: peterschrammel

regression/cbmc-java/address_space_size_limit1/Test.class

@@ -0,0 +1,13 @@
+public class Test {
+    int x;
+    Test(int x) { this.x = x; }
+
+    public static void main(String[] args) {
+        int i;
+        Test[] tests = new Test[30];
+        for(i = 0; i < 30; ++i) {
+            tests[i] = new Test(i);
+        }
+        assert i == tests[0].x;
+    }
+}

regression/cbmc-java/address_space_size_limit1/Test.java

@@ -0,0 +1,5 @@
+CORE
+Test.class
+--object-bits 4
+too many addressed objects
+--

regression/cbmc-java/address_space_size_limit1/test.desc

@@ -0,0 +1,13 @@
+public class Test {
+    int x;
+    Test(int x) { this.x = x; }
+
+    public static void main(String[] args) {
+        int i;
+        Test[] tests = new Test[30];
+        for(i = 0; i < 30; ++i) {
+            tests[i] = new Test(i);
+        }
+        assert i == tests[0].x;
+    }
+}

regression/cbmc-java/address_space_size_limit2/Test.class

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--object-bits 8
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[java::Test.main:\(\[Ljava/lang/String;\)V.assertion.1\] .*: FAILURE$
+--