Merge pull request #2280 from cesaro/java-concurrency-synchronization

Java threading: support for synchronization

Author: cesaro

appveyor.yml

@@ -18,6 +18,7 @@ install:
     Move-Item win_flex.exe bin\flex.exe -force
     Move-Item FlexLexer.h include\FlexLexer.h -force
     Remove-Item bin\data -Force -Recurse -ErrorAction SilentlyContinue
+    Remove-Item java-models-library-master -Force -Recurse -ErrorAction SilentlyContinue
     Move-Item data bin\data -force
     bison -V
     flex -V
@@ -90,7 +91,6 @@ test_script:
     rmdir /s /q jbmc\classpath1
     rmdir /s /q jbmc\jar-file3
     rmdir /s /q jbmc\tableswitch2
-    rmdir /s /q jbmc-concurrency\explicit_thread_blocks
     cd ../..
 
     make -C jbmc/regression test

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$1.class

@@ -0,0 +1,39 @@
+import java.lang.Thread;
+import org.cprover.CProver;
+
+public class A
+{
+  int x = 0;
+
+  // expected verfication success
+  public void me()
+  {
+    Thread t = new Thread()
+    {
+      public void run()
+      {
+        x = 44;
+        int local_x = x;
+        assert(local_x == 44 || x == 10);
+      }
+    };
+    t.start();
+    x = 10;
+  }
+
+  // expected verfication failure
+  public void me2()
+  {
+    Thread t = new Thread()
+    {
+      public void run()
+      {
+        x = 44;
+        int local_x = x;
+        assert(local_x == 44);
+      }
+    };
+    t.start();
+    x = 10;
+  }
+}

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$2.class

@@ -0,0 +1,6 @@
+CORE
+A.class
+--function 'A.me:()V' --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/anonymous-java.lang.thread/A.class

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

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.java

@@ -1,7 +1,6 @@
 CORE
 A.class
---function "A.me:()V" --lazy-methods --java-threading
-
+--function 'A.me:()V' --lazy-methods --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL