Add MustNotThrow annotations to Class.java in tests

These are cut-down versions of the model for java.lang.Class. The
methods that are kept are now marked MustNotThrow in the model, so
that exception-handling code isn't generated in __CPROVER_initialize.
We should therefore update the cut-down versions.

Author: Owen

jbmc/regression/jbmc/class-fields/java/lang/Class.class

@@ -4,6 +4,7 @@ public class Class {
 
   public Integer field;
 
+  @org.cprover.MustNotThrow
   protected void cproverNondetInitialize() {
     org.cprover.CProver.assume(field == null);
   }

jbmc/regression/jbmc/class-fields/java/lang/Class.java

@@ -0,0 +1,15 @@
+package org.cprover;
+
+public final class CProver
+{
+  public static final boolean enableAssume=true;
+
+  public static void assume(boolean condition)
+  {
+    if(enableAssume)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.assume()");
+    }
+  }
+}

jbmc/regression/jbmc/class-fields/org/cprover/CProver.class

@@ -0,0 +1,8 @@
+package org.cprover;
+
+/**
+ * This can be added to methods to indicate they aren't allowed to throw
+ * exceptions. JBMC and related tools will truncate any execution path on which
+ * they do with an ASSUME FALSE instruction.
+ */
+public @interface MustNotThrow { }

jbmc/regression/jbmc/class-fields/org/cprover/CProver.java

@@ -12,6 +12,7 @@ public class Class {
   private boolean isMemberClass;
   private boolean isEnum;
 
+  @org.cprover.MustNotThrow
   public void cproverInitializeClassLiteral(
     String name,
     boolean isAnnotation,

jbmc/regression/jbmc/class-fields/org/cprover/MustNotThrow.class

@@ -0,0 +1,15 @@
+package org.cprover;
+
+public final class CProver
+{
+  public static final boolean enableAssume=true;
+
+  public static void assume(boolean condition)
+  {
+    if(enableAssume)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.assume()");
+    }
+  }
+}

jbmc/regression/jbmc/class-fields/org/cprover/MustNotThrow.java

@@ -0,0 +1,8 @@
+package org.cprover;
+
+/**
+ * This can be added to methods to indicate they aren't allowed to throw
+ * exceptions. JBMC and related tools will truncate any execution path on which
+ * they do with an ASSUME FALSE instruction.
+ */
+public @interface MustNotThrow { }