Skip to content

Commit 05eaa8d

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 b57022c commit 05eaa8d

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
@@ -1858,6 +1858,14 @@ void java_string_library_preprocesst::initialize_conversion_table()
18581858
std::placeholders::_2,
18591859
std::placeholders::_3,
18601860
std::placeholders::_4);
1861+
1862+
std::string format_signature = "java::org.cprover.CProverString.format:(";
1863+
for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i)
1864+
format_signature += "Ljava/lang/String;";
1865+
format_signature += ")Ljava/lang/String;";
1866+
cprover_equivalent_to_java_string_returning_function[format_signature] =
1867+
ID_cprover_string_format_func;
1868+
18611869
cprover_equivalent_to_java_function
18621870
["java::java.lang.String.hashCode:()I"]=
18631871
ID_cprover_string_hash_code_func;

0 commit comments

Comments
 (0)