Skip to content

Commit bd292f7

Browse files
Stop preprocessing for unsupported functions
Conversion from char array to string does not work, because the string refinement is not aware of the operations performed on the arrays. To construct strings from char array, the constructors have to be implemented using loops instead.
1 parent 6d86626 commit bd292f7

File tree

1 file changed

+0
-16
lines changed

1 file changed

+0
-16
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 0 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1922,13 +1922,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
19221922
std::placeholders::_2,
19231923
std::placeholders::_3,
19241924
std::placeholders::_4);
1925-
conversion_table["java::java.lang.String.<init>:([CII)V"] = std::bind(
1926-
&java_string_library_preprocesst::make_init_from_array_code,
1927-
this,
1928-
std::placeholders::_1,
1929-
std::placeholders::_2,
1930-
std::placeholders::_3,
1931-
std::placeholders::_4);
19321925
cprover_equivalent_to_java_constructor
19331926
["java::java.lang.String.<init>:()V"]=
19341927
ID_cprover_string_empty_string_func;
@@ -1956,12 +1949,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
19561949
cprover_equivalent_to_java_function
19571950
["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
19581951
ID_cprover_string_contains_func;
1959-
cprover_equivalent_to_java_string_returning_function
1960-
["java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]=
1961-
ID_cprover_string_copy_func;
1962-
cprover_equivalent_to_java_string_returning_function
1963-
["java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]=
1964-
ID_cprover_string_copy_func;
19651952
cprover_equivalent_to_java_function
19661953
["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
19671954
ID_cprover_string_endswith_func;
@@ -2108,9 +2095,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
21082095
cprover_equivalent_to_java_assign_and_return_function
21092096
["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
21102097
ID_cprover_string_concat_char_func;
2111-
cprover_equivalent_to_java_assign_and_return_function
2112-
["java::java.lang.StringBuilder.append:([C)Ljava/lang/StringBuilder;"] =
2113-
ID_cprover_string_concat_func;
21142098
cprover_equivalent_to_java_assign_and_return_function
21152099
["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] =
21162100
ID_cprover_string_concat_double_func;

0 commit comments

Comments
 (0)