Add tests for inherited static fields

These cover various permutations of static fields defined on parents, on interfaces,
and those parents and/or interfaces being opaque (stubs). They check both that
jbmc doesn't outright crash, and in some cases that jbmc correctly determines that
two static fields must be the same one, and therefore cannot differ.

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;
+
+}