From 674c9f00f30cf39e95e4486a7c1cfe42ae1624bd Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 26 Mar 2018 14:09:03 +0100 Subject: [PATCH] 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) --- .../jbmc-strings/StringConcat/test_buffer_nondet_loop.desc | 4 ++-- .../jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc | 2 +- .../jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc | 4 ++-- .../jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc | 4 ++-- regression/jbmc-strings/StringConcat/test_string_nondet.desc | 2 +- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc b/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc index 85e22913994..75f57525803 100644 --- 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 index 8f2983e4c34..63814912cda 100644 --- 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 index 6d2ad2eac22..fbc95cd4df6 100644 --- 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 index 87c043ab693..7022df3ff8d 100644 --- 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 index 14f7c8ae8d0..cfce92f3210 100644 --- 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$