Skip to content

Commit 123541f

Browse files
romainbrenguierromainbrenguier
committed
Correct string-max-input-length tests
Remove test from max_input_length This remove test which was using the way max-input-length was limiting the size of strings, even constant one. The solver is now more permisives and the long strings would just get troncated instead of leading to a solver contradiction. For MemberTest, we add a new test. We now have two tests with different values of the option, which should give different results.
1 parent 411e654 commit 123541f

File tree

7 files changed

+25
-17
lines changed

7 files changed

+25
-17
lines changed

‎regression/strings-smoke-tests/max_input_length/MemberTest.class‎

16 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/max_input_length/MemberTest.desc‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
MemberTest.class
3-
--refine-strings --verbosity 10 --string-max-length 29 --java-assume-inputs-non-null --function MemberTest.main
4-
^EXIT=0$
3+
--refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 31 --function MemberTest.main
4+
^EXIT=10$
55
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
6+
^VERIFICATION FAILED$
77
--
88
non equal types

‎regression/strings-smoke-tests/max_input_length/MemberTest.java‎

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,17 @@
11
public class MemberTest {
22
String foo;
3+
34
public void main() {
4-
// Causes this function to be ignored if string-max-length is
5-
// less than 40
5+
if (foo == null)
6+
return;
7+
8+
// This would prevent anything from happening if we were to add a
9+
// constraints on strings being smaller than 40
610
String t = new String("0123456789012345678901234567890123456789");
7-
assert foo != null && foo.length() < 30;
11+
12+
if (foo.length() >= 30)
13+
// This should not happen when string-max-input length is smaller
14+
// than 30
15+
assert false;
816
}
917
}

‎regression/strings-smoke-tests/max_input_length/MemberTest2.desc‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
MemberTest.class
3+
--refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 20 --function MemberTest.main
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
non equal types

‎regression/strings-smoke-tests/max_input_length/Test.class‎

7 Bytes
Binary file not shown.

‎regression/strings-smoke-tests/max_input_length/Test.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
public class Test {
22
public static void main(String s) {
3-
// This prevent anything from happening if string-max-length is smaller
4-
// than 40
5-
String t = new String("0123456789012345678901234567890123456789");
3+
// This prevent anything from happening if we were to add a constraints on strings
4+
// being smaller than 40
5+
String t = new String("0123456789012345678901234567890123456789");
66
if (s.length() >= 30)
77
// This should not happen when string-max-input length is smaller
88
// than 30

‎regression/strings-smoke-tests/max_input_length/test.desc‎

Lines changed: 0 additions & 8 deletions
This file was deleted.

0 commit comments

Comments
 (0)