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 38fa5289bd2..e8d4260b1e0 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test.desc @@ -1,7 +1,10 @@ CORE test_int.class --refine-strings -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +assertion.* file test_int.java line 6 .* SUCCESS$ +assertion.* file test_int.java line 9 .* SUCCESS$ +assertion.* file test_int.java line 11 .* FAILURE$ +assertion.* file test_int.java line 13 .* FAILURE$ -- diff --git a/regression/strings-smoke-tests/java_int_to_string/test_int.class b/regression/strings-smoke-tests/java_int_to_string/test_int.class index eff0e5a422e..ca4e3be5dc4 100644 Binary files a/regression/strings-smoke-tests/java_int_to_string/test_int.class and b/regression/strings-smoke-tests/java_int_to_string/test_int.class differ diff --git a/regression/strings-smoke-tests/java_int_to_string/test_int.java b/regression/strings-smoke-tests/java_int_to_string/test_int.java index f46411ed166..9ddbc332b6f 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test_int.java +++ b/regression/strings-smoke-tests/java_int_to_string/test_int.java @@ -1,11 +1,15 @@ public class test_int { - public static void main(/*String[] argv*/) + public static void main(int i) { String s = Integer.toString(12); assert(s.equals("12")); String t = Integer.toString(-23); System.out.println(t); assert(t.equals("-23")); + if(i==1) + assert(!s.equals("12")); + else if(i==2) + assert(!t.equals("-23")); } } diff --git a/regression/strings-smoke-tests/java_value_of_long/test.class b/regression/strings-smoke-tests/java_value_of_long/test.class new file mode 100644 index 00000000000..b559af818fb Binary files /dev/null and b/regression/strings-smoke-tests/java_value_of_long/test.class differ diff --git a/regression/strings-smoke-tests/java_value_of_long/test.desc b/regression/strings-smoke-tests/java_value_of_long/test.desc new file mode 100644 index 00000000000..f96a114f708 --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_long/test.desc @@ -0,0 +1,8 @@ +CORE +test.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +assertion.* file test.java line 9 .* SUCCESS$ +assertion.* file test.java line 14 .* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_value_of_long/test.java b/regression/strings-smoke-tests/java_value_of_long/test.java new file mode 100644 index 00000000000..a9ceaa964a7 --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_long/test.java @@ -0,0 +1,17 @@ +public class test +{ + public static void main(int i) + { + long l1=12345678901234L; + if(i == 0) + { + String s = String.valueOf(l1); + assert(s.equals("12345678901234")); + } + else + { + String s = String.valueOf(-l1); + assert(!s.equals("-12345678901234")); + } + } +} diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 9ad1845c9d0..7416bc1a341 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -209,16 +209,17 @@ string_exprt string_constraint_generatort::add_axioms_from_bool( /// add axioms to say the string corresponds to the result of String.valueOf(I) /// or String.valueOf(J) java functions applied on the integer expression -/// \par parameters: a signed integer expression, and a maximal size for the -/// string -/// representation +/// \param i: a signed integer expression +/// \param max_size: a maximal size for the string representation +/// \param ref_type: type for refined strings /// \return a string expression string_exprt string_constraint_generatort::add_axioms_from_int( const exprt &i, size_t max_size, const refined_string_typet &ref_type) { + PRECONDITION(i.type().id()==ID_signedbv); + PRECONDITION(max_size::max()); string_exprt res=fresh_string(ref_type); const typet &type=i.type(); - assert(type.id()==ID_signedbv); exprt ten=from_integer(10, type); const typet &char_type=ref_type.get_char_type(); const typet &index_type=ref_type.get_index_type(); @@ -262,12 +263,20 @@ string_exprt string_constraint_generatort::add_axioms_from_int( not_exprt(equal_exprt(res[1], zero_char))); axioms.push_back(a4); - assert(max_size::max()); - for(size_t size=1; size<=max_size; size++) { - // For each possible size, we add axioms: - // a5 : forall 1 <= j < size. '0' <= res[j] <= '9' && sum == 10 * (sum/10) + // For each possible size, we have: + // sum_0 = starts_with_digit ? res[0]-'0' : 0 + // sum_j = 10 * sum_{j-1} + res[i] - '0' + // and add axioms: + // a5 : |res| == size => + // forall 1 <= j < size. + // is_number && (j >= max_size-2 => no_overflow) + // where is_number := '0' <= res[j] <= '9' + // and no_overflow := sum_{j-1} = (10 * sum_{j-1} / 10) + // && sum_j >= sum_{j - 1} + // (the first part avoid overflows in multiplication and + // the second one in additions) // a6 : |res| == size && '0' <= res[0] <= '9' => i == sum // a7 : |res| == size && res[0] == '-' => i == -sum @@ -288,7 +297,11 @@ string_exprt string_constraint_generatort::add_axioms_from_int( binary_relation_exprt(res[j], ID_le, nine_char)); digit_constraints.push_back(is_number); - if(j>=max_size-1) + // An overflow can happen when reaching the last index of a string of + // maximal size which is `max_size` for negative numbers and + // `max_size - 1` for positive numbers because of the abscence of a `-` + // sign. + if(j>=max_size-2) { // check for overflows if the size is big and_exprt no_overflow( @@ -299,10 +312,10 @@ string_exprt string_constraint_generatort::add_axioms_from_int( sum=new_sum; } - exprt a5=conjunction(digit_constraints); + equal_exprt premise=res.axiom_for_has_length(size); + implies_exprt a5(premise, conjunction(digit_constraints)); axioms.push_back(a5); - equal_exprt premise=res.axiom_for_has_length(size); implies_exprt a6( and_exprt(premise, starts_with_digit), equal_exprt(i, sum)); axioms.push_back(a6);