diff --git a/src/main/java/java/lang/Boolean.java b/src/main/java/java/lang/Boolean.java new file mode 100644 index 0000000..fee8ae1 --- /dev/null +++ b/src/main/java/java/lang/Boolean.java @@ -0,0 +1,339 @@ +/* + * Copyright (c) 1994, 2013, Oracle and/or its affiliates. All rights reserved. + * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER. + * + * This code is free software; you can redistribute it and/or modify it + * under the terms of the GNU General Public License version 2 only, as + * published by the Free Software Foundation. Oracle designates this + * particular file as subject to the "Classpath" exception as provided + * by Oracle in the LICENSE file that accompanied this code. + * + * This code is distributed in the hope that it will be useful, but WITHOUT + * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or + * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License + * version 2 for more details (a copy is included in the LICENSE file that + * accompanied this code). + * + * You should have received a copy of the GNU General Public License version + * 2 along with this work; if not, write to the Free Software Foundation, + * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA. + * + * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA + * or visit www.oracle.com if you need additional information or have any + * questions. + */ + +package java.lang; + +/** + * The Boolean class wraps a value of the primitive type + * {@code boolean} in an object. An object of type + * {@code Boolean} contains a single field whose type is + * {@code boolean}. + *
+ * In addition, this class provides many methods for
+ * converting a {@code boolean} to a {@code String} and a
+ * {@code String} to a {@code boolean}, as well as other
+ * constants and methods useful when dealing with a
+ * {@code boolean}.
+ *
+ * @author Arthur van Hoff
+ * @since JDK1.0
+ */
+public final class Boolean implements java.io.Serializable,
+ Comparable Note: It is rarely appropriate to use this constructor.
+ * Unless a new instance is required, the static factory
+ * {@link #valueOf(boolean)} is generally a better choice. It is
+ * likely to yield significantly better space and time performance.
+ *
+ * @param value the value of the {@code Boolean}.
+ */
+ public Boolean(boolean value) {
+ this.value = value;
+ }
+
+ /**
+ * Allocates a {@code Boolean} object representing the value
+ * {@code true} if the string argument is not {@code null}
+ * and is equal, ignoring case, to the string {@code "true"}.
+ * Otherwise, allocate a {@code Boolean} object representing the
+ * value {@code false}. Examples:
+ * {@code new Boolean("True")} produces a {@code Boolean} object
+ * that represents {@code true}.
+ * Example: {@code Boolean.parseBoolean("True")} returns {@code true}.
+ * If there is no property with the specified name, or if the specified
+ * name is empty or null, then {@code false} is returned.
+ *
+ * @param name the system property name.
+ * @return the {@code boolean} value of the system property.
+ * @throws SecurityException for the same reasons as
+ * {@link System#getProperty(String) System.getProperty}
+ * @see java.lang.System#getProperty(java.lang.String)
+ * @see java.lang.System#getProperty(java.lang.String, java.lang.String)
+ */
+ public static boolean getBoolean(String name) {
+ boolean result = false;
+ try {
+ result = parseBoolean(System.getProperty(name));
+ } catch (IllegalArgumentException | NullPointerException e) {
+ }
+ return result;
+ }
+
+ /**
+ * Compares this {@code Boolean} instance with another.
+ *
+ * @param b the {@code Boolean} instance to be compared
+ * @return zero if this object represents the same boolean value as the
+ * argument; a positive value if this object represents true
+ * and the argument represents false; and a negative value if
+ * this object represents false and the argument represents true
+ * @throws NullPointerException if the argument is {@code null}
+ * @see Comparable
+ * @since 1.5
+ */
+ public int compareTo(Boolean b) {
+ return compare(this.value, b.value);
+ }
+
+ /**
+ * Compares two {@code boolean} values.
+ * The value returned is identical to what would be returned by:
+ * In addition, this class provides several methods for converting
+ * a {@code byte} to a {@code String} and a {@code String} to a {@code
+ * byte}, as well as other constants and methods useful when dealing
+ * with a {@code byte}.
+ *
+ * @author Nakul Saraiya
+ * @author Joseph D. Darcy
+ * @see java.lang.Number
+ * @since JDK1.1
+ */
+public final class Byte extends Number implements Comparable An exception of type {@code NumberFormatException} is
+ * thrown if any of the following situations occurs:
+ * In other words, this method returns a {@code Byte} object
+ * equal to the value of:
+ *
+ * In other words, this method returns a {@code Byte} object
+ * equal to the value of:
+ *
+ * The sequence of characters following an optional
+ * sign and/or radix specifier ("{@code 0x}", "{@code 0X}",
+ * "{@code #}", or leading zero) is parsed as by the {@code
+ * Byte.parseByte} method with the indicated radix (10, 16, or 8).
+ * This sequence of characters must represent a positive value or
+ * a {@link NumberFormatException} will be thrown. The result is
+ * negated if first character of the specified {@code String} is
+ * the minus sign. No whitespace characters are permitted in the
+ * {@code String}.
+ *
+ * @param nm the {@code String} to decode.
+ * @return a {@code Byte} object holding the {@code byte}
+ * value represented by {@code nm}
+ * @throws NumberFormatException if the {@code String} does not
+ * contain a parsable {@code byte}.
+ * @see java.lang.Byte#parseByte(java.lang.String, int)
+ */
+ public static Byte decode(String nm) throws NumberFormatException {
+ int i = Integer.decode(nm);
+ if (i < MIN_VALUE || i > MAX_VALUE)
+ throw new NumberFormatException(
+ "Value " + i + " out of range from input " + nm);
+ return valueOf((byte)i);
+ }
+
+ /**
+ * The value of the {@code Byte}.
+ *
+ * @serial
+ */
+ private final byte value;
+
+ /**
+ * Constructs a newly allocated {@code Byte} object that
+ * represents the specified {@code byte} value.
+ *
+ * @param value the value to be represented by the
+ * {@code Byte}.
+ */
+ public Byte(byte value) {
+ this.value = value;
+ }
+
+ /**
+ * Constructs a newly allocated {@code Byte} object that
+ * represents the {@code byte} value indicated by the
+ * {@code String} parameter. The string is converted to a
+ * {@code byte} value in exactly the manner used by the
+ * {@code parseByte} method for radix 10.
+ *
+ * @param s the {@code String} to be converted to a
+ * {@code Byte}
+ * @throws NumberFormatException If the {@code String}
+ * does not contain a parsable {@code byte}.
+ * @see java.lang.Byte#parseByte(java.lang.String, int)
+ */
+ public Byte(String s) throws NumberFormatException {
+ this.value = parseByte(s, 10);
+ }
+
+ /**
+ * Returns the value of this {@code Byte} as a
+ * {@code byte}.
+ */
+ public byte byteValue() {
+ return value;
+ }
+
+ /**
+ * Returns the value of this {@code Byte} as a {@code short} after
+ * a widening primitive conversion.
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public short shortValue() {
+ return (short)value;
+ }
+
+ /**
+ * Returns the value of this {@code Byte} as an {@code int} after
+ * a widening primitive conversion.
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public int intValue() {
+ return (int)value;
+ }
+
+ /**
+ * Returns the value of this {@code Byte} as a {@code long} after
+ * a widening primitive conversion.
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public long longValue() {
+ return (long)value;
+ }
+
+ /**
+ * Returns the value of this {@code Byte} as a {@code float} after
+ * a widening primitive conversion.
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public float floatValue() {
+ return (float)value;
+ }
+
+ /**
+ * Returns the value of this {@code Byte} as a {@code double}
+ * after a widening primitive conversion.
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public double doubleValue() {
+ return (double)value;
+ }
+
+ /**
+ * Returns a {@code String} object representing this
+ * {@code Byte}'s value. The value is converted to signed
+ * decimal representation and returned as a string, exactly as if
+ * the {@code byte} value were given as an argument to the
+ * {@link java.lang.Byte#toString(byte)} method.
+ *
+ * @return a string representation of the value of this object in
+ * base 10.
+ */
+ public String toString() {
+ return Integer.toString((int)value);
+ }
+
+ /**
+ * Returns a hash code for this {@code Byte}; equal to the result
+ * of invoking {@code intValue()}.
+ *
+ * @return a hash code value for this {@code Byte}
+ */
+ @Override
+ public int hashCode() {
+ return Byte.hashCode(value);
+ }
+
+ /**
+ * Returns a hash code for a {@code byte} value; compatible with
+ * {@code Byte.hashCode()}.
+ *
+ * @param value the value to hash
+ * @return a hash code value for a {@code byte} value.
+ * @since 1.8
+ */
+ public static int hashCode(byte value) {
+ return (int)value;
+ }
+
+ /**
+ * Compares this object to the specified object. The result is
+ * {@code true} if and only if the argument is not
+ * {@code null} and is a {@code Byte} object that
+ * contains the same {@code byte} value as this object.
+ *
+ * @param obj the object to compare with
+ * @return {@code true} if the objects are the same;
+ * {@code false} otherwise.
+ */
+ public boolean equals(Object obj) {
+ if (obj instanceof Byte) {
+ return value == ((Byte)obj).byteValue();
+ }
+ return false;
+ }
+
+ /**
+ * Compares two {@code Byte} objects numerically.
+ *
+ * @param anotherByte the {@code Byte} to be compared.
+ * @return the value {@code 0} if this {@code Byte} is
+ * equal to the argument {@code Byte}; a value less than
+ * {@code 0} if this {@code Byte} is numerically less
+ * than the argument {@code Byte}; and a value greater than
+ * {@code 0} if this {@code Byte} is numerically
+ * greater than the argument {@code Byte} (signed
+ * comparison).
+ * @since 1.2
+ */
+ public int compareTo(Byte anotherByte) {
+ return compare(this.value, anotherByte.value);
+ }
+
+ /**
+ * Compares two {@code byte} values numerically.
+ * The value returned is identical to what would be returned by:
+ * The field to be reflected is determined by the algorithm that
+ * follows. Let C be the class or interface represented by this object:
+ *
+ * If this {@code Class} object represents an array type, then this
+ * method does not find the {@code length} field of the array type.
+ *
+ * @param name the field name
+ * @return the {@code Field} object of this class specified by
+ * {@code name}
+ * @throws NoSuchFieldException if a field with the specified name is
+ * not found.
+ * @throws NullPointerException if {@code name} is {@code null}
+ * @throws SecurityException
+ * If a security manager, s, is present and
+ * the caller's class loader is not the same as or an
+ * ancestor of the class loader for the current class and
+ * invocation of {@link SecurityManager#checkPackageAccess
+ * s.checkPackageAccess()} denies access to the package
+ * of this class.
+ *
+ * @since JDK1.1
+ * @jls 8.2 Class Members
+ * @jls 8.3 Field Declarations
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public Field getField(String name) throws NoSuchFieldException, SecurityException {
+ return new Field(this, name);
}
+ /**
+ * Returns a {@code Method} object that reflects the specified public
+ * member method of the class or interface represented by this
+ * {@code Class} object. The {@code name} parameter is a
+ * {@code String} specifying the simple name of the desired method. The
+ * {@code parameterTypes} parameter is an array of {@code Class}
+ * objects that identify the method's formal parameter types, in declared
+ * order. If {@code parameterTypes} is {@code null}, it is
+ * treated as if it were an empty array.
+ *
+ * If the {@code name} is "{@code To find a matching method in a class or interface C: If C
+ * declares exactly one public method with the specified name and exactly
+ * the same formal parameter types, that is the method reflected. If more
+ * than one such method is found in C, and one of these methods has a
+ * return type that is more specific than any of the others, that method is
+ * reflected; otherwise one of the methods is chosen arbitrarily.
+ *
+ * Note that there may be more than one matching method in a
+ * class because while the Java language forbids a class to
+ * declare multiple methods with the same signature but different
+ * return types, the Java virtual machine does not. This
+ * increased flexibility in the virtual machine can be used to
+ * implement various language features. For example, covariant
+ * returns can be implemented with {@linkplain
+ * java.lang.reflect.Method#isBridge bridge methods}; the bridge
+ * method and the method being overridden would have the same
+ * signature but different return types.
+ *
+ * If this {@code Class} object represents an array type, then this
+ * method does not find the {@code clone()} method.
+ *
+ * Static methods declared in superinterfaces of the class or interface
+ * represented by this {@code Class} object are not considered members of
+ * the class or interface.
+ *
+ * @param name the name of the method
+ * @param parameterTypes the list of parameters
+ * @return the {@code Method} object that matches the specified
+ * {@code name} and {@code parameterTypes}
+ * @throws NoSuchMethodException if a matching method is not found
+ * or if the name is "<init>"or "<clinit>".
+ * @throws NullPointerException if {@code name} is {@code null}
+ * @throws SecurityException
+ * If a security manager, s, is present and
+ * the caller's class loader is not the same as or an
+ * ancestor of the class loader for the current class and
+ * invocation of {@link SecurityManager#checkPackageAccess
+ * s.checkPackageAccess()} denies access to the package
+ * of this class.
+ *
+ * @jls 8.2 Class Members
+ * @jls 8.4 Method Declarations
+ * @since JDK1.1
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public Method getMethod(String name, Class>... parameterTypes) throws NoSuchMethodException, SecurityException {
+ return new Method(this, name, parameterTypes);
+ }
}
diff --git a/src/main/java/java/lang/Double.java b/src/main/java/java/lang/Double.java
new file mode 100644
index 0000000..2bb0975
--- /dev/null
+++ b/src/main/java/java/lang/Double.java
@@ -0,0 +1,1105 @@
+/*
+ * Copyright (c) 1994, 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.lang;
+
+import org.cprover.CProverString;
+// DIFFBLUE MODEL LIBRARY
+// removed for compatibility with Java 9 and newer
+// import sun.misc.FloatingDecimal;
+// import sun.misc.FpUtils;
+import sun.misc.DoubleConsts;
+import org.cprover.CProver;
+/**
+ * The {@code Double} class wraps a value of the primitive type
+ * {@code double} in an object. An object of type
+ * {@code Double} contains a single field whose type is
+ * {@code double}.
+ *
+ * In addition, this class provides several methods for converting a
+ * {@code double} to a {@code String} and a
+ * {@code String} to a {@code double}, as well as other
+ * constants and methods useful when dealing with a
+ * {@code double}.
+ *
+ * @author Lee Boynton
+ * @author Arthur van Hoff
+ * @author Joseph D. Darcy
+ * @since JDK1.0
+ */
+public final class Double extends Number implements Comparable To create localized string representations of a floating-point
+ * value, use subclasses of {@link java.text.NumberFormat}.
+ *
+ * @param d the {@code double} to be converted.
+ * @return a string representation of the argument.
+ * @diffblue.noSupport
+ */
+ public static String toString(double d) {
+ // return FloatingDecimal.toJavaFormatString(d);
+ return String.valueOf(d);
+ }
+
+ /**
+ * Returns a hexadecimal string representation of the
+ * {@code double} argument. All characters mentioned below
+ * are ASCII characters.
+ *
+ * If {@code s} is {@code null}, then a
+ * {@code NullPointerException} is thrown.
+ *
+ * Leading and trailing whitespace characters in {@code s}
+ * are ignored. Whitespace is removed as if by the {@link
+ * String#trim} method; that is, both ASCII space and control
+ * characters are removed. The rest of {@code s} should
+ * constitute a FloatValue as described by the lexical
+ * syntax rules:
+ *
+ * To interpret localized string representations of a
+ * floating-point value, use subclasses of {@link
+ * java.text.NumberFormat}.
+ *
+ * Note that trailing format specifiers, specifiers that
+ * determine the type of a floating-point literal
+ * ({@code 1.0f} is a {@code float} value;
+ * {@code 1.0d} is a {@code double} value), do
+ * not influence the results of this method. In other
+ * words, the numerical value of the input string is converted
+ * directly to the target floating-point type. The two-step
+ * sequence of conversions, string to {@code float} followed
+ * by {@code float} to {@code double}, is not
+ * equivalent to converting a string directly to
+ * {@code double}. For example, the {@code float}
+ * literal {@code 0.1f} is equal to the {@code double}
+ * value {@code 0.10000000149011612}; the {@code float}
+ * literal {@code 0.1f} represents a different numerical
+ * value than the {@code double} literal
+ * {@code 0.1}. (The numerical value 0.1 cannot be exactly
+ * represented in a binary floating-point number.)
+ *
+ * To avoid calling this method on an invalid string and having
+ * a {@code NumberFormatException} be thrown, the regular
+ * expression below can be used to screen the input string:
+ *
+ * Note that in most cases, for two instances of class
+ * {@code Double}, {@code d1} and {@code d2}, the
+ * value of {@code d1.equals(d2)} is {@code true} if and
+ * only if
+ *
+ * also has the value {@code true}. However, there are two
+ * exceptions:
+ * Bit 63 (the bit that is selected by the mask
+ * {@code 0x8000000000000000L}) represents the sign of the
+ * floating-point number. Bits
+ * 62-52 (the bits that are selected by the mask
+ * {@code 0x7ff0000000000000L}) represent the exponent. Bits 51-0
+ * (the bits that are selected by the mask
+ * {@code 0x000fffffffffffffL}) represent the significand
+ * (sometimes called the mantissa) of the floating-point number.
+ *
+ * If the argument is positive infinity, the result is
+ * {@code 0x7ff0000000000000L}.
+ *
+ * If the argument is negative infinity, the result is
+ * {@code 0xfff0000000000000L}.
+ *
+ * If the argument is NaN, the result is
+ * {@code 0x7ff8000000000000L}.
+ *
+ * In all cases, the result is a {@code long} integer that, when
+ * given to the {@link #longBitsToDouble(long)} method, will produce a
+ * floating-point value the same as the argument to
+ * {@code doubleToLongBits} (except all NaN values are
+ * collapsed to a single "canonical" NaN value).
+ *
+ * @param value a {@code double} precision floating-point number.
+ * @return the bits that represent the floating-point number.
+ */
+ public static long doubleToLongBits(double value) {
+ long result = doubleToRawLongBits(value);
+ // Check for NaN based on values of bit fields, maximum
+ // exponent and nonzero significand.
+ if ( ((result & DoubleConsts.EXP_BIT_MASK) ==
+ DoubleConsts.EXP_BIT_MASK) &&
+ (result & DoubleConsts.SIGNIF_BIT_MASK) != 0L)
+ result = 0x7ff8000000000000L;
+ return result;
+ }
+
+ /**
+ * Returns a representation of the specified floating-point value
+ * according to the IEEE 754 floating-point "double
+ * format" bit layout, preserving Not-a-Number (NaN) values.
+ *
+ * Bit 63 (the bit that is selected by the mask
+ * {@code 0x8000000000000000L}) represents the sign of the
+ * floating-point number. Bits
+ * 62-52 (the bits that are selected by the mask
+ * {@code 0x7ff0000000000000L}) represent the exponent. Bits 51-0
+ * (the bits that are selected by the mask
+ * {@code 0x000fffffffffffffL}) represent the significand
+ * (sometimes called the mantissa) of the floating-point number.
+ *
+ * If the argument is positive infinity, the result is
+ * {@code 0x7ff0000000000000L}.
+ *
+ * If the argument is negative infinity, the result is
+ * {@code 0xfff0000000000000L}.
+ *
+ * If the argument is NaN, the result is the {@code long}
+ * integer representing the actual NaN value. Unlike the
+ * {@code doubleToLongBits} method,
+ * {@code doubleToRawLongBits} does not collapse all the bit
+ * patterns encoding a NaN to a single "canonical" NaN
+ * value.
+ *
+ * In all cases, the result is a {@code long} integer that,
+ * when given to the {@link #longBitsToDouble(long)} method, will
+ * produce a floating-point value the same as the argument to
+ * {@code doubleToRawLongBits}.
+ *
+ * @param value a {@code double} precision floating-point number.
+ * @return the bits that represent the floating-point number.
+ * @since 1.3
+ */
+ public static long doubleToRawLongBits(double value){
+ //@TODO: implement this method internally in CBMC
+ return CProver.nondetLong();
+ }
+
+ /**
+ * Returns the {@code double} value corresponding to a given
+ * bit representation.
+ * The argument is considered to be a representation of a
+ * floating-point value according to the IEEE 754 floating-point
+ * "double format" bit layout.
+ *
+ * If the argument is {@code 0x7ff0000000000000L}, the result
+ * is positive infinity.
+ *
+ * If the argument is {@code 0xfff0000000000000L}, the result
+ * is negative infinity.
+ *
+ * If the argument is any value in the range
+ * {@code 0x7ff0000000000001L} through
+ * {@code 0x7fffffffffffffffL} or in the range
+ * {@code 0xfff0000000000001L} through
+ * {@code 0xffffffffffffffffL}, the result is a NaN. No IEEE
+ * 754 floating-point operation provided by Java can distinguish
+ * between two NaN values of the same type with different bit
+ * patterns. Distinct values of NaN are only distinguishable by
+ * use of the {@code Double.doubleToRawLongBits} method.
+ *
+ * In all other cases, let s, e, and m be three
+ * values that can be computed from the argument:
+ *
+ * Note that this method may not be able to return a
+ * {@code double} NaN with exactly same bit pattern as the
+ * {@code long} argument. IEEE 754 distinguishes between two
+ * kinds of NaNs, quiet NaNs and signaling NaNs. The
+ * differences between the two kinds of NaN are generally not
+ * visible in Java. Arithmetic operations on signaling NaNs turn
+ * them into quiet NaNs with a different, but often similar, bit
+ * pattern. However, on some processors merely copying a
+ * signaling NaN also performs that conversion. In particular,
+ * copying a signaling NaN to return it to the calling method
+ * may perform this conversion. So {@code longBitsToDouble}
+ * may not be able to return a {@code double} with a
+ * signaling NaN bit pattern. Consequently, for some
+ * {@code long} values,
+ * {@code doubleToRawLongBits(longBitsToDouble(start))} may
+ * not equal {@code start}. Moreover, which
+ * particular bit patterns represent signaling NaNs is platform
+ * dependent; although all NaN bit patterns, quiet or signaling,
+ * must be in the NaN range identified above.
+ *
+ * @param bits any {@code long} integer.
+ * @return the {@code double} floating-point value with the same
+ * bit pattern.
+ */
+ public static double longBitsToDouble(long bits){
+ //@TODO: implement this method internally in CBMC
+ return CProver.nondetDouble();
+ }
+
+ /**
+ * Compares two {@code Double} objects numerically. There
+ * are two ways in which comparisons performed by this method
+ * differ from those performed by the Java language numerical
+ * comparison operators ({@code <, <=, ==, >=, >})
+ * when applied to primitive {@code double} values:
+ * In addition, this class provides several methods for converting a
+ * {@code float} to a {@code String} and a
+ * {@code String} to a {@code float}, as well as other
+ * constants and methods useful when dealing with a
+ * {@code float}.
+ *
+ * @author Lee Boynton
+ * @author Arthur van Hoff
+ * @author Joseph D. Darcy
+ * @since JDK1.0
+ */
+public final class Float extends Number implements Comparable To create localized string representations of a floating-point
+ * value, use subclasses of {@link java.text.NumberFormat}.
+ *
+ * @param f the float to be converted.
+ * @return a string representation of the argument.
+ * @diffblue.noSupport
+ */
+ public static String toString(float f) {
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // return FloatingDecimal.toJavaFormatString(f);
+ CProver.notModelled();
+ return CProver.nondetWithNullForNotModelled();
+ }
+
+ /**
+ * Returns a hexadecimal string representation of the
+ * {@code float} argument. All characters mentioned below are
+ * ASCII characters.
+ *
+ * If {@code s} is {@code null}, then a
+ * {@code NullPointerException} is thrown.
+ *
+ * Leading and trailing whitespace characters in {@code s}
+ * are ignored. Whitespace is removed as if by the {@link
+ * String#trim} method; that is, both ASCII space and control
+ * characters are removed. The rest of {@code s} should
+ * constitute a FloatValue as described by the lexical
+ * syntax rules:
+ *
+ * To interpret localized string representations of a
+ * floating-point value, use subclasses of {@link
+ * java.text.NumberFormat}.
+ *
+ * Note that trailing format specifiers, specifiers that
+ * determine the type of a floating-point literal
+ * ({@code 1.0f} is a {@code float} value;
+ * {@code 1.0d} is a {@code double} value), do
+ * not influence the results of this method. In other
+ * words, the numerical value of the input string is converted
+ * directly to the target floating-point type. In general, the
+ * two-step sequence of conversions, string to {@code double}
+ * followed by {@code double} to {@code float}, is
+ * not equivalent to converting a string directly to
+ * {@code float}. For example, if first converted to an
+ * intermediate {@code double} and then to
+ * {@code float}, the string To avoid calling this method on an invalid string and having
+ * a {@code NumberFormatException} be thrown, the documentation
+ * for {@link Double#valueOf Double.valueOf} lists a regular
+ * expression which can be used to screen the input.
+ *
+ * @param s the string to be parsed.
+ * @return a {@code Float} object holding the value
+ * represented by the {@code String} argument.
+ * @throws NumberFormatException if the string does not contain a
+ * parsable number.
+ */
+ public static Float valueOf(String s) throws NumberFormatException {
+ return new Float(parseFloat(s));
+ }
+
+ /**
+ * Returns a {@code Float} instance representing the specified
+ * {@code float} value.
+ * If a new {@code Float} instance is not required, this method
+ * should generally be used in preference to the constructor
+ * {@link #Float(float)}, as this method is likely to yield
+ * significantly better space and time performance by caching
+ * frequently requested values.
+ *
+ * @param f a float value.
+ * @return a {@code Float} instance representing {@code f}.
+ * @since 1.5
+ */
+ public static Float valueOf(float f) {
+ return new Float(f);
+ }
+
+ /**
+ * Returns a new {@code float} initialized to the value
+ * represented by the specified {@code String}, as performed
+ * by the {@code valueOf} method of class {@code Float}.
+ *
+ * @param s the string to be parsed.
+ * @return the {@code float} value represented by the string
+ * argument.
+ * @throws NullPointerException if the string is null
+ * @throws NumberFormatException if the string does not contain a
+ * parsable {@code float}.
+ * @see java.lang.Float#valueOf(String)
+ * @since 1.2
+ */
+ public static float parseFloat(String s) throws NumberFormatException {
+ return CProver.nondetFloat(); //The function is handled by cbmc internally
+ }
+
+ /**
+ * Returns {@code true} if the specified number is a
+ * Not-a-Number (NaN) value, {@code false} otherwise.
+ *
+ * @param v the value to be tested.
+ * @return {@code true} if the argument is NaN;
+ * {@code false} otherwise.
+ */
+ public static boolean isNaN(float v) {
+ return (v != v);
+ }
+
+ /**
+ * Returns {@code true} if the specified number is infinitely
+ * large in magnitude, {@code false} otherwise.
+ *
+ * @param v the value to be tested.
+ * @return {@code true} if the argument is positive infinity or
+ * negative infinity; {@code false} otherwise.
+ */
+ public static boolean isInfinite(float v) {
+ return (v == POSITIVE_INFINITY) || (v == NEGATIVE_INFINITY);
+ }
+
+
+ /**
+ * Returns {@code true} if the argument is a finite floating-point
+ * value; returns {@code false} otherwise (for NaN and infinity
+ * arguments).
+ *
+ * @param f the {@code float} value to be tested
+ * @return {@code true} if the argument is a finite
+ * floating-point value, {@code false} otherwise.
+ * @since 1.8
+ */
+ public static boolean isFinite(float f) {
+ return FloatConsts.MIN_VALUE <= f && f <= FloatConsts.MAX_VALUE;
+ }
+
+ /**
+ * The value of the Float.
+ *
+ * @serial
+ */
+ private final float value;
+
+ /**
+ * Constructs a newly allocated {@code Float} object that
+ * represents the primitive {@code float} argument.
+ *
+ * @param value the value to be represented by the {@code Float}.
+ */
+ public Float(float value) {
+ this.value = value;
+ }
+
+ /**
+ * Constructs a newly allocated {@code Float} object that
+ * represents the argument converted to type {@code float}.
+ *
+ * @param value the value to be represented by the {@code Float}.
+ */
+ public Float(double value) {
+ this.value = (float)value;
+ }
+
+ /**
+ * Constructs a newly allocated {@code Float} object that
+ * represents the floating-point value of type {@code float}
+ * represented by the string. The string is converted to a
+ * {@code float} value as if by the {@code valueOf} method.
+ *
+ * @param s a string to be converted to a {@code Float}.
+ * @throws NumberFormatException if the string does not contain a
+ * parsable number.
+ * @see java.lang.Float#valueOf(java.lang.String)
+ */
+ public Float(String s) throws NumberFormatException {
+ value = parseFloat(s);
+ }
+
+ /**
+ * Returns {@code true} if this {@code Float} value is a
+ * Not-a-Number (NaN), {@code false} otherwise.
+ *
+ * @return {@code true} if the value represented by this object is
+ * NaN; {@code false} otherwise.
+ */
+ public boolean isNaN() {
+ return isNaN(value);
+ }
+
+ /**
+ * Returns {@code true} if this {@code Float} value is
+ * infinitely large in magnitude, {@code false} otherwise.
+ *
+ * @return {@code true} if the value represented by this object is
+ * positive infinity or negative infinity;
+ * {@code false} otherwise.
+ */
+ public boolean isInfinite() {
+ return isInfinite(value);
+ }
+
+ /**
+ * Returns a string representation of this {@code Float} object.
+ * The primitive {@code float} value represented by this object
+ * is converted to a {@code String} exactly as if by the method
+ * {@code toString} of one argument.
+ *
+ * @return a {@code String} representation of this object.
+ * @see java.lang.Float#toString(float)
+ */
+ public String toString() {
+ return Float.toString(value);
+ }
+
+ /**
+ * Returns the value of this {@code Float} as a {@code byte} after
+ * a narrowing primitive conversion.
+ *
+ * @return the {@code float} value represented by this object
+ * converted to type {@code byte}
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ */
+ public byte byteValue() {
+ return (byte)value;
+ }
+
+ /**
+ * Returns the value of this {@code Float} as a {@code short}
+ * after a narrowing primitive conversion.
+ *
+ * @return the {@code float} value represented by this object
+ * converted to type {@code short}
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ * @since JDK1.1
+ */
+ public short shortValue() {
+ return (short)value;
+ }
+
+ /**
+ * Returns the value of this {@code Float} as an {@code int} after
+ * a narrowing primitive conversion.
+ *
+ * @return the {@code float} value represented by this object
+ * converted to type {@code int}
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ */
+ public int intValue() {
+ return (int)value;
+ }
+
+ /**
+ * Returns value of this {@code Float} as a {@code long} after a
+ * narrowing primitive conversion.
+ *
+ * @return the {@code float} value represented by this object
+ * converted to type {@code long}
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ */
+ public long longValue() {
+ return (long)value;
+ }
+
+ /**
+ * Returns the {@code float} value of this {@code Float} object.
+ *
+ * @return the {@code float} value represented by this object
+ */
+ public float floatValue() {
+ return value;
+ }
+
+ /**
+ * Returns the value of this {@code Float} as a {@code double}
+ * after a widening primitive conversion.
+ *
+ * @return the {@code float} value represented by this
+ * object converted to type {@code double}
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public double doubleValue() {
+ return (double)value;
+ }
+
+ /**
+ * Returns a hash code for this {@code Float} object. The
+ * result is the integer bit representation, exactly as produced
+ * by the method {@link #floatToIntBits(float)}, of the primitive
+ * {@code float} value represented by this {@code Float}
+ * object.
+ *
+ * @return a hash code value for this object.
+ */
+ @Override
+ public int hashCode() {
+ // return Float.hashCode(value);
+ return 0;
+ }
+
+ /**
+ * Returns a hash code for a {@code float} value; compatible with
+ * {@code Float.hashCode()}.
+ *
+ * @param value the value to hash
+ * @return a hash code value for a {@code float} value.
+ * @since 1.8
+ */
+ public static int hashCode(float value) {
+ // return floatToIntBits(value);
+ return 0;
+ }
+
+ /**
+ * Compares this object against the specified object. The result
+ * is {@code true} if and only if the argument is not
+ * {@code null} and is a {@code Float} object that
+ * represents a {@code float} with the same value as the
+ * {@code float} represented by this object. For this
+ * purpose, two {@code float} values are considered to be the
+ * same if and only if the method {@link #floatToIntBits(float)}
+ * returns the identical {@code int} value when applied to
+ * each.
+ *
+ * Note that in most cases, for two instances of class
+ * {@code Float}, {@code f1} and {@code f2}, the value
+ * of {@code f1.equals(f2)} is {@code true} if and only if
+ *
+ * also has the value {@code true}. However, there are two exceptions:
+ * Bit 31 (the bit that is selected by the mask
+ * {@code 0x80000000}) represents the sign of the floating-point
+ * number.
+ * Bits 30-23 (the bits that are selected by the mask
+ * {@code 0x7f800000}) represent the exponent.
+ * Bits 22-0 (the bits that are selected by the mask
+ * {@code 0x007fffff}) represent the significand (sometimes called
+ * the mantissa) of the floating-point number.
+ *
+ * If the argument is positive infinity, the result is
+ * {@code 0x7f800000}.
+ *
+ * If the argument is negative infinity, the result is
+ * {@code 0xff800000}.
+ *
+ * If the argument is NaN, the result is {@code 0x7fc00000}.
+ *
+ * In all cases, the result is an integer that, when given to the
+ * {@link #intBitsToFloat(int)} method, will produce a floating-point
+ * value the same as the argument to {@code floatToIntBits}
+ * (except all NaN values are collapsed to a single
+ * "canonical" NaN value).
+ *
+ * @param value a floating-point number.
+ * @return the bits that represent the floating-point number.
+ */
+ public static int floatToIntBits(float value) {
+ int result = floatToRawIntBits(value);
+ // Check for NaN based on values of bit fields, maximum
+ // exponent and nonzero significand.
+ if ( ((result & FloatConsts.EXP_BIT_MASK) ==
+ FloatConsts.EXP_BIT_MASK) &&
+ (result & FloatConsts.SIGNIF_BIT_MASK) != 0)
+ result = 0x7fc00000;
+ return result;
+ }
+
+ /**
+ * Returns a representation of the specified floating-point value
+ * according to the IEEE 754 floating-point "single format" bit
+ * layout, preserving Not-a-Number (NaN) values.
+ *
+ * Bit 31 (the bit that is selected by the mask
+ * {@code 0x80000000}) represents the sign of the floating-point
+ * number.
+ * Bits 30-23 (the bits that are selected by the mask
+ * {@code 0x7f800000}) represent the exponent.
+ * Bits 22-0 (the bits that are selected by the mask
+ * {@code 0x007fffff}) represent the significand (sometimes called
+ * the mantissa) of the floating-point number.
+ *
+ * If the argument is positive infinity, the result is
+ * {@code 0x7f800000}.
+ *
+ * If the argument is negative infinity, the result is
+ * {@code 0xff800000}.
+ *
+ * If the argument is NaN, the result is the integer representing
+ * the actual NaN value. Unlike the {@code floatToIntBits}
+ * method, {@code floatToRawIntBits} does not collapse all the
+ * bit patterns encoding a NaN to a single "canonical"
+ * NaN value.
+ *
+ * In all cases, the result is an integer that, when given to the
+ * {@link #intBitsToFloat(int)} method, will produce a
+ * floating-point value the same as the argument to
+ * {@code floatToRawIntBits}.
+ *
+ * @param value a floating-point number.
+ * @return the bits that represent the floating-point number.
+ * @since 1.3
+ */
+ public static int floatToRawIntBits(float value){
+ //@TODO: implement this method internally in CBMC
+ return CProver.nondetInt();
+ }
+
+ /**
+ * Returns the {@code float} value corresponding to a given
+ * bit representation.
+ * The argument is considered to be a representation of a
+ * floating-point value according to the IEEE 754 floating-point
+ * "single format" bit layout.
+ *
+ * If the argument is {@code 0x7f800000}, the result is positive
+ * infinity.
+ *
+ * If the argument is {@code 0xff800000}, the result is negative
+ * infinity.
+ *
+ * If the argument is any value in the range
+ * {@code 0x7f800001} through {@code 0x7fffffff} or in
+ * the range {@code 0xff800001} through
+ * {@code 0xffffffff}, the result is a NaN. No IEEE 754
+ * floating-point operation provided by Java can distinguish
+ * between two NaN values of the same type with different bit
+ * patterns. Distinct values of NaN are only distinguishable by
+ * use of the {@code Float.floatToRawIntBits} method.
+ *
+ * In all other cases, let s, e, and m be three
+ * values that can be computed from the argument:
+ *
+ * Note that this method may not be able to return a
+ * {@code float} NaN with exactly same bit pattern as the
+ * {@code int} argument. IEEE 754 distinguishes between two
+ * kinds of NaNs, quiet NaNs and signaling NaNs. The
+ * differences between the two kinds of NaN are generally not
+ * visible in Java. Arithmetic operations on signaling NaNs turn
+ * them into quiet NaNs with a different, but often similar, bit
+ * pattern. However, on some processors merely copying a
+ * signaling NaN also performs that conversion. In particular,
+ * copying a signaling NaN to return it to the calling method may
+ * perform this conversion. So {@code intBitsToFloat} may
+ * not be able to return a {@code float} with a signaling NaN
+ * bit pattern. Consequently, for some {@code int} values,
+ * {@code floatToRawIntBits(intBitsToFloat(start))} may
+ * not equal {@code start}. Moreover, which
+ * particular bit patterns represent signaling NaNs is platform
+ * dependent; although all NaN bit patterns, quiet or signaling,
+ * must be in the NaN range identified above.
+ *
+ * @param bits an integer.
+ * @return the {@code float} floating-point value with the same bit
+ * pattern.
+ */
+ public static float intBitsToFloat(int bits){
+ //@TODO: implement this method internally in CBMC
+ return CProver.nondetFloat();
+ }
+
+ /**
+ * Compares two {@code Float} objects numerically. There are
+ * two ways in which comparisons performed by this method differ
+ * from those performed by the Java language numerical comparison
+ * operators ({@code <, <=, ==, >=, >}) when
+ * applied to primitive {@code float} values:
+ *
+ * In addition, this class provides several methods for converting
+ * a {@code long} to a {@code String} and a {@code String} to a {@code
+ * long}, as well as other constants and methods useful when dealing
+ * with a {@code long}.
+ *
+ * Implementation note: The implementations of the "bit twiddling"
+ * methods (such as {@link #highestOneBit(long) highestOneBit} and
+ * {@link #numberOfTrailingZeros(long) numberOfTrailingZeros}) are
+ * based on material from Henry S. Warren, Jr.'s Hacker's
+ * Delight, (Addison Wesley, 2002).
+ *
+ * @author Lee Boynton
+ * @author Arthur van Hoff
+ * @author Josh Bloch
+ * @author Joseph D. Darcy
+ * @since JDK1.0
+ */
+public final class Long extends Number implements Comparable If the radix is smaller than {@code Character.MIN_RADIX}
+ * or larger than {@code Character.MAX_RADIX}, then the radix
+ * {@code 10} is used instead.
+ *
+ * If the first argument is negative, the first element of the
+ * result is the ASCII minus sign {@code '-'}
+ * ({@code '\u005Cu002d'}). If the first argument is not
+ * negative, no sign character appears in the result.
+ *
+ * The remaining characters of the result represent the magnitude
+ * of the first argument. If the magnitude is zero, it is
+ * represented by a single zero character {@code '0'}
+ * ({@code '\u005Cu0030'}); otherwise, the first character of
+ * the representation of the magnitude will not be the zero
+ * character. The following ASCII characters are used as digits:
+ *
+ * If the radix is smaller than {@code Character.MIN_RADIX}
+ * or larger than {@code Character.MAX_RADIX}, then the radix
+ * {@code 10} is used instead.
+ *
+ * Note that since the first argument is treated as an unsigned
+ * value, no leading sign character is printed.
+ *
+ * If the magnitude is zero, it is represented by a single zero
+ * character {@code '0'} ({@code '\u005Cu0030'}); otherwise,
+ * the first character of the representation of the magnitude will
+ * not be the zero character.
+ *
+ * The behavior of radixes and the characters used as digits
+ * are the same as {@link #toString(long, int) toString}.
+ *
+ * @param i an integer to be converted to an unsigned string.
+ * @param radix the radix to use in the string representation.
+ * @return an unsigned string representation of the argument in the specified radix.
+ * @see #toString(long, int)
+ * @since 1.8
+ */
+ public static String toUnsignedString(long i, int radix) {
+ if (i >= 0)
+ return toString(i, radix);
+ else {
+ switch (radix) {
+ case 2:
+ return toBinaryString(i);
+
+ case 4:
+ return toUnsignedString0(i, 2);
+
+ case 8:
+ return toOctalString(i);
+
+ case 10:
+ /*
+ * We can get the effect of an unsigned division by 10
+ * on a long value by first shifting right, yielding a
+ * positive value, and then dividing by 5. This
+ * allows the last digit and preceding digits to be
+ * isolated more quickly than by an initial conversion
+ * to BigInteger.
+ */
+ long quot = (i >>> 1) / 5;
+ long rem = i - quot * 10;
+ return toString(quot) + rem;
+
+ case 16:
+ return toHexString(i);
+
+ case 32:
+ return toUnsignedString0(i, 5);
+
+ default:
+ return toUnsignedBigInteger(i).toString(radix);
+ }
+ }
+ }
+
+ /**
+ * Return a BigInteger equal to the unsigned value of the
+ * argument.
+ */
+ private static BigInteger toUnsignedBigInteger(long i) {
+ if (i >= 0L)
+ return BigInteger.valueOf(i);
+ else {
+ int upper = (int) (i >>> 32);
+ int lower = (int) i;
+
+ // return (upper << 32) + lower
+ return (BigInteger.valueOf(Integer.toUnsignedLong(upper))).shiftLeft(32).
+ add(BigInteger.valueOf(Integer.toUnsignedLong(lower)));
+ }
+ }
+
+ /**
+ * Returns a string representation of the {@code long}
+ * argument as an unsigned integer in base 16.
+ *
+ * The unsigned {@code long} value is the argument plus
+ * 264 if the argument is negative; otherwise, it is
+ * equal to the argument. This value is converted to a string of
+ * ASCII digits in hexadecimal (base 16) with no extra
+ * leading {@code 0}s.
+ *
+ * The value of the argument can be recovered from the returned
+ * string {@code s} by calling {@link
+ * Long#parseUnsignedLong(String, int) Long.parseUnsignedLong(s,
+ * 16)}.
+ *
+ * If the unsigned magnitude is zero, it is represented by a
+ * single zero character {@code '0'} ({@code '\u005Cu0030'});
+ * otherwise, the first character of the representation of the
+ * unsigned magnitude will not be the zero character. The
+ * following characters are used as hexadecimal digits:
+ *
+ * The unsigned {@code long} value is the argument plus
+ * 264 if the argument is negative; otherwise, it is
+ * equal to the argument. This value is converted to a string of
+ * ASCII digits in octal (base 8) with no extra leading
+ * {@code 0}s.
+ *
+ * The value of the argument can be recovered from the returned
+ * string {@code s} by calling {@link
+ * Long#parseUnsignedLong(String, int) Long.parseUnsignedLong(s,
+ * 8)}.
+ *
+ * If the unsigned magnitude is zero, it is represented by a
+ * single zero character {@code '0'} ({@code '\u005Cu0030'});
+ * otherwise, the first character of the representation of the
+ * unsigned magnitude will not be the zero character. The
+ * following characters are used as octal digits:
+ *
+ * The unsigned {@code long} value is the argument plus
+ * 264 if the argument is negative; otherwise, it is
+ * equal to the argument. This value is converted to a string of
+ * ASCII digits in binary (base 2) with no extra leading
+ * {@code 0}s.
+ *
+ * The value of the argument can be recovered from the returned
+ * string {@code s} by calling {@link
+ * Long#parseUnsignedLong(String, int) Long.parseUnsignedLong(s,
+ * 2)}.
+ *
+ * If the unsigned magnitude is zero, it is represented by a
+ * single zero character {@code '0'} ({@code '\u005Cu0030'});
+ * otherwise, the first character of the representation of the
+ * unsigned magnitude will not be the zero character. The
+ * characters {@code '0'} ({@code '\u005Cu0030'}) and {@code
+ * '1'} ({@code '\u005Cu0031'}) are used as binary digits.
+ *
+ * @param i a {@code long} to be converted to a string.
+ * @return the string representation of the unsigned {@code long}
+ * value represented by the argument in binary (base 2).
+ * @see #parseUnsignedLong(String, int)
+ * @see #toUnsignedString(long, int)
+ * @since JDK 1.0.2
+ */
+ public static String toBinaryString(long i) {
+ return toUnsignedString0(i, 1);
+ }
+
+ /**
+ * Format a long (treated as unsigned) into a String.
+ * @param val the value to format
+ * @param shift the log2 of the base to format in (4 for hex, 3 for octal, 1 for binary)
+ */
+ // DIFFBLUE MODEL LIBRARY: Handled internally by CBMC
+ static String toUnsignedString0(long val, int shift) {
+ CProver.assume(0 <= val && val <= Integer.MAX_VALUE);
+ return Integer.toString((int)val, 1 << shift);
+ }
+
+ /**
+ * Returns a {@code String} object representing the specified
+ * {@code long}. The argument is converted to signed decimal
+ * representation and returned as a string, exactly as if the
+ * argument and the radix 10 were given as arguments to the {@link
+ * #toString(long, int)} method.
+ *
+ * @param i a {@code long} to be converted.
+ * @return a string representation of the argument in base 10.
+ */
+ public static String toString(long i) {
+ // this function is handled by cbmc internally
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * Returns a string representation of the argument as an unsigned
+ * decimal value.
+ *
+ * The argument is converted to unsigned decimal representation
+ * and returned as a string exactly as if the argument and radix
+ * 10 were given as arguments to the {@link #toUnsignedString(long,
+ * int)} method.
+ *
+ * @param i an integer to be converted to an unsigned string.
+ * @return an unsigned string representation of the argument.
+ * @see #toUnsignedString(long, int)
+ * @since 1.8
+ */
+ public static String toUnsignedString(long i) {
+ return toUnsignedString(i, 10);
+ }
+
+ /**
+ * Places characters representing the integer i into the
+ * character array buf. The characters are placed into
+ * the buffer backwards starting with the least significant
+ * digit at the specified index (exclusive), and working
+ * backwards from there.
+ *
+ * Will fail if i == Long.MIN_VALUE
+ */
+
+ // Requires positive x
+ static int stringSize(long x) {
+ long p = 10;
+ for (int i=1; i<19; i++) {
+ if (x < p)
+ return i;
+ p = 10*p;
+ }
+ return 19;
+ }
+
+ /**
+ * Parses the string argument as a signed {@code long} in the
+ * radix specified by the second argument. The characters in the
+ * string must all be digits of the specified radix (as determined
+ * by whether {@link java.lang.Character#digit(char, int)} returns
+ * a nonnegative value), except that the first character may be an
+ * ASCII minus sign {@code '-'} ({@code '\u005Cu002D'}) to
+ * indicate a negative value or an ASCII plus sign {@code '+'}
+ * ({@code '\u005Cu002B'}) to indicate a positive value. The
+ * resulting {@code long} value is returned.
+ *
+ * Note that neither the character {@code L}
+ * ({@code '\u005Cu004C'}) nor {@code l}
+ * ({@code '\u005Cu006C'}) is permitted to appear at the end
+ * of the string as a type indicator, as would be permitted in
+ * Java programming language source code - except that either
+ * {@code L} or {@code l} may appear as a digit for a
+ * radix greater than or equal to 22.
+ *
+ * An exception of type {@code NumberFormatException} is
+ * thrown if any of the following situations occurs:
+ * Examples:
+ * Note that neither the character {@code L}
+ * ({@code '\u005Cu004C'}) nor {@code l}
+ * ({@code '\u005Cu006C'}) is permitted to appear at the end
+ * of the string as a type indicator, as would be permitted in
+ * Java programming language source code.
+ *
+ * @param s a {@code String} containing the {@code long}
+ * representation to be parsed
+ * @return the {@code long} represented by the argument in
+ * decimal.
+ * @throws NumberFormatException if the string does not contain a
+ * parsable {@code long}.
+ */
+ public static long parseLong(String s) throws NumberFormatException {
+ return CProver.nondetLong(); //The function is handled by cbmc internally
+ }
+
+ /**
+ * Parses the string argument as an unsigned {@code long} in the
+ * radix specified by the second argument. An unsigned integer
+ * maps the values usually associated with negative numbers to
+ * positive numbers larger than {@code MAX_VALUE}.
+ *
+ * The characters in the string must all be digits of the
+ * specified radix (as determined by whether {@link
+ * java.lang.Character#digit(char, int)} returns a nonnegative
+ * value), except that the first character may be an ASCII plus
+ * sign {@code '+'} ({@code '\u005Cu002B'}). The resulting
+ * integer value is returned.
+ *
+ * An exception of type {@code NumberFormatException} is
+ * thrown if any of the following situations occurs:
+ * In other words, this method returns a {@code Long} object equal
+ * to the value of:
+ *
+ * In other words, this method returns a {@code Long} object
+ * equal to the value of:
+ *
+ * The sequence of characters following an optional
+ * sign and/or radix specifier ("{@code 0x}", "{@code 0X}",
+ * "{@code #}", or leading zero) is parsed as by the {@code
+ * Long.parseLong} method with the indicated radix (10, 16, or 8).
+ * This sequence of characters must represent a positive value or
+ * a {@link NumberFormatException} will be thrown. The result is
+ * negated if first character of the specified {@code String} is
+ * the minus sign. No whitespace characters are permitted in the
+ * {@code String}.
+ *
+ * @param nm the {@code String} to decode.
+ * @return a {@code Long} object holding the {@code long}
+ * value represented by {@code nm}
+ * @throws NumberFormatException if the {@code String} does not
+ * contain a parsable {@code long}.
+ * @see java.lang.Long#parseLong(String, int)
+ * @since 1.2
+ */
+ public static Long decode(String nm) throws NumberFormatException {
+ int radix = 10;
+ int index = 0;
+ boolean negative = false;
+ Long result;
+
+ if (nm.length() == 0)
+ throw new NumberFormatException("Zero length string");
+ char firstChar = CProverString.charAt(nm, 0);
+ // Handle sign, if present
+ if (firstChar == '-') {
+ negative = true;
+ index++;
+ } else if (firstChar == '+')
+ index++;
+
+ // Handle radix specifier, if present
+ if (nm.startsWith("0x", index) || nm.startsWith("0X", index)) {
+ index += 2;
+ radix = 16;
+ }
+ else if (nm.startsWith("#", index)) {
+ index ++;
+ radix = 16;
+ }
+ else if (nm.startsWith("0", index) && nm.length() > 1 + index) {
+ index ++;
+ radix = 8;
+ }
+
+ if (nm.startsWith("-", index) || nm.startsWith("+", index))
+ throw new NumberFormatException("Sign character in wrong position");
+
+ // DIFFBLUE MODEL LIBRARY we compute the sub index only once
+ String nm_sub_index = CProverString.substring(nm, index);
+ try {
+ // DIFFBLUE MODEL LIBRARY
+ // result = Long.valueOf(nm.substring(index), radix);
+ result = Long.valueOf(nm_sub_index, radix);
+ result = negative ? Long.valueOf(-result.longValue()) : result;
+ } catch (NumberFormatException e) {
+ // If number is Long.MIN_VALUE, we'll end up here. The next line
+ // handles this case, and causes any genuine format error to be
+ // rethrown.
+ // DIFFBLUE MODEL LIBRARY
+ // String constant = negative ? ("-" + nm_sub_index)
+ // : nm.substring(index);
+ String constant = negative ? ("-" + nm_sub_index)
+ : nm_sub_index;
+ result = Long.valueOf(constant, radix);
+ }
+ return result;
+ }
+
+ /**
+ * The value of the {@code Long}.
+ *
+ * @serial
+ */
+ private final long value;
+
+ /**
+ * Constructs a newly allocated {@code Long} object that
+ * represents the specified {@code long} argument.
+ *
+ * @param value the value to be represented by the
+ * {@code Long} object.
+ */
+ public Long(long value) {
+ this.value = value;
+ }
+
+ /**
+ * Constructs a newly allocated {@code Long} object that
+ * represents the {@code long} value indicated by the
+ * {@code String} parameter. The string is converted to a
+ * {@code long} value in exactly the manner used by the
+ * {@code parseLong} method for radix 10.
+ *
+ * @param s the {@code String} to be converted to a
+ * {@code Long}.
+ * @throws NumberFormatException if the {@code String} does not
+ * contain a parsable {@code long}.
+ * @see java.lang.Long#parseLong(java.lang.String, int)
+ */
+ public Long(String s) throws NumberFormatException {
+ this.value = parseLong(s, 10);
+ }
+
+ /**
+ * Returns the value of this {@code Long} as a {@code byte} after
+ * a narrowing primitive conversion.
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ */
+ public byte byteValue() {
+ return (byte)value;
+ }
+
+ /**
+ * Returns the value of this {@code Long} as a {@code short} after
+ * a narrowing primitive conversion.
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ */
+ public short shortValue() {
+ return (short)value;
+ }
+
+ /**
+ * Returns the value of this {@code Long} as an {@code int} after
+ * a narrowing primitive conversion.
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ */
+ public int intValue() {
+ return (int)value;
+ }
+
+ /**
+ * Returns the value of this {@code Long} as a
+ * {@code long} value.
+ */
+ public long longValue() {
+ return value;
+ }
+
+ /**
+ * Returns the value of this {@code Long} as a {@code float} after
+ * a widening primitive conversion.
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public float floatValue() {
+ return (float)value;
+ }
+
+ /**
+ * Returns the value of this {@code Long} as a {@code double}
+ * after a widening primitive conversion.
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public double doubleValue() {
+ return (double)value;
+ }
+
+ /**
+ * Returns a {@code String} object representing this
+ * {@code Long}'s value. The value is converted to signed
+ * decimal representation and returned as a string, exactly as if
+ * the {@code long} value were given as an argument to the
+ * {@link java.lang.Long#toString(long)} method.
+ *
+ * @return a string representation of the value of this object in
+ * base 10.
+ */
+ public String toString() {
+ return toString(value);
+ }
+
+ /**
+ * Returns a hash code for this {@code Long}. The result is
+ * the exclusive OR of the two halves of the primitive
+ * {@code long} value held by this {@code Long}
+ * object. That is, the hashcode is the value of the expression:
+ *
+ * The first argument is treated as the name of a system
+ * property. System properties are accessible through the {@link
+ * java.lang.System#getProperty(java.lang.String)} method. The
+ * string value of this property is then interpreted as a {@code
+ * long} value using the grammar supported by {@link Long#decode decode}
+ * and a {@code Long} object representing this value is returned.
+ *
+ * If there is no property with the specified name, if the
+ * specified name is empty or {@code null}, or if the property
+ * does not have the correct numeric format, then {@code null} is
+ * returned.
+ *
+ * In other words, this method returns a {@code Long} object
+ * equal to the value of:
+ *
+ * The first argument is treated as the name of a system
+ * property. System properties are accessible through the {@link
+ * java.lang.System#getProperty(java.lang.String)} method. The
+ * string value of this property is then interpreted as a {@code
+ * long} value using the grammar supported by {@link Long#decode decode}
+ * and a {@code Long} object representing this value is returned.
+ *
+ * The second argument is the default value. A {@code Long} object
+ * that represents the value of the second argument is returned if there
+ * is no property of the specified name, if the property does not have
+ * the correct numeric format, or if the specified name is empty or null.
+ *
+ * In other words, this method returns a {@code Long} object equal
+ * to the value of:
+ *
+ * Note that, in every case, neither {@code L}
+ * ({@code '\u005Cu004C'}) nor {@code l}
+ * ({@code '\u005Cu006C'}) is permitted to appear at the end
+ * of the property value as a type indicator, as would be
+ * permitted in Java programming language source code.
+ *
+ * The second argument is the default value. The default value is
+ * returned if there is no property of the specified name, if the
+ * property does not have the correct numeric format, or if the
+ * specified name is empty or {@code null}.
+ *
+ * @param nm property name.
+ * @param val default value.
+ * @return the {@code Long} value of the property.
+ * @throws SecurityException for the same reasons as
+ * {@link System#getProperty(String) System.getProperty}
+ * @see System#getProperty(java.lang.String)
+ * @see System#getProperty(java.lang.String, java.lang.String)
+ */
+ public static Long getLong(String nm, Long val) {
+ String v = null;
+ try {
+ v = System.getProperty(nm);
+ } catch (IllegalArgumentException | NullPointerException e) {
+ }
+ if (v != null) {
+ try {
+ return Long.decode(v);
+ } catch (NumberFormatException e) {
+ }
+ }
+ return val;
+ }
+
+ /**
+ * Compares two {@code Long} objects numerically.
+ *
+ * @param anotherLong the {@code Long} to be compared.
+ * @return the value {@code 0} if this {@code Long} is
+ * equal to the argument {@code Long}; a value less than
+ * {@code 0} if this {@code Long} is numerically less
+ * than the argument {@code Long}; and a value greater
+ * than {@code 0} if this {@code Long} is numerically
+ * greater than the argument {@code Long} (signed
+ * comparison).
+ * @since 1.2
+ */
+ public int compareTo(Long anotherLong) {
+ return compare(this.value, anotherLong.value);
+ }
+
+ /**
+ * Compares two {@code long} values numerically.
+ * The value returned is identical to what would be returned by:
+ * Note that in two's complement arithmetic, the three other
+ * basic arithmetic operations of add, subtract, and multiply are
+ * bit-wise identical if the two operands are regarded as both
+ * being signed or both being unsigned. Therefore separate {@code
+ * addUnsigned}, etc. methods are not provided.
+ *
+ * @param dividend the value to be divided
+ * @param divisor the value doing the dividing
+ * @return the unsigned quotient of the first argument divided by
+ * the second argument
+ * @see #remainderUnsigned
+ * @since 1.8
+ */
+ public static long divideUnsigned(long dividend, long divisor) {
+ if (divisor < 0L) { // signed comparison
+ // Answer must be 0 or 1 depending on relative magnitude
+ // of dividend and divisor.
+ return (compareUnsigned(dividend, divisor)) < 0 ? 0L :1L;
+ }
+
+ if (dividend > 0) // Both inputs non-negative
+ return dividend/divisor;
+ else {
+ /*
+ * For simple code, leveraging BigInteger. Longer and faster
+ * code written directly in terms of operations on longs is
+ * possible; see "Hacker's Delight" for divide and remainder
+ * algorithms.
+ */
+ return toUnsignedBigInteger(dividend).
+ divide(toUnsignedBigInteger(divisor)).longValue();
+ }
+ }
+
+ /**
+ * Returns the unsigned remainder from dividing the first argument
+ * by the second where each argument and the result is interpreted
+ * as an unsigned value.
+ *
+ * @param dividend the value to be divided
+ * @param divisor the value doing the dividing
+ * @return the unsigned remainder of the first argument divided by
+ * the second argument
+ * @see #divideUnsigned
+ * @since 1.8
+ */
+ public static long remainderUnsigned(long dividend, long divisor) {
+ if (dividend > 0 && divisor > 0) { // signed comparisons
+ return dividend % divisor;
+ } else {
+ if (compareUnsigned(dividend, divisor) < 0) // Avoid explicit check for 0 divisor
+ return dividend;
+ else
+ return toUnsignedBigInteger(dividend).
+ remainder(toUnsignedBigInteger(divisor)).longValue();
+ }
+ }
+
+ // Bit Twiddling
+
+ /**
+ * The number of bits used to represent a {@code long} value in two's
+ * complement binary form.
+ *
+ * @since 1.5
+ */
+ @Native public static final int SIZE = 64;
+
+ /**
+ * The number of bytes used to represent a {@code long} value in two's
+ * complement binary form.
+ *
+ * @since 1.8
+ */
+ public static final int BYTES = SIZE / Byte.SIZE;
+
+ /**
+ * Returns a {@code long} value with at most a single one-bit, in the
+ * position of the highest-order ("leftmost") one-bit in the specified
+ * {@code long} value. Returns zero if the specified value has no
+ * one-bits in its two's complement binary representation, that is, if it
+ * is equal to zero.
+ *
+ * @param i the value whose highest one bit is to be computed
+ * @return a {@code long} value with a single one-bit, in the position
+ * of the highest-order one-bit in the specified value, or zero if
+ * the specified value is itself equal to zero.
+ * @since 1.5
+ */
+ public static long highestOneBit(long i) {
+ // HD, Figure 3-1
+ i |= (i >> 1);
+ i |= (i >> 2);
+ i |= (i >> 4);
+ i |= (i >> 8);
+ i |= (i >> 16);
+ i |= (i >> 32);
+ return i - (i >>> 1);
+ }
+
+ /**
+ * Returns a {@code long} value with at most a single one-bit, in the
+ * position of the lowest-order ("rightmost") one-bit in the specified
+ * {@code long} value. Returns zero if the specified value has no
+ * one-bits in its two's complement binary representation, that is, if it
+ * is equal to zero.
+ *
+ * @param i the value whose lowest one bit is to be computed
+ * @return a {@code long} value with a single one-bit, in the position
+ * of the lowest-order one-bit in the specified value, or zero if
+ * the specified value is itself equal to zero.
+ * @since 1.5
+ */
+ public static long lowestOneBit(long i) {
+ // HD, Section 2-1
+ return i & -i;
+ }
+
+ /**
+ * Returns the number of zero bits preceding the highest-order
+ * ("leftmost") one-bit in the two's complement binary representation
+ * of the specified {@code long} value. Returns 64 if the
+ * specified value has no one-bits in its two's complement representation,
+ * in other words if it is equal to zero.
+ *
+ * Note that this method is closely related to the logarithm base 2.
+ * For all positive {@code long} values x:
+ * Note that left rotation with a negative distance is equivalent to
+ * right rotation: {@code rotateLeft(val, -distance) == rotateRight(val,
+ * distance)}. Note also that rotation by any multiple of 64 is a
+ * no-op, so all but the last six bits of the rotation distance can be
+ * ignored, even if the distance is negative: {@code rotateLeft(val,
+ * distance) == rotateLeft(val, distance & 0x3F)}.
+ *
+ * @param i the value whose bits are to be rotated left
+ * @param distance the number of bit positions to rotate left
+ * @return the value obtained by rotating the two's complement binary
+ * representation of the specified {@code long} value left by the
+ * specified number of bits.
+ * @since 1.5
+ */
+ public static long rotateLeft(long i, int distance) {
+ return (i << distance) | (i >>> -distance);
+ }
+
+ /**
+ * Returns the value obtained by rotating the two's complement binary
+ * representation of the specified {@code long} value right by the
+ * specified number of bits. (Bits shifted out of the right hand, or
+ * low-order, side reenter on the left, or high-order.)
+ *
+ * Note that right rotation with a negative distance is equivalent to
+ * left rotation: {@code rotateRight(val, -distance) == rotateLeft(val,
+ * distance)}. Note also that rotation by any multiple of 64 is a
+ * no-op, so all but the last six bits of the rotation distance can be
+ * ignored, even if the distance is negative: {@code rotateRight(val,
+ * distance) == rotateRight(val, distance & 0x3F)}.
+ *
+ * @param i the value whose bits are to be rotated right
+ * @param distance the number of bit positions to rotate right
+ * @return the value obtained by rotating the two's complement binary
+ * representation of the specified {@code long} value right by the
+ * specified number of bits.
+ * @since 1.5
+ */
+ public static long rotateRight(long i, int distance) {
+ return (i >>> distance) | (i << -distance);
+ }
+
+ /**
+ * Returns the value obtained by reversing the order of the bits in the
+ * two's complement binary representation of the specified {@code long}
+ * value.
+ *
+ * @param i the value to be reversed
+ * @return the value obtained by reversing order of the bits in the
+ * specified {@code long} value.
+ * @since 1.5
+ */
+ public static long reverse(long i) {
+ // HD, Figure 7-1
+ i = (i & 0x5555555555555555L) << 1 | (i >>> 1) & 0x5555555555555555L;
+ i = (i & 0x3333333333333333L) << 2 | (i >>> 2) & 0x3333333333333333L;
+ i = (i & 0x0f0f0f0f0f0f0f0fL) << 4 | (i >>> 4) & 0x0f0f0f0f0f0f0f0fL;
+ i = (i & 0x00ff00ff00ff00ffL) << 8 | (i >>> 8) & 0x00ff00ff00ff00ffL;
+ i = (i << 48) | ((i & 0xffff0000L) << 16) |
+ ((i >>> 16) & 0xffff0000L) | (i >>> 48);
+ return i;
+ }
+
+ /**
+ * Returns the signum function of the specified {@code long} value. (The
+ * return value is -1 if the specified value is negative; 0 if the
+ * specified value is zero; and 1 if the specified value is positive.)
+ *
+ * @param i the value whose signum is to be computed
+ * @return the signum function of the specified {@code long} value.
+ * @since 1.5
+ */
+ public static int signum(long i) {
+ // HD, Section 2-7
+ return (int) ((i >> 63) | (-i >>> 63));
+ }
+
+ /**
+ * Returns the value obtained by reversing the order of the bytes in the
+ * two's complement representation of the specified {@code long} value.
+ *
+ * @param i the value whose bytes are to be reversed
+ * @return the value obtained by reversing the bytes in the specified
+ * {@code long} value.
+ * @since 1.5
+ */
+ public static long reverseBytes(long i) {
+ i = (i & 0x00ff00ff00ff00ffL) << 8 | (i >>> 8) & 0x00ff00ff00ff00ffL;
+ return (i << 48) | ((i & 0xffff0000L) << 16) |
+ ((i >>> 16) & 0xffff0000L) | (i >>> 48);
+ }
+
+ /**
+ * Adds two {@code long} values together as per the + operator.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the sum of {@code a} and {@code b}
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static long sum(long a, long b) {
+ return a + b;
+ }
+
+ /**
+ * Returns the greater of two {@code long} values
+ * as if by calling {@link Math#max(long, long) Math.max}.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the greater of {@code a} and {@code b}
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static long max(long a, long b) {
+ long result = CProver.nondetLong();
+ CProver.assume((result == a || result == b) && result >= a && result >= b);
+ return result;
+ }
+
+ /**
+ * Returns the smaller of two {@code long} values
+ * as if by calling {@link Math#min(long, long) Math.min}.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the smaller of {@code a} and {@code b}
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static long min(long a, long b) {
+ long result = CProver.nondetLong();
+ CProver.assume((result == a || result == b) && result <= a && result <= b);
+ return result;
+ }
+
+ /** use serialVersionUID from JDK 1.0.2 for interoperability */
+ @Native private static final long serialVersionUID = 4290774380558885855L;
+}
diff --git a/src/main/java/java/lang/Math.java b/src/main/java/java/lang/Math.java
index 1779ff3..9c214af 100644
--- a/src/main/java/java/lang/Math.java
+++ b/src/main/java/java/lang/Math.java
@@ -245,11 +245,11 @@ public static double atan(double a) {
* @return the measurement of the angle {@code angdeg}
* in radians.
* @since 1.2
+ *
+ * @diffblue.fullSupport
*/
public static double toRadians(double angdeg) {
- CProver.notModelled();
- return CProver.nondetDouble();
- // return angdeg / 180.0 * PI;
+ return angdeg / 180.0 * PI;
}
/**
@@ -358,15 +358,48 @@ public static double log10(double a) {
* @param a a value.
* @return the positive square root of {@code a}.
* If the argument is NaN or less than zero, the result is NaN.
+ *
+ * @diffblue.limitedSupport
+ * This implementation using solver constraints only works if squaring the
+ * result of sqrt is equal to the original number, which is not always
+ * true. As a result, the solver will return UNSAT in many cases.
+ * For instance, {@code Math.sqrt(2.0)} will cause the solver to be UNSAT.
+ * Reported in: TG-5598
+ *
+ * Also, there are precision issues on very small numbers. For instance,
+ * for values between 0 and {@code 0x0.0000000000001p-900}, the sqrt method
+ * is likely to not be equal to the result of the real Math.sqrt method.
+ * Reported in: TG-5602
*/
public static double sqrt(double a) {
- CProver.notModelled();
- return CProver.nondetDouble();
// return StrictMath.sqrt(a); // default impl. delegates to StrictMath
// Note that hardware sqrt instructions
// frequently can be directly used by JITs
// and should be much faster than doing
// Math.sqrt in software.
+ if (Double.isNaN(a) || a < 0.0) {
+ return Double.NaN;
+ }
+ if (a == Double.POSITIVE_INFINITY || a == 0.0) {
+ return a;
+ }
+ double sqrt = CProver.nondetDouble();
+ CProver.assume(sqrt >= 0);
+ CProver.assume(sqrt * sqrt == a);
+
+ // To solve the satisfiability issue, we should adapt the constraints
+ // to something like:
+ //
+ // double reMultiplied = sqrt * sqrt;
+ // CProver.assume(reMultiplied > lower);
+ // CProver.assume(reMultiplied <= upper);
+ //
+ // Where lower and upper only differ by one bit in their
+ // representation, which should ensure that they are the double values
+ // that are the closest to reMultiplied.
+ // This implementation cannot be done yet because it would require
+ // Double.doubleToRawLongBits() to be supported.
+ return sqrt;
}
@@ -1270,11 +1303,12 @@ public static long floorMod(long x, long y) {
*
* @param a the argument whose absolute value is to be determined
* @return the absolute value of the argument.
+ *
+ * @diffblue.fullSupport
+ * @diffblue.untested
*/
public static int abs(int a) {
- CProver.notModelled();
- return CProver.nondetInt();
- // return (a < 0) ? -a : a;
+ return (a < 0) ? -a : a;
}
/**
@@ -1289,11 +1323,12 @@ public static int abs(int a) {
*
* @param a the argument whose absolute value is to be determined
* @return the absolute value of the argument.
+ *
+ * @diffblue.fullSupport
+ * @diffblue.untested
*/
public static long abs(long a) {
- CProver.notModelled();
- return CProver.nondetLong();
- // return (a < 0) ? -a : a;
+ return (a < 0) ? -a : a;
}
/**
@@ -1310,11 +1345,11 @@ public static long abs(long a) {
*
* @param a the argument whose absolute value is to be determined
* @return the absolute value of the argument.
+ *
+ * @diffblue.fullSupport
*/
public static float abs(float a) {
- CProver.notModelled();
- return CProver.nondetFloat();
- // return (a <= 0.0F) ? 0.0F - a : a;
+ return (a <= 0.0F) ? 0.0F - a : a;
}
/**
@@ -1331,11 +1366,11 @@ public static float abs(float a) {
*
* @param a the argument whose absolute value is to be determined
* @return the absolute value of the argument.
+ *
+ * @diffblue.fullSupport
*/
public static double abs(double a) {
- CProver.notModelled();
- return CProver.nondetDouble();
- // return (a <= 0.0D) ? 0.0D - a : a;
+ return (a <= 0.0D) ? 0.0D - a : a;
}
/**
@@ -1664,11 +1699,15 @@ public static float ulp(float f) {
* @return the signum function of the argument
* @author Joseph D. Darcy
* @since 1.5
+ *
+ * @diffblue.fullSupport
*/
public static double signum(double d) {
- CProver.notModelled();
- return CProver.nondetDouble();
// return (d == 0.0 || Double.isNaN(d))?d:copySign(1.0, d);
+ if (d == 0 || Double.isNaN(d)) {
+ return d;
+ }
+ return d > 0.0 ? 1.0 : -1.0;
}
/**
@@ -1687,11 +1726,16 @@ public static double signum(double d) {
* @return the signum function of the argument
* @author Joseph D. Darcy
* @since 1.5
+ *
+ * @diffblue.fullSupport
+ * @diffblue.untested
*/
public static float signum(float f) {
- CProver.notModelled();
- return CProver.nondetFloat();
// return (f == 0.0f || Float.isNaN(f))?f:copySign(1.0f, f);
+ if (f == 0 || Float.isNaN(f)) {
+ return f;
+ }
+ return f > 0.0f ? 1.0f : -1.0f;
}
/**
diff --git a/src/main/java/java/lang/Number.java b/src/main/java/java/lang/Number.java
new file mode 100644
index 0000000..d901609
--- /dev/null
+++ b/src/main/java/java/lang/Number.java
@@ -0,0 +1,124 @@
+/*
+ * Copyright (c) 1994, 2011, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.lang;
+
+/**
+ * The abstract class {@code Number} is the superclass of platform
+ * classes representing numeric values that are convertible to the
+ * primitive types {@code byte}, {@code double}, {@code float}, {@code
+ * int}, {@code long}, and {@code short}.
+ *
+ * The specific semantics of the conversion from the numeric value of
+ * a particular {@code Number} implementation to a given primitive
+ * type is defined by the {@code Number} implementation in question.
+ *
+ * For platform classes, the conversion is often analogous to a
+ * narrowing primitive conversion or a widening primitive conversion
+ * as defining in The Java™ Language Specification
+ * for converting between primitive types. Therefore, conversions may
+ * lose information about the overall magnitude of a numeric value, may
+ * lose precision, and may even return a result of a different sign
+ * than the input.
+ *
+ * See the documentation of a given {@code Number} implementation for
+ * conversion details.
+ *
+ * @author Lee Boynton
+ * @author Arthur van Hoff
+ * @jls 5.1.2 Widening Primitive Conversions
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ * @since JDK1.0
+ */
+public abstract class Number implements java.io.Serializable {
+ /**
+ * Returns the value of the specified number as an {@code int},
+ * which may involve rounding or truncation.
+ *
+ * @return the numeric value represented by this object after conversion
+ * to type {@code int}.
+ */
+ public abstract int intValue();
+
+ /**
+ * Returns the value of the specified number as a {@code long},
+ * which may involve rounding or truncation.
+ *
+ * @return the numeric value represented by this object after conversion
+ * to type {@code long}.
+ */
+ public abstract long longValue();
+
+ /**
+ * Returns the value of the specified number as a {@code float},
+ * which may involve rounding.
+ *
+ * @return the numeric value represented by this object after conversion
+ * to type {@code float}.
+ */
+ public abstract float floatValue();
+
+ /**
+ * Returns the value of the specified number as a {@code double},
+ * which may involve rounding.
+ *
+ * @return the numeric value represented by this object after conversion
+ * to type {@code double}.
+ */
+ public abstract double doubleValue();
+
+ /**
+ * Returns the value of the specified number as a {@code byte},
+ * which may involve rounding or truncation.
+ *
+ * This implementation returns the result of {@link #intValue} cast
+ * to a {@code byte}.
+ *
+ * @return the numeric value represented by this object after conversion
+ * to type {@code byte}.
+ * @since JDK1.1
+ */
+ public byte byteValue() {
+ return (byte)intValue();
+ }
+
+ /**
+ * Returns the value of the specified number as a {@code short},
+ * which may involve rounding or truncation.
+ *
+ * This implementation returns the result of {@link #intValue} cast
+ * to a {@code short}.
+ *
+ * @return the numeric value represented by this object after conversion
+ * to type {@code short}.
+ * @since JDK1.1
+ */
+ public short shortValue() {
+ return (short)intValue();
+ }
+
+ /** use serialVersionUID from JDK 1.0.2 for interoperability */
+ private static final long serialVersionUID = -8742448824652078965L;
+}
diff --git a/src/main/java/java/lang/Object.java b/src/main/java/java/lang/Object.java
index ba9bf63..dfe9363 100644
--- a/src/main/java/java/lang/Object.java
+++ b/src/main/java/java/lang/Object.java
@@ -31,7 +31,7 @@
public class Object {
- // lock needed for synchronization in cbmc
+ // lock needed for synchronization in JBMC
// used by monitorenter, monitorexit, wait, and notify
// Not present in the original Object class
public int cproverMonitorCount;
@@ -40,6 +40,13 @@ public Object() {
cproverMonitorCount = 0;
}
+ /**
+ * @diffblue.limitedSupport
+ * This relies on Class.forName whose model is only partial. The model of
+ * Class is made to work for combinations of calls to Object.getClass,
+ * Class.forName and Class.getName but other operations are unlikely to
+ * work.
+ */
public final Class> getClass() {
// DIFFBLUE MODEL LIBRARY
return Class.forName(CProver.classIdentifier(this));
@@ -61,20 +68,17 @@ public String toString() {
return getClass().getName() + "@" + Integer.toHexString(hashCode());
}
- public final void notify()
- {
- // FIXME: the thread must own the lock when it calls notify
+ public final void notify() {
+ // TODO: the thread must own the lock when it calls notify
}
- // See implementation of notify
- public final void notifyAll()
- {
- // FIXME: the thread must own the lock when it calls notifyAll
+ public final void notifyAll() {
+ // TODO: the thread must own the lock when it calls notifyAll
}
public final void wait(long timeout) throws InterruptedException {
- // FIXME: the thread must own the lock when it calls wait
- // FIXME: should only throw if the interrupted flag in Thread is enabled
+ // TODO: the thread must own the lock when it calls wait
+ // should only throw if the interrupted flag in Thread is enabled
throw new InterruptedException();
}
@@ -112,8 +116,8 @@ protected void finalize() throws Throwable { }
*/
public static void monitorenter(Object object)
{
- //FIXME: we shoud remove the call to this method from the call
- // stack appended to the thrown exception
+ // TODO: we shoud remove the call to this method from the call
+ // stack appended to the thrown exception
if (object == null)
throw new NullPointerException();
@@ -135,19 +139,17 @@ public static void monitorenter(Object object)
*/
public static void monitorexit(Object object)
{
- //FIXME: we shoud remove the call to this method from the call
- // stack appended to the thrown exception
- // FIXME: Enabling these exceptions makes
- // jbmc-regression/synchronized-blocks/test_sync.desc
- // run into an infinite loop during symex
+ // TODO: we shoud remove the call to this method from the call
+ // stack appended to the thrown exception
+ // TODO: Enabling these exceptions makes
+ // jbmc/synchronized-blocks/test_sync.desc
+ // run into an infinite loop during symex
// if (object == null)
// throw new NullPointerException();
-
// if (object.cproverMonitorCount == 0)
// throw new IllegalMonitorStateException();
CProver.atomicBegin();
object.cproverMonitorCount--;
CProver.atomicEnd();
}
-
}
diff --git a/src/main/java/java/lang/Short.java b/src/main/java/java/lang/Short.java
new file mode 100644
index 0000000..a4a700d
--- /dev/null
+++ b/src/main/java/java/lang/Short.java
@@ -0,0 +1,522 @@
+/*
+ * Copyright (c) 1996, 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.lang;
+
+import org.cprover.CProver;
+
+/**
+ * The {@code Short} class wraps a value of primitive type {@code
+ * short} in an object. An object of type {@code Short} contains a
+ * single field whose type is {@code short}.
+ *
+ * In addition, this class provides several methods for converting
+ * a {@code short} to a {@code String} and a {@code String} to a
+ * {@code short}, as well as other constants and methods useful when
+ * dealing with a {@code short}.
+ *
+ * @author Nakul Saraiya
+ * @author Joseph D. Darcy
+ * @see java.lang.Number
+ * @since JDK1.1
+ */
+public final class Short extends Number implements Comparable An exception of type {@code NumberFormatException} is
+ * thrown if any of the following situations occurs:
+ * In other words, this method returns a {@code Short} object
+ * equal to the value of:
+ *
+ * In other words, this method returns a {@code Short} object
+ * equal to the value of:
+ *
+ * The sequence of characters following an optional
+ * sign and/or radix specifier ("{@code 0x}", "{@code 0X}",
+ * "{@code #}", or leading zero) is parsed as by the {@code
+ * Short.parseShort} method with the indicated radix (10, 16, or
+ * 8). This sequence of characters must represent a positive
+ * value or a {@link NumberFormatException} will be thrown. The
+ * result is negated if first character of the specified {@code
+ * String} is the minus sign. No whitespace characters are
+ * permitted in the {@code String}.
+ *
+ * @param nm the {@code String} to decode.
+ * @return a {@code Short} object holding the {@code short}
+ * value represented by {@code nm}
+ * @throws NumberFormatException if the {@code String} does not
+ * contain a parsable {@code short}.
+ * @see java.lang.Short#parseShort(java.lang.String, int)
+ */
+ public static Short decode(String nm) throws NumberFormatException {
+ int i = Integer.decode(nm);
+ if (i < MIN_VALUE || i > MAX_VALUE)
+ throw new NumberFormatException(
+ "Value " + i + " out of range from input " + nm);
+ return valueOf((short)i);
+ }
+
+ /**
+ * The value of the {@code Short}.
+ *
+ * @serial
+ */
+ private final short value;
+
+ /**
+ * Constructs a newly allocated {@code Short} object that
+ * represents the specified {@code short} value.
+ *
+ * @param value the value to be represented by the
+ * {@code Short}.
+ */
+ public Short(short value) {
+ this.value = value;
+ }
+
+ /**
+ * Constructs a newly allocated {@code Short} object that
+ * represents the {@code short} value indicated by the
+ * {@code String} parameter. The string is converted to a
+ * {@code short} value in exactly the manner used by the
+ * {@code parseShort} method for radix 10.
+ *
+ * @param s the {@code String} to be converted to a
+ * {@code Short}
+ * @throws NumberFormatException If the {@code String}
+ * does not contain a parsable {@code short}.
+ * @see java.lang.Short#parseShort(java.lang.String, int)
+ */
+ public Short(String s) throws NumberFormatException {
+ this.value = parseShort(s, 10);
+ }
+
+ /**
+ * Returns the value of this {@code Short} as a {@code byte} after
+ * a narrowing primitive conversion.
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ */
+ public byte byteValue() {
+ return (byte)value;
+ }
+
+ /**
+ * Returns the value of this {@code Short} as a
+ * {@code short}.
+ */
+ public short shortValue() {
+ return value;
+ }
+
+ /**
+ * Returns the value of this {@code Short} as an {@code int} after
+ * a widening primitive conversion.
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public int intValue() {
+ return (int)value;
+ }
+
+ /**
+ * Returns the value of this {@code Short} as a {@code long} after
+ * a widening primitive conversion.
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public long longValue() {
+ return (long)value;
+ }
+
+ /**
+ * Returns the value of this {@code Short} as a {@code float}
+ * after a widening primitive conversion.
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public float floatValue() {
+ return (float)value;
+ }
+
+ /**
+ * Returns the value of this {@code Short} as a {@code double}
+ * after a widening primitive conversion.
+ * @jls 5.1.2 Widening Primitive Conversions
+ */
+ public double doubleValue() {
+ return (double)value;
+ }
+
+ /**
+ * Returns a {@code String} object representing this
+ * {@code Short}'s value. The value is converted to signed
+ * decimal representation and returned as a string, exactly as if
+ * the {@code short} value were given as an argument to the
+ * {@link java.lang.Short#toString(short)} method.
+ *
+ * @return a string representation of the value of this object in
+ * base 10.
+ */
+ public String toString() {
+ return Integer.toString((int)value);
+ }
+
+ /**
+ * Returns a hash code for this {@code Short}; equal to the result
+ * of invoking {@code intValue()}.
+ *
+ * @return a hash code value for this {@code Short}
+ */
+ @Override
+ public int hashCode() {
+ return Short.hashCode(value);
+ }
+
+ /**
+ * Returns a hash code for a {@code short} value; compatible with
+ * {@code Short.hashCode()}.
+ *
+ * @param value the value to hash
+ * @return a hash code value for a {@code short} value.
+ * @since 1.8
+ */
+ public static int hashCode(short value) {
+ return (int)value;
+ }
+
+ /**
+ * Compares this object to the specified object. The result is
+ * {@code true} if and only if the argument is not
+ * {@code null} and is a {@code Short} object that
+ * contains the same {@code short} value as this object.
+ *
+ * @param obj the object to compare with
+ * @return {@code true} if the objects are the same;
+ * {@code false} otherwise.
+ */
+ public boolean equals(Object obj) {
+ if (obj instanceof Short) {
+ return value == ((Short)obj).shortValue();
+ }
+ return false;
+ }
+
+ /**
+ * Compares two {@code Short} objects numerically.
+ *
+ * @param anotherShort the {@code Short} to be compared.
+ * @return the value {@code 0} if this {@code Short} is
+ * equal to the argument {@code Short}; a value less than
+ * {@code 0} if this {@code Short} is numerically less
+ * than the argument {@code Short}; and a value greater than
+ * {@code 0} if this {@code Short} is numerically
+ * greater than the argument {@code Short} (signed
+ * comparison).
+ * @since 1.2
+ */
+ public int compareTo(Short anotherShort) {
+ return compare(this.value, anotherShort.value);
+ }
+
+ /**
+ * Compares two {@code short} values numerically.
+ * The value returned is identical to what would be returned by:
+ * Setting the {@code accessible} flag in a reflected object
+ * permits sophisticated applications with sufficient privilege, such
+ * as Java Object Serialization or other persistence mechanisms, to
+ * manipulate objects in a manner that would normally be prohibited.
+ *
+ * By default, a reflected object is not accessible.
+ *
+ * @see Field
+ * @see Method
+ * @see Constructor
+ * @see ReflectPermission
+ *
+ * @since 1.2
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ * This model was automatically generated by the JDK Processor tool.
+ */
+public class AccessibleObject implements AnnotatedElement {
+
+ /**
+ * The Permission object that is used to check whether a client
+ * has sufficient privilege to defeat Java language access
+ * control checks.
+ */
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // static final private java.security.Permission ACCESS_PERMISSION =
+ // new ReflectPermission("suppressAccessChecks");
+
+ /**
+ * Convenience method to set the {@code accessible} flag for an
+ * array of objects with a single security check (for efficiency).
+ *
+ * First, if there is a security manager, its
+ * {@code checkPermission} method is called with a
+ * {@code ReflectPermission("suppressAccessChecks")} permission.
+ *
+ * A {@code SecurityException} is raised if {@code flag} is
+ * {@code true} but accessibility of any of the elements of the input
+ * {@code array} may not be changed (for example, if the element
+ * object is a {@link Constructor} object for the class {@link
+ * java.lang.Class}). In the event of such a SecurityException, the
+ * accessibility of objects is set to {@code flag} for array elements
+ * upto (and excluding) the element for which the exception occurred; the
+ * accessibility of elements beyond (and including) the element for which
+ * the exception occurred is unchanged.
+ *
+ * @param array the array of AccessibleObjects
+ * @param flag the new value for the {@code accessible} flag
+ * in each object
+ * @throws SecurityException if the request is denied.
+ * @see SecurityManager#checkPermission
+ * @see java.lang.RuntimePermission
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public static void setAccessible(AccessibleObject[] array, boolean flag)
+ throws SecurityException {
+ // SecurityManager sm = System.getSecurityManager();
+ // if (sm != null) sm.checkPermission(ACCESS_PERMISSION);
+ // for (int i = 0; i < array.length; i++) {
+ // setAccessible0(array[i], flag);
+ // }
+ CProver.notModelled();
+ }
+
+ /**
+ * Set the {@code accessible} flag for this object to
+ * the indicated boolean value. A value of {@code true} indicates that
+ * the reflected object should suppress Java language access
+ * checking when it is used. A value of {@code false} indicates
+ * that the reflected object should enforce Java language access checks.
+ *
+ * First, if there is a security manager, its
+ * {@code checkPermission} method is called with a
+ * {@code ReflectPermission("suppressAccessChecks")} permission.
+ *
+ * A {@code SecurityException} is raised if {@code flag} is
+ * {@code true} but accessibility of this object may not be changed
+ * (for example, if this element object is a {@link Constructor} object for
+ * the class {@link java.lang.Class}).
+ *
+ * A {@code SecurityException} is raised if this object is a {@link
+ * java.lang.reflect.Constructor} object for the class
+ * {@code java.lang.Class}, and {@code flag} is true.
+ *
+ * @param flag the new value for the {@code accessible} flag
+ * @throws SecurityException if the request is denied.
+ * @see SecurityManager#checkPermission
+ * @see java.lang.RuntimePermission
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public void setAccessible(boolean flag) throws SecurityException {
+ // SecurityManager sm = System.getSecurityManager();
+ // if (sm != null) sm.checkPermission(ACCESS_PERMISSION);
+ // setAccessible0(this, flag);
+ CProver.notModelled();
+ }
+
+ /* Check that you aren't exposing java.lang.Class. If a formal parameter type is a parameterized type,
+ * the {@code Type} object returned for it must accurately reflect
+ * the actual type parameters used in the source code.
+ *
+ * If a formal parameter type is a type variable or a parameterized
+ * type, it is created. Otherwise, it is resolved.
+ *
+ * @return an array of {@code Type}s that represent the formal
+ * parameter types of the underlying executable, in declaration order
+ * @throws GenericSignatureFormatError
+ * if the generic method signature does not conform to the format
+ * specified in
+ * The Java™ Virtual Machine Specification
+ * @throws TypeNotPresentException if any of the parameter
+ * types of the underlying executable refers to a non-existent type
+ * declaration
+ * @throws MalformedParameterizedTypeException if any of
+ * the underlying executable's parameter types refer to a parameterized
+ * type that cannot be instantiated for any reason
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public Type[] getGenericParameterTypes() {
+ // if (hasGenericInformation())
+ // return getGenericInfo().getParameterTypes();
+ // else
+ // return getParameterTypes();
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * Behaves like {@code getGenericParameterTypes}, but returns type
+ * information for all parameters, including synthetic parameters.
+ */
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // Type[] getAllGenericParameterTypes() {
+ // final boolean genericInfo = hasGenericInformation();
+
+ // // Easy case: we don't have generic parameter information. In
+ // // this case, we just return the result of
+ // // getParameterTypes().
+ // if (!genericInfo) {
+ // return getParameterTypes();
+ // } else {
+ // final boolean realParamData = hasRealParameterData();
+ // final Type[] genericParamTypes = getGenericParameterTypes();
+ // final Type[] nonGenericParamTypes = getParameterTypes();
+ // final Type[] out = new Type[nonGenericParamTypes.length];
+ // final Parameter[] params = getParameters();
+ // int fromidx = 0;
+ // // If we have real parameter data, then we use the
+ // // synthetic and mandate flags to our advantage.
+ // if (realParamData) {
+ // for (int i = 0; i < out.length; i++) {
+ // final Parameter param = params[i];
+ // if (param.isSynthetic() || param.isImplicit()) {
+ // // If we hit a synthetic or mandated parameter,
+ // // use the non generic parameter info.
+ // out[i] = nonGenericParamTypes[i];
+ // } else {
+ // // Otherwise, use the generic parameter info.
+ // out[i] = genericParamTypes[fromidx];
+ // fromidx++;
+ // }
+ // }
+ // } else {
+ // // Otherwise, use the non-generic parameter data.
+ // // Without method parameter reflection data, we have
+ // // no way to figure out which parameters are
+ // // synthetic/mandated, thus, no way to match up the
+ // // indexes.
+ // return genericParamTypes.length == nonGenericParamTypes.length ?
+ // genericParamTypes : nonGenericParamTypes;
+ // }
+ // return out;
+ // }
+ // }
+
+ /**
+ * Returns an array of {@code Parameter} objects that represent
+ * all the parameters to the underlying executable represented by
+ * this object. Returns an array of length 0 if the executable
+ * has no parameters.
+ *
+ * The parameters of the underlying executable do not necessarily
+ * have unique names, or names that are legal identifiers in the
+ * Java programming language (JLS 3.8).
+ *
+ * @throws MalformedParametersException if the class file contains
+ * a MethodParameters attribute that is improperly formatted.
+ * @return an array of {@code Parameter} objects representing all
+ * the parameters to the executable this object represents.
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public Parameter[] getParameters() {
+ // // TODO: This may eventually need to be guarded by security
+ // // mechanisms similar to those in Field, Method, etc.
+ // //
+ // // Need to copy the cached array to prevent users from messing
+ // // with it. Since parameters are immutable, we can
+ // // shallow-copy.
+ // return privateGetParameters().clone();
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private Parameter[] synthesizeAllParams() {
+ // final int realparams = getParameterCount();
+ // final Parameter[] out = new Parameter[realparams];
+ // for (int i = 0; i < realparams; i++)
+ // // TODO: is there a way to synthetically derive the
+ // // modifiers? Probably not in the general case, since
+ // // we'd have no way of knowing about them, but there
+ // // may be specific cases.
+ // out[i] = new Parameter("arg" + i, 0, this, i);
+ // return out;
+ // }
+
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private void verifyParameters(final Parameter[] parameters) {
+ // final int mask = Modifier.FINAL | Modifier.SYNTHETIC | Modifier.MANDATED;
+
+ // if (getParameterTypes().length != parameters.length)
+ // throw new MalformedParametersException("Wrong number of parameters in MethodParameters attribute");
+
+ // for (Parameter parameter : parameters) {
+ // final String name = parameter.getRealName();
+ // final int mods = parameter.getModifiers();
+
+ // if (name != null) {
+ // if (name.isEmpty() || name.indexOf('.') != -1 ||
+ // name.indexOf(';') != -1 || name.indexOf('[') != -1 ||
+ // name.indexOf('/') != -1) {
+ // throw new MalformedParametersException("Invalid parameter name \"" + name + "\"");
+ // }
+ // }
+
+ // if (mods != (mods & mask)) {
+ // throw new MalformedParametersException("Invalid parameter modifiers");
+ // }
+ // }
+ // }
+
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private Parameter[] privateGetParameters() {
+ // // Use tmp to avoid multiple writes to a volatile.
+ // Parameter[] tmp = parameters;
+
+ // if (tmp == null) {
+
+ // // Otherwise, go to the JVM to get them
+ // try {
+ // tmp = getParameters0();
+ // } catch(IllegalArgumentException e) {
+ // // Rethrow ClassFormatErrors
+ // throw new MalformedParametersException("Invalid constant pool index");
+ // }
+
+ // // If we get back nothing, then synthesize parameters
+ // if (tmp == null) {
+ // hasRealParameterData = false;
+ // tmp = synthesizeAllParams();
+ // } else {
+ // hasRealParameterData = true;
+ // verifyParameters(tmp);
+ // }
+
+ // parameters = tmp;
+ // }
+
+ // return tmp;
+ // }
+
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // boolean hasRealParameterData() {
+ // // If this somehow gets called before parameters gets
+ // // initialized, force it into existence.
+ // if (parameters == null) {
+ // privateGetParameters();
+ // }
+ // return hasRealParameterData;
+ // }
+
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private transient volatile boolean hasRealParameterData;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private transient volatile Parameter[] parameters;
+
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private native Parameter[] getParameters0();
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // native byte[] getTypeAnnotationBytes0();
+
+ // Needed by reflectaccess
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // byte[] getTypeAnnotationBytes() {
+ // return getTypeAnnotationBytes0();
+ // }
+
+ /**
+ * Returns an array of {@code Class} objects that represent the
+ * types of exceptions declared to be thrown by the underlying
+ * executable represented by this object. Returns an array of
+ * length 0 if the executable declares no exceptions in its {@code
+ * throws} clause.
+ *
+ * @return the exception types declared as being thrown by the
+ * executable this object represents
+ */
+ public abstract Class>[] getExceptionTypes();
+
+ /**
+ * Returns an array of {@code Type} objects that represent the
+ * exceptions declared to be thrown by this executable object.
+ * Returns an array of length 0 if the underlying executable declares
+ * no exceptions in its {@code throws} clause.
+ *
+ * If an exception type is a type variable or a parameterized
+ * type, it is created. Otherwise, it is resolved.
+ *
+ * @return an array of Types that represent the exception types
+ * thrown by the underlying executable
+ * @throws GenericSignatureFormatError
+ * if the generic method signature does not conform to the format
+ * specified in
+ * The Java™ Virtual Machine Specification
+ * @throws TypeNotPresentException if the underlying executable's
+ * {@code throws} clause refers to a non-existent type declaration
+ * @throws MalformedParameterizedTypeException if
+ * the underlying executable's {@code throws} clause refers to a
+ * parameterized type that cannot be instantiated for any reason
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public Type[] getGenericExceptionTypes() {
+ // Type[] result;
+ // if (hasGenericInformation() &&
+ // ((result = getGenericInfo().getExceptionTypes()).length > 0))
+ // return result;
+ // else
+ // return getExceptionTypes();
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * Returns a string describing this {@code Executable}, including
+ * any type parameters.
+ * @return a string describing this {@code Executable}, including
+ * any type parameters
+ */
+ public abstract String toGenericString();
+
+ /**
+ * Returns {@code true} if this executable was declared to take a
+ * variable number of arguments; returns {@code false} otherwise.
+ *
+ * @return {@code true} if an only if this executable was declared
+ * to take a variable number of arguments.
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public boolean isVarArgs() {
+ // return (getModifiers() & Modifier.VARARGS) != 0;
+ CProver.notModelled();
+ return CProver.nondetBoolean();
+ }
+
+ /**
+ * Returns {@code true} if this executable is a synthetic
+ * construct; returns {@code false} otherwise.
+ *
+ * @return true if and only if this executable is a synthetic
+ * construct as defined by
+ * The Java™ Language Specification.
+ * @jls 13.1 The Form of a Binary
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public boolean isSynthetic() {
+ // return Modifier.isSynthetic(getModifiers());
+ CProver.notModelled();
+ return CProver.nondetBoolean();
+ }
+
+ /**
+ * Returns an array of arrays of {@code Annotation}s that
+ * represent the annotations on the formal parameters, in
+ * declaration order, of the {@code Executable} represented by
+ * this object. Synthetic and mandated parameters (see
+ * explanation below), such as the outer "this" parameter to an
+ * inner class constructor will be represented in the returned
+ * array. If the executable has no parameters (meaning no formal,
+ * no synthetic, and no mandated parameters), a zero-length array
+ * will be returned. If the {@code Executable} has one or more
+ * parameters, a nested array of length zero is returned for each
+ * parameter with no annotations. The annotation objects contained
+ * in the returned arrays are serializable. The caller of this
+ * method is free to modify the returned arrays; it will have no
+ * effect on the arrays returned to other callers.
+ *
+ * A compiler may add extra parameters that are implicitly
+ * declared in source ("mandated"), as well as parameters that
+ * are neither implicitly nor explicitly declared in source
+ * ("synthetic") to the parameter list for a method. See {@link
+ * java.lang.reflect.Parameter} for more information.
+ *
+ * @see java.lang.reflect.Parameter
+ * @see java.lang.reflect.Parameter#getAnnotations
+ * @return an array of arrays that represent the annotations on
+ * the formal and implicit parameters, in declaration order, of
+ * the executable represented by this object
+ */
+ public abstract Annotation[][] getParameterAnnotations();
+
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // Annotation[][] sharedGetParameterAnnotations(Class>[] parameterTypes,
+ // byte[] parameterAnnotations) {
+ // int numParameters = parameterTypes.length;
+ // if (parameterAnnotations == null)
+ // return new Annotation[numParameters][0];
+
+ // Annotation[][] result = parseParameterAnnotations(parameterAnnotations);
+
+ // if (result.length != numParameters)
+ // handleParameterNumberMismatch(result.length, numParameters);
+ // return result;
+ // }
+
+ abstract void handleParameterNumberMismatch(int resultLength, int numParameters);
+
+ /**
+ * {@inheritDoc}
+ * @throws NullPointerException {@inheritDoc}
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public A {@code Field} permits widening conversions to occur during a get or
+ * set access operation, but throws an {@code IllegalArgumentException} if a
+ * narrowing conversion would occur.
+ *
+ * @see Member
+ * @see java.lang.Class
+ * @see java.lang.Class#getFields()
+ * @see java.lang.Class#getField(String)
+ * @see java.lang.Class#getDeclaredFields()
+ * @see java.lang.Class#getDeclaredField(String)
+ *
+ * @author Kenneth Russell
+ * @author Nakul Saraiya
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ * This model was automatically generated by the JDK Processor tool.
+ */
+public final
+class Field extends AccessibleObject implements Member {
+
+ private Class> clazz;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private int slot;
+ // This is guaranteed to be interned by the VM in the 1.4
+ // reflection implementation
+ private String name;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private Class> type;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private int modifiers;
+ // Generics and annotations support
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private transient String signature;
+ // generic info repository; lazily initialized
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private transient FieldRepository genericInfo;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private byte[] annotations;
+ // Cached field accessor created without override
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private FieldAccessor fieldAccessor;
+ // Cached field accessor created with override
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private FieldAccessor overrideFieldAccessor;
+ // For sharing of FieldAccessors. This branching structure is
+ // currently only two levels deep (i.e., one root Field and
+ // potentially many Field objects pointing to it.)
+ //
+ // If this branching structure would ever contain cycles, deadlocks can
+ // occur in annotation code.
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private Field root;
+
+ // Generics infrastructure
+
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private String getGenericSignature() {return signature;}
+
+ // Accessor for factory
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private GenericsFactory getFactory() {
+ // Class> c = getDeclaringClass();
+ // // create scope and factory
+ // return CoreReflectionFactory.make(c, ClassScope.make(c));
+ // }
+
+ // Accessor for generic info repository
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private FieldRepository getGenericInfo() {
+ // // lazily initialize repository if necessary
+ // if (genericInfo == null) {
+ // // create and cache generic info repository
+ // genericInfo = FieldRepository.make(getGenericSignature(),
+ // getFactory());
+ // }
+ // return genericInfo; //return cached repository
+ // }
+
+
+ /**
+ * Package-private constructor used by ReflectAccess to enable
+ * instantiation of these objects in Java code from the java.lang
+ * package via sun.reflect.LangReflectAccess.
+ */
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // Field(Class> declaringClass,
+ // String name,
+ // Class> type,
+ // int modifiers,
+ // int slot,
+ // String signature,
+ // byte[] annotations)
+ // {
+ // this.clazz = declaringClass;
+ // this.name = name;
+ // this.type = type;
+ // this.modifiers = modifiers;
+ // this.slot = slot;
+ // this.signature = signature;
+ // this.annotations = annotations;
+ // }
+
+ /**
+ * This constructor does not exist in the JDK, only in the model
+ */
+ public Field(
+ Class> declaringClass,
+ String name)
+ {
+ this.clazz = declaringClass;
+ this.name = name;
+ }
+
+ /**
+ * Package-private routine (exposed to java.lang.Class via
+ * ReflectAccess) which returns a copy of this Field. The copy's
+ * "root" field points to this Field.
+ */
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // Field copy() {
+ // // This routine enables sharing of FieldAccessor objects
+ // // among Field objects which refer to the same underlying
+ // // method in the VM. (All of this contortion is only necessary
+ // // because of the "accessibility" bit in AccessibleObject,
+ // // which implicitly requires that new java.lang.reflect
+ // // objects be fabricated for each reflective call on Class
+ // // objects.)
+ // if (this.root != null)
+ // throw new IllegalArgumentException("Can not copy a non-root Field");
+
+ // Field res = new Field(clazz, name, type, modifiers, slot, signature, annotations);
+ // res.root = this;
+ // // Might as well eagerly propagate this if already present
+ // res.fieldAccessor = fieldAccessor;
+ // res.overrideFieldAccessor = overrideFieldAccessor;
+
+ // return res;
+ // }
+
+ /**
+ * Returns the {@code Class} object representing the class or interface
+ * that declares the field represented by this {@code Field} object.
+ *
+ * @diffblue.fullSupport
+ */
+ public Class> getDeclaringClass() {
+ return clazz;
+ }
+
+ /**
+ * Returns the name of the field represented by this {@code Field} object.
+ *
+ * @diffblue.fullSupport
+ */
+ public String getName() {
+ return name;
+ }
+
+ /**
+ * Returns the Java language modifiers for the field represented
+ * by this {@code Field} object, as an integer. The {@code Modifier} class should
+ * be used to decode the modifiers.
+ *
+ * @see Modifier
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public int getModifiers() {
+ // return modifiers;
+ CProver.notModelled();
+ return CProver.nondetInt();
+ }
+
+ /**
+ * Returns {@code true} if this field represents an element of
+ * an enumerated type; returns {@code false} otherwise.
+ *
+ * @return {@code true} if and only if this field represents an element of
+ * an enumerated type.
+ * @since 1.5
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public boolean isEnumConstant() {
+ // return (getModifiers() & Modifier.ENUM) != 0;
+ CProver.notModelled();
+ return CProver.nondetBoolean();
+ }
+
+ /**
+ * Returns {@code true} if this field is a synthetic
+ * field; returns {@code false} otherwise.
+ *
+ * @return true if and only if this field is a synthetic
+ * field as defined by the Java Language Specification.
+ * @since 1.5
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public boolean isSynthetic() {
+ // return Modifier.isSynthetic(getModifiers());
+ CProver.notModelled();
+ return CProver.nondetBoolean();
+ }
+
+ /**
+ * Returns a {@code Class} object that identifies the
+ * declared type for the field represented by this
+ * {@code Field} object.
+ *
+ * @return a {@code Class} object identifying the declared
+ * type of the field represented by this object
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public Class> getType() {
+ // return type;
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * Returns a {@code Type} object that represents the declared type for
+ * the field represented by this {@code Field} object.
+ *
+ * If the {@code Type} is a parameterized type, the
+ * {@code Type} object returned must accurately reflect the
+ * actual type parameters used in the source code.
+ *
+ * If the type of the underlying field is a type variable or a
+ * parameterized type, it is created. Otherwise, it is resolved.
+ *
+ * @return a {@code Type} object that represents the declared type for
+ * the field represented by this {@code Field} object
+ * @throws GenericSignatureFormatError if the generic field
+ * signature does not conform to the format specified in
+ * The Java™ Virtual Machine Specification
+ * @throws TypeNotPresentException if the generic type
+ * signature of the underlying field refers to a non-existent
+ * type declaration
+ * @throws MalformedParameterizedTypeException if the generic
+ * signature of the underlying field refers to a parameterized type
+ * that cannot be instantiated for any reason
+ * @since 1.5
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public Type getGenericType() {
+ // if (getGenericSignature() != null)
+ // return getGenericInfo().getGenericType();
+ // else
+ // return getType();
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+
+ /**
+ * Compares this {@code Field} against the specified object. Returns
+ * true if the objects are the same. Two {@code Field} objects are the same if
+ * they were declared by the same class and have the same name
+ * and type.
+ *
+ * @diffblue.limitedSupport
+ */
+ public boolean equals(Object obj) {
+ if (obj != null && obj instanceof Field) {
+ Field other = (Field)obj;
+ return (getDeclaringClass() == other.getDeclaringClass())
+ && (getName() == other.getName());
+ }
+ return false;
+ }
+
+ /**
+ * Returns a hashcode for this {@code Field}. This is computed as the
+ * exclusive-or of the hashcodes for the underlying field's
+ * declaring class name and its name.
+ *
+ * @diffblue.untested
+ * @diffblue.fullSupport
+ */
+ public int hashCode() {
+ return getDeclaringClass().getName().hashCode() ^ getName().hashCode();
+ }
+
+ /**
+ * Returns a string describing this {@code Field}. The format is
+ * the access modifiers for the field, if any, followed
+ * by the field type, followed by a space, followed by
+ * the fully-qualified name of the class declaring the field,
+ * followed by a period, followed by the name of the field.
+ * For example:
+ * The modifiers are placed in canonical order as specified by
+ * "The Java Language Specification". This is {@code public},
+ * {@code protected} or {@code private} first, and then other
+ * modifiers in the following order: {@code static}, {@code final},
+ * {@code transient}, {@code volatile}.
+ *
+ * @return a string describing this {@code Field}
+ * @jls 8.3.1 Field Modifiers
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public String toString() {
+ // int mod = getModifiers();
+ // return (((mod == 0) ? "" : (Modifier.toString(mod) + " "))
+ // + getType().getTypeName() + " "
+ // + getDeclaringClass().getTypeName() + "."
+ // + getName());
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * Returns a string describing this {@code Field}, including
+ * its generic type. The format is the access modifiers for the
+ * field, if any, followed by the generic field type, followed by
+ * a space, followed by the fully-qualified name of the class
+ * declaring the field, followed by a period, followed by the name
+ * of the field.
+ *
+ * The modifiers are placed in canonical order as specified by
+ * "The Java Language Specification". This is {@code public},
+ * {@code protected} or {@code private} first, and then other
+ * modifiers in the following order: {@code static}, {@code final},
+ * {@code transient}, {@code volatile}.
+ *
+ * @return a string describing this {@code Field}, including
+ * its generic type
+ *
+ * @since 1.5
+ * @jls 8.3.1 Field Modifiers
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public String toGenericString() {
+ // int mod = getModifiers();
+ // Type fieldType = getGenericType();
+ // return (((mod == 0) ? "" : (Modifier.toString(mod) + " "))
+ // + fieldType.getTypeName() + " "
+ // + getDeclaringClass().getTypeName() + "."
+ // + getName());
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * Returns the value of the field represented by this {@code Field}, on
+ * the specified object. The value is automatically wrapped in an
+ * object if it has a primitive type.
+ *
+ * The underlying field's value is obtained as follows:
+ *
+ * If the underlying field is a static field, the {@code obj} argument
+ * is ignored; it may be null.
+ *
+ * Otherwise, the underlying field is an instance field. If the
+ * specified {@code obj} argument is null, the method throws a
+ * {@code NullPointerException}. If the specified object is not an
+ * instance of the class or interface declaring the underlying
+ * field, the method throws an {@code IllegalArgumentException}.
+ *
+ * If this {@code Field} object is enforcing Java language access control, and
+ * the underlying field is inaccessible, the method throws an
+ * {@code IllegalAccessException}.
+ * If the underlying field is static, the class that declared the
+ * field is initialized if it has not already been initialized.
+ *
+ * Otherwise, the value is retrieved from the underlying instance
+ * or static field. If the field has a primitive type, the value
+ * is wrapped in an object before being returned, otherwise it is
+ * returned as is.
+ *
+ * If the field is hidden in the type of {@code obj},
+ * the field's value is obtained according to the preceding rules.
+ *
+ * @param obj object from which the represented field's value is
+ * to be extracted
+ * @return the value of the represented field in object
+ * {@code obj}; primitive values are wrapped in an appropriate
+ * object before being returned
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is inaccessible.
+ * @exception IllegalArgumentException if the specified object is not an
+ * instance of the class or interface declaring the underlying
+ * field (or a subclass or implementor thereof).
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public Object get(Object obj)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // return getFieldAccessor(obj).get(obj);
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * Gets the value of a static or instance {@code boolean} field.
+ *
+ * @param obj the object to extract the {@code boolean} value
+ * from
+ * @return the value of the {@code boolean} field
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is inaccessible.
+ * @exception IllegalArgumentException if the specified object is not
+ * an instance of the class or interface declaring the
+ * underlying field (or a subclass or implementor
+ * thereof), or if the field value cannot be
+ * converted to the type {@code boolean} by a
+ * widening conversion.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#get
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public boolean getBoolean(Object obj)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // return getFieldAccessor(obj).getBoolean(obj);
+ CProver.notModelled();
+ return CProver.nondetBoolean();
+ }
+
+ /**
+ * Gets the value of a static or instance {@code byte} field.
+ *
+ * @param obj the object to extract the {@code byte} value
+ * from
+ * @return the value of the {@code byte} field
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is inaccessible.
+ * @exception IllegalArgumentException if the specified object is not
+ * an instance of the class or interface declaring the
+ * underlying field (or a subclass or implementor
+ * thereof), or if the field value cannot be
+ * converted to the type {@code byte} by a
+ * widening conversion.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#get
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public byte getByte(Object obj)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // return getFieldAccessor(obj).getByte(obj);
+ CProver.notModelled();
+ return CProver.nondetByte();
+ }
+
+ /**
+ * Gets the value of a static or instance field of type
+ * {@code char} or of another primitive type convertible to
+ * type {@code char} via a widening conversion.
+ *
+ * @param obj the object to extract the {@code char} value
+ * from
+ * @return the value of the field converted to type {@code char}
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is inaccessible.
+ * @exception IllegalArgumentException if the specified object is not
+ * an instance of the class or interface declaring the
+ * underlying field (or a subclass or implementor
+ * thereof), or if the field value cannot be
+ * converted to the type {@code char} by a
+ * widening conversion.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#get
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public char getChar(Object obj)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // return getFieldAccessor(obj).getChar(obj);
+ CProver.notModelled();
+ return CProver.nondetChar();
+ }
+
+ /**
+ * Gets the value of a static or instance field of type
+ * {@code short} or of another primitive type convertible to
+ * type {@code short} via a widening conversion.
+ *
+ * @param obj the object to extract the {@code short} value
+ * from
+ * @return the value of the field converted to type {@code short}
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is inaccessible.
+ * @exception IllegalArgumentException if the specified object is not
+ * an instance of the class or interface declaring the
+ * underlying field (or a subclass or implementor
+ * thereof), or if the field value cannot be
+ * converted to the type {@code short} by a
+ * widening conversion.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#get
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public short getShort(Object obj)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // return getFieldAccessor(obj).getShort(obj);
+ CProver.notModelled();
+ return CProver.nondetShort();
+ }
+
+ /**
+ * Gets the value of a static or instance field of type
+ * {@code int} or of another primitive type convertible to
+ * type {@code int} via a widening conversion.
+ *
+ * @param obj the object to extract the {@code int} value
+ * from
+ * @return the value of the field converted to type {@code int}
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is inaccessible.
+ * @exception IllegalArgumentException if the specified object is not
+ * an instance of the class or interface declaring the
+ * underlying field (or a subclass or implementor
+ * thereof), or if the field value cannot be
+ * converted to the type {@code int} by a
+ * widening conversion.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#get
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public int getInt(Object obj)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // return getFieldAccessor(obj).getInt(obj);
+ CProver.notModelled();
+ return CProver.nondetInt();
+ }
+
+ /**
+ * Gets the value of a static or instance field of type
+ * {@code long} or of another primitive type convertible to
+ * type {@code long} via a widening conversion.
+ *
+ * @param obj the object to extract the {@code long} value
+ * from
+ * @return the value of the field converted to type {@code long}
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is inaccessible.
+ * @exception IllegalArgumentException if the specified object is not
+ * an instance of the class or interface declaring the
+ * underlying field (or a subclass or implementor
+ * thereof), or if the field value cannot be
+ * converted to the type {@code long} by a
+ * widening conversion.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#get
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public long getLong(Object obj)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // return getFieldAccessor(obj).getLong(obj);
+ CProver.notModelled();
+ return CProver.nondetLong();
+ }
+
+ /**
+ * Gets the value of a static or instance field of type
+ * {@code float} or of another primitive type convertible to
+ * type {@code float} via a widening conversion.
+ *
+ * @param obj the object to extract the {@code float} value
+ * from
+ * @return the value of the field converted to type {@code float}
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is inaccessible.
+ * @exception IllegalArgumentException if the specified object is not
+ * an instance of the class or interface declaring the
+ * underlying field (or a subclass or implementor
+ * thereof), or if the field value cannot be
+ * converted to the type {@code float} by a
+ * widening conversion.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#get
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public float getFloat(Object obj)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // return getFieldAccessor(obj).getFloat(obj);
+ CProver.notModelled();
+ return CProver.nondetFloat();
+ }
+
+ /**
+ * Gets the value of a static or instance field of type
+ * {@code double} or of another primitive type convertible to
+ * type {@code double} via a widening conversion.
+ *
+ * @param obj the object to extract the {@code double} value
+ * from
+ * @return the value of the field converted to type {@code double}
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is inaccessible.
+ * @exception IllegalArgumentException if the specified object is not
+ * an instance of the class or interface declaring the
+ * underlying field (or a subclass or implementor
+ * thereof), or if the field value cannot be
+ * converted to the type {@code double} by a
+ * widening conversion.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#get
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public double getDouble(Object obj)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // return getFieldAccessor(obj).getDouble(obj);
+ CProver.notModelled();
+ return CProver.nondetDouble();
+ }
+
+ /**
+ * Sets the field represented by this {@code Field} object on the
+ * specified object argument to the specified new value. The new
+ * value is automatically unwrapped if the underlying field has a
+ * primitive type.
+ *
+ * The operation proceeds as follows:
+ *
+ * If the underlying field is static, the {@code obj} argument is
+ * ignored; it may be null.
+ *
+ * Otherwise the underlying field is an instance field. If the
+ * specified object argument is null, the method throws a
+ * {@code NullPointerException}. If the specified object argument is not
+ * an instance of the class or interface declaring the underlying
+ * field, the method throws an {@code IllegalArgumentException}.
+ *
+ * If this {@code Field} object is enforcing Java language access control, and
+ * the underlying field is inaccessible, the method throws an
+ * {@code IllegalAccessException}.
+ *
+ * If the underlying field is final, the method throws an
+ * {@code IllegalAccessException} unless {@code setAccessible(true)}
+ * has succeeded for this {@code Field} object
+ * and the field is non-static. Setting a final field in this way
+ * is meaningful only during deserialization or reconstruction of
+ * instances of classes with blank final fields, before they are
+ * made available for access by other parts of a program. Use in
+ * any other context may have unpredictable effects, including cases
+ * in which other parts of a program continue to use the original
+ * value of this field.
+ *
+ * If the underlying field is of a primitive type, an unwrapping
+ * conversion is attempted to convert the new value to a value of
+ * a primitive type. If this attempt fails, the method throws an
+ * {@code IllegalArgumentException}.
+ *
+ * If, after possible unwrapping, the new value cannot be
+ * converted to the type of the underlying field by an identity or
+ * widening conversion, the method throws an
+ * {@code IllegalArgumentException}.
+ *
+ * If the underlying field is static, the class that declared the
+ * field is initialized if it has not already been initialized.
+ *
+ * The field is set to the possibly unwrapped and widened new value.
+ *
+ * If the field is hidden in the type of {@code obj},
+ * the field's value is set according to the preceding rules.
+ *
+ * @param obj the object whose field should be modified
+ * @param value the new value for the field of {@code obj}
+ * being modified
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is either inaccessible or final.
+ * @exception IllegalArgumentException if the specified object is not an
+ * instance of the class or interface declaring the underlying
+ * field (or a subclass or implementor thereof),
+ * or if an unwrapping conversion fails.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public void set(Object obj, Object value)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // getFieldAccessor(obj).set(obj, value);
+ CProver.notModelled();
+ }
+
+ /**
+ * Sets the value of a field as a {@code boolean} on the specified object.
+ * This method is equivalent to
+ * {@code set(obj, zObj)},
+ * where {@code zObj} is a {@code Boolean} object and
+ * {@code zObj.booleanValue() == z}.
+ *
+ * @param obj the object whose field should be modified
+ * @param z the new value for the field of {@code obj}
+ * being modified
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is either inaccessible or final.
+ * @exception IllegalArgumentException if the specified object is not an
+ * instance of the class or interface declaring the underlying
+ * field (or a subclass or implementor thereof),
+ * or if an unwrapping conversion fails.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#set
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public void setBoolean(Object obj, boolean z)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // getFieldAccessor(obj).setBoolean(obj, z);
+ CProver.notModelled();
+ }
+
+ /**
+ * Sets the value of a field as a {@code byte} on the specified object.
+ * This method is equivalent to
+ * {@code set(obj, bObj)},
+ * where {@code bObj} is a {@code Byte} object and
+ * {@code bObj.byteValue() == b}.
+ *
+ * @param obj the object whose field should be modified
+ * @param b the new value for the field of {@code obj}
+ * being modified
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is either inaccessible or final.
+ * @exception IllegalArgumentException if the specified object is not an
+ * instance of the class or interface declaring the underlying
+ * field (or a subclass or implementor thereof),
+ * or if an unwrapping conversion fails.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#set
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public void setByte(Object obj, byte b)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // getFieldAccessor(obj).setByte(obj, b);
+ CProver.notModelled();
+ }
+
+ /**
+ * Sets the value of a field as a {@code char} on the specified object.
+ * This method is equivalent to
+ * {@code set(obj, cObj)},
+ * where {@code cObj} is a {@code Character} object and
+ * {@code cObj.charValue() == c}.
+ *
+ * @param obj the object whose field should be modified
+ * @param c the new value for the field of {@code obj}
+ * being modified
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is either inaccessible or final.
+ * @exception IllegalArgumentException if the specified object is not an
+ * instance of the class or interface declaring the underlying
+ * field (or a subclass or implementor thereof),
+ * or if an unwrapping conversion fails.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#set
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public void setChar(Object obj, char c)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // getFieldAccessor(obj).setChar(obj, c);
+ CProver.notModelled();
+ }
+
+ /**
+ * Sets the value of a field as a {@code short} on the specified object.
+ * This method is equivalent to
+ * {@code set(obj, sObj)},
+ * where {@code sObj} is a {@code Short} object and
+ * {@code sObj.shortValue() == s}.
+ *
+ * @param obj the object whose field should be modified
+ * @param s the new value for the field of {@code obj}
+ * being modified
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is either inaccessible or final.
+ * @exception IllegalArgumentException if the specified object is not an
+ * instance of the class or interface declaring the underlying
+ * field (or a subclass or implementor thereof),
+ * or if an unwrapping conversion fails.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#set
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public void setShort(Object obj, short s)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // getFieldAccessor(obj).setShort(obj, s);
+ CProver.notModelled();
+ }
+
+ /**
+ * Sets the value of a field as an {@code int} on the specified object.
+ * This method is equivalent to
+ * {@code set(obj, iObj)},
+ * where {@code iObj} is a {@code Integer} object and
+ * {@code iObj.intValue() == i}.
+ *
+ * @param obj the object whose field should be modified
+ * @param i the new value for the field of {@code obj}
+ * being modified
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is either inaccessible or final.
+ * @exception IllegalArgumentException if the specified object is not an
+ * instance of the class or interface declaring the underlying
+ * field (or a subclass or implementor thereof),
+ * or if an unwrapping conversion fails.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#set
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public void setInt(Object obj, int i)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // getFieldAccessor(obj).setInt(obj, i);
+ CProver.notModelled();
+ }
+
+ /**
+ * Sets the value of a field as a {@code long} on the specified object.
+ * This method is equivalent to
+ * {@code set(obj, lObj)},
+ * where {@code lObj} is a {@code Long} object and
+ * {@code lObj.longValue() == l}.
+ *
+ * @param obj the object whose field should be modified
+ * @param l the new value for the field of {@code obj}
+ * being modified
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is either inaccessible or final.
+ * @exception IllegalArgumentException if the specified object is not an
+ * instance of the class or interface declaring the underlying
+ * field (or a subclass or implementor thereof),
+ * or if an unwrapping conversion fails.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#set
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public void setLong(Object obj, long l)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // getFieldAccessor(obj).setLong(obj, l);
+ CProver.notModelled();
+ }
+
+ /**
+ * Sets the value of a field as a {@code float} on the specified object.
+ * This method is equivalent to
+ * {@code set(obj, fObj)},
+ * where {@code fObj} is a {@code Float} object and
+ * {@code fObj.floatValue() == f}.
+ *
+ * @param obj the object whose field should be modified
+ * @param f the new value for the field of {@code obj}
+ * being modified
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is either inaccessible or final.
+ * @exception IllegalArgumentException if the specified object is not an
+ * instance of the class or interface declaring the underlying
+ * field (or a subclass or implementor thereof),
+ * or if an unwrapping conversion fails.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#set
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public void setFloat(Object obj, float f)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // getFieldAccessor(obj).setFloat(obj, f);
+ CProver.notModelled();
+ }
+
+ /**
+ * Sets the value of a field as a {@code double} on the specified object.
+ * This method is equivalent to
+ * {@code set(obj, dObj)},
+ * where {@code dObj} is a {@code Double} object and
+ * {@code dObj.doubleValue() == d}.
+ *
+ * @param obj the object whose field should be modified
+ * @param d the new value for the field of {@code obj}
+ * being modified
+ *
+ * @exception IllegalAccessException if this {@code Field} object
+ * is enforcing Java language access control and the underlying
+ * field is either inaccessible or final.
+ * @exception IllegalArgumentException if the specified object is not an
+ * instance of the class or interface declaring the underlying
+ * field (or a subclass or implementor thereof),
+ * or if an unwrapping conversion fails.
+ * @exception NullPointerException if the specified object is null
+ * and the field is an instance field.
+ * @exception ExceptionInInitializerError if the initialization provoked
+ * by this method fails.
+ * @see Field#set
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public void setDouble(Object obj, double d)
+ throws IllegalArgumentException, IllegalAccessException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // getFieldAccessor(obj).setDouble(obj, d);
+ CProver.notModelled();
+ }
+
+ // security check is done before calling this method
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private FieldAccessor getFieldAccessor(Object obj)
+ // throws IllegalAccessException
+ // {
+ // boolean ov = override;
+ // FieldAccessor a = (ov) ? overrideFieldAccessor : fieldAccessor;
+ // return (a != null) ? a : acquireFieldAccessor(ov);
+ // }
+
+ // NOTE that there is no synchronization used here. It is correct
+ // (though not efficient) to generate more than one FieldAccessor
+ // for a given Field. However, avoiding synchronization will
+ // probably make the implementation more scalable.
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private FieldAccessor acquireFieldAccessor(boolean overrideFinalCheck) {
+ // // First check to see if one has been created yet, and take it
+ // // if so
+ // FieldAccessor tmp = null;
+ // if (root != null) tmp = root.getFieldAccessor(overrideFinalCheck);
+ // if (tmp != null) {
+ // if (overrideFinalCheck)
+ // overrideFieldAccessor = tmp;
+ // else
+ // fieldAccessor = tmp;
+ // } else {
+ // // Otherwise fabricate one and propagate it up to the root
+ // tmp = reflectionFactory.newFieldAccessor(this, overrideFinalCheck);
+ // setFieldAccessor(tmp, overrideFinalCheck);
+ // }
+
+ // return tmp;
+ // }
+
+ // Returns FieldAccessor for this Field object, not looking up
+ // the chain to the root
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private FieldAccessor getFieldAccessor(boolean overrideFinalCheck) {
+ // return (overrideFinalCheck)? overrideFieldAccessor : fieldAccessor;
+ // }
+
+ // Sets the FieldAccessor for this Field object and
+ // (recursively) its root
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private void setFieldAccessor(FieldAccessor accessor, boolean overrideFinalCheck) {
+ // if (overrideFinalCheck)
+ // overrideFieldAccessor = accessor;
+ // else
+ // fieldAccessor = accessor;
+ // // Propagate up
+ // if (root != null) {
+ // root.setFieldAccessor(accessor, overrideFinalCheck);
+ // }
+ // }
+
+ /**
+ * @throws NullPointerException {@inheritDoc}
+ * @since 1.5
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public As of release 1.4, this exception has been retrofitted to conform to
+ * the general purpose exception-chaining mechanism. The "target exception"
+ * that is provided at construction time and accessed via the
+ * {@link #getTargetException()} method is now known as the cause,
+ * and may be accessed via the {@link Throwable#getCause()} method,
+ * as well as the aforementioned "legacy method."
+ *
+ * @see Method
+ * @see Constructor
+ */
+public class InvocationTargetException extends ReflectiveOperationException {
+ /**
+ * Use serialVersionUID from JDK 1.1.X for interoperability
+ */
+ private static final long serialVersionUID = 4085088731926701167L;
+
+ /**
+ * This field holds the target if the
+ * InvocationTargetException(Throwable target) constructor was
+ * used to instantiate the object
+ *
+ * @serial
+ *
+ */
+ private Throwable target;
+
+ /**
+ * Constructs an {@code InvocationTargetException} with
+ * {@code null} as the target exception.
+ */
+ protected InvocationTargetException() {
+ super((Throwable)null); // Disallow initCause
+ }
+
+ /**
+ * Constructs a InvocationTargetException with a target exception.
+ *
+ * @param target the target exception
+ */
+ public InvocationTargetException(Throwable target) {
+ super((Throwable)null); // Disallow initCause
+ this.target = target;
+ }
+
+ /**
+ * Constructs a InvocationTargetException with a target exception
+ * and a detail message.
+ *
+ * @param target the target exception
+ * @param s the detail message
+ */
+ public InvocationTargetException(Throwable target, String s) {
+ super(s, null); // Disallow initCause
+ this.target = target;
+ }
+
+ /**
+ * Get the thrown target exception.
+ *
+ * This method predates the general-purpose exception chaining facility.
+ * The {@link Throwable#getCause()} method is now the preferred means of
+ * obtaining this information.
+ *
+ * @return the thrown target exception (cause of this exception).
+ */
+ public Throwable getTargetException() {
+ return target;
+ }
+
+ /**
+ * Returns the cause of this exception (the thrown target exception,
+ * which may be {@code null}).
+ *
+ * @return the cause of this exception.
+ * @since 1.4
+ */
+ public Throwable getCause() {
+ return target;
+ }
+
+ // DIFFBLUE MODEL LIBRARY
+ // While Object.getClass() is not modelled, we can get the same
+ // functionality by adding one toString() method per subclass of
+ // Throwable.
+ @Override
+ public String toString() {
+ String message = getLocalizedMessage();
+ return (message != null)
+ ? ("java.lang.reflect.InvocationTargetException: " + message)
+ : "java.lang.reflect.InvocationTargetException";
+ }
+}
diff --git a/src/main/java/java/lang/reflect/MalformedParameterizedTypeException.java b/src/main/java/java/lang/reflect/MalformedParameterizedTypeException.java
new file mode 100644
index 0000000..9c1eec5
--- /dev/null
+++ b/src/main/java/java/lang/reflect/MalformedParameterizedTypeException.java
@@ -0,0 +1,51 @@
+/*
+ * Copyright (c) 2003, 2008, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+
+package java.lang.reflect;
+
+/**
+ * Thrown when a semantically malformed parameterized type is
+ * encountered by a reflective method that needs to instantiate it.
+ * For example, if the number of type arguments to a parameterized type
+ * is wrong.
+ *
+ * @since 1.5
+ */
+public class MalformedParameterizedTypeException extends RuntimeException {
+ private static final long serialVersionUID = -5696557788586220964L;
+
+ // DIFFBLUE MODEL LIBRARY
+ // While Object.getClass() is not modelled, we can get the same
+ // functionality by adding one toString() method per subclass of
+ // Throwable.
+ @Override
+ public String toString() {
+ String message = getLocalizedMessage();
+ return (message != null)
+ ? ("java.lang.reflect.MalformedParameterizedTypeException: " + message)
+ : "java.lang.reflect.MalformedParameterizedTypeException";
+ }
+}
diff --git a/src/main/java/java/lang/reflect/MalformedParametersException.java b/src/main/java/java/lang/reflect/MalformedParametersException.java
new file mode 100644
index 0000000..7ce36ac
--- /dev/null
+++ b/src/main/java/java/lang/reflect/MalformedParametersException.java
@@ -0,0 +1,84 @@
+/*
+ * Copyright (c) 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.lang.reflect;
+
+/**
+ * Thrown when {@link java.lang.reflect.Executable#getParameters the
+ * java.lang.reflect package} attempts to read method parameters from
+ * a class file and determines that one or more parameters are
+ * malformed.
+ *
+ * The following is a list of conditions under which this exception
+ * can be thrown:
+ * A {@code Method} permits widening conversions to occur when matching the
+ * actual parameters to invoke with the underlying method's formal
+ * parameters, but it throws an {@code IllegalArgumentException} if a
+ * narrowing conversion would occur.
+ *
+ * @see Member
+ * @see java.lang.Class
+ * @see java.lang.Class#getMethods()
+ * @see java.lang.Class#getMethod(String, Class[])
+ * @see java.lang.Class#getDeclaredMethods()
+ * @see java.lang.Class#getDeclaredMethod(String, Class[])
+ *
+ * @author Kenneth Russell
+ * @author Nakul Saraiya
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ * This model was automatically generated by the JDK Processor tool.
+ */
+public final class Method extends Executable {
+ private Class> clazz;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private int slot;
+ // This is guaranteed to be interned by the VM in the 1.4
+ // reflection implementation
+ private String name;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private Class> returnType;
+ private Class>[] parameterTypes;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private Class>[] exceptionTypes;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private int modifiers;
+ // Generics and annotations support
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private transient String signature;
+ // generic info repository; lazily initialized
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private transient MethodRepository genericInfo;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private byte[] annotations;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private byte[] parameterAnnotations;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private byte[] annotationDefault;
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private volatile MethodAccessor methodAccessor;
+ // For sharing of MethodAccessors. This branching structure is
+ // currently only two levels deep (i.e., one root Method and
+ // potentially many Method objects pointing to it.)
+ //
+ // If this branching structure would ever contain cycles, deadlocks can
+ // occur in annotation code.
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private Method root;
+
+ // Generics infrastructure
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private String getGenericSignature() {return signature;}
+
+ // Accessor for factory
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private GenericsFactory getFactory() {
+ // // create scope and factory
+ // return CoreReflectionFactory.make(this, MethodScope.make(this));
+ // }
+
+ /**
+ * Accessor for generic info repository
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ @Override
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ MethodRepository getGenericInfo() {
+ // // lazily initialize repository if necessary
+ // if (genericInfo == null) {
+ // // create and cache generic info repository
+ // genericInfo = MethodRepository.make(getGenericSignature(),
+ // getFactory());
+ // }
+ // return genericInfo; //return cached repository
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * Package-private constructor used by ReflectAccess to enable
+ * instantiation of these objects in Java code from the java.lang
+ * package via sun.reflect.LangReflectAccess.
+ */
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // Method(Class> declaringClass,
+ // String name,
+ // Class>[] parameterTypes,
+ // Class> returnType,
+ // Class>[] checkedExceptions,
+ // int modifiers,
+ // int slot,
+ // String signature,
+ // byte[] annotations,
+ // byte[] parameterAnnotations,
+ // byte[] annotationDefault) {
+ // this.clazz = declaringClass;
+ // this.name = name;
+ // this.parameterTypes = parameterTypes;
+ // this.returnType = returnType;
+ // this.exceptionTypes = checkedExceptions;
+ // this.modifiers = modifiers;
+ // this.slot = slot;
+ // this.signature = signature;
+ // this.annotations = annotations;
+ // this.parameterAnnotations = parameterAnnotations;
+ // this.annotationDefault = annotationDefault;
+ // }
+
+ /**
+ * This constructor does not exist in the JDK, only in the model
+ */
+ public Method(
+ Class> declaringClass,
+ String name,
+ Class>[] parameterTypes)
+ {
+ this.clazz = declaringClass;
+ this.name = name;
+ this.parameterTypes = parameterTypes;
+ }
+
+ /**
+ * Package-private routine (exposed to java.lang.Class via
+ * ReflectAccess) which returns a copy of this Method. The copy's
+ * "root" field points to this Method.
+ */
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // Method copy() {
+ // // This routine enables sharing of MethodAccessor objects
+ // // among Method objects which refer to the same underlying
+ // // method in the VM. (All of this contortion is only necessary
+ // // because of the "accessibility" bit in AccessibleObject,
+ // // which implicitly requires that new java.lang.reflect
+ // // objects be fabricated for each reflective call on Class
+ // // objects.)
+ // if (this.root != null)
+ // throw new IllegalArgumentException("Can not copy a non-root Method");
+
+ // Method res = new Method(clazz, name, parameterTypes, returnType,
+ // exceptionTypes, modifiers, slot, signature,
+ // annotations, parameterAnnotations, annotationDefault);
+ // res.root = this;
+ // // Might as well eagerly propagate this if already present
+ // res.methodAccessor = methodAccessor;
+ // return res;
+ // }
+
+ /**
+ * Used by Excecutable for annotation sharing.
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ @Override
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ Executable getRoot() {
+ // return root;
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ @Override
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ boolean hasGenericInformation() {
+ // return (getGenericSignature() != null);
+ CProver.notModelled();
+ return CProver.nondetBoolean();
+ }
+
+ /**
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ @Override
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ byte[] getAnnotationBytes() {
+ // return annotations;
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ * @diffblue.fullSupport
+ */
+ @Override
+ public Class> getDeclaringClass() {
+ return clazz;
+ }
+
+ /**
+ * Returns the name of the method represented by this {@code Method}
+ * object, as a {@code String}.
+ *
+ * @diffblue.fullSupport
+ */
+ @Override
+ public String getName() {
+ return name;
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ @Override
+ public int getModifiers() {
+ // return modifiers;
+ CProver.notModelled();
+ return CProver.nondetInt();
+ }
+
+ /**
+ * {@inheritDoc}
+ * @throws GenericSignatureFormatError {@inheritDoc}
+ * @since 1.5
+ */
+ @Override
+ @SuppressWarnings({"rawtypes", "unchecked"})
+ public TypeVariable If the return type is a parameterized type,
+ * the {@code Type} object returned must accurately reflect
+ * the actual type parameters used in the source code.
+ *
+ * If the return type is a type variable or a parameterized type, it
+ * is created. Otherwise, it is resolved.
+ *
+ * @return a {@code Type} object that represents the formal return
+ * type of the underlying method
+ * @throws GenericSignatureFormatError
+ * if the generic method signature does not conform to the format
+ * specified in
+ * The Java™ Virtual Machine Specification
+ * @throws TypeNotPresentException if the underlying method's
+ * return type refers to a non-existent type declaration
+ * @throws MalformedParameterizedTypeException if the
+ * underlying method's return typed refers to a parameterized
+ * type that cannot be instantiated for any reason
+ * @since 1.5
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public Type getGenericReturnType() {
+// if (getGenericSignature() != null) {
+ // return getGenericInfo().getReturnType();
+// } else { return getReturnType();}
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ * @diffblue.untested
+ * @diffblue.fullSupport
+ */
+ @Override
+ public Class>[] getParameterTypes() {
+ return parameterTypes.clone();
+ }
+
+ /**
+ * {@inheritDoc}
+ * @since 1.8
+ *
+ * @diffblue.untested
+ * @diffblue.fullSupport
+ */
+ public int getParameterCount() {
+ return parameterTypes.length;
+ }
+
+
+ /**
+ * {@inheritDoc}
+ * @throws GenericSignatureFormatError {@inheritDoc}
+ * @throws TypeNotPresentException {@inheritDoc}
+ * @throws MalformedParameterizedTypeException {@inheritDoc}
+ * @since 1.5
+ *
+ * @diffblue.untested
+ */
+ @Override
+ public Type[] getGenericParameterTypes() {
+ return super.getGenericParameterTypes();
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ @Override
+ public Class>[] getExceptionTypes() {
+ // return exceptionTypes.clone();
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * {@inheritDoc}
+ * @throws GenericSignatureFormatError {@inheritDoc}
+ * @throws TypeNotPresentException {@inheritDoc}
+ * @throws MalformedParameterizedTypeException {@inheritDoc}
+ * @since 1.5
+ *
+ * @diffblue.untested
+ */
+ @Override
+ public Type[] getGenericExceptionTypes() {
+ return super.getGenericExceptionTypes();
+ }
+
+ /**
+ * Compares this {@code Method} against the specified object. Returns
+ * true if the objects are the same. Two {@code Methods} are the same if
+ * they were declared by the same class and have the same name
+ * and formal parameter types and return type.
+ *
+ * @diffblue.limitedSupport
+ */
+ public boolean equals(Object obj) {
+ if (obj != null && obj instanceof Method) {
+ Method other = (Method)obj;
+ if ((getDeclaringClass() == other.getDeclaringClass())
+ && (getName() == other.getName())) {
+ return equalParamTypes(parameterTypes, other.parameterTypes);
+ }
+ }
+ return false;
+ }
+
+ /**
+ * Returns a hashcode for this {@code Method}. The hashcode is computed
+ * as the exclusive-or of the hashcodes for the underlying
+ * method's declaring class name and the method's name.
+ *
+ * @diffblue.untested
+ */
+ public int hashCode() {
+ return getDeclaringClass().getName().hashCode() ^ getName().hashCode();
+ }
+
+ /**
+ * Returns a string describing this {@code Method}. The string is
+ * formatted as the method access modifiers, if any, followed by
+ * the method return type, followed by a space, followed by the
+ * class declaring the method, followed by a period, followed by
+ * the method name, followed by a parenthesized, comma-separated
+ * list of the method's formal parameter types. If the method
+ * throws checked exceptions, the parameter list is followed by a
+ * space, followed by the word throws followed by a
+ * comma-separated list of the thrown exception types.
+ * For example:
+ * The access modifiers are placed in canonical order as
+ * specified by "The Java Language Specification". This is
+ * {@code public}, {@code protected} or {@code private} first,
+ * and then other modifiers in the following order:
+ * {@code abstract}, {@code default}, {@code static}, {@code final},
+ * {@code synchronized}, {@code native}, {@code strictfp}.
+ *
+ * @return a string describing this {@code Method}
+ *
+ * @jls 8.4.3 Method Modifiers
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public String toString() {
+ // return sharedToString(Modifier.methodModifiers(),
+ // isDefault(),
+ // parameterTypes,
+ // exceptionTypes);
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ @Override
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ void specificToStringHeader(StringBuilder sb) {
+ // sb.append(getReturnType().getTypeName()).append(' ');
+ // sb.append(getDeclaringClass().getTypeName()).append('.');
+ // sb.append(getName());
+ CProver.notModelled();
+ }
+
+ /**
+ * Returns a string describing this {@code Method}, including
+ * type parameters. The string is formatted as the method access
+ * modifiers, if any, followed by an angle-bracketed
+ * comma-separated list of the method's type parameters, if any,
+ * followed by the method's generic return type, followed by a
+ * space, followed by the class declaring the method, followed by
+ * a period, followed by the method name, followed by a
+ * parenthesized, comma-separated list of the method's generic
+ * formal parameter types.
+ *
+ * If this method was declared to take a variable number of
+ * arguments, instead of denoting the last parameter as
+ * "Type[]", it is denoted as
+ * "Type...".
+ *
+ * A space is used to separate access modifiers from one another
+ * and from the type parameters or return type. If there are no
+ * type parameters, the type parameter list is elided; if the type
+ * parameter list is present, a space separates the list from the
+ * class name. If the method is declared to throw exceptions, the
+ * parameter list is followed by a space, followed by the word
+ * throws followed by a comma-separated list of the generic thrown
+ * exception types.
+ *
+ * The access modifiers are placed in canonical order as
+ * specified by "The Java Language Specification". This is
+ * {@code public}, {@code protected} or {@code private} first,
+ * and then other modifiers in the following order:
+ * {@code abstract}, {@code default}, {@code static}, {@code final},
+ * {@code synchronized}, {@code native}, {@code strictfp}.
+ *
+ * @return a string describing this {@code Method},
+ * include type parameters
+ *
+ * @since 1.5
+ *
+ * @jls 8.4.3 Method Modifiers
+ *
+ * @diffblue.untested
+ */
+ @Override
+ public String toGenericString() {
+ return sharedToGenericString(Modifier.methodModifiers(), isDefault());
+ }
+
+ /**
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ @Override
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ void specificToGenericStringHeader(StringBuilder sb) {
+ // Type genRetType = getGenericReturnType();
+ // sb.append(genRetType.getTypeName()).append(' ');
+ // sb.append(getDeclaringClass().getTypeName()).append('.');
+ // sb.append(getName());
+ CProver.notModelled();
+ }
+
+ /**
+ * Invokes the underlying method represented by this {@code Method}
+ * object, on the specified object with the specified parameters.
+ * Individual parameters are automatically unwrapped to match
+ * primitive formal parameters, and both primitive and reference
+ * parameters are subject to method invocation conversions as
+ * necessary.
+ *
+ * If the underlying method is static, then the specified {@code obj}
+ * argument is ignored. It may be null.
+ *
+ * If the number of formal parameters required by the underlying method is
+ * 0, the supplied {@code args} array may be of length 0 or null.
+ *
+ * If the underlying method is an instance method, it is invoked
+ * using dynamic method lookup as documented in The Java Language
+ * Specification, Second Edition, section 15.12.4.4; in particular,
+ * overriding based on the runtime type of the target object will occur.
+ *
+ * If the underlying method is static, the class that declared
+ * the method is initialized if it has not already been initialized.
+ *
+ * If the method completes normally, the value it returns is
+ * returned to the caller of invoke; if the value has a primitive
+ * type, it is first appropriately wrapped in an object. However,
+ * if the value has the type of an array of a primitive type, the
+ * elements of the array are not wrapped in objects; in
+ * other words, an array of primitive type is returned. If the
+ * underlying method return type is void, the invocation returns
+ * null.
+ *
+ * @param obj the object the underlying method is invoked from
+ * @param args the arguments used for the method call
+ * @return the result of dispatching the method represented by
+ * this object on {@code obj} with parameters
+ * {@code args}
+ *
+ * @exception IllegalAccessException if this {@code Method} object
+ * is enforcing Java language access control and the underlying
+ * method is inaccessible.
+ * @exception IllegalArgumentException if the method is an
+ * instance method and the specified object argument
+ * is not an instance of the class or interface
+ * declaring the underlying method (or of a subclass
+ * or implementor thereof); if the number of actual
+ * and formal parameters differ; if an unwrapping
+ * conversion for primitive arguments fails; or if,
+ * after possible unwrapping, a parameter value
+ * cannot be converted to the corresponding formal
+ * parameter type by a method invocation conversion.
+ * @exception InvocationTargetException if the underlying method
+ * throws an exception.
+ * @exception NullPointerException if the specified object is null
+ * and the method is an instance method.
+ * @exception ExceptionInInitializerError if the initialization
+ * provoked by this method fails.
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
+ // @CallerSensitive
+ public Object invoke(Object obj, Object... args)
+ throws IllegalAccessException, IllegalArgumentException,
+ InvocationTargetException
+ {
+ // if (!override) {
+ // if (!Reflection.quickCheckMemberAccess(clazz, modifiers)) {
+ // Class> caller = Reflection.getCallerClass();
+ // checkAccess(caller, clazz, obj, modifiers);
+ // }
+ // }
+ // MethodAccessor ma = methodAccessor; // read volatile
+ // if (ma == null) {
+ // ma = acquireMethodAccessor();
+ // }
+ // return ma.invoke(obj, args);
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * Returns {@code true} if this method is a bridge
+ * method; returns {@code false} otherwise.
+ *
+ * @return true if and only if this method is a bridge
+ * method as defined by the Java Language Specification.
+ * @since 1.5
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public boolean isBridge() {
+ // return (getModifiers() & Modifier.BRIDGE) != 0;
+ CProver.notModelled();
+ return CProver.nondetBoolean();
+ }
+
+ /**
+ * {@inheritDoc}
+ * @since 1.5
+ *
+ * @diffblue.untested
+ */
+ @Override
+ public boolean isVarArgs() {
+ return super.isVarArgs();
+ }
+
+ /**
+ * {@inheritDoc}
+ * @jls 13.1 The Form of a Binary
+ * @since 1.5
+ *
+ * @diffblue.untested
+ */
+ @Override
+ public boolean isSynthetic() {
+ return super.isSynthetic();
+ }
+
+ /**
+ * Returns {@code true} if this method is a default
+ * method; returns {@code false} otherwise.
+ *
+ * A default method is a public non-abstract instance method, that
+ * is, a non-static method with a body, declared in an interface
+ * type.
+ *
+ * @return true if and only if this method is a default
+ * method as defined by the Java Language Specification.
+ * @since 1.8
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public boolean isDefault() {
+ // // Default methods are public non-abstract instance methods
+ // // declared in an interface.
+ // return ((getModifiers() & (Modifier.ABSTRACT | Modifier.PUBLIC | Modifier.STATIC)) ==
+ // Modifier.PUBLIC) && getDeclaringClass().isInterface();
+ CProver.notModelled();
+ return CProver.nondetBoolean();
+ }
+
+ // NOTE that there is no synchronization used here. It is correct
+ // (though not efficient) to generate more than one MethodAccessor
+ // for a given Method. However, avoiding synchronization will
+ // probably make the implementation more scalable.
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private MethodAccessor acquireMethodAccessor() {
+ // // First check to see if one has been created yet, and take it
+ // // if so
+ // MethodAccessor tmp = null;
+ // if (root != null) tmp = root.getMethodAccessor();
+ // if (tmp != null) {
+ // methodAccessor = tmp;
+ // } else {
+ // // Otherwise fabricate one and propagate it up to the root
+ // tmp = reflectionFactory.newMethodAccessor(this);
+ // setMethodAccessor(tmp);
+ // }
+
+ // return tmp;
+ // }
+
+ // Returns MethodAccessor for this Method object, not looking up
+ // the chain to the root
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // MethodAccessor getMethodAccessor() {
+ // return methodAccessor;
+ // }
+
+ // Sets the MethodAccessor for this Method object and
+ // (recursively) its root
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // void setMethodAccessor(MethodAccessor accessor) {
+ // methodAccessor = accessor;
+ // // Propagate up
+ // if (root != null) {
+ // root.setMethodAccessor(accessor);
+ // }
+ // }
+
+ /**
+ * Returns the default value for the annotation member represented by
+ * this {@code Method} instance. If the member is of a primitive type,
+ * an instance of the corresponding wrapper type is returned. Returns
+ * null if no default is associated with the member, or if the method
+ * instance does not represent a declared member of an annotation type.
+ *
+ * @return the default value for the annotation member represented
+ * by this {@code Method} instance.
+ * @throws TypeNotPresentException if the annotation is of type
+ * {@link Class} and no definition can be found for the
+ * default class value.
+ * @since 1.5
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public Object getDefaultValue() {
+ // if (annotationDefault == null)
+ // return null;
+ // Class> memberType = AnnotationType.invocationHandlerReturnType(
+ // getReturnType());
+ // Object result = AnnotationParser.parseMemberValue(
+ // memberType, ByteBuffer.wrap(annotationDefault),
+ // sun.misc.SharedSecrets.getJavaLangAccess().
+ // getConstantPool(getDeclaringClass()),
+ // getDeclaringClass());
+ // if (result instanceof sun.reflect.annotation.ExceptionProxy)
+ // throw new AnnotationFormatError("Invalid default: " + this);
+ // return result;
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * {@inheritDoc}
+ * @throws NullPointerException {@inheritDoc}
+ * @since 1.5
+ *
+ * @diffblue.untested
+ */
+ public An {@code UndeclaredThrowableException} instance contains
+ * the undeclared checked exception that was thrown by the invocation
+ * handler, and it can be retrieved with the
+ * {@code getUndeclaredThrowable()} method.
+ * {@code UndeclaredThrowableException} extends
+ * {@code RuntimeException}, so it is an unchecked exception
+ * that wraps a checked exception.
+ *
+ * As of release 1.4, this exception has been retrofitted to
+ * conform to the general purpose exception-chaining mechanism. The
+ * "undeclared checked exception that was thrown by the invocation
+ * handler" that may be provided at construction time and accessed via
+ * the {@link #getUndeclaredThrowable()} method is now known as the
+ * cause, and may be accessed via the {@link
+ * Throwable#getCause()} method, as well as the aforementioned "legacy
+ * method."
+ *
+ * @author Peter Jones
+ * @see InvocationHandler
+ * @since 1.3
+ */
+public class UndeclaredThrowableException extends RuntimeException {
+ static final long serialVersionUID = 330127114055056639L;
+
+ /**
+ * the undeclared checked exception that was thrown
+ * @serial
+ */
+ private Throwable undeclaredThrowable;
+
+ /**
+ * Constructs an {@code UndeclaredThrowableException} with the
+ * specified {@code Throwable}.
+ *
+ * @param undeclaredThrowable the undeclared checked exception
+ * that was thrown
+ */
+ public UndeclaredThrowableException(Throwable undeclaredThrowable) {
+ super((Throwable) null); // Disallow initCause
+ this.undeclaredThrowable = undeclaredThrowable;
+ }
+
+ /**
+ * Constructs an {@code UndeclaredThrowableException} with the
+ * specified {@code Throwable} and a detail message.
+ *
+ * @param undeclaredThrowable the undeclared checked exception
+ * that was thrown
+ * @param s the detail message
+ */
+ public UndeclaredThrowableException(Throwable undeclaredThrowable,
+ String s)
+ {
+ super(s, null); // Disallow initCause
+ this.undeclaredThrowable = undeclaredThrowable;
+ }
+
+ /**
+ * Returns the {@code Throwable} instance wrapped in this
+ * {@code UndeclaredThrowableException}, which may be {@code null}.
+ *
+ * This method predates the general-purpose exception chaining facility.
+ * The {@link Throwable#getCause()} method is now the preferred means of
+ * obtaining this information.
+ *
+ * @return the undeclared checked exception that was thrown
+ */
+ public Throwable getUndeclaredThrowable() {
+ return undeclaredThrowable;
+ }
+
+ /**
+ * Returns the cause of this exception (the {@code Throwable}
+ * instance wrapped in this {@code UndeclaredThrowableException},
+ * which may be {@code null}).
+ *
+ * @return the cause of this exception.
+ * @since 1.4
+ */
+ public Throwable getCause() {
+ return undeclaredThrowable;
+ }
+
+ // DIFFBLUE MODEL LIBRARY
+ // While Object.getClass() is not modelled, we can get the same
+ // functionality by adding one toString() method per subclass of
+ // Throwable.
+ @Override
+ public String toString() {
+ String message = getLocalizedMessage();
+ return (message != null)
+ ? ("java.lang.reflect.UndeclaredThrowableException: " + message)
+ : "java.lang.reflect.UndeclaredThrowableException";
+ }
+}
diff --git a/src/main/java/java/util/Random.java b/src/main/java/java/util/Random.java
index 49a5597..ead9e2c 100644
--- a/src/main/java/java/util/Random.java
+++ b/src/main/java/java/util/Random.java
@@ -186,14 +186,13 @@ public Random(long seed) {
*
* @param seed the initial seed
*
- * @diffblue.noSupport
- * Due to TG-2435.
+ * The pattern is compared to the input one character at a time, from
+ * the rightmost character in the pattern to the left. If the characters
+ * all match the pattern has been found. If a character does not match,
+ * the pattern is shifted right a distance that is the maximum of two
+ * functions, the bad character shift and the good suffix shift. This
+ * shift moves the attempted match position through the input more
+ * quickly than a naive one position at a time check.
+ *
+ * The bad character shift is based on the character from the text that
+ * did not match. If the character does not appear in the pattern, the
+ * pattern can be shifted completely beyond the bad character. If the
+ * character does occur in the pattern, the pattern can be shifted to
+ * line the pattern up with the next occurrence of that character.
+ *
+ * The good suffix shift is based on the idea that some subset on the right
+ * side of the pattern has matched. When a bad character is found, the
+ * pattern can be shifted right by the pattern length if the subset does
+ * not occur again in pattern, or by the amount of distance to the
+ * next occurrence of the subset in the pattern.
+ *
+ * Boyer-Moore search methods adapted from code by Amy Yu.
+ */
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // static class BnM extends Node {
+ // int[] buffer;
+ // int[] lastOcc;
+ // int[] optoSft;
+
+ // /**
+ // * Pre calculates arrays needed to generate the bad character
+ // * shift and the good suffix shift. Only the last seven bits
+ // * are used to see if chars match; This keeps the tables small
+ // * and covers the heavily used ASCII range, but occasionally
+ // * results in an aliased match for the bad character shift.
+ // */
+ // static Node optimize(Node node) {
+ // if (!(node instanceof Slice)) {
+ // return node;
+ // }
+
+ // int[] src = ((Slice) node).buffer;
+ // int patternLength = src.length;
+ // // The BM algorithm requires a bit of overhead;
+ // // If the pattern is short don't use it, since
+ // // a shift larger than the pattern length cannot
+ // // be used anyway.
+ // if (patternLength < 4) {
+ // return node;
+ // }
+ // int i, j, k;
+ // int[] lastOcc = new int[128];
+ // int[] optoSft = new int[patternLength];
+ // // Precalculate part of the bad character shift
+ // // It is a table for where in the pattern each
+ // // lower 7-bit value occurs
+ // for (i = 0; i < patternLength; i++) {
+ // lastOcc[src[i]&0x7F] = i + 1;
+ // }
+ // // Precalculate the good suffix shift
+ // // i is the shift amount being considered
+// NEXT: for (i = patternLength; i > 0; i--) {
+ // // j is the beginning index of suffix being considered
+ // for (j = patternLength - 1; j >= i; j--) {
+ // // Testing for good suffix
+ // if (src[j] == src[j-i]) {
+ // // src[j..len] is a good suffix
+ // optoSft[j-1] = i;
+ // } else {
+ // // No match. The array has already been
+ // // filled up with correct values before.
+ // continue NEXT;
+ // }
+ // }
+ // // This fills up the remaining of optoSft
+ // // any suffix can not have larger shift amount
+ // // then its sub-suffix. Why???
+ // while (j > 0) {
+ // optoSft[--j] = i;
+ // }
+ // }
+ // // Set the guard value because of unicode compression
+ // optoSft[patternLength-1] = 1;
+ // if (node instanceof SliceS)
+ // return new BnMS(src, lastOcc, optoSft, node.next);
+ // return new BnM(src, lastOcc, optoSft, node.next);
+ // }
+ // BnM(int[] src, int[] lastOcc, int[] optoSft, Node next) {
+ // this.buffer = src;
+ // this.lastOcc = lastOcc;
+ // this.optoSft = optoSft;
+ // this.next = next;
+ // }
+ // boolean match(Matcher matcher, int i, CharSequence seq) {
+ // int[] src = buffer;
+ // int patternLength = src.length;
+ // int last = matcher.to - patternLength;
+
+ // // Loop over all possible match positions in text
+// NEXT: while (i <= last) {
+ // // Loop over pattern from right to left
+ // for (int j = patternLength - 1; j >= 0; j--) {
+ // int ch = seq.charAt(i+j);
+ // if (ch != src[j]) {
+ // // Shift search to the right by the maximum of the
+ // // bad character shift and the good suffix shift
+ // i += Math.max(j + 1 - lastOcc[ch&0x7F], optoSft[j]);
+ // continue NEXT;
+ // }
+ // }
+ // // Entire pattern matched starting at i
+ // matcher.first = i;
+ // boolean ret = next.match(matcher, i + patternLength, seq);
+ // if (ret) {
+ // matcher.first = i;
+ // matcher.groups[0] = matcher.first;
+ // matcher.groups[1] = matcher.last;
+ // return true;
+ // }
+ // i++;
+ // }
+ // // BnM is only used as the leading node in the unanchored case,
+ // // and it replaced its Start() which always searches to the end
+ // // if it doesn't find what it's looking for, so hitEnd is true.
+ // matcher.hitEnd = true;
+ // return false;
+ // }
+ // boolean study(TreeInfo info) {
+ // info.minLength += buffer.length;
+ // info.maxValid = false;
+ // return next.study(info);
+ // }
+ // }
+
+ /**
+ * Supplementary support version of BnM(). Unpaired surrogates are
+ * also handled by this class.
+ */
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // static final class BnMS extends BnM {
+ // int lengthInChars;
+
+ // BnMS(int[] src, int[] lastOcc, int[] optoSft, Node next) {
+ // super(src, lastOcc, optoSft, next);
+ // for (int x = 0; x < buffer.length; x++) {
+ // lengthInChars += Character.charCount(buffer[x]);
+ // }
+ // }
+ // boolean match(Matcher matcher, int i, CharSequence seq) {
+ // int[] src = buffer;
+ // int patternLength = src.length;
+ // int last = matcher.to - lengthInChars;
+
+ // // Loop over all possible match positions in text
+// NEXT: while (i <= last) {
+ // // Loop over pattern from right to left
+ // int ch;
+ // for (int j = countChars(seq, i, patternLength), x = patternLength - 1;
+ // j > 0; j -= Character.charCount(ch), x--) {
+ // ch = Character.codePointBefore(seq, i+j);
+ // if (ch != src[x]) {
+ // // Shift search to the right by the maximum of the
+ // // bad character shift and the good suffix shift
+ // int n = Math.max(x + 1 - lastOcc[ch&0x7F], optoSft[x]);
+ // i += countChars(seq, i, n);
+ // continue NEXT;
+ // }
+ // }
+ // // Entire pattern matched starting at i
+ // matcher.first = i;
+ // boolean ret = next.match(matcher, i + lengthInChars, seq);
+ // if (ret) {
+ // matcher.first = i;
+ // matcher.groups[0] = matcher.first;
+ // matcher.groups[1] = matcher.last;
+ // return true;
+ // }
+ // i += countChars(seq, i, 1);
+ // }
+ // matcher.hitEnd = true;
+ // return false;
+ // }
+ // }
+
+///////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////////
+
+ /**
+ * This must be the very first initializer.
+ */
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // static Node accept = new Node();
+
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // static Node lastAccept = new LastNode();
+
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private static class CharPropertyNames {
+
+ // static CharProperty charPropertyFor(String name) {
+ // CharPropertyFactory m = map.get(name);
+ // return m == null ? null : m.make();
+ // }
+
+ // private static abstract class CharPropertyFactory {
+ // abstract CharProperty make();
+ // }
+
+ // private static void defCategory(String name,
+ // final int typeMask) {
+ // map.put(name, new CharPropertyFactory() {
+ // CharProperty make() { return new Category(typeMask);}});
+ // }
+
+ // private static void defRange(String name,
+ // final int lower, final int upper) {
+ // map.put(name, new CharPropertyFactory() {
+ // CharProperty make() { return rangeFor(lower, upper);}});
+ // }
+
+ // private static void defCtype(String name,
+ // final int ctype) {
+ // map.put(name, new CharPropertyFactory() {
+ // CharProperty make() { return new Ctype(ctype);}});
+ // }
+
+ // private static abstract class CloneableProperty
+ // extends CharProperty implements Cloneable
+ // {
+ // public CloneableProperty clone() {
+ // try {
+ // return (CloneableProperty) super.clone();
+ // } catch (CloneNotSupportedException e) {
+ // throw new AssertionError(e);
+ // }
+ // }
+ // }
+
+ // private static void defClone(String name,
+ // final CloneableProperty p) {
+ // map.put(name, new CharPropertyFactory() {
+ // CharProperty make() { return p.clone();}});
+ // }
+
+ // private static final HashMap The stream returned by this method contains each substring of the
+ * input sequence that is terminated by another subsequence that matches
+ * this pattern or is terminated by the end of the input sequence. The
+ * substrings in the stream are in the order in which they occur in the
+ * input. Trailing empty strings will be discarded and not encountered in
+ * the stream.
+ *
+ * If this pattern does not match any subsequence of the input then
+ * the resulting stream has just one element, namely the input sequence in
+ * string form.
+ *
+ * When there is a positive-width match at the beginning of the input
+ * sequence then an empty leading substring is included at the beginning
+ * of the stream. A zero-width match at the beginning however never produces
+ * such empty leading substring.
+ *
+ * If the input sequence is mutable, it must remain constant during the
+ * execution of the terminal stream operation. Otherwise, the result of the
+ * terminal stream operation is undefined.
+ *
+ * @param input
+ * The character sequence to be split
+ *
+ * @return The stream of strings computed by splitting the input
+ * around matches of this pattern
+ * @see #split(CharSequence)
+ * @since 1.8
+ *
+ * @diffblue.untested
+ * @diffblue.noSupport
+ */
+ public Stream
+ * {@code new Boolean("yes")} produces a {@code Boolean} object
+ * that represents {@code false}.
+ *
+ * @param s the string to be converted to a {@code Boolean}.
+ */
+ public Boolean(String s) {
+ this(parseBoolean(s));
+ }
+
+ /**
+ * Parses the string argument as a boolean. The {@code boolean}
+ * returned represents the value {@code true} if the string argument
+ * is not {@code null} and is equal, ignoring case, to the string
+ * {@code "true"}.
+ * Example: {@code Boolean.parseBoolean("yes")} returns {@code false}.
+ *
+ * @param s the {@code String} containing the boolean
+ * representation to be parsed
+ * @return the boolean represented by the string argument
+ * @since 1.5
+ */
+ public static boolean parseBoolean(String s) {
+ return ((s != null) && s.equalsIgnoreCase("true"));
+ }
+
+ /**
+ * Returns the value of this {@code Boolean} object as a boolean
+ * primitive.
+ *
+ * @return the primitive {@code boolean} value of this object.
+ */
+ public boolean booleanValue() {
+ return value;
+ }
+
+ /**
+ * Returns a {@code Boolean} instance representing the specified
+ * {@code boolean} value. If the specified {@code boolean} value
+ * is {@code true}, this method returns {@code Boolean.TRUE};
+ * if it is {@code false}, this method returns {@code Boolean.FALSE}.
+ * If a new {@code Boolean} instance is not required, this method
+ * should generally be used in preference to the constructor
+ * {@link #Boolean(boolean)}, as this method is likely to yield
+ * significantly better space and time performance.
+ *
+ * @param b a boolean value.
+ * @return a {@code Boolean} instance representing {@code b}.
+ * @since 1.4
+ */
+ public static Boolean valueOf(boolean b) {
+ return (b ? TRUE : FALSE);
+ }
+
+ /**
+ * Returns a {@code Boolean} with a value represented by the
+ * specified string. The {@code Boolean} returned represents a
+ * true value if the string argument is not {@code null}
+ * and is equal, ignoring case, to the string {@code "true"}.
+ *
+ * @param s a string.
+ * @return the {@code Boolean} value represented by the string.
+ */
+ public static Boolean valueOf(String s) {
+ return parseBoolean(s) ? TRUE : FALSE;
+ }
+
+ /**
+ * Returns a {@code String} object representing the specified
+ * boolean. If the specified boolean is {@code true}, then
+ * the string {@code "true"} will be returned, otherwise the
+ * string {@code "false"} will be returned.
+ *
+ * @param b the boolean to be converted
+ * @return the string representation of the specified {@code boolean}
+ * @since 1.4
+ */
+ public static String toString(boolean b) {
+ return b ? "true" : "false";
+ }
+
+ /**
+ * Returns a {@code String} object representing this Boolean's
+ * value. If this object represents the value {@code true},
+ * a string equal to {@code "true"} is returned. Otherwise, a
+ * string equal to {@code "false"} is returned.
+ *
+ * @return a string representation of this object.
+ */
+ public String toString() {
+ return value ? "true" : "false";
+ }
+
+ /**
+ * Returns a hash code for this {@code Boolean} object.
+ *
+ * @return the integer {@code 1231} if this object represents
+ * {@code true}; returns the integer {@code 1237} if this
+ * object represents {@code false}.
+ */
+ @Override
+ public int hashCode() {
+ return Boolean.hashCode(value);
+ }
+
+ /**
+ * Returns a hash code for a {@code boolean} value; compatible with
+ * {@code Boolean.hashCode()}.
+ *
+ * @param value the value to hash
+ * @return a hash code value for a {@code boolean} value.
+ * @since 1.8
+ */
+ public static int hashCode(boolean value) {
+ return value ? 1231 : 1237;
+ }
+
+ /**
+ * Returns {@code true} if and only if the argument is not
+ * {@code null} and is a {@code Boolean} object that
+ * represents the same {@code boolean} value as this object.
+ *
+ * @param obj the object to compare with.
+ * @return {@code true} if the Boolean objects represent the
+ * same value; {@code false} otherwise.
+ */
+ public boolean equals(Object obj) {
+ if (obj instanceof Boolean) {
+ return value == ((Boolean)obj).booleanValue();
+ }
+ return false;
+ }
+
+ /**
+ * Returns {@code true} if and only if the system property
+ * named by the argument exists and is equal to the string
+ * {@code "true"}. (Beginning with version 1.0.2 of the
+ * JavaTM platform, the test of
+ * this string is case insensitive.) A system property is accessible
+ * through {@code getProperty}, a method defined by the
+ * {@code System} class.
+ *
+ * Boolean.valueOf(x).compareTo(Boolean.valueOf(y))
+ *
+ *
+ * @param x the first {@code boolean} to compare
+ * @param y the second {@code boolean} to compare
+ * @return the value {@code 0} if {@code x == y};
+ * a value less than {@code 0} if {@code !x && y}; and
+ * a value greater than {@code 0} if {@code x && !y}
+ * @since 1.7
+ */
+ public static int compare(boolean x, boolean y) {
+ return (x == y) ? 0 : (x ? 1 : -1);
+ }
+
+ /**
+ * Returns the result of applying the logical AND operator to the
+ * specified {@code boolean} operands.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the logical AND of {@code a} and {@code b}
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static boolean logicalAnd(boolean a, boolean b) {
+ return a && b;
+ }
+
+ /**
+ * Returns the result of applying the logical OR operator to the
+ * specified {@code boolean} operands.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the logical OR of {@code a} and {@code b}
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static boolean logicalOr(boolean a, boolean b) {
+ return a || b;
+ }
+
+ /**
+ * Returns the result of applying the logical XOR operator to the
+ * specified {@code boolean} operands.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the logical XOR of {@code a} and {@code b}
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static boolean logicalXor(boolean a, boolean b) {
+ return a ^ b;
+ }
+}
diff --git a/src/main/java/java/lang/Byte.java b/src/main/java/java/lang/Byte.java
new file mode 100644
index 0000000..5901176
--- /dev/null
+++ b/src/main/java/java/lang/Byte.java
@@ -0,0 +1,510 @@
+/*
+ * Copyright (c) 1996, 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.lang;
+
+import org.cprover.CProver;
+
+/**
+ *
+ * The {@code Byte} class wraps a value of primitive type {@code byte}
+ * in an object. An object of type {@code Byte} contains a single
+ * field whose type is {@code byte}.
+ *
+ *
+ *
+ *
+ * @param s the {@code String} containing the
+ * {@code byte}
+ * representation to be parsed
+ * @param radix the radix to be used while parsing {@code s}
+ * @return the {@code byte} value represented by the string
+ * argument in the specified radix
+ * @throws NumberFormatException If the string does
+ * not contain a parsable {@code byte}.
+ */
+ public static byte parseByte(String s, int radix)
+ throws NumberFormatException {
+ int i = Integer.parseInt(s, radix);
+ if (i < MIN_VALUE || i > MAX_VALUE)
+ throw new NumberFormatException(
+ "Value out of range. Value:\"" + s + "\" Radix:" + radix);
+ return (byte)i;
+ }
+
+ /**
+ * Parses the string argument as a signed decimal {@code
+ * byte}. The characters in the string must all be decimal digits,
+ * except that the first character may be an ASCII minus sign
+ * {@code '-'} ({@code '\u005Cu002D'}) to indicate a negative
+ * value or an ASCII plus sign {@code '+'}
+ * ({@code '\u005Cu002B'}) to indicate a positive value. The
+ * resulting {@code byte} value is returned, exactly as if the
+ * argument and the radix 10 were given as arguments to the {@link
+ * #parseByte(java.lang.String, int)} method.
+ *
+ * @param s a {@code String} containing the
+ * {@code byte} representation to be parsed
+ * @return the {@code byte} value represented by the
+ * argument in decimal
+ * @throws NumberFormatException if the string does not
+ * contain a parsable {@code byte}.
+ */
+ public static byte parseByte(String s) throws NumberFormatException {
+ return CProver.nondetByte(); //The function is handled by cbmc internally
+ }
+
+ /**
+ * Returns a {@code Byte} object holding the value
+ * extracted from the specified {@code String} when parsed
+ * with the radix given by the second argument. The first argument
+ * is interpreted as representing a signed {@code byte} in
+ * the radix specified by the second argument, exactly as if the
+ * argument were given to the {@link #parseByte(java.lang.String,
+ * int)} method. The result is a {@code Byte} object that
+ * represents the {@code byte} value specified by the string.
+ *
+ *
+ * {@code new Byte(Byte.parseByte(s, radix))}
+ *
+ *
+ * @param s the string to be parsed
+ * @param radix the radix to be used in interpreting {@code s}
+ * @return a {@code Byte} object holding the value
+ * represented by the string argument in the
+ * specified radix.
+ * @throws NumberFormatException If the {@code String} does
+ * not contain a parsable {@code byte}.
+ */
+ public static Byte valueOf(String s, int radix)
+ throws NumberFormatException {
+ return valueOf(parseByte(s, radix));
+ }
+
+ /**
+ * Returns a {@code Byte} object holding the value
+ * given by the specified {@code String}. The argument is
+ * interpreted as representing a signed decimal {@code byte},
+ * exactly as if the argument were given to the {@link
+ * #parseByte(java.lang.String)} method. The result is a
+ * {@code Byte} object that represents the {@code byte}
+ * value specified by the string.
+ *
+ *
+ * {@code new Byte(Byte.parseByte(s))}
+ *
+ *
+ * @param s the string to be parsed
+ * @return a {@code Byte} object holding the value
+ * represented by the string argument
+ * @throws NumberFormatException If the {@code String} does
+ * not contain a parsable {@code byte}.
+ */
+ public static Byte valueOf(String s) throws NumberFormatException {
+ return valueOf(s, 10);
+ }
+
+ /**
+ * Decodes a {@code String} into a {@code Byte}.
+ * Accepts decimal, hexadecimal, and octal numbers given by
+ * the following grammar:
+ *
+ *
+ *
+ *
+ * DecimalNumeral, HexDigits, and OctalDigits
+ * are as defined in section 3.10.1 of
+ * The Java™ Language Specification,
+ * except that underscores are not accepted between digits.
+ *
+ *
+ *
+ *
+ * Byte.valueOf(x).compareTo(Byte.valueOf(y))
+ *
+ *
+ * @param x the first {@code byte} to compare
+ * @param y the second {@code byte} to compare
+ * @return the value {@code 0} if {@code x == y};
+ * a value less than {@code 0} if {@code x < y}; and
+ * a value greater than {@code 0} if {@code x > y}
+ * @since 1.7
+ */
+ public static int compare(byte x, byte y) {
+ return x - y;
+ }
+
+ /**
+ * Converts the argument to an {@code int} by an unsigned
+ * conversion. In an unsigned conversion to an {@code int}, the
+ * high-order 24 bits of the {@code int} are zero and the
+ * low-order 8 bits are equal to the bits of the {@code byte} argument.
+ *
+ * Consequently, zero and positive {@code byte} values are mapped
+ * to a numerically equal {@code int} value and negative {@code
+ * byte} values are mapped to an {@code int} value equal to the
+ * input plus 28.
+ *
+ * @param x the value to convert to an unsigned {@code int}
+ * @return the argument converted to {@code int} by an unsigned
+ * conversion
+ * @since 1.8
+ */
+ public static int toUnsignedInt(byte x) {
+ return ((int) x) & 0xff;
+ }
+
+ /**
+ * Converts the argument to a {@code long} by an unsigned
+ * conversion. In an unsigned conversion to a {@code long}, the
+ * high-order 56 bits of the {@code long} are zero and the
+ * low-order 8 bits are equal to the bits of the {@code byte} argument.
+ *
+ * Consequently, zero and positive {@code byte} values are mapped
+ * to a numerically equal {@code long} value and negative {@code
+ * byte} values are mapped to a {@code long} value equal to the
+ * input plus 28.
+ *
+ * @param x the value to convert to an unsigned {@code long}
+ * @return the argument converted to {@code long} by an unsigned
+ * conversion
+ * @since 1.8
+ */
+ public static long toUnsignedLong(byte x) {
+ return ((long) x) & 0xffL;
+ }
+
+
+ /**
+ * The number of bits used to represent a {@code byte} value in two's
+ * complement binary form.
+ *
+ * @since 1.5
+ */
+ public static final int SIZE = 8;
+
+ /**
+ * The number of bytes used to represent a {@code byte} value in two's
+ * complement binary form.
+ *
+ * @since 1.8
+ */
+ public static final int BYTES = SIZE / Byte.SIZE;
+
+ /** use serialVersionUID from JDK 1.1. for interoperability */
+ private static final long serialVersionUID = -7183698231559129828L;
+}
diff --git a/src/main/java/java/lang/Character.java b/src/main/java/java/lang/Character.java
index 8952165..75a15f7 100644
--- a/src/main/java/java/lang/Character.java
+++ b/src/main/java/java/lang/Character.java
@@ -25,13 +25,13 @@
package java.lang;
-import org.cprover.CProver;
-
import java.util.Arrays;
import java.util.Map;
import java.util.HashMap;
import java.util.Locale;
+import org.cprover.CProver;
+
/**
* The {@code Character} class wraps a value of the primitive
* type {@code char} in an object. An object of type
@@ -7217,8 +7217,15 @@ public static char reverseBytes(char ch) {
* code point.
*
* @since 1.7
+ *
+ * @diffblue.limitedSupport Only works for capital latin letters.
*/
public static String getName(int codePoint) {
+ if (!isValidCodePoint(codePoint)) {
+ throw new IllegalArgumentException();
+ }
+ // DIFFBLUE MODEL LIBRARY
+ // removed for compatibility with Java 9 and newer
// if (!isValidCodePoint(codePoint)) {
// throw new IllegalArgumentException();
// }
@@ -7233,7 +7240,13 @@ public static String getName(int codePoint) {
// + Integer.toHexString(codePoint).toUpperCase(Locale.ENGLISH);
// // should never come here
// return Integer.toHexString(codePoint).toUpperCase(Locale.ENGLISH);
- CProver.notModelled();
- return CProver.nondetWithoutNullForNotModelled();
+ return cproverGetNameRestricted(codePoint);
}
+
+ public static String cproverGetNameRestricted(int codePoint)
+ {
+ CProver.assume(codePoint >= 65 && codePoint <= 90);
+ return "LATIN CAPITAL LETTER " + ((char) codePoint);
+ }
+
}
diff --git a/src/main/java/java/lang/Class.java b/src/main/java/java/lang/Class.java
index b8ad087..9a6350a 100644
--- a/src/main/java/java/lang/Class.java
+++ b/src/main/java/java/lang/Class.java
@@ -25,14 +25,19 @@
package java.lang;
+import java.lang.reflect.Field;
+import java.lang.reflect.Method;
import java.util.HashMap;
import java.util.Map;
+import org.cprover.CProverString;
+
+// DIFFBLUE MODEL LIBRARY
+// removed for compatibility with Java 9 and newer
// import sun.reflect.CallerSensitive;
// import sun.reflect.Reflection;
import org.cprover.CProver;
-import org.cprover.CProverString;
public final class Class
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ * How many digits must be printed for the fractional part of
+ * m or a? There must be at least one digit to represent
+ * the fractional part, and beyond that as many, but only as many, more
+ * digits as are needed to uniquely distinguish the argument value from
+ * adjacent values of type {@code double}. That is, suppose that
+ * x is the exact mathematical value represented by the decimal
+ * representation produced by this method for a finite nonzero argument
+ * d. Then d must be the {@code double} value nearest
+ * to x; or if two {@code double} values are equally close
+ * to x, then d must be one of them and the least
+ * significant bit of the significand of d must be {@code 0}.
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ * @param d the {@code double} to be converted.
+ * @return a hex string representation of the argument.
+ * @since 1.5
+ * @author Joseph D. Darcy
+ */
+ public static String toHexString(double d) {
+ /*
+ * Modeled after the "a" conversion specifier in C99, section
+ * 7.19.6.1; however, the output of this method is more
+ * tightly specified.
+ */
+ if (!isFinite(d) )
+ // For infinity and NaN, use the decimal output.
+ return Double.toString(d);
+ else {
+ // Initialized to maximum size of output.
+ StringBuilder answer = new StringBuilder(24);
+
+ if (Math.copySign(1.0, d) == -1.0) // value is negative,
+ answer.append("-"); // so append sign info
+
+ answer.append("0x");
+
+ d = Math.abs(d);
+
+ if(d == 0.0) {
+ answer.append("0.0p0");
+ } else {
+ boolean subnormal = (d < DoubleConsts.MIN_NORMAL);
+
+ // Isolate significand bits and OR in a high-order bit
+ // so that the string representation has a known
+ // length.
+ long signifBits = (Double.doubleToLongBits(d)
+ & DoubleConsts.SIGNIF_BIT_MASK) |
+ 0x1000000000000000L;
+
+ // Subnormal values have a 0 implicit bit; normal
+ // values have a 1 implicit bit.
+ answer.append(subnormal ? "0." : "1.");
+
+ // Isolate the low-order 13 digits of the hex
+ // representation. If all the digits are zero,
+ // replace with a single 0; otherwise, remove all
+ // trailing zeros.
+ String signif = CProverString.substring(Long.toHexString(signifBits), 3, 16);
+ answer.append(signif.equals("0000000000000") ? // 13 zeros
+ "0":
+ signif.replaceFirst("0{1,12}$", ""));
+
+ answer.append('p');
+ // If the value is subnormal, use the E_min exponent
+ // value for double; otherwise, extract and report d's
+ // exponent (the representation of a subnormal uses
+ // E_min -1).
+ answer.append(subnormal ?
+ DoubleConsts.MIN_EXPONENT:
+ Math.getExponent(d));
+ }
+ return answer.toString();
+ }
+ }
+
+ /**
+ * Returns a {@code Double} object holding the
+ * {@code double} value represented by the argument string
+ * {@code s}.
+ *
+ * Floating-point Value Hexadecimal String
+ * {@code 1.0} {@code 0x1.0p0}
+ * {@code -1.0} {@code -0x1.0p0}
+ * {@code 2.0} {@code 0x1.0p1}
+ * {@code 3.0} {@code 0x1.8p1}
+ * {@code 0.5} {@code 0x1.0p-1}
+ * {@code 0.25} {@code 0x1.0p-2}
+ * {@code Double.MAX_VALUE}
+ * {@code 0x1.fffffffffffffp1023}
+ * {@code Minimum Normal Value}
+ * {@code 0x1.0p-1022}
+ * {@code Maximum Subnormal Value}
+ * {@code 0x0.fffffffffffffp-1022}
+ * {@code Double.MIN_VALUE}
+ * {@code 0x0.0000000000001p-1022}
+ *
+ *
+ *
+ * where Sign, FloatingPointLiteral,
+ * HexNumeral, HexDigits, SignedInteger and
+ * FloatTypeSuffix are as defined in the lexical structure
+ * sections of
+ * The Java™ Language Specification,
+ * except that underscores are not accepted between digits.
+ * If {@code s} does not have the form of
+ * a FloatValue, then a {@code NumberFormatException}
+ * is thrown. Otherwise, {@code s} is regarded as
+ * representing an exact decimal value in the usual
+ * "computerized scientific notation" or as an exact
+ * hexadecimal value; this exact numerical value is then
+ * conceptually converted to an "infinitely precise"
+ * binary value that is then rounded to type {@code double}
+ * by the usual round-to-nearest rule of IEEE 754 floating-point
+ * arithmetic, which includes preserving the sign of a zero
+ * value.
+ *
+ * Note that the round-to-nearest rule also implies overflow and
+ * underflow behaviour; if the exact value of {@code s} is large
+ * enough in magnitude (greater than or equal to ({@link
+ * #MAX_VALUE} + {@link Math#ulp(double) ulp(MAX_VALUE)}/2),
+ * rounding to {@code double} will result in an infinity and if the
+ * exact value of {@code s} is small enough in magnitude (less
+ * than or equal to {@link #MIN_VALUE}/2), rounding to float will
+ * result in a zero.
+ *
+ * Finally, after rounding a {@code Double} object representing
+ * this {@code double} value is returned.
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ * {@code
+ * final String Digits = "(\\p{Digit}+)";
+ * final String HexDigits = "(\\p{XDigit}+)";
+ * // an exponent is 'e' or 'E' followed by an optionally
+ * // signed decimal integer.
+ * final String Exp = "[eE][+-]?"+Digits;
+ * final String fpRegex =
+ * ("[\\x00-\\x20]*"+ // Optional leading "whitespace"
+ * "[+-]?(" + // Optional sign character
+ * "NaN|" + // "NaN" string
+ * "Infinity|" + // "Infinity" string
+ *
+ * // A decimal floating-point string representing a finite positive
+ * // number without a leading sign has at most five basic pieces:
+ * // Digits . Digits ExponentPart FloatTypeSuffix
+ * //
+ * // Since this method allows integer-only strings as input
+ * // in addition to strings of floating-point literals, the
+ * // two sub-patterns below are simplifications of the grammar
+ * // productions from section 3.10.2 of
+ * // The Java Language Specification.
+ *
+ * // Digits ._opt Digits_opt ExponentPart_opt FloatTypeSuffix_opt
+ * "((("+Digits+"(\\.)?("+Digits+"?)("+Exp+")?)|"+
+ *
+ * // . Digits ExponentPart_opt FloatTypeSuffix_opt
+ * "(\\.("+Digits+")("+Exp+")?)|"+
+ *
+ * // Hexadecimal strings
+ * "((" +
+ * // 0[xX] HexDigits ._opt BinaryExponent FloatTypeSuffix_opt
+ * "(0[xX]" + HexDigits + "(\\.)?)|" +
+ *
+ * // 0[xX] HexDigits_opt . HexDigits BinaryExponent FloatTypeSuffix_opt
+ * "(0[xX]" + HexDigits + "?(\\.)" + HexDigits + ")" +
+ *
+ * ")[pP][+-]?" + Digits + "))" +
+ * "[fFdD]?))" +
+ * "[\\x00-\\x20]*");// Optional trailing "whitespace"
+ *
+ * if (Pattern.matches(fpRegex, myString))
+ * Double.valueOf(myString); // Will not throw NumberFormatException
+ * else {
+ * // Perform suitable alternative action
+ * }
+ * }
+ *
+ * @param s the string to be parsed.
+ * @return a {@code Double} object holding the value
+ * represented by the {@code String} argument.
+ * @throws NumberFormatException if the string does not contain a
+ * parsable number.
+ */
+ public static Double valueOf(String s) throws NumberFormatException {
+ return new Double(parseDouble(s));
+ }
+
+ /**
+ * Returns a {@code Double} instance representing the specified
+ * {@code double} value.
+ * If a new {@code Double} instance is not required, this method
+ * should generally be used in preference to the constructor
+ * {@link #Double(double)}, as this method is likely to yield
+ * significantly better space and time performance by caching
+ * frequently requested values.
+ *
+ * @param d a double value.
+ * @return a {@code Double} instance representing {@code d}.
+ * @since 1.5
+ */
+ public static Double valueOf(double d) {
+ return new Double(d);
+ }
+
+ /**
+ * Returns a new {@code double} initialized to the value
+ * represented by the specified {@code String}, as performed
+ * by the {@code valueOf} method of class
+ * {@code Double}.
+ *
+ * @param s the string to be parsed.
+ * @return the {@code double} value represented by the string
+ * argument.
+ * @throws NullPointerException if the string is null
+ * @throws NumberFormatException if the string does not contain
+ * a parsable {@code double}.
+ * @see java.lang.Double#valueOf(String)
+ * @since 1.2
+ *
+ * @diffblue.noSupport
+ */
+ public static double parseDouble(String s) throws NumberFormatException {
+ CProver.notModelled();
+ return CProver.nondetDouble();
+ }
+
+ /**
+ * Returns {@code true} if the specified number is a
+ * Not-a-Number (NaN) value, {@code false} otherwise.
+ *
+ * @param v the value to be tested.
+ * @return {@code true} if the value of the argument is NaN;
+ * {@code false} otherwise.
+ */
+ public static boolean isNaN(double v) {
+ return (v != v);
+ }
+
+ /**
+ * Returns {@code true} if the specified number is infinitely
+ * large in magnitude, {@code false} otherwise.
+ *
+ * @param v the value to be tested.
+ * @return {@code true} if the value of the argument is positive
+ * infinity or negative infinity; {@code false} otherwise.
+ */
+ public static boolean isInfinite(double v) {
+ return (v == POSITIVE_INFINITY) || (v == NEGATIVE_INFINITY);
+ }
+
+ /**
+ * Returns {@code true} if the argument is a finite floating-point
+ * value; returns {@code false} otherwise (for NaN and infinity
+ * arguments).
+ *
+ * @param d the {@code double} value to be tested
+ * @return {@code true} if the argument is a finite
+ * floating-point value, {@code false} otherwise.
+ * @since 1.8
+ */
+ public static boolean isFinite(double d) {
+ return DoubleConsts.MIN_VALUE <= d && d <= DoubleConsts.MAX_VALUE;
+ }
+
+ /**
+ * The value of the Double.
+ *
+ * @serial
+ */
+ private final double value;
+
+ /**
+ * Constructs a newly allocated {@code Double} object that
+ * represents the primitive {@code double} argument.
+ *
+ * @param value the value to be represented by the {@code Double}.
+ */
+ public Double(double value) {
+ this.value = value;
+ }
+
+ /**
+ * Constructs a newly allocated {@code Double} object that
+ * represents the floating-point value of type {@code double}
+ * represented by the string. The string is converted to a
+ * {@code double} value as if by the {@code valueOf} method.
+ *
+ * @param s a string to be converted to a {@code Double}.
+ * @throws NumberFormatException if the string does not contain a
+ * parsable number.
+ * @see java.lang.Double#valueOf(java.lang.String)
+ */
+ public Double(String s) throws NumberFormatException {
+ value = parseDouble(s);
+ }
+
+ /**
+ * Returns {@code true} if this {@code Double} value is
+ * a Not-a-Number (NaN), {@code false} otherwise.
+ *
+ * @return {@code true} if the value represented by this object is
+ * NaN; {@code false} otherwise.
+ */
+ public boolean isNaN() {
+ return isNaN(value);
+ }
+
+ /**
+ * Returns {@code true} if this {@code Double} value is
+ * infinitely large in magnitude, {@code false} otherwise.
+ *
+ * @return {@code true} if the value represented by this object is
+ * positive infinity or negative infinity;
+ * {@code false} otherwise.
+ */
+ public boolean isInfinite() {
+ return isInfinite(value);
+ }
+
+ /**
+ * Returns a string representation of this {@code Double} object.
+ * The primitive {@code double} value represented by this
+ * object is converted to a string exactly as if by the method
+ * {@code toString} of one argument.
+ *
+ * @return a {@code String} representation of this object.
+ * @see java.lang.Double#toString(double)
+ */
+ public String toString() {
+ return toString(value);
+ }
+
+ /**
+ * Returns the value of this {@code Double} as a {@code byte}
+ * after a narrowing primitive conversion.
+ *
+ * @return the {@code double} value represented by this object
+ * converted to type {@code byte}
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ * @since JDK1.1
+ */
+ public byte byteValue() {
+ return (byte)value;
+ }
+
+ /**
+ * Returns the value of this {@code Double} as a {@code short}
+ * after a narrowing primitive conversion.
+ *
+ * @return the {@code double} value represented by this object
+ * converted to type {@code short}
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ * @since JDK1.1
+ */
+ public short shortValue() {
+ return (short)value;
+ }
+
+ /**
+ * Returns the value of this {@code Double} as an {@code int}
+ * after a narrowing primitive conversion.
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ *
+ * @return the {@code double} value represented by this object
+ * converted to type {@code int}
+ */
+ public int intValue() {
+ return (int)value;
+ }
+
+ /**
+ * Returns the value of this {@code Double} as a {@code long}
+ * after a narrowing primitive conversion.
+ *
+ * @return the {@code double} value represented by this object
+ * converted to type {@code long}
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ */
+ public long longValue() {
+ return (long)value;
+ }
+
+ /**
+ * Returns the value of this {@code Double} as a {@code float}
+ * after a narrowing primitive conversion.
+ *
+ * @return the {@code double} value represented by this object
+ * converted to type {@code float}
+ * @jls 5.1.3 Narrowing Primitive Conversions
+ * @since JDK1.0
+ */
+ public float floatValue() {
+ return (float)value;
+ }
+
+ /**
+ * Returns the {@code double} value of this {@code Double} object.
+ *
+ * @return the {@code double} value represented by this object
+ */
+ public double doubleValue() {
+ return value;
+ }
+
+ /**
+ * Returns a hash code for this {@code Double} object. The
+ * result is the exclusive OR of the two halves of the
+ * {@code long} integer bit representation, exactly as
+ * produced by the method {@link #doubleToLongBits(double)}, of
+ * the primitive {@code double} value represented by this
+ * {@code Double} object. That is, the hash code is the value
+ * of the expression:
+ *
+ *
+ * {@code (int)(v^(v>>>32))}
+ *
+ *
+ * where {@code v} is defined by:
+ *
+ *
+ * {@code long v = Double.doubleToLongBits(this.doubleValue());}
+ *
+ *
+ * @return a {@code hash code} value for this object.
+ */
+ @Override
+ public int hashCode() {
+ // return Double.hashCode(value);
+ return 0;
+ }
+
+ /**
+ * Returns a hash code for a {@code double} value; compatible with
+ * {@code Double.hashCode()}.
+ *
+ * @param value the value to hash
+ * @return a hash code value for a {@code double} value.
+ * @since 1.8
+ */
+ public static int hashCode(double value) {
+ // long bits = doubleToLongBits(value);
+ // return (int)(bits ^ (bits >>> 32));
+ return 0;
+ }
+
+ /**
+ * Compares this object against the specified object. The result
+ * is {@code true} if and only if the argument is not
+ * {@code null} and is a {@code Double} object that
+ * represents a {@code double} that has the same value as the
+ * {@code double} represented by this object. For this
+ * purpose, two {@code double} values are considered to be
+ * the same if and only if the method {@link
+ * #doubleToLongBits(double)} returns the identical
+ * {@code long} value when applied to each.
+ *
+ *
+ * {@code d1.doubleValue() == d2.doubleValue()}
+ *
+ *
+ *
+ *
+ * This definition allows hash tables to operate properly.
+ * @param obj the object to compare with.
+ * @return {@code true} if the objects are the same;
+ * {@code false} otherwise.
+ * @see java.lang.Double#doubleToLongBits(double)
+ *
+ * @diffblue.fullSupport
+ *
+ * Until the native method doubleToRawLongBits(D) is implemented in
+ * CBMC, this model will allow test generation for checking equality
+ * between two Doubles.
+ */
+ public boolean equals(Object obj) {
+ // return (obj instanceof Double)
+ // && (doubleToLongBits(((Double)obj).value) ==
+ // doubleToLongBits(value));
+
+ // DIFFBLUE MODEL LIBRARY
+ if (!(obj instanceof Double))
+ return false;
+ Double d = (Double) obj;
+ double dValue = d.doubleValue();
+ // We inline isNaN here to avoid calls to a static method
+ boolean bothAreNaN = (dValue != dValue) && (value != value);
+ return bothAreNaN ||(
+ (value == 0.0 && dValue == 0.0)
+ ? ((1/value == POSITIVE_INFINITY && 1/dValue == POSITIVE_INFINITY)
+ || (1/value == NEGATIVE_INFINITY && 1/dValue == NEGATIVE_INFINITY))
+ : ((value == POSITIVE_INFINITY && dValue == POSITIVE_INFINITY)
+ || (value == NEGATIVE_INFINITY && dValue == NEGATIVE_INFINITY)
+ || value == dValue));
+ }
+
+ /**
+ * Returns a representation of the specified floating-point value
+ * according to the IEEE 754 floating-point "double
+ * format" bit layout.
+ *
+ *
+ *
+ * Then the floating-point result equals the value of the mathematical
+ * expression s·m·2e-1075.
+ *
+ * {@code
+ * int s = ((bits >> 63) == 0) ? 1 : -1;
+ * int e = (int)((bits >> 52) & 0x7ffL);
+ * long m = (e == 0) ?
+ * (bits & 0xfffffffffffffL) << 1 :
+ * (bits & 0xfffffffffffffL) | 0x10000000000000L;
+ * }
+ * This ensures that the natural ordering of
+ * {@code Double} objects imposed by this method is consistent
+ * with equals.
+ *
+ * @param anotherDouble the {@code Double} to be compared.
+ * @return the value {@code 0} if {@code anotherDouble} is
+ * numerically equal to this {@code Double}; a value
+ * less than {@code 0} if this {@code Double}
+ * is numerically less than {@code anotherDouble};
+ * and a value greater than {@code 0} if this
+ * {@code Double} is numerically greater than
+ * {@code anotherDouble}.
+ *
+ * @since 1.2
+ */
+ public int compareTo(Double anotherDouble) {
+ return Double.compare(value, anotherDouble.value);
+ }
+
+ /**
+ * Compares the two specified {@code double} values. The sign
+ * of the integer value returned is the same as that of the
+ * integer that would be returned by the call:
+ *
+ * new Double(d1).compareTo(new Double(d2))
+ *
+ *
+ * @param d1 the first {@code double} to compare
+ * @param d2 the second {@code double} to compare
+ * @return the value {@code 0} if {@code d1} is
+ * numerically equal to {@code d2}; a value less than
+ * {@code 0} if {@code d1} is numerically less than
+ * {@code d2}; and a value greater than {@code 0}
+ * if {@code d1} is numerically greater than
+ * {@code d2}.
+ * @since 1.4
+ */
+ public static int compare(double d1, double d2) {
+ if (d1 < d2)
+ return -1; // Neither val is NaN, thisVal is smaller
+ if (d1 > d2)
+ return 1; // Neither val is NaN, thisVal is larger
+
+ // Cannot use doubleToRawLongBits because of possibility of NaNs.
+ long thisBits = Double.doubleToLongBits(d1);
+ long anotherBits = Double.doubleToLongBits(d2);
+
+ return (thisBits == anotherBits ? 0 : // Values are equal
+ (thisBits < anotherBits ? -1 : // (-0.0, 0.0) or (!NaN, NaN)
+ 1)); // (0.0, -0.0) or (NaN, !NaN)
+ }
+
+ /**
+ * Adds two {@code double} values together as per the + operator.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the sum of {@code a} and {@code b}
+ * @jls 4.2.4 Floating-Point Operations
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static double sum(double a, double b) {
+ return a + b;
+ }
+
+ /**
+ * Returns the greater of two {@code double} values
+ * as if by calling {@link Math#max(double, double) Math.max}.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the greater of {@code a} and {@code b}
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static double max(double a, double b) {
+ double result = CProver.nondetDouble();
+ CProver.assume((result == a || result == b) && result >= a && result >= b);
+ return result;
+ }
+
+ /**
+ * Returns the smaller of two {@code double} values
+ * as if by calling {@link Math#min(double, double) Math.min}.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the smaller of {@code a} and {@code b}.
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static double min(double a, double b) {
+ double result = CProver.nondetDouble();
+ CProver.assume((result == a || result == b) && result <= a && result <= b);
+ return result;
+ }
+
+ /** use serialVersionUID from JDK 1.0.2 for interoperability */
+ private static final long serialVersionUID = -9172774392245257468L;
+}
diff --git a/src/main/java/java/lang/Float.java b/src/main/java/java/lang/Float.java
new file mode 100644
index 0000000..1003bcc
--- /dev/null
+++ b/src/main/java/java/lang/Float.java
@@ -0,0 +1,1005 @@
+/*
+ * Copyright (c) 1994, 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.lang;
+
+// DIFFBLUE MODEL LIBRARY
+// removed for compatibility with Java 9 and newer
+// import sun.misc.FloatingDecimal;
+import sun.misc.FloatConsts;
+import sun.misc.DoubleConsts;
+import org.cprover.CProver;
+
+/**
+ * The {@code Float} class wraps a value of primitive type
+ * {@code float} in an object. An object of type
+ * {@code Float} contains a single field whose type is
+ * {@code float}.
+ *
+ *
+ *
+ * How many digits must be printed for the fractional part of
+ * m or a? There must be at least one digit
+ * to represent the fractional part, and beyond that as many, but
+ * only as many, more digits as are needed to uniquely distinguish
+ * the argument value from adjacent values of type
+ * {@code float}. That is, suppose that x is the
+ * exact mathematical value represented by the decimal
+ * representation produced by this method for a finite nonzero
+ * argument f. Then f must be the {@code float}
+ * value nearest to x; or, if two {@code float} values are
+ * equally close to x, then f must be one of
+ * them and the least significant bit of the significand of
+ * f must be {@code 0}.
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ * @param f the {@code float} to be converted.
+ * @return a hex string representation of the argument.
+ * @since 1.5
+ * @author Joseph D. Darcy
+ */
+ public static String toHexString(float f) {
+ if (Math.abs(f) < FloatConsts.MIN_NORMAL
+ && f != 0.0f ) {// float subnormal
+ // Adjust exponent to create subnormal double, then
+ // replace subnormal double exponent with subnormal float
+ // exponent
+ String s = Double.toHexString(Math.scalb((double)f,
+ /* -1022+126 */
+ DoubleConsts.MIN_EXPONENT-
+ FloatConsts.MIN_EXPONENT));
+ return s.replaceFirst("p-1022$", "p-126");
+ }
+ else // double string will be the same as float string
+ return Double.toHexString(f);
+ }
+
+ /**
+ * Returns a {@code Float} object holding the
+ * {@code float} value represented by the argument string
+ * {@code s}.
+ *
+ * Floating-point Value Hexadecimal String
+ * {@code 1.0} {@code 0x1.0p0}
+ * {@code -1.0} {@code -0x1.0p0}
+ * {@code 2.0} {@code 0x1.0p1}
+ * {@code 3.0} {@code 0x1.8p1}
+ * {@code 0.5} {@code 0x1.0p-1}
+ * {@code 0.25} {@code 0x1.0p-2}
+ * {@code Float.MAX_VALUE}
+ * {@code 0x1.fffffep127}
+ * {@code Minimum Normal Value}
+ * {@code 0x1.0p-126}
+ * {@code Maximum Subnormal Value}
+ * {@code 0x0.fffffep-126}
+ * {@code Float.MIN_VALUE}
+ * {@code 0x0.000002p-126}
+ *
+ *
+ *
+ * where Sign, FloatingPointLiteral,
+ * HexNumeral, HexDigits, SignedInteger and
+ * FloatTypeSuffix are as defined in the lexical structure
+ * sections of
+ * The Java™ Language Specification,
+ * except that underscores are not accepted between digits.
+ * If {@code s} does not have the form of
+ * a FloatValue, then a {@code NumberFormatException}
+ * is thrown. Otherwise, {@code s} is regarded as
+ * representing an exact decimal value in the usual
+ * "computerized scientific notation" or as an exact
+ * hexadecimal value; this exact numerical value is then
+ * conceptually converted to an "infinitely precise"
+ * binary value that is then rounded to type {@code float}
+ * by the usual round-to-nearest rule of IEEE 754 floating-point
+ * arithmetic, which includes preserving the sign of a zero
+ * value.
+ *
+ * Note that the round-to-nearest rule also implies overflow and
+ * underflow behaviour; if the exact value of {@code s} is large
+ * enough in magnitude (greater than or equal to ({@link
+ * #MAX_VALUE} + {@link Math#ulp(float) ulp(MAX_VALUE)}/2),
+ * rounding to {@code float} will result in an infinity and if the
+ * exact value of {@code s} is small enough in magnitude (less
+ * than or equal to {@link #MIN_VALUE}/2), rounding to float will
+ * result in a zero.
+ *
+ * Finally, after rounding a {@code Float} object representing
+ * this {@code float} value is returned.
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ * {@code "1.00000017881393421514957253748434595763683319091796875001d"}
+ * results in the {@code float} value
+ * {@code 1.0000002f}; if the string is converted directly to
+ * {@code float}, 1.0000001f results.
+ *
+ *
+ *
+ *
+ * f1.floatValue() == f2.floatValue()
+ *
+ *
+ *
+ * This definition allows hash tables to operate properly.
+ *
+ * @param obj the object to be compared
+ * @return {@code true} if the objects are the same;
+ * {@code false} otherwise.
+ * @see java.lang.Float#floatToIntBits(float)
+ *
+ * @diffblue.fullSupport
+ *
+ * Until the native method floatToRawIntBits(F) is implemented in
+ * CBMC, this model will allow test generation for checking equality
+ * between two Floats.
+ */
+ public boolean equals(Object obj) {
+ // return (obj instanceof Float)
+ // && (floatToIntBits(((Float)obj).value) == floatToIntBits(value));
+
+ // DIFFBLUE MODEL LIBRARY
+ if (!(obj instanceof Float))
+ return false;
+ Float f = (Float) obj;
+ float fValue = f.floatValue();
+ // We inline isNaN here to avoid calls to a static method
+ boolean bothAreNaN = (value != value) && (fValue != fValue);
+ return bothAreNaN ||
+ ((value == 0.0 && fValue == 0.0)
+ ? ((1/value == POSITIVE_INFINITY && 1/fValue == POSITIVE_INFINITY)
+ || (1/value == NEGATIVE_INFINITY && 1/fValue == NEGATIVE_INFINITY))
+ : ((value == POSITIVE_INFINITY && fValue == POSITIVE_INFINITY)
+ || (value == NEGATIVE_INFINITY && fValue == NEGATIVE_INFINITY)
+ || value == fValue));
+ }
+
+ /**
+ * Returns a representation of the specified floating-point value
+ * according to the IEEE 754 floating-point "single format" bit
+ * layout.
+ *
+ *
+ *
+ * Then the floating-point result equals the value of the mathematical
+ * expression s·m·2e-150.
+ *
+ * {@code
+ * int s = ((bits >> 31) == 0) ? 1 : -1;
+ * int e = ((bits >> 23) & 0xff);
+ * int m = (e == 0) ?
+ * (bits & 0x7fffff) << 1 :
+ * (bits & 0x7fffff) | 0x800000;
+ * }
+ *
+ * This ensures that the natural ordering of {@code Float}
+ * objects imposed by this method is consistent with equals.
+ *
+ * @param anotherFloat the {@code Float} to be compared.
+ * @return the value {@code 0} if {@code anotherFloat} is
+ * numerically equal to this {@code Float}; a value
+ * less than {@code 0} if this {@code Float}
+ * is numerically less than {@code anotherFloat};
+ * and a value greater than {@code 0} if this
+ * {@code Float} is numerically greater than
+ * {@code anotherFloat}.
+ *
+ * @since 1.2
+ * @see Comparable#compareTo(Object)
+ */
+ public int compareTo(Float anotherFloat) {
+ return Float.compare(value, anotherFloat.value);
+ }
+
+ /**
+ * Compares the two specified {@code float} values. The sign
+ * of the integer value returned is the same as that of the
+ * integer that would be returned by the call:
+ *
+ * new Float(f1).compareTo(new Float(f2))
+ *
+ *
+ * @param f1 the first {@code float} to compare.
+ * @param f2 the second {@code float} to compare.
+ * @return the value {@code 0} if {@code f1} is
+ * numerically equal to {@code f2}; a value less than
+ * {@code 0} if {@code f1} is numerically less than
+ * {@code f2}; and a value greater than {@code 0}
+ * if {@code f1} is numerically greater than
+ * {@code f2}.
+ * @since 1.4
+ */
+ public static int compare(float f1, float f2) {
+ if (f1 < f2)
+ return -1; // Neither val is NaN, thisVal is smaller
+ if (f1 > f2)
+ return 1; // Neither val is NaN, thisVal is larger
+
+ // Cannot use floatToRawIntBits because of possibility of NaNs.
+ int thisBits = Float.floatToIntBits(f1);
+ int anotherBits = Float.floatToIntBits(f2);
+
+ return (thisBits == anotherBits ? 0 : // Values are equal
+ (thisBits < anotherBits ? -1 : // (-0.0, 0.0) or (!NaN, NaN)
+ 1)); // (0.0, -0.0) or (NaN, !NaN)
+ }
+
+ /**
+ * Adds two {@code float} values together as per the + operator.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the sum of {@code a} and {@code b}
+ * @jls 4.2.4 Floating-Point Operations
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static float sum(float a, float b) {
+ return a + b;
+ }
+
+ /**
+ * Returns the greater of two {@code float} values
+ * as if by calling {@link Math#max(float, float) Math.max}.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the greater of {@code a} and {@code b}
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static float max(float a, float b) {
+ float result = CProver.nondetFloat();
+ CProver.assume((result == a || result == b) && result >= a && result >= b);
+ return result;
+ }
+
+ /**
+ * Returns the smaller of two {@code float} values
+ * as if by calling {@link Math#min(float, float) Math.min}.
+ *
+ * @param a the first operand
+ * @param b the second operand
+ * @return the smaller of {@code a} and {@code b}
+ * @see java.util.function.BinaryOperator
+ * @since 1.8
+ */
+ public static float min(float a, float b) {
+ float result = CProver.nondetFloat();
+ CProver.assume((result == a || result == b) && result <= a && result <= b);
+ return result;
+ }
+
+ /** use serialVersionUID from JDK 1.0.2 for interoperability */
+ private static final long serialVersionUID = -2671257302660747028L;
+}
diff --git a/src/main/java/java/lang/Long.java b/src/main/java/java/lang/Long.java
new file mode 100644
index 0000000..4cc5e3f
--- /dev/null
+++ b/src/main/java/java/lang/Long.java
@@ -0,0 +1,1537 @@
+/*
+ * Copyright (c) 1994, 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.lang;
+
+import java.lang.annotation.Native;
+import java.math.*;
+import org.cprover.CProver;
+import org.cprover.CProverString;
+
+/**
+ * The {@code Long} class wraps a value of the primitive type {@code
+ * long} in an object. An object of type {@code Long} contains a
+ * single field whose type is {@code long}.
+ *
+ *
+ * {@code 0123456789abcdefghijklmnopqrstuvwxyz}
+ *
+ *
+ * These are {@code '\u005Cu0030'} through
+ * {@code '\u005Cu0039'} and {@code '\u005Cu0061'} through
+ * {@code '\u005Cu007a'}. If {@code radix} is
+ * N, then the first N of these characters
+ * are used as radix-N digits in the order shown. Thus,
+ * the digits for hexadecimal (radix 16) are
+ * {@code 0123456789abcdef}. If uppercase letters are
+ * desired, the {@link java.lang.String#toUpperCase()} method may
+ * be called on the result:
+ *
+ *
+ * {@code Long.toString(n, 16).toUpperCase()}
+ *
+ *
+ * @param i 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.
+ * @see java.lang.Character#MAX_RADIX
+ * @see java.lang.Character#MIN_RADIX
+ */
+ public static String toString(long i, int radix) {
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+ /**
+ * Returns a string representation of the first argument as an
+ * unsigned integer value in the radix specified by the second
+ * argument.
+ *
+ *
+ * {@code 0123456789abcdef}
+ *
+ *
+ * These are the characters {@code '\u005Cu0030'} through
+ * {@code '\u005Cu0039'} and {@code '\u005Cu0061'} through
+ * {@code '\u005Cu0066'}. If uppercase letters are desired,
+ * the {@link java.lang.String#toUpperCase()} method may be called
+ * on the result:
+ *
+ *
+ * {@code Long.toHexString(n).toUpperCase()}
+ *
+ *
+ * @param i a {@code long} to be converted to a string.
+ * @return the string representation of the unsigned {@code long}
+ * value represented by the argument in hexadecimal
+ * (base 16).
+ * @see #parseUnsignedLong(String, int)
+ * @see #toUnsignedString(long, int)
+ * @since JDK 1.0.2
+ */
+ public static String toHexString(long i) {
+ return toUnsignedString0(i, 4);
+ }
+
+ /**
+ * Returns a string representation of the {@code long}
+ * argument as an unsigned integer in base 8.
+ *
+ *
+ * {@code 01234567}
+ *
+ *
+ * These are the characters {@code '\u005Cu0030'} through
+ * {@code '\u005Cu0037'}.
+ *
+ * @param i a {@code long} to be converted to a string.
+ * @return the string representation of the unsigned {@code long}
+ * value represented by the argument in octal (base 8).
+ * @see #parseUnsignedLong(String, int)
+ * @see #toUnsignedString(long, int)
+ * @since JDK 1.0.2
+ */
+ public static String toOctalString(long i) {
+ return toUnsignedString0(i, 3);
+ }
+
+ /**
+ * Returns a string representation of the {@code long}
+ * argument as an unsigned integer in base 2.
+ *
+ *
+ *
+ *
+ *
+ *
+ *
+ * @param s the {@code String} containing the
+ * {@code long} representation to be parsed.
+ * @param radix the radix to be used while parsing {@code s}.
+ * @return the {@code long} represented by the string argument in
+ * the specified radix.
+ * @throws NumberFormatException if the string does not contain a
+ * parsable {@code long}.
+ */
+ public static long parseLong(String s, int radix)
+ throws NumberFormatException
+ {
+ if (s == null) {
+ throw new NumberFormatException("null");
+ }
+
+ if (radix < Character.MIN_RADIX) {
+ throw new NumberFormatException("radix " + radix +
+ " less than Character.MIN_RADIX");
+ }
+ if (radix > Character.MAX_RADIX) {
+ throw new NumberFormatException("radix " + radix +
+ " greater than Character.MAX_RADIX");
+ }
+
+ long result = 0;
+ boolean negative = false;
+ int i = 0, len = s.length();
+ long limit = -Long.MAX_VALUE;
+ long multmin;
+ int digit;
+
+ if (len > 0) {
+ char firstChar = CProverString.charAt(s, 0);
+ if (firstChar < '0') { // Possible leading "+" or "-"
+ if (firstChar == '-') {
+ negative = true;
+ limit = Long.MIN_VALUE;
+ } else if (firstChar != '+')
+ throw NumberFormatException.forInputString(s);
+
+ if (len == 1) // Cannot have lone "+" or "-"
+ throw NumberFormatException.forInputString(s);
+ i++;
+ }
+ multmin = limit / radix;
+ while (i < len) {
+ // Accumulating negatively avoids surprises near MAX_VALUE
+ digit = Character.digit(CProverString.charAt(s, i++), radix);
+ if (digit < 0) {
+ throw NumberFormatException.forInputString(s);
+ }
+ if (result < multmin) {
+ throw NumberFormatException.forInputString(s);
+ }
+ result *= radix;
+ if (result < limit + digit) {
+ throw NumberFormatException.forInputString(s);
+ }
+ result -= digit;
+ }
+ } else {
+ throw NumberFormatException.forInputString(s);
+ }
+ return negative ? result : -result;
+ }
+
+ /**
+ * Parses the string argument as a signed decimal {@code long}.
+ * The characters in the string must all be decimal digits, except
+ * that the first character may be an ASCII minus sign {@code '-'}
+ * ({@code \u005Cu002D'}) to indicate a negative value or an
+ * ASCII plus sign {@code '+'} ({@code '\u005Cu002B'}) to
+ * indicate a positive value. The resulting {@code long} value is
+ * returned, exactly as if the argument and the radix {@code 10}
+ * were given as arguments to the {@link
+ * #parseLong(java.lang.String, int)} method.
+ *
+ *
+ * parseLong("0", 10) returns 0L
+ * parseLong("473", 10) returns 473L
+ * parseLong("+42", 10) returns 42L
+ * parseLong("-0", 10) returns 0L
+ * parseLong("-FF", 16) returns -255L
+ * parseLong("1100110", 2) returns 102L
+ * parseLong("99", 8) throws a NumberFormatException
+ * parseLong("Hazelnut", 10) throws a NumberFormatException
+ * parseLong("Hazelnut", 36) returns 1356099454469L
+ *
+ *
+ *
+ *
+ * @param s the {@code String} containing the unsigned integer
+ * representation to be parsed
+ * @param radix the radix to be used while parsing {@code s}.
+ * @return the unsigned {@code long} represented by the string
+ * argument in the specified radix.
+ * @throws NumberFormatException if the {@code String}
+ * does not contain a parsable {@code long}.
+ * @since 1.8
+ */
+ public static long parseUnsignedLong(String s, int radix)
+ throws NumberFormatException {
+ if (s == null) {
+ throw new NumberFormatException("null");
+ }
+
+ int len = s.length();
+ if (len > 0) {
+ char firstChar = CProverString.charAt(s, 0);
+ if (firstChar == '-') {
+ throw new
+ NumberFormatException(String.format("Illegal leading minus sign " +
+ "on unsigned string %s.", s));
+ } else {
+ if (len <= 12 || // Long.MAX_VALUE in Character.MAX_RADIX is 13 digits
+ (radix == 10 && len <= 18) ) { // Long.MAX_VALUE in base 10 is 19 digits
+ return parseLong(s, radix);
+ }
+
+ // No need for range checks on len due to testing above.
+ long first = parseLong(CProverString.substring(s, 0, len - 1), radix);
+ int second = Character.digit(CProverString.charAt(s, len - 1), radix);
+ if (second < 0) {
+ throw new NumberFormatException("Bad digit at end of " + s);
+ }
+ long result = first * radix + second;
+ if (compareUnsigned(result, first) < 0) {
+ /*
+ * The maximum unsigned value, (2^64)-1, takes at
+ * most one more digit to represent than the
+ * maximum signed value, (2^63)-1. Therefore,
+ * parsing (len - 1) digits will be appropriately
+ * in-range of the signed parsing. In other
+ * words, if parsing (len -1) digits overflows
+ * signed parsing, parsing len digits will
+ * certainly overflow unsigned parsing.
+ *
+ * The compareUnsigned check above catches
+ * situations where an unsigned overflow occurs
+ * incorporating the contribution of the final
+ * digit.
+ */
+ throw new NumberFormatException(String.format("String value %s exceeds " +
+ "range of unsigned long.", s));
+ }
+ return result;
+ }
+ } else {
+ throw NumberFormatException.forInputString(s);
+ }
+ }
+
+ /**
+ * Parses the string argument as an unsigned decimal {@code long}. The
+ * characters in the string must all be decimal digits, except
+ * that the first character may be an an ASCII plus sign {@code
+ * '+'} ({@code '\u005Cu002B'}). The resulting integer value
+ * is returned, exactly as if the argument and the radix 10 were
+ * given as arguments to the {@link
+ * #parseUnsignedLong(java.lang.String, int)} method.
+ *
+ * @param s a {@code String} containing the unsigned {@code long}
+ * representation to be parsed
+ * @return the unsigned {@code long} value represented by the decimal string argument
+ * @throws NumberFormatException if the string does not contain a
+ * parsable unsigned integer.
+ * @since 1.8
+ */
+ public static long parseUnsignedLong(String s) throws NumberFormatException {
+ return parseUnsignedLong(s, 10);
+ }
+
+ /**
+ * Returns a {@code Long} object holding the value
+ * extracted from the specified {@code String} when parsed
+ * with the radix given by the second argument. The first
+ * argument is interpreted as representing a signed
+ * {@code long} in the radix specified by the second
+ * argument, exactly as if the arguments were given to the {@link
+ * #parseLong(java.lang.String, int)} method. The result is a
+ * {@code Long} object that represents the {@code long}
+ * value specified by the string.
+ *
+ *
+ * {@code new Long(Long.parseLong(s, radix))}
+ *
+ *
+ * @param s the string to be parsed
+ * @param radix the radix to be used in interpreting {@code s}
+ * @return a {@code Long} object holding the value
+ * represented by the string argument in the specified
+ * radix.
+ * @throws NumberFormatException If the {@code String} does not
+ * contain a parsable {@code long}.
+ */
+ public static Long valueOf(String s, int radix) throws NumberFormatException {
+ return Long.valueOf(parseLong(s, radix));
+ }
+
+ /**
+ * Returns a {@code Long} object holding the value
+ * of the specified {@code String}. The argument is
+ * interpreted as representing a signed decimal {@code long},
+ * exactly as if the argument were given to the {@link
+ * #parseLong(java.lang.String)} method. The result is a
+ * {@code Long} object that represents the integer value
+ * specified by the string.
+ *
+ *
+ * {@code new Long(Long.parseLong(s))}
+ *
+ *
+ * @param s the string to be parsed.
+ * @return a {@code Long} object holding the value
+ * represented by the string argument.
+ * @throws NumberFormatException If the string cannot be parsed
+ * as a {@code long}.
+ */
+ public static Long valueOf(String s) throws NumberFormatException
+ {
+ return Long.valueOf(parseLong(s, 10));
+ }
+
+ private static class LongCache {
+ private LongCache(){}
+
+ static final Long cache[] = new Long[-(-128) + 127 + 1];
+
+ static {
+ for(int i = 0; i < cache.length; i++)
+ cache[i] = new Long(i - 128);
+ }
+ }
+
+ /**
+ * Returns a {@code Long} instance representing the specified
+ * {@code long} value.
+ * If a new {@code Long} instance is not required, this method
+ * should generally be used in preference to the constructor
+ * {@link #Long(long)}, as this method is likely to yield
+ * significantly better space and time performance by caching
+ * frequently requested values.
+ *
+ * Note that unlike the {@linkplain Integer#valueOf(int)
+ * corresponding method} in the {@code Integer} class, this method
+ * is not required to cache values within a particular
+ * range.
+ *
+ * @param l a long value.
+ * @return a {@code Long} instance representing {@code l}.
+ * @since 1.5
+ */
+ public static Long valueOf(long l) {
+ return new Long(l);
+ }
+
+ /**
+ * Decodes a {@code String} into a {@code Long}.
+ * Accepts decimal, hexadecimal, and octal numbers given by the
+ * following grammar:
+ *
+ *
+ *
+ *
+ * DecimalNumeral, HexDigits, and OctalDigits
+ * are as defined in section 3.10.1 of
+ * The Java™ Language Specification,
+ * except that underscores are not accepted between digits.
+ *
+ *
+ *
+ *
+ * {@code (int)(this.longValue()^(this.longValue()>>>32))}
+ *
+ *
+ * @return a hash code value for this object.
+ */
+ @Override
+ public int hashCode() {
+ return Long.hashCode(value);
+ }
+
+ /**
+ * Returns a hash code for a {@code long} value; compatible with
+ * {@code Long.hashCode()}.
+ *
+ * @param value the value to hash
+ * @return a hash code value for a {@code long} value.
+ * @since 1.8
+ */
+ public static int hashCode(long value) {
+ return (int)(value ^ (value >>> 32));
+ }
+
+ /**
+ * Compares this object to the specified object. The result is
+ * {@code true} if and only if the argument is not
+ * {@code null} and is a {@code Long} object that
+ * contains the same {@code long} value as this object.
+ *
+ * @param obj the object to compare with.
+ * @return {@code true} if the objects are the same;
+ * {@code false} otherwise.
+ */
+ public boolean equals(Object obj) {
+ if (obj instanceof Long) {
+ return value == ((Long)obj).longValue();
+ }
+ return false;
+ }
+
+ /**
+ * Determines the {@code long} value of the system property
+ * with the specified name.
+ *
+ *
+ * {@code getLong(nm, null)}
+ *
+ *
+ * @param nm property name.
+ * @return the {@code Long} value of the property.
+ * @throws SecurityException for the same reasons as
+ * {@link System#getProperty(String) System.getProperty}
+ * @see java.lang.System#getProperty(java.lang.String)
+ * @see java.lang.System#getProperty(java.lang.String, java.lang.String)
+ */
+ public static Long getLong(String nm) {
+ return getLong(nm, null);
+ }
+
+ /**
+ * Determines the {@code long} value of the system property
+ * with the specified name.
+ *
+ *
+ * {@code getLong(nm, new Long(val))}
+ *
+ *
+ * but in practice it may be implemented in a manner such as:
+ *
+ *
+ *
+ * to avoid the unnecessary allocation of a {@code Long} object when
+ * the default value is not needed.
+ *
+ * @param nm property name.
+ * @param val default value.
+ * @return the {@code Long} value of the property.
+ * @throws SecurityException for the same reasons as
+ * {@link System#getProperty(String) System.getProperty}
+ * @see java.lang.System#getProperty(java.lang.String)
+ * @see java.lang.System#getProperty(java.lang.String, java.lang.String)
+ */
+ public static Long getLong(String nm, long val) {
+ Long result = Long.getLong(nm, null);
+ return (result == null) ? Long.valueOf(val) : result;
+ }
+
+ /**
+ * Returns the {@code long} value of the system property with
+ * the specified name. The first argument is treated as the name
+ * of a system property. System properties are accessible through
+ * the {@link java.lang.System#getProperty(java.lang.String)}
+ * method. The string value of this property is then interpreted
+ * as a {@code long} value, as per the
+ * {@link Long#decode decode} method, and a {@code Long} object
+ * representing this value is returned; in summary:
+ *
+ *
+ * Long result = getLong(nm, null);
+ * return (result == null) ? new Long(val) : result;
+ *
+ *
+ *
+ *
+ * Long.valueOf(x).compareTo(Long.valueOf(y))
+ *
+ *
+ * @param x the first {@code long} to compare
+ * @param y the second {@code long} to compare
+ * @return the value {@code 0} if {@code x == y};
+ * a value less than {@code 0} if {@code x < y}; and
+ * a value greater than {@code 0} if {@code x > y}
+ * @since 1.7
+ */
+ public static int compare(long x, long y) {
+ return (x < y) ? -1 : ((x == y) ? 0 : 1);
+ }
+
+ /**
+ * Compares two {@code long} values numerically treating the values
+ * as unsigned.
+ *
+ * @param x the first {@code long} to compare
+ * @param y the second {@code long} to compare
+ * @return the value {@code 0} if {@code x == y}; a value less
+ * than {@code 0} if {@code x < y} as unsigned values; and
+ * a value greater than {@code 0} if {@code x > y} as
+ * unsigned values
+ * @since 1.8
+ */
+ public static int compareUnsigned(long x, long y) {
+ return compare(x + MIN_VALUE, y + MIN_VALUE);
+ }
+
+
+ /**
+ * Returns the unsigned quotient of dividing the first argument by
+ * the second where each argument and the result is interpreted as
+ * an unsigned value.
+ *
+ *
+ *
+ *
+ * @param i the value whose number of leading zeros is to be computed
+ * @return the number of zero bits preceding the highest-order
+ * ("leftmost") one-bit in the two's complement binary representation
+ * of the specified {@code long} value, or 64 if the value
+ * is equal to zero.
+ * @since 1.5
+ */
+ public static int numberOfLeadingZeros(long i) {
+ // HD, Figure 5-6
+ if (i == 0)
+ return 64;
+ int n = 1;
+ int x = (int)(i >>> 32);
+ if (x == 0) { n += 32; x = (int)i; }
+ if (x >>> 16 == 0) { n += 16; x <<= 16; }
+ if (x >>> 24 == 0) { n += 8; x <<= 8; }
+ if (x >>> 28 == 0) { n += 4; x <<= 4; }
+ if (x >>> 30 == 0) { n += 2; x <<= 2; }
+ n -= x >>> 31;
+ return n;
+ }
+
+ /**
+ * Returns the number of zero bits following the lowest-order ("rightmost")
+ * one-bit in the two's complement binary representation of the specified
+ * {@code long} value. Returns 64 if the specified value has no
+ * one-bits in its two's complement representation, in other words if it is
+ * equal to zero.
+ *
+ * @param i the value whose number of trailing zeros is to be computed
+ * @return the number of zero bits following the lowest-order ("rightmost")
+ * one-bit in the two's complement binary representation of the
+ * specified {@code long} value, or 64 if the value is equal
+ * to zero.
+ * @since 1.5
+ */
+ public static int numberOfTrailingZeros(long i) {
+ // HD, Figure 5-14
+ int x, y;
+ if (i == 0) return 64;
+ int n = 63;
+ y = (int)i; if (y != 0) { n = n -32; x = y; } else x = (int)(i>>>32);
+ y = x <<16; if (y != 0) { n = n -16; x = y; }
+ y = x << 8; if (y != 0) { n = n - 8; x = y; }
+ y = x << 4; if (y != 0) { n = n - 4; x = y; }
+ y = x << 2; if (y != 0) { n = n - 2; x = y; }
+ return n - ((x << 1) >>> 31);
+ }
+
+ /**
+ * Returns the number of one-bits in the two's complement binary
+ * representation of the specified {@code long} value. This function is
+ * sometimes referred to as the population count.
+ *
+ * @param i the value whose bits are to be counted
+ * @return the number of one-bits in the two's complement binary
+ * representation of the specified {@code long} value.
+ * @since 1.5
+ */
+ public static int bitCount(long i) {
+ // HD, Figure 5-14
+ i = i - ((i >>> 1) & 0x5555555555555555L);
+ i = (i & 0x3333333333333333L) + ((i >>> 2) & 0x3333333333333333L);
+ i = (i + (i >>> 4)) & 0x0f0f0f0f0f0f0f0fL;
+ i = i + (i >>> 8);
+ i = i + (i >>> 16);
+ i = i + (i >>> 32);
+ return (int)i & 0x7f;
+ }
+
+ /**
+ * Returns the value obtained by rotating the two's complement binary
+ * representation of the specified {@code long} value left by the
+ * specified number of bits. (Bits shifted out of the left hand, or
+ * high-order, side reenter on the right, or low-order.)
+ *
+ *
+ *
+ *
+ * @param s the {@code String} containing the
+ * {@code short} representation to be parsed
+ * @param radix the radix to be used while parsing {@code s}
+ * @return the {@code short} represented by the string
+ * argument in the specified radix.
+ * @throws NumberFormatException If the {@code String}
+ * does not contain a parsable {@code short}.
+ */
+ public static short parseShort(String s, int radix)
+ throws NumberFormatException {
+ int i = Integer.parseInt(s, radix);
+ if (i < MIN_VALUE || i > MAX_VALUE)
+ throw new NumberFormatException(
+ "Value out of range. Value:\"" + s + "\" Radix:" + radix);
+ return (short)i;
+ }
+
+ /**
+ * Parses the string argument as a signed decimal {@code
+ * short}. The characters in the string must all be decimal
+ * digits, except that the first character may be an ASCII minus
+ * sign {@code '-'} ({@code '\u005Cu002D'}) to indicate a
+ * negative value or an ASCII plus sign {@code '+'}
+ * ({@code '\u005Cu002B'}) to indicate a positive value. The
+ * resulting {@code short} value is returned, exactly as if the
+ * argument and the radix 10 were given as arguments to the {@link
+ * #parseShort(java.lang.String, int)} method.
+ *
+ * @param s a {@code String} containing the {@code short}
+ * representation to be parsed
+ * @return the {@code short} value represented by the
+ * argument in decimal.
+ * @throws NumberFormatException If the string does not
+ * contain a parsable {@code short}.
+ */
+ public static short parseShort(String s) throws NumberFormatException {
+ return CProver.nondetShort(); //The function is handled by cbmc internally
+ }
+
+ /**
+ * Returns a {@code Short} object holding the value
+ * extracted from the specified {@code String} when parsed
+ * with the radix given by the second argument. The first argument
+ * is interpreted as representing a signed {@code short} in
+ * the radix specified by the second argument, exactly as if the
+ * argument were given to the {@link #parseShort(java.lang.String,
+ * int)} method. The result is a {@code Short} object that
+ * represents the {@code short} value specified by the string.
+ *
+ *
+ * {@code new Short(Short.parseShort(s, radix))}
+ *
+ *
+ * @param s the string to be parsed
+ * @param radix the radix to be used in interpreting {@code s}
+ * @return a {@code Short} object holding the value
+ * represented by the string argument in the
+ * specified radix.
+ * @throws NumberFormatException If the {@code String} does
+ * not contain a parsable {@code short}.
+ */
+ public static Short valueOf(String s, int radix)
+ throws NumberFormatException {
+ return valueOf(parseShort(s, radix));
+ }
+
+ /**
+ * Returns a {@code Short} object holding the
+ * value given by the specified {@code String}. The argument
+ * is interpreted as representing a signed decimal
+ * {@code short}, exactly as if the argument were given to
+ * the {@link #parseShort(java.lang.String)} method. The result is
+ * a {@code Short} object that represents the
+ * {@code short} value specified by the string.
+ *
+ *
+ * {@code new Short(Short.parseShort(s))}
+ *
+ *
+ * @param s the string to be parsed
+ * @return a {@code Short} object holding the value
+ * represented by the string argument
+ * @throws NumberFormatException If the {@code String} does
+ * not contain a parsable {@code short}.
+ */
+ public static Short valueOf(String s) throws NumberFormatException {
+ return valueOf(s, 10);
+ }
+
+ /**
+ * Returns a {@code Short} instance representing the specified
+ * {@code short} value.
+ * If a new {@code Short} instance is not required, this method
+ * should generally be used in preference to the constructor
+ * {@link #Short(short)}, as this method is likely to yield
+ * significantly better space and time performance by caching
+ * frequently requested values.
+ *
+ * This method will always cache values in the range -128 to 127,
+ * inclusive, and may cache other values outside of this range.
+ *
+ * @param s a short value.
+ * @return a {@code Short} instance representing {@code s}.
+ * @since 1.5
+ */
+ public static Short valueOf(short s) {
+ return new Short(s);
+ }
+
+ /**
+ * Decodes a {@code String} into a {@code Short}.
+ * Accepts decimal, hexadecimal, and octal numbers given by
+ * the following grammar:
+ *
+ *
+ *
+ *
+ * DecimalNumeral, HexDigits, and OctalDigits
+ * are as defined in section 3.10.1 of
+ * The Java™ Language Specification,
+ * except that underscores are not accepted between digits.
+ *
+ *
+ *
+ *
+ * Short.valueOf(x).compareTo(Short.valueOf(y))
+ *
+ *
+ * @param x the first {@code short} to compare
+ * @param y the second {@code short} to compare
+ * @return the value {@code 0} if {@code x == y};
+ * a value less than {@code 0} if {@code x < y}; and
+ * a value greater than {@code 0} if {@code x > y}
+ * @since 1.7
+ */
+ public static int compare(short x, short y) {
+ return x - y;
+ }
+
+ /**
+ * The number of bits used to represent a {@code short} value in two's
+ * complement binary form.
+ * @since 1.5
+ */
+ public static final int SIZE = 16;
+
+ /**
+ * The number of bytes used to represent a {@code short} value in two's
+ * complement binary form.
+ *
+ * @since 1.8
+ */
+ public static final int BYTES = SIZE / Byte.SIZE;
+
+ /**
+ * Returns the value obtained by reversing the order of the bytes in the
+ * two's complement representation of the specified {@code short} value.
+ *
+ * @param i the value whose bytes are to be reversed
+ * @return the value obtained by reversing (or, equivalently, swapping)
+ * the bytes in the specified {@code short} value.
+ * @since 1.5
+ */
+ public static short reverseBytes(short i) {
+ return (short) (((i & 0xFF00) >> 8) | (i << 8));
+ }
+
+
+ /**
+ * Converts the argument to an {@code int} by an unsigned
+ * conversion. In an unsigned conversion to an {@code int}, the
+ * high-order 16 bits of the {@code int} are zero and the
+ * low-order 16 bits are equal to the bits of the {@code short} argument.
+ *
+ * Consequently, zero and positive {@code short} values are mapped
+ * to a numerically equal {@code int} value and negative {@code
+ * short} values are mapped to an {@code int} value equal to the
+ * input plus 216.
+ *
+ * @param x the value to convert to an unsigned {@code int}
+ * @return the argument converted to {@code int} by an unsigned
+ * conversion
+ * @since 1.8
+ */
+ public static int toUnsignedInt(short x) {
+ return ((int) x) & 0xffff;
+ }
+
+ /**
+ * Converts the argument to a {@code long} by an unsigned
+ * conversion. In an unsigned conversion to a {@code long}, the
+ * high-order 48 bits of the {@code long} are zero and the
+ * low-order 16 bits are equal to the bits of the {@code short} argument.
+ *
+ * Consequently, zero and positive {@code short} values are mapped
+ * to a numerically equal {@code long} value and negative {@code
+ * short} values are mapped to a {@code long} value equal to the
+ * input plus 216.
+ *
+ * @param x the value to convert to an unsigned {@code long}
+ * @return the argument converted to {@code long} by an unsigned
+ * conversion
+ * @since 1.8
+ */
+ public static long toUnsignedLong(short x) {
+ return ((long) x) & 0xffffL;
+ }
+
+ /** use serialVersionUID from JDK 1.1. for interoperability */
+ private static final long serialVersionUID = 7515723908773894738L;
+}
diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java
index f690b63..dd64c4a 100644
--- a/src/main/java/java/lang/String.java
+++ b/src/main/java/java/lang/String.java
@@ -151,7 +151,6 @@ public final class String
* unnecessary since Strings are immutable.
*
* @diffblue.fullSupport
- * @diffblue.untested
*/
public String() {
// DIFFBLUE MODEL LIBRARY This is treated internally in CBMC
@@ -169,7 +168,6 @@ public String() {
* A {@code String}
*
* @diffblue.fullSupport
- * @diffblue.untested
*/
public String(String original) {
// DIFFBLUE MODEL LIBRARY This is treated internally in CBMC
@@ -307,6 +305,8 @@ private static String cproverNonDet()
*
* @diffblue.limitedSupport
* Assumes all codePoints are in the Basic Multilingual Plane.
+ * An implication of this limitation is that no trace is generated for
+ * the cases where IllegalArgumentException would be thrown.
*/
public String(int[] codePoints, int offset, int count) {
// if (offset < 0) {
@@ -595,7 +595,8 @@ public String(byte bytes[], int offset, int length, String charsetName)
* The length of the String constructed is limited by the unwind
* parameter.
*/
- public String(byte bytes[], int offset, int length, Charset charset) {
+ public String(byte bytes[], int offset, int length, Charset charset)
+ {
// if (charset == null)
// throw new NullPointerException("charset");
// checkBounds(bytes, offset, length);
@@ -663,7 +664,8 @@ public String(byte bytes[], String charsetName)
*
* @return the constructed string
*/
- private static String cproverOfByteArray(byte[] bytes, Charset charset) {
+ private static String cproverOfByteArray(byte[] bytes, Charset charset)
+ {
String s = CProver.nondetWithoutNull("");
byte[] getBytesResult = s.cproverReversibleGetBytes(charset);
CProver.assume(getBytesResult.length == bytes.length);
@@ -696,10 +698,9 @@ private static String cproverOfByteArray(byte[] bytes, Charset charset) {
* @diffblue.limitedSupport
* Only standard charsets are supported and for ASCII, UTF-8 and ISO-8859-1
* we restrict all the characters to be ASCII.
- * Generated tests will not pass if the function under test takes a
- * Charset argument because it is set using reflection.
*/
- public String(byte bytes[], Charset charset) {
+ public String(byte bytes[], Charset charset)
+ {
// this(bytes, 0, bytes.length, charset);
// DIFFBLUE MODEL LIBRARY
@@ -734,7 +735,6 @@ public String(byte bytes[], Charset charset) {
*
* @diffblue.limitedSupport We assume all the bytes are ASCII characters,
* and that the default charset encodes ASCII characters with one byte.
- * In particular test may fail if the default charset is UTF-16.
*/
public String(byte bytes[], int offset, int length) {
// DIFFBLUE MODEL LIBRARY
@@ -772,7 +772,6 @@ public String(byte bytes[], int offset, int length) {
*
* @diffblue.limitedSupport We assume all the bytes are ASCII characters,
* and that the default charset encodes ASCII characters with one byte.
- * In particular test may fail if the default charset is UTF-16.
*/
public String(byte bytes[]) {
this(bytes, 0, bytes.length);
@@ -1080,15 +1079,17 @@ public void getChars(int srcBegin, int srcEnd, char dst[], int dstBegin) {
if (srcBegin < 0) {
throw new StringIndexOutOfBoundsException(srcBegin);
}
+ // if (srcEnd > value.length) {
+ // DIFFBLUE MODEL LIBRARY we have no value member
if (srcEnd > length()) {
throw new StringIndexOutOfBoundsException(srcEnd);
}
if (srcBegin > srcEnd) {
throw new StringIndexOutOfBoundsException(srcEnd - srcBegin);
}
+ // System.arraycopy(value, srcBegin, dst, dstBegin, srcEnd - srcBegin);
// DIFFBLUE MODEL LIBRARY we inline System.arraycopy here so that we
// can specialize it for characters.
- // System.arraycopy(value, srcBegin, dst, dstBegin, srcEnd - srcBegin);
for(int i = 0; i < srcEnd - srcBegin; i++) {
dst[dstBegin + i] = CProverString.charAt(this, srcBegin + i);
}
@@ -1461,7 +1462,9 @@ else if(c<=0xFFFF)
* @param charsetName
* The name of the Charset used to encode the {@code String}
*/
- private byte[] cproverReversibleGetBytes(String charsetName) {
+ private byte[] cproverReversibleGetBytes(String charsetName)
+ throws UnsupportedEncodingException
+ {
if (CProverString.equals(charsetName, "UTF-16BE")) {
return getBytesUTF_16BE();
}
@@ -1471,10 +1474,12 @@ private byte[] cproverReversibleGetBytes(String charsetName) {
if (CProverString.equals(charsetName, "UTF-16")) {
return getBytesUTF_16();
}
- CProver.assume(CProverString.equals(charsetName, "UTF-8")
+ if (CProverString.equals(charsetName, "UTF-8")
|| CProverString.equals(charsetName, "ISO-8859-1")
- || CProverString.equals(charsetName, "US-ASCII"));
- return cproverGetBytesEnforceAscii();
+ || CProverString.equals(charsetName, "US-ASCII")) {
+ return cproverGetBytesEnforceAscii();
+ }
+ throw new UnsupportedEncodingException(charsetName);
}
/**
@@ -1489,7 +1494,12 @@ private byte[] cproverReversibleGetBytes(Charset charset) {
if (charset == null) {
throw new NullPointerException();
}
- return cproverReversibleGetBytes(charset.name());
+ try {
+ return cproverReversibleGetBytes(charset.name());
+ } catch (UnsupportedEncodingException e) {
+ CProver.assume(false);
+ return new byte[0];
+ }
}
/**
@@ -2976,13 +2986,32 @@ public String replaceFirst(String regex, String replacement) {
* @since 1.4
* @spec JSR-51
*
- * @diffblue.noSupport
+ * @diffblue.limitedSupport
+ * We enforce the regex argument is a string literal without any special
+ * characters used in regular expressions:
+ * '[', ']','.', '\\', '?', '^', '$', '*', '+', '{', '}', '|', '(', ')',
+ * hence PatternSyntaxException will never be thrown.
*/
public String replaceAll(String regex, String replacement)
{
- CProver.notModelled();
- return CProver.nondetWithNullForNotModelled();
// return Pattern.compile(regex).matcher(this).replaceAll(replacement);
+ // DIFFBLUE MODELS LIBRARY: we assume the expression is just a string literal
+ CProver.assume(
+ regex.indexOf('[') == -1 &&
+ regex.indexOf(']') == -1 &&
+ regex.indexOf('.') == -1 &&
+ regex.indexOf('\\') == -1 &&
+ regex.indexOf('?') == -1 &&
+ regex.indexOf('^') == -1 &&
+ regex.indexOf('$') == -1 &&
+ regex.indexOf('*') == -1 &&
+ regex.indexOf('+') == -1 &&
+ regex.indexOf('{') == -1 &&
+ regex.indexOf('}') == -1 &&
+ regex.indexOf('|') == -1 &&
+ regex.indexOf('(') == -1 &&
+ regex.indexOf(')') == -1);
+ return replace(regex, replacement);
}
/**
@@ -2997,10 +3026,14 @@ public String replaceAll(String regex, String replacement)
* @return The resulting string
* @since 1.5
*
- * @diffblue.noSupport
+ * @diffblue.limitedSupport
+ * Only works for arguments that are constant strings with only 1 character.
+ * For instance, we can generate traces for s.replace("a", "b") but not
+ * s.replace("a", "bc") or s.replace(arg, "b").
+ * @diffblue.untested
*/
public String replace(CharSequence target, CharSequence replacement) {
- CProver.notModelled();
+ // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC
return CProver.nondetWithNullForNotModelled();
// return Pattern.compile(target.toString(), Pattern.LITERAL).matcher(
// this).replaceAll(Matcher.quoteReplacement(replacement.toString()));
@@ -3092,7 +3125,17 @@ public String replace(CharSequence target, CharSequence replacement) {
* @since 1.4
* @spec JSR-51
*
- * @diffblue.noSupport
+ * @diffblue.limitedSupport
+ * This forces the regex argument to contain at most one character.
+ * The model assumes the regex is not a special regex character:
+ * \.[{()<>*+-=?^$| .
+ * So no trace can be generated for these characters.
+ * In particular this prevents any trace for the PatternSyntaxException case
+ * from being generated.
+ *
+ * The size of the computed array is limited by the unwind parameter.
+ * No trace can be generated for which the resulting array would be greater
+ * than the unwind value.
*/
public String[] split(String regex, int limit) {
// /* fastpath if the regex is a
@@ -3252,14 +3295,24 @@ public String[] split(String regex, int limit) {
* @since 1.4
* @spec JSR-51
*
- * @diffblue.noSupport
+ * @diffblue.limitedSupport
+ * This forces the regex argument to contain at most one character.
+ * The model assumes the regex is not a special regex character:
+ * \.[{()<>*+-=?^$| .
+ * So no trace can be generated for these characters.
+ * In particular this prevents any trace for the PatternSyntaxException case
+ * from being generated.
+ *
+ * The size of the computed array is limited by the unwind parameter.
+ * No trace can be generated for which the resulting array would be greater
+ * than the unwind value.
*/
public String[] split(String regex) {
// return split(regex, 0);
// DIFFBLUE MODEL LIBRARY
// The (String, int) version in our model calls the String version,
- // which is the other way in the original implementation.
+ // which the other way in the original implementation.
// This way, if the String version is called in the code we analyse,
// only the code for this one is loaded.
// The 0 case is a bit special compared to the others in that it disregard trailing empty strings.
@@ -3916,10 +3969,13 @@ static String cproverFormatArgument(Object obj) {
} else if (obj instanceof Byte) {
byte byteValue = ((Byte) obj);
longValue = (long) byteValue;
+ } else if (obj instanceof Short) {
+ short shortValue = ((Short) obj);
+ longValue = (long) shortValue;
} else if (obj instanceof Boolean) {
longValue = ((Boolean) obj) ? 1 : 0;
} else {
- return CProver.nondetWithoutNull("");
+ CProver.assume(false);
}
// The long value is encoded using a string of 4 characters
@@ -3986,15 +4042,15 @@ static String cproverFormatArgument(Object obj) {
*
*
* @diffblue.untested
*/
public static String format(String format, Object... args) {
// return new Formatter().format(format, args).toString();
// DIFFBLUE MODEL LIBRARY
- if (args.length > 10) {
- return CProver.nondetWithoutNull("");
- }
+ CProver.assume(args.length <= 10);
String arg0 = args.length > 0 ? cproverFormatArgument(args[0]) : "";
String arg1 = args.length > 1 ? cproverFormatArgument(args[1]) : "";
String arg2 = args.length > 2 ? cproverFormatArgument(args[2]) : "";
@@ -4028,10 +4077,11 @@ public static String format(String format, Object... args) {
String arg7 = args.length > 7 ? cproverFormatArgument(args[7]) : "";
String arg8 = args.length > 8 ? cproverFormatArgument(args[8]) : "";
String arg9 = args.length > 9 ? cproverFormatArgument(args[9]) : "";
- return CProverString.format(format, arg0, arg1, arg2, arg3, arg4, arg5,
- arg6, arg7, arg8, arg9);
+ return CProverString.format(format, arg0, arg1, arg2, arg3, arg4, arg5, arg6,
+ arg7, arg8, arg9);
}
+
/**
* Returns a formatted string using the specified locale, format string,
* and arguments.
@@ -4069,8 +4119,7 @@ public static String format(String format, Object... args) {
* @see java.util.Formatter
* @since 1.5
*
- * @diffblue.limitedSupport The locale argument is ignored and it has the
- * same limitations as {@link #format(String, Object...)}.
+ * @diffblue.noSupport
*/
public static String format(Locale l, String format, Object... args) {
// return new Formatter(l).format(format, args).toString();
@@ -4187,10 +4236,11 @@ public static String copyValueOf(char data[]) {
* {@code "false"} is returned.
*
* @diffblue.fullSupport
- * @diffblue.untested
*/
public static String valueOf(boolean b) {
- return b ? "true" : "false";
+ // DIFFBLUE MODEL LIBRARY This is treated internally in JBMC
+ return CProver.nondetWithoutNullForNotModelled();
+ // return b ? "true" : "false";
}
/**
@@ -4285,7 +4335,7 @@ public static String valueOf(float f) {
*/
public static String valueOf(double d) {
// DIFFBLUE MODEL LIBRARY we cast the number down to float because
- // the string solver only knows how to convert floats to string
+ // string solver only knows how to convert floats to string
return valueOf(CProver.doubleToFloat(d));
// return Double.toString(d);
}
@@ -4296,7 +4346,7 @@ public static String valueOf(double d) {
static String[] cproverInternPool = null;
/**
- * Number of elements stored in the pool for {@code String.intern} pool.
+ * Number of elements stored in the pool for {@code String.intern}.
* This can be smaller than {@code cproverInternPool.length} which
* represents the capacity of the array and is fixed for each execution.
*/
@@ -4327,6 +4377,7 @@ public static String valueOf(double d) {
*
* @diffblue.limitedSupport literal strings and string-valued constant
* expressions are not interned.
+ * @diffblue.untested
*/
// DIFFBLUE MODEL LIBRARY
// public native String intern();
diff --git a/src/main/java/java/lang/StringBuffer.java b/src/main/java/java/lang/StringBuffer.java
index 35c56dd..46f3cd9 100644
--- a/src/main/java/java/lang/StringBuffer.java
+++ b/src/main/java/java/lang/StringBuffer.java
@@ -505,11 +505,11 @@ public synchronized StringBuffer append(char[] str, int offset, int len) {
*/
@Override
public synchronized StringBuffer append(boolean b) {
- // DIFFBLUE MODEL LIBRARY do not use cache
+ // DIFFBLUE MODEL LIBRARY this is replaced internally
// toStringCache = null;
// super.append(b);
// return this;
- return append(b ? "true" : "false");
+ return CProver.nondetWithoutNullForNotModelled();
}
/**
@@ -527,7 +527,6 @@ public synchronized StringBuffer append(char c) {
/**
* @diffblue.fullSupport
- * @diffblue.untested
*/
@Override
public synchronized StringBuffer append(int i) {
@@ -567,11 +566,9 @@ public synchronized StringBuffer append(long lng) {
/**
* @diffblue.fullSupport
- * @diffblue.untested
*/
@Override
public synchronized StringBuffer append(float f) {
- // DIFFBLUE MODEL LIBRARY this is replaced internally
// toStringCache = null;
// super.append(f);
// return this;
@@ -579,12 +576,10 @@ public synchronized StringBuffer append(float f) {
}
/**
- * @diffblue.fullSupport
- * @diffblue.untested
+ * @diffblue.partialSupport This uses float approximation, so might return incorrect results
*/
@Override
public synchronized StringBuffer append(double d) {
- // DIFFBLUE MODEL LIBRARY this is replaced internally
// toStringCache = null;
// super.append(d);
// return this;
diff --git a/src/main/java/java/lang/Throwable.java b/src/main/java/java/lang/Throwable.java
index bed9779..23d3723 100644
--- a/src/main/java/java/lang/Throwable.java
+++ b/src/main/java/java/lang/Throwable.java
@@ -263,6 +263,7 @@ public class Throwable implements Serializable {
*/
public Throwable() {
// fillInStackTrace();
+ detailMessage = null;
}
/**
diff --git a/src/main/java/java/lang/reflect/AccessibleObject.java b/src/main/java/java/lang/reflect/AccessibleObject.java
new file mode 100644
index 0000000..0746796
--- /dev/null
+++ b/src/main/java/java/lang/reflect/AccessibleObject.java
@@ -0,0 +1,357 @@
+/*
+ * Copyright (c) 1997, 2014, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.lang.reflect;
+
+import org.cprover.CProver;
+
+import java.security.AccessController;
+// DIFFBLUE MODEL LIBRARY
+// removed for compatibility with Java 9 and newer
+// import sun.reflect.Reflection;
+// import sun.reflect.ReflectionFactory;
+import java.lang.annotation.Annotation;
+
+/**
+ * The AccessibleObject class is the base class for Field, Method and
+ * Constructor objects. It provides the ability to flag a reflected
+ * object as suppressing default Java language access control checks
+ * when it is used. The access checks--for public, default (package)
+ * access, protected, and private members--are performed when Fields,
+ * Methods or Constructors are used to set or get fields, to invoke
+ * methods, or to create and initialize new instances of classes,
+ * respectively.
+ *
+ *
+ * public static final int java.lang.Thread.MIN_PRIORITY
+ * private int java.io.FileDescriptor.fd
+ *
+ *
+ *
+ *
+ *
+ * See {@link java.lang.reflect.Executable#getParameters} for more
+ * information.
+ *
+ * @see java.lang.reflect.Executable#getParameters
+ * @since 1.8
+ */
+public class MalformedParametersException extends RuntimeException {
+
+ /**
+ * Version for serialization.
+ */
+ private static final long serialVersionUID = 20130919L;
+
+ /**
+ * Create a {@code MalformedParametersException} with an empty
+ * reason.
+ */
+ public MalformedParametersException() {}
+
+ /**
+ * Create a {@code MalformedParametersException}.
+ *
+ * @param reason The reason for the exception.
+ */
+ public MalformedParametersException(String reason) {
+ super(reason);
+ }
+
+ // DIFFBLUE MODEL LIBRARY
+ // While Object.getClass() is not modelled, we can get the same
+ // functionality by adding one toString() method per subclass of
+ // Throwable.
+ @Override
+ public String toString() {
+ String message = getLocalizedMessage();
+ return (message != null)
+ ? ("java.lang.reflect.MalformedParametersException: " + message)
+ : "java.lang.reflect.MalformedParametersException";
+ }
+}
diff --git a/src/main/java/java/lang/reflect/Method.java b/src/main/java/java/lang/reflect/Method.java
new file mode 100644
index 0000000..fdab45c
--- /dev/null
+++ b/src/main/java/java/lang/reflect/Method.java
@@ -0,0 +1,825 @@
+/*
+ * Copyright (c) 1996, 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.lang.reflect;
+
+import org.cprover.CProver;
+
+// DIFFBLUE MODEL LIBRARY
+// removed for compatibility with Java 9 and newer
+// import sun.reflect.CallerSensitive;
+// import sun.reflect.MethodAccessor;
+// import sun.reflect.Reflection;
+import sun.reflect.generics.repository.MethodRepository;
+import sun.reflect.generics.factory.CoreReflectionFactory;
+import sun.reflect.generics.factory.GenericsFactory;
+import sun.reflect.generics.scope.MethodScope;
+import sun.reflect.annotation.AnnotationType;
+import sun.reflect.annotation.AnnotationParser;
+import java.lang.annotation.Annotation;
+import java.lang.annotation.AnnotationFormatError;
+import java.nio.ByteBuffer;
+
+/**
+ * A {@code Method} provides information about, and access to, a single method
+ * on a class or interface. The reflected method may be a class method
+ * or an instance method (including an abstract method).
+ *
+ *
+ * public boolean java.lang.Object.equals(java.lang.Object)
+ *
+ *
+ *
+ * @diffblue.mock
+ * @diffblue.limitedSupport
* We currently ignore seeds and make test-generator pick return values
* for the methods in this class nondeterministically rather than
* calculating them according to a probability distribution. So this
* method is simply modelled as a no-op.
*
- * @diffblue.mock
*/
synchronized public void setSeed(long seed) {
// this.seed.set(initialScramble(seed));
@@ -258,14 +257,9 @@ protected int next(int bits) {
* @throws NullPointerException if the byte array is null
* @since 1.1
*
- * @diffblue.noSupport
- * Due to TG-2435.
- * This method sets each entry of the argument to a nondeterministic
- * {@code byte} value.
- * The nondeterminism is introduced by test-generator itself, and
- * probability distributions are ignored.
- *
* @diffblue.mock
+ * @diffblue.limitedSupport
+ *
*/
public void nextBytes(byte[] bytes) {
// for (int i = 0, len = bytes.length; i < len; )
@@ -273,7 +267,6 @@ public void nextBytes(byte[] bytes) {
// n = Math.min(len - i, Integer.SIZE/Byte.SIZE);
// n-- > 0; rnd >>= Byte.SIZE)
// bytes[i++] = (byte)rnd;
-
for (int i = 0; i < bytes.length; i++) {
byte b = CProver.nondetByte();
bytes[i] = b;
diff --git a/src/main/java/java/util/regex/Pattern.java b/src/main/java/java/util/regex/Pattern.java
index 931bcf9..ae980dd 100644
--- a/src/main/java/java/util/regex/Pattern.java
+++ b/src/main/java/java/util/regex/Pattern.java
@@ -1,5 +1,5 @@
/*
- * Copyright (c) 1999, 2017, Oracle and/or its affiliates. All rights reserved.
+ * Copyright (c) 1999, 2013, Oracle and/or its affiliates. All rights reserved.
* DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
*
* This code is free software; you can redistribute it and/or modify it
@@ -26,6 +26,7 @@
package java.util.regex;
import org.cprover.CProver;
+import org.cprover.CProverString;
import java.text.Normalizer;
import java.util.Locale;
@@ -937,8 +938,7 @@ public final class Pattern
*
* @serial
*/
- // DIFFBLUE MODEL LIBRARY - not used in model
- // private String pattern;
+ private String pattern;
/**
* The original pattern flags.
@@ -1046,13 +1046,13 @@ public final class Pattern
* @throws PatternSyntaxException
* If the expression's syntax is invalid
*
- * @diffblue.untested
- * @diffblue.noSupport
+ * @diffblue.limitedSupport
+ * PatternSyntaxException is not thrown by the model, we only assume that
+ * the first character is not a '?' character. This should be sufficient
+ * for most cases, as `compile` is often used with String constants.
*/
public static Pattern compile(String regex) {
- // return new Pattern(regex, 0);
- CProver.notModelled();
- return CProver.nondetWithoutNullForNotModelled();
+ return new Pattern(regex, 0);
}
/**
@@ -1078,12 +1078,15 @@ public static Pattern compile(String regex) {
* If the expression's syntax is invalid
*
* @diffblue.untested
- * @diffblue.noSupport
+ * @diffblue.limitedSupport
+ * Argument `flags` is ignored.
+ * PatternSyntaxException is not thrown by the model, we only assume that
+ * the first character is not a '?' character. This should be sufficient
+ * for most cases, as `compile` is often used with String constants.
+
*/
public static Pattern compile(String regex, int flags) {
- // return new Pattern(regex, flags);
- CProver.notModelled();
- return CProver.nondetWithoutNullForNotModelled();
+ return new Pattern(regex, flags);
}
/**
@@ -1091,13 +1094,10 @@ public static Pattern compile(String regex, int flags) {
*
* @return The source of this pattern
*
- * @diffblue.untested
- * @diffblue.noSupport
+ * @diffblue.fullSupport
*/
public String pattern() {
- // return pattern;
- CProver.notModelled();
- return CProver.nondetWithoutNullForNotModelled();
+ return pattern;
}
/**
@@ -1108,13 +1108,10 @@ public String pattern() {
* @return The string representation of this pattern
* @since 1.5
*
- * @diffblue.untested
- * @diffblue.noSupport
+ * @diffblue.fullSupport
*/
public String toString() {
- // return pattern;
- CProver.notModelled();
- return CProver.nondetWithoutNullForNotModelled();
+ return pattern;
}
/**
@@ -1151,10 +1148,34 @@ public Matcher matcher(CharSequence input) {
*/
public int flags() {
// return flags;
- CProver.notModelled();
return CProver.nondetInt();
}
+ /**
+ * DIFFBLUE MODEL LIBRARY
+ * This method enforces an assumption that its argument contains
+ * no characters that has special meaning in regular expressions.
+ * This way we can then match the regex using String.equals().
+ */
+ private static void cproverAssumeIsPlainString(String regex)
+ {
+ CProver.assume(
+ regex.indexOf('[') == -1 &&
+ regex.indexOf(']') == -1 &&
+ regex.indexOf('{') == -1 &&
+ regex.indexOf('}') == -1 &&
+ regex.indexOf('(') == -1 &&
+ regex.indexOf(')') == -1 &&
+ regex.indexOf('?') == -1 &&
+ regex.indexOf('.') == -1 &&
+ regex.indexOf('+') == -1 &&
+ regex.indexOf('\\') == -1 &&
+ regex.indexOf('*') == -1 &&
+ regex.indexOf('^') == -1 &&
+ regex.indexOf('$') == -1 &&
+ regex.indexOf('|') == -1);
+ }
+
/**
* Compiles the given regular expression and attempts to match the given
* input against it.
@@ -1182,14 +1203,21 @@ public int flags() {
* If the expression's syntax is invalid
*
* @diffblue.untested
- * @diffblue.noSupport
+ * @diffblue.limitedSupport Regex can only be a plain string.
*/
public static boolean matches(String regex, CharSequence input) {
// Pattern p = Pattern.compile(regex);
// Matcher m = p.matcher(input);
// return m.matches();
- CProver.notModelled();
- return CProver.nondetBoolean();
+
+ // DIFFBLUE MODEL LIBRARY
+ // We disallow special characters so that we can do matching using equals.
+ cproverAssumeIsPlainString(regex);
+ //
+ if (input == null) {
+ throw new NullPointerException(); // JDK throws NPE when the 2nd param is null
+ }
+ return regex.equals(input);
}
/**
@@ -1377,4 +1405,4705 @@ public static String quote(String s) {
CProver.notModelled();
return CProver.nondetWithoutNullForNotModelled();
}
+
+ /**
+ * Recompile the Pattern instance from a stream. The original pattern
+ * string is read in and the object tree is recompiled from it.
+ */
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private void readObject(java.io.ObjectInputStream s)
+ // throws java.io.IOException, ClassNotFoundException {
+
+ // // Read in all fields
+ // s.defaultReadObject();
+
+ // // Initialize counts
+ // capturingGroupCount = 1;
+ // localCount = 0;
+
+ // // if length > 0, the Pattern is lazily compiled
+ // compiled = false;
+ // if (pattern.length() == 0) {
+ // root = new Start(lastAccept);
+ // matchRoot = lastAccept;
+ // compiled = true;
+ // }
+ // }
+
+ /**
+ * This private constructor is used to create all Patterns. The pattern
+ * string and match flags are all that is needed to completely describe
+ * a Pattern. An empty pattern string results in an object tree with
+ * only a Start node and a LastNode node.
+ */
+ // DIFFBLUE MODEL LIBRARY - argument `f` is ignored for now but kept
+ // to stay closer to the original implementation
+ private Pattern(String p, int f) {
+ // DIFFBLUE MODEL LIBRARY
+ // We disallow special characters so that we can use equals for matching.
+ cproverAssumeIsPlainString(p);
+ pattern = p;
+ // pattern = p;
+ // flags = f;
+
+ // // to use UNICODE_CASE if UNICODE_CHARACTER_CLASS present
+ // if ((flags & UNICODE_CHARACTER_CLASS) != 0)
+ // flags |= UNICODE_CASE;
+
+ // // Reset group index count
+ // capturingGroupCount = 1;
+ // localCount = 0;
+
+ // if (pattern.length() > 0) {
+ // compile();
+ // } else {
+ // root = new Start(lastAccept);
+ // matchRoot = lastAccept;
+ // }
+ }
+
+ /**
+ * The pattern is converted to normalizedD form and then a pure group
+ * is constructed to match canonical equivalences of the characters.
+ */
+ // DIFFBLUE MODEL LIBRARY - not used in model
+ // private void normalize() {
+ // boolean inCharClass = false;
+ // int lastCodePoint = -1;
+
+ // // Convert pattern into normalizedD form
+ // normalizedPattern = Normalizer.normalize(pattern, Normalizer.Form.NFD);
+ // patternLength = normalizedPattern.length();
+
+ // // Modify pattern to match canonical equivalences
+ // StringBuilder newPattern = new StringBuilder(patternLength);
+ // for(int i=0; idouble type.
+ *
+ * @author Joseph D. Darcy
+ */
+
+public class DoubleConsts {
+ /**
+ * Don't let anyone instantiate this class.
+ */
+ private DoubleConsts() {}
+
+ public static final double POSITIVE_INFINITY = java.lang.Double.POSITIVE_INFINITY;
+ public static final double NEGATIVE_INFINITY = java.lang.Double.NEGATIVE_INFINITY;
+ public static final double NaN = java.lang.Double.NaN;
+ public static final double MAX_VALUE = java.lang.Double.MAX_VALUE;
+ public static final double MIN_VALUE = java.lang.Double.MIN_VALUE;
+
+ /**
+ * A constant holding the smallest positive normal value of type
+ * double, 2-1022. It is equal to the
+ * value returned by
+ * Double.longBitsToDouble(0x0010000000000000L).
+ *
+ * @since 1.5
+ */
+ public static final double MIN_NORMAL = 2.2250738585072014E-308;
+
+
+ /**
+ * The number of logical bits in the significand of a
+ * double number, including the implicit bit.
+ */
+ public static final int SIGNIFICAND_WIDTH = 53;
+
+ /**
+ * Maximum exponent a finite double number may have.
+ * It is equal to the value returned by
+ * Math.ilogb(Double.MAX_VALUE).
+ */
+ public static final int MAX_EXPONENT = 1023;
+
+ /**
+ * Minimum exponent a normalized double number may
+ * have. It is equal to the value returned by
+ * Math.ilogb(Double.MIN_NORMAL).
+ */
+ public static final int MIN_EXPONENT = -1022;
+
+ /**
+ * The exponent the smallest positive double
+ * subnormal value would have if it could be normalized. It is
+ * equal to the value returned by
+ * FpUtils.ilogb(Double.MIN_VALUE).
+ */
+ public static final int MIN_SUB_EXPONENT = MIN_EXPONENT -
+ (SIGNIFICAND_WIDTH - 1);
+
+ /**
+ * Bias used in representing a double exponent.
+ */
+ public static final int EXP_BIAS = 1023;
+
+ /**
+ * Bit mask to isolate the sign bit of a double.
+ */
+ public static final long SIGN_BIT_MASK = 0x8000000000000000L;
+
+ /**
+ * Bit mask to isolate the exponent field of a
+ * double.
+ */
+ public static final long EXP_BIT_MASK = 0x7FF0000000000000L;
+
+ /**
+ * Bit mask to isolate the significand field of a
+ * double.
+ */
+ public static final long SIGNIF_BIT_MASK = 0x000FFFFFFFFFFFFFL;
+
+ static {
+ // verify bit masks cover all bit positions and that the bit
+ // masks are non-overlapping
+ assert(((SIGN_BIT_MASK | EXP_BIT_MASK | SIGNIF_BIT_MASK) == ~0L) &&
+ (((SIGN_BIT_MASK & EXP_BIT_MASK) == 0L) &&
+ ((SIGN_BIT_MASK & SIGNIF_BIT_MASK) == 0L) &&
+ ((EXP_BIT_MASK & SIGNIF_BIT_MASK) == 0L)));
+ }
+}
diff --git a/src/main/java/sun/misc/FloatConsts.java b/src/main/java/sun/misc/FloatConsts.java
new file mode 100644
index 0000000..4345c19
--- /dev/null
+++ b/src/main/java/sun/misc/FloatConsts.java
@@ -0,0 +1,112 @@
+/*
+ * Copyright (c) 2003, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package sun.misc;
+
+/**
+ * This class contains additional constants documenting limits of the
+ * float type.
+ *
+ * @author Joseph D. Darcy
+ */
+
+public class FloatConsts {
+ /**
+ * Don't let anyone instantiate this class.
+ */
+ private FloatConsts() {}
+
+ public static final float POSITIVE_INFINITY = java.lang.Float.POSITIVE_INFINITY;
+ public static final float NEGATIVE_INFINITY = java.lang.Float.NEGATIVE_INFINITY;
+ public static final float NaN = java.lang.Float.NaN;
+ public static final float MAX_VALUE = java.lang.Float.MAX_VALUE;
+ public static final float MIN_VALUE = java.lang.Float.MIN_VALUE;
+
+ /**
+ * A constant holding the smallest positive normal value of type
+ * float, 2-126. It is equal to the value
+ * returned by Float.intBitsToFloat(0x00800000).
+ */
+ public static final float MIN_NORMAL = 1.17549435E-38f;
+
+ /**
+ * The number of logical bits in the significand of a
+ * float number, including the implicit bit.
+ */
+ public static final int SIGNIFICAND_WIDTH = 24;
+
+ /**
+ * Maximum exponent a finite float number may have.
+ * It is equal to the value returned by
+ * Math.ilogb(Float.MAX_VALUE).
+ */
+ public static final int MAX_EXPONENT = 127;
+
+ /**
+ * Minimum exponent a normalized float number may
+ * have. It is equal to the value returned by
+ * Math.ilogb(Float.MIN_NORMAL).
+ */
+ public static final int MIN_EXPONENT = -126;
+
+ /**
+ * The exponent the smallest positive float subnormal
+ * value would have if it could be normalized. It is equal to the
+ * value returned by FpUtils.ilogb(Float.MIN_VALUE).
+ */
+ public static final int MIN_SUB_EXPONENT = MIN_EXPONENT -
+ (SIGNIFICAND_WIDTH - 1);
+
+ /**
+ * Bias used in representing a float exponent.
+ */
+ public static final int EXP_BIAS = 127;
+
+ /**
+ * Bit mask to isolate the sign bit of a float.
+ */
+ public static final int SIGN_BIT_MASK = 0x80000000;
+
+ /**
+ * Bit mask to isolate the exponent field of a
+ * float.
+ */
+ public static final int EXP_BIT_MASK = 0x7F800000;
+
+ /**
+ * Bit mask to isolate the significand field of a
+ * float.
+ */
+ public static final int SIGNIF_BIT_MASK = 0x007FFFFF;
+
+ static {
+ // verify bit masks cover all bit positions and that the bit
+ // masks are non-overlapping
+ assert(((SIGN_BIT_MASK | EXP_BIT_MASK | SIGNIF_BIT_MASK) == ~0) &&
+ (((SIGN_BIT_MASK & EXP_BIT_MASK) == 0) &&
+ ((SIGN_BIT_MASK & SIGNIF_BIT_MASK) == 0) &&
+ ((EXP_BIT_MASK & SIGNIF_BIT_MASK) == 0)));
+ }
+}