Skip to content

Commit ac4175c

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 142932a commit ac4175c

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
@@ -1963,13 +1963,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
19631963
std::placeholders::_2,
19641964
std::placeholders::_3,
19651965
std::placeholders::_4);
1966-
conversion_table["java::java.lang.String.<init>:([CII)V"] = std::bind(
1967-
&java_string_library_preprocesst::make_init_from_array_code,
1968-
this,
1969-
std::placeholders::_1,
1970-
std::placeholders::_2,
1971-
std::placeholders::_3,
1972-
std::placeholders::_4);
19731966
cprover_equivalent_to_java_constructor
19741967
["java::java.lang.String.<init>:()V"]=
19751968
ID_cprover_string_empty_string_func;
@@ -1997,12 +1990,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
19971990
cprover_equivalent_to_java_function
19981991
["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
19991992
ID_cprover_string_contains_func;
2000-
cprover_equivalent_to_java_string_returning_function
2001-
["java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]=
2002-
ID_cprover_string_copy_func;
2003-
cprover_equivalent_to_java_string_returning_function
2004-
["java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]=
2005-
ID_cprover_string_copy_func;
20061993
cprover_equivalent_to_java_function
20071994
["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
20081995
ID_cprover_string_endswith_func;
@@ -2158,9 +2145,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
21582145
cprover_equivalent_to_java_assign_and_return_function
21592146
["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
21602147
ID_cprover_string_concat_char_func;
2161-
cprover_equivalent_to_java_assign_and_return_function
2162-
["java::java.lang.StringBuilder.append:([C)Ljava/lang/StringBuilder;"] =
2163-
ID_cprover_string_concat_func;
21642148
cprover_equivalent_to_java_assign_and_return_function
21652149
["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] =
21662150
ID_cprover_string_concat_double_func;

0 commit comments

Comments
 (0)