From 93d7a9e796d9e00a0996827af5da2522b927863e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 20 Nov 2018 10:41:22 +0000 Subject: [PATCH 1/2] Update lib/java-models-library for java-models-library#14 (String.valueOf(boolean)) https://github.com/diffblue/java-models-library/pull/14 --- jbmc/lib/java-models-library | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index 1068a992642..d825533d7fe 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit 1068a992642ab6adbe1d4aab2c868cf81445ca25 +Subproject commit d825533d7feaa477dba880abd679805dede9bb4e From 371903697da18b01fae601e1cda288ada349ba6c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 20 Nov 2018 10:48:15 +0000 Subject: [PATCH 2/2] Remove preprocessing that was using string_concat_bool This function is not handled by the solver, so preprocessing functions and producing ID_cprover_string_concat_bool_func could only lead to errors. It should rather be using models of these functions given in java classes. --- jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 6 ------ src/util/irep_ids.def | 1 - 2 files changed, 7 deletions(-) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 73d392151aa..8fa9f5fc310 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -2051,9 +2051,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)" "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_bool_func; cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuilder.appendCodePoint:(I)" "Ljava/lang/StringBuilder;"]= @@ -2160,9 +2157,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)" "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;"] = - ID_cprover_string_concat_bool_func; cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuffer.appendCodePoint:(I)" "Ljava/lang/StringBuffer;"]= diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 4d2b2b4a43d..9b43116c3e4 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -597,7 +597,6 @@ IREP_ID_ONE(cprover_string_concat_func) IREP_ID_ONE(cprover_string_concat_int_func) IREP_ID_ONE(cprover_string_concat_long_func) IREP_ID_ONE(cprover_string_concat_char_func) -IREP_ID_ONE(cprover_string_concat_bool_func) IREP_ID_ONE(cprover_string_concat_double_func) IREP_ID_ONE(cprover_string_concat_float_func) IREP_ID_ONE(cprover_string_concat_code_point_func)