Java nondet test gen support

regression/cbmc-java/Makefile

@@ -18,3 +18,16 @@ show:
 			vim -o "$$dir/*.java" "$$dir/*.out"; \
 		fi; \
 	done;
+
+%.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/nondetAssume1/NondetAssume1.java

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

regression/cbmc-java/nondetAssume1/test.desc

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

regression/cbmc-java/nondetAssume2/NondetAssume2.java

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

regression/cbmc-java/nondetAssume2/test.desc

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

regression/cbmc-java/nondetBoolean/NondetBoolean.java

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

regression/cbmc-java/nondetBoolean/test.desc

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

regression/cbmc-java/nondetByte/NondetByte.java

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

regression/cbmc-java/nondetByte/test.desc

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

regression/cbmc-java/nondetCastToObject/NondetCastToObject.java

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

regression/cbmc-java/nondetCastToObject/test.desc

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

regression/cbmc-java/nondetChar/NondetChar.java

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

regression/cbmc-java/nondetChar/test.desc

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

regression/cbmc-java/nondetDouble/NondetDouble.java

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

regression/cbmc-java/nondetDouble/test.desc

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

regression/cbmc-java/nondetFloat/NondetFloat.java

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

regression/cbmc-java/nondetFloat/test.desc

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

regression/cbmc-java/nondetGenericArray/NondetGenericArray.java

@@ -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 foo()
+  {
+    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/nondetGenericArray/test.desc

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

regression/cbmc-java/nondetGenericRecursive/NondetGenericRecursive.java

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

regression/cbmc-java/nondetGenericRecursive/test.desc

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

regression/cbmc-java/nondetGenericRecursive2/NondetGenericRecursive2.java

@@ -0,0 +1,27 @@
+import org.cprover.CProver;
+
+class A
+{
+}
+
+class B
+{
+  A a;
+}
+
+class C
+{
+  B b;
+}
+
+class NondetGenericRecursive2
+{
+  static void foo()
+  {
+    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/nondetGenericRecursive2/test.desc

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

regression/cbmc-java/nondetGenericWithNull/NondetGenericWithNull.java

@@ -0,0 +1,13 @@
+import org.cprover.CProver;
+
+class B { int a; }
+
+class NondetGenericWithNull
+{
+  static void foo()
+  {
+    B b = CProver.nondetWithNull();
+    assert b != null;
+    assert b.a != 0;
+  }
+}

regression/cbmc-java/nondetGenericWithNull/test.desc

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

regression/cbmc-java/nondetInt/NondetInt.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetInt
+{
+  static void foo()
+  {
+    int x = CProver.nondetInt();
+    assert x == 0;
+  }
+}

regression/cbmc-java/nondetInt/test.desc

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

regression/cbmc-java/nondetLong/NondetLong.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetLong
+{
+  static void foo()
+  {
+    long x = CProver.nondetLong();
+    assert x == 0;
+  }
+}

regression/cbmc-java/nondetLong/test.desc

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

regression/cbmc-java/nondetShort/NondetShort.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetShort
+{
+  static void foo()
+  {
+    short x = CProver.nondetShort();
+    assert x == 0;
+  }
+}

regression/cbmc-java/nondetShort/test.desc

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

src/goto-programs/goto_convert.cpp

@@ -6,6 +6,10 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#ifdef DEBUG
+#include <iostream>
+#endif
+
 #include <cassert>
 
 #include <util/cprover_prefix.h>
@@ -905,6 +909,7 @@ void goto_convertt::convert_assign(
 
     copy(new_assign, ASSIGN, dest);
   }
+
   else
   {
     clean_expr(rhs, dest);

src/goto-programs/goto_convert_side_effect.cpp

@@ -6,6 +6,10 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#ifdef DEBUG
+#include <iostream>
+#endif
+
 #include <util/arith_tools.h>
 #include <util/expr_util.h>
 #include <util/std_expr.h>