From 5481f2e801f45c4324f71b56440c281bb0430216 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 6 Feb 2020 11:45:28 +0000 Subject: [PATCH 1/2] String solver: avoid cubic formulas for string-to-int conversions Previously when the string radix was unknown we generated a conjunction of no-overflow checks which was (in total) cubic in the number of digits in the string being converted to an integer. For instance, it would define a series of 'sum's, like: sum0 = digit0 sum1 = digit0 * radix + digit1 sum2 = (digit0 * radix + digit1) * radix + digit2 Where the definitions are truly inlined like this and don't use symbols to represent sum0...n, so |sumn| is O(n), and the sum of all sums is O(n^2) Then for each digit it would emit an overflow check: constraint2 = size = 2 => nooverflow(sum1) constraint3 = size = 3 => nooverflow(sum1) && nooverflow(sum2) constraint4 = size = 4 => nooverflow(sum1) && nooverflow(sum2) && nooverflow(sum3) However those sums are again expanded inline, meaning the sum of all constraints is O(n^3) The obvious fix is to define symbols for sum0... sumn and then constraint0... constraintn, but this slows the solver down considerably for small formulas (e.g. Byte.parseByte, with max size 3 digits), so I compromise here by replacing the constraints with: constraint2 = size >= 2 => nooverflow(sum1) constraint3 = size >= 3 => nooverflow(sum2) constraint4 = size >= 4 => nooverflow(sum3) Thus the formula size is quadratic not cubic but still fast for cases where the radix is known. --- .../string_constraint_generator_valueof.cpp | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp index c6797b219e2..c25c7f9d274 100644 --- a/src/solvers/strings/string_constraint_generator_valueof.cpp +++ b/src/solvers/strings/string_constraint_generator_valueof.cpp @@ -385,7 +385,6 @@ string_constraint_generatort::add_axioms_for_characters_in_integer_string( const equal_exprt starts_with_minus(str[0], from_integer('-', char_type)); const constant_exprt zero_expr = from_integer(0, type); - exprt::operandst digit_constraints; exprt sum = get_numeric_value_from_character( str[0], char_type, type, strict_formatting, radix_ul); @@ -407,8 +406,7 @@ string_constraint_generatort::add_axioms_for_characters_in_integer_string( // (the first part avoid overflows in the multiplication and the second // one in the addition of the definition of sum_j) // For all 1<=size<=max_string_length we add axioms: - // a5 : |res| == size => - // forall max_string_length-2 <= j < size. no_overflow_j + // a5 : |res| >= size => no_overflow_j (only added when overflow possible) // a6 : |res| == size && res[0] is a digit for radix => // input_int == sum_{size-1} // a7 : |res| == size && res[0] == '-' => input_int == -sum_{size-1} @@ -424,31 +422,33 @@ string_constraint_generatort::add_axioms_for_characters_in_integer_string( // a digit, which is `max_string_length - 2` because of the space left for // a minus sign. That assumes that we were able to identify the radix. If we // weren't then we check for overflow on every index. + optionalt no_overflow; if(size - 1 >= max_string_length - 2 || radix_ul == 0) { - const and_exprt no_overflow( - equal_exprt(sum, div_exprt(radix_sum, radix)), - binary_relation_exprt(new_sum, ID_ge, radix_sum)); - digit_constraints.push_back(no_overflow); + no_overflow = and_exprt{equal_exprt(sum, div_exprt(radix_sum, radix)), + binary_relation_exprt(new_sum, ID_ge, radix_sum)}; } sum = new_sum; - const equal_exprt premise = - equal_to(array_pool.get_or_create_length(str), size); + exprt length_expr = array_pool.get_or_create_length(str); - if(!digit_constraints.empty()) + if(no_overflow.has_value()) { - const implies_exprt a5(premise, conjunction(digit_constraints)); + const binary_predicate_exprt string_length_ge_size{ + length_expr, ID_ge, from_integer(size, length_expr.type())}; + const implies_exprt a5(string_length_ge_size, *no_overflow); constraints.existential.push_back(a5); } + const equal_exprt string_length_equals_size = equal_to(length_expr, size); + const implies_exprt a6( - and_exprt(premise, not_exprt(starts_with_minus)), + and_exprt(string_length_equals_size, not_exprt(starts_with_minus)), equal_exprt(input_int, sum)); constraints.existential.push_back(a6); const implies_exprt a7( - and_exprt(premise, starts_with_minus), + and_exprt(string_length_equals_size, starts_with_minus), equal_exprt(input_int, unary_minus_exprt(sum))); constraints.existential.push_back(a7); } From b8e774c91f4addf1427a65437aa7cd66319d9272 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 6 Feb 2020 16:52:10 +0000 Subject: [PATCH 2/2] Ensure string is non-null, radix is in range before parsing integers Previously we passed the input to parseInt/parseLong straight to the built-in string solver functions, meaning it was possible to crash jbmc by passing an out-of-range constant radix or for the solver to produce crazy results when it regarded the radix as a free choice. Now the models apply the constraint that it falls in a sensible range. I add a test for parseint with a free radix, but am unable to add one for parselong yet as it takes too long to solve. --- jbmc/lib/java-models-library | 2 +- .../java_parseint/test1.desc | 2 +- .../java_parseint/test2.desc | 2 +- .../java_parseint/test3.desc | 2 +- .../java_parseint_knownbug/test.desc | 2 +- .../java_parseint_unknown_radix/Test.class | Bin 0 -> 887 bytes .../java_parseint_unknown_radix/Test.java | 18 ++++++++++++++++++ .../java_parseint_unknown_radix/test.desc | 9 +++++++++ .../java_parseint_with_radix/test1.desc | 2 +- .../java_parseint_with_radix/test2.desc | 2 +- .../java_parseint_with_radix/test3.desc | 2 +- .../java_parseint_with_radix/test4.desc | 2 +- .../java_parseint_with_radix/test5.desc | 2 +- .../java_parseint_with_radix/test6.desc | 2 +- .../java_parselong/test_binary_min.desc | 2 +- .../java_parselong/test_decimal_max.desc | 2 +- .../java_parselong/test_decimal_min.desc | 2 +- .../java_parselong/test_hex.desc | 2 +- .../java_parselong/test_octal.desc | 2 +- .../java_parselong_unknown_radix/Test.class | Bin 0 -> 900 bytes .../java_parselong_unknown_radix/Test.java | 18 ++++++++++++++++++ .../java_parselong_unknown_radix/test.desc | 9 +++++++++ .../java_string_library_preprocess.cpp | 18 ++++++------------ 23 files changed, 76 insertions(+), 28 deletions(-) create mode 100644 jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.class create mode 100644 jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.java create mode 100644 jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/test.desc create mode 100644 jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/Test.class create mode 100644 jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/Test.java create mode 100644 jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/test.desc diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index 31df88c0bba..ee97592c10b 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit 31df88c0bba7fa5f9c4eeb53a79f8902246f386a +Subproject commit ee97592c10bb6d8c8c65472e547e9d1e41fa9b8d diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test1.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test1.desc index 1cb966074c6..4779e107ffd 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint/test1.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint/test1.desc @@ -1,6 +1,6 @@ CORE Test1 ---max-nondet-string-length 1000 --function Test1.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test1.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test2.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test2.desc index 38261f6441e..a98505a2026 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint/test2.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint/test2.desc @@ -1,6 +1,6 @@ CORE Test2 ---max-nondet-string-length 1000 --function Test2.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test2.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc index 089dff1e273..2ec5fcbf2ea 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc @@ -1,6 +1,6 @@ CORE Test3 ---max-nondet-string-length 1000 --function Test3.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test3.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 7.* FAILURE$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_knownbug/test.desc b/jbmc/regression/strings-smoke-tests/java_parseint_knownbug/test.desc index 73c00e60e6a..8b94e1d2486 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_knownbug/test.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_knownbug/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Test ---max-nondet-string-length 1000 --function Test.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 10.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.class b/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..8ab584c606b186c0077b3ebe1c7d1951ff04fbb8 GIT binary patch literal 887 zcmZ`%&rcIU7=6>-cH3p4Eg({hKnrSHmHGp{07inEG!{KTNaQwcCuL#XlHD!wZ{dWA ziDxtcqlw-;_%|8jn--|Xc$x3#yzjkl=EtwkUjZ!Qp$!`|HfB-KN72R{=2J-GnuY5& z5}2`Y!$t{Z3l)K}c^QT(h}@1JK5;|Y@Kj4cYzrioUEhr!2^gjFmVmj|X(@qp-SyRr z?(2pMHg&VWXuZ>v-j)np9iJu5XvYnSQQuTyv_vPOU1#@1slF=@WYv>?ySfntuHRm& zY5chB?{^~&_fMV0K(^dBQg{9^6~= z_w-0R6LneO+ij!3*SGmOL}pU!q-TKp!wAnbqbjYSjaN<~j_JgZ;hE?q zNt3?QZ@?(V7^N_dOU&rY$Luy}>y_^)R89~xkC3YvConR5M@Z*0({GXD`3~lBCI1QL z%2a0j2-y#aA0qb!iC3qvzV)J^^GI_rdK{)<(YH{fggJ^RQ$Uq$R!IIiJ2bc1{(MZ} zG9xmzmtCIi# literal 0 HcmV?d00001 diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.java b/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.java new file mode 100644 index 00000000000..ece00ea510f --- /dev/null +++ b/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.java @@ -0,0 +1,18 @@ +public class Test { + + public static void testMe(String input, int radix) { + + // Railroad the solver a bit to speed up solving + // (note use of > and < to dodge constant propagation) + if(input == null || input.length() != 1 || input.charAt(0) != 'k' || radix < 30 || radix > 30) + return; + + int value = Integer.parseInt(input, radix); + if(value == 20) + assert false; + else + assert false; + + } + +} diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/test.desc b/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/test.desc new file mode 100644 index 00000000000..84c7ab2182f --- /dev/null +++ b/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/test.desc @@ -0,0 +1,9 @@ +CORE +Test +--max-nondet-string-length 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test.testMe --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 12.* FAILURE$ +^\[.*assertion.2\].* line 14.* SUCCESS$ +-- +non equal types diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc index 1cb966074c6..4779e107ffd 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc @@ -1,6 +1,6 @@ CORE Test1 ---max-nondet-string-length 1000 --function Test1.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test1.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc index cd1d038f76c..160deb14def 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc @@ -1,6 +1,6 @@ CORE Test2 ---max-nondet-string-length 1000 --function Test2.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test2.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc index de14d77c44d..df497badb22 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc @@ -1,6 +1,6 @@ CORE Test3 ---max-nondet-string-length 1000 --function Test3.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test3.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc index 539651ed9e7..59570e81f11 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc @@ -1,6 +1,6 @@ CORE Test4 ---max-nondet-string-length 1000 --function Test4.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test4.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc index 0c81faf44d4..3dda5185d6d 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc @@ -1,6 +1,6 @@ CORE Test5 ---max-nondet-string-length 1000 --function Test5.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test5.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc index 07f65d534f3..cf35f361031 100644 --- a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc +++ b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc @@ -1,6 +1,6 @@ CORE Test6 ---max-nondet-string-length 1000 --function Test6.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test6.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_binary_min.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_binary_min.desc index d20c1215eb9..e887d1612ff 100644 --- a/jbmc/regression/strings-smoke-tests/java_parselong/test_binary_min.desc +++ b/jbmc/regression/strings-smoke-tests/java_parselong/test_binary_min.desc @@ -1,6 +1,6 @@ CORE Test_binary_min ---max-nondet-string-length 1000 --function Test_binary_min.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_binary_min.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc index 1b89ef8987e..03d6c5b3feb 100644 --- a/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc +++ b/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc @@ -1,6 +1,6 @@ CORE Test_decimal_max ---max-nondet-string-length 1000 --function Test_decimal_max.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_decimal_max.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc index b8dcfbd6229..28a8a979bed 100644 --- a/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc +++ b/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc @@ -1,6 +1,6 @@ CORE Test_decimal_min ---max-nondet-string-length 1000 --function Test_decimal_min.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_decimal_min.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_hex.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_hex.desc index 4ee4647236c..539c655161d 100644 --- a/jbmc/regression/strings-smoke-tests/java_parselong/test_hex.desc +++ b/jbmc/regression/strings-smoke-tests/java_parselong/test_hex.desc @@ -1,6 +1,6 @@ CORE Test_hex ---max-nondet-string-length 1000 --function Test_hex.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_hex.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_octal.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_octal.desc index 46724c6ac99..e3f38b1298e 100644 --- a/jbmc/regression/strings-smoke-tests/java_parselong/test_octal.desc +++ b/jbmc/regression/strings-smoke-tests/java_parselong/test_octal.desc @@ -1,6 +1,6 @@ CORE Test_octal ---max-nondet-string-length 1000 --function Test_octal.main +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_octal.main ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/Test.class b/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..04ed12dc6420ce1f7b0cd3f2bcc57ccec31ce7eb GIT binary patch literal 900 zcmZuvT~8B16g|^!yL4G-i-@gNgaX=DrGDU7AZk-JscG?{ghbwkc2gGCZL_;2{t%yd z!oG{ee=QJWQ=D@p(MDQ%-nnD&Y5%0%MFngkj)aay6GhxHaToV=+&5|90~2Ey7f20{FP%8^((~FLEl?;r z9-4TB#{!9A=bO!Kt3mQ-O2^u$+_BtNu+_Jb?4yk>>6O^3R&8eZ(_~ z>5qtU`~>ZwkogL&G&70Fhdm^}K;J|9J4W6fA@;MMjh and < to dodge constant propagation) + if(input == null || input.length() != 1 || input.charAt(0) != 'k' || radix < 30 || radix > 30) + return; + + long value = Long.parseLong(input, radix); + if(value == 20) + assert false; + else + assert false; + + } + +} diff --git a/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/test.desc b/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/test.desc new file mode 100644 index 00000000000..ff5e8d11e1f --- /dev/null +++ b/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/test.desc @@ -0,0 +1,9 @@ +THOROUGH +Test +--max-nondet-string-length 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test.testMe --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 12.* FAILURE$ +^\[.*assertion.2\].* line 14.* SUCCESS$ +-- +non equal types diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 3b03aa7dc39..4748549e0c5 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1574,6 +1574,12 @@ void java_string_library_preprocesst::initialize_conversion_table() std::placeholders::_2, std::placeholders::_3, std::placeholders::_4); + cprover_equivalent_to_java_function + ["java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] = + ID_cprover_string_parse_int_func; + cprover_equivalent_to_java_function + ["java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] = + ID_cprover_string_parse_int_func; // String library conversion_table["java::java.lang.String.:(Ljava/lang/String;)V"] = @@ -1819,18 +1825,6 @@ void java_string_library_preprocesst::initialize_conversion_table() conversion_table["java::java.lang.String.length:()I"]; // Other libraries - cprover_equivalent_to_java_function - ["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]= - ID_cprover_string_parse_int_func; - cprover_equivalent_to_java_function - ["java::java.lang.Integer.parseInt:(Ljava/lang/String;I)I"]= - ID_cprover_string_parse_int_func; - cprover_equivalent_to_java_function - ["java::java.lang.Long.parseLong:(Ljava/lang/String;)J"]= - ID_cprover_string_parse_int_func; - cprover_equivalent_to_java_function - ["java::java.lang.Long.parseLong:(Ljava/lang/String;I)J"]= - ID_cprover_string_parse_int_func; cprover_equivalent_to_java_string_returning_function ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]= ID_cprover_string_of_int_hex_func;