JBMC: Regression tests for multi-threaded java programs

Author: Degiorgio

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

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc

@@ -0,0 +1,5 @@
+CORE
+A.class
+--function 'A.me2:()V' --lazy-methods --java-threading
+^SIGNAL=0$
+^VERIFICATION FAILED