Merge pull request diffblue#2487 from JohnDumbell/bugfix/add_java_load_class

Adds --java-load-class to tests that require it

Author: Daniel Kroening

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

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

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

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 10000 --verbosity 10 Test.class --function Test.testFail
+--refine-strings --string-max-length 10000 --verbosity 10 --function Test.testFail
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 38 .*: FAILURE

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

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

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

@@ -1,6 +1,6 @@
 CORE
 IntegerTests.class
--refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMySet --cover location
+-refine-strings --string-max-length 100 --function IntegerTests.testMySet --cover location
 ^EXIT=0$
 ^SIGNAL=0$
 coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED

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

@@ -1,6 +1,6 @@
 CORE
 IntegerTests.class
--refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMyGenSet --cover location
+-refine-strings --string-max-length 100 --function IntegerTests.testMyGenSet --cover location
 ^EXIT=0$
 ^SIGNAL=0$
 coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED

jbmc/regression/jbmc/package_friendly1/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 main.class
-package_friendly1.class package_friendly2.class --show-goto-functions
+--java-load-class package_friendly1 --java-load-class package_friendly2 --show-goto-functions
 ^main[.]main[\(].*[\)].*$
 ^package_friendly2[.]operation2[\(][\)].*$
 ^EXIT=0$