Add --cp <classpath> option for regression tests that now need models

Author: danpoe

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

@@ -1,6 +1,6 @@
 FUTURE
 StringValueOf01.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -1,6 +1,6 @@
 CORE
 StringValueOf02.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$

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

@@ -1,6 +1,6 @@
 CORE
 StringValueOf03.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$

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

@@ -1,6 +1,6 @@
 CORE
 StringValueOf04.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$

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

@@ -1,6 +1,6 @@
 CORE
 StringValueOf05.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$

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

@@ -1,6 +1,6 @@
 CORE
 StringValueOf06.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$

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

@@ -1,6 +1,6 @@
 CORE
 StringValueOf07.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 8 .* FAILURE$

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

@@ -1,6 +1,6 @@
 CORE
 StringValueOf08.class
---max-nondet-string-length 100
+--max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$

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

@@ -1,6 +1,6 @@
 FUTURE
 StringValueOf10.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.checkWithDependency --depth 10000
+--function Test.checkWithDependency --depth 10000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 63 .*: SUCCESS

jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.checkDet
+--function Test.checkDet --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 26 .*: FAILURE

jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.checkNonDet
+--function Test.checkNonDet --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 55 .*: FAILURE