Skip to content

Commit 32318b7

Browse files
authored
Merge pull request #7520 from tautschnig/cleanup/thorough-to-core
Mark quick "THOROUGH" tests as "CORE"
2 parents 7f96b25 + f3840be commit 32318b7

File tree

7 files changed

+12
-8
lines changed

7 files changed

+12
-8
lines changed

jbmc/regression/jbmc-strings/ConstantEvaluationToString01/test_long_no_propagation2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
THOROUGH
1+
CORE
22
Main
33
--function Main.testLongToStringNoPropagation2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$

jbmc/regression/jbmc-strings/StringBuilderChars01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
THOROUGH
1+
CORE
22
StringBuilderChars01
33
--function StringBuilderChars01.test --unwind 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$

jbmc/regression/jbmc-strings/StringIndexMethods01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
THOROUGH
1+
CORE
22
StringIndexMethods01
33
--max-nondet-string-length 1000
44
^EXIT=0$

jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
THOROUGH
1+
CORE
22
Test
33
--function Test.check --unwind 10 --max-nondet-string-length 10 --java-assume-inputs-non-null
44
^EXIT=0$

jbmc/regression/jbmc-strings/StringStartEnd01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
THOROUGH
1+
CORE
22
StringStartEnd01
33
--max-nondet-string-length 1000 --unwind 30
44
^EXIT=0$

jbmc/regression/jbmc-strings/StringStartEnd03/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
THOROUGH
1+
CORE
22
StringStartEnd03
33
--max-nondet-string-length 1000 --unwind 15
44
^EXIT=10$
Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
THOROUGH
1+
CORE
22
main.c
33
--cover location
44
^EXIT=0$
@@ -8,6 +8,10 @@ main.c
88
^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$
99
^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$
1010
^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$
11-
^\*\* 3 of 5 covered \(60.0%\)
11+
^\*\* 3 of \d+ covered
1212
--
1313
^warning: ignoring
14+
--
15+
This test yields 5 blocks on Linux, 60 blocks on MacOS, and 65 blocks on
16+
Windows. In all cases, 3 blocks are covered successfully, everything else is
17+
unreachable.

0 commit comments

Comments
 (0)