Merge pull request #691 from reuk/java-nondet-new-pass

Add support for explicit nondet in java code

Author: peterschrammel

regression/cbmc-java/Makefile

@@ -23,3 +23,16 @@ clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
 	$(RM) tests.log
+
+%.class: %.java ../../src/org.cprover.jar
+	javac -g -cp ../../src/org.cprover.jar:. $<
+
+nondet_java_files := $(shell find . -name "Nondet*.java")
+nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files))
+
+.PHONY: nondet-class-files
+nondet-class-files: $(nondet_class_files)
+
+.PHONY: clean-nondet-class-files
+clean-nondet-class-files:
+	-rm $(nondet_class_files)

regression/cbmc-java/NondetArray/NondetArray.class

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetArray
+{
+  void main()
+  {
+    Object[] obj = CProver.nondetWithoutNull();
+    assert obj != null;
+  }
+}

regression/cbmc-java/NondetArray/NondetArray.java

@@ -0,0 +1,6 @@
+CORE
+NondetArray.class
+--function NondetArray.main
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/NondetArray/test.desc

@@ -0,0 +1,15 @@
+import org.cprover.CProver;
+
+class NondetArray2
+{
+  void main()
+  {
+    Integer[] ints = CProver.nondetWithoutNull();
+
+    int num = 0;
+    for (Integer i : ints) {
+      num *= i.intValue();
+    }
+    assert num == 0;
+  }
+}

regression/cbmc-java/NondetArray2/NondetArray2.class

@@ -0,0 +1,6 @@
+CORE
+NondetArray2.class
+--function NondetArray2.main --unwind 5
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/NondetArray2/NondetArray2.java

@@ -0,0 +1,16 @@
+import org.cprover.CProver;
+
+class NondetArray3
+{
+  void main()
+  {
+    Integer[] ints = CProver.nondetWithoutNull();
+    assert ints != null;
+
+    int num = 0;
+    for (Integer i : ints) {
+      num *= i.intValue();
+    }
+    assert num == 0;
+  }
+}

regression/cbmc-java/NondetArray2/test.desc

@@ -0,0 +1,6 @@
+CORE
+NondetArray3.class
+--function NondetArray3.main --unwind 5
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/NondetArray3/NondetArray3.class

@@ -0,0 +1,14 @@
+import org.cprover.CProver;
+
+class NondetArray4
+{
+  void main()
+  {
+    int a = 1;
+    int b = 2;
+    int c = 3;
+
+    Integer[] ints = CProver.nondetWithoutNull();
+    assert ints != null;
+  }
+}

regression/cbmc-java/NondetArray3/NondetArray3.java

@@ -0,0 +1,6 @@
+CORE
+NondetArray4.class
+--function NondetArray4.main
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/NondetArray3/test.desc

@@ -0,0 +1,11 @@
+import org.cprover.CProver;
+
+class NondetAssume1
+{
+  void main()
+  {
+    int x = CProver.nondetInt();
+    CProver.assume(x == 1);
+    assert x == 1;
+  }
+}

regression/cbmc-java/NondetArray4/NondetArray4.class

@@ -0,0 +1,6 @@
+CORE
+NondetAssume1.class
+--function NondetAssume1.main
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/NondetArray4/NondetArray4.java

@@ -0,0 +1,17 @@
+import org.cprover.CProver;
+
+class A { int x; }
+
+class B { A a; }
+
+class C { B b; }
+
+class NondetAssume2
+{
+  void main()
+  {
+    C c = CProver.nondetWithNull();
+    CProver.assume(c != null);
+    assert c != null;
+  }
+}

regression/cbmc-java/NondetArray4/test.desc

@@ -0,0 +1,6 @@
+CORE
+NondetAssume2.class
+--function NondetAssume2.main
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/NondetAssume1/NondetAssume1.class

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetBoolean
+{
+  static void main()
+  {
+    boolean x = CProver.nondetBoolean();
+    assert x == false;
+  }
+}

regression/cbmc-java/NondetAssume1/NondetAssume1.java

@@ -0,0 +1,6 @@
+CORE
+NondetBoolean.class
+--function NondetBoolean.main
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NondetAssume1/test.desc

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetByte
+{
+  static void main()
+  {
+    byte x = CProver.nondetByte();
+    assert x == 0;
+  }
+}

regression/cbmc-java/NondetAssume2/A.class

