From e8491a604ea768afbe67119f05afc0090b5b5225 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 10 Aug 2017 12:09:59 +0100 Subject: [PATCH 1/7] Factoring assign_java_string_to_string_expr with process_operands These were doing mostly the same thing. Renamd function convert_exprt_to_string_exprt: This describes more precisely what the function does. --- .../java_string_library_preprocess.cpp | 47 +++++++------------ .../java_string_library_preprocess.h | 3 +- 2 files changed, 17 insertions(+), 33 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 8e7947d9636..ae151179a17 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -287,32 +287,27 @@ exprt::operandst java_string_library_preprocesst::process_parameters( return process_operands(ops, loc, symbol_table, init_code); } -/// Creates a string_exprt from the input exprt and adds it to processed_ops -/// \param processed_ops: the list of processed operands to populate -/// \param op_to_process: a list of expressions +/// Creates a string_exprt from the input exprt representing a char sequence +/// \param op_to_process: an operand of a type which implements char sequence /// \param loc: location in the source /// \param symbol_table: symbol table /// \param init_code: code block, in which declaration of some arguments may be /// added -void java_string_library_preprocesst::process_single_operand( - exprt::operandst &processed_ops, +/// \return the processed operand +exprt java_string_library_preprocesst::convert_exprt_to_string_exprt( const exprt &op_to_process, const source_locationt &loc, symbol_tablet &symbol_table, code_blockt &init_code) { - member_exprt length( - op_to_process, "length", string_length_type()); - member_exprt data(op_to_process, "data", string_data_type(symbol_table)); - dereference_exprt deref_data(data, data.type().subtype()); + PRECONDITION(implements_java_char_sequence(op_to_process.type())); string_exprt string_expr=fresh_string_expr(loc, symbol_table, init_code); + init_code.add(code_assign_java_string_to_string_expr( + string_expr, op_to_process, symbol_table)); exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, init_code); init_code.add(code_declt(string_expr_sym)); - init_code.add(code_assignt(string_expr.length(), length)); - init_code.add( - code_assignt(string_expr.content(), deref_data)); init_code.add(code_assignt(string_expr_sym, string_expr)); - processed_ops.push_back(string_expr); + return string_expr; } /// for each expression that is of a type implementing strings, we declare a new @@ -336,19 +331,12 @@ exprt::operandst java_string_library_preprocesst::process_operands( for(const auto &p : operands) { if(implements_java_char_sequence(p.type())) - { - dereference_exprt deref= - checked_dereference(p, to_pointer_type(p.type()).subtype()); - process_single_operand(ops, deref, loc, symbol_table, init_code); - } + ops.push_back( + convert_exprt_to_string_exprt(p, loc, symbol_table, init_code)); else if(is_java_char_array_pointer_type(p.type())) - { ops.push_back(replace_char_array(p, loc, symbol_table, init_code)); - } else - { ops.push_back(p); - } } return ops; } @@ -370,22 +358,19 @@ exprt::operandst code_blockt &init_code) { PRECONDITION(operands.size()==2); - exprt::operandst ops; const exprt &op0=operands[0]; - const exprt &op1=operands[1]; PRECONDITION(implements_java_char_sequence(op0.type())); - dereference_exprt deref0= - checked_dereference(op0, to_pointer_type(op0.type()).subtype()); - process_single_operand(ops, deref0, loc, symbol_table, init_code); + exprt::operandst ops; + ops.push_back( + convert_exprt_to_string_exprt(op0, loc, symbol_table, init_code)); // TODO: Manage the case where we have a non-String Object (this should // probably be handled upstream. At any rate, the following code should be // protected with assertions on the type of op1. - typecast_exprt tcast(op1, to_pointer_type(op0.type())); - dereference_exprt deref1= - checked_dereference(tcast, to_pointer_type(op0.type()).subtype()); - process_single_operand(ops, deref1, loc, symbol_table, init_code); + typecast_exprt tcast(operands[1], to_pointer_type(op0.type())); + ops.push_back( + convert_exprt_to_string_exprt(tcast, loc, symbol_table, init_code)); return ops; } diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h index cc8dd4cf469..4579f2ee2c9 100644 --- a/src/java_bytecode/java_string_library_preprocess.h +++ b/src/java_bytecode/java_string_library_preprocess.h @@ -173,8 +173,7 @@ class java_string_library_preprocesst:public messaget symbol_tablet &symbol_table, code_blockt &init_code); - void process_single_operand( - exprt::operandst &processed_ops, + exprt convert_exprt_to_string_exprt( const exprt &deref, const source_locationt &loc, symbol_tablet &symbol_table, From 870814ec5d81438bbf5eb99c2f728239b2c7855f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 22 Aug 2017 14:22:56 +0100 Subject: [PATCH 2/7] Make code_assign_java_string_to_string_expr append to a code argument This avoids creating new code blocks inside already existing code blocks. --- .../java_string_library_preprocess.cpp | 37 ++++++++++--------- .../java_string_library_preprocess.h | 7 +++- 2 files changed, 24 insertions(+), 20 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index ae151179a17..6d638f80f76 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -302,10 +302,9 @@ exprt java_string_library_preprocesst::convert_exprt_to_string_exprt( { PRECONDITION(implements_java_char_sequence(op_to_process.type())); string_exprt string_expr=fresh_string_expr(loc, symbol_table, init_code); - init_code.add(code_assign_java_string_to_string_expr( - string_expr, op_to_process, symbol_table)); + code_assign_java_string_to_string_expr( + string_expr, op_to_process, symbol_table, init_code); exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, init_code); - init_code.add(code_declt(string_expr_sym)); init_code.add(code_assignt(string_expr_sym, string_expr)); return string_expr; } @@ -781,13 +780,16 @@ codet java_string_library_preprocesst:: /// \param lhs: a string expression /// \param rhs: an expression representing a java string /// \param symbol_table: symbol table -/// \return return the following code: +/// \param code: code block that gets appended the following code: /// ~~~~~~~~~~~~~~~~~~~~~~ /// lhs.length=rhs->length /// lhs.data=*(rhs->data) /// ~~~~~~~~~~~~~~~~~~~~~~ -codet java_string_library_preprocesst::code_assign_java_string_to_string_expr( - const string_exprt &lhs, const exprt &rhs, symbol_tablet &symbol_table) +void java_string_library_preprocesst::code_assign_java_string_to_string_expr( + const string_exprt &lhs, + const exprt &rhs, + symbol_tablet &symbol_table, + code_blockt &code) { PRECONDITION(implements_java_char_sequence(rhs.type())); @@ -806,7 +808,6 @@ codet java_string_library_preprocesst::code_assign_java_string_to_string_expr( dereference_exprt rhs_data(member_data, member_data.type().subtype()); // Assignments - code_blockt code; code.add(code_assignt(lhs.length(), rhs_length)); // We always assume data of a String is not null @@ -814,7 +815,6 @@ codet java_string_library_preprocesst::code_assign_java_string_to_string_expr( member_data, null_pointer_exprt(to_pointer_type(member_data.type())))); code.add(code_assumet(data_not_null)); code.add(code_assignt(lhs.content(), rhs_data)); - return code; } /// \param lhs: an expression representing a java string @@ -1140,8 +1140,8 @@ codet java_string_library_preprocesst::make_string_to_char_array_code( // string_expr = {this->length, this->data} string_exprt string_expr=fresh_string_expr(loc, symbol_table, code); - code.add(code_assign_java_string_to_string_expr( - string_expr, string_argument, symbol_table)); + code_assign_java_string_to_string_expr( + string_expr, string_argument, symbol_table, code); exprt string_expr_sym=fresh_string_expr_symbol( loc, symbol_table, code); code.add(code_assignt(string_expr_sym, string_expr)); @@ -1391,8 +1391,11 @@ exprt java_string_library_preprocesst::make_argument_for_format( pointer_typet string_pointer= java_reference_type(symbol_typet("java::java.lang.String")); typecast_exprt arg_i_as_string(arg_i, string_pointer); - code_not_null.add(code_assign_java_string_to_string_expr( - to_string_expr(field_expr), arg_i_as_string, symbol_table)); + code_assign_java_string_to_string_expr( + to_string_expr(field_expr), + arg_i_as_string, + symbol_table, + code_not_null); exprt arg_i_string_expr_sym=fresh_string_expr_symbol( loc, symbol_table, code_not_null); code_not_null.add(code_assignt( @@ -1651,8 +1654,7 @@ codet java_string_library_preprocesst::make_copy_string_code( // Assign the argument to string_expr code_typet::parametert op=type.parameters()[0]; symbol_exprt arg0(op.get_identifier(), op.type()); - code.add(code_assign_java_string_to_string_expr( - string_expr, arg0, symbol_table)); + code_assign_java_string_to_string_expr(string_expr, arg0, symbol_table, code); // Assign string_expr to string_expr_sym exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code); @@ -1693,8 +1695,7 @@ codet java_string_library_preprocesst::make_copy_constructor_code( // Assign argument to a string_expr code_typet::parameterst params=type.parameters(); symbol_exprt arg1(params[1].get_identifier(), params[1].type()); - code.add(code_assign_java_string_to_string_expr( - string_expr, arg1, symbol_table)); + code_assign_java_string_to_string_expr(string_expr, arg1, symbol_table, code); // Assign string_expr to symbol to keep track of it exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code); @@ -1735,8 +1736,8 @@ codet java_string_library_preprocesst::make_string_length_code( string_exprt str_expr=fresh_string_expr(loc, symbol_table, code); // Assign this to str_expr - code.add( - code_assign_java_string_to_string_expr(str_expr, arg_this, symbol_table)); + code_assign_java_string_to_string_expr( + str_expr, arg_this, symbol_table, code); // Assign str_expr to str_expr_sym for that expression to be present in the // symbol table in order to be processed by the string solver diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h index 4579f2ee2c9..ad0cfd1e959 100644 --- a/src/java_bytecode/java_string_library_preprocess.h +++ b/src/java_bytecode/java_string_library_preprocess.h @@ -285,8 +285,11 @@ class java_string_library_preprocesst:public messaget const source_locationt &loc, symbol_tablet &symbol_table); - codet code_assign_java_string_to_string_expr( - const string_exprt &lhs, const exprt &rhs, symbol_tablet &symbol_table); + void code_assign_java_string_to_string_expr( + const string_exprt &lhs, + const exprt &rhs, + symbol_tablet &symbol_table, + code_blockt &code); codet code_assign_string_literal_to_string_expr( const string_exprt &lhs, From 02e42da64b7690e2d1633892681ca855e7ae6794 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 22 Aug 2017 13:33:18 +0100 Subject: [PATCH 3/7] Adding unit test for convert exprt to string exprt --- .../java_string_library_preprocess.h | 7 +++ unit/Makefile | 1 + .../convert_exprt_to_string_exprt.cpp | 59 +++++++++++++++++++ 3 files changed, 67 insertions(+) create mode 100644 unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h index ad0cfd1e959..cff80bea63f 100644 --- a/src/java_bytecode/java_string_library_preprocess.h +++ b/src/java_bytecode/java_string_library_preprocess.h @@ -173,6 +173,13 @@ class java_string_library_preprocesst:public messaget symbol_tablet &symbol_table, code_blockt &init_code); + friend exprt convert_exprt_to_string_exprt_unit_test( + java_string_library_preprocesst &preprocess, + const exprt &deref, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &init_code); + exprt convert_exprt_to_string_exprt( const exprt &deref, const source_locationt &loc, diff --git a/unit/Makefile b/unit/Makefile index 0f81813e67e..a9f4da75522 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -20,6 +20,7 @@ SRC += unit_tests.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \ miniBDD_new.cpp \ + java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \ solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \ solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \ diff --git a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp new file mode 100644 index 00000000000..f7125f4fe17 --- /dev/null +++ b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp @@ -0,0 +1,59 @@ +/*******************************************************************\ + + Module: Java string library preprocess. + Test for converting an expression to a string expression. + + Author: Diffblue Limited. All rights reserved. + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +exprt convert_exprt_to_string_exprt_unit_test( + java_string_library_preprocesst &preprocess, + const exprt &deref, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &init_code) +{ + return preprocess.convert_exprt_to_string_exprt( + deref, loc, symbol_table, init_code); +} + +TEST_CASE("Convert exprt to string exprt") +{ + source_locationt loc; + symbol_tablet symbol_table; + namespacet ns(symbol_table); + code_blockt code; + java_string_library_preprocesst preprocess; + preprocess.add_string_type("java.lang.String", symbol_table); + symbol_typet java_string_type("java::java.lang.String"); + symbol_exprt expr("a", pointer_type(java_string_type)); + convert_exprt_to_string_exprt_unit_test( + preprocess, expr, loc, symbol_table, code); + register_language(new_java_bytecode_language); + + std::vector code_string; + for(auto op : code.operands()) + code_string.push_back(from_expr(ns, "", op)); + + REQUIRE(code_string.size()==7); + REQUIRE(code_string[0]=="int cprover_string_length$1;"); + REQUIRE(code_string[1]=="char cprover_string_array$2[INFINITY()];"); + REQUIRE(code_string[2]=="cprover_string_length$1 = a->length;"); + REQUIRE(code_string[3]=="__CPROVER_assume(!(a->data == null));"); + REQUIRE(code_string[4]=="cprover_string_array$2 = *a->data;"); + REQUIRE(code_string[5]=="struct __CPROVER_refined_string_type { int length; " + "char content[INFINITY()]; } cprover_string$3;"); + REQUIRE(code_string[6]=="cprover_string$3 = { .=cprover_string_length$1, " + ".=cprover_string_array$2 };"); +} From 52a08d8c34c44d8fe6ac8eedc6a325083437e034 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 30 Aug 2017 12:09:13 +0100 Subject: [PATCH 4/7] Setting string-max-length on strings test The solver can run out of memory in an unpredictable way when string max length is not set. --- regression/strings-smoke-tests/java_append_int/test.desc | 2 +- regression/strings-smoke-tests/java_append_object/test.desc | 2 +- regression/strings-smoke-tests/java_append_string/test.desc | 2 +- regression/strings-smoke-tests/java_char_array/test.desc | 2 +- regression/strings-smoke-tests/java_char_array_init/test.desc | 2 +- regression/strings-smoke-tests/java_char_at/test.desc | 2 +- regression/strings-smoke-tests/java_code_point/test.desc | 2 +- regression/strings-smoke-tests/java_compare/test.desc | 2 +- regression/strings-smoke-tests/java_concat/test.desc | 2 +- regression/strings-smoke-tests/java_delete/test.desc | 2 +- regression/strings-smoke-tests/java_delete_char_at/test.desc | 2 +- regression/strings-smoke-tests/java_empty/test.desc | 2 +- regression/strings-smoke-tests/java_float/test.desc | 2 +- regression/strings-smoke-tests/java_hash_code/test.desc | 2 +- regression/strings-smoke-tests/java_index_of/test.desc | 2 +- regression/strings-smoke-tests/java_index_of2/test.desc | 2 +- regression/strings-smoke-tests/java_index_of_char/test.desc | 2 +- regression/strings-smoke-tests/java_int_to_string/test1.desc | 2 +- regression/strings-smoke-tests/java_int_to_string/test2.desc | 2 +- regression/strings-smoke-tests/java_int_to_string/test4.desc | 2 +- .../strings-smoke-tests/java_int_to_string_knownbug/test.desc | 2 +- .../java_int_to_string_with_radix/test_binary3.desc | 2 +- .../java_int_to_string_with_radix/test_decimal.desc | 2 +- .../java_int_to_string_with_radix/test_octal1.desc | 2 +- .../java_int_to_string_with_radix_knownbug/test_binary.desc | 2 +- .../java_int_to_string_with_radix_knownbug/test_hex.desc | 2 +- .../java_int_to_string_with_radix_knownbug/test_octal.desc | 2 +- regression/strings-smoke-tests/java_intern/test.desc | 2 +- regression/strings-smoke-tests/java_last_index_of/test.desc | 2 +- regression/strings-smoke-tests/java_last_index_of2/test.desc | 2 +- .../strings-smoke-tests/java_last_index_of_char/test.desc | 2 +- regression/strings-smoke-tests/java_length/test.desc | 2 +- regression/strings-smoke-tests/java_length2/test.desc | 2 +- regression/strings-smoke-tests/java_long_to_string/test1.desc | 2 +- regression/strings-smoke-tests/java_long_to_string/test2.desc | 2 +- regression/strings-smoke-tests/java_long_to_string/test3.desc | 2 +- regression/strings-smoke-tests/java_long_to_string/test4.desc | 2 +- regression/strings-smoke-tests/java_long_to_string/test5.desc | 2 +- .../java_long_to_string_with_radix/test_binary1.desc | 2 +- .../java_long_to_string_with_radix/test_binary2.desc | 2 +- .../java_long_to_string_with_radix/test_binary3.desc | 2 +- .../java_long_to_string_with_radix/test_decimal.desc | 2 +- .../java_long_to_string_with_radix/test_hex2.desc | 2 +- regression/strings-smoke-tests/java_object_allocation/test.desc | 2 +- regression/strings-smoke-tests/java_parseint/test1.desc | 2 +- regression/strings-smoke-tests/java_parseint/test2.desc | 2 +- regression/strings-smoke-tests/java_parseint/test3.desc | 2 +- regression/strings-smoke-tests/java_parseint_knownbug/test.desc | 2 +- .../strings-smoke-tests/java_parseint_with_radix/test1.desc | 2 +- .../strings-smoke-tests/java_parseint_with_radix/test2.desc | 2 +- .../strings-smoke-tests/java_parseint_with_radix/test3.desc | 2 +- .../strings-smoke-tests/java_parseint_with_radix/test4.desc | 2 +- .../strings-smoke-tests/java_parseint_with_radix/test5.desc | 2 +- .../strings-smoke-tests/java_parseint_with_radix/test6.desc | 2 +- .../java_parseint_with_radix_knownbug/test.desc | 2 +- .../strings-smoke-tests/java_parselong/test_binary_min.desc | 2 +- .../strings-smoke-tests/java_parselong/test_decimal_max.desc | 2 +- .../strings-smoke-tests/java_parselong/test_decimal_min.desc | 2 +- regression/strings-smoke-tests/java_parselong/test_hex.desc | 2 +- regression/strings-smoke-tests/java_parselong/test_octal.desc | 2 +- regression/strings-smoke-tests/java_replace_char/test.desc | 2 +- regression/strings-smoke-tests/java_set_char_at/test.desc | 2 +- regression/strings-smoke-tests/java_starts_with/test.desc | 2 +- .../strings-smoke-tests/java_string_builder_length/test.desc | 2 +- regression/strings-smoke-tests/java_subsequence/test.desc | 2 +- regression/strings-smoke-tests/java_substring/test.desc | 2 +- regression/strings-smoke-tests/java_value_of_float_3/test.desc | 2 +- regression/strings-smoke-tests/java_value_of_float_4/test.desc | 2 +- regression/strings-smoke-tests/java_value_of_float_5/test.desc | 2 +- regression/strings/CharacterGetNumericValue/test.desc | 2 +- regression/strings/RegexMatches01/test.desc | 2 +- regression/strings/RegexMatches02/test.desc | 2 +- regression/strings/RegexSubstitution01/test.desc | 2 +- regression/strings/RegexSubstitution02/test.desc | 2 +- regression/strings/RegexSubstitution03/test.desc | 2 +- regression/strings/StaticCharMethods01/test.desc | 2 +- regression/strings/StaticCharMethods02/test.desc | 2 +- regression/strings/StaticCharMethods03/test.desc | 2 +- regression/strings/StaticCharMethods04/test.desc | 2 +- regression/strings/StaticCharMethods05/test.desc | 2 +- regression/strings/StaticCharMethods06/test.desc | 2 +- regression/strings/StringBuilderAppend01/test.desc | 2 +- regression/strings/StringBuilderAppend02/test.desc | 2 +- regression/strings/StringBuilderCapLen01/test.desc | 2 +- regression/strings/StringBuilderCapLen02/test.desc | 2 +- regression/strings/StringBuilderCapLen03/test.desc | 2 +- regression/strings/StringBuilderCapLen04/test.desc | 2 +- regression/strings/StringBuilderChars01/test.desc | 2 +- regression/strings/StringBuilderChars02/test.desc | 2 +- regression/strings/StringBuilderChars03/test.desc | 2 +- regression/strings/StringBuilderChars04/test.desc | 2 +- regression/strings/StringBuilderChars05/test.desc | 2 +- regression/strings/StringBuilderChars06/test.desc | 2 +- regression/strings/StringBuilderConstructors01/test.desc | 2 +- regression/strings/StringBuilderConstructors02/test.desc | 2 +- regression/strings/StringBuilderInsertDelete01/test.desc | 2 +- regression/strings/StringBuilderInsertDelete02/test.desc | 2 +- regression/strings/StringBuilderInsertDelete03/test.desc | 2 +- regression/strings/StringCompare01/test.desc | 2 +- regression/strings/StringCompare02/test.desc | 2 +- regression/strings/StringCompare03/test.desc | 2 +- regression/strings/StringCompare04/test.desc | 2 +- regression/strings/StringCompare05/test.desc | 2 +- regression/strings/StringConcatenation01/test.desc | 2 +- regression/strings/StringConcatenation02/test.desc | 2 +- regression/strings/StringConcatenation03/test.desc | 2 +- regression/strings/StringConcatenation04/test.desc | 2 +- regression/strings/StringConstructors01/test.desc | 2 +- regression/strings/StringConstructors02/test.desc | 2 +- regression/strings/StringConstructors03/test.desc | 2 +- regression/strings/StringConstructors04/test.desc | 2 +- regression/strings/StringConstructors05/test.desc | 2 +- regression/strings/StringContains01/test.desc | 2 +- regression/strings/StringContains02/test.desc | 2 +- regression/strings/StringIndexMethods01/test.desc | 2 +- regression/strings/StringIndexMethods02/test.desc | 2 +- regression/strings/StringIndexMethods03/test.desc | 2 +- regression/strings/StringIndexMethods04/test.desc | 2 +- regression/strings/StringIndexMethods05/test.desc | 2 +- regression/strings/StringMiscellaneous01/test.desc | 2 +- regression/strings/StringMiscellaneous02/test.desc | 2 +- regression/strings/StringMiscellaneous03/test.desc | 2 +- regression/strings/StringMiscellaneous04/test.desc | 2 +- regression/strings/StringStartEnd01/test.desc | 2 +- regression/strings/StringStartEnd03/test.desc | 2 +- regression/strings/StringValueOf01/test.desc | 2 +- regression/strings/StringValueOf02/test.desc | 2 +- regression/strings/StringValueOf03/test.desc | 2 +- regression/strings/StringValueOf04/test.desc | 2 +- regression/strings/StringValueOf05/test.desc | 2 +- regression/strings/StringValueOf06/test.desc | 2 +- regression/strings/StringValueOf07/test.desc | 2 +- regression/strings/StringValueOf09/test.desc | 2 +- regression/strings/StringValueOf10/test.desc | 2 +- regression/strings/SubString01/test.desc | 2 +- regression/strings/SubString02/test.desc | 2 +- regression/strings/SubString03/test.desc | 2 +- regression/strings/TokenTest01/test.desc | 2 +- regression/strings/TokenTest02/test.desc | 2 +- regression/strings/Validate01/test.desc | 2 +- regression/strings/Validate02/test.desc | 2 +- regression/strings/bug-test-gen-095/test.desc | 2 +- regression/strings/bug-test-gen-119-2/test.desc | 2 +- regression/strings/bug-test-gen-119/test.desc | 2 +- regression/strings/java_append_int/test.desc | 2 +- regression/strings/java_append_object/test.desc | 2 +- regression/strings/java_append_string/test.desc | 2 +- regression/strings/java_char_array/test.desc | 2 +- regression/strings/java_char_at/test.desc | 2 +- regression/strings/java_code_point/test.desc | 2 +- regression/strings/java_compare/test.desc | 2 +- regression/strings/java_concat/test.desc | 2 +- regression/strings/java_contains/test.desc | 2 +- regression/strings/java_delete/test.desc | 2 +- regression/strings/java_delete_char_at/test.desc | 2 +- regression/strings/java_easychair/test.desc | 2 +- regression/strings/java_empty/test.desc | 2 +- regression/strings/java_endswith/test.desc | 2 +- regression/strings/java_equal/test.desc | 2 +- regression/strings/java_float/test.desc | 2 +- regression/strings/java_hash_code/test.desc | 2 +- regression/strings/java_index_of/test.desc | 2 +- regression/strings/java_index_of_char/test.desc | 2 +- regression/strings/java_insert_multiple/test.desc | 2 +- regression/strings/test1/test.desc | 2 +- regression/strings/test2/test.desc | 2 +- regression/strings/test3.1/test.desc | 2 +- regression/strings/test3.2/test.desc | 2 +- regression/strings/test3.3/test.desc | 2 +- regression/strings/test3.4/test.desc | 2 +- regression/strings/test3/test.desc | 2 +- regression/strings/test4/test.desc | 2 +- regression/strings/test5/test.desc | 2 +- regression/strings/test_char_set/test.desc | 2 +- regression/strings/test_concat/test.desc | 2 +- regression/strings/test_contains/test.desc | 2 +- regression/strings/test_equal/test.desc | 2 +- regression/strings/test_index_of/test.desc | 2 +- regression/strings/test_int/test.desc | 2 +- regression/strings/test_pass1/test.desc | 2 +- regression/strings/test_pass_pc3/test.desc | 2 +- regression/strings/test_prefix/test.desc | 2 +- regression/strings/test_strlen/test.desc | 2 +- regression/strings/test_substring/test.desc | 2 +- regression/strings/test_suffix/test.desc | 2 +- 185 files changed, 185 insertions(+), 185 deletions(-) diff --git a/regression/strings-smoke-tests/java_append_int/test.desc b/regression/strings-smoke-tests/java_append_int/test.desc index e1455859470..17f38286a5b 100644 --- a/regression/strings-smoke-tests/java_append_int/test.desc +++ b/regression/strings-smoke-tests/java_append_int/test.desc @@ -1,6 +1,6 @@ FUTURE test_append_int.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_append_object/test.desc b/regression/strings-smoke-tests/java_append_object/test.desc index 787852963ed..62c1f56eea2 100644 --- a/regression/strings-smoke-tests/java_append_object/test.desc +++ b/regression/strings-smoke-tests/java_append_object/test.desc @@ -1,6 +1,6 @@ FUTURE test_append_object.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_append_string/test.desc b/regression/strings-smoke-tests/java_append_string/test.desc index 943ca820bcc..39c04f7031d 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 +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_char_array/test.desc b/regression/strings-smoke-tests/java_char_array/test.desc index d00a921a8c1..5c8a13eddd3 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 +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ .*assertion.* test_char_array.java line 9 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_char_array_init/test.desc b/regression/strings-smoke-tests/java_char_array_init/test.desc index 04096a8a984..1202bb035b6 100644 --- a/regression/strings-smoke-tests/java_char_array_init/test.desc +++ b/regression/strings-smoke-tests/java_char_array_init/test.desc @@ -1,6 +1,6 @@ FUTURE test_init.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_char_at/test.desc b/regression/strings-smoke-tests/java_char_at/test.desc index f2d5ecad6c7..2be2ab204ca 100644 --- a/regression/strings-smoke-tests/java_char_at/test.desc +++ b/regression/strings-smoke-tests/java_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_char_at.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_code_point/test.desc b/regression/strings-smoke-tests/java_code_point/test.desc index e3be9616fa5..aa7799f5170 100644 --- a/regression/strings-smoke-tests/java_code_point/test.desc +++ b/regression/strings-smoke-tests/java_code_point/test.desc @@ -1,6 +1,6 @@ CORE test_code_point.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_compare/test.desc b/regression/strings-smoke-tests/java_compare/test.desc index 9e6810476b9..a7d8151b55b 100644 --- a/regression/strings-smoke-tests/java_compare/test.desc +++ b/regression/strings-smoke-tests/java_compare/test.desc @@ -1,6 +1,6 @@ CORE test_compare.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_concat/test.desc b/regression/strings-smoke-tests/java_concat/test.desc index 2dcca464779..6063f361aa5 100644 --- a/regression/strings-smoke-tests/java_concat/test.desc +++ b/regression/strings-smoke-tests/java_concat/test.desc @@ -1,6 +1,6 @@ CORE test_concat.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 10.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_delete/test.desc b/regression/strings-smoke-tests/java_delete/test.desc index f0c0aedda91..dd957dd16bd 100644 --- a/regression/strings-smoke-tests/java_delete/test.desc +++ b/regression/strings-smoke-tests/java_delete/test.desc @@ -1,6 +1,6 @@ CORE test_delete.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_delete_char_at/test.desc b/regression/strings-smoke-tests/java_delete_char_at/test.desc index d415d16e9b6..cfd8b4778d1 100644 --- a/regression/strings-smoke-tests/java_delete_char_at/test.desc +++ b/regression/strings-smoke-tests/java_delete_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_delete_char_at.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_empty/test.desc b/regression/strings-smoke-tests/java_empty/test.desc index 181ff4ee5fd..e82479e301b 100644 --- a/regression/strings-smoke-tests/java_empty/test.desc +++ b/regression/strings-smoke-tests/java_empty/test.desc @@ -1,6 +1,6 @@ CORE test_empty.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_float/test.desc b/regression/strings-smoke-tests/java_float/test.desc index 427d1fca836..5f225af821a 100644 --- a/regression/strings-smoke-tests/java_float/test.desc +++ b/regression/strings-smoke-tests/java_float/test.desc @@ -1,6 +1,6 @@ FUTURE test_float.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_hash_code/test.desc b/regression/strings-smoke-tests/java_hash_code/test.desc index fc628393186..c00e466b8c4 100644 --- a/regression/strings-smoke-tests/java_hash_code/test.desc +++ b/regression/strings-smoke-tests/java_hash_code/test.desc @@ -1,6 +1,6 @@ CORE test_hash_code.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_index_of/test.desc b/regression/strings-smoke-tests/java_index_of/test.desc index e0e7de66561..3fdfa1ffc5d 100644 --- a/regression/strings-smoke-tests/java_index_of/test.desc +++ b/regression/strings-smoke-tests/java_index_of/test.desc @@ -1,6 +1,6 @@ CORE test_index_of.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_index_of2/test.desc b/regression/strings-smoke-tests/java_index_of2/test.desc index 09a7398d4b7..2c9d464054c 100644 --- a/regression/strings-smoke-tests/java_index_of2/test.desc +++ b/regression/strings-smoke-tests/java_index_of2/test.desc @@ -1,6 +1,6 @@ CORE test_index_of2.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings-smoke-tests/java_index_of_char/test.desc b/regression/strings-smoke-tests/java_index_of_char/test.desc index a95467b52e4..59d3310fa48 100644 --- a/regression/strings-smoke-tests/java_index_of_char/test.desc +++ b/regression/strings-smoke-tests/java_index_of_char/test.desc @@ -1,6 +1,6 @@ CORE test_index_of_char.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ 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 88f39d5eb12..318ec0fb224 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 +--refine-strings --string-max-length 1000 ^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 5ff465a846e..186a25d2d8b 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 +--refine-strings --string-max-length 1000 ^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 2106e2defa5..abba00197d9 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 +--refine-strings --string-max-length 1000 ^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 b1ed3bac24c..416e3caec69 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 +--refine-strings --string-max-length 1000 ^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 a4e6438623e..c24b0bbd20b 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 +--refine-strings --string-max-length 1000 ^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 7226334925f..de106c0cbf5 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 +--refine-strings --string-max-length 1000 ^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 9afe7b06279..f4b1e2b219d 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 +--refine-strings --string-max-length 1000 ^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 d8959c329a7..20efbdfa239 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 +--refine-strings --string-max-length 1000 ^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 324cd50051e..69dbaba276d 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 +--refine-strings --string-max-length 1000 ^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 ce0a5607186..7cfc1c19f24 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 +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_intern/test.desc b/regression/strings-smoke-tests/java_intern/test.desc index c8d0eea43bd..58c51bce301 100644 --- a/regression/strings-smoke-tests/java_intern/test.desc +++ b/regression/strings-smoke-tests/java_intern/test.desc @@ -1,6 +1,6 @@ CORE test_intern.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_last_index_of/test.desc b/regression/strings-smoke-tests/java_last_index_of/test.desc index 381078254cd..afda4875b71 100644 --- a/regression/strings-smoke-tests/java_last_index_of/test.desc +++ b/regression/strings-smoke-tests/java_last_index_of/test.desc @@ -1,6 +1,6 @@ CORE test_last_index_of.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_last_index_of2/test.desc b/regression/strings-smoke-tests/java_last_index_of2/test.desc index 5348cbe7fce..28af8ca48e6 100644 --- a/regression/strings-smoke-tests/java_last_index_of2/test.desc +++ b/regression/strings-smoke-tests/java_last_index_of2/test.desc @@ -1,6 +1,6 @@ CORE test_last_index_of2.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_last_index_of_char/test.desc b/regression/strings-smoke-tests/java_last_index_of_char/test.desc index aa88fc5f6ef..aa59690787c 100644 --- a/regression/strings-smoke-tests/java_last_index_of_char/test.desc +++ b/regression/strings-smoke-tests/java_last_index_of_char/test.desc @@ -1,6 +1,6 @@ CORE test_last_index_of_char.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_length/test.desc b/regression/strings-smoke-tests/java_length/test.desc index 60c360eecb8..7802a6d675b 100644 --- a/regression/strings-smoke-tests/java_length/test.desc +++ b/regression/strings-smoke-tests/java_length/test.desc @@ -1,6 +1,6 @@ CORE test_length.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings-smoke-tests/java_length2/test.desc b/regression/strings-smoke-tests/java_length2/test.desc index e473b51d950..4647009f3cf 100644 --- a/regression/strings-smoke-tests/java_length2/test.desc +++ b/regression/strings-smoke-tests/java_length2/test.desc @@ -1,6 +1,6 @@ FUTURE test.class ---refine-strings --function test.check +--refine-strings --string-max-length 1000 --function test.check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ 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 88f39d5eb12..318ec0fb224 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 +--refine-strings --string-max-length 1000 ^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 a4f7d628251..1f6206fafd9 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 +--refine-strings --string-max-length 1000 ^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 5e96ef2ae6d..ea8df93a51f 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 +--refine-strings --string-max-length 1000 ^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 aa12d7732f1..13dd59d749e 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 +--refine-strings --string-max-length 1000 ^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 08531bc36e0..524a176db3f 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 +--refine-strings --string-max-length 1000 ^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 bfdddd48786..6f9c074face 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 +--refine-strings --string-max-length 1000 ^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 7cabc082721..0729b99b895 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 +--refine-strings --string-max-length 1000 ^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 cd10cf15647..d87aaaecb3d 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 +--refine-strings --string-max-length 1000 ^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 7226334925f..de106c0cbf5 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 +--refine-strings --string-max-length 1000 ^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 d21d067e620..89c4928e147 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 +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_object_allocation/test.desc b/regression/strings-smoke-tests/java_object_allocation/test.desc index fe10bf71202..bac94ff5307 100644 --- a/regression/strings-smoke-tests/java_object_allocation/test.desc +++ b/regression/strings-smoke-tests/java_object_allocation/test.desc @@ -1,6 +1,6 @@ CORE test.class ---refine-strings --show-goto-functions +--refine-strings --string-max-length 1000 --show-goto-functions // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/strings-smoke-tests/java_parseint/test1.desc b/regression/strings-smoke-tests/java_parseint/test1.desc index 5d48a0d6aad..5307e54205f 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 +--refine-strings --string-max-length 1000 ^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 16f6de423bf..b61e0912459 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 +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint/test3.desc b/regression/strings-smoke-tests/java_parseint/test3.desc index bb643427dd2..06f5f081dfd 100644 --- a/regression/strings-smoke-tests/java_parseint/test3.desc +++ b/regression/strings-smoke-tests/java_parseint/test3.desc @@ -1,6 +1,6 @@ CORE Test3.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 7.* FAILURE$ diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc index 76feb55c355..f66e48584e2 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 +--refine-strings --string-max-length 1000 ^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 0ab380c3cde..07502efb78d 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 +--refine-strings --string-max-length 1000 ^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 0b6a1a2dd97..0755c7a91cf 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 +--refine-strings --string-max-length 1000 ^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 7b68147d90b..ef8136a08ab 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 +--refine-strings --string-max-length 1000 ^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 8c775500aaa..7934721b588 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 +--refine-strings --string-max-length 1000 ^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 2b0338b1c0c..a829acab959 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 +--refine-strings --string-max-length 1000 ^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 71b3d8423e4..d3dadcebc8f 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 +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc index b0af402d3bd..485ca577bcc 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc +++ b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Test2.class ---refine-strings +--refine-strings --string-max-length 1000 ^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 9fa189f76cf..ce64f5e6db6 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 +--refine-strings --string-max-length 1000 ^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 25795287397..1e195fcaaf2 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 +--refine-strings --string-max-length 1000 ^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 95a847bf862..7f97fa3a95e 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 +--refine-strings --string-max-length 1000 ^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 efae1994f9e..c21910790b5 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 +--refine-strings --string-max-length 1000 ^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 72dc00545cb..152484b2d2a 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 +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_replace_char/test.desc b/regression/strings-smoke-tests/java_replace_char/test.desc index 5c336326e5d..9cf3b2fbced 100644 --- a/regression/strings-smoke-tests/java_replace_char/test.desc +++ b/regression/strings-smoke-tests/java_replace_char/test.desc @@ -1,6 +1,6 @@ CORE test_replace_char.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_set_char_at/test.desc b/regression/strings-smoke-tests/java_set_char_at/test.desc index 1c471d0194a..72f26dda255 100644 --- a/regression/strings-smoke-tests/java_set_char_at/test.desc +++ b/regression/strings-smoke-tests/java_set_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_set_char_at.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_starts_with/test.desc b/regression/strings-smoke-tests/java_starts_with/test.desc index ec6b84102f2..5c62d2f2718 100644 --- a/regression/strings-smoke-tests/java_starts_with/test.desc +++ b/regression/strings-smoke-tests/java_starts_with/test.desc @@ -1,6 +1,6 @@ CORE test_starts_with.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_string_builder_length/test.desc b/regression/strings-smoke-tests/java_string_builder_length/test.desc index 2a37e02a36c..3ad293630e3 100644 --- a/regression/strings-smoke-tests/java_string_builder_length/test.desc +++ b/regression/strings-smoke-tests/java_string_builder_length/test.desc @@ -1,6 +1,6 @@ CORE test_sb_length.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_subsequence/test.desc b/regression/strings-smoke-tests/java_subsequence/test.desc index df3cc28619f..3f4941d15dd 100644 --- a/regression/strings-smoke-tests/java_subsequence/test.desc +++ b/regression/strings-smoke-tests/java_subsequence/test.desc @@ -1,6 +1,6 @@ CORE test_subsequence.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_substring/test.desc b/regression/strings-smoke-tests/java_substring/test.desc index 26ec800cfac..9faeee00d73 100644 --- a/regression/strings-smoke-tests/java_substring/test.desc +++ b/regression/strings-smoke-tests/java_substring/test.desc @@ -1,6 +1,6 @@ CORE test_substring.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings-smoke-tests/java_value_of_float_3/test.desc b/regression/strings-smoke-tests/java_value_of_float_3/test.desc index 771fdebe7cc..2c28aafd4d9 100644 --- a/regression/strings-smoke-tests/java_value_of_float_3/test.desc +++ b/regression/strings-smoke-tests/java_value_of_float_3/test.desc @@ -1,6 +1,6 @@ KNOWNBUG test.class ---refine-strings --function test.check +--refine-strings --string-max-length 1000 --function test.check ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 7 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_value_of_float_4/test.desc b/regression/strings-smoke-tests/java_value_of_float_4/test.desc index 7f1e0f8819a..a85559c560e 100644 --- a/regression/strings-smoke-tests/java_value_of_float_4/test.desc +++ b/regression/strings-smoke-tests/java_value_of_float_4/test.desc @@ -1,6 +1,6 @@ THOROUGH test.class ---refine-strings --function test.check +--refine-strings --string-max-length 1000 --function test.check ^EXIT=10$ ^SIGNAL=0$ assertion.* test.java line 8 .* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_value_of_float_5/test.desc b/regression/strings-smoke-tests/java_value_of_float_5/test.desc index 7a279ade453..07a7bd7edde 100644 --- a/regression/strings-smoke-tests/java_value_of_float_5/test.desc +++ b/regression/strings-smoke-tests/java_value_of_float_5/test.desc @@ -1,6 +1,6 @@ THOROUGH test.class ---refine-strings --function test.check +--refine-strings --string-max-length 1000 --function test.check ^EXIT=10$ ^SIGNAL=0$ assertion.* file test.java line 6 .* SUCCESS$ diff --git a/regression/strings/CharacterGetNumericValue/test.desc b/regression/strings/CharacterGetNumericValue/test.desc index 9f34df46fd6..30ce2644914 100644 --- a/regression/strings/CharacterGetNumericValue/test.desc +++ b/regression/strings/CharacterGetNumericValue/test.desc @@ -1,6 +1,6 @@ CORE test.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ assertion at file test.java line 8 .* SUCCESS$ diff --git a/regression/strings/RegexMatches01/test.desc b/regression/strings/RegexMatches01/test.desc index e4259466e6b..4a95eb71ab0 100644 --- a/regression/strings/RegexMatches01/test.desc +++ b/regression/strings/RegexMatches01/test.desc @@ -1,6 +1,6 @@ FUTURE RegexMatches01.class ---refine-strings --unwind 100 +--refine-strings --string-max-length 1000 --unwind 100 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/RegexMatches02/test.desc b/regression/strings/RegexMatches02/test.desc index 006922c3d6a..9b754d1a449 100644 --- a/regression/strings/RegexMatches02/test.desc +++ b/regression/strings/RegexMatches02/test.desc @@ -1,6 +1,6 @@ FUTURE RegexMatches02.class ---refine-strings --unwind 100 +--refine-strings --string-max-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/RegexSubstitution01/test.desc b/regression/strings/RegexSubstitution01/test.desc index ccf24b2e8fa..2d24db23d16 100644 --- a/regression/strings/RegexSubstitution01/test.desc +++ b/regression/strings/RegexSubstitution01/test.desc @@ -1,6 +1,6 @@ FUTURE RegexSubstitution01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/RegexSubstitution02/test.desc b/regression/strings/RegexSubstitution02/test.desc index 7064bcc0333..2caa11a3221 100644 --- a/regression/strings/RegexSubstitution02/test.desc +++ b/regression/strings/RegexSubstitution02/test.desc @@ -1,6 +1,6 @@ FUTURE RegexSubstitution02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/RegexSubstitution03/test.desc b/regression/strings/RegexSubstitution03/test.desc index 4b0d5739c42..9f141b34217 100644 --- a/regression/strings/RegexSubstitution03/test.desc +++ b/regression/strings/RegexSubstitution03/test.desc @@ -1,6 +1,6 @@ FUTURE RegexSubstitution03.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StaticCharMethods01/test.desc b/regression/strings/StaticCharMethods01/test.desc index 0440fc98273..35c0f3a7f1e 100644 --- a/regression/strings/StaticCharMethods01/test.desc +++ b/regression/strings/StaticCharMethods01/test.desc @@ -1,6 +1,6 @@ CORE StaticCharMethods01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StaticCharMethods02/test.desc b/regression/strings/StaticCharMethods02/test.desc index d537da812c9..70e90e4115a 100644 --- a/regression/strings/StaticCharMethods02/test.desc +++ b/regression/strings/StaticCharMethods02/test.desc @@ -1,6 +1,6 @@ CORE StaticCharMethods02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StaticCharMethods03/test.desc b/regression/strings/StaticCharMethods03/test.desc index 174071ed1da..712044431a5 100644 --- a/regression/strings/StaticCharMethods03/test.desc +++ b/regression/strings/StaticCharMethods03/test.desc @@ -1,6 +1,6 @@ CORE StaticCharMethods03.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/regression/strings/StaticCharMethods04/test.desc b/regression/strings/StaticCharMethods04/test.desc index ecc807f2d31..ee66116b0fa 100644 --- a/regression/strings/StaticCharMethods04/test.desc +++ b/regression/strings/StaticCharMethods04/test.desc @@ -1,6 +1,6 @@ CORE StaticCharMethods04.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StaticCharMethods05/test.desc b/regression/strings/StaticCharMethods05/test.desc index f8abd67fc57..e6f2a0e6ee8 100644 --- a/regression/strings/StaticCharMethods05/test.desc +++ b/regression/strings/StaticCharMethods05/test.desc @@ -1,6 +1,6 @@ CORE StaticCharMethods05.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ null-pointer-exception\.14\] Throw null: FAILURE diff --git a/regression/strings/StaticCharMethods06/test.desc b/regression/strings/StaticCharMethods06/test.desc index 3caa6a7b878..b0047376ea1 100644 --- a/regression/strings/StaticCharMethods06/test.desc +++ b/regression/strings/StaticCharMethods06/test.desc @@ -1,6 +1,6 @@ FUTURE StaticCharMethods06.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderAppend01/test.desc b/regression/strings/StringBuilderAppend01/test.desc index d0207fc9ea7..925b862d11e 100644 --- a/regression/strings/StringBuilderAppend01/test.desc +++ b/regression/strings/StringBuilderAppend01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderAppend01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderAppend02/test.desc b/regression/strings/StringBuilderAppend02/test.desc index 70357b670d8..d0ef683f373 100644 --- a/regression/strings/StringBuilderAppend02/test.desc +++ b/regression/strings/StringBuilderAppend02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderAppend02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderCapLen01/test.desc b/regression/strings/StringBuilderCapLen01/test.desc index 4186f2534ac..12d6f321534 100644 --- a/regression/strings/StringBuilderCapLen01/test.desc +++ b/regression/strings/StringBuilderCapLen01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderCapLen02/test.desc b/regression/strings/StringBuilderCapLen02/test.desc index f9db006ed0b..68183ab0c8b 100644 --- a/regression/strings/StringBuilderCapLen02/test.desc +++ b/regression/strings/StringBuilderCapLen02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderCapLen03/test.desc b/regression/strings/StringBuilderCapLen03/test.desc index c35dfb33871..98f5aa74306 100644 --- a/regression/strings/StringBuilderCapLen03/test.desc +++ b/regression/strings/StringBuilderCapLen03/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen03.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderCapLen04/test.desc b/regression/strings/StringBuilderCapLen04/test.desc index 78930851e45..2bf31910709 100644 --- a/regression/strings/StringBuilderCapLen04/test.desc +++ b/regression/strings/StringBuilderCapLen04/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderCapLen04.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderChars01/test.desc b/regression/strings/StringBuilderChars01/test.desc index 48acfb25a5d..df8aa84cc74 100644 --- a/regression/strings/StringBuilderChars01/test.desc +++ b/regression/strings/StringBuilderChars01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars01.class ---refine-strings --unwind 100 +--refine-strings --string-max-length 1000 --unwind 100 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderChars02/test.desc b/regression/strings/StringBuilderChars02/test.desc index d9006ab74ba..991d4cca0eb 100644 --- a/regression/strings/StringBuilderChars02/test.desc +++ b/regression/strings/StringBuilderChars02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars02.class ---refine-strings --unwind 100 +--refine-strings --string-max-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderChars03/test.desc b/regression/strings/StringBuilderChars03/test.desc index d6f1cb4155c..6ec91ba3f69 100644 --- a/regression/strings/StringBuilderChars03/test.desc +++ b/regression/strings/StringBuilderChars03/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars03.class ---refine-strings --unwind 100 +--refine-strings --string-max-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderChars04/test.desc b/regression/strings/StringBuilderChars04/test.desc index 37009795a48..802a60269ec 100644 --- a/regression/strings/StringBuilderChars04/test.desc +++ b/regression/strings/StringBuilderChars04/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars04.class ---refine-strings --unwind 100 +--refine-strings --string-max-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderChars05/test.desc b/regression/strings/StringBuilderChars05/test.desc index 49aed9d48fd..fdb12721623 100644 --- a/regression/strings/StringBuilderChars05/test.desc +++ b/regression/strings/StringBuilderChars05/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars05.class ---refine-strings --unwind 100 +--refine-strings --string-max-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderChars06/test.desc b/regression/strings/StringBuilderChars06/test.desc index 5ccf470590e..fbb6f1bb87d 100644 --- a/regression/strings/StringBuilderChars06/test.desc +++ b/regression/strings/StringBuilderChars06/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderChars06.class ---refine-strings --unwind 100 +--refine-strings --string-max-length 1000 --unwind 100 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderConstructors01/test.desc b/regression/strings/StringBuilderConstructors01/test.desc index 3e27d46c329..39bcec0b205 100644 --- a/regression/strings/StringBuilderConstructors01/test.desc +++ b/regression/strings/StringBuilderConstructors01/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringBuilderConstructors01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderConstructors02/test.desc b/regression/strings/StringBuilderConstructors02/test.desc index f6c0cded34e..889460297ea 100644 --- a/regression/strings/StringBuilderConstructors02/test.desc +++ b/regression/strings/StringBuilderConstructors02/test.desc @@ -1,6 +1,6 @@ KNOWNBUG StringBuilderConstructors02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderInsertDelete01/test.desc b/regression/strings/StringBuilderInsertDelete01/test.desc index b2f927ad3b7..5c347f7792a 100644 --- a/regression/strings/StringBuilderInsertDelete01/test.desc +++ b/regression/strings/StringBuilderInsertDelete01/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderInsertDelete01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringBuilderInsertDelete02/test.desc b/regression/strings/StringBuilderInsertDelete02/test.desc index 1e67f7eb3c0..576410049d8 100644 --- a/regression/strings/StringBuilderInsertDelete02/test.desc +++ b/regression/strings/StringBuilderInsertDelete02/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderInsertDelete02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringBuilderInsertDelete03/test.desc b/regression/strings/StringBuilderInsertDelete03/test.desc index 084038f4465..934b4de8579 100644 --- a/regression/strings/StringBuilderInsertDelete03/test.desc +++ b/regression/strings/StringBuilderInsertDelete03/test.desc @@ -1,6 +1,6 @@ FUTURE StringBuilderInsertDelete03.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringCompare01/test.desc b/regression/strings/StringCompare01/test.desc index 2140f3a0c48..5e60d31b865 100644 --- a/regression/strings/StringCompare01/test.desc +++ b/regression/strings/StringCompare01/test.desc @@ -1,6 +1,6 @@ FUTURE StringCompare01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringCompare02/test.desc b/regression/strings/StringCompare02/test.desc index d20bfb7eb5c..2970a511914 100644 --- a/regression/strings/StringCompare02/test.desc +++ b/regression/strings/StringCompare02/test.desc @@ -1,6 +1,6 @@ CORE StringCompare02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 12 .* FAILURE$ diff --git a/regression/strings/StringCompare03/test.desc b/regression/strings/StringCompare03/test.desc index afc9b9b5307..15b7f91b1fe 100644 --- a/regression/strings/StringCompare03/test.desc +++ b/regression/strings/StringCompare03/test.desc @@ -1,6 +1,6 @@ CORE StringCompare03.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 12 .* FAILURE$ diff --git a/regression/strings/StringCompare04/test.desc b/regression/strings/StringCompare04/test.desc index afc70f4933b..176142e064e 100644 --- a/regression/strings/StringCompare04/test.desc +++ b/regression/strings/StringCompare04/test.desc @@ -1,6 +1,6 @@ CORE StringCompare04.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringCompare05/test.desc b/regression/strings/StringCompare05/test.desc index 0f24821dee6..a182fecf008 100644 --- a/regression/strings/StringCompare05/test.desc +++ b/regression/strings/StringCompare05/test.desc @@ -1,6 +1,6 @@ CORE StringCompare05.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConcatenation01/test.desc b/regression/strings/StringConcatenation01/test.desc index 29244c24734..09414c5a3f6 100644 --- a/regression/strings/StringConcatenation01/test.desc +++ b/regression/strings/StringConcatenation01/test.desc @@ -1,6 +1,6 @@ CORE StringConcatenation01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringConcatenation02/test.desc b/regression/strings/StringConcatenation02/test.desc index ad9402eaec9..90c299fea1a 100644 --- a/regression/strings/StringConcatenation02/test.desc +++ b/regression/strings/StringConcatenation02/test.desc @@ -1,6 +1,6 @@ CORE StringConcatenation02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConcatenation03/test.desc b/regression/strings/StringConcatenation03/test.desc index c5798d1ae1d..2dd24800903 100644 --- a/regression/strings/StringConcatenation03/test.desc +++ b/regression/strings/StringConcatenation03/test.desc @@ -1,6 +1,6 @@ CORE StringConcatenation03.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConcatenation04/test.desc b/regression/strings/StringConcatenation04/test.desc index a781c7887b1..5fbdea80b8a 100644 --- a/regression/strings/StringConcatenation04/test.desc +++ b/regression/strings/StringConcatenation04/test.desc @@ -1,6 +1,6 @@ CORE StringConcatenation04.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 8 .* FAILURE$ diff --git a/regression/strings/StringConstructors01/test.desc b/regression/strings/StringConstructors01/test.desc index b1465868c19..6c3fdfb7af8 100644 --- a/regression/strings/StringConstructors01/test.desc +++ b/regression/strings/StringConstructors01/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringConstructors02/test.desc b/regression/strings/StringConstructors02/test.desc index 37838aafbc9..f39f6dbcf25 100644 --- a/regression/strings/StringConstructors02/test.desc +++ b/regression/strings/StringConstructors02/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConstructors03/test.desc b/regression/strings/StringConstructors03/test.desc index 10193fc66c2..3df88975a3e 100644 --- a/regression/strings/StringConstructors03/test.desc +++ b/regression/strings/StringConstructors03/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors03.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConstructors04/test.desc b/regression/strings/StringConstructors04/test.desc index 2e6e88fa862..9e889d73812 100644 --- a/regression/strings/StringConstructors04/test.desc +++ b/regression/strings/StringConstructors04/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors04.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringConstructors05/test.desc b/regression/strings/StringConstructors05/test.desc index a3c6a6c0437..80b0ee57307 100644 --- a/regression/strings/StringConstructors05/test.desc +++ b/regression/strings/StringConstructors05/test.desc @@ -1,6 +1,6 @@ FUTURE StringConstructors05.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringContains01/test.desc b/regression/strings/StringContains01/test.desc index 2e66f73126f..6a299037d6f 100644 --- a/regression/strings/StringContains01/test.desc +++ b/regression/strings/StringContains01/test.desc @@ -1,6 +1,6 @@ FUTURE test.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringContains02/test.desc b/regression/strings/StringContains02/test.desc index 2e66f73126f..6a299037d6f 100644 --- a/regression/strings/StringContains02/test.desc +++ b/regression/strings/StringContains02/test.desc @@ -1,6 +1,6 @@ FUTURE test.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/StringIndexMethods01/test.desc b/regression/strings/StringIndexMethods01/test.desc index 4bdc0d39b71..96c8fb19994 100644 --- a/regression/strings/StringIndexMethods01/test.desc +++ b/regression/strings/StringIndexMethods01/test.desc @@ -1,6 +1,6 @@ THOROUGH StringIndexMethods01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringIndexMethods02/test.desc b/regression/strings/StringIndexMethods02/test.desc index 05518537f78..69250ebae1d 100644 --- a/regression/strings/StringIndexMethods02/test.desc +++ b/regression/strings/StringIndexMethods02/test.desc @@ -1,6 +1,6 @@ CORE StringIndexMethods02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/regression/strings/StringIndexMethods03/test.desc b/regression/strings/StringIndexMethods03/test.desc index 17a62282b22..ce9b8e5a339 100644 --- a/regression/strings/StringIndexMethods03/test.desc +++ b/regression/strings/StringIndexMethods03/test.desc @@ -1,6 +1,6 @@ CORE StringIndexMethods03.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/regression/strings/StringIndexMethods04/test.desc b/regression/strings/StringIndexMethods04/test.desc index 5902a92be18..f63d2152f09 100644 --- a/regression/strings/StringIndexMethods04/test.desc +++ b/regression/strings/StringIndexMethods04/test.desc @@ -1,6 +1,6 @@ CORE StringIndexMethods04.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/regression/strings/StringIndexMethods05/test.desc b/regression/strings/StringIndexMethods05/test.desc index 29dee098ac7..243c43e965a 100644 --- a/regression/strings/StringIndexMethods05/test.desc +++ b/regression/strings/StringIndexMethods05/test.desc @@ -1,6 +1,6 @@ FUTURE StringIndexMethods05.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/regression/strings/StringMiscellaneous01/test.desc b/regression/strings/StringMiscellaneous01/test.desc index 624c8028cb3..6443a3f37d8 100644 --- a/regression/strings/StringMiscellaneous01/test.desc +++ b/regression/strings/StringMiscellaneous01/test.desc @@ -1,6 +1,6 @@ FUTURE StringMiscellaneous01.class ---refine-strings --unwind 30 +--refine-strings --string-max-length 1000 --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringMiscellaneous02/test.desc b/regression/strings/StringMiscellaneous02/test.desc index 7fd0118b93a..987299cb4af 100644 --- a/regression/strings/StringMiscellaneous02/test.desc +++ b/regression/strings/StringMiscellaneous02/test.desc @@ -1,6 +1,6 @@ CORE StringMiscellaneous02.class ---refine-strings --unwind 30 +--refine-strings --string-max-length 1000 --unwind 30 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 6 .* FAILURE$ diff --git a/regression/strings/StringMiscellaneous03/test.desc b/regression/strings/StringMiscellaneous03/test.desc index d19fcdfaa5e..7a20ece6152 100644 --- a/regression/strings/StringMiscellaneous03/test.desc +++ b/regression/strings/StringMiscellaneous03/test.desc @@ -1,6 +1,6 @@ CORE StringMiscellaneous03.class ---refine-strings --unwind 30 +--refine-strings --string-max-length 1000 --unwind 30 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 11 .* FAILURE$ diff --git a/regression/strings/StringMiscellaneous04/test.desc b/regression/strings/StringMiscellaneous04/test.desc index 9eb355cd0d2..5657433d8c7 100644 --- a/regression/strings/StringMiscellaneous04/test.desc +++ b/regression/strings/StringMiscellaneous04/test.desc @@ -1,6 +1,6 @@ CORE StringMiscellaneous04.class ---refine-strings --unwind 30 +--refine-strings --string-max-length 1000 --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringStartEnd01/test.desc b/regression/strings/StringStartEnd01/test.desc index 123429bd623..21181368d56 100644 --- a/regression/strings/StringStartEnd01/test.desc +++ b/regression/strings/StringStartEnd01/test.desc @@ -1,6 +1,6 @@ THOROUGH StringStartEnd01.class ---refine-strings --unwind 30 +--refine-strings --string-max-length 1000 --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringStartEnd03/test.desc b/regression/strings/StringStartEnd03/test.desc index b7727fd8b91..ad05b3a1904 100644 --- a/regression/strings/StringStartEnd03/test.desc +++ b/regression/strings/StringStartEnd03/test.desc @@ -1,6 +1,6 @@ THOROUGH StringStartEnd03.class ---refine-strings --unwind 15 +--refine-strings --string-max-length 1000 --unwind 15 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 13 .* FAILURE$ diff --git a/regression/strings/StringValueOf01/test.desc b/regression/strings/StringValueOf01/test.desc index c6098401ba0..19dc04f76f3 100644 --- a/regression/strings/StringValueOf01/test.desc +++ b/regression/strings/StringValueOf01/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/StringValueOf02/test.desc b/regression/strings/StringValueOf02/test.desc index 906d983e34f..3640d830371 100644 --- a/regression/strings/StringValueOf02/test.desc +++ b/regression/strings/StringValueOf02/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/regression/strings/StringValueOf03/test.desc b/regression/strings/StringValueOf03/test.desc index ffde4e2de6f..788c99b840c 100644 --- a/regression/strings/StringValueOf03/test.desc +++ b/regression/strings/StringValueOf03/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf03.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/regression/strings/StringValueOf04/test.desc b/regression/strings/StringValueOf04/test.desc index e73f1492261..1628779f989 100644 --- a/regression/strings/StringValueOf04/test.desc +++ b/regression/strings/StringValueOf04/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf04.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/regression/strings/StringValueOf05/test.desc b/regression/strings/StringValueOf05/test.desc index 494b6779cc2..281e1787b98 100644 --- a/regression/strings/StringValueOf05/test.desc +++ b/regression/strings/StringValueOf05/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf05.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/regression/strings/StringValueOf06/test.desc b/regression/strings/StringValueOf06/test.desc index 29fe55a89f2..23d219415d2 100644 --- a/regression/strings/StringValueOf06/test.desc +++ b/regression/strings/StringValueOf06/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf06.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/regression/strings/StringValueOf07/test.desc b/regression/strings/StringValueOf07/test.desc index e1d94ae7025..af73181177d 100644 --- a/regression/strings/StringValueOf07/test.desc +++ b/regression/strings/StringValueOf07/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf07.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 8 .* FAILURE$ diff --git a/regression/strings/StringValueOf09/test.desc b/regression/strings/StringValueOf09/test.desc index d1bad9a12b6..d3387709636 100644 --- a/regression/strings/StringValueOf09/test.desc +++ b/regression/strings/StringValueOf09/test.desc @@ -1,6 +1,6 @@ THOROUGH StringValueOf09.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/regression/strings/StringValueOf10/test.desc b/regression/strings/StringValueOf10/test.desc index 3f8c5d6d60f..90a38f97794 100644 --- a/regression/strings/StringValueOf10/test.desc +++ b/regression/strings/StringValueOf10/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf10.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/SubString01/test.desc b/regression/strings/SubString01/test.desc index 975eaa118f3..f77f04ee2c7 100644 --- a/regression/strings/SubString01/test.desc +++ b/regression/strings/SubString01/test.desc @@ -1,6 +1,6 @@ CORE SubString01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/SubString02/test.desc b/regression/strings/SubString02/test.desc index 2003191a147..c487dd9ab17 100644 --- a/regression/strings/SubString02/test.desc +++ b/regression/strings/SubString02/test.desc @@ -1,6 +1,6 @@ CORE SubString02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/regression/strings/SubString03/test.desc b/regression/strings/SubString03/test.desc index 22143857480..48075842027 100644 --- a/regression/strings/SubString03/test.desc +++ b/regression/strings/SubString03/test.desc @@ -1,6 +1,6 @@ CORE SubString03.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/regression/strings/TokenTest01/test.desc b/regression/strings/TokenTest01/test.desc index 122e6a8830a..921e312b85e 100644 --- a/regression/strings/TokenTest01/test.desc +++ b/regression/strings/TokenTest01/test.desc @@ -1,6 +1,6 @@ FUTURE TokenTest01.class ---refine-strings --unwind 30 +--refine-strings --string-max-length 1000 --unwind 30 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/TokenTest02/test.desc b/regression/strings/TokenTest02/test.desc index 6d1dabed602..0cc1d6a0d26 100644 --- a/regression/strings/TokenTest02/test.desc +++ b/regression/strings/TokenTest02/test.desc @@ -1,6 +1,6 @@ FUTURE TokenTest02.class ---refine-strings --unwind 15 +--refine-strings --string-max-length 1000 --unwind 15 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/Validate01/test.desc b/regression/strings/Validate01/test.desc index 649136a2956..7893ef03d1b 100644 --- a/regression/strings/Validate01/test.desc +++ b/regression/strings/Validate01/test.desc @@ -1,6 +1,6 @@ FUTURE Validate01.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/Validate02/test.desc b/regression/strings/Validate02/test.desc index 22251c38a95..36385610844 100644 --- a/regression/strings/Validate02/test.desc +++ b/regression/strings/Validate02/test.desc @@ -1,6 +1,6 @@ FUTURE Validate02.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/bug-test-gen-095/test.desc b/regression/strings/bug-test-gen-095/test.desc index 9f39bb3f26c..9c690be3298 100644 --- a/regression/strings/bug-test-gen-095/test.desc +++ b/regression/strings/bug-test-gen-095/test.desc @@ -1,6 +1,6 @@ FUTURE test.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ \[.*assertion\.1\] .* line 8 .* FAILURE diff --git a/regression/strings/bug-test-gen-119-2/test.desc b/regression/strings/bug-test-gen-119-2/test.desc index 312601b835d..447be05df73 100644 --- a/regression/strings/bug-test-gen-119-2/test.desc +++ b/regression/strings/bug-test-gen-119-2/test.desc @@ -1,6 +1,6 @@ CORE StringValueOfLong.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/bug-test-gen-119/test.desc b/regression/strings/bug-test-gen-119/test.desc index c5672ad9702..22bd78b3cac 100644 --- a/regression/strings/bug-test-gen-119/test.desc +++ b/regression/strings/bug-test-gen-119/test.desc @@ -1,6 +1,6 @@ CORE StringValueOfBool.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/java_append_int/test.desc b/regression/strings/java_append_int/test.desc index 1d3e387d278..8edf69c9fec 100644 --- a/regression/strings/java_append_int/test.desc +++ b/regression/strings/java_append_int/test.desc @@ -1,6 +1,6 @@ KNOWNBUG test_append_int.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 9.* FAILURE$ diff --git a/regression/strings/java_append_object/test.desc b/regression/strings/java_append_object/test.desc index 23ad1a81be4..2af06f2686a 100644 --- a/regression/strings/java_append_object/test.desc +++ b/regression/strings/java_append_object/test.desc @@ -1,6 +1,6 @@ KNOWNBUG test_append_object.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 15.* FAILURE$ diff --git a/regression/strings/java_append_string/test.desc b/regression/strings/java_append_string/test.desc index 7b6ea8ccae7..cb881ab83d9 100644 --- a/regression/strings/java_append_string/test.desc +++ b/regression/strings/java_append_string/test.desc @@ -1,6 +1,6 @@ FUTURE test_append_string.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 12.* FAILURE$ diff --git a/regression/strings/java_char_array/test.desc b/regression/strings/java_char_array/test.desc index 0acb4c57e47..aaf2c9f8fd4 100644 --- a/regression/strings/java_char_array/test.desc +++ b/regression/strings/java_char_array/test.desc @@ -1,6 +1,6 @@ CORE test_char_array.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 9.* FAILURE$ diff --git a/regression/strings/java_char_at/test.desc b/regression/strings/java_char_at/test.desc index b9f7706b7e2..dd2c1c343ae 100644 --- a/regression/strings/java_char_at/test.desc +++ b/regression/strings/java_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_char_at.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 5.* FAILURE$ diff --git a/regression/strings/java_code_point/test.desc b/regression/strings/java_code_point/test.desc index b8571739ab9..322ead7c0a1 100644 --- a/regression/strings/java_code_point/test.desc +++ b/regression/strings/java_code_point/test.desc @@ -1,6 +1,6 @@ CORE test_code_point.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/regression/strings/java_compare/test.desc b/regression/strings/java_compare/test.desc index c409e58fadc..6b8c890288d 100644 --- a/regression/strings/java_compare/test.desc +++ b/regression/strings/java_compare/test.desc @@ -1,6 +1,6 @@ CORE test_compare.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 7.* FAILURE$ diff --git a/regression/strings/java_concat/test.desc b/regression/strings/java_concat/test.desc index 2dcca464779..6063f361aa5 100644 --- a/regression/strings/java_concat/test.desc +++ b/regression/strings/java_concat/test.desc @@ -1,6 +1,6 @@ CORE test_concat.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 10.* SUCCESS$ diff --git a/regression/strings/java_contains/test.desc b/regression/strings/java_contains/test.desc index e5bb1edbc3b..c5166216bb1 100644 --- a/regression/strings/java_contains/test.desc +++ b/regression/strings/java_contains/test.desc @@ -1,6 +1,6 @@ CORE test_contains.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 7.* FAILURE$ diff --git a/regression/strings/java_delete/test.desc b/regression/strings/java_delete/test.desc index 964669b6896..721165e152d 100644 --- a/regression/strings/java_delete/test.desc +++ b/regression/strings/java_delete/test.desc @@ -1,6 +1,6 @@ CORE test_delete.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/regression/strings/java_delete_char_at/test.desc b/regression/strings/java_delete_char_at/test.desc index 8450851614c..2ec7b55da93 100644 --- a/regression/strings/java_delete_char_at/test.desc +++ b/regression/strings/java_delete_char_at/test.desc @@ -1,6 +1,6 @@ CORE test_delete_char_at.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 9.* FAILURE$ diff --git a/regression/strings/java_easychair/test.desc b/regression/strings/java_easychair/test.desc index 004b61e2b18..079e02ddee2 100644 --- a/regression/strings/java_easychair/test.desc +++ b/regression/strings/java_easychair/test.desc @@ -1,6 +1,6 @@ THOROUGH easychair.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 30.* FAILURE$ diff --git a/regression/strings/java_empty/test.desc b/regression/strings/java_empty/test.desc index 0d2635c6963..4c9cf9d82eb 100644 --- a/regression/strings/java_empty/test.desc +++ b/regression/strings/java_empty/test.desc @@ -1,6 +1,6 @@ CORE test_empty.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 6.* FAILURE$ diff --git a/regression/strings/java_endswith/test.desc b/regression/strings/java_endswith/test.desc index 8d6444b75bd..10f8a8b0e2f 100644 --- a/regression/strings/java_endswith/test.desc +++ b/regression/strings/java_endswith/test.desc @@ -1,6 +1,6 @@ CORE test_endswith.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 7.* FAILURE$ diff --git a/regression/strings/java_equal/test.desc b/regression/strings/java_equal/test.desc index 3e744a2eb05..bd4d1022d78 100644 --- a/regression/strings/java_equal/test.desc +++ b/regression/strings/java_equal/test.desc @@ -1,6 +1,6 @@ CORE test_equal.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/regression/strings/java_float/test.desc b/regression/strings/java_float/test.desc index 7a560bf3ccf..d79c25dab3a 100644 --- a/regression/strings/java_float/test.desc +++ b/regression/strings/java_float/test.desc @@ -1,6 +1,6 @@ THOROUGH test_float.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 15.* FAILURE$ diff --git a/regression/strings/java_hash_code/test.desc b/regression/strings/java_hash_code/test.desc index b8893f4a9b0..70dfc7e6bbe 100644 --- a/regression/strings/java_hash_code/test.desc +++ b/regression/strings/java_hash_code/test.desc @@ -1,6 +1,6 @@ CORE test_hash_code.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 7.* FAILURE$ diff --git a/regression/strings/java_index_of/test.desc b/regression/strings/java_index_of/test.desc index 67ff3297142..b4289558902 100644 --- a/regression/strings/java_index_of/test.desc +++ b/regression/strings/java_index_of/test.desc @@ -1,6 +1,6 @@ CORE test_index_of.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/regression/strings/java_index_of_char/test.desc b/regression/strings/java_index_of_char/test.desc index 83fbccc0515..e40554cc835 100644 --- a/regression/strings/java_index_of_char/test.desc +++ b/regression/strings/java_index_of_char/test.desc @@ -1,6 +1,6 @@ CORE test_index_of_char.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 8.* FAILURE$ diff --git a/regression/strings/java_insert_multiple/test.desc b/regression/strings/java_insert_multiple/test.desc index 3ad6df9d1e2..cae43d53985 100644 --- a/regression/strings/java_insert_multiple/test.desc +++ b/regression/strings/java_insert_multiple/test.desc @@ -1,6 +1,6 @@ CORE test_insert_multiple.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\].* line 9.* FAILURE$ diff --git a/regression/strings/test1/test.desc b/regression/strings/test1/test.desc index 2e0b38c3ae3..7fdf7649b86 100644 --- a/regression/strings/test1/test.desc +++ b/regression/strings/test1/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion c1 == c2: SUCCESS$ diff --git a/regression/strings/test2/test.desc b/regression/strings/test2/test.desc index 809cbcdaa29..c3457da325a 100644 --- a/regression/strings/test2/test.desc +++ b/regression/strings/test2/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion n == 5: SUCCESS$ diff --git a/regression/strings/test3.1/test.desc b/regression/strings/test3.1/test.desc index 6fddff4c129..28b09f80cbb 100644 --- a/regression/strings/test3.1/test.desc +++ b/regression/strings/test3.1/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/test3.2/test.desc b/regression/strings/test3.2/test.desc index 6fddff4c129..28b09f80cbb 100644 --- a/regression/strings/test3.2/test.desc +++ b/regression/strings/test3.2/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/test3.3/test.desc b/regression/strings/test3.3/test.desc index 6fddff4c129..28b09f80cbb 100644 --- a/regression/strings/test3.3/test.desc +++ b/regression/strings/test3.3/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/test3.4/test.desc b/regression/strings/test3.4/test.desc index fc1cde2392c..87e4f8c97ae 100644 --- a/regression/strings/test3.4/test.desc +++ b/regression/strings/test3.4/test.desc @@ -1,6 +1,6 @@ FUTURE test_init.class ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/test3/test.desc b/regression/strings/test3/test.desc index f6f9a63520a..20e7e66c522 100644 --- a/regression/strings/test3/test.desc +++ b/regression/strings/test3/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion __CPROVER_string_length\(s\) == i \+ 5: SUCCESS$ diff --git a/regression/strings/test4/test.desc b/regression/strings/test4/test.desc index 6fddff4c129..28b09f80cbb 100644 --- a/regression/strings/test4/test.desc +++ b/regression/strings/test4/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/strings/test5/test.desc b/regression/strings/test5/test.desc index 303defd9de4..cc9ce200da3 100644 --- a/regression/strings/test5/test.desc +++ b/regression/strings/test5/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/strings/test_char_set/test.desc b/regression/strings/test_char_set/test.desc index 360759faf98..1266bbac4d5 100644 --- a/regression/strings/test_char_set/test.desc +++ b/regression/strings/test_char_set/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* SUCCESS$ diff --git a/regression/strings/test_concat/test.desc b/regression/strings/test_concat/test.desc index 317a4d1b4dd..c2ff491673f 100644 --- a/regression/strings/test_concat/test.desc +++ b/regression/strings/test_concat/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion c == .p.: SUCCESS$ diff --git a/regression/strings/test_contains/test.desc b/regression/strings/test_contains/test.desc index b0e33ce2b43..44862a304a8 100644 --- a/regression/strings/test_contains/test.desc +++ b/regression/strings/test_contains/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"3\"\)): SUCCESS$ diff --git a/regression/strings/test_equal/test.desc b/regression/strings/test_equal/test.desc index 34297ec50f5..7647a04397f 100644 --- a/regression/strings/test_equal/test.desc +++ b/regression/strings/test_equal/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*.assertion.1\].* SUCCESS$ diff --git a/regression/strings/test_index_of/test.desc b/regression/strings/test_index_of/test.desc index a2c12c3d259..dcb245dbf5e 100644 --- a/regression/strings/test_index_of/test.desc +++ b/regression/strings/test_index_of/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion firstSlash == 3: SUCCESS$ diff --git a/regression/strings/test_int/test.desc b/regression/strings/test_int/test.desc index fcce43ca76c..0638394661c 100644 --- a/regression/strings/test_int/test.desc +++ b/regression/strings/test_int/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion __CPROVER_char_at\(s,0\) == .1.: SUCCESS$ diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc index f2f54e69921..77f0c2e7eb8 100644 --- a/regression/strings/test_pass1/test.desc +++ b/regression/strings/test_pass1/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): SUCCESS diff --git a/regression/strings/test_pass_pc3/test.desc b/regression/strings/test_pass_pc3/test.desc index f1f3d1618c8..a88fd61db47 100644 --- a/regression/strings/test_pass_pc3/test.desc +++ b/regression/strings/test_pass_pc3/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion __CPROVER_string_length\(s3\) == 0: FAILURE$ diff --git a/regression/strings/test_prefix/test.desc b/regression/strings/test_prefix/test.desc index be0ed5dc69e..53e37ec7dc8 100644 --- a/regression/strings/test_prefix/test.desc +++ b/regression/strings/test_prefix/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion b: SUCCESS$ diff --git a/regression/strings/test_strlen/test.desc b/regression/strings/test_strlen/test.desc index 28ed1b7e698..9040a64de73 100644 --- a/regression/strings/test_strlen/test.desc +++ b/regression/strings/test_strlen/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion len_s == len_t: SUCCESS$ diff --git a/regression/strings/test_substring/test.desc b/regression/strings/test_substring/test.desc index f0e4b5832b2..cbde7978b4c 100644 --- a/regression/strings/test_substring/test.desc +++ b/regression/strings/test_substring/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* SUCCESS$ diff --git a/regression/strings/test_suffix/test.desc b/regression/strings/test_suffix/test.desc index e7e8c1e36be..e9c8580be6f 100644 --- a/regression/strings/test_suffix/test.desc +++ b/regression/strings/test_suffix/test.desc @@ -1,6 +1,6 @@ FUTURE test.c ---refine-strings +--refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion __CPROVER_string_issuffix\(__CPROVER_string_literal\("po"\),s\): SUCCESS$ From e0441cb96da19daba4960c7fd2ed67266662fd90 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 30 Aug 2017 12:12:10 +0100 Subject: [PATCH 5/7] Add example where the solver potentially runing out of memory --- .../java_int_to_string/test2_bug.desc | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 regression/strings-smoke-tests/java_int_to_string/test2_bug.desc 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 new file mode 100644 index 00000000000..00047bad217 --- /dev/null +++ b/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc @@ -0,0 +1,11 @@ +KNOWNBUG +Test2.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +assertion.* line 7 .* SUCCESS$ +assertion.* line 10 .* FAILURE$ +-- +-- +When string-max-length is not set, the solver can run out of memory in +an unpredictable way. \ No newline at end of file From df88b49464bb1f423beefaef523aa816e5a8c4e5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 28 Sep 2017 14:59:18 +0100 Subject: [PATCH 6/7] Rename operand_to_process into expr_to_process --- src/java_bytecode/java_string_library_preprocess.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 6d638f80f76..5ccfecaf81c 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -288,22 +288,23 @@ exprt::operandst java_string_library_preprocesst::process_parameters( } /// Creates a string_exprt from the input exprt representing a char sequence -/// \param op_to_process: an operand of a type which implements char sequence +/// \param expr_to_process: an expression of a type which implements char +/// sequence /// \param loc: location in the source /// \param symbol_table: symbol table /// \param init_code: code block, in which declaration of some arguments may be /// added /// \return the processed operand exprt java_string_library_preprocesst::convert_exprt_to_string_exprt( - const exprt &op_to_process, + const exprt &expr_to_process, const source_locationt &loc, symbol_tablet &symbol_table, code_blockt &init_code) { - PRECONDITION(implements_java_char_sequence(op_to_process.type())); + PRECONDITION(implements_java_char_sequence(expr_to_process.type())); string_exprt string_expr=fresh_string_expr(loc, symbol_table, init_code); code_assign_java_string_to_string_expr( - string_expr, op_to_process, symbol_table, init_code); + string_expr, expr_to_process, symbol_table, init_code); exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, init_code); init_code.add(code_assignt(string_expr_sym, string_expr)); return string_expr; From c24e6c93b2e36af273a6fb13a22e4fd128f8206e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 28 Sep 2017 20:09:12 +0100 Subject: [PATCH 7/7] Update regression test that can randomly fail This test could randomly fail, it was simplified and the previous version is marked as knownbug. The problem should be corrected by PR 1420 --- .../StringIndexMethods04.class | Bin 695 -> 811 bytes .../StringIndexMethods04.java | 6 ++++++ .../strings/StringIndexMethods04/test_bug.desc | 12 ++++++++++++ 3 files changed, 18 insertions(+) create mode 100644 regression/strings/StringIndexMethods04/test_bug.desc diff --git a/regression/strings/StringIndexMethods04/StringIndexMethods04.class b/regression/strings/StringIndexMethods04/StringIndexMethods04.class index 69a8fe4d628343caa7e78dbb94db2c2836b7591c..10dc4401805471f0ec2386fd5d743da6b1a87850 100644 GIT binary patch delta 415 zcmYL^y-or_6otRpWp|d{6=4-bSrq?J!B`lzu`!nF3uvcN42fU^or%vtwxhA6uu>C9 zG|}G2@D1#Z@vc9ZNlxb6JNLV12G*^;`TF_z3~aFK;xXk=NRlLUD7s8Dqba%AaeY=Z z=Q7WNX0fy0^2!R`IIcH$+vlC$Rwc!#!oO@Dw@&M|+Q~)x%*SU$;rw|`*=LF6sHBRW zw{omZ(hu&A2!R^+7?C6>e_G-T&nl11IK2Yev}k zCwM~e2_@-}5XJA6<1Dy`7q7!)24ou&?efY}p4?#*6KRnJ6Sua7wzOR3$aJ zJwm<2LNbEZ_)?J~OHOz!J;9J8BROOEXq0YZU0Up9SkRJhYNn;LQQs6ad0{huLA9|X hWOMdAsRwl8iG=xz8HXDGLSvI8hI