Merge pull request #3448 from romainbrenguier/bugfix/string-concat-bool

tautschnig · web-flow · commit 9706f5319d27 · 2018-11-20T12:42:56.000Z
Remove preprocessing that was using ID_cprover_string_concat_bool_func
diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library
@@ -1 +1 @@
-Subproject commit 1068a992642ab6adbe1d4aab2c868cf81445ca25
+Subproject commit d825533d7feaa477dba880abd679805dede9bb4e
diff --git 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
@@ -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)
