Mark tests failing on Windows as KNOWNBUG

tautschnig · tautschnig · commit 00bdd8722762 · 2018-12-29T21:14:42.000Z
All 35 fail with

File: arith_tools.cpp:196 function: from_integer
Condition: false
Reason: Precondition
diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me:()V' --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me:()V'  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test.desc b/jbmc/regression/jbmc-concurrency/several-threads/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function A.me --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test2.desc b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test3.desc b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function A.me3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading --unwind 3
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions --java-threading
 ATOMIC_BEGIN
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Sync.class
 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized/test.desc b/jbmc/regression/jbmc-concurrency/synchronized/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Sync.class
 --java-threading --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init1/test1.desc b/jbmc/regression/jbmc/static_init1/test1.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 static_init.class
 --function static_init.main --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init2/test1.desc b/jbmc/regression/jbmc/static_init2/test1.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 static_init.class
 --function static_init.main --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init_order/test3.desc b/jbmc/regression/jbmc/static_init_order/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 static_init_order.class
 --function static_init_order.test1 --trace --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init_order/test4.desc b/jbmc/regression/jbmc/static_init_order/test4.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 static_init_order.class
 --function static_init_order.test2 --java-threading
 ^EXIT=10$

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+KNOWNBUG`
`2`	`2`	`A.class`
`3`	`3`	--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
`4`	`4`	`^VERIFICATION SUCCESSFUL$`