Skip to content

Commit d0acccb

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 c9e1281 commit d0acccb

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
@@ -1962,13 +1962,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
19621962
std::placeholders::_2,
19631963
std::placeholders::_3,
19641964
std::placeholders::_4);
1965-
conversion_table["java::java.lang.String.<init>:([CII)V"] = std::bind(
1966-
&java_string_library_preprocesst::make_init_from_array_code,
1967-
this,
1968-
std::placeholders::_1,
1969-
std::placeholders::_2,
1970-
std::placeholders::_3,
1971-
std::placeholders::_4);
19721965
cprover_equivalent_to_java_constructor
19731966
["java::java.lang.String.<init>:()V"]=
19741967
ID_cprover_string_empty_string_func;
@@ -1996,12 +1989,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
19961989
cprover_equivalent_to_java_function
19971990
["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
19981991
ID_cprover_string_contains_func;
1999-
cprover_equivalent_to_java_string_returning_function
2000-
["java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]=
2001-
ID_cprover_string_copy_func;
2002-
cprover_equivalent_to_java_string_returning_function
2003-
["java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]=
2004-
ID_cprover_string_copy_func;
20051992
cprover_equivalent_to_java_function
20061993
["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
20071994
ID_cprover_string_endswith_func;
@@ -2157,9 +2144,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
21572144
cprover_equivalent_to_java_assign_and_return_function
21582145
["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
21592146
ID_cprover_string_concat_char_func;
2160-
cprover_equivalent_to_java_assign_and_return_function
2161-
["java::java.lang.StringBuilder.append:([C)Ljava/lang/StringBuilder;"] =
2162-
ID_cprover_string_concat_func;
21632147
cprover_equivalent_to_java_assign_and_return_function
21642148
["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] =
21652149
ID_cprover_string_concat_double_func;

0 commit comments

Comments
 (0)