From 9b82c978dee1a6a9bcdde0c76394615b66f87164 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Mon, 25 Jul 2016 16:21:30 +0200 Subject: [PATCH] skitp monitorenter / monitorexit Thread synchronization is currently not supported in Java. Emit warning upon entering a critical section which is marked by `monitorenter`, simply skip `monitorexit`. --- src/java_bytecode/java_bytecode_convert_method.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 2f1e822dbbc..f14c0bca716 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1349,6 +1349,13 @@ codet java_bytecode_convert_methodt::convert_instructions( results[0]= binary_predicate_exprt(op[0], "java_instanceof", arg0); } + else if(statement=="monitorenter") + warning() << "critical section with lock object is ignored (" + << i_it->source_location << ")" << eom; + else if(statement=="monitorexit") + // just skip, is always preceeded with "monitorenter" + { + } else { c=codet(statement);