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 2c78d4648103085d59348db07d3a1d5c7bcd55e7 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Apr 2017 13:34:42 +0100 Subject: [PATCH 2/2] Correcting constraints for conversion from int diffblue/test-gen#241 The first two constraints that were previously added in add_axioms_from_int were not enough to ensure correctness. They are replaced here by: * a1 : i < 0 => 1 <|res|<=max_size && res[0]='-' * a2 : i >= 0 => 0 <|res|<=max_size-1 && '0'<=res[0]<='9' Clarifications in add_axioms_from_int diffblue/test-gen#241 We make the code clearer and add overflow checks. Corrections after Peter's review. --- .../string_constraint_generator_valueof.cpp | 155 +++++++----------- 1 file changed, 63 insertions(+), 92 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index edff2d726e7..d967e5bb820 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -267,23 +267,6 @@ string_exprt string_constraint_generatort::add_axioms_from_bool( /*******************************************************************\ -Function: smallest_by_digit - - Inputs: number of digit - - Outputs: an integer with the right number of digit - - Purpose: gives the smallest integer with the specified number of digits - -\*******************************************************************/ - -static mp_integer smallest_by_digit(int nb) -{ - return power(10, nb-1); -} - -/*******************************************************************\ - Function: string_constraint_generatort::add_axioms_from_int Inputs: a signed integer expression, and a maximal size for the string @@ -313,102 +296,90 @@ string_exprt string_constraint_generatort::add_axioms_from_int( exprt max=from_integer(max_size, index_type); // We add axioms: - // a1 : 0 <|res|<=max_size - // a2 : (res[0]='-')||('0'<=res[0]<='9') - - and_exprt a1(res.axiom_for_is_strictly_longer_than(zero), - res.axiom_for_is_shorter_than(max)); + // a1 : i < 0 => 1 <|res|<=max_size && res[0]='-' + // a2 : i >= 0 => 0 <|res|<=max_size-1 && '0'<=res[0]<='9' + // a3 : |res|>1 && '0'<=res[0]<='9' => res[0]!='0' + // a4 : |res|>1 && res[0]='-' => res[1]!='0' + + binary_relation_exprt is_negative(i, ID_lt, zero); + and_exprt correct_length1( + res.axiom_for_is_strictly_longer_than(1), + res.axiom_for_is_shorter_than(max)); + equal_exprt starts_with_minus(res[0], minus_char); + implies_exprt a1(is_negative, and_exprt(correct_length1, starts_with_minus)); axioms.push_back(a1); - exprt chr=res[0]; - equal_exprt starts_with_minus(chr, minus_char); + not_exprt is_positive(is_negative); and_exprt starts_with_digit( - binary_relation_exprt(chr, ID_ge, zero_char), - binary_relation_exprt(chr, ID_le, nine_char)); - or_exprt a2(starts_with_digit, starts_with_minus); + binary_relation_exprt(res[0], ID_ge, zero_char), + binary_relation_exprt(res[0], ID_le, nine_char)); + and_exprt correct_length2( + res.axiom_for_is_strictly_longer_than(0), + res.axiom_for_is_strictly_shorter_than(max)); + implies_exprt a2(is_positive, and_exprt(correct_length2, starts_with_digit)); axioms.push_back(a2); - // These are constraints to detect number that requiere the maximum number - // of digits - exprt smallest_with_max_digits= - from_integer(smallest_by_digit(max_size-1), type); - binary_relation_exprt big_negative( - i, ID_le, unary_minus_exprt(smallest_with_max_digits)); - binary_relation_exprt big_positive(i, ID_ge, smallest_with_max_digits); - or_exprt requieres_max_digits(big_negative, big_positive); + implies_exprt a3( + and_exprt(res.axiom_for_is_strictly_longer_than(1), starts_with_digit), + not_exprt(equal_exprt(res[0], zero_char))); + axioms.push_back(a3); + + implies_exprt a4( + and_exprt(res.axiom_for_is_strictly_longer_than(1), starts_with_minus), + 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: - // all_numbers: forall 1<=i<=size. '0'<=res[i]<='9' - // a3 : |res|=size&&'0'<=res[0]<='9' => - // i=sum+str[0]-'0' &&all_numbers - // a4 : |res|=size&&res[0]='-' => i=-sum - // a5 : size>1 => |res|=size&&'0'<=res[0]<='9' => res[0]!='0' - // a6 : size>1 => |res|=size&&res[0]'-' => res[1]!='0' - // a7 : size==max_size => i>1000000000 - exprt sum=from_integer(0, type); - exprt all_numbers=true_exprt(); - chr=res[0]; - exprt first_value=typecast_exprt(minus_exprt(chr, zero_char), type); + // a5 : forall 1 <= j < size. '0' <= res[j] <= '9' && sum == 10 * (sum/10) + // a6 : |res| == size && '0' <= res[0] <= '9' => i == sum + // a7 : |res| == size && res[0] == '-' => i == -sum + + exprt::operandst digit_constraints; + exprt sum=if_exprt( + starts_with_digit, + typecast_exprt(minus_exprt(res[0], zero_char), type), + from_integer(0, type)); for(size_t j=1; j=max_size-1) + { + // check for overflows if the size is big + and_exprt no_overflow( + equal_exprt(sum, div_exprt(ten_sum, ten)), + binary_relation_exprt(new_sum, ID_ge, ten_sum)); + digit_constraints.push_back(no_overflow); + } + sum=new_sum; } - axioms.push_back(all_numbers); + exprt a5=conjunction(digit_constraints); + axioms.push_back(a5); equal_exprt premise=res.axiom_for_has_length(size); - equal_exprt constr3(i, plus_exprt(sum, first_value)); - implies_exprt a3(and_exprt(premise, starts_with_digit), constr3); - axioms.push_back(a3); + implies_exprt a6( + and_exprt(premise, starts_with_digit), equal_exprt(i, sum)); + axioms.push_back(a6); - implies_exprt a4( + implies_exprt a7( and_exprt(premise, starts_with_minus), equal_exprt(i, unary_minus_exprt(sum))); - axioms.push_back(a4); - - // disallow 0s at the beginning - if(size>1) - { - equal_exprt r0_zero(res[zero], zero_char); - implies_exprt a5( - and_exprt(premise, starts_with_digit), - not_exprt(r0_zero)); - axioms.push_back(a5); - - exprt one=from_integer(1, index_type); - equal_exprt r1_zero(res[one], zero_char); - implies_exprt a6( - and_exprt(premise, starts_with_minus), - not_exprt(r1_zero)); - axioms.push_back(a6); - } - - // when the size is close to the maximum, either the number is very big - // or it is negative - if(size==max_size-1) - { - implies_exprt a7(premise, or_exprt(requieres_max_digits, - starts_with_minus)); - axioms.push_back(a7); - } - // when we reach the maximal size the number is very big in the negative - if(size==max_size) - { - implies_exprt a7(premise, and_exprt(starts_with_minus, big_negative)); - axioms.push_back(a7); - } + axioms.push_back(a7); } + return res; }