add Java monitorenter/exit symbols

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -15,8 +15,36 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/c_types.h>
 
+#include "java_types.h"
+
 void java_internal_additions(symbol_table_baset &dest)
 {
+  // add monitorenter
+
+  {
+    code_typet type(
+      {code_typet::parametert(java_lang_object_type())}, void_typet());
+    symbolt symbol;
+    symbol.base_name = "monitorenter";
+    symbol.name = "java::monitorenter";
+    symbol.type = type;
+    symbol.mode = ID_java;
+    dest.add(symbol);
+  }
+
+  // add monitorexit
+
+  {
+    code_typet type(
+      {code_typet::parametert(java_lang_object_type())}, void_typet());
+    symbolt symbol;
+    symbol.base_name = "monitorexit";
+    symbol.name = "java::monitorexit";
+    symbol.type = type;
+    symbol.mode = ID_java;
+    dest.add(symbol);
+  }
+
   // add __CPROVER_rounding_mode
 
   {