Adding regression tests showing the modified gen code works

The nondet generation code has been modified to select a concrete
subtype when given an abstract type. These tests verify these cases are
correctly generated.

Author: thk123

regression/cbmc-java/instance-method-user-interface-field/A.class

@@ -0,0 +1,44 @@
+interface I
+{
+    int getANumber();
+}
+
+class A implements I {
+    public int a;
+
+    public int getANumber() { return a; }
+}
+
+class B implements I {
+    public int b;
+    public int getANumber() { return b; }
+}
+
+class TestClass
+{
+    public I someObject;
+
+    public boolean foo() {
+        if(someObject!=null)
+        {
+            int result = someObject.getANumber();
+            if(result == 42) {
+                return true;
+            } else {
+                return false;
+            }
+        }
+        else
+        {
+            return false;
+        }
+    }
+
+    public static void main(String[] args)
+    {
+        // ensure that A, B are referenced explicitly
+        // in order to get them converted into GOTO
+        A a = new A();
+        B b = new B();
+    }
+}

regression/cbmc-java/instance-method-user-interface-field/B.class

@@ -0,0 +1,6 @@
+CORE
+TestClass.class
+--cover location --function TestClass.foo --show-goto-functions
+
+\.someObject = \(struct I \*\)\w+
+@class_identifier = "java::A";

regression/cbmc-java/instance-method-user-interface-field/I.class

@@ -0,0 +1,61 @@
+interface I
+{
+    int getANumber();
+}
+
+class A implements I {
+    public int a;
+
+    public int getANumber() { return a; }
+}
+
+class B implements I {
+    public int b;
+    public int getANumber() { return b; }
+}
+
+interface J
+{
+    int getANumber();
+}
+
+class C implements J {
+    public int c;
+    public int getANumber() { return c; }
+}
+
+class D implements J {
+    public int d;
+    public int getANumber() { return d; }
+}
+
+class TestClass
+{
+    public I someObject1;
+    public J someObject2;
+
+    public boolean foo() {
+        if(someObject1 != null && someObject2 != null)
+        {
+            if(someObject1.getANumber() == someObject2.getANumber()) {
+                return true;
+            } else {
+                return false;
+            }
+        }
+        else
+        {
+            return false;
+        }
+    }
+
+    public static void main(String[] args)
+    {
+        // ensure that A, B, C, D are referenced explicitly
+        // in order to get them converted into GOTO
+        A a = new A();
+        B b = new B();
+        C c = new C();
+        D d = new D();
+    }
+}

regression/cbmc-java/instance-method-user-interface-field/TestClass.class

@@ -0,0 +1,8 @@
+CORE
+TestClass.class
+--cover location --function TestClass.foo --show-goto-functions
+
+@class_identifier = "java::A";
+@class_identifier = "java::C";
+.someObject1 = \(struct I \*\)
+.someObject2 = \(struct J \*\)

regression/cbmc-java/instance-method-user-interface-field/TestClass.java

@@ -0,0 +1,42 @@
+interface I
+{
+    int getANumber();
+}
+
+class A implements I {
+    public int a;
+
+    public int getANumber() { return a; }
+}
+
+class B implements I {
+    public int b;
+    public int getANumber() { return b; }
+}
+
+class TestClass
+{
+    public static boolean foo(I someObject) {
+        if(someObject!=null)
+        {
+            int result = someObject.getANumber();
+            if(result == 42) {
+                return true;
+            } else {
+                return false;
+            }
+        }
+        else
+        {
+            return false;
+        }
+    }
+
+    public static void main(String[] args)
+    {
+        // ensure that A, B are referenced explicitly
+        // in order to get them converted into GOTO
+        A a = new A();
+        B b = new B();
+    }
+}

regression/cbmc-java/instance-method-user-interface-field/test.desc

@@ -0,0 +1,7 @@
+CORE
+TestClass.class
+--cover location --function TestClass.foo --show-goto-functions
+
+@class_identifier = "java::A";
+ = \(struct I \*\)
+tmp_object_factory\$\d+ = null;

regression/cbmc-java/instance-method-user-interface-two-fields-different/A.class

@@ -0,0 +1,57 @@
+interface I
+{
+    int getANumber();
+}
+
+class A implements I {
+    public int a;
+    public int getANumber() { return a; }
+}
+
+class B implements I {
+    public int b;
+    public int getANumber() { return b; }
+}
+
+interface J
+{
+    int getANumber();
+}
+
+class C implements J {
+    public int c;
+    public int getANumber() { return c; }
+}
+
+class D implements J {
+    public int d;
+    public int getANumber() { return d; }
+}
+
+class TestClass
+{
+    public static boolean foo(I someObject1, J someObject2) {
+        if(someObject1 != null && someObject2 != null)
+        {
+            if(someObject1.getANumber() == someObject2.getANumber()) {
+                return true;
+            } else {
+                return false;
+            }
+        }
+        else
+        {
+            return false;
+        }
+    }
+
+    public static void main(String[] args)
+    {
+        // ensure that A, B, C, D are referenced explicitly
+        // in order to get them converted into GOTO
+        A a = new A();
+        B b = new B();
+        C c = new C();
+        D d = new D();
+    }
+}

regression/cbmc-java/instance-method-user-interface-two-fields-different/B.class

@@ -0,0 +1,9 @@
+CORE
+TestClass.class
+--cover location --function TestClass.foo --show-goto-functions
+
+@class_identifier = "java::A";
+ = \(struct I \*\)
+@class_identifier = "java::C";
+ = \(struct J \*\)
+tmp_object_factory\$\d+ = null;

regression/cbmc-java/instance-method-user-interface-two-fields-different/C.class

@@ -0,0 +1,41 @@
+interface I
+{
+    int getANumber();
+}
+
+class A implements I {
+    public int a;
+
+    public int getANumber() { return a; }
+}
+
+class B implements I {
+    public int b;
+    public int getANumber() { return b; }
+}
+
+class TestClass
+{
+    public static boolean foo(I someObject1, I someObject2) {
+        if(someObject1 != null && someObject2 != null)
+        {
+            if(someObject1.getANumber() == someObject2.getANumber()) {
+                return true;
+            } else {
+                return false;
+            }
+        }
+        else
+        {
+            return false;
+        }
+    }
+
+    public static void main(String[] args)
+    {
+        // ensure that A, B are referenced explicitly
+        // in order to get them converted into GOTO
+        A a = new A();
+        B b = new B();
+    }
+}

regression/cbmc-java/instance-method-user-interface-two-fields-different/D.class

@@ -0,0 +1,7 @@
+CORE
+TestClass.class
+--cover location --function TestClass.foo --show-goto-functions
+
+@class_identifier = "java::A";
+ = \(struct I \*\)
+tmp_object_factory\$\d+ = null;