Skip to content

Commit 862a366

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 433e4e4 commit 862a366

File tree

1 file changed

+0
-10
lines changed

1 file changed

+0
-10
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1848,16 +1848,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
18481848
cprover_equivalent_to_java_function
18491849
["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
18501850
ID_cprover_string_equals_ignore_case_func;
1851-
conversion_table
1852-
["java::java.lang.String.format:(Ljava/lang/String;[Ljava/lang/Object;)"
1853-
"Ljava/lang/String;"] =
1854-
std::bind(
1855-
&java_string_library_preprocesst::make_string_format_code,
1856-
this,
1857-
std::placeholders::_1,
1858-
std::placeholders::_2,
1859-
std::placeholders::_3,
1860-
std::placeholders::_4);
18611851

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

0 commit comments

Comments
 (0)