Merge pull request #2486 from Degiorgio/jbmc-synchronoization-asymmetry-fix

JBMC: Fixed asymmetry between synchronized blocks and methods.

Author: Thomas Kiley

jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class

@@ -14,6 +14,25 @@ public void me0()
     }
   }
 
+  // expected verification success
+  public static void aStatic() throws java.io.IOException
+  {
+    Object _lock = new Object();
+    try
+    {
+      synchronized (_lock)
+      {
+        if(true)
+          throw new java.io.IOException();
+      }
+    }
+    catch (java.io.IOException e)
+    {
+      return;
+    }
+    assert false; // unreachable
+  }
+
   // expected verification success
   // --
   // base-case, no synchronization

jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
+--function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading
 ATOMIC_BEGIN
 ATOMIC_END
 --

jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc

@@ -0,0 +1,10 @@
+CORE
+A.class
+--function 'A.aStatic' --lazy-methods
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that throwing an exception from a synchronization blocks does not cause reachability issues when the java-threading flag is not specified.
+