Add tests for inheritance of cproverNondetInitialize

Author: owen-mc-diffblue

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/A.class

@@ -0,0 +1,68 @@
+import org.cprover.CProver;
+
+class A {
+  int x;
+
+  public void cproverNondetInitialize() { CProver.assume(x == 42); }
+}
+
+class B extends A {}
+
+class C extends B {}
+
+class F extends A {
+  public void cproverNondetInitialize() {}
+}
+
+interface I {
+}
+
+class J extends A implements I {
+}
+
+class K extends A {
+  int y;
+
+  public void cproverNondetInitialize() {
+    super.cproverNondetInitialize();
+    CProver.assume(y == 6);
+  }
+}
+
+abstract class M {
+  int x;
+
+  public void cproverNondetInitialize() { CProver.assume(x == 42); }
+}
+
+class N extends M {}
+
+public class Test {
+
+  void inheritanceTwoLevels(C c) {
+    if (c != null)
+      assert (c.x == 42);
+  }
+
+  void override(F f) {
+    if (f != null)
+      assert (f.x == 42);
+  }
+
+  void callingSuperCproverNondetInitialize(K k) {
+    if (k != null) {
+      assert (k.x == 42);
+      assert (k.y == 6);
+    }
+  }
+
+  void inheritanceFromAbstractClass(N n) {
+    if (n != null)
+      assert (n.x == 42);
+  }
+
+  void alsoImplementsInterface(J j) {
+    if (j != null)
+        assert (j.x == 42);
+    }
+}

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/B.class

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.alsoImplementsInterface --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that if J extends A and implements the interface I,
+J.cproverNondetInitialize doesn't exist and A.cproverNondetInitialize does then
+a nondet J gets the constraints specified in A.cproverNondetInitialize.

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/C.class

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.callingSuperCproverNondetInitialize --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that calls to super.cproverNondetInitialize call cproverNondetInitialize
+in the base class.

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/F.class

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.inheritanceFromAbstractClass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that if N extends the abstract class M, N.cproverNondetInitialize doesn't
+exist and M.cproverNondetInitialize does and is defined then a
+nondet N gets the constraints specified in M.cproverNondetInitialize.

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/I.class

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.inheritanceTwoLevels --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that if C extends B, B extends A, B.cproverNondetInitialize and
+C.cproverNondetInitialize don't exist and A.cproverNondetInitialize does then a
+nondet C gets the constraints specified in A.cproverNondetInitialize.

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/J.class

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.override --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Check that if F extends A, and A.cproverNondetInitialize and
+F.cproverNondetInitialize both exist then a nondet F doesn't get the constraint
+specified in A.cproverNondetInitialize. Specifically, it doesn't get the
+constraint that x must be 42, so when we assert that x is 42 jbmc is able to
+falsify it.