diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index ccf0abbed92..b5459581cb8 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit ccf0abbed92bf9d5c7ef9ad8efbc45a81e147393 +Subproject commit b5459581cb894990c47712af7f1216d5f4cf9cd2 diff --git a/jbmc/regression/jbmc-strings/StringValueOf01/test.desc b/jbmc/regression/jbmc-strings/StringValueOf01/test.desc index 89f2a08336e..a718ff88fd0 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf01/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf01/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf01.class ---max-nondet-string-length 1000 +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf02/test.desc b/jbmc/regression/jbmc-strings/StringValueOf02/test.desc index 354c20c239b..ddb75c24ff3 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf02/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf02/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf02.class ---max-nondet-string-length 1000 +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf03/test.desc b/jbmc/regression/jbmc-strings/StringValueOf03/test.desc index d44990b4910..192c75aaf64 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf03/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf03/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf03.class ---max-nondet-string-length 1000 +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf04/test.desc b/jbmc/regression/jbmc-strings/StringValueOf04/test.desc index 6dd28b97a01..b6bd60e3ba5 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf04/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf04/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf04.class ---max-nondet-string-length 1000 +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf05/test.desc b/jbmc/regression/jbmc-strings/StringValueOf05/test.desc index aab18c3bad6..291658b084b 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf05/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf05/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf05.class ---max-nondet-string-length 1000 +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf06/test.desc b/jbmc/regression/jbmc-strings/StringValueOf06/test.desc index 0bd02bf0492..c7fa2da4292 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf06/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf06/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf06.class ---max-nondet-string-length 1000 +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf07/test.desc b/jbmc/regression/jbmc-strings/StringValueOf07/test.desc index 234ff205769..e2b62a67131 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf07/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf07/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf07.class ---max-nondet-string-length 1000 +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 8 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf08/test.desc b/jbmc/regression/jbmc-strings/StringValueOf08/test.desc index db32c5fef09..7c8330c495d 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf08/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf08/test.desc @@ -1,6 +1,6 @@ CORE StringValueOf08.class ---max-nondet-string-length 100 +--max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf09/test.desc b/jbmc/regression/jbmc-strings/StringValueOf09/test.desc index a7d67344a20..cbbf49fb2cd 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf09/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf09/test.desc @@ -1,6 +1,6 @@ -CORE +KNOWNBUG StringValueOf09.class ---max-nondet-string-length 1000 +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion\.1\] .* line 7 .* FAILURE$ diff --git a/jbmc/regression/jbmc-strings/StringValueOf10/test.desc b/jbmc/regression/jbmc-strings/StringValueOf10/test.desc index 783cd2935dc..02a55a92b89 100644 --- a/jbmc/regression/jbmc-strings/StringValueOf10/test.desc +++ b/jbmc/regression/jbmc-strings/StringValueOf10/test.desc @@ -1,6 +1,6 @@ FUTURE StringValueOf10.class ---max-nondet-string-length 1000 +--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc index 23646edbe11..20ba70d5c09 100644 --- a/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc +++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc @@ -1,6 +1,6 @@ CORE Test.class ---function Test.checkWithDependency --depth 10000 +--function Test.checkWithDependency --depth 10000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 63 .*: SUCCESS diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc index dfb4189ada5..f58580459fb 100644 --- a/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc +++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc @@ -1,6 +1,6 @@ CORE Test.class ---function Test.checkDet +--function Test.checkDet --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 26 .*: FAILURE diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc index a143d6cd3db..03ab7df7e31 100644 --- a/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc +++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc @@ -1,6 +1,6 @@ CORE Test.class ---function Test.checkNonDet +--function Test.checkNonDet --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 55 .*: FAILURE diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc index 1c3eaaa7630..7d05da8f41f 100644 --- a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc +++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc @@ -1,6 +1,6 @@ CORE Main.class ---function Main.main +--function Main.main --max-nondet-string-length 10000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 5d17f10699c..5b981a8d47e 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1669,26 +1669,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_string_returning_function ["java::java.lang.String.trim:()Ljava/lang/String;"]= ID_cprover_string_trim_func; - cprover_equivalent_to_java_string_returning_function - ["java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]= - ID_cprover_string_of_bool_func; - cprover_equivalent_to_java_string_returning_function - ["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]= - ID_cprover_string_of_char_func; - conversion_table["java::java.lang.String.valueOf:(F)Ljava/lang/String;"] = - std::bind( - &java_string_library_preprocesst::make_float_to_string_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3, - std::placeholders::_4); - cprover_equivalent_to_java_string_returning_function - ["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]= - ID_cprover_string_of_int_func; - cprover_equivalent_to_java_string_returning_function - ["java::java.lang.String.valueOf:(J)Ljava/lang/String;"]= - ID_cprover_string_of_long_func; // StringBuilder library conversion_table @@ -1827,14 +1807,6 @@ void java_string_library_preprocesst::initialize_conversion_table() conversion_table["java::java.lang.String.length:()I"]; // Other libraries - conversion_table["java::java.lang.Float.toString:(F)Ljava/lang/String;"] = - std::bind( - &java_string_library_preprocesst::make_float_to_string_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3, - std::placeholders::_4); cprover_equivalent_to_java_function ["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]= ID_cprover_string_parse_int_func; @@ -1850,18 +1822,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_string_returning_function ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]= ID_cprover_string_of_int_hex_func; - cprover_equivalent_to_java_string_returning_function - ["java::java.lang.Integer.toString:(I)Ljava/lang/String;"]= - ID_cprover_string_of_int_func; - cprover_equivalent_to_java_string_returning_function - ["java::java.lang.Integer.toString:(II)Ljava/lang/String;"]= - ID_cprover_string_of_int_func; - cprover_equivalent_to_java_string_returning_function - ["java::java.lang.Long.toString:(J)Ljava/lang/String;"]= - ID_cprover_string_of_int_func; - cprover_equivalent_to_java_string_returning_function - ["java::java.lang.Long.toString:(JI)Ljava/lang/String;"]= - ID_cprover_string_of_int_func; conversion_table["java::org.cprover.CProver.classIdentifier:(" "Ljava/lang/Object;)Ljava/lang/String;"] = std::bind( diff --git a/src/solvers/README.md b/src/solvers/README.md index a6e92a17944..a601feac8b4 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -499,9 +499,6 @@ This is described in more detail \link string_builtin_functiont here. \endlink * `cprover_string_of_float_scientific_notation` : \copybrief string_constraint_generatort::add_axioms_from_float_scientific_notation \link string_constraint_generatort::add_axioms_from_float_scientific_notation More... \endlink - * `cprover_string_of_char` : - \copybrief string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) - \link string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) More... \endlink * `cprover_string_parse_int` : \copybrief string_constraint_generatort::add_axioms_for_parse_int \link string_constraint_generatort::add_axioms_for_parse_int More... \endlink @@ -530,8 +527,6 @@ This is described in more detail \link string_builtin_functiont here. \endlink * `cprover_string_delete_char_at` : A call to `cprover_string_delete_char_at(s, i)` would be the same thing as `cprover_string_delete(s, i, i+1)`. - * `cprover_string_of_bool` : - Language dependent, should be implemented in the models. * `cprover_string_copy` : Same as `cprover_string_substring(s, 0)`. * `cprover_string_of_int_hex` : Same as `cprover_string_of_int(s, 16)`. * `cprover_string_of_double` : Same as `cprover_string_of_float`. diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index 4b9babd63aa..6fd862fdd36 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -273,10 +273,6 @@ string_constraint_generatort::add_axioms_for_function_application( return add_axioms_from_double(expr); else if(id == ID_cprover_string_of_long_func) return add_axioms_from_long(expr); - else if(id == ID_cprover_string_of_bool_func) - return add_axioms_from_bool(expr); - else if(id == ID_cprover_string_of_char_func) - return add_axioms_from_char(expr); else if(id == ID_cprover_string_set_length_func) return add_axioms_for_set_length(expr); else if(id == ID_cprover_string_delete_func) diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp index 8badede72c9..c6797b219e2 100644 --- a/src/solvers/strings/string_constraint_generator_valueof.cpp +++ b/src/solvers/strings/string_constraint_generator_valueof.cpp @@ -55,21 +55,6 @@ string_constraint_generatort::add_axioms_from_long( return add_axioms_for_string_of_int(res, f.arguments()[2], 0); } -/// Add axioms corresponding to the String.valueOf(Z) java function. -/// \deprecated This is Java specific and should be implemented in Java instead -/// \param f: function application with a Boolean argument -/// \return a new string expression -DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java")) -std::pair -string_constraint_generatort::add_axioms_from_bool( - const function_application_exprt &f) -{ - PRECONDITION(f.arguments().size() == 3); - const array_string_exprt res = - array_pool.find(f.arguments()[1], f.arguments()[0]); - return add_axioms_from_bool(res, f.arguments()[2]); -} - /// Add axioms stating that the returned string equals "true" when the Boolean /// expression is true and "false" when it is false. /// \deprecated This is Java specific and should be implemented in Java instead @@ -281,44 +266,6 @@ string_constraint_generatort::add_axioms_from_int_hex( return add_axioms_from_int_hex(res, f.arguments()[2]); } -/// Conversion from char to string -/// -// NOLINTNEXTLINE -/// \copybrief add_axioms_from_char(const array_string_exprt &res, const exprt &c) -// NOLINTNEXTLINE -/// \link add_axioms_from_char(const array_string_exprt &res, const exprt &c) -/// (More...) \endlink -/// \param f: function application with arguments integer `|res|`, character -/// pointer `&res[0]` and character `c` -/// \return code 0 on success -std::pair -string_constraint_generatort::add_axioms_from_char( - const function_application_exprt &f) -{ - PRECONDITION(f.arguments().size() == 3); - const array_string_exprt res = - array_pool.find(f.arguments()[1], f.arguments()[0]); - return add_axioms_from_char(res, f.arguments()[2]); -} - -/// Add axiom stating that string `res` has length 1 and the character -/// it contains equals `c`. -/// -/// This axiom is: \f$ |{\tt res}| = 1 \land {\tt res}[0] = {\tt c} \f$. -/// \param res: array of characters expression -/// \param c: character expression -/// \return code 0 on success -std::pair -string_constraint_generatort::add_axioms_from_char( - const array_string_exprt &res, - const exprt &c) -{ - string_constraintst constraints; - constraints.existential = {and_exprt( - equal_exprt(res[0], c), equal_to(array_pool.get_or_create_length(res), 1))}; - return {from_integer(0, get_return_code_type()), std::move(constraints)}; -} - /// Add axioms making the return value true if the given string is a correct /// number in the given radix /// \param str: string expression diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index e9e704863ad..8988b345747 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -619,11 +619,9 @@ IREP_ID_ONE(cprover_string_length_func) IREP_ID_ONE(cprover_string_of_int_func) IREP_ID_ONE(cprover_string_of_int_hex_func) IREP_ID_ONE(cprover_string_of_long_func) -IREP_ID_ONE(cprover_string_of_bool_func) IREP_ID_ONE(cprover_string_of_float_func) IREP_ID_ONE(cprover_string_of_float_scientific_notation_func) IREP_ID_ONE(cprover_string_of_double_func) -IREP_ID_ONE(cprover_string_of_char_func) IREP_ID_ONE(cprover_string_parse_int_func) IREP_ID_ONE(cprover_string_replace_func) IREP_ID_ONE(cprover_string_set_length_func)