Fix allow-null initialization logic for class models

@class_model.name must be non-null whereas
@class_mode.table must be null. These constraints are
enforced in the models library. The generic nondet-
initialisation must use allow-null for these constraints
to take effect correctly.

Author: peterschrammel

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -210,18 +210,18 @@ static void java_static_lifetime_init(
       }
       else if(sym.value.is_nil() && sym.type!=empty_typet())
       {
-        bool allow_null=!assume_init_pointers_not_null;
-        if(allow_null)
-        {
-          irep_idt nameid=sym.symbol_expr().get_identifier();
-          if(allow_null && is_java_string_literal_id(nameid))
-            allow_null=false;
-          if(allow_null && is_non_null_library_global(nameid))
-            allow_null = false;
-        }
+        irep_idt nameid = sym.symbol_expr().get_identifier();
+        const bool is_class_model =
+          has_suffix(id2string(nameid), "@class_model");
         object_factory_parameterst parameters = object_factory_parameters;
-        if(!allow_null)
+        if(
+          !is_class_model &&
+          (is_java_string_literal_id(nameid) ||
+           is_non_null_library_global(nameid) || assume_init_pointers_not_null))
+        {
+          // do not allow null
           parameters.max_nonnull_tree_depth = 1;
+        }
 
         gen_nondet_init(
           sym.symbol_expr(),