From e708bfb52fdbd7ba16564d306b6e99fa8abcffce Mon Sep 17 00:00:00 2001 From: johndumbell Date: Fri, 15 Jun 2018 18:11:58 +0100 Subject: [PATCH] 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. --- jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc | 2 +- .../jbmc-strings/StringConcat_StringII/test_fail.desc | 2 +- jbmc/regression/jbmc-strings/StringDependencies/test.desc | 2 +- jbmc/regression/jbmc-strings/max-length-generic-array/test.desc | 2 +- .../jbmc-strings/max-length-generic-array/test_gen.desc | 2 +- jbmc/regression/jbmc/package_friendly1/test.desc | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc b/jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc index 4876a04b8e4..79b0e5636c5 100644 --- a/jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc +++ b/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 diff --git a/jbmc/regression/jbmc-strings/StringConcat_StringII/test_fail.desc b/jbmc/regression/jbmc-strings/StringConcat_StringII/test_fail.desc index f8751dbb3a3..47e0399c5b2 100644 --- a/jbmc/regression/jbmc-strings/StringConcat_StringII/test_fail.desc +++ b/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 diff --git a/jbmc/regression/jbmc-strings/StringDependencies/test.desc b/jbmc/regression/jbmc-strings/StringDependencies/test.desc index 8368650a1cf..9a1485143a8 100644 --- a/jbmc/regression/jbmc-strings/StringDependencies/test.desc +++ b/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 diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc b/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc index 3862a4978b3..abd5e382ff9 100644 --- a/jbmc/regression/jbmc-strings/max-length-generic-array/test.desc +++ b/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 diff --git a/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc b/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc index ec123c9a16a..3f8a4ce6ea3 100644 --- a/jbmc/regression/jbmc-strings/max-length-generic-array/test_gen.desc +++ b/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 diff --git a/jbmc/regression/jbmc/package_friendly1/test.desc b/jbmc/regression/jbmc/package_friendly1/test.desc index 78e710b263a..e3250bd8d47 100644 --- a/jbmc/regression/jbmc/package_friendly1/test.desc +++ b/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$