@@ -0,0 +1,6 @@
+CORE
+NondetByte.class
+--function NondetByte.main
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NondetAssume2/B.class

@@ -0,0 +1,11 @@
+import org.cprover.CProver;
+
+class NondetCastToObject
+{
+  void main()
+  {
+    Object o = CProver.nondetWithNull();
+    CProver.assume(o != null);
+    assert o != null;
+  }
+}

regression/cbmc-java/NondetAssume2/C.class

@@ -0,0 +1,6 @@
+CORE
+NondetCastToObject.class
+--function NondetCastToObject.main
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/NondetAssume2/NondetAssume2.class

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetChar
+{
+  static void main()
+  {
+    char x = CProver.nondetChar();
+    assert x == '\0';
+  }
+}

regression/cbmc-java/NondetAssume2/NondetAssume2.java

@@ -0,0 +1,6 @@
+CORE
+NondetChar.class
+--function NondetChar.main
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NondetAssume2/test.desc

@@ -0,0 +1,19 @@
+import org.cprover.CProver;
+
+class A
+{
+  int a;
+}
+
+class NondetDirectFromMethod
+{
+  A methodReturningA()
+  {
+    return CProver.nondetWithoutNull();
+  }
+
+  void main()
+  {
+    assert methodReturningA() != null;
+  }
+}

regression/cbmc-java/NondetBoolean/NondetBoolean.class

@@ -0,0 +1,6 @@
+CORE
+NondetDirectFromMethod.class
+--function NondetDirectFromMethod.main
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/NondetBoolean/NondetBoolean.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetDouble
+{
+  static void main()
+  {
+    double x = CProver.nondetDouble();
+    assert x == 0;
+  }
+}

regression/cbmc-java/NondetBoolean/test.desc

@@ -0,0 +1,6 @@
+CORE
+NondetDouble.class
+--function NondetDouble.main
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NondetByte/NondetByte.class

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetFloat
+{
+  static void main()
+  {
+    float x = CProver.nondetFloat();
+    assert x == 0;
+  }
+}

regression/cbmc-java/NondetByte/NondetByte.java

@@ -0,0 +1,6 @@
+CORE
+NondetFloat.class
+--function NondetFloat.main
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NondetByte/test.desc

@@ -0,0 +1,30 @@
+import org.cprover.CProver;
+
+class A
+{
+  int[] ints = new int[10];
+}
+
+class B
+{
+  A a;
+}
+
+class C
+{
+  B b;
+}
+
+class NondetGenericArray
+{
+  static void main()
+  {
+    C c = CProver.nondetWithNull();
+    CProver.assume(c != null);
+    CProver.assume(c.b != null);
+    CProver.assume(c.b.a != null);
+    CProver.assume(c.b.a.ints != null);
+    assert c.b.a != null;
+    assert c.b.a.ints != null;
+  }
+}

regression/cbmc-java/NondetCastToObject/NondetCastToObject.class

@@ -0,0 +1,6 @@
+CORE
+NondetGenericArray.class
+--function NondetGenericArray.main
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/NondetCastToObject/NondetCastToObject.java

@@ -0,0 +1,24 @@
+import org.cprover.CProver;
+
+class A
+{
+}
+
+class B
+{
+  A a;
+}
+
+class C
+{
+  B b;
+}
+
+class NondetGenericRecursive
+{
+  static void main()
+  {
+    C c = CProver.nondetWithNull();
+    assert c == null;
+  }
+}

regression/cbmc-java/NondetCastToObject/test.desc

@@ -0,0 +1,6 @@
+CORE
+NondetGenericRecursive.class
+--function NondetGenericRecursive.main
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NondetChar/NondetChar.class

@@ -0,0 +1,27 @@
+import org.cprover.CProver;
+
+class A
+{
+}
+
+class B
+{
+  A a;
+}
+
+class C
+{
+  B b;
+}
+
+class NondetGenericRecursive2
+{
+  static void main()
+  {
+    C c = CProver.nondetWithNull();
+    CProver.assume(c != null);
+    CProver.assume(c.b != null);
+    CProver.assume(c.b.a != null);
+    assert c.b.a != null;
+  }
+}

regression/cbmc-java/NondetChar/NondetChar.java

@@ -0,0 +1,6 @@
+CORE
+NondetGenericRecursive2.class
+--function NondetGenericRecursive2.main
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring