JBMC: Renamed root class component 'monitorCount' to 'cproverMonitorCount'

Author: Degiorgio

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1072,9 +1072,9 @@ void java_object_factoryt::gen_nondet_struct_init(
     {
       continue;
     }
-    else if(name == "monitorCount")
+    else if(name == "cproverMonitorCount")
     {
-      // Zero-initialize 'monitorCount' field as it is not meant to be nondet.
+      // Zero-initialize 'cproverMonitorCount' field as it is not meant to be nondet.
       // This field is only present when the java core models are embedded. It
       // is used to implement a critical section, which is necessary to support
       // concurrency.

jbmc/src/java_bytecode/java_root_class.cpp

@@ -52,13 +52,14 @@ void java_root_class_init(
   constant_exprt clsid(class_identifier, clsid_type);
   jlo.operands()[clsid_nb]=clsid;
 
-  // Check if the 'monitorCount' component exists and initialize it.
+  // Check if the 'cproverMonitorCount' component exists and initialize it.
   // This field is only present when the java core models are embedded. It is
   // used to implement a critical section, which is necessary to support
   // concurrency.
-  if(root_type.has_component("monitorCount"))
+  if(root_type.has_component("cproverMonitorCount"))
   {
-    const std::size_t count_nb = root_type.component_number("monitorCount");
+    const std::size_t count_nb =
+      root_type.component_number("cproverMonitorCount");
     const typet &count_type = root_type.components()[count_nb].type();
     jlo.operands()[count_nb] = from_integer(0, count_type);
   }