Merge pull request #1976 from romainbrenguier/regression/activate-dep…

…endency-tests Activate tests for StringBuffer.append in loops
diffblue · Apr 5, 2018 · c2f3726 · c2f3726
2 parents 69fb74a + 674c9f0
commit c2f3726
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 8 deletions.
diff --git a/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc
@@ -1,6 +1,6 @@
-FUTURE
+CORE
 Test.class
---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"
+--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'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

diff --git a/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 Test.class
 --refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5  --verbosity 10
 ^EXIT=10$

diff --git a/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc
@@ -1,6 +1,6 @@
-FUTURE
+CORE
 Test.class
---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"
+--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'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

diff --git a/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc
@@ -1,6 +1,6 @@
-FUTURE
+CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 5  --verbosity 10
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 3 --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

diff --git a/regression/jbmc-strings/StringConcat/test_string_nondet.desc b/regression/jbmc-strings/StringConcat/test_string_nondet.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 Test.class
 --refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.stringNonDet --depth 10000 --unwind 5 --verbosity 10
 ^EXIT=10$