Note: If the character at the given index is a supplementary - * character, this method does not remove the entire character. If - * correct handling of supplementary characters is required, - * determine the number of {@code char}s to remove by calling - * {@code Character.charCount(thisSequence.codePointAt(index))}, - * where {@code thisSequence} is this sequence. - * - * @param instance the StringBuffer instance. - * @param index index of {@code char} to remove - * @return this object. - */ - public static StringBuffer deleteCharAt(StringBuffer instance, int index) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Returns a new {@code String} that contains a subsequence of - * characters currently contained in this sequence. - * - * @param instance the StringBuffer instance. - * @param start the beginning index, inclusive. - * @param end the ending index, exclusive. - * @return The new string. - */ - public static String substring(StringBuffer instance, int start, int end) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Inserts the string into this character sequence. - * - * @param instance the StringBuffer instance. - * @param offset the offset. - * @param str a string. - * @return The modified StringBuffer. - */ - public static StringBuffer insert( - StringBuffer instance, int offset, String str) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Inserts the string representation of the {@code boolean} - * argument into this sequence. - * - * @param offset the offset. - * @param b a {@code boolean}. - * @return a reference to this object. - */ - public static StringBuffer insert( - StringBuffer instance, int offset, boolean b) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Inserts the string representation of the {@code char} - * argument into this sequence. - * - * @param offset the offset. - * @param c a {@code char}. - * @return a reference to this object. - */ - public static StringBuffer insert( - StringBuffer instance, int offset, char c) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Inserts the string representation of the {@code int} - * argument into this sequence. - * - * @param offset the offset. - * @param i a {@code int}. - * @return a reference to this object. - */ - public static StringBuffer insert( - StringBuffer instance, int offset, int i) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Inserts the string representation of the {@code long} - * argument into this sequence. - * - * @param offset the offset. - * @param l a {@code long}. - * @return a reference to this object. - */ - public static StringBuffer insert( - StringBuffer instance, int offset, long l) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Converts an array of characters to a string. This uses a loop and - * therefore in test-generation the {@code count} will be limited by the - * unwind parameter. - * This constrains {@code value} to not be null, its length to be greater - * or equal to {@code offset + count} and {@code offset} and {@code count} - * to be non-negative. - * - * @param value array of characters which is the source to copy from - * @param offset index in {@code value} of the first character to copy - * @param count number of characters to copy - * @return The created String - */ - public static String ofCharArray(char value[], int offset, int count) { - CProver.assume(value != null); - CProver.assume(value.length - count >= offset - && offset >= 0 && count >= 0); - StringBuilder builder = new StringBuilder(); - for(int i = 0; i < count; i++) { - builder.append(value[offset + i]); - } - return builder.toString(); - } - - /** - * Format a string according to the given {@param formatString}. - * Unlike the JDK version, all arguments are given by strings, there is - * a fixed number of them and they should not be null. - * This fixed number corresponds to the constant {@code MAX_FORMAT_ARGS} defined in - * {@code java_string_library_preprocess.h} from JBMC. - */ - public static String format( - String formatString, String arg0, String arg1, String arg2, String arg3, - String arg4, String arg5, String arg6, String arg7, String arg8, String arg9) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Returns a {@code String} object representing the - * specified integer. The argument is converted to signed decimal - * representation and returned as a string. - * - * @param i an integer to be converted. - * @return a string representation of the argument in base 10. - */ - public static String toString(int i) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Returns a string representation of the first argument in the - * radix specified by the second argument. - * - * @param i an integer to be converted to a string. - * @param radix the radix to use in the string representation. - * @return a string representation of the argument in the specified radix. - */ - public static String toString(int i, int radix) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Returns a {@code String} object representing the specified - * {@code long}. The argument is converted to signed decimal - * representation and returned as a string. - * - * @param l a {@code long} to be converted. - * @return a string representation of the argument in base 10. - */ - public static String toString(long l) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Returns a string representation of the first argument in the - * radix specified by the second argument. - * - * @param l a {@code long} to be converted to a string. - * @param radix the radix to use in the string representation. - * @return a string representation of the argument in the specified radix. - */ - public static String toString(long l, int radix) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Returns a string representation of the {@code float} - * argument. - * - * @param f the float to be converted. - * @return a string representation of the argument. - */ - public static String toString(float f) { - return CProver.nondetWithoutNullForNotModelled(); - } - - /** - * Returns a string representation of the {@code double} - * argument. - * - * The double is converted to a float first as the string solver currently - * can convert float to String but not double to String. - * - * @param d the double to be converted. - * @return a string representation of the argument. - */ - public static String toString(double d) { - return toString(CProver.doubleToFloat(d)); - } - - /** - * Exactly as Integer.parseInt, except s is already checked non-null, the - * radix is already checked in-range and 's' is known to be a valid integer - * according to isValidInt below - */ - public static int parseInt(String s, int radix) { - return CProver.nondetInt(); - } - - /** - * Exactly as Long.parseLong, except s is already checked non-null, the - * radix is already checked in-range and 's' is known to be a valid integer - * according to isValidLong below - */ - public static long parseLong(String s, int radix) { - return CProver.nondetLong(); - } - - /** - * Returns true if string 's' is a valid integer: contains at least one - * digit, perhaps a leading '+' or '-', and doesn't contain invalid chars - * for the given radix. - */ - public static boolean isValidInt(String s, int radix) { - return CProver.nondetBoolean(); - } - - /** - * Returns true if string 's' is a valid long: contains at least one - * digit, perhaps a leading '+' or '-', and doesn't contain invalid chars - * for the given radix. - */ - public static boolean isValidLong(String s, int radix) { - return CProver.nondetBoolean(); - } -} diff --git a/src/main/java/org/cprover/MustNotThrow.java b/src/main/java/org/cprover/MustNotThrow.java deleted file mode 100644 index 7be14b1..0000000 --- a/src/main/java/org/cprover/MustNotThrow.java +++ /dev/null @@ -1,8 +0,0 @@ -package org.cprover; - -/** - * This can be added to methods to indicate they aren't allowed to throw - * exceptions. JBMC and related tools will truncate any execution path on which - * they do with an ASSUME FALSE instruction. - */ -public @interface MustNotThrow { }