From 8f6431c6c99b266bdee21f66c61c60298a35cb70 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Thu, 8 Feb 2018 22:34:31 +1300 Subject: [PATCH 1/3] Introduce more string primitives in JBMC We replace some java signatures with CProver primitives. This concerns those String, StringBuilder and StringBuffer methods that throw exceptions. We do that to be able to wrap some functionality around the string methods in the library of models, e.g. throwing out of bounds exceptions. --- .../java_string_library_preprocess.cpp | 101 +++++++++--------- 1 file changed, 52 insertions(+), 49 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 936ea85ac5c..dbbaae750c3 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -1921,13 +1921,13 @@ void java_string_library_preprocesst::initialize_conversion_table() ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]= ID_cprover_string_char_at_func; cprover_equivalent_to_java_function - ["java::java.lang.String.codePointAt:(I)I"]= + ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] = ID_cprover_string_code_point_at_func; cprover_equivalent_to_java_function - ["java::java.lang.String.codePointBefore:(I)I"]= + ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] = ID_cprover_string_code_point_before_func; cprover_equivalent_to_java_function - ["java::java.lang.String.codePointCount:(II)I"]= + ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] = ID_cprover_string_code_point_count_func; cprover_equivalent_to_java_function ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]= @@ -2009,8 +2009,8 @@ void java_string_library_preprocesst::initialize_conversion_table() std::placeholders::_2, std::placeholders::_3); cprover_equivalent_to_java_function - ["java::java.lang.String.offsetByCodePoints:(II)I"]= - ID_cprover_string_offset_by_code_point_func; + ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/" + "String;II)I"] = ID_cprover_string_offset_by_code_point_func; cprover_equivalent_to_java_string_returning_function ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]= ID_cprover_string_replace_func; @@ -2024,8 +2024,8 @@ void java_string_library_preprocesst::initialize_conversion_table() ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]= ID_cprover_string_startswith_func; cprover_equivalent_to_java_string_returning_function - ["java::java.lang.String.subSequence:(II)Ljava/lang/CharSequence;"]= - ID_cprover_string_substring_func; + ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/" + "lang/CharSequence;"] = ID_cprover_string_substring_func; // CProverString.substring differs from the Java String.substring in that no // exception is raised for the out of bounds case. cprover_equivalent_to_java_string_returning_function @@ -2105,17 +2105,15 @@ void java_string_library_preprocesst::initialize_conversion_table() ["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_double_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;II)" - "Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)" - "Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)" - "Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_func; + ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/" + "lang/CharSequence;II)" + "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)" + "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)" + "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func; cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;"]= ID_cprover_string_concat_bool_func; @@ -2136,27 +2134,32 @@ void java_string_library_preprocesst::initialize_conversion_table() ["java::java.lang.StringBuilder.codePointCount:(II)I"]= ID_cprover_string_code_point_count_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.delete:(II)Ljava/lang/StringBuilder;"]= + ["java::org.cprover.CProverString.delete:(Ljava/lang/" + "StringBuilder;II)Ljava/lang/StringBuilder;"] = ID_cprover_string_delete_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.deleteCharAt:(I)Ljava/lang/StringBuilder;"]= - ID_cprover_string_delete_char_at_func; + ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" + "StringBuilder;I)Ljava/lang/StringBuilder;"] = + ID_cprover_string_delete_char_at_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.insert:(IC)Ljava/lang/StringBuilder;"]= - ID_cprover_string_insert_char_func; + ["java::org.cprover.CProverString.insert:(Ljava/lang/" + "StringBuilder;IC)Ljava/lang/StringBuilder;"] = + ID_cprover_string_insert_char_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.insert:(IZ)Ljava/lang/StringBuilder;"]= + ["java::org.cprover.CProverString.insert:(Ljava/lang/" + "StringBuilder;IZ)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_bool_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.insert:(II)Ljava/lang/StringBuilder;"]= + ["java::org.cprover.CProverString.insert:(Ljava/lang/" + "StringBuilder;II)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_int_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.insert:(IJ)Ljava/lang/StringBuilder;"]= + ["java::org.cprover.CProverString.insert:(Ljava/lang/" + "StringBuilder;IJ)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_long_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.insert:(ILjava/lang/String;)" - "Ljava/lang/StringBuilder;"]= - ID_cprover_string_insert_func; + ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/" + "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func; conversion_table ["java::java.lang.StringBuilder.length:()I"]= std::bind( @@ -2229,7 +2232,7 @@ void java_string_library_preprocesst::initialize_conversion_table() "Ljava/lang/StringBuffer;"]= ID_cprover_string_concat_code_point_func; cprover_equivalent_to_java_function - ["java::java.lang.StringBuffer.charAt:(I)C"]= + ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] = ID_cprover_string_char_at_func; cprover_equivalent_to_java_function ["java::java.lang.StringBuffer.codePointAt:(I)I"]= @@ -2241,42 +2244,42 @@ void java_string_library_preprocesst::initialize_conversion_table() ["java::java.lang.StringBuffer.codePointCount:(II)I"]= ID_cprover_string_code_point_count_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuffer.delete:(II)Ljava/lang/StringBuffer;"]= - ID_cprover_string_delete_func; + ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/" + "lang/StringBuffer;"] = ID_cprover_string_delete_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuffer.deleteCharAt:(I)Ljava/lang/StringBuffer;"]= + ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" + "StringBufferI)Ljava/lang/StringBuffer;"] = ID_cprover_string_delete_char_at_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuffer.insert:(IC)Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_char_func; + ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IC)Ljava/" + "lang/StringBuffer;"] = ID_cprover_string_insert_char_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuffer.insert:(II)Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_int_func; + ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;II)Ljava/" + "lang/StringBuffer;"] = ID_cprover_string_insert_int_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuffer.insert:(IJ)Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_long_func; + ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IJ)Ljava/" + "lang/StringBuffer;"] = ID_cprover_string_insert_long_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuffer.insert:(ILjava/lang/String;)" - "Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_func; + ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;ILjava/" + "lang/String;)Ljava/lang/StringBuffer;"] = ID_cprover_string_insert_func; cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuffer.insert:(IZ)Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_bool_func; + ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IZ)Ljava/" + "lang/StringBuffer;"] = ID_cprover_string_insert_bool_func; conversion_table ["java::java.lang.StringBuffer.length:()I"]= conversion_table["java::java.lang.String.length:()I"]; cprover_equivalent_to_java_assign_function - ["java::java.lang.StringBuffer.setCharAt:(IC)V"]= + ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] = ID_cprover_string_char_set_func; cprover_equivalent_to_java_assign_function - ["java::java.lang.StringBuffer.setLength:(I)V"]= - ID_cprover_string_set_length_func; + ["java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] = + ID_cprover_string_set_length_func; cprover_equivalent_to_java_string_returning_function ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]= ID_cprover_string_substring_func; cprover_equivalent_to_java_string_returning_function - ["java::java.lang.StringBuffer.substring:(II)Ljava/lang/String;"]= - ID_cprover_string_substring_func; + ["java::org.cprover.CProverString.substring:(Ljava/Lang/" + "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func; conversion_table ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"]= std::bind( From dd5a6748c721c4758755c42beb6e19d6997a5042 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Fri, 9 Feb 2018 21:33:33 +1300 Subject: [PATCH 2/3] Add jbmc string primitives to CProverString Allows to compile and run jbmc tests. --- .../cprover/CProverString.class | Bin 790 -> 4153 bytes .../cprover/CProverString.java | 121 ++++++++++++++++++ 2 files changed, 121 insertions(+) diff --git a/regression/strings-smoke-tests/cprover/CProverString.class b/regression/strings-smoke-tests/cprover/CProverString.class index c1cf5742e3955fa4c05a1d8df8a09fcc6d21d44c..8eb78d4aaa4179eb951b284df7cf07f2b598d2f5 100644 GIT binary patch literal 4153 zcmbVOTXz#x6#k}3lQtdN(%M!?dJ$04KwGd-Dy<+*DF#ca77O+2B=BYnF3a_;0QTT*xw{g;J9t;%J%PBuvOq#$MZgkB3akoT z4IqUz0ftH8n!viibpiTIAuW&**bulOko6+uN;!9kOXHQYk8=hZ_-;9r~$J480OZjXny*d>ejvCmpl#eH_or`Zc zinat@EoM^be0^DrpYA`lT7BU{LF1xwjC>HpeIyK z@2~GEDz1*yw`<$fUW9@1`Z8UPj!HAfGlf!GnqZvc)AhqVS?4){8)T{NyT{A4UH5pI zw&xsKU@23`Cak%XoYh^?#cbxLl`T!xs2tZO_TgDS3MOvimWeRlH*o;BO^gVP;sXQa;@lqs`J%A57`w~_kizJWUisFytL9Y=NME@&#Exh zE2xsObNjWS%BL$cs9j>&JQ|MGCeTR0c-l@by^8GhXj`_zuI4SJp$Dy;>tWst^#q#u5A=9~zhh@GQbf~lXpIDm@I3N7 zqM^x_w!_2wX6&GoZnPl6Umh6U^mPCS9bW^EFQ3T0BCd>Uk~^a3HmlrDaz`=d_#I>@ z3Ga^tLq+&hau3Oe>X7{^c{j<2@x0b^%cipAL6XP$pBY1ir@d|j=Z zl5ar7rDFB6P~gURxg|bsN;@mPlQoy3dC}wx*lv$HZc}_F*^LH&K_KD@{e`y8knF=l zbVNLI<6V(w!O&JP7Qrk>8-SncgY+_jHdd{hr5I#E_A$@>%v7Q_!_(I7XV?iGbHWZ$ z;H9Z0av;=S#11w0V`NX_1#O|)Rq_no3WfX{&>H+_}-Fit!Cs%?2%9gH<{=Wxd1?yVZRU8?gm z`#M9xBwlt`?xxAD*{!ZTNAhvRbSnv}+*{<1=FT~H&bc#h^T%-Y_4ED#9J7q5lST{~DU54Obhi;TGOczDQ^V}x<-GWG zE{of6v506G<}tf0ViNWoi0QDe&{H@lPRyAzDAx6U@ogq4D{-q!9{4!OeZjc6h|)n* zxKK{uNk>AfQtqSWohpg2sy8w8L~mDpj+Py|+A72;t}GbZXM()6`384Q*!9cYZU{<| zTycPuK(Hw@B;wf;Y*#kw>f?s`74m|u?G4vLYW$IXBFeq&m9WgV=B?b*!oO0^W`Akf m2J;^`m7z7%mtSl!65}y5ChTK5B&!}1;5B+i68qBXGWZ3}_bN94 diff --git a/regression/strings-smoke-tests/cprover/CProverString.java b/regression/strings-smoke-tests/cprover/CProverString.java index 572056b2100..0603aac5dc6 100644 --- a/regression/strings-smoke-tests/cprover/CProverString.java +++ b/regression/strings-smoke-tests/cprover/CProverString.java @@ -8,6 +8,29 @@ public static char charAt(String s, int i) { return '\u0000'; } + public static int codePointAt(String s, int index) { + return s.codePointAt(index); + } + + public static int codePointBefore(String s, int index) { + return s.codePointBefore(index); + } + + public static int codePointCount( + String s, int beginIndex, int endIndex) { + return s.codePointCount(beginIndex, endIndex); + } + + public static int offsetByCodePoints( + String s, int index, int codePointOffset) { + return s.offsetByCodePoints(index, codePointOffset); + } + + public static CharSequence subSequence( + String s, int beginIndex, int endIndex) { + return s.subSequence(beginIndex, endIndex); + } + public static String substring(String s, int i) { if (i <= 0) return s; @@ -26,4 +49,102 @@ public static String substring(String s, int i, int j) { return ""; return s.substring(i, j); } + + public static StringBuilder append( + StringBuilder sb, CharSequence cs, int i, int j) { + return sb.append(cs, i, j); + } + + public static StringBuilder delete(StringBuilder sb, int start, int end) { + return sb.delete(start, end); + } + + public static StringBuilder deleteCharAt(StringBuilder sb, int index) { + return sb.deleteCharAt(index); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, String str) { + return sb.insert(offset, str); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, boolean b) { + return sb.insert(offset, b); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, char c) { + return sb.insert(offset, c); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, int i) { + return sb.insert(offset, i); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, long l) { + return sb.insert(offset, l); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, float f) { + return sb.insert(offset, f); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, double d) { + return sb.insert(offset, d); + } + + public static void setLength(StringBuffer sb, int newLength) { + sb.setLength(newLength); + } + + public static char charAt(StringBuffer sb, int index) { + return sb.charAt(index); + } + + public static void setCharAt(StringBuffer sb, int index, char c) { + sb.setCharAt(index, c); + } + + public static StringBuffer delete( + StringBuffer sb, int start, int end) { + return sb.delete(start, end); + } + + public static StringBuffer deleteCharAt(StringBuffer sb, int index) { + return sb.deleteCharAt(index); + } + + public static String substring(StringBuffer sb, int start, int end) { + return sb.substring(start, end); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, String str) { + return sb.insert(offset, str); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, boolean b) { + return sb.insert(offset, b); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, char c) { + return sb.insert(offset, c); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, int i) { + return sb.insert(offset, i); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, long l) { + return sb.insert(offset, l); + } } From 2b92cd3be810a9bfd45323c5e70d53f8ed3ea1e1 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Fri, 9 Feb 2018 21:34:40 +1300 Subject: [PATCH 3/3] Update regression tests to use string primitives Instead of calling the original Java string methods, regression tests now call the jbmc string primitives. Not all string methods have a jbmc counterpart yet. It is limited to methods that throw exceptions. --- .../jbmc-strings/cprover/CProverString.class | Bin 790 -> 4153 bytes .../jbmc-strings/cprover/CProverString.java | 121 ++++++++++++++++++ .../java_delete/test_delete.class | Bin 800 -> 856 bytes .../jbmc-strings/java_delete/test_delete.java | 2 +- .../test_delete_char_at.class | Bin 867 -> 923 bytes .../test_delete_char_at.java | 2 +- .../java_insert_char/test_insert_char.class | Bin 811 -> 867 bytes .../java_insert_char/test_insert_char.java | 2 +- .../java_insert_char_array/test.desc | 4 +- .../test_insert_char_array.class | Bin 1360 -> 1416 bytes .../test_insert_char_array.java | 2 +- .../java_insert_int/test_insert_int.class | Bin 810 -> 866 bytes .../java_insert_int/test_insert_int.java | 2 +- .../test_insert_multiple.class | Bin 898 -> 979 bytes .../test_insert_multiple.java | 4 +- .../test_insert_string.class | Bin 841 -> 897 bytes .../test_insert_string.java | 2 +- .../test_append_string.class | Bin 1577 -> 1602 bytes .../test_append_string.java | 2 +- .../java_append_string/test_substring.desc | 2 +- .../java_code_point/test_code_point.class | Bin 1090 -> 1123 bytes .../java_code_point/test_code_point.java | 8 +- .../java_delete/test_delete.class | Bin 943 -> 856 bytes .../java_delete/test_delete.java | 2 +- .../test_delete_char_at.class | Bin 867 -> 923 bytes .../test_delete_char_at.java | 2 +- .../java_insert_char/test_insert_char.class | Bin 811 -> 867 bytes .../java_insert_char/test_insert_char.java | 2 +- .../test_insert_char_array.class | Bin 1185 -> 1241 bytes .../test_insert_char_array.java | 2 +- .../java_insert_int/test_insert_int.class | Bin 810 -> 866 bytes .../java_insert_int/test_insert_int.java | 2 +- .../test_insert_multiple.class | Bin 898 -> 979 bytes .../test_insert_multiple.java | 4 +- .../test_insert_string.class | Bin 841 -> 897 bytes .../test_insert_string.java | 2 +- .../java_subsequence/test_subsequence.class | Bin 789 -> 835 bytes .../java_subsequence/test_subsequence.java | 2 +- 38 files changed, 146 insertions(+), 25 deletions(-) diff --git a/regression/jbmc-strings/cprover/CProverString.class b/regression/jbmc-strings/cprover/CProverString.class index c1cf5742e3955fa4c05a1d8df8a09fcc6d21d44c..8eb78d4aaa4179eb951b284df7cf07f2b598d2f5 100644 GIT binary patch literal 4153 zcmbVOTXz#x6#k}3lQtdN(%M!?dJ$04KwGd-Dy<+*DF#ca77O+2B=BYnF3a_;0QTT*xw{g;J9t;%J%PBuvOq#$MZgkB3akoT z4IqUz0ftH8n!viibpiTIAuW&**bulOko6+uN;!9kOXHQYk8=hZ_-;9r~$J480OZjXny*d>ejvCmpl#eH_or`Zc zinat@EoM^be0^DrpYA`lT7BU{LF1xwjC>HpeIyK z@2~GEDz1*yw`<$fUW9@1`Z8UPj!HAfGlf!GnqZvc)AhqVS?4){8)T{NyT{A4UH5pI zw&xsKU@23`Cak%XoYh^?#cbxLl`T!xs2tZO_TgDS3MOvimWeRlH*o;BO^gVP;sXQa;@lqs`J%A57`w~_kizJWUisFytL9Y=NME@&#Exh zE2xsObNjWS%BL$cs9j>&JQ|MGCeTR0c-l@by^8GhXj`_zuI4SJp$Dy;>tWst^#q#u5A=9~zhh@GQbf~lXpIDm@I3N7 zqM^x_w!_2wX6&GoZnPl6Umh6U^mPCS9bW^EFQ3T0BCd>Uk~^a3HmlrDaz`=d_#I>@ z3Ga^tLq+&hau3Oe>X7{^c{j<2@x0b^%cipAL6XP$pBY1ir@d|j=Z zl5ar7rDFB6P~gURxg|bsN;@mPlQoy3dC}wx*lv$HZc}_F*^LH&K_KD@{e`y8knF=l zbVNLI<6V(w!O&JP7Qrk>8-SncgY+_jHdd{hr5I#E_A$@>%v7Q_!_(I7XV?iGbHWZ$ z;H9Z0av;=S#11w0V`NX_1#O|)Rq_no3WfX{&>H+_}-Fit!Cs%?2%9gH<{=Wxd1?yVZRU8?gm z`#M9xBwlt`?xxAD*{!ZTNAhvRbSnv}+*{<1=FT~H&bc#h^T%-Y_4ED#9J7q5lST{~DU54Obhi;TGOczDQ^V}x<-GWG zE{of6v506G<}tf0ViNWoi0QDe&{H@lPRyAzDAx6U@ogq4D{-q!9{4!OeZjc6h|)n* zxKK{uNk>AfQtqSWohpg2sy8w8L~mDpj+Py|+A72;t}GbZXM()6`384Q*!9cYZU{<| zTycPuK(Hw@B;wf;Y*#kw>f?s`74m|u?G4vLYW$IXBFeq&m9WgV=B?b*!oO0^W`Akf m2J;^`m7z7%mtSl!65}y5ChTK5B&!}1;5B+i68qBXGWZ3}_bN94 diff --git a/regression/jbmc-strings/cprover/CProverString.java b/regression/jbmc-strings/cprover/CProverString.java index 572056b2100..0603aac5dc6 100644 --- a/regression/jbmc-strings/cprover/CProverString.java +++ b/regression/jbmc-strings/cprover/CProverString.java @@ -8,6 +8,29 @@ public static char charAt(String s, int i) { return '\u0000'; } + public static int codePointAt(String s, int index) { + return s.codePointAt(index); + } + + public static int codePointBefore(String s, int index) { + return s.codePointBefore(index); + } + + public static int codePointCount( + String s, int beginIndex, int endIndex) { + return s.codePointCount(beginIndex, endIndex); + } + + public static int offsetByCodePoints( + String s, int index, int codePointOffset) { + return s.offsetByCodePoints(index, codePointOffset); + } + + public static CharSequence subSequence( + String s, int beginIndex, int endIndex) { + return s.subSequence(beginIndex, endIndex); + } + public static String substring(String s, int i) { if (i <= 0) return s; @@ -26,4 +49,102 @@ public static String substring(String s, int i, int j) { return ""; return s.substring(i, j); } + + public static StringBuilder append( + StringBuilder sb, CharSequence cs, int i, int j) { + return sb.append(cs, i, j); + } + + public static StringBuilder delete(StringBuilder sb, int start, int end) { + return sb.delete(start, end); + } + + public static StringBuilder deleteCharAt(StringBuilder sb, int index) { + return sb.deleteCharAt(index); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, String str) { + return sb.insert(offset, str); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, boolean b) { + return sb.insert(offset, b); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, char c) { + return sb.insert(offset, c); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, int i) { + return sb.insert(offset, i); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, long l) { + return sb.insert(offset, l); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, float f) { + return sb.insert(offset, f); + } + + public static StringBuilder insert( + StringBuilder sb, int offset, double d) { + return sb.insert(offset, d); + } + + public static void setLength(StringBuffer sb, int newLength) { + sb.setLength(newLength); + } + + public static char charAt(StringBuffer sb, int index) { + return sb.charAt(index); + } + + public static void setCharAt(StringBuffer sb, int index, char c) { + sb.setCharAt(index, c); + } + + public static StringBuffer delete( + StringBuffer sb, int start, int end) { + return sb.delete(start, end); + } + + public static StringBuffer deleteCharAt(StringBuffer sb, int index) { + return sb.deleteCharAt(index); + } + + public static String substring(StringBuffer sb, int start, int end) { + return sb.substring(start, end); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, String str) { + return sb.insert(offset, str); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, boolean b) { + return sb.insert(offset, b); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, char c) { + return sb.insert(offset, c); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, int i) { + return sb.insert(offset, i); + } + + public static StringBuffer insert( + StringBuffer sb, int offset, long l) { + return sb.insert(offset, l); + } } diff --git a/regression/jbmc-strings/java_delete/test_delete.class b/regression/jbmc-strings/java_delete/test_delete.class index 7036ce13c9036943ef66368d595e31b8ed88ca47..251aa67bc18c05fa21ee6d60c2c45caaf5b41d5b 100644 GIT binary patch delta 204 zcmZ3$c7x63)W2Q(7#J8#7%aFL_!wl^8Du#a@GuxNm`oO7)Mhi~VK8GbpX|!$;2@b_l&+s#P?TSmTBPqB0H%XWiZb)k85!78 tQgc#EQW+V{G<>oW%M$f-67$maA+k=TnK>z`Mb?uiFn(g(F}ay(E&yRXE5rZ* delta 155 zcmcb?wt&s$)W2Q(7#J8#7|ggB_!wl^8Du#a?;$TqbVo+gF zWoJ<1V&DR)ROe#QV9;b|(3)g8>f%KZ5`x1CwJiJA*b4 zgCT>_WN}7qHe(*3Ri=|Y7#;Z7Qc`nLOHvsbWHmfJH7BoUl$`v8@fzc{$-9~60syw1 B8Y}<+ diff --git a/regression/jbmc-strings/java_delete/test_delete.java b/regression/jbmc-strings/java_delete/test_delete.java index ea846cd215a..62ea5dbf9ce 100644 --- a/regression/jbmc-strings/java_delete/test_delete.java +++ b/regression/jbmc-strings/java_delete/test_delete.java @@ -3,7 +3,7 @@ public class test_delete public static void main(/*String[] argv*/) { StringBuilder s = new StringBuilder("Abc"); - s.delete(1,2); + org.cprover.CProverString.delete(s,1,2); String str = s.toString(); assert(!str.equals("Ac")); } diff --git a/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class b/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class index ed3148e2f7e60738b9863b1e47c0d50650b289cc..130e3d10f6c1fc4b451b5ce93a816a301c3171d7 100644 GIT binary patch delta 202 zcmaFNHk;k^)W2Q(7#J8#7_7J$_!(r`8RWPam>6U^800~;0vCfKgA$0P%*nvZpu)kR z%Eh3@pw7;q!NtH0Qm)Cxpv9og&Y&~VGmcSr;)*CGJqCSt1_K@jLk1%r24e;j9tHsh zK}H59$7FT}T^*hOvX@0}27f2r)`w%8CkANlg(A_PU}$Q_?zlE73k( z7j}oPrbk~hV5muu6j<&?($mRh9m8~~<+ONuh{(is`p dGV_X4i%J+7%rqv?Wt5yei}5q#j>&yYa{+RrBzOP- delta 149 zcmaFNwwlf5)W2Q(7#J8#7|ggB_!wl^8Du#a?;$TqbVo+gF zWoJ<1V&DR)ROe#QV9;b|(34}&g)9uI>)g8>f%KZ5`x19M_hGCPAd u4}&3t(PSA$12$tGpk1bugBTsS*)sErQ;SL%8DupkUt;{sxNY(=rnvx0YZ&|h diff --git a/regression/jbmc-strings/java_insert_char/test_insert_char.java b/regression/jbmc-strings/java_insert_char/test_insert_char.java index 3a83f03b332..12dcc8cdb90 100644 --- a/regression/jbmc-strings/java_insert_char/test_insert_char.java +++ b/regression/jbmc-strings/java_insert_char/test_insert_char.java @@ -3,7 +3,7 @@ public class test_insert_char public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ac"); - sb.insert(1, 'b'); + org.cprover.CProverString.insert(sb, 1, 'b'); String s = sb.toString(); assert(!s.equals("abc")); } diff --git a/regression/jbmc-strings/java_insert_char_array/test.desc b/regression/jbmc-strings/java_insert_char_array/test.desc index 012a7e34e22..0fd3fc08bb0 100644 --- a/regression/jbmc-strings/java_insert_char_array/test.desc +++ b/regression/jbmc-strings/java_insert_char_array/test.desc @@ -3,6 +3,6 @@ test_insert_char_array.class --refine-strings --string-max-length 1000 --function test_insert_char_array.main ^EXIT=10$ ^SIGNAL=0$ -assertion.* line 28.* SUCCESS$ -assertion.* line 30.* FAILURE$ +assertion.* line 26.* SUCCESS$ +assertion.* line 28.* FAILURE$ -- diff --git a/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class b/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class index 302260031f2e028ac521be852138f3a632d4e524..c19a742c0f4ddb43f1234627a0ee00cf490fecfb 100644 GIT binary patch delta 290 zcmW-c%PvDv7)IBw!)~|jlG1W$OJh<7j!RqjYj5sK2PPe;RvHtP6Y&5>CL+z5nRx^; z5eYFi@+MwD#AdR-^$os1`9IZ7yZZQfc>|J^nkt@hnD8^H2r?C5nxrB{I$-LIpIOBm z^O6NcHwnq2Vu@wRO7r;DT9vGMaZ%2%YcgatIr5r8B9ek;hz)_SQv0)E$);wDZOM*i z7c&SE7Fd;&YRz2H?6L2?i*#F2bHJhZE$(7=!>v2j3%7A~>N=U?f0i!Yv-7&3knkRS z_S3EJUPPbqA3d6P1OtYhv>0~KYE0ARWv%PcAc`K-dksVM6DCF|X2@(gKP$U+j1&-i6B8oFqHWWVPGpwxa47r_uVN5Jcv@teT zevx`KC)qiB$j-j&`f~2``{fN-q|tWyQou~atfPmyB=amdHA+dP<%lK6GAouEYRf(JADOmy+6TMfgCDLVc!K{rC$--NeQeK_q)k)f9X Y2KB}mVnXxNx}`{#swz!#elijN0;E4AbpQYW diff --git a/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java b/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java index 1f93e00b8da..f392655afc1 100644 --- a/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java +++ b/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java @@ -11,7 +11,7 @@ public static String stringOfCharArray(char arr[]) public static void insert(StringBuilder sb, int pos, char arr[]) { String s=stringOfCharArray(arr); - sb.insert(pos, s); + org.cprover.CProverString.insert(sb, pos, s); } public static void main(int i) { diff --git a/regression/jbmc-strings/java_insert_int/test_insert_int.class b/regression/jbmc-strings/java_insert_int/test_insert_int.class index cd355c86546c241bb051f08cde05d31a44674c53..538a5890e2d56fddf879cf342c1addf7e7541d89 100644 GIT binary patch delta 185 zcmZ3*_K3~p)W2Q(7#J8#7%aFL_!wl^8Du#a=?;HT8gG-7s^U@g^ e*fR5qQ;SL%8O$^$&ta6DJd^P=?;$TqbVo+gF zWoJ<1V&DR)ROe#QV9;b|(3)g8>f%KZ5`x152WbQ8GJ& vHV=a#gVAIeMtwG89-w8WlLHwYxY;uEic^b97#U7R|y#V diff --git a/regression/jbmc-strings/java_insert_int/test_insert_int.java b/regression/jbmc-strings/java_insert_int/test_insert_int.java index 15a7a2d53f6..2765859866f 100644 --- a/regression/jbmc-strings/java_insert_int/test_insert_int.java +++ b/regression/jbmc-strings/java_insert_int/test_insert_int.java @@ -3,7 +3,7 @@ public class test_insert_int public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ac"); - sb.insert(1, 42); + org.cprover.CProverString.insert(sb, 1, 42); String s = sb.toString(); assert(!s.equals("a42c")); } diff --git a/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class b/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class index d6b470a1f72e41dd2bae763f8e15e9b5239bdd9f..9e6a87de460edd04e3d7b1da2ef15b32d1eece00 100644 GIT binary patch delta 294 zcmZo-zs&A)>ff$?3=9k=47OYh0t|BO4DuWd3S10K42oO~N({;z3@RX66(pj@$-u{; z&cUF;#h}Tc#m=D3#lQp7p~J^3pg++kj?rM^>KJW9b_OFJ24e;jMh3?LMF)2BPoxy;I!GghZvOc2;n-vd(HG|FMOh$)#$^4>p{p5n8{Ib*{ zedho$9b8hBnU~JUz?PX;oLW@E$Y7@7la*MOsGpOVm#zff$?3=9k=4Axu>0t|BO4DuWd3S10K42mE^iGx8IM5}-ZRZa#z1~m=_ zbuI=C22FMbEiMKgkPdAw1|0@nb_TtPK5>lt6IaJ*81OI{G8i#3FeZT*#ymjdO?emu z8H5-aSQ3+xQ`i~wc^J$X%qJT$ny^{$Fjz8JP0nF-;AYFrD^4vcVPufinEZxOj!92r Yvnmq{Bj+{-)^IHrA+~LkjhGh#03v4`dH?_b diff --git a/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java b/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java index c976ddd807f..60daceea887 100644 --- a/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java +++ b/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java @@ -3,8 +3,8 @@ public class test_insert_multiple public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ad"); - sb.insert(1, 'c'); - sb.insert(1, "b"); + org.cprover.CProverString.insert(sb, 1, 'c'); + org.cprover.CProverString.insert(sb, 1, "b"); String s = sb.toString(); assert(!s.equals("abcd")); } diff --git a/regression/jbmc-strings/java_insert_string/test_insert_string.class b/regression/jbmc-strings/java_insert_string/test_insert_string.class index be8f7ad0f79126964af9df57d0e5500d86d69cdd..e5990e07a15d25e478bdb5a83afa107b1553147c 100644 GIT binary patch delta 196 zcmX@f*2wOD>ff$?3=9k=3|3qW{0y?}400R{@>~o|3JA>{-_c%tqiOZtY^%)tMl9JgO40sp}8H{)sj2TRL z7z7vu85vj-laf=|8T5D4DK2}6Ca2(T5n#?$im3DWAYlNxd6R`CMf^_ delta 159 zcmWm4ISv6)9DwofKbg!MZ=T=)_I=-%Qs)i|VkAY C=NaMv diff --git a/regression/jbmc-strings/java_insert_string/test_insert_string.java b/regression/jbmc-strings/java_insert_string/test_insert_string.java index 028a348122b..50cd222f6ec 100644 --- a/regression/jbmc-strings/java_insert_string/test_insert_string.java +++ b/regression/jbmc-strings/java_insert_string/test_insert_string.java @@ -3,7 +3,7 @@ public class test_insert_string public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ad"); - sb.insert(1, "bc"); + org.cprover.CProverString.insert(sb, 1, "bc"); String s = sb.toString(); assert(!s.equals("abcd")); } diff --git a/regression/strings-smoke-tests/java_append_string/test_append_string.class b/regression/strings-smoke-tests/java_append_string/test_append_string.class index 3594e509e8700037ca37e4a6569574dad55021e5..020199a685440e7d9df58dd84ad38b004e785cc4 100644 GIT binary patch delta 80 zcmV-W0I&b448jbMS_?b?JqiE<06q!;Jh5eP0T%}VRSW<}09FhDR{&TH09gQ93;-Nw`cMsXencZN_NhA@V3c7_NZhDe4e9)@U!@Xc=+ xy%?EHH74gWM@vcO7p3bb7Zl}}r55Qs2Y~6|lA_GK^v%bZYZ)20O?F}Z2LK_N8fyRm diff --git a/regression/strings-smoke-tests/java_append_string/test_append_string.java b/regression/strings-smoke-tests/java_append_string/test_append_string.java index 83a9ddf9b4c..d5665b01a88 100644 --- a/regression/strings-smoke-tests/java_append_string/test_append_string.java +++ b/regression/strings-smoke-tests/java_append_string/test_append_string.java @@ -17,7 +17,7 @@ public static void check(StringBuilder sb, String str) String init = sb.toString(); if(str.length() >= 4) { - sb.append(str, 2, 4); + org.cprover.CProverString.append(sb, str, 2, 4); String res = sb.toString(); assert(res.startsWith(init)); assert(res.endsWith(org.cprover.CProverString.substring(str, 2, 4))); diff --git a/regression/strings-smoke-tests/java_append_string/test_substring.desc b/regression/strings-smoke-tests/java_append_string/test_substring.desc index de4c8675ad1..dfddb22d72b 100644 --- a/regression/strings-smoke-tests/java_append_string/test_substring.desc +++ b/regression/strings-smoke-tests/java_append_string/test_substring.desc @@ -1,6 +1,6 @@ CORE test_append_string.class ---refine-strings --verbosity 10 --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null +--refine-strings --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.*\].* line 22.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_code_point/test_code_point.class b/regression/strings-smoke-tests/java_code_point/test_code_point.class index df523be365ba4f6037c25c04e198b74e673bd336..c07bae0ffb5bc0072e4080b71261b391683c7a6b 100644 GIT binary patch delta 203 zcmX@a@tA|_)W2Q(7#J8#7@Q_@*$OK&Xmc@eGw850=yEaWG3c{17)*?cW;C3*ZM_N) zgEfN<4}&d(9U}vONosLPd~$wDYJ5R{W?l(9gFO#}1B2t_9!8DHR!lNn+#tCCkksU8 zCaKBC7}XfXCnqq8On%SkJvof&veym<79rO84BWdJ*dn(xu zgEbF>4TCKYgB^oCBLja)YH>+?a(+r`d_jI@UI{yc0}q2EgVW?rMhyXOkaz${*s+9> zfkk8Tdqxc=R*lKpOg@u0GRjOYXS(dQje$jobv^_4ZU(l= 2); - assert(s.offsetByCodePoints(1,2) >= 3); + assert(org.cprover.CProverString.codePointAt(s, 1) == 67847); + assert(org.cprover.CProverString.codePointBefore(s, 3) == 67847); + assert(org.cprover.CProverString.codePointCount(s,1,5) >= 2); + assert(org.cprover.CProverString.offsetByCodePoints(s,1,2) >= 3); StringBuilder sb = new StringBuilder(); sb.appendCodePoint(0x10907); assert(org.cprover.CProverString.charAt(s, 1) == org.cprover.CProverString.charAt(sb.toString(), 0)); diff --git a/regression/strings-smoke-tests/java_delete/test_delete.class b/regression/strings-smoke-tests/java_delete/test_delete.class index f18891851b1e69aae1bc9416dd3316dab6c8e3b1..44a8fdc10db2d6d2f74b2300b796753d55a27517 100644 GIT binary patch delta 485 zcmYL_&rTCj6vlsd+L_xNuRy1K#g@grYOiE%{j%CsS4UkD8tn?Y0 z?)m~QjheJX5?z?M@CkSlcN)$N5jW?Yd(L;i?>pzCK6h4s{r&n4sPfF^8WWny6t`V0 z?zr6LUQ`v+81AQ-a+zjEGwb3;$T^n>lr-hetM&X)z3n&lUiycd{@Yd{G@AL&&q^Xo zuJgNC%u>-T7(5;t9oZ2)&ip zajv(+o&Bc5*$!GkJ5VgmZS4BTzSr{io8IO0#nDb{I|!G%KUA%|Y1Q8w*$dS0Xe23B z0)@Dectc*3l9gn;G(dfdfaE1QaZ{0IYWs9GzsC7atqKDv7n*_q;gTk$`q?Aq-j+Q601H# z6`XmH&j%^}TUiz5yO zN272o3R5=6IpJ`Ul1+-T#k50(s;1`PMw(L&bxv!}bZ^|Mjg=lPJoR3B^|septuF;z zYn|0*`GI0&DezXFEqa^xyvJ={HfhdwU)RhWc|{?7s|ww3Rz1f#S8!%r&T~O?(d81C zHBFZ*Q71!IVa%!kemh6pG{~4lb68Z^6d0FxG`c0ynBKzyMRPxMJVtn@J#chS{8 z)-HCBd^PLzN%lzYZR0Kv82J==8$<6&ahHWSk~3(jS%P89H613TlSF-|p_$a|m)3zl mtc@WQWU{F~`+Dg38{)C|*nho$b4NZ247a5m5fz8K5B>ySqFxdJ diff --git a/regression/strings-smoke-tests/java_delete/test_delete.java b/regression/strings-smoke-tests/java_delete/test_delete.java index 13bd09cd075..99298e536c3 100644 --- a/regression/strings-smoke-tests/java_delete/test_delete.java +++ b/regression/strings-smoke-tests/java_delete/test_delete.java @@ -3,7 +3,7 @@ public class test_delete public static void main(/*String[] argv*/) { StringBuilder s = new StringBuilder("Abc"); - s.delete(1,2); + org.cprover.CProverString.delete(s,1,2); String str = s.toString(); assert(str.equals("Ac")); } diff --git a/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class b/regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.class index cfd8561e5960688dd28ec9e722c7353b57d35ec8..d9148dfc2112f54814f3231a370326c490b626f8 100644 GIT binary patch delta 202 zcmaFNHk;k^)W2Q(7#J8#7_7J$_!(r`8RWPam>6U^800~;0vCfKgA$0P%*nvZpu)kR z%Eh3@pw7;q!NtH0Qm)Cxpv9og&Y&~VGmcSr;)*CGJqCSt1_K@jLk1%r24e;j9tHsh zK}H59$7FT}T^*hOvX@0}27f2r)`w%8CkANlg(A_PU}$Q_?zlE73k( z7j}oPrbk~hV5muu6j<&?($mRh9m8~~<+ONuh{(is`p dGV_X4i%J+7%rqv?Wt5yei}5q#j>&yYa{+RrBzOP- delta 149 zcmaFNwwlf5)W2Q(7#J8#7|ggB_!wl^8Du#a?;$TqbVo+gF zWoJ<1V&DR)ROe#QV9;b|(34}&g)9uI>)g8>f%KZ5`x19M_hGCPAd u4}&3t(PSA$12$tGpk1bugBTsS*)sErQ;SL%8DupkUt;{sxNY(=rnvx0YZ&|h diff --git a/regression/strings-smoke-tests/java_insert_char/test_insert_char.java b/regression/strings-smoke-tests/java_insert_char/test_insert_char.java index ac6beb4ffcf..940292296f1 100644 --- a/regression/strings-smoke-tests/java_insert_char/test_insert_char.java +++ b/regression/strings-smoke-tests/java_insert_char/test_insert_char.java @@ -3,7 +3,7 @@ public class test_insert_char public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ac"); - sb.insert(1, 'b'); + org.cprover.CProverString.insert(sb, 1, 'b'); String s = sb.toString(); assert(s.equals("abc")); } diff --git a/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.class b/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.class index d0edb7e3e24763f20cd2df4361d9678ad838b983..ceb34bf1896283ce163ac530457738e03d8e2d65 100644 GIT binary patch delta 240 zcmW-YOG?8~6hP0T;!Pe8#EDqMQT)_Tjh|Y7^;>NfCqjlDgcw8Zq?OkwxCjTKE9e@E zAP!uBJ8%KwF2vT+IdC|A_sb1Ff8RfV5?7i@JeLXPgn3O4PqVXU<4tjOvT~|h$Hym;#92-tJ70wJ* zDvGh_HohBPhI1|yQ)$vo!&bYS*ffmqBO6B6M$bacQ0KDus*1Duj&1t!gY7&e*00|D YGe~W#-Bgsb{>InMM!#D&jq6e83v<5+< zhZf)tT0y&zX5J3J!|(k1pMGaH|Na3^dD1LV@L6O_*w(ldG&zbw$)lX%j!tDIqg|gp zs+xTcJPtKS91ABpt<;42xbq<;;Y>Im|GjvIRW20yWYft%D;ygdmT6@3n&FZw;o5M+ ztC_AH_j$V57iBk$o2)43D&vFI9Cm%9C~HO{wW5 Haog%2f~F+% diff --git a/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java b/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java index ab28b86ffdc..543b9aa2024 100644 --- a/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java +++ b/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java @@ -4,7 +4,7 @@ public static void insert(StringBuilder sb, int offset, char[] arr) { assert(arr.length<5); for(int i=0; i=?;HT8gG-7s^U@g^ e*fR5qQ;SL%8O$^$&ta6DJd^P=?;$TqbVo+gF zWoJ<1V&DR)ROe#QV9;b|(3)g8>f%KZ5`x152WbQ8GJ& vHV=a#gVAIeMtwG89-w8WlLHwYxY;uEic^b97#U7R|y#V diff --git a/regression/strings-smoke-tests/java_insert_int/test_insert_int.java b/regression/strings-smoke-tests/java_insert_int/test_insert_int.java index b787141e51a..e480683821f 100644 --- a/regression/strings-smoke-tests/java_insert_int/test_insert_int.java +++ b/regression/strings-smoke-tests/java_insert_int/test_insert_int.java @@ -3,7 +3,7 @@ public class test_insert_int public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ac"); - sb.insert(1, 42); + org.cprover.CProverString.insert(sb, 1, 42); String s = sb.toString(); assert(s.equals("a42c")); } diff --git a/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.class b/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.class index 17ced6ec67ccfb1c029201464eccaaedd035cffc..443b43e90ddd74b00b6f6e6921f924f0d6cd28cd 100644 GIT binary patch delta 294 zcmZo-zs&A)>ff$?3=9k=47OYh0t|BO4DuWd3S10K42oO~N({;z3@RX66(pj@$-u{; z&cUF;#h}Tc#m=D3#lQp7p~J^3pg++kj?rM^>KJW9b_OFJ24e;jMh3?LMF)2BPoxy;I!GghZvOc2;n-vd(HG|FMOh$)#$^4>p{p5n8{Ib*{ zedho$9b8hBnU~JUz?PX;oLW@E$Y7@7la*MOsGpOVm#zff$?3=9k=4Axu>0t|BO4DuWd3S10K42mE^iGx8IM5}-ZRZa#z1~m=_ zbuI=C22FMbEiMKgkPdAw1|0@nb_TtPK5>lt6IaJ*81OI{G8i#3FeZT*#ymjdO?emu z8H5-aSQ3+xQ`i~wc^J$X%qJT$ny^{$Fjz8JP0nF-;AYFrD^4vcVPufinEZxOj!92r Yvnmq{Bj+{-)^IHrA+~LkjhGh#03v4`dH?_b diff --git a/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java b/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java index cce6881ca7d..b505e24020e 100644 --- a/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java +++ b/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java @@ -3,8 +3,8 @@ public class test_insert_multiple public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ad"); - sb.insert(1, 'c'); - sb.insert(1, "b"); + org.cprover.CProverString.insert(sb, 1, 'c'); + org.cprover.CProverString.insert(sb, 1, "b"); String s = sb.toString(); assert(s.equals("abcd")); } diff --git a/regression/strings-smoke-tests/java_insert_string/test_insert_string.class b/regression/strings-smoke-tests/java_insert_string/test_insert_string.class index 39cc969a902e163ccfdfe821e6b8ae8b9f30aa07..fdadf1f64921ead702eaf4b388519ae568839d52 100644 GIT binary patch delta 196 zcmX@f*2wOD>ff$?3=9k=3|3qW{0y?}400R{@>~o|3JA>{-_c%tqiOZtY^%)tMl9JgO40sp}8H{)sj2TRL z7z7vu85vj-laf=|8T5D4DK2}6Ca2(T5n#?$im3DWAYlNxd6R`CMf^_ delta 159 zcmWm4ISv6)9DwofKbg!MZ=T=)_I=-%Qs)i|VkAY C=NaMv diff --git a/regression/strings-smoke-tests/java_insert_string/test_insert_string.java b/regression/strings-smoke-tests/java_insert_string/test_insert_string.java index 7c161205131..547b89ae569 100644 --- a/regression/strings-smoke-tests/java_insert_string/test_insert_string.java +++ b/regression/strings-smoke-tests/java_insert_string/test_insert_string.java @@ -3,7 +3,7 @@ public class test_insert_string public static void main(/*String[] argv*/) { StringBuilder sb = new StringBuilder("ad"); - sb.insert(1, "bc"); + org.cprover.CProverString.insert(sb, 1, "bc"); String s = sb.toString(); assert(s.equals("abcd")); } diff --git a/regression/strings-smoke-tests/java_subsequence/test_subsequence.class b/regression/strings-smoke-tests/java_subsequence/test_subsequence.class index 0f8410939e1af315893c149dafa8190916146c35..17265a88517b08659420e54383c6cf7f76eaa8ca 100644 GIT binary patch delta 120 zcmbQrc9@Op)W2Q(7#J8#81yD`o#a#FVNhq#U}sR}VbEmIn)uL^O`C^7he3C;45Oo+ zWPVY)esV!kepzafzH55B$NOE delta 74 zcmV-Q0JZNE4DhvQC04$Rn g0YMN8b9G`