Add org.cprover package and makefile

Author: reuk

src/java_bytecode/library/Makefile

@@ -0,0 +1,26 @@
+all: org.cprover.jar
+
+SOURCE_DIR := src
+BINARY_DIR := classes
+
+FIND := find
+
+JAVAC := javac
+JFLAGS := -sourcepath $(SOURCE_DIR) -d $(BINARY_DIR)
+
+CLASSPATH := SOURCE_DIR
+
+all_javas := $(shell $(FIND) $(SOURCE_DIR) -name '*.java')
+
+$(BINARY_DIR):
+	mkdir -p $(BINARY_DIR)
+
+.PHONY: compile
+compile: $(BINARY_DIR)
+	$(JAVAC) $(JFLAGS) $(all_javas)
+
+JAR := jar
+JARFLAGS := -cf
+
+org.cprover.jar: compile
+	$(JAR) $(JARFLAGS) $@ -C $(BINARY_DIR) org

src/java_bytecode/library/src/org/cprover/CProver.java

@@ -3,9 +3,124 @@
 public final class CProver
 {
   public static boolean enableAssume=true;
-  public static void assume(boolean condition) 
+  public static boolean enableNondet=true;
+
+  public static boolean nondetBoolean()
+  {
+    if (enableNondet)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.nondetBoolean()");
+    }
+
+    return false;
+  }
+
+  public static byte nondetByte()
+  {
+    if (enableNondet)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.nondetByte()");
+    }
+
+    return 0;
+  }
+
+  public static char nondetChar()
+  {
+    if (enableNondet)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.nondetChar()");
+    }
+
+    return '\0';
+  }
+
+  public static short nondetShort()
+  {
+    if (enableNondet)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.nondetShort()");
+    }
+
+    return 0;
+  }
+
+  public static int nondetInt()
+  {
+    if (enableNondet)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.nondetInt()");
+    }
+
+    return 0;
+  }
+
+  public static long nondetLong()
+  {
+    if (enableNondet)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.nondetLong()");
+    }
+
+    return 0;
+  }
+
+  public static float nondetFloat()
+  {
+    if (enableNondet)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.nondetFloat()");
+    }
+
+    return 0;
+  }
+
+  public static double nondetDouble()
+  {
+    if (enableNondet)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.nondetDouble()");
+    }
+
+    return 0;
+  }
+
+  public static <T> T nondetWithNull()
+  {
+    if (enableNondet)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.nondetWithNull<T>(T)");
+    }
+
+    return null;
+  }
+
+  public static <T> T nondetWithoutNull()
+  {
+    if (enableNondet)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.nondetWithoutNull<T>(T)");
+    }
+
+    return null;
+  }
+
+  public static void assume(boolean condition)
   {
     if(enableAssume)
-      throw new RuntimeException("Cannot execute program with CProver.assume()");
-  }  
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.assume()");
+    }
+  }
 }