Skip to content

Commit e708bfb

Browse files
committed
Adds --java-load-class to tests that require it
Passing .class files in the arguments list is (soon) to be deprecated, this just cleans up the last few places where this was happening in tests.
1 parent 5b8897e commit e708bfb

File tree

6 files changed

+6
-6
lines changed

6 files changed

+6
-6
lines changed

jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test.class
3-
--refine-strings --string-max-length 100 --string-max-input-length 4 --verbosity 10 --unwind 5 Test.class --function Test.testSuccess
3+
--refine-strings --string-max-length 100 --string-max-input-length 4 --verbosity 10 --unwind 5 --function Test.testSuccess
44
^EXIT=0$
55
^SIGNAL=0$
66
assertion at file Test.java line 23 .*: SUCCESS

jbmc/regression/jbmc-strings/StringConcat_StringII/test_fail.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test.class
3-
--refine-strings --string-max-length 10000 --verbosity 10 Test.class --function Test.testFail
3+
--refine-strings --string-max-length 10000 --verbosity 10 --function Test.testFail
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion at file Test.java line 38 .*: FAILURE

jbmc/regression/jbmc-strings/StringDependencies/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test.class
3-
--refine-strings --string-max-length 1000 --string-max-input-length 100 --verbosity 10 Test.class --function Test.test
3+
--refine-strings --string-max-length 1000 --string-max-input-length 100 --verbosity 10 --function Test.test
44
^EXIT=0$
55
^SIGNAL=0$
66
assertion at file Test.java line 20 .*: SUCCESS

jbmc/regression/jbmc-strings/max-length-generic-array/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
IntegerTests.class
3-
-refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMySet --cover location
3+
-refine-strings --string-max-length 100 --function IntegerTests.testMySet --cover location
44
^EXIT=0$
55
^SIGNAL=0$
66
coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED

jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
IntegerTests.class
3-
-refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMyGenSet --cover location
3+
-refine-strings --string-max-length 100 --function IntegerTests.testMyGenSet --cover location
44
^EXIT=0$
55
^SIGNAL=0$
66
coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED

jbmc/regression/jbmc/package_friendly1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
main.class
3-
package_friendly1.class package_friendly2.class --show-goto-functions
3+
--java-load-class package_friendly1 --java-load-class package_friendly2 --show-goto-functions
44
^main[.]main[\(].*[\)].*$
55
^package_friendly2[.]operation2[\(][\)].*$
66
^EXIT=0$

0 commit comments

Comments
 (0)