Skip to content

Commit 733a88e

Browse files
Add preprocessing for CProverString.format
This makes the link between the CProverString.format signature from java and the ID_cprover_string_format_func from the solver.
1 parent c19cca9 commit 733a88e

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1807,6 +1807,14 @@ void java_string_library_preprocesst::initialize_conversion_table()
18071807
std::bind(&java_string_library_preprocesst::make_string_format_code,
18081808
this, std::placeholders::_1, std::placeholders::_2,
18091809
std::placeholders::_3, std::placeholders::_4);
1810+
1811+
std::string format_signature = "java::org.cprover.CProverString.format:(";
1812+
for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i)
1813+
format_signature += "Ljava/lang/String;";
1814+
format_signature += ")Ljava/lang/String;";
1815+
cprover_equivalent_to_java_string_returning_function[format_signature] =
1816+
ID_cprover_string_format_func;
1817+
18101818
cprover_equivalent_to_java_function
18111819
["java::java.lang.String.hashCode:()I"]=
18121820
ID_cprover_string_hash_code_func;

0 commit comments

Comments
 (0)