Skip to content

Commit 7b52701

Browse files
committed
Remove string operations from preprocessing that are handled by models
1 parent 8c7ee00 commit 7b52701

File tree

1 file changed

+0
-40
lines changed

1 file changed

+0
-40
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 0 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -1668,26 +1668,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
16681668
cprover_equivalent_to_java_string_returning_function
16691669
["java::java.lang.String.trim:()Ljava/lang/String;"]=
16701670
ID_cprover_string_trim_func;
1671-
cprover_equivalent_to_java_string_returning_function
1672-
["java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]=
1673-
ID_cprover_string_of_bool_func;
1674-
cprover_equivalent_to_java_string_returning_function
1675-
["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]=
1676-
ID_cprover_string_of_char_func;
1677-
conversion_table["java::java.lang.String.valueOf:(F)Ljava/lang/String;"] =
1678-
std::bind(
1679-
&java_string_library_preprocesst::make_float_to_string_code,
1680-
this,
1681-
std::placeholders::_1,
1682-
std::placeholders::_2,
1683-
std::placeholders::_3,
1684-
std::placeholders::_4);
1685-
cprover_equivalent_to_java_string_returning_function
1686-
["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]=
1687-
ID_cprover_string_of_int_func;
1688-
cprover_equivalent_to_java_string_returning_function
1689-
["java::java.lang.String.valueOf:(J)Ljava/lang/String;"]=
1690-
ID_cprover_string_of_long_func;
16911671

16921672
// StringBuilder library
16931673
conversion_table
@@ -1826,14 +1806,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
18261806
conversion_table["java::java.lang.String.length:()I"];
18271807

18281808
// Other libraries
1829-
conversion_table["java::java.lang.Float.toString:(F)Ljava/lang/String;"] =
1830-
std::bind(
1831-
&java_string_library_preprocesst::make_float_to_string_code,
1832-
this,
1833-
std::placeholders::_1,
1834-
std::placeholders::_2,
1835-
std::placeholders::_3,
1836-
std::placeholders::_4);
18371809
cprover_equivalent_to_java_function
18381810
["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
18391811
ID_cprover_string_parse_int_func;
@@ -1849,18 +1821,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
18491821
cprover_equivalent_to_java_string_returning_function
18501822
["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
18511823
ID_cprover_string_of_int_hex_func;
1852-
cprover_equivalent_to_java_string_returning_function
1853-
["java::java.lang.Integer.toString:(I)Ljava/lang/String;"]=
1854-
ID_cprover_string_of_int_func;
1855-
cprover_equivalent_to_java_string_returning_function
1856-
["java::java.lang.Integer.toString:(II)Ljava/lang/String;"]=
1857-
ID_cprover_string_of_int_func;
1858-
cprover_equivalent_to_java_string_returning_function
1859-
["java::java.lang.Long.toString:(J)Ljava/lang/String;"]=
1860-
ID_cprover_string_of_int_func;
1861-
cprover_equivalent_to_java_string_returning_function
1862-
["java::java.lang.Long.toString:(JI)Ljava/lang/String;"]=
1863-
ID_cprover_string_of_int_func;
18641824
conversion_table["java::org.cprover.CProver.classIdentifier:("
18651825
"Ljava/lang/Object;)Ljava/lang/String;"] =
18661826
std::bind(

0 commit comments

Comments
 (0)