Skip to content

Commit f3840be

Browse files
committed
Mark quick "THOROUGH" tests as "CORE"
These perhaps used to take much longer, but currently complete within a small number of seconds (with both MiniSat and CaDiCaL as back-ends): * ConstantEvaluationToString01/test_long_no_propagation2.desc: * cadical: 11 seconds * minisat: 9 seconds * StringBuilderChars01/test.desc: * cadical: 8 seconds * minisat: 4 seconds * StringIndexMethods01/test.desc: * cadical: 0 seconds * minisat: 0 seconds * StringIndexOf/test_thorough.desc: * cadical: 1 seconds * minisat: 2 seconds * StringStartEnd01/test.desc: * cadical: 0 seconds * minisat: 0 seconds * StringStartEnd03/test.desc: * cadical: 0 seconds * minisat: 0 seconds * location15/test.desc: * cadical: 5 seconds * minisat: 5 seconds
1 parent 3f578e1 commit f3840be

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)