Merge pull request #5719 from tautschnig/knownbug

tautschnig · web-flow · commit d0be4a1d6d89 · 2021-01-11T11:41:11.000+01:00
Mark various working KNOWNBUG tests "CORE"
diff --git a/jbmc/regression/janalyzer-taint/taint-map1/test.desc b/jbmc/regression/janalyzer-taint/taint-map1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 map1
 --taint taint.json
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A
 --function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A
 --function 'A.me_bug:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 Sync
 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 Sync
 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-fail.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-fail.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 StringBuilderConstructors01
 --function StringBuilderConstructors01.capacityFail --max-nondet-string-length 1000
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-pass.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-capacity-pass.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 StringBuilderConstructors01
 --function StringBuilderConstructors01.capacityPass --max-nondet-string-length 1000
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors02/test.desc b/jbmc/regression/jbmc-strings/StringBuilderConstructors02/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 StringBuilderConstructors02
 --max-nondet-string-length 1000
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-pass.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-pass.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE symex-driven-lazy-loading-expected-failure
 Test
 --function Test.testBoolLengthTrue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testBoolLengthTrue:()Ljava/lang/String;.assertion.2'
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringFormatVerification/check_boolean_null.desc b/jbmc/regression/jbmc-strings/StringFormatVerification/check_boolean_null.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 test
 --max-nondet-string-length 20 --function test.check_boolean_null --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringFormatVerification/fail_alternative.desc b/jbmc/regression/jbmc-strings/StringFormatVerification/fail_alternative.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 test
 --max-nondet-string-length 20 --function test.fail_alternative --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringFormatVerification/fail_boolean_null.desc b/jbmc/regression/jbmc-strings/StringFormatVerification/fail_boolean_null.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 test
 --max-nondet-string-length 20 --function test.fail_boolean_null --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringFormatVerification/fail_general_scientific.desc b/jbmc/regression/jbmc-strings/StringFormatVerification/fail_general_scientific.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 test
 --max-nondet-string-length 20 --function test.fail_general_scientific --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringFormatVerification/fail_general_scientific_uppercase.desc b/jbmc/regression/jbmc-strings/StringFormatVerification/fail_general_scientific_uppercase.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 test
 --max-nondet-string-length 20 --function test.fail_general_scientific_uppercase --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc/athrow1/test.desc b/jbmc/regression/jbmc/athrow1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 athrow1
 
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 Test
 --function Test.test --show-goto-functions
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_class_fail.desc b/jbmc/regression/jbmc/deterministic_assignments_json/test_reference_to_other_class_fail.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 StaticValues
 --unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --static-values clinit-state.json --function StaticValues.testReferenceToOtherClassFail
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc/function3/test.desc b/jbmc/regression/jbmc/function3/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 Main
 --function 'A.dummy:()V'
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/lazyloading_nested_generic_parameters/test.desc b/jbmc/regression/jbmc/lazyloading_nested_generic_parameters/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE symex-driven-lazy-loading-expected-failure
 test
 --verbosity 10 --function test.g
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/virtual9/test.desc b/jbmc/regression/jbmc/virtual9/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 Test
 --program-only
 ^EXIT=0$
diff --git a/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc b/jbmc/regression/strings-smoke-tests/java_contains/test_string_printable.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 test_contains
 --max-nondet-string-length 100 --string-printable --function test_contains.main
 ^EXIT=0$
diff --git a/regression/cbmc-library/_read-01/test.desc b/regression/cbmc-library/_read-01/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --unwind 1 --unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/_write-01/test.desc b/regression/cbmc-library/_write-01/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --unwind 1 --unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/abort-01/test.desc b/regression/cbmc-library/abort-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc-library/memcpy-05/test.desc b/regression/cbmc-library/memcpy-05/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/memmove-01/test.desc b/regression/cbmc-library/memmove-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --unwind 17
 ^EXIT=0$
diff --git a/regression/cbmc-library/vasprintf-01/test.desc b/regression/cbmc-library/vasprintf-01/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --unwind 1 --unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Array_Propagation1/test.desc b/regression/cbmc/Array_Propagation1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$
@@ -9,5 +9,4 @@ main.c
 ^warning: ignoring
 --
 This requires field-sensitive SSA encoding of arrays to pass entirely via
