From 21eeb297950fc06e830c293e015e0302fa590bbe Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Thu, 20 Apr 2017 09:46:20 +0100 Subject: [PATCH 1/2] Enable working smoke tests Set the currently working some tests as CORE and link the others to GitHub issues. --- regression/strings-smoke-tests/java_append_char/test.desc | 2 +- regression/strings-smoke-tests/java_append_int/test.desc | 2 +- regression/strings-smoke-tests/java_append_object/test.desc | 1 + regression/strings-smoke-tests/java_append_string/test.desc | 2 +- regression/strings-smoke-tests/java_case/test.desc | 2 +- regression/strings-smoke-tests/java_char_array/test.desc | 2 +- regression/strings-smoke-tests/java_char_array_init/test.desc | 1 + 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_contains/test.desc | 3 ++- 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_endswith/test.desc | 2 +- regression/strings-smoke-tests/java_equal/test.desc | 4 ++-- 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 | 3 ++- regression/strings-smoke-tests/java_index_of_char/test.desc | 3 ++- regression/strings-smoke-tests/java_insert_char/test.desc | 2 +- .../strings-smoke-tests/java_insert_char_array/test.desc | 2 +- regression/strings-smoke-tests/java_insert_int/test.desc | 2 +- regression/strings-smoke-tests/java_insert_multiple/test.desc | 2 +- regression/strings-smoke-tests/java_insert_string/test.desc | 2 +- regression/strings-smoke-tests/java_int_to_string/test.desc | 2 +- regression/strings-smoke-tests/java_intern/test.desc | 2 +- regression/strings-smoke-tests/java_last_index_of/test.desc | 3 ++- .../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_parseint/test.desc | 2 +- regression/strings-smoke-tests/java_replace/test.desc | 3 ++- 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_set_length/test.desc | 4 ++-- 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_trim/test.desc | 4 ++-- 41 files changed, 49 insertions(+), 42 deletions(-) diff --git a/regression/strings-smoke-tests/java_append_char/test.desc b/regression/strings-smoke-tests/java_append_char/test.desc index 0f1b3ae243f..88d1cbf2114 100644 --- a/regression/strings-smoke-tests/java_append_char/test.desc +++ b/regression/strings-smoke-tests/java_append_char/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_append_char.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_append_int/test.desc b/regression/strings-smoke-tests/java_append_int/test.desc index e1455859470..e0b30e7827d 100644 --- a/regression/strings-smoke-tests/java_append_int/test.desc +++ b/regression/strings-smoke-tests/java_append_int/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_append_int.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_append_object/test.desc b/regression/strings-smoke-tests/java_append_object/test.desc index 5db2ac1db73..787852963ed 100644 --- a/regression/strings-smoke-tests/java_append_object/test.desc +++ b/regression/strings-smoke-tests/java_append_object/test.desc @@ -5,3 +5,4 @@ test_append_object.class ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +Issue: diffblue/test-gen#82 diff --git a/regression/strings-smoke-tests/java_append_string/test.desc b/regression/strings-smoke-tests/java_append_string/test.desc index 18035539d58..943ca820bcc 100644 --- a/regression/strings-smoke-tests/java_append_string/test.desc +++ b/regression/strings-smoke-tests/java_append_string/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_append_string.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_case/test.desc b/regression/strings-smoke-tests/java_case/test.desc index e01a5054419..9a254ae3484 100644 --- a/regression/strings-smoke-tests/java_case/test.desc +++ b/regression/strings-smoke-tests/java_case/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_case.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_char_array/test.desc b/regression/strings-smoke-tests/java_char_array/test.desc index ecce56c1ab8..efb6ad4c5d7 100644 --- a/regression/strings-smoke-tests/java_char_array/test.desc +++ b/regression/strings-smoke-tests/java_char_array/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_char_array.class --refine-strings ^EXIT=0$ 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 fc1cde2392c..04096a8a984 100644 --- a/regression/strings-smoke-tests/java_char_array_init/test.desc +++ b/regression/strings-smoke-tests/java_char_array_init/test.desc @@ -5,3 +5,4 @@ test_init.class ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +cbmc/test-gen#259 diff --git a/regression/strings-smoke-tests/java_char_at/test.desc b/regression/strings-smoke-tests/java_char_at/test.desc index 5bf29fc7a4d..f2d5ecad6c7 100644 --- a/regression/strings-smoke-tests/java_char_at/test.desc +++ b/regression/strings-smoke-tests/java_char_at/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_char_at.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_code_point/test.desc b/regression/strings-smoke-tests/java_code_point/test.desc index 012c7c3501b..e3be9616fa5 100644 --- a/regression/strings-smoke-tests/java_code_point/test.desc +++ b/regression/strings-smoke-tests/java_code_point/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_code_point.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_compare/test.desc b/regression/strings-smoke-tests/java_compare/test.desc index 38aa025f416..9e6810476b9 100644 --- a/regression/strings-smoke-tests/java_compare/test.desc +++ b/regression/strings-smoke-tests/java_compare/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_compare.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_concat/test.desc b/regression/strings-smoke-tests/java_concat/test.desc index fb784efd723..2dcca464779 100644 --- a/regression/strings-smoke-tests/java_concat/test.desc +++ b/regression/strings-smoke-tests/java_concat/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_concat.class --refine-strings ^EXIT=10$ diff --git a/regression/strings-smoke-tests/java_contains/test.desc b/regression/strings-smoke-tests/java_contains/test.desc index 2b96346d718..e40d51aa473 100644 --- a/regression/strings-smoke-tests/java_contains/test.desc +++ b/regression/strings-smoke-tests/java_contains/test.desc @@ -1,4 +1,4 @@ -FUTURE +KNOWNBUG test_contains.class --refine-strings ^EXIT=10$ @@ -6,3 +6,4 @@ test_contains.class ^\[.*assertion.1\].* line 8.* SUCCESS$ ^\[.*assertion.2\].* line 9.* FAILURE$ -- +Issue: diffblue/test-gen#201 diff --git a/regression/strings-smoke-tests/java_delete/test.desc b/regression/strings-smoke-tests/java_delete/test.desc index 27a1406cdb7..f0c0aedda91 100644 --- a/regression/strings-smoke-tests/java_delete/test.desc +++ b/regression/strings-smoke-tests/java_delete/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_delete.class --refine-strings ^EXIT=0$ 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 94ba56a2c54..d415d16e9b6 100644 --- a/regression/strings-smoke-tests/java_delete_char_at/test.desc +++ b/regression/strings-smoke-tests/java_delete_char_at/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_delete_char_at.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_empty/test.desc b/regression/strings-smoke-tests/java_empty/test.desc index 9951c8a13ee..181ff4ee5fd 100644 --- a/regression/strings-smoke-tests/java_empty/test.desc +++ b/regression/strings-smoke-tests/java_empty/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_empty.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_endswith/test.desc b/regression/strings-smoke-tests/java_endswith/test.desc index 0461a3e50e6..8b058f48d78 100644 --- a/regression/strings-smoke-tests/java_endswith/test.desc +++ b/regression/strings-smoke-tests/java_endswith/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_endswith.class --refine-strings ^EXIT=10$ diff --git a/regression/strings-smoke-tests/java_equal/test.desc b/regression/strings-smoke-tests/java_equal/test.desc index 05f0f383230..964c3b72bae 100644 --- a/regression/strings-smoke-tests/java_equal/test.desc +++ b/regression/strings-smoke-tests/java_equal/test.desc @@ -1,6 +1,6 @@ -FUTURE +CORE test_equal.class ---refine-strings +--refine-strings --string-max-length 100 --string-max-length 100 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* FAILURE$ diff --git a/regression/strings-smoke-tests/java_float/test.desc b/regression/strings-smoke-tests/java_float/test.desc index 427d1fca836..e81b6b4feba 100644 --- a/regression/strings-smoke-tests/java_float/test.desc +++ b/regression/strings-smoke-tests/java_float/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_float.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_hash_code/test.desc b/regression/strings-smoke-tests/java_hash_code/test.desc index 2db8d7116f9..fc628393186 100644 --- a/regression/strings-smoke-tests/java_hash_code/test.desc +++ b/regression/strings-smoke-tests/java_hash_code/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_hash_code.class --refine-strings ^EXIT=10$ diff --git a/regression/strings-smoke-tests/java_index_of/test.desc b/regression/strings-smoke-tests/java_index_of/test.desc index f2fa825597d..6033af25d1b 100644 --- a/regression/strings-smoke-tests/java_index_of/test.desc +++ b/regression/strings-smoke-tests/java_index_of/test.desc @@ -1,7 +1,8 @@ -FUTURE +KNOWNBUG test_index_of.class --refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +Issue: cbmc/test-gen#77 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 63382a455f3..a95467b52e4 100644 --- a/regression/strings-smoke-tests/java_index_of_char/test.desc +++ b/regression/strings-smoke-tests/java_index_of_char/test.desc @@ -1,7 +1,8 @@ -FUTURE +CORE test_index_of_char.class --refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +Issue: cbmc/test-gen#77 diff --git a/regression/strings-smoke-tests/java_insert_char/test.desc b/regression/strings-smoke-tests/java_insert_char/test.desc index 77d3ce2ebd9..0e9a06d5afb 100644 --- a/regression/strings-smoke-tests/java_insert_char/test.desc +++ b/regression/strings-smoke-tests/java_insert_char/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_insert_char.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_insert_char_array/test.desc b/regression/strings-smoke-tests/java_insert_char_array/test.desc index d48c601b61b..082771dd2db 100644 --- a/regression/strings-smoke-tests/java_insert_char_array/test.desc +++ b/regression/strings-smoke-tests/java_insert_char_array/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_insert_char_array.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_insert_int/test.desc b/regression/strings-smoke-tests/java_insert_int/test.desc index dc039fedbea..df87a5f5728 100644 --- a/regression/strings-smoke-tests/java_insert_int/test.desc +++ b/regression/strings-smoke-tests/java_insert_int/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_insert_int.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_insert_multiple/test.desc b/regression/strings-smoke-tests/java_insert_multiple/test.desc index 983d416dd3b..bb9a23f1b5c 100644 --- a/regression/strings-smoke-tests/java_insert_multiple/test.desc +++ b/regression/strings-smoke-tests/java_insert_multiple/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_insert_multiple.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_insert_string/test.desc b/regression/strings-smoke-tests/java_insert_string/test.desc index b438d32d6d9..44bf9f268d9 100644 --- a/regression/strings-smoke-tests/java_insert_string/test.desc +++ b/regression/strings-smoke-tests/java_insert_string/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_insert_string.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_int_to_string/test.desc b/regression/strings-smoke-tests/java_int_to_string/test.desc index a615a10f538..38fa5289bd2 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_int.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_intern/test.desc b/regression/strings-smoke-tests/java_intern/test.desc index 645e267029c..c8d0eea43bd 100644 --- a/regression/strings-smoke-tests/java_intern/test.desc +++ b/regression/strings-smoke-tests/java_intern/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_intern.class --refine-strings ^EXIT=0$ 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 77bc5b7f18f..5ee1604e846 100644 --- a/regression/strings-smoke-tests/java_last_index_of/test.desc +++ b/regression/strings-smoke-tests/java_last_index_of/test.desc @@ -1,7 +1,8 @@ -FUTURE +KNOWNBUG test_last_index_of.class --refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +Issue: diffblue/test-gen#77 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 3e9a3d4b547..aa88fc5f6ef 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,4 +1,4 @@ -FUTURE +CORE test_last_index_of_char.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_length/test.desc b/regression/strings-smoke-tests/java_length/test.desc index 913afbf13c7..d7f0e02feca 100644 --- a/regression/strings-smoke-tests/java_length/test.desc +++ b/regression/strings-smoke-tests/java_length/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_length.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_parseint/test.desc b/regression/strings-smoke-tests/java_parseint/test.desc index 9cb70f5a957..6a513e61deb 100644 --- a/regression/strings-smoke-tests/java_parseint/test.desc +++ b/regression/strings-smoke-tests/java_parseint/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_parseint.class --refine-strings ^EXIT=10$ diff --git a/regression/strings-smoke-tests/java_replace/test.desc b/regression/strings-smoke-tests/java_replace/test.desc index 59c7d326a0b..d86aae6b5a9 100644 --- a/regression/strings-smoke-tests/java_replace/test.desc +++ b/regression/strings-smoke-tests/java_replace/test.desc @@ -1,7 +1,8 @@ FUTURE test_replace.class ---refine-strings +--refine-strings --string-max-length 100 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +diffblue/test-gen#256 diff --git a/regression/strings-smoke-tests/java_replace_char/test.desc b/regression/strings-smoke-tests/java_replace_char/test.desc index 528d4eead6c..5c336326e5d 100644 --- a/regression/strings-smoke-tests/java_replace_char/test.desc +++ b/regression/strings-smoke-tests/java_replace_char/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_replace_char.class --refine-strings ^EXIT=0$ 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 650e7712278..1c471d0194a 100644 --- a/regression/strings-smoke-tests/java_set_char_at/test.desc +++ b/regression/strings-smoke-tests/java_set_char_at/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_set_char_at.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_set_length/test.desc b/regression/strings-smoke-tests/java_set_length/test.desc index ab59e459eb1..d19eb265fa4 100644 --- a/regression/strings-smoke-tests/java_set_length/test.desc +++ b/regression/strings-smoke-tests/java_set_length/test.desc @@ -1,6 +1,6 @@ -FUTURE +CORE test_set_length.class ---refine-strings +--refine-strings --string-max-length 100 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_starts_with/test.desc b/regression/strings-smoke-tests/java_starts_with/test.desc index 5c5d85565c2..ec6b84102f2 100644 --- a/regression/strings-smoke-tests/java_starts_with/test.desc +++ b/regression/strings-smoke-tests/java_starts_with/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_starts_with.class --refine-strings ^EXIT=10$ 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 ba9187109ed..2a37e02a36c 100644 --- a/regression/strings-smoke-tests/java_string_builder_length/test.desc +++ b/regression/strings-smoke-tests/java_string_builder_length/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_sb_length.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_subsequence/test.desc b/regression/strings-smoke-tests/java_subsequence/test.desc index 34585a7900d..df3cc28619f 100644 --- a/regression/strings-smoke-tests/java_subsequence/test.desc +++ b/regression/strings-smoke-tests/java_subsequence/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_subsequence.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_substring/test.desc b/regression/strings-smoke-tests/java_substring/test.desc index 8a29460f529..26ec800cfac 100644 --- a/regression/strings-smoke-tests/java_substring/test.desc +++ b/regression/strings-smoke-tests/java_substring/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_substring.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_trim/test.desc b/regression/strings-smoke-tests/java_trim/test.desc index c7a307c37ed..171ada28356 100644 --- a/regression/strings-smoke-tests/java_trim/test.desc +++ b/regression/strings-smoke-tests/java_trim/test.desc @@ -1,6 +1,6 @@ -FUTURE +CORE test_trim.class ---refine-strings +--refine-strings --string-max-length 100 ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 6.* SUCCESS$ From 6b24ec76dbf83dc64f282ac20d82739f13958c21 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Apr 2017 17:44:11 +0100 Subject: [PATCH 2/2] Implement StringBuffer methods Addresses issue diffblue/test-gen#245. This adds preprocessing for StringBuffer methods --- .../string_refine_preprocess.cpp | 151 +++++++++++++++++- src/goto-programs/string_refine_preprocess.h | 5 + 2 files changed, 153 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/string_refine_preprocess.cpp b/src/goto-programs/string_refine_preprocess.cpp index f6e2b432c92..26abe8d2dc6 100644 --- a/src/goto-programs/string_refine_preprocess.cpp +++ b/src/goto-programs/string_refine_preprocess.cpp @@ -123,6 +123,44 @@ bool string_refine_preprocesst::is_java_string_builder_pointer_type( /*******************************************************************\ +Function: string_refine_preprocesst::is_java_string_buffer_type + + Inputs: a type + + Outputs: Boolean telling whether the type is that of java string buffer + +\*******************************************************************/ + +bool string_refine_preprocesst::is_java_string_buffer_type(const typet &type) +{ + return check_java_type(type, "java.lang.StringBuffer"); +} + +/*******************************************************************\ + +Function: string_refine_preprocesst::is_java_string_buffer_pointer_type + + Inputs: a type + + Outputs: Boolean telling whether the type is that of java StringBuffer + pointers + +\*******************************************************************/ + +bool string_refine_preprocesst::is_java_string_buffer_pointer_type( + const typet &type) +{ + if(type.id()==ID_pointer) + { + const pointer_typet &pt=to_pointer_type(type); + const typet &subtype=pt.subtype(); + return is_java_string_buffer_type(subtype); + } + return false; +} + +/*******************************************************************\ + Function: string_refine_preprocesst::is_java_char_sequence_type Inputs: a type @@ -315,9 +353,7 @@ Function: string_refine_preprocesst::get_data_and_length_type_of_string void string_refine_preprocesst::get_data_and_length_type_of_string( const exprt &expr, typet &data_type, typet &length_type) { - assert(is_java_string_type(expr.type()) || - is_java_string_builder_type(expr.type()) || - is_java_char_sequence_type(expr.type())); + assert(implements_java_char_sequence(pointer_typet(expr.type()))); typet object_type=ns.follow(expr.type()); const struct_typet &struct_type=to_struct_type(object_type); for(const auto &component : struct_type.components()) @@ -1351,6 +1387,115 @@ void string_refine_preprocesst::initialize_string_function_table() // Not supported "java.lang.StringBuilder.trimToSize" // TODO clean irep ids from insert_char_array etc... + // StringBuffer library + string_function_calls + ["java::java.lang.StringBuffer.:(Ljava/lang/String;)V"]= + ID_cprover_string_copy_func; + string_function_calls["java::java.lang.StringBuffer.:()V"]= + ID_cprover_string_empty_string_func; + + side_effect_functions + ["java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_bool_func; + side_effect_functions + ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_char_func; + side_effect_functions + ["java::java.lang.StringBuffer.append:([C)" + "Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_func; + // Not supported: "java.lang.StringBuffer.append:([CII)" + // Not supported: "java.lang.StringBuffer.append:(LCharSequence;)" + side_effect_functions + ["java::java.lang.StringBuffer.append:(D)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_double_func; + side_effect_functions + ["java::java.lang.StringBuffer.append:(F)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_float_func; + side_effect_functions + ["java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_int_func; + side_effect_functions + ["java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_long_func; + // Not supported: "java.lang.StringBuffer.append:(LObject;)" + side_effect_functions + ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)" + "Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_func; + side_effect_functions + ["java::java.lang.StringBuffer.appendCodePoint:(I)" + "Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_code_point_func; + // Not supported: "java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)" + // Not supported: "java.lang.StringBuffer.capacity:()" + string_functions["java::java.lang.StringBuffer.charAt:(I)C"]= + ID_cprover_string_char_at_func; + string_functions["java::java.lang.StringBuffer.codePointAt:(I)I"]= + ID_cprover_string_code_point_at_func; + string_functions["java::java.lang.StringBuffer.codePointBefore:(I)I"]= + ID_cprover_string_code_point_before_func; + string_functions["java::java.lang.StringBuffer.codePointCount:(II)I"]= + ID_cprover_string_code_point_count_func; + side_effect_functions + ["java::java.lang.StringBuffer.delete:(II)Ljava/lang/StringBuffer;"]= + ID_cprover_string_delete_func; + side_effect_functions + ["java::java.lang.StringBuffer.deleteCharAt:(I)Ljava/lang/StringBuffer;"]= + ID_cprover_string_delete_char_at_func; + // Not supported: "java.lang.StringBuffer.ensureCapacity:()" + // Not supported: "java.lang.StringBuffer.getChars:()" + // Not supported: "java.lang.StringBuffer.indexOf:()" + side_effect_functions + ["java::java.lang.StringBuffer.insert:(IZ)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_bool_func; + side_effect_functions + ["java::java.lang.StringBuffer.insert:(IC)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_char_func; + side_effect_functions + ["java::java.lang.StringBuffer.insert:(I[C)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_func; + side_effect_functions + ["java::java.lang.StringBuffer.insert:(I[CII)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_func; + // Not supported "java.lang.StringBuffer.insert:(ILCharSequence;)" + // Not supported "java.lang.StringBuffer.insert:(ILCharSequence;II)" + // Not supported "java.lang.StringBuffer.insert:(ID)" + // Not supported "java.lang.StringBuffer.insert:(IF)" + side_effect_functions + ["java::java.lang.StringBuffer.insert:(II)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_int_func; + side_effect_functions + ["java::java.lang.StringBuffer.insert:(IJ)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_long_func; + // Not supported "java.lang.StringBuffer.insert:(ILObject;)" + side_effect_functions + ["java::java.lang.StringBuffer.insert:(ILjava/lang/String;)" + "Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_func; + // Not supported "java.lang.StringBuffer.lastIndexOf" + string_functions["java::java.lang.StringBuffer.length:()I"]= + ID_cprover_string_length_func; + // Not supported "java.lang.StringBuffer.offsetByCodePoints" + // Not supported "java.lang.StringBuffer.replace" + // Not supported "java.lang.StringBuffer.reverse" + side_effect_functions["java::java.lang.StringBuffer.setCharAt:(IC)V"]= + ID_cprover_string_char_set_func; + side_effect_functions + ["java::java.lang.StringBuffer.setLength:(I)V"]= + ID_cprover_string_set_length_func; + // Not supported "java.lang.StringBuffer.subSequence" + string_functions + ["java::java.lang.StringBuffer.substring:(II)Ljava/lang/String;"]= + ID_cprover_string_substring_func; + string_functions + ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]= + ID_cprover_string_substring_func; + string_functions + ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"]= + ID_cprover_string_copy_func; + // Not supported "java.lang.StringBuffer.trimToSize" + // Other libraries string_functions["java::java.lang.CharSequence.charAt:(I)C"]= ID_cprover_string_char_at_func; diff --git a/src/goto-programs/string_refine_preprocess.h b/src/goto-programs/string_refine_preprocess.h index 5ae398b757a..df419c73750 100644 --- a/src/goto-programs/string_refine_preprocess.h +++ b/src/goto-programs/string_refine_preprocess.h @@ -53,6 +53,10 @@ class string_refine_preprocesst:public messaget static bool is_java_string_builder_pointer_type(const typet &type); + static bool is_java_string_buffer_type(const typet &type); + + static bool is_java_string_buffer_pointer_type(const typet &type); + static bool is_java_char_sequence_type(const typet &type); static bool is_java_char_sequence_pointer_type(const typet &type); @@ -66,6 +70,7 @@ class string_refine_preprocesst:public messaget return is_java_char_sequence_pointer_type(type) || is_java_string_builder_pointer_type(type) || + is_java_string_buffer_pointer_type(type) || is_java_string_pointer_type(type); }