Merge pull request #186 from mgudemann/skip_monitorenter_exit_instruction

Daniel Kroening · web-flow · commit d7bcd083b0e3 · 2016-07-25T15:27:55.000+01:00
skip monitorenter / monitorexit
diff --git 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);

Original file line number	Diff line number	Diff line change
`@@ -1349,6 +1349,13 @@ codet java_bytecode_convert_methodt::convert_instructions(`
`1349`	`1349`	`results[0]=`
`1350`	`1350`	`binary_predicate_exprt(op[0], "java_instanceof", arg0);`
`1351`	`1351`	`}`
	`1352`	`+ else if(statement=="monitorenter")`
	`1353`	`+ warning() << "critical section with lock object is ignored ("`
	`1354`	`+ << i_it->source_location << ")" << eom;`
	`1355`	`+ else if(statement=="monitorexit")`
	`1356`	`+ // just skip, is always preceeded with "monitorenter"`
	`1357`	`+ {`
	`1358`	`+ }`
`1352`	`1359`	`else`
`1353`	`1360`	`{`
`1354`	`1361`	`c=codet(statement);`