Skip to content

Commit 3719036

Browse files
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.
1 parent 93d7a9e commit 3719036

File tree

2 files changed

+0
-7
lines changed

2 files changed

+0
-7
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

-6
Original file line numberDiff line numberDiff line change
@@ -2051,9 +2051,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
20512051
cprover_equivalent_to_java_assign_and_return_function
20522052
["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
20532053
"Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2054-
cprover_equivalent_to_java_assign_and_return_function
2055-
["java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;"]=
2056-
ID_cprover_string_concat_bool_func;
20572054
cprover_equivalent_to_java_assign_and_return_function
20582055
["java::java.lang.StringBuilder.appendCodePoint:(I)"
20592056
"Ljava/lang/StringBuilder;"]=
@@ -2160,9 +2157,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
21602157
cprover_equivalent_to_java_assign_and_return_function
21612158
["java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
21622159
"Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
2163-
cprover_equivalent_to_java_assign_and_return_function
2164-
["java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;"] =
2165-
ID_cprover_string_concat_bool_func;
21662160
cprover_equivalent_to_java_assign_and_return_function
21672161
["java::java.lang.StringBuffer.appendCodePoint:(I)"
21682162
"Ljava/lang/StringBuffer;"]=

src/util/irep_ids.def

-1
Original file line numberDiff line numberDiff line change
@@ -597,7 +597,6 @@ IREP_ID_ONE(cprover_string_concat_func)
597597
IREP_ID_ONE(cprover_string_concat_int_func)
598598
IREP_ID_ONE(cprover_string_concat_long_func)
599599
IREP_ID_ONE(cprover_string_concat_char_func)
600-
IREP_ID_ONE(cprover_string_concat_bool_func)
601600
IREP_ID_ONE(cprover_string_concat_double_func)
602601
IREP_ID_ONE(cprover_string_concat_float_func)
603602
IREP_ID_ONE(cprover_string_concat_code_point_func)

0 commit comments

Comments
 (0)