Merge pull request #1826 from smowton/smowton/fix/java-inherited-static-fields

Add support for inheritence of Java static fields. Fixes TG-2457

Author: smowton

regression/cbmc-java/inherited_static_field1/Parent.class

@@ -0,0 +1,16 @@
+public class Test extends Parent {
+
+  public static void main(int nondet) {
+
+    x = nondet;
+    assert x == Parent.x;
+
+  }
+
+}
+
+class Parent {
+
+  public static int x;
+
+}

regression/cbmc-java/inherited_static_field1/Test.class

@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^VERIFICATION SUCCESSFUL$
+--
+--
+This checks that jbmc knows that test.x and parent.x refer to the same field.
+Both test and parent are concrete (available) classes.

regression/cbmc-java/inherited_static_field1/Test.java

@@ -0,0 +1,9 @@
+
+public class Parent {
+
+  // This is the version of Parent we will run jbmc against, which has
+  // a static field 'x', but that field is private and cannot correspond
+  // to the reference 'Test.x'.
+  private static int x;
+
+}

regression/cbmc-java/inherited_static_field1/test.desc

@@ -0,0 +1,10 @@
+public class Test extends Parent {
+
+  public static void main(int nondet) {
+
+    x = nondet;
+    assert x == Parent.x;
+
+  }
+
+}

regression/cbmc-java/inherited_static_field10/Parent.class

@@ -0,0 +1,8 @@
+
+public class Parent {
+
+  // This is the version of Parent we compile Test.java against, which does
+  // have a static field 'x'.
+  public static int x;
+
+}