Select concrete class for abstract types

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

@@ -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/test.desc

@@ -0,0 +1,5 @@
+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-two-fields-different/TestClass.java

@@ -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-two-fields-different/test.desc

@@ -0,0 +1,7 @@
+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/static-method-user-interface-param/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/static-method-user-interface-param/test.desc

@@ -0,0 +1,6 @@
+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/static-method-user-interface-two-params-different/TestClass.java

@@ -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/static-method-user-interface-two-params-different/test.desc

@@ -0,0 +1,8 @@
+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/static-method-user-interface-two-params-same/TestClass.java

@@ -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/static-method-user-interface-two-params-same/test.desc

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

regression/strings-smoke-tests/jsonArrays/test.desc

@@ -3,7 +3,7 @@ test.class
 --refine-strings --function test.check --json-ui --trace --string-max-length 100 --cover location
 ^EXIT=0$
 ^SIGNAL=0$
-\"data\".*\"tmp_object_factory\$6.*\"
+\"data\".*\"tmp_object_factory\$\d+.*\"
 --
 This checks that tmp_object_factory$6 gets affected to the data field
 of some strings, which was not the case in previous versions of cbmc,

src/java_bytecode/Makefile

@@ -2,6 +2,7 @@ SRC = bytecode_info.cpp \
       character_refine_preprocess.cpp \
       ci_lazy_methods.cpp \
       expr2java.cpp \
+      get_concrete_class_alphabetically.cpp \
       jar_file.cpp \
       java_bytecode_convert_class.cpp \
       java_bytecode_convert_method.cpp \
@@ -24,6 +25,7 @@ SRC = bytecode_info.cpp \
       java_string_library_preprocess.cpp \
       java_types.cpp \
       java_utils.cpp \
+      select_pointer_type.cpp \
       # Empty last line
 
 INCLUDES= -I ..