Object factory: permit null pointers within java.lang.Class

This is in fact required by the Deeptest models library, and is generally sensible if we don't
know whether or not a particular implementation of java.lang.Class should or should not be able
to store null in any particular field. If you're running an implementation that requires them
not null, add a cproverNondetInitialize function to that effect.

This was blocking using implementations that expect a null value from passing initialization.

Author: smowton

jbmc/regression/jbmc/class-fields/Test.class

@@ -0,0 +1,10 @@
+public class Test {
+
+  public static void main() {
+
+    java.lang.Class c = Test.class;
+    assert false;
+
+  }
+
+}

jbmc/regression/jbmc/class-fields/Test.java

@@ -0,0 +1,11 @@
+package java.lang;
+
+public class Class {
+
+  public Integer field;
+
+  protected void cproverNondetInitialize() {
+    org.cprover.CProver.assume(field == null);
+  }
+
+}

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

@@ -0,0 +1,9 @@
+CORE
+Test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Test\.java line 6.*: FAILURE$
+--
+^warning: ignoring

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

@@ -94,11 +94,6 @@ static void java_static_lifetime_init(
         if(allow_null)
         {
           irep_idt nameid=sym.symbol_expr().get_identifier();
-          std::string namestr=id2string(nameid);
-          const std::string suffix="@class_model";
-          // Static '.class' fields are always non-null.
-          if(has_suffix(namestr, suffix))
-            allow_null=false;
           if(allow_null && is_java_string_literal_id(nameid))
             allow_null=false;
           if(allow_null && is_non_null_library_global(nameid))

jbmc/regression/jbmc/class-fields/test.desc

@@ -874,10 +874,6 @@ void java_object_factoryt::gen_nondet_pointer_init(
 
   auto set_null_inst=get_null_assignment(expr, pointer_type);
 
-  // Determine whether the pointer can be null. In particular the pointers
-  // inside the java.lang.Class class shall not be null
-  const bool not_null = !allow_null || class_identifier == "java.lang.Class";
-
   // Alternatively, if this is a void* we *must* initialise with null:
   // (This can currently happen for some cases of #exception_value)
   bool must_be_null=
@@ -889,7 +885,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
     // <expr> = nullptr;
     new_object_assignments.add(set_null_inst);
   }
-  else if(not_null)
+  else if(!allow_null)
   {
     // Add the following code to assignments:
     // <expr> = <aoe>;