Skip to content

Commit 2306be0

Browse files
Remove preprocessing for String.format
This should now be in the model, and the implementation of models can use CProverString.format.
1 parent 278adbd commit 2306be0

File tree

1 file changed

+0
-6
lines changed

1 file changed

+0
-6
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1801,12 +1801,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
18011801
cprover_equivalent_to_java_function
18021802
["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
18031803
ID_cprover_string_equals_ignore_case_func;
1804-
conversion_table
1805-
["java::java.lang.String.format:(Ljava/lang/String;[Ljava/lang/Object;)"
1806-
"Ljava/lang/String;"] =
1807-
std::bind(&java_string_library_preprocesst::make_string_format_code,
1808-
this, std::placeholders::_1, std::placeholders::_2,
1809-
std::placeholders::_3, std::placeholders::_4);
18101804

18111805
std::string format_signature = "java::org.cprover.CProverString.format:(";
18121806
for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i)

0 commit comments

Comments
 (0)