File tree Expand file tree Collapse file tree 3 files changed +5
-5
lines changed
jbmc/regression/jbmc-strings Expand file tree Collapse file tree 3 files changed +5
-5
lines changed Original file line number Diff line number Diff line change 1
1
CORE
2
2
Test.class
3
- --function Test.check
3
+ --function Test.check --max-nondet-string-length 1000000000
4
4
^EXIT=10$
5
5
^SIGNAL=0$
6
6
^VERIFICATION FAILED$
7
7
file Test.java line 20 .*: FAILURE$
8
8
--
9
9
--
10
- --max-nondet-string-length is not used on purpose, because this tests the behaviour
11
- of string refinement on very large strings.
10
+ this tests the behaviour of string refinement on very large strings
Original file line number Diff line number Diff line change 1
1
CORE
2
2
Test.class
3
- --function Test.checkAbort --trace
3
+ --function Test.checkAbort --trace --max-nondet-string-length 1000000000
4
4
^EXIT=10$
5
5
^SIGNAL=0$
6
6
dynamic_object[0-9]*=\(assignment removed\)
Original file line number Diff line number Diff line change 1
1
CORE
2
2
Test.class
3
- --function Test.checkMinLength --string-non-empty
3
+ --function Test.checkMinLength --string-non-empty --max-nondet-string-length 1000000000
4
4
^EXIT=10$
5
5
^SIGNAL=0$
6
6
assertion.* line 11 function java::Test.checkMinLength.*: SUCCESS
@@ -9,3 +9,4 @@ assertion.* line 17 function java::Test.checkMinLength.*: FAILURE
9
9
assertion.* line 19 function java::Test.checkMinLength.*: FAILURE
10
10
--
11
11
^Building error trace
12
+ --
You can’t perform that action at this time.
0 commit comments