add Java monitorenter/exit symbols

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -15,8 +15,42 @@ 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;
+    type.return_type() = void_typet();
+    type.parameters().resize(1);
+    type.parameters()[0].type() = java_reference_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;
+    type.return_type() = void_typet();
+    type.parameters().resize(1);
+    type.parameters()[0].type() = java_reference_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
 
   {