From a6fd7295e3e8da70466433324d12bd4ccb396f84 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 15 Feb 2018 13:16:57 +0000 Subject: [PATCH] Cleanup tests with anomalous main functions A forthcoming PR will make jbmc only recognise 'public static void main(String[])' as a main entry point (anything named 'main' but not matching that type will need explicit --function nomination. This adds the extra argument where required. One test (NondetInit3) is fixed as it was previously assuming that its parameter couldn't be null, which only happens when main(Subclass) is handled like it was main(String[]), where the String[] reference really cannot be null. --- .../cbmc-java/ArithmeticException6/test.desc | 2 +- regression/cbmc-java/LocalVarTable5/test.desc | 2 +- regression/cbmc-java/NondetInit2/test.desc | 3 +-- regression/cbmc-java/NondetInit3/Subclass.class | Bin 174 -> 174 bytes regression/cbmc-java/NondetInit3/Test.class | Bin 729 -> 737 bytes regression/cbmc-java/NondetInit3/Test.java | 3 ++- regression/cbmc-java/NondetInit3/test.desc | 3 +-- .../cbmc-java/VarLengthArrayTrace1/test.desc | 2 +- regression/cbmc-java/arrayread1/test.desc | 2 +- regression/cbmc-java/cast_null1/test.desc | 2 +- regression/cbmc-java/cast_null2/test.desc | 2 +- regression/cbmc-java/destructor1/test.desc | 2 +- regression/cbmc-java/exceptions22/test.desc | 2 +- .../cbmc-java/external_getstatic1/test.desc | 2 +- .../cbmc-java/inferlexicalscope1/test.desc | 2 +- .../cbmc-java/inherited_static_field1/test.desc | 2 +- .../inherited_static_field10/test.desc | 2 +- .../cbmc-java/inherited_static_field2/test.desc | 2 +- .../cbmc-java/inherited_static_field3/test.desc | 2 +- .../cbmc-java/inherited_static_field4/test.desc | 2 +- .../cbmc-java/inherited_static_field5/test.desc | 2 +- .../cbmc-java/inherited_static_field6/test.desc | 2 +- .../cbmc-java/inherited_static_field7/test.desc | 2 +- .../cbmc-java/inherited_static_field8/test.desc | 2 +- .../cbmc-java/inherited_static_field9/test.desc | 2 +- regression/cbmc-java/isnan1/test.desc | 2 +- regression/cbmc-java/json_trace1/test.desc | 2 +- regression/cbmc-java/json_trace3/test.desc | 2 +- .../check_clinit_normally_present.desc | 3 +-- .../check_clinit_removed_by_lazy_loading.desc | 2 +- .../check_runs_with_lazy_loading.desc | 3 +-- .../check_clinit_normally_present.desc | 3 +-- .../check_clinit_removed_by_lazy_loading.desc | 2 +- .../check_runs_with_lazy_loading.desc | 3 +-- .../check_clinit_normally_present.desc | 2 +- .../check_clinit_removed_by_lazy_loading.desc | 2 +- .../check_runs_with_lazy_loading.desc | 3 +-- .../putstatic_source_location/test.desc | 2 +- regression/cbmc-java/static_init1/test.desc | 2 +- regression/cbmc-java/static_init2/test.desc | 2 +- .../trace_options_json_extended/extended.desc | 2 +- .../non-extended.desc | 2 +- regression/cbmc-java/virtual7/test.desc | 2 +- regression/cbmc-java/virtual8/test.desc | 2 +- .../jbmc-strings/java_append_char/test.desc | 2 +- .../jbmc-strings/java_char_array_init/test.desc | 2 +- .../java_insert_char_array/test.desc | 2 +- .../java_append_string/test.desc | 2 +- .../strings-smoke-tests/java_case/test.desc | 2 +- .../java_char_array/test.desc | 2 +- .../java_insert_char_array/test.desc | 2 +- .../java_int_to_string/test1.desc | 2 +- .../java_int_to_string/test2.desc | 2 +- .../java_int_to_string/test2_bug.desc | 2 +- .../java_int_to_string/test3.desc | 2 +- .../java_int_to_string/test4.desc | 2 +- .../java_int_to_string/test5.desc | 2 +- .../java_int_to_string_knownbug/test.desc | 2 +- .../test_binary1.desc | 2 +- .../test_binary2.desc | 2 +- .../test_binary3.desc | 2 +- .../test_decimal.desc | 2 +- .../test_hex1.desc | 2 +- .../test_hex2.desc | 2 +- .../test_hex3.desc | 2 +- .../test_octal1.desc | 2 +- .../test_octal2.desc | 2 +- .../test_octal3.desc | 2 +- .../test_binary.desc | 2 +- .../test_hex.desc | 2 +- .../test_octal.desc | 2 +- .../java_long_to_string/test1.desc | 2 +- .../java_long_to_string/test2.desc | 2 +- .../java_long_to_string/test3.desc | 2 +- .../java_long_to_string/test4.desc | 2 +- .../java_long_to_string/test5.desc | 2 +- .../test_binary1.desc | 2 +- .../test_binary2.desc | 2 +- .../test_binary3.desc | 2 +- .../test_decimal.desc | 2 +- .../test_hex1.desc | 2 +- .../test_hex2.desc | 2 +- .../test_hex3.desc | 2 +- .../test_octal1.desc | 2 +- .../test_octal2.desc | 2 +- .../test_octal3.desc | 2 +- .../java_parseint/test1.desc | 2 +- .../java_parseint/test2.desc | 2 +- .../java_parseint_knownbug/test.desc | 2 +- .../java_parseint_with_radix/test1.desc | 2 +- .../java_parseint_with_radix/test2.desc | 2 +- .../java_parseint_with_radix/test3.desc | 2 +- .../java_parseint_with_radix/test4.desc | 2 +- .../java_parseint_with_radix/test5.desc | 2 +- .../java_parseint_with_radix/test6.desc | 2 +- .../java_parselong/test_binary_min.desc | 2 +- .../java_parselong/test_decimal_max.desc | 2 +- .../java_parselong/test_decimal_min.desc | 2 +- .../java_parselong/test_hex.desc | 2 +- .../java_parselong/test_octal.desc | 2 +- .../java_value_of_long/test.desc | 2 +- .../max_input_length/MemberTest.desc | 2 +- 102 files changed, 101 insertions(+), 107 deletions(-) diff --git a/regression/cbmc-java/ArithmeticException6/test.desc b/regression/cbmc-java/ArithmeticException6/test.desc index 8cab5f69869..8cd09de8d51 100644 --- a/regression/cbmc-java/ArithmeticException6/test.desc +++ b/regression/cbmc-java/ArithmeticException6/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest.class ---java-throw-runtime-exceptions +--java-throw-runtime-exceptions --function ArithmeticExceptionTest.main ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$ diff --git a/regression/cbmc-java/LocalVarTable5/test.desc b/regression/cbmc-java/LocalVarTable5/test.desc index 6f55a0d2bc6..82237a426e9 100644 --- a/regression/cbmc-java/LocalVarTable5/test.desc +++ b/regression/cbmc-java/LocalVarTable5/test.desc @@ -1,6 +1,6 @@ CORE test.class ---show-goto-functions +--show-goto-functions --function test.main dead anonlocal::1i dead anonlocal::2i dead anonlocal::3a diff --git a/regression/cbmc-java/NondetInit2/test.desc b/regression/cbmc-java/NondetInit2/test.desc index d75e7538e9b..4d752d2f54a 100644 --- a/regression/cbmc-java/NondetInit2/test.desc +++ b/regression/cbmc-java/NondetInit2/test.desc @@ -1,5 +1,4 @@ CORE Test.class - +--function Test.main ^VERIFICATION SUCCESSFUL$ - diff --git a/regression/cbmc-java/NondetInit3/Subclass.class b/regression/cbmc-java/NondetInit3/Subclass.class index ff6f1ffb00111e1d4689a261397bc350e10f1591..68201e11870c52a7bc66ff8687e111da47ee133d 100644 GIT binary patch delta 18 ZcmZ3-xQ=ncVs3E;Mg|TB1_mYuP5>!J0>}UW delta 18 ZcmZ3-xQ=ncVs2puMg|TB1_mYuP5>zy0>l6S diff --git a/regression/cbmc-java/NondetInit3/Test.class b/regression/cbmc-java/NondetInit3/Test.class index d3b4a9378f889132a3111b0bed8ef5b0dcfbc3a8..0c032f41a9c06219f9d5b259ce15325b571121e2 100644 GIT binary patch delta 54 zcmcb~`jB;lKNGJj0}}%y0|SGM)-eXD$q`J75_}BIK)xUY3xg1YG=ngM2$09jz$iVr Hm&peJ`k@DI delta 46 zcmaFJdXsg7KNF`d0}}%y0|SG^\(\) - diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc index f832b065f69..7cb991a807f 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc @@ -1,6 +1,6 @@ CORE Test.class ---lazy-methods --show-goto-functions +--lazy-methods --show-goto-functions --function Test.main -- java::Unused::clinit_wrapper Unused\.\(\) diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc index a9222f08176..67aa49a0689 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc @@ -1,5 +1,4 @@ CORE Test.class ---lazy-methods +--lazy-methods --function Test.main VERIFICATION SUCCESSFUL - diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc index d3d2757212f..32ea1eabe00 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc @@ -1,7 +1,6 @@ CORE Test.class ---show-goto-functions +--show-goto-functions --function Test.main java::Unused1::clinit_wrapper java::Unused2::clinit_wrapper Unused2\.\(\) - diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc index 0dcedea2911..3fb25e852a4 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc @@ -1,6 +1,6 @@ CORE Test.class ---lazy-methods --show-goto-functions +--lazy-methods --show-goto-functions --function Test.main -- java::Unused1::clinit_wrapper java::Unused2::clinit_wrapper diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc index a9222f08176..67aa49a0689 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc @@ -1,5 +1,4 @@ CORE Test.class ---lazy-methods +--lazy-methods --function Test.main VERIFICATION SUCCESSFUL - diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc index e412a962e54..689fdc3efad 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc @@ -1,5 +1,5 @@ CORE Test.class ---show-goto-functions +--show-goto-functions --function Test.main java::Opaque\.:\(\)V java::Opaque::clinit_wrapper diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc index 9b1fb07cc31..ec1d71302d6 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc @@ -1,6 +1,6 @@ CORE Test.class ---lazy-methods --show-goto-functions +--lazy-methods --show-goto-functions --function Test.main -- java::Opaque\.:\(\)V java::Opaque::clinit_wrapper diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc index a9222f08176..67aa49a0689 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc @@ -1,5 +1,4 @@ CORE Test.class ---lazy-methods +--lazy-methods --function Test.main VERIFICATION SUCCESSFUL - diff --git a/regression/cbmc-java/putstatic_source_location/test.desc b/regression/cbmc-java/putstatic_source_location/test.desc index fdb85eb8ee7..c788f292700 100644 --- a/regression/cbmc-java/putstatic_source_location/test.desc +++ b/regression/cbmc-java/putstatic_source_location/test.desc @@ -1,6 +1,6 @@ CORE test.class ---show-goto-functions +--show-goto-functions --function test.main ^EXIT=0$ ^SIGNAL=0$ test\.java line 5 function java::test.main:\(\)V bytecode-index 1 diff --git a/regression/cbmc-java/static_init1/test.desc b/regression/cbmc-java/static_init1/test.desc index 30868289dae..74331f8c333 100644 --- a/regression/cbmc-java/static_init1/test.desc +++ b/regression/cbmc-java/static_init1/test.desc @@ -1,6 +1,6 @@ CORE static_init.class - +--function static_init.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-java/static_init2/test.desc b/regression/cbmc-java/static_init2/test.desc index 30868289dae..74331f8c333 100644 --- a/regression/cbmc-java/static_init2/test.desc +++ b/regression/cbmc-java/static_init2/test.desc @@ -1,6 +1,6 @@ CORE static_init.class - +--function static_init.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-java/trace_options_json_extended/extended.desc b/regression/cbmc-java/trace_options_json_extended/extended.desc index a0234582e1d..16819b0ce24 100644 --- a/regression/cbmc-java/trace_options_json_extended/extended.desc +++ b/regression/cbmc-java/trace_options_json_extended/extended.desc @@ -1,6 +1,6 @@ CORE Test.class ---trace --json-ui --trace-json-extended +--trace --json-ui --trace-json-extended --function Test.main ^EXIT=10$ ^SIGNAL=0$ rawLhs diff --git a/regression/cbmc-java/trace_options_json_extended/non-extended.desc b/regression/cbmc-java/trace_options_json_extended/non-extended.desc index d13bdcd5f3f..8691dc49359 100644 --- a/regression/cbmc-java/trace_options_json_extended/non-extended.desc +++ b/regression/cbmc-java/trace_options_json_extended/non-extended.desc @@ -1,6 +1,6 @@ CORE Test.class ---trace --json-ui +--trace --json-ui --function Test.main ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc index d873bbcc8f9..6e420f8430c 100644 --- a/regression/cbmc-java/virtual7/test.desc +++ b/regression/cbmc-java/virtual7/test.desc @@ -1,6 +1,6 @@ CORE test.class ---show-goto-functions +--show-goto-functions --function test.main ^EXIT=0$ ^SIGNAL=0$ IF.*"java::C".*THEN GOTO [12] diff --git a/regression/cbmc-java/virtual8/test.desc b/regression/cbmc-java/virtual8/test.desc index 774005ac03d..dd23bff445d 100644 --- a/regression/cbmc-java/virtual8/test.desc +++ b/regression/cbmc-java/virtual8/test.desc @@ -1,6 +1,6 @@ CORE Test.class ---program-only +--program-only --function Test.main ^EXIT=0$ ^SIGNAL=0$ C\.f diff --git a/regression/jbmc-strings/java_append_char/test.desc b/regression/jbmc-strings/java_append_char/test.desc index 783301b2d52..efe6c611b39 100644 --- a/regression/jbmc-strings/java_append_char/test.desc +++ b/regression/jbmc-strings/java_append_char/test.desc @@ -1,6 +1,6 @@ CORE test_append_char.class ---refine-strings --string-max-length 1000 --no-core-models +--refine-strings --string-max-length 1000 --no-core-models --function test_append_char.main ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/jbmc-strings/java_char_array_init/test.desc b/regression/jbmc-strings/java_char_array_init/test.desc index e93fd2a4dc2..47fcb2fd1ce 100644 --- a/regression/jbmc-strings/java_char_array_init/test.desc +++ b/regression/jbmc-strings/java_char_array_init/test.desc @@ -1,6 +1,6 @@ CORE test_init.class ---refine-strings --string-max-length 1000 +--refine-strings --string-max-length 1000 --function test_init.main ^EXIT=10$ ^SIGNAL=0$ assertion.* file test_init.java line 31 .* SUCCESS$ diff --git a/regression/jbmc-strings/java_insert_char_array/test.desc b/regression/jbmc-strings/java_insert_char_array/test.desc index ea77b6e60aa..012a7e34e22 100644 --- a/regression/jbmc-strings/java_insert_char_array/test.desc +++ b/regression/jbmc-strings/java_insert_char_array/test.desc @@ -1,6 +1,6 @@ CORE test_insert_char_array.class ---refine-strings --string-max-length 1000 +--refine-strings --string-max-length 1000 --function test_insert_char_array.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 28.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_append_string/test.desc b/regression/strings-smoke-tests/java_append_string/test.desc index 9b6882b5f3f..847ade7776d 100644 --- a/regression/strings-smoke-tests/java_append_string/test.desc +++ b/regression/strings-smoke-tests/java_append_string/test.desc @@ -1,6 +1,6 @@ CORE test_append_string.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_append_string.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_case/test.desc b/regression/strings-smoke-tests/java_case/test.desc index bf6722dd2f8..18fa3cccaa9 100644 --- a/regression/strings-smoke-tests/java_case/test.desc +++ b/regression/strings-smoke-tests/java_case/test.desc @@ -1,6 +1,6 @@ CORE test_case.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_case.main ^EXIT=10$ ^SIGNAL=0$ assertion.* file test_case.java line 10 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_char_array/test.desc b/regression/strings-smoke-tests/java_char_array/test.desc index 3b1bf17532a..5d9ef1fdd7c 100644 --- a/regression/strings-smoke-tests/java_char_array/test.desc +++ b/regression/strings-smoke-tests/java_char_array/test.desc @@ -1,6 +1,6 @@ CORE test_char_array.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_char_array.main ^EXIT=10$ ^SIGNAL=0$ .*assertion.* test_char_array.java line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_insert_char_array/test.desc b/regression/strings-smoke-tests/java_insert_char_array/test.desc index a0614d7f360..53af52fc3ef 100644 --- a/regression/strings-smoke-tests/java_insert_char_array/test.desc +++ b/regression/strings-smoke-tests/java_insert_char_array/test.desc @@ -1,6 +1,6 @@ CORE test_insert_char_array.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_char_array.main ^EXIT=10$ ^SIGNAL=0$ assertion.* file test_insert_char_array.java line 20 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string/test1.desc b/regression/strings-smoke-tests/java_int_to_string/test1.desc index fd14afd9e7f..a8ace56c37b 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test1.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test1.desc @@ -1,6 +1,6 @@ CORE Test1.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string/test2.desc b/regression/strings-smoke-tests/java_int_to_string/test2.desc index 08bb206db54..e068d78d000 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test2.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test2.desc @@ -1,6 +1,6 @@ CORE Test2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc b/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc index c2917e25045..dc7e825073c 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc @@ -1,6 +1,6 @@ KNOWNBUG Test2.class ---refine-strings --verbosity 10 +--refine-strings --verbosity 10 --function Test2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string/test3.desc b/regression/strings-smoke-tests/java_int_to_string/test3.desc index c17950bade2..b35b58c87fa 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test3.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test3.desc @@ -1,6 +1,6 @@ CORE Test3.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string/test4.desc b/regression/strings-smoke-tests/java_int_to_string/test4.desc index e8085e4cc0b..3630073e1dd 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test4.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test4.desc @@ -1,6 +1,6 @@ CORE Test4.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test4.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string/test5.desc b/regression/strings-smoke-tests/java_int_to_string/test5.desc index 7a6c4dab79d..9fdf756a99d 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test5.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test5.desc @@ -1,6 +1,6 @@ CORE Test5.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test5.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc b/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc index 0d37463d104..4c289d1853c 100644 --- a/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc +++ b/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Test.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc index 3b0e8c9f52e..f76d7849b64 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc @@ -1,6 +1,6 @@ CORE Test_binary1.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary1.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc index 4b75576a9e0..b6b50f07cb3 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc @@ -1,6 +1,6 @@ CORE Test_binary2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc index c0dc5a0d100..0252051ba90 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc @@ -1,6 +1,6 @@ CORE Test_binary3.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary3.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc index 5df0fa0c612..391797533f5 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc @@ -1,6 +1,6 @@ CORE Test_decimal.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc index 65d42d9d4f4..e37cf5534de 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc @@ -1,6 +1,6 @@ CORE Test_hex1.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex1.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc index ca27aacf182..e6ca4960d19 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc @@ -1,6 +1,6 @@ CORE Test_hex2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc index d100589824c..d2f4d7cbb1c 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc @@ -1,6 +1,6 @@ CORE Test_hex3.class ---refine-strings --verbosity 10 --string-max-length 100 +--refine-strings --verbosity 10 --string-max-length 100 --function Test_hex3.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc index 16600fd2a12..a223a0e81df 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc @@ -1,6 +1,6 @@ CORE Test_octal1.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal1.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc index cbe2eab8212..229c999d00c 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc @@ -1,6 +1,6 @@ CORE Test_octal2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc index a742982813e..8b9c5a50209 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc @@ -1,6 +1,6 @@ CORE Test_octal3.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal3.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc index c81c25f146f..6d5672788ae 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc @@ -1,6 +1,6 @@ KNOWNBUG Test_binary.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc index 5fec73731fc..c5d33723394 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc @@ -1,6 +1,6 @@ KNOWNBUG Test_hex.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc index c47d55b6cf3..135a6d1a4aa 100644 --- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc +++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc @@ -1,6 +1,6 @@ KNOWNBUG Test_octal.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string/test1.desc b/regression/strings-smoke-tests/java_long_to_string/test1.desc index fd14afd9e7f..a8ace56c37b 100644 --- a/regression/strings-smoke-tests/java_long_to_string/test1.desc +++ b/regression/strings-smoke-tests/java_long_to_string/test1.desc @@ -1,6 +1,6 @@ CORE Test1.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string/test2.desc b/regression/strings-smoke-tests/java_long_to_string/test2.desc index a58153ecbd5..45859f9d225 100644 --- a/regression/strings-smoke-tests/java_long_to_string/test2.desc +++ b/regression/strings-smoke-tests/java_long_to_string/test2.desc @@ -1,6 +1,6 @@ THOROUGH Test2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string/test3.desc b/regression/strings-smoke-tests/java_long_to_string/test3.desc index 4cc0e5b4f0a..8f4c4c1aae9 100644 --- a/regression/strings-smoke-tests/java_long_to_string/test3.desc +++ b/regression/strings-smoke-tests/java_long_to_string/test3.desc @@ -1,6 +1,6 @@ THOROUGH Test3.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string/test4.desc b/regression/strings-smoke-tests/java_long_to_string/test4.desc index 11df46814d6..9f0dea8b275 100644 --- a/regression/strings-smoke-tests/java_long_to_string/test4.desc +++ b/regression/strings-smoke-tests/java_long_to_string/test4.desc @@ -1,6 +1,6 @@ THOROUGH Test4.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test4.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string/test5.desc b/regression/strings-smoke-tests/java_long_to_string/test5.desc index 7a6c4dab79d..9fdf756a99d 100644 --- a/regression/strings-smoke-tests/java_long_to_string/test5.desc +++ b/regression/strings-smoke-tests/java_long_to_string/test5.desc @@ -1,6 +1,6 @@ CORE Test5.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test5.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc index 46852f73fd8..64b50f64e69 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc @@ -1,6 +1,6 @@ THOROUGH Test_binary1.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary1.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc index 88ecdd6658e..fe04564fdbc 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc @@ -1,6 +1,6 @@ THOROUGH Test_binary2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc index 690a7051bff..22abe124fb8 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc @@ -1,6 +1,6 @@ THOROUGH Test_binary3.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary3.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc index 5df0fa0c612..391797533f5 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc @@ -1,6 +1,6 @@ CORE Test_decimal.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc index 65d42d9d4f4..e37cf5534de 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc @@ -1,6 +1,6 @@ CORE Test_hex1.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex1.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc index ca27aacf182..e6ca4960d19 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc @@ -1,6 +1,6 @@ CORE Test_hex2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc index d100589824c..d2f4d7cbb1c 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc @@ -1,6 +1,6 @@ CORE Test_hex3.class ---refine-strings --verbosity 10 --string-max-length 100 +--refine-strings --verbosity 10 --string-max-length 100 --function Test_hex3.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc index 87aad11f09f..6543f6938f7 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc @@ -1,6 +1,6 @@ CORE Test_octal1.class ---refine-strings --verbosity 10 --string-max-length 100 +--refine-strings --verbosity 10 --string-max-length 100 --function Test_octal1.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc index 11904eb55b9..7597b88f4be 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc @@ -1,6 +1,6 @@ CORE Test_octal2.class ---refine-strings --verbosity 10 --string-max-length 100 +--refine-strings --verbosity 10 --string-max-length 100 --function Test_octal2.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc index ef669e31737..aea786f5b92 100644 --- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc +++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc @@ -1,6 +1,6 @@ CORE Test_octal3.class ---refine-strings --verbosity 10 --string-max-length 100 +--refine-strings --verbosity 10 --string-max-length 100 --function Test_octal3.main ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint/test1.desc b/regression/strings-smoke-tests/java_parseint/test1.desc index 78d825da2ae..9b4e20397e0 100644 --- a/regression/strings-smoke-tests/java_parseint/test1.desc +++ b/regression/strings-smoke-tests/java_parseint/test1.desc @@ -1,6 +1,6 @@ CORE Test1.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint/test2.desc b/regression/strings-smoke-tests/java_parseint/test2.desc index 84540226f3c..eb61c1ce86a 100644 --- a/regression/strings-smoke-tests/java_parseint/test2.desc +++ b/regression/strings-smoke-tests/java_parseint/test2.desc @@ -1,6 +1,6 @@ CORE Test2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc index aa80ccad92f..f71c35b54bd 100644 --- a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc +++ b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Test.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 10.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc index 78d825da2ae..9b4e20397e0 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc +++ b/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc @@ -1,6 +1,6 @@ CORE Test1.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc index 40528a8244d..8ea06b614e0 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc +++ b/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc @@ -1,6 +1,6 @@ CORE Test2.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc index ea37ca8efb1..1e96c531c29 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc +++ b/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc @@ -1,6 +1,6 @@ CORE Test3.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc index aa4756341bb..e0980a2d899 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc +++ b/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc @@ -1,6 +1,6 @@ CORE Test4.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test4.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc index ea45d5af377..b7f35f7dccb 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc +++ b/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc @@ -1,6 +1,6 @@ CORE Test5.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test5.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc index 3ce216107c7..0f42ae7f205 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc +++ b/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc @@ -1,6 +1,6 @@ CORE Test6.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test6.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parselong/test_binary_min.desc b/regression/strings-smoke-tests/java_parselong/test_binary_min.desc index 0271a0c984a..9243521d9ff 100644 --- a/regression/strings-smoke-tests/java_parselong/test_binary_min.desc +++ b/regression/strings-smoke-tests/java_parselong/test_binary_min.desc @@ -1,6 +1,6 @@ CORE Test_binary_min.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary_min.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc b/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc index 640ed17fa83..9797e44dff0 100644 --- a/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc +++ b/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc @@ -1,6 +1,6 @@ CORE Test_decimal_max.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal_max.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc b/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc index 432fa01db5b..e2f1869d29d 100644 --- a/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc +++ b/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc @@ -1,6 +1,6 @@ CORE Test_decimal_min.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal_min.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parselong/test_hex.desc b/regression/strings-smoke-tests/java_parselong/test_hex.desc index 7dfd21113a5..7a991265f4c 100644 --- a/regression/strings-smoke-tests/java_parselong/test_hex.desc +++ b/regression/strings-smoke-tests/java_parselong/test_hex.desc @@ -1,6 +1,6 @@ CORE Test_hex.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parselong/test_octal.desc b/regression/strings-smoke-tests/java_parselong/test_octal.desc index b3310436432..a35595e7d2c 100644 --- a/regression/strings-smoke-tests/java_parselong/test_octal.desc +++ b/regression/strings-smoke-tests/java_parselong/test_octal.desc @@ -1,6 +1,6 @@ CORE Test_octal.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_value_of_long/test.desc b/regression/strings-smoke-tests/java_value_of_long/test.desc index e4e7094d764..e91920c7478 100644 --- a/regression/strings-smoke-tests/java_value_of_long/test.desc +++ b/regression/strings-smoke-tests/java_value_of_long/test.desc @@ -1,6 +1,6 @@ CORE test.class ---refine-strings --verbosity 10 --string-max-length 1000 +--refine-strings --verbosity 10 --string-max-length 1000 --function test.main ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 9 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.desc b/regression/strings-smoke-tests/max_input_length/MemberTest.desc index 01640d0a77c..2a62caa2eda 100644 --- a/regression/strings-smoke-tests/max_input_length/MemberTest.desc +++ b/regression/strings-smoke-tests/max_input_length/MemberTest.desc @@ -1,6 +1,6 @@ CORE MemberTest.class ---refine-strings --verbosity 10 --string-max-length 29 --java-assume-inputs-non-null +--refine-strings --verbosity 10 --string-max-length 29 --java-assume-inputs-non-null --function MemberTest.main ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$