-constant propagation (changing the above condition to "1 remaining after
-simplification" would also make it pass, but this isn't the point of the test).
+constant propagation.
diff --git a/regression/cbmc/Float-equality1/test_equality.desc b/regression/cbmc/Float-equality1/test_equality.desc
@@ -1,4 +1,4 @@
-KNOWNBUG broken-smt-backend
+THOROUGH
 main.c
 -DEQUALITY
 ^EXIT=0$
@@ -7,4 +7,6 @@ main.c
 --
 ^warning: ignoring
 --
-Times out. See #4337.
+Takes approximately 1000 seconds to complete when using the SAT back-end (and
+Minisat2). The SMT solver completes this task in less than 0.1 seconds.
+See #4337.
diff --git a/regression/cbmc/Initialization7/test.desc b/regression/cbmc/Initialization7/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_Assume1/test.desc b/regression/cbmc/Pointer_Assume1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/assert_func_four/test.desc b/regression/cbmc/assert_func_four/test.desc
@@ -1,6 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 
+function .* is not declared
 ^EXIT=6$
 ^SIGNAL=0$
 expected to have four arguments
diff --git a/regression/cbmc/assert_lhs/test.desc b/regression/cbmc/assert_lhs/test.desc
@@ -1,6 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 
+function .* is not declared
 ^EXIT=6$
 ^SIGNAL=0$
 expected not to have LHS
diff --git a/regression/cbmc/assert_one/test.desc b/regression/cbmc/assert_one/test.desc
@@ -1,6 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 
+function .* is not declared
 ^EXIT=6$
 ^SIGNAL=0$
 expected to have one argument
diff --git a/regression/cbmc/assert_rtn_four/test.desc b/regression/cbmc/assert_rtn_four/test.desc
@@ -1,6 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 
+function .* is not declared
 ^EXIT=6$
 ^SIGNAL=0$
 expected to have four arguments
diff --git a/regression/cbmc/constant_folding2/test.desc b/regression/cbmc/constant_folding2/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/gcc_builtin_va_arg_one/test.desc b/regression/cbmc/gcc_builtin_va_arg_one/test.desc
@@ -1,6 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 
+function .* is not declared
 ^EXIT=6$
 ^SIGNAL=0$
 expected to have one argument
diff --git a/regression/cbmc/scanf1/big-endian.desc b/regression/cbmc/scanf1/big-endian.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.i
 --big-endian
 ^EXIT=10$
diff --git a/regression/cbmc/struct11/test.desc b/regression/cbmc/struct11/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/verifier_error_lhs/test.desc b/regression/cbmc/verifier_error_lhs/test.desc
@@ -1,6 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 
+function .* is not declared
 ^EXIT=6$
 ^SIGNAL=0$
 expected not to have LHS
diff --git a/regression/cbmc/verifier_error_zero/test.desc b/regression/cbmc/verifier_error_zero/test.desc
@@ -1,6 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 
+function .* is not declared
 ^EXIT=6$
 ^SIGNAL=0$
 expected to have no arguments
diff --git a/regression/goto-analyzer/variable-sensitivity-bug-02/test.desc b/regression/goto-analyzer/variable-sensitivity-bug-02/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers constants --show
 ^EXIT=0$
diff --git a/regression/goto-analyzer/variable-sensitivity-bug-03/test.desc b/regression/goto-analyzer/variable-sensitivity-bug-03/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers constants --show
 ^EXIT=0$
diff --git a/regression/goto-instrument/slice17/test.desc b/regression/goto-instrument/slice17/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --full-slice
 ^EXIT=0$
diff --git a/regression/goto-instrument/slice21/main.c b/regression/goto-instrument/slice21/main.c
diff --git a/regression/goto-instrument/slice21/test.desc b/regression/goto-instrument/slice21/test.desc

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG`
	`1`	`+CORE`
`2`	`2`	`map1`
`3`	`3`	`--taint taint.json`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG`
	`1`	`+CORE symex-driven-lazy-loading-expected-failure`
`2`	`2`	`Test`
`3`	`3`	--function Test.testBoolLengthTrue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testBoolLengthTrue:()Ljava/lang/String;.assertion.2'
`4`	`4`	`^EXIT=0$`