From 9ff1e825e059e4c091f4c8e642ca6e924c87102d Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 19 Mar 2018 08:44:18 +0000 Subject: [PATCH 1/7] Fix eval of insert to match string constraints String constraints for insert are permisive with index that are negative or exceed the length of the string so the eval method should do the same, and in particular should not make an invariant fail. --- .../refinement/string_refinement_util.cpp | 22 +++++++++++-------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 236847659a0..46cb5178389 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -322,18 +322,22 @@ std::vector string_insertion_builtin_functiont::eval( const std::vector &args_value) const { PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3); - const std::size_t &offset = numeric_cast_v(args_value[0]); - const std::size_t &start = - args_value.size() > 1 ? numeric_cast_v(args_value[1]) : 0; - const std::size_t &end = args_value.size() > 2 - ? numeric_cast_v(args_value[2]) - : input2_value.size(); + const auto offset = std::max(args_value[0], mp_integer(0)); + const auto start = args_value.size() > 1 + ? std::max(args_value[1], mp_integer(0)) + : mp_integer(0); + + const mp_integer input2_size(input2_value.size()); + const auto end = + args_value.size() > 2 + ? std::max(std::min(args_value[2], input2_size), mp_integer(0)) + : input2_size; std::vector result(input1_value); result.insert( - result.begin() + offset, - input2_value.begin() + start, - input2_value.end() + end); + result.begin() + numeric_cast_v(offset), + input2_value.begin() + numeric_cast_v(start), + input2_value.begin() + numeric_cast_v(end)); return result; } From 5f96226e50b3f5cecf2474f753ade364b8e02beb Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 15 Mar 2018 15:14:40 +0000 Subject: [PATCH 2/7] Fix string constraints for substring It was previously not clear what could happen when the argument of substring were out of bounds. This is now clearly specified and avoids getting formulas with array accesses at negative indexes in particular. --- .../refinement/string_constraint_generator.h | 3 ++ .../string_constraint_generator_main.cpp | 5 +++ ...ng_constraint_generator_transformation.cpp | 41 ++++++++----------- 3 files changed, 24 insertions(+), 25 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 68e77136a15..b7a3397acb9 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -439,4 +439,7 @@ utf16_constant_array_to_java(const array_exprt &arr, std::size_t length); /// \return expression representing the minimum of two expressions exprt minimum(const exprt &a, const exprt &b); +/// \return expression representing the maximum of two expressions +exprt maximum(const exprt &a, const exprt &b); + #endif diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index a739aa18efe..efd85c8165b 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -667,3 +667,8 @@ exprt minimum(const exprt &a, const exprt &b) { return if_exprt(binary_relation_exprt(a, ID_le, b), a, b); } + +exprt maximum(const exprt &a, const exprt &b) +{ + return if_exprt(binary_relation_exprt(a, ID_le, b), b, a); +} diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index e4df62603fd..a5b01005c7b 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -98,16 +98,14 @@ exprt string_constraint_generatort::add_axioms_for_substring( } /// Add axioms ensuring that `res` corresponds to the substring of `str` -/// between indexes `start` and `end`. +/// between indexes `start' = max(start, 0)` and +/// `end' = max(min(end, |str|), start')`. /// /// These axioms are: -/// 1. \f$ {\tt start} < {\tt end} \Rightarrow -/// |{\tt res}| = {\tt end} - {\tt start} \f$ -/// 2. \f$ {\tt start} \ge {\tt end} \Rightarrow |{\tt res}| = 0 \f$ -/// 3. \f$ |{\tt str}| > {\tt end} \f$ -/// 4. \f$ \forall i<|{\tt str}|.\ {\tt res}[i]={\tt str}[{\tt start}+i] \f$ -/// \todo Should return code different from 0 if `|str| <= |end|` instead of -/// adding constraint 3. +/// 1. \f$ |{\tt res}| = end' - start' \f$ +/// 2. \f$ \forall i<|{\tt res}|.\ {\tt res}[i]={\tt str}[{\tt start'}+i] \f$ +/// \todo Should return code different from 0 if `start' != start` or +/// `end' != end` /// \param res: array of characters expression /// \param str: array of characters expression /// \param start: integer expression @@ -123,26 +121,19 @@ exprt string_constraint_generatort::add_axioms_for_substring( PRECONDITION(start.type()==index_type); PRECONDITION(end.type()==index_type); - // We add axioms: + const exprt start1 = maximum(start, from_integer(0, start.type())); + const exprt end1 = maximum(minimum(end, str.length()), start1); - implies_exprt a1( - binary_relation_exprt(start, ID_lt, end), - res.axiom_for_has_length(minus_exprt(end, start))); - lemmas.push_back(a1); + // Axiom 1. + lemmas.push_back(equal_exprt(res.length(), minus_exprt(end1, start1))); - exprt is_empty=res.axiom_for_has_length(from_integer(0, index_type)); - implies_exprt a2(binary_relation_exprt(start, ID_ge, end), is_empty); - lemmas.push_back(a2); + // Axiom 2. + constraints.push_back([&] { // NOLINT + const symbol_exprt idx = fresh_univ_index("QA_index_substring", index_type); + return string_constraintt( + idx, res.length(), equal_exprt(res[idx], str[plus_exprt(start1, idx)])); + }()); - // Warning: check what to do if the string is not long enough - lemmas.push_back(str.axiom_for_length_ge(end)); - - symbol_exprt idx=fresh_univ_index("QA_index_substring", index_type); - string_constraintt a4(idx, - res.length(), - equal_exprt(res[idx], - str[plus_exprt(start, idx)])); - constraints.push_back(a4); return from_integer(0, signedbv_typet(32)); } From 4be75327d4dd4046db27b780372588af90f9f11f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 16 Mar 2018 09:15:04 +0000 Subject: [PATCH 3/7] Test for CProverString.insert This function behaves slightly differently from StringBuilder.insert since it never raise an exception. This tests the cases where the index exceeds the limits. --- .../StringBuilderInsert/Test.class | Bin 0 -> 1132 bytes .../StringBuilderInsert/Test.java | 48 ++++++++++++++++++ .../StringBuilderInsert/test.desc | 12 +++++ 3 files changed, 60 insertions(+) create mode 100644 regression/jbmc-strings/StringBuilderInsert/Test.class create mode 100644 regression/jbmc-strings/StringBuilderInsert/Test.java create mode 100644 regression/jbmc-strings/StringBuilderInsert/test.desc diff --git a/regression/jbmc-strings/StringBuilderInsert/Test.class b/regression/jbmc-strings/StringBuilderInsert/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..3496f23684e7b1683c6fab42d5e99f3395c9ada1 GIT binary patch literal 1132 zcmbtTO-~b16g{t#5e}{>6 zu!CUnQ)wrg57=ceiCr7ABo zunmUboLMv7>kR%>`aXlSXq7obc-gG+yY)vUZm$V2L%?{*jV%JC3If-=>gvW;QQ!8` zq>VwDGpdJN>Z(<@4Sw4cl|5_Rai=%+9bLl!VhnNd&Q|qWCA;d{X05VNH>+iClZKLR z3s8=p4=hW@jE3{LprId8jhwhhdMQpQ8J9F%#ubL)Hrsrw$6K~-5nYgg1Sio#f{d#g zt|8A5X_u^&Ho4(445pUb!2?x!(dUR|SF*;oZS8P7yLivL57I<$)`X`Fce;xYTgn&y zLfaK;fyqPHYO%*s=`P@(+FQsVe_YqAPDc|5o#oRs<8ZsR#VRcV!%&$!rp?R09iwr& zbxP0{Y+#)BDnhHrBE!OYdig;+gczNJ^fgL1qdPFw1bZWZ7@{-i1$}hJF-#{x*#?#R zDfcbWKw%HQ^{BrIshIIc1Md+mzJ=UCJhKZW+OrF_fzTd8>rH5%Ix^4NnS}HLOGl_8 z-~WRv(7~m4arORFm&hE^C5-TSMl5*lNsu6ulPbk}k)zlWdAUNitdl(@B=7`DJjEEE z)6e`8lX#6ZJ|ly#$YO-pMiJacPR6kx7}>{6#{&vcv_>-Pc@OkQ`*sm-K$c!X^1p-J UR@EAhU=F~i-4H`O?uj1#1*M|+O#lD@ literal 0 HcmV?d00001 diff --git a/regression/jbmc-strings/StringBuilderInsert/Test.java b/regression/jbmc-strings/StringBuilderInsert/Test.java new file mode 100644 index 00000000000..173b3b53dd2 --- /dev/null +++ b/regression/jbmc-strings/StringBuilderInsert/Test.java @@ -0,0 +1,48 @@ + +public class Test { + public void check (int i) { + if(i == 0) + { + // Arrange + StringBuilder s = new StringBuilder("bar"); + + // Act + s = org.cprover.CProverString.insert(s, 0, "foo"); + + // Should succeed + assert s.toString().equals("foobar"); + + // Should fail + assert !s.toString().equals("foobar"); + } + if(i == 1) + { + // Arrange + StringBuilder s = new StringBuilder("bar"); + + // Act + s = org.cprover.CProverString.insert(s, -10, "foo"); + + // Should succeed + assert s.toString().equals("foobar"); + + // Should fail + assert !s.toString().equals("foobar"); + } + if(i == 2) + { + // Arrange + StringBuilder s = new StringBuilder("bar"); + + // Act + s = org.cprover.CProverString.insert(s, 10, "foo"); + + // Should succeed + assert s.toString().equals("barfoo"); + + // Should fail + assert !s.toString().equals("barfoo"); + } + + } +} diff --git a/regression/jbmc-strings/StringBuilderInsert/test.desc b/regression/jbmc-strings/StringBuilderInsert/test.desc new file mode 100644 index 00000000000..68b636a5d67 --- /dev/null +++ b/regression/jbmc-strings/StringBuilderInsert/test.desc @@ -0,0 +1,12 @@ +CORE +Test.class +--refine-strings --function Test.check +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 13 .*: SUCCESS +assertion at file Test.java line 16 .*: FAILURE +assertion at file Test.java line 27 .*: SUCCESS +assertion at file Test.java line 30 .*: FAILURE +assertion at file Test.java line 41 .*: SUCCESS +assertion at file Test.java line 44 .*: FAILURE +-- From b43bbff4c9dc6a6b3e31e895318c7d1468a06b82 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 16 Mar 2018 10:47:15 +0000 Subject: [PATCH 4/7] Tests for CProverString.substring --- .../jbmc-strings/StringSubstring/Test.class | Bin 0 -> 1409 bytes .../jbmc-strings/StringSubstring/Test.java | 47 ++++++++++++++++++ .../jbmc-strings/StringSubstring/test.desc | 6 +++ .../StringSubstring/test_fail.desc | 10 ++++ 4 files changed, 63 insertions(+) create mode 100644 regression/jbmc-strings/StringSubstring/Test.class create mode 100644 regression/jbmc-strings/StringSubstring/Test.java create mode 100644 regression/jbmc-strings/StringSubstring/test.desc create mode 100644 regression/jbmc-strings/StringSubstring/test_fail.desc diff --git a/regression/jbmc-strings/StringSubstring/Test.class b/regression/jbmc-strings/StringSubstring/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..87ab45d5ca6cac299ef4981df65a74c90b799e63 GIT binary patch literal 1409 zcmZuxO>Y}j6g|)L8E0ZUlQ@kVJN-(i9lJJ!P#{T5Q@4RgEg-ofqU~m4Ptz&J6K2L; zu;w4Ifrtg_rt5&@R#dr4Ros&S_KqHM&%o}*!#2Y3SO}uGfDUG*q-oV=e z6LU@&xe!K04p}?{7wR_Her_ptK+l^Kfc)jhFjSU%KtQ9%!&#pT=@jVh^1p=nLz3zBj zW+>Coz&ku#ZFgTJPq+Mj(0127nQG()o$E5bg((~}@UDertT5~0oR|Avx8nvDR&l|? zMZ9O>64oqCB5&a`nij6$s=#z|Z*5ScnAyDvx?M8bi@b9}pqxo_C-cK+R_P4@VGlBBaLLL=T@4CJ1=x*Gp z4K}WQ*9q20VCtw4l_ou$ogKHwJ{QZ)%231?+EG?B^7pAtmWLhbp}Sx7oi6*He>vB4 z1y(AYqHH2#v&&Hg>a*W;MsDqRQs3Jkt)SAT=LS1pzvBekqPf%54isLNXMJ7~&<;(0x< zmmXj?uU7}q9w1-Ps(Jk}^Z|^`uXOS7|G$2Kxr^z7TF?d<86drj(I*&X6zf;XAQdyH z^D_hUsW73@9z%w-v*eRQkww*Eb5_SWhI!l~Ql$4JH0@tZ87LW;eTtO$2Pcn{{Rzqt z*C3V|OQGkV=Fb?rUQ_IhqOy!uO{HbTmS$&CN^I$NCiizLHVtX!3euk0MKP{ms-`U3 zS@Qoj;Xk8(e}JlscIFVOC8)M&=MJHIg6hMlk)Xy<#yo?_F$sS+Rd;q<}SEKyJS jjN9V_*t;;)hftLtVJ1ZOM@R Date: Fri, 16 Mar 2018 13:24:44 +0000 Subject: [PATCH 5/7] Fix add_axioms_for_concat_substr What was happening for start and end index out of bound wasn't clear and could lead to empty index set because the strings where sometimes indexed at negative indices. The behavior is now similar to substring: the actual start index is `start_index' = max(0, start_index)` (where start_index is the argument value) and the actual end index is `max(min(end_index, s2.length), start_index')`. --- .../string_constraint_generator_concat.cpp | 69 +++++++++---------- 1 file changed, 34 insertions(+), 35 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index fa38ac46bc1..6c258566351 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -14,22 +14,16 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include /// Add axioms enforcing that `res` is the concatenation of `s1` with -/// the substring of `s2` starting at index `start_index` and ending -/// at index `end_index`. -/// -/// If `start_index >= end_index`, the value returned is `s1`. -/// If `end_index > |s2|` and/or `start_index < 0`, the appended string will -/// be of length `end_index - start_index` and padded with non-deterministic -/// values. +/// the substring of `s2` starting at index `start_index'` and ending +/// at index `end_index'`. +/// Where start_index' is max(0, start_index) and end_index' is +/// max(min(end_index, s2.length), start_index') /// /// These axioms are: -/// 1. \f$end\_index > start\_index \Rightarrow |res| = |s_1| + end\_index - -/// start\_index -/// \f$ -/// 2. \f$end\_index \le start\_index \Rightarrow res = s_1 \f$ -/// 3. \f$\forall i<|s_1|. res[i]=s_1[i] \f$ -/// 4. \f$\forall i< end\_index - start\_index.\ res[i+|s_1|] -/// = s_2[start\_index+i]\f$ +/// 1. \f$|res| = |s_1| + end\_index' - start\_index' \f$ +/// 2. \f$\forall i<|s_1|. res[i]=s_1[i] \f$ +/// 3. \f$\forall i< end\_index' - start\_index'.\ res[i+|s_1|] +/// = s_2[start\_index'+i]\f$ /// /// \param res: an array of characters expression /// \param s1: an array of characters expression @@ -44,28 +38,33 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr( const exprt &start_index, const exprt &end_index) { - binary_relation_exprt prem(end_index, ID_gt, start_index); - - exprt res_length=plus_exprt_with_overflow_check( - s1.length(), minus_exprt(end_index, start_index)); - implies_exprt a1(prem, equal_exprt(res.length(), res_length)); - lemmas.push_back(a1); - - implies_exprt a2(not_exprt(prem), equal_exprt(res.length(), s1.length())); - lemmas.push_back(a2); + const typet &index_type = start_index.type(); + const exprt start1 = maximum(start_index, from_integer(0, index_type)); + const exprt end1 = maximum(minimum(end_index, s2.length()), start1); + + // Axiom 1. + lemmas.push_back([&] { // NOLINT + const plus_exprt res_length(s1.length(), minus_exprt(end1, start1)); + return equal_exprt(res.length(), res_length); + }()); + + // Axiom 2. + constraints.push_back([&] { // NOLINT + const symbol_exprt idx = + fresh_univ_index("QA_index_concat", res.length().type()); + return string_constraintt(idx, s1.length(), equal_exprt(s1[idx], res[idx])); + }()); + + // Axiom 3. + constraints.push_back([&] { // NOLINT + const symbol_exprt idx2 = + fresh_univ_index("QA_index_concat2", res.length().type()); + const equal_exprt res_eq( + res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start1, idx2)]); + return string_constraintt(idx2, minus_exprt(end1, start1), res_eq); + }()); - symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type()); - string_constraintt a3(idx, s1.length(), equal_exprt(s1[idx], res[idx])); - constraints.push_back(a3); - - symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type()); - equal_exprt res_eq( - res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start_index, idx2)]); - string_constraintt a4(idx2, minus_exprt(end_index, start_index), res_eq); - constraints.push_back(a4); - - // We should have a enum type for the possible error codes - return from_integer(0, res.length().type()); + return from_integer(0, get_return_code_type()); } /// Add axioms enforcing that `res` is the concatenation of `s1` with From 882bbb19561b7bd00af4004d04bd55965fd2d122 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 19 Mar 2018 11:03:25 +0000 Subject: [PATCH 6/7] Fix eval of concatenation builtin functions The previous version was not handling correcly the case where end_index was smaller than start_index. --- .../refinement/string_refinement_util.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 46cb5178389..c9071509452 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -292,17 +292,19 @@ std::vector string_concatenation_builtin_functiont::eval( const std::vector &input2_value, const std::vector &args_value) const { - const std::size_t start_index = - args_value.size() > 0 && args_value[0] > 0 ? args_value[0].to_ulong() : 0; - const std::size_t end_index = args_value.size() > 1 && args_value[1] > 0 - ? args_value[1].to_ulong() - : input2_value.size(); + const auto start_index = + args_value.size() > 0 && args_value[0] > 0 ? args_value[0] : mp_integer(0); + const mp_integer input2_size(input2_value.size()); + const auto end_index = + args_value.size() > 1 + ? std::max(std::min(args_value[1], input2_size), start_index) + : input2_size; std::vector result(input1_value); result.insert( result.end(), - input2_value.begin() + start_index, - input2_value.begin() + end_index); + input2_value.begin() + numeric_cast_v(start_index), + input2_value.begin() + numeric_cast_v(end_index)); return result; } From 84186ffca4c36a0609c65fa1b57983a3fc49253a Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 19 Mar 2018 11:04:33 +0000 Subject: [PATCH 7/7] Tests for CProverString.append with start/end args This test the CProverString.append function when start_index and end_index arguments are proivided. --- .../StringConcat_StringII/Test.class | Bin 0 -> 1336 bytes .../StringConcat_StringII/Test.java | 40 ++++++++++++++++++ .../StringConcat_StringII/test.desc | 8 ++++ .../StringConcat_StringII/test_fail.desc | 8 ++++ 4 files changed, 56 insertions(+) create mode 100644 regression/jbmc-strings/StringConcat_StringII/Test.class create mode 100644 regression/jbmc-strings/StringConcat_StringII/Test.java create mode 100644 regression/jbmc-strings/StringConcat_StringII/test.desc create mode 100644 regression/jbmc-strings/StringConcat_StringII/test_fail.desc diff --git a/regression/jbmc-strings/StringConcat_StringII/Test.class b/regression/jbmc-strings/StringConcat_StringII/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..c1783156f96185e00d29561379e59d619df4f66d GIT binary patch literal 1336 zcmZuw+int36kP`fW|&SbrJ_ZP+Ey)C6z`W(tChCe#9Knu=-V(H>nJjH82keN!PxlZ zi_dC8jVAi0iO>FkKjDKh>N*sP6`63(I(zond#|GH0gcXG}ZQb}eSf zYxs^_a8>5m5Cb0eA)E63VwIY4>`m~NS7N$_JFpaa!WMKy9ES$%zGGDMT zgsm2em=hT8#+mJ?Gw=JJPciO#9@nx>Y!a7=S_e%PqhsE}0xk-~yCJTX?@K4xWLg(S zAo(A)lrkyLU(P!#zV}%A`Qr7~-nkRCS5{<=O}g59xy|=)#f$fBza$?uWX+KU>fY0g z&K;$^*GaN9)9YB^OjKoUIk?xFiA5eA2A?IhZM~%w7PCcxkxa2SP&Z?gh1pe(%_bq% z1uJAZgacg}i&ai4Q&nW$^<`zFF&v_x!519UJJ`dqPw+bt@nO|ZB8`6z2RI!>Y3_o1 z7)I2fql()u>~1rBN`_&2-%tb+{bY6}m)H_kylyF=uY>+jxDDdpL+y9*@9~s^ zEf(8JGLje|iD&;KF~;(N5tvLo#14&+!aj_Vz&Jm={aC_8t7rq_Cze<&{r7Bi>^O^6 jzrjSjiNRIq+DmBRH;8pr>U2*rk04~7S3Mr(A%w9%!si^0 literal 0 HcmV?d00001 diff --git a/regression/jbmc-strings/StringConcat_StringII/Test.java b/regression/jbmc-strings/StringConcat_StringII/Test.java new file mode 100644 index 00000000000..50faba13c80 --- /dev/null +++ b/regression/jbmc-strings/StringConcat_StringII/Test.java @@ -0,0 +1,40 @@ +// This test uses CProverString so should be compiled with +// javac Test.java ../cprover/CProverString.java +import org.cprover.CProverString; + +class Test { + public void testSuccess(String s, String t, int start, int end) { + // Filter + if (s == null || t == null) + return; + + // Act + StringBuilder sb = new StringBuilder(s); + String result = CProverString.append(sb, t, start, end).toString(); + + // Arrange + StringBuilder reference = new StringBuilder(s); + if(start < 0) + start = 0; + for (int i = start; i < end && i < t.length(); i++) + reference.append(org.cprover.CProverString.charAt(t, i)); + + // Assert + assert result.equals(reference.toString()); + } + + public void testFail(int i) { + // Arrange + StringBuilder sb = new StringBuilder("foo"); + + // Act + CProverString.append(sb, "bar", 0, 1); + CProverString.append(sb, "bar", 0, 4); + CProverString.append(sb, "foo", -1, 0); + CProverString.append(sb, "foo", -10, -1); + CProverString.append(sb, "bar", -10, 25); + + // Assert + assert !sb.toString().equals("foobbarbar"); + } +} diff --git a/regression/jbmc-strings/StringConcat_StringII/test.desc b/regression/jbmc-strings/StringConcat_StringII/test.desc new file mode 100644 index 00000000000..4876a04b8e4 --- /dev/null +++ b/regression/jbmc-strings/StringConcat_StringII/test.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--refine-strings --string-max-length 100 --string-max-input-length 4 --verbosity 10 --unwind 5 Test.class --function Test.testSuccess +^EXIT=0$ +^SIGNAL=0$ +assertion at file Test.java line 23 .*: SUCCESS +-- +^warning: ignoring diff --git a/regression/jbmc-strings/StringConcat_StringII/test_fail.desc b/regression/jbmc-strings/StringConcat_StringII/test_fail.desc new file mode 100644 index 00000000000..f8751dbb3a3 --- /dev/null +++ b/regression/jbmc-strings/StringConcat_StringII/test_fail.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--refine-strings --string-max-length 10000 --verbosity 10 Test.class --function Test.testFail +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 38 .*: FAILURE +-- +^warning: ignoring