Skip to content

Commit 59cfa41

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

File tree

1 file changed

+13
-0
lines changed

1 file changed

+13
-0
lines changed

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -410,4 +410,17 @@ 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 {@param formatString}.
416+
* Unlike the JDK version, all arguments are given by strings, there is
417+
* a fixed number of them and they should not be null.
418+
* This fixed number corresponds to the constant {@code MAX_FORMAT_ARGS} defined in
419+
* {@code java_string_library_preprocess.h} from JBMC.
420+
*/
421+
public static String format(
422+
String formatString, String arg0, String arg1, String arg2, String arg3,
423+
String arg4, String arg5, String arg6, String arg7, String arg8, String arg9) {
424+
return CProver.nondetWithoutNullForNotModelled();
425+
}
413426
}

0 commit comments

Comments
 (0)