diffblue · tautschnig · Dec 31, 2018 · Dec 28, 2018 · Dec 28, 2018 · Dec 28, 2018
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$

diff --git a/regression/ansi-c/const1/const-array.desc b/regression/ansi-c/const1/const-array.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 const-array.c
  ^.*: .* is constant$
 ^   array\[1\] = 2;$

diff --git a/regression/ansi-c/const1/const-member.desc b/regression/ansi-c/const1/const-member.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 const-member.c
 
 ^.*: .* is constant$

diff --git a/regression/ansi-c/cprover_bool1/test.desc b/regression/ansi-c/cprover_bool1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$