Skip to content

Commit c2fdd88

Browse files
Add CProverString.format function
This directly translates to a builtin function of CBMC string solver.
1 parent d92026c commit c2fdd88

File tree

1 file changed

+11
-0
lines changed

1 file changed

+11
-0
lines changed

src/main/java/org/cprover/CProverString.java

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -410,4 +410,15 @@ public static String ofCharArray(char value[], int offset, int count) {
410410
}
411411
return builder.toString();
412412
}
413+
414+
/**
415+
* Format a string according to the given {@code format}.
416+
* Unlike the java version, all arguments are given by strings, there is
417+
* a fixed number of them and they should not be null.
418+
*/
419+
public static String format(
420+
String formatString, String arg0, String arg1, String arg2, String arg3,
421+
String arg4, String arg5, String arg6, String arg7, String arg8, String arg9) {
422+
return CProver.nondetWithoutNullForNotModelled();
423+
}
413424
}

0 commit comments

Comments
 (0)