Skip to content

Commit 674c9f0

Browse files
Activate tests for StringBuffer concat in loops
We activate these tests which check that refinement is not needed when strings are not tested. They should all run in a reasonnable time now, the most difficult takes about 2 seconds. This also fixes quote problems (single quotes have to be used for Windows)
1 parent 18478e9 commit 674c9f0

5 files changed

+8
-8
lines changed

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
FUTURE
1+
CORE
22
Test.class
3-
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5 --verbosity 10 --property "java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1"
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5 --verbosity 10 --property 'java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1'
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
CORE
22
Test.class
33
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5 --verbosity 10
44
^EXIT=10$

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
FUTURE
1+
CORE
22
Test.class
3-
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5 --verbosity 10 --property "java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1"
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5 --verbosity 10 --property 'java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1'
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
FUTURE
1+
CORE
22
Test.class
3-
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 5 --verbosity 10
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 3 --verbosity 10
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

regression/jbmc-strings/StringConcat/test_string_nondet.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
CORE
22
Test.class
33
--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.stringNonDet --depth 10000 --unwind 5 --verbosity 10
44
^EXIT=10$

0 commit comments

Comments
 (0)