From: yeom Date: Tue, 20 Sep 2011 01:41:12 +0000 (+0000) Subject: bug fixes + annotations X-Git-Url: http://plrg.eecs.uci.edu/git/?p=IRC.git;a=commitdiff_plain;h=1b1cd580d16bc4f8b514ce9ff8b88f2b7072c0d7 bug fixes + annotations --- diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index ab026926..76a9d7fa 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -841,6 +841,10 @@ public class FlowDownCheck { // values // in this case, we don't need to check flow down rule! + System.out.println("\n#tertiary cond=" + tn.getCond().printNode(0) + " Loc=" + condLoc); + System.out.println("# true=" + tn.getTrueExpr().printNode(0) + " Loc=" + trueLoc); + System.out.println("# false=" + tn.getFalseExpr().printNode(0) + " Loc=" + falseLoc); + // check if condLoc is higher than trueLoc & falseLoc if (!trueLoc.get(0).isTop() && !CompositeLattice.isGreaterThan(condLoc, trueLoc, generateErrorMessage(cd, tn))) { @@ -892,6 +896,7 @@ public class FlowDownCheck { checkLocationFromExpressionNode(md, nametable, min.getExpression(), new CompositeLocation(), constraint, false); } else { + System.out.println("min=" + min.getMethod()); if (min.getMethod().isStatic()) { String globalLocId = ssjava.getMethodLattice(md).getGlobalLoc(); if (globalLocId == null) { @@ -906,18 +911,13 @@ public class FlowDownCheck { } - // System.out.println("\n#checkLocationFromMethodInvokeNode=" + - // min.printNode(0) - // + " baseLocation=" + baseLocation + " constraint=" + constraint); + System.out.println("\n#checkLocationFromMethodInvokeNode=" + min.printNode(0) + + " baseLocation=" + baseLocation + " constraint=" + constraint); if (constraint != null) { int compareResult = CompositeLattice.compare(constraint, baseLocation, true, generateErrorMessage(cd, min)); - - if (compareResult == ComparisonResult.LESS) { - throw new Error("Method invocation does not respect the current branch constraint at " - + generateErrorMessage(cd, min)); - } else if (compareResult != ComparisonResult.GREATER) { + if (compareResult != ComparisonResult.GREATER) { // if the current constraint is higher than method's THIS location // no need to check constraints! CompositeLocation calleeConstraint = @@ -1141,9 +1141,29 @@ public class FlowDownCheck { int callerResult = CompositeLattice.compare(callerLoc1, callerLoc2, true, generateErrorMessage(md.getClassDesc(), min)); + System.out.println("callerResult=" + callerResult); int calleeResult = CompositeLattice.compare(calleeLoc1, calleeLoc2, true, generateErrorMessage(md.getClassDesc(), min)); + System.out.println("calleeResult=" + calleeResult); + + if (callerResult == ComparisonResult.EQUAL) { + if (ssjava.isSharedLocation(callerLoc1.get(callerLoc1.getSize() - 1)) + && ssjava.isSharedLocation(callerLoc2.get(callerLoc2.getSize() - 1))) { + // if both of them are shared locations, promote them to + // "GREATER relation" + callerResult = ComparisonResult.GREATER; + } + } + + if (calleeResult == ComparisonResult.EQUAL) { + if (ssjava.isSharedLocation(calleeLoc1.get(calleeLoc1.getSize() - 1)) + && ssjava.isSharedLocation(calleeLoc2.get(calleeLoc2.getSize() - 1))) { + // if both of them are shared locations, promote them to + // "GREATER relation" + calleeResult = ComparisonResult.GREATER; + } + } if (calleeResult == ComparisonResult.GREATER && callerResult != ComparisonResult.GREATER) { @@ -1411,7 +1431,11 @@ public class FlowDownCheck { // System.out.println("### checkLocationFromFieldAccessNode=" + // fan.printNode(0)); // System.out.println("### left=" + left.printNode(0)); - if (!left.getType().isPrimitive()) { + + if (left.getType().isArray()) { + // array.length case: return the location of the array + return loc; + } else if (!left.getType().isPrimitive()) { Location fieldLoc = getFieldLocation(fd); loc.addLocation(fieldLoc); } @@ -1797,7 +1821,7 @@ public class FlowDownCheck { public static int compare(CompositeLocation loc1, CompositeLocation loc2, boolean ignore, String msg) { - // System.out.println("compare=" + loc1 + " " + loc2); + System.out.println("compare=" + loc1 + " " + loc2); int baseCompareResult = compareBaseLocationSet(loc1, loc2, false, ignore, msg); if (baseCompareResult == ComparisonResult.EQUAL) { diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java b/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java index 4f5f8f34..53e26e23 100644 --- a/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java +++ b/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java @@ -21,20 +21,20 @@ * * @author Florian */ -@LATTICE("V") +@LATTICE("FACE= avg); + for (@LOC("THIS,Classifier.C") int i = 0; i < this.scanAreas.length; ++i) { + @LOC("THIS,Classifier.V") boolean bright = (values[i] >= avg); isFaceYes *= (bright ? this.possibilities_FaceYes[i] : 1 - this.possibilities_FaceYes[i]); isFaceNo *= (bright ? this.possibilities_FaceNo[i] : 1 - this.possibilities_FaceNo[i]); } @@ -161,7 +163,7 @@ public class Classifier { public String toString() { @LOC("OUT") String str = ""; - for (@LOC("C") int i = 0; i < scanAreas.length; i++) { + for (@LOC("THIS,Classifier.C") int i = 0; i < scanAreas.length; i++) { str += scanAreas[i].toString() + "\n"; } diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/EyeDetector.java b/Robust/src/Benchmarks/SSJava/EyeTracking/EyeDetector.java index 22171742..e6bbd029 100644 --- a/Robust/src/Benchmarks/SSJava/EyeTracking/EyeDetector.java +++ b/Robust/src/Benchmarks/SSJava/EyeTracking/EyeDetector.java @@ -22,27 +22,32 @@ * * @author Florian Frankenberger */ +@LATTICE("IMG") +@METHODDEFAULT("OUT> 16, (pixelBuffer[position] & 0x00FF00) >> 8, pixelBuffer[position] & 0x0000FF }; // System.out.println("("+x+","+y+")="+color[0]+" "+color[1]+" "+color[2]); - final float acBrightness = getBrightness(color); + @LOC("V") final float acBrightness = getBrightness(color); if (acBrightness < brightness) { eyePosition = new Point(x + (int) percent, y + (int) percent); @@ -74,9 +80,9 @@ class EyeDetector { return eyePosition; } - private static float getBrightness(int[] color) { - int min = Math.min(Math.min(color[0], color[1]), color[2]); - int max = Math.max(Math.max(color[0], color[1]), color[2]); + private static float getBrightness(@LOC("IN") int[] color) { + @LOC("IN") int min = Math.min(Math.min(color[0], color[1]), color[2]); + @LOC("IN") int max = Math.max(Math.max(color[0], color[1]), color[2]); return 0.5f * (max + min); } diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/EyePosition.java b/Robust/src/Benchmarks/SSJava/EyeTracking/EyePosition.java index a4bf4670..5b4ffd5b 100644 --- a/Robust/src/Benchmarks/SSJava/EyeTracking/EyePosition.java +++ b/Robust/src/Benchmarks/SSJava/EyeTracking/EyePosition.java @@ -17,69 +17,78 @@ * along with LEA. If not, see . */ - /** * No description given. * * @author Florian Frankenberger */ +@LATTICE("POS") +@METHODDEFAULT("OUT 0.1) return Deviation.NONE; -// -// int maxDeviationX = (int)Math.round(this.faceRect.getWidth() / 4f); -// int maxDeviationY = (int)Math.round(this.faceRect.getWidth() / 8f); -// int minDeviation = (int)Math.round(this.faceRect.getWidth() / 16f); -// -// int deviationX = Math.abs(x - oldEyePosition.x); -// int directionX = sgn(x - oldEyePosition.x); -// if (deviationX < minDeviation || deviationX > maxDeviationX) directionX = 0; -// -// int deviationY = Math.abs(y - oldEyePosition.y); -// int directionY = sgn(y - oldEyePosition.y); -// if (deviationY < minDeviation || deviationY > maxDeviationY) directionY = 0; -// -// double deviationXPercent = deviationX / this.faceRect.getWidth(); -// double deviationYPercent = deviationY / this.faceRect.getWidth(); -// -// System.out.println(String.format("devX: %.2f | devY: %.2f", deviationXPercent*100f, deviationYPercent*100f)); -// return Deviation.getDirectionFor(directionX, directionY); -// } + public String toString() { + return "(" + x + "," + y + ")"; + } + // public Deviation getDeviation(EyePosition oldEyePosition) { + // if (oldEyePosition == null) return Deviation.NONE; + // + // //first we check if the faceRects are corresponding + // double widthChange = (this.faceRect.getWidth() - + // oldEyePosition.faceRect.getWidth()) / this.faceRect.getWidth(); + // if (widthChange > 0.1) return Deviation.NONE; + // + // int maxDeviationX = (int)Math.round(this.faceRect.getWidth() / 4f); + // int maxDeviationY = (int)Math.round(this.faceRect.getWidth() / 8f); + // int minDeviation = (int)Math.round(this.faceRect.getWidth() / 16f); + // + // int deviationX = Math.abs(x - oldEyePosition.x); + // int directionX = sgn(x - oldEyePosition.x); + // if (deviationX < minDeviation || deviationX > maxDeviationX) directionX = + // 0; + // + // int deviationY = Math.abs(y - oldEyePosition.y); + // int directionY = sgn(y - oldEyePosition.y); + // if (deviationY < minDeviation || deviationY > maxDeviationY) directionY = + // 0; + // + // double deviationXPercent = deviationX / this.faceRect.getWidth(); + // double deviationYPercent = deviationY / this.faceRect.getWidth(); + // + // System.out.println(String.format("devX: %.2f | devY: %.2f", + // deviationXPercent*100f, deviationYPercent*100f)); + // return Deviation.getDirectionFor(directionX, directionY); + // } - private static int sgn(int i) { - if (i > 0) return 1; - if (i < 0) return -1; - return 0; - } + private static int sgn(int i) { + if (i > 0) + return 1; + if (i < 0) + return -1; + return 0; + } } diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/FaceAndEyePosition.java b/Robust/src/Benchmarks/SSJava/EyeTracking/FaceAndEyePosition.java index 83955ec5..29e0f6ee 100644 --- a/Robust/src/Benchmarks/SSJava/EyeTracking/FaceAndEyePosition.java +++ b/Robust/src/Benchmarks/SSJava/EyeTracking/FaceAndEyePosition.java @@ -22,9 +22,13 @@ * * @author Florian Frankenberger */ +@LATTICE("POS") +@METHODDEFAULT("OUTJava Media Framework just start from here. + * @METHOD To test LEA with the first capture device from the + * Java Media Framework just start from here. * * @param args * @throws Exception @@ -87,15 +89,14 @@ public class LEA { lea.doRun(); } + @LATTICE("THISDouble represent primitive * double values. - * + * * Additionally, this class provides various helper functions and variables * related to doubles. - * + * * @author Paul Fisher * @author Andrew Haley (aph@cygnus.com) * @author Eric Blake (ebb9@email.byu.edu) @@ -54,36 +53,42 @@ * @since 1.0 * @status partly updated to 1.5 */ -public final class Double extends Number //implements Comparable +@LATTICE("V") +@METHODDEFAULT("OUT { /** * Compatible with JDK 1.0+. */ /** * The immutable value of this Double. - * + * * @serial the wrapped double */ + @LOC("V") private final double value; /** * Create a Double from the primitive double * specified. - * - * @param value the double argument + * + * @param value + * the double argument */ public Double(double value) { this.value = value; } /** - * Create a Double from the specified String. - * This method calls Double.parseDouble(). - * - * @param s the String to convert - * @throws NumberFormatException if s cannot be parsed as a - * double - * @throws NullPointerException if s is null + * Create a Double from the specified String. This + * method calls Double.parseDouble(). + * + * @param s + * the String to convert + * @throws NumberFormatException + * if s cannot be parsed as a double + * @throws NullPointerException + * if s is null * @see #parseDouble(String) */ public Double(String s) { @@ -91,126 +96,120 @@ public final class Double extends Number //implements Comparable } /** - * Convert the double to a String. - * Floating-point string representation is fairly complex: here is a - * rundown of the possible values. "[-]" indicates that a - * negative sign will be printed if the value (or exponent) is negative. - * "<number>" means a string of digits ('0' to '9'). - * "<digit>" means a single digit ('0' to '9').
- * + * Convert the double to a String. Floating-point + * string representation is fairly complex: here is a rundown of the possible + * values. "[-]" indicates that a negative sign will be printed + * if the value (or exponent) is negative. "<number>" means + * a string of digits ('0' to '9'). "<digit>" means a + * single digit ('0' to '9').
+ * * - * - * - * - * - * - * - * - * + * + * + * + * + * + * + * + * + * + * + * + * + * + * + * + * + * + * + * + * + * + * + * + * *
Value of DoubleString Representation
[+-] 0 [-]0.0
Between [+-] 10-3 and 107, exclusive[-]number.number
Other numeric value[-]<digit>.<number> - * E[-]<number>
[+-] infinity [-]Infinity
NaN NaN
Value of DoubleString Representation
[+-] 0[-]0.0
Between [+-] 10-3 and 107, exclusive[-]number.number
Other numeric value[-]<digit>.<number> + * E[-]<number>
[+-] infinity[-]Infinity
NaNNaN
- * - * Yes, negative zero is a possible value. Note that there is - * always a . and at least one digit printed after - * it: even if the number is 3, it will be printed as 3.0. - * After the ".", all digits will be printed except trailing zeros. The - * result is rounded to the shortest decimal number which will parse back - * to the same double. - * - *

To create other output formats, use {@link java.text.NumberFormat}. - * + * + * Yes, negative zero is a possible value. Note that there is + * always a . and at least one digit printed after it: + * even if the number is 3, it will be printed as 3.0. After the + * ".", all digits will be printed except trailing zeros. The result is + * rounded to the shortest decimal number which will parse back to the same + * double. + * + *

+ * To create other output formats, use {@link java.text.NumberFormat}. + * * @XXX specify where we are not in accord with the spec. - * - * @param d the double to convert + * + * @param d + * the double to convert * @return the String representing the double */ - public static String toString(double d) { + public static String toString(@LOC("IN") double d) { return String.valueOf(d); } /** - * Convert a double value to a hexadecimal string. This converts as - * follows: + * Convert a double value to a hexadecimal string. This converts as follows: *

    - *
  • A NaN value is converted to the string "NaN". - *
  • Positive infinity is converted to the string "Infinity". - *
  • Negative infinity is converted to the string "-Infinity". - *
  • For all other values, the first character of the result is '-' - * if the value is negative. This is followed by '0x1.' if the - * value is normal, and '0x0.' if the value is denormal. This is - * then followed by a (lower-case) hexadecimal representation of the - * mantissa, with leading zeros as required for denormal values. - * The next character is a 'p', and this is followed by a decimal - * representation of the unbiased exponent. + *
  • A NaN value is converted to the string "NaN". + *
  • Positive infinity is converted to the string "Infinity". + *
  • Negative infinity is converted to the string "-Infinity". + *
  • For all other values, the first character of the result is '-' if the + * value is negative. This is followed by '0x1.' if the value is normal, and + * '0x0.' if the value is denormal. This is then followed by a (lower-case) + * hexadecimal representation of the mantissa, with leading zeros as required + * for denormal values. The next character is a 'p', and this is followed by a + * decimal representation of the unbiased exponent. *
- * @param d the double value + * + * @param d + * the double value * @return the hexadecimal string representation * @since 1.5 */ public static String toHexString(double d) { /* - if (isNaN(d)) - return "NaN"; - if (isInfinite(d)) - return d < 0 ? "-Infinity" : "Infinity"; - - long bits = doubleToLongBits(d); - StringBuilder result = new StringBuilder(); - - if (bits < 0) - result.append('-'); - result.append("0x"); - - final int mantissaBits = 52; - final int exponentBits = 11; - long mantMask = (1L << mantissaBits) - 1; - long mantissa = bits & mantMask; - long expMask = (1L << exponentBits) - 1; - long exponent = (bits >>> mantissaBits) & expMask; - - result.append(exponent == 0 ? '0' : '1'); - result.append('.'); - result.append(Long.toHexString(mantissa)); - if (exponent == 0 && mantissa != 0) - { - // Treat denormal specially by inserting '0's to make - // the length come out right. The constants here are - // to account for things like the '0x'. - int offset = 4 + ((bits < 0) ? 1 : 0); - // The silly +3 is here to keep the code the same between - // the Float and Double cases. In Float the value is - // not a multiple of 4. - int desiredLength = offset + (mantissaBits + 3) / 4; - while (result.length() < desiredLength) - result.insert(offset, '0'); - } - result.append('p'); - if (exponent == 0 && mantissa == 0) - { - // Zero, so do nothing special. - } - else - { - // Apply bias. - boolean denormal = exponent == 0; - exponent -= (1 << (exponentBits - 1)) - 1; - // Handle denormal. - if (denormal) - ++exponent; - } - - result.append(Long.toString(exponent)); - return result.toString(); + * if (isNaN(d)) return "NaN"; if (isInfinite(d)) return d < 0 ? "-Infinity" + * : "Infinity"; + * + * long bits = doubleToLongBits(d); StringBuilder result = new + * StringBuilder(); + * + * if (bits < 0) result.append('-'); result.append("0x"); + * + * final int mantissaBits = 52; final int exponentBits = 11; long mantMask = + * (1L << mantissaBits) - 1; long mantissa = bits & mantMask; long expMask = + * (1L << exponentBits) - 1; long exponent = (bits >>> mantissaBits) & + * expMask; + * + * result.append(exponent == 0 ? '0' : '1'); result.append('.'); + * result.append(Long.toHexString(mantissa)); if (exponent == 0 && mantissa + * != 0) { // Treat denormal specially by inserting '0's to make // the + * length come out right. The constants here are // to account for things + * like the '0x'. int offset = 4 + ((bits < 0) ? 1 : 0); // The silly +3 is + * here to keep the code the same between // the Float and Double cases. In + * Float the value is // not a multiple of 4. int desiredLength = offset + + * (mantissaBits + 3) / 4; while (result.length() < desiredLength) + * result.insert(offset, '0'); } result.append('p'); if (exponent == 0 && + * mantissa == 0) { // Zero, so do nothing special. } else { // Apply bias. + * boolean denormal = exponent == 0; exponent -= (1 << (exponentBits - 1)) - + * 1; // Handle denormal. if (denormal) ++exponent; } + * + * result.append(Long.toString(exponent)); return result.toString(); */ return "0x0"; } /** - * Returns a Double object wrapping the value. - * In contrast to the Double constructor, this method - * may cache some values. It is used by boxing conversion. - * - * @param val the value to wrap + * Returns a Double object wrapping the value. In contrast to the + * Double constructor, this method may cache some values. It is + * used by boxing conversion. + * + * @param val + * the value to wrap * @return the Double * @since 1.5 */ @@ -221,12 +220,14 @@ public final class Double extends Number //implements Comparable /** * Create a new Double object using the String. - * - * @param s the String to convert + * + * @param s + * the String to convert * @return the new Double - * @throws NumberFormatException if s cannot be parsed as a - * double - * @throws NullPointerException if s is null. + * @throws NumberFormatException + * if s cannot be parsed as a double + * @throws NullPointerException + * if s is null. * @see #parseDouble(String) */ public static Double valueOf(String s) { @@ -236,6 +237,7 @@ public final class Double extends Number //implements Comparable /** * Parse the specified String as a double. The * extended BNF grammar is as follows:
+ * * 
    * DecodableString:
    *      ( [ - | + ] NaN )
@@ -252,30 +254,35 @@ public final class Double extends Number //implements Comparable
    *              [ - | + ] { Digit }+ )
    * Digit: '0' through '9'
    *
- * - *

NaN and infinity are special cases, to allow parsing of the output - * of toString. Otherwise, the result is determined by calculating - * n * 10exponent to infinite precision, then rounding - * to the nearest double. Remember that many numbers cannot be precisely - * represented in floating point. In case of overflow, infinity is used, - * and in case of underflow, signed zero is used. Unlike Integer.parseInt, - * this does not accept Unicode digits outside the ASCII range. - * - *

If an unexpected character is found in the String, a - * NumberFormatException will be thrown. Leading and trailing - * 'whitespace' is ignored via String.trim(), but spaces - * internal to the actual number are not allowed. - * - *

To parse numbers according to another format, consider using + * + *

+ * NaN and infinity are special cases, to allow parsing of the output of + * toString. Otherwise, the result is determined by calculating + * n * 10exponent to infinite precision, then rounding to + * the nearest double. Remember that many numbers cannot be precisely + * represented in floating point. In case of overflow, infinity is used, and + * in case of underflow, signed zero is used. Unlike Integer.parseInt, this + * does not accept Unicode digits outside the ASCII range. + * + *

+ * If an unexpected character is found in the String, a + * NumberFormatException will be thrown. Leading and trailing + * 'whitespace' is ignored via String.trim(), but spaces internal + * to the actual number are not allowed. + * + *

+ * To parse numbers according to another format, consider using * {@link java.text.NumberFormat}. - * + * * @XXX specify where/how we are not in accord with the spec. - * - * @param str the String to convert + * + * @param str + * the String to convert * @return the double value of s - * @throws NumberFormatException if s cannot be parsed as a - * double - * @throws NullPointerException if s is null + * @throws NumberFormatException + * if s cannot be parsed as a double + * @throws NullPointerException + * if s is null * @see #MIN_VALUE * @see #MAX_VALUE * @see #POSITIVE_INFINITY @@ -287,27 +294,30 @@ public final class Double extends Number //implements Comparable } public static native double nativeparsedouble(String str); + public static native double nativeparsedouble(int start, int length, byte[] str); /** - * Return true if the double has the same - * value as NaN, otherwise return false. - * - * @param v the double to compare + * Return true if the double has the same value as + * NaN, otherwise return false. + * + * @param v + * the double to compare * @return whether the argument is NaN. */ - public static boolean isNaN(double v) { + public static boolean isNaN(@LOC("IN") double v) { // This works since NaN != NaN is the only reflexive inequality // comparison which returns true. return v != v; } /** - * Return true if the double has a value - * equal to either NEGATIVE_INFINITY or - * POSITIVE_INFINITY, otherwise return false. - * - * @param v the double to compare + * Return true if the double has a value equal to + * either NEGATIVE_INFINITY or POSITIVE_INFINITY, + * otherwise return false. + * + * @param v + * the double to compare * @return whether the argument is (-/+) infinity. */ public static boolean isInfinite(double v) { @@ -315,9 +325,9 @@ public final class Double extends Number //implements Comparable } /** - * Return true if the value of this Double - * is the same as NaN, otherwise return false. - * + * Return true if the value of this Double is the + * same as NaN, otherwise return false. + * * @return whether this Double is NaN */ public boolean isNaN() { @@ -325,10 +335,10 @@ public final class Double extends Number //implements Comparable } /** - * Return true if the value of this Double - * is the same as NEGATIVE_INFINITY or - * POSITIVE_INFINITY, otherwise return false. - * + * Return true if the value of this Double is the + * same as NEGATIVE_INFINITY or POSITIVE_INFINITY, + * otherwise return false. + * * @return whether this Double is (-/+) infinity */ public boolean isInfinite() { @@ -336,10 +346,10 @@ public final class Double extends Number //implements Comparable } /** - * Convert the double value of this Double - * to a String. This method calls - * Double.toString(double) to do its dirty work. - * + * Convert the double value of this Double to a + * String. This method calls Double.toString(double) + * to do its dirty work. + * * @return the String representation * @see #toString(double) */ @@ -349,7 +359,7 @@ public final class Double extends Number //implements Comparable /** * Return the value of this Double as a byte. - * + * * @return the byte value * @since 1.1 */ @@ -359,7 +369,7 @@ public final class Double extends Number //implements Comparable /** * Return the value of this Double as a short. - * + * * @return the short value * @since 1.1 */ @@ -369,7 +379,7 @@ public final class Double extends Number //implements Comparable /** * Return the value of this Double as an int. - * + * * @return the int value */ public int intValue() { @@ -378,7 +388,7 @@ public final class Double extends Number //implements Comparable /** * Return the value of this Double as a long. - * + * * @return the long value */ public long longValue() { @@ -387,7 +397,7 @@ public final class Double extends Number //implements Comparable /** * Return the value of this Double as a float. - * + * * @return the float value */ public float floatValue() { @@ -396,7 +406,7 @@ public final class Double extends Number //implements Comparable /** * Return the value of this Double. - * + * * @return the double value */ public double doubleValue() { @@ -404,16 +414,16 @@ public final class Double extends Number //implements Comparable } /** - * Return a hashcode representing this Object. Double's hash - * code is calculated by:
+ * Return a hashcode representing this Object. Double's hash code + * is calculated by:
* long v = Double.doubleToLongBits(doubleValue());
* int hash = (int)(v^(v>>32)). - * + * * @return this Object's hash code * @see #doubleToLongBits(double) */ public int hashCode() { - long v = doubleToLongBits(value); + @LOC("OUT") long v = doubleToLongBits(value); return (int) (v ^ (v >>> 32)); } @@ -423,12 +433,14 @@ public final class Double extends Number //implements Comparable * two doubles with ==, this treats two instances of * Double.NaN as equal, but treats 0.0 and * -0.0 as unequal. - * - *

Note that d1.equals(d2) is identical to + * + *

+ * Note that d1.equals(d2) is identical to * doubleToLongBits(d1.doubleValue()) == * doubleToLongBits(d2.doubleValue()). - * - * @param obj the object to compare + * + * @param obj + * the object to compare * @return whether the objects are semantically equal */ public boolean equals(Object obj) { @@ -447,73 +459,75 @@ public final class Double extends Number //implements Comparable /** * Convert the double to the IEEE 754 floating-point "double format" bit - * layout. Bit 63 (the most significant) is the sign bit, bits 62-52 - * (masked by 0x7ff0000000000000L) represent the exponent, and bits 51-0 - * (masked by 0x000fffffffffffffL) are the mantissa. This function - * collapses all versions of NaN to 0x7ff8000000000000L. The result of this - * function can be used as the argument to - * Double.longBitsToDouble(long) to obtain the original - * double value. - * - * @param value the double to convert + * layout. Bit 63 (the most significant) is the sign bit, bits 62-52 (masked + * by 0x7ff0000000000000L) represent the exponent, and bits 51-0 (masked by + * 0x000fffffffffffffL) are the mantissa. This function collapses all versions + * of NaN to 0x7ff8000000000000L. The result of this function can be used as + * the argument to Double.longBitsToDouble(long) to obtain the + * original double value. + * + * @param value + * the double to convert * @return the bits of the double * @see #longBitsToDouble(long) */ - public static long doubleToLongBits(double value) { + public static long doubleToLongBits(@LOC("IN") double value) { if (isNaN(value)) return 0x7ff8000000000000L; else - return /*VMDouble.*/ doubleToRawLongBits(value); + return /* VMDouble. */doubleToRawLongBits(value); } /** * Convert the double to the IEEE 754 floating-point "double format" bit - * layout. Bit 63 (the most significant) is the sign bit, bits 62-52 - * (masked by 0x7ff0000000000000L) represent the exponent, and bits 51-0 - * (masked by 0x000fffffffffffffL) are the mantissa. This function - * leaves NaN alone, rather than collapsing to a canonical value. The - * result of this function can be used as the argument to - * Double.longBitsToDouble(long) to obtain the original - * double value. - * - * @param value the double to convert + * layout. Bit 63 (the most significant) is the sign bit, bits 62-52 (masked + * by 0x7ff0000000000000L) represent the exponent, and bits 51-0 (masked by + * 0x000fffffffffffffL) are the mantissa. This function leaves NaN alone, + * rather than collapsing to a canonical value. The result of this function + * can be used as the argument to Double.longBitsToDouble(long) + * to obtain the original double value. + * + * @param value + * the double to convert * @return the bits of the double * @see #longBitsToDouble(long) */ - /*public static long doubleToRawLongBits(double value) - { - return VMDouble.doubleToRawLongBits(value); - }*/ + /* + * public static long doubleToRawLongBits(double value) { return + * VMDouble.doubleToRawLongBits(value); } + */ public static native long doubleToRawLongBits(double value); /** - * Convert the argument in IEEE 754 floating-point "double format" bit - * layout to the corresponding float. Bit 63 (the most significant) is the - * sign bit, bits 62-52 (masked by 0x7ff0000000000000L) represent the - * exponent, and bits 51-0 (masked by 0x000fffffffffffffL) are the mantissa. - * This function leaves NaN alone, so that you can recover the bit pattern - * with Double.doubleToRawLongBits(double). - * - * @param bits the bits to convert + * Convert the argument in IEEE 754 floating-point "double format" bit layout + * to the corresponding float. Bit 63 (the most significant) is the sign bit, + * bits 62-52 (masked by 0x7ff0000000000000L) represent the exponent, and bits + * 51-0 (masked by 0x000fffffffffffffL) are the mantissa. This function leaves + * NaN alone, so that you can recover the bit pattern with + * Double.doubleToRawLongBits(double). + * + * @param bits + * the bits to convert * @return the double represented by the bits * @see #doubleToLongBits(double) * @see #doubleToRawLongBits(double) */ - /*public static double longBitsToDouble(long bits) - { - return VMDouble.longBitsToDouble(bits); - }*/ + /* + * public static double longBitsToDouble(long bits) { return + * VMDouble.longBitsToDouble(bits); } + */ public static native double longBitsToDouble(long bits); /** * Compare two Doubles numerically by comparing their double * values. The result is positive if the first is greater, negative if the - * second is greater, and 0 if the two are equal. However, this special - * cases NaN and signed zero as follows: NaN is considered greater than - * all other doubles, including POSITIVE_INFINITY, and positive - * zero is considered greater than negative zero. - * - * @param d the Double to compare + * second is greater, and 0 if the two are equal. However, this special cases + * NaN and signed zero as follows: NaN is considered greater than all other + * doubles, including POSITIVE_INFINITY, and positive zero is + * considered greater than negative zero. + * + * @param d + * the Double to compare * @return the comparison * @since 1.2 */ @@ -522,12 +536,14 @@ public final class Double extends Number //implements Comparable } /** - * Behaves like new Double(x).compareTo(new Double(y)); in - * other words this compares two doubles, special casing NaN and zero, - * without the overhead of objects. - * - * @param x the first double to compare - * @param y the second double to compare + * Behaves like new Double(x).compareTo(new Double(y)); in other + * words this compares two doubles, special casing NaN and zero, without the + * overhead of objects. + * + * @param x + * the first double to compare + * @param y + * the second double to compare * @return the comparison * @since 1.4 */ @@ -546,11 +562,11 @@ public final class Double extends Number //implements Comparable // handle NaNs: if (x != x) - return (y != y)?0:1; + return (y != y) ? 0 : 1; else if (y != y) return -1; // handle +/- 0.0 - return (lx < ly)?-1:1; + return (lx < ly) ? -1 : 1; } } diff --git a/Robust/src/ClassLibrary/SSJava/Math.java b/Robust/src/ClassLibrary/SSJava/Math.java index b6f4a130..85596dc0 100644 --- a/Robust/src/ClassLibrary/SSJava/Math.java +++ b/Robust/src/ClassLibrary/SSJava/Math.java @@ -1,5 +1,5 @@ @LATTICE("B b) ? a : b; } - public static float max(float a, float b) { + public static float max(@LOC("IN") float a, @LOC("IN") float b) { return (a > b) ? a : b; } - public static int max(int a, int b) { + public static int max(@LOC("IN") int a, @LOC("IN") int b) { return (a > b) ? a : b; } @@ -77,7 +77,7 @@ public class Math { return r; } - public static int round(float a) { + public static int round(@LOC("IN") float a) { // this check for NaN, from JLS 15.21.1, saves a method call return (int) floor(a + 0.5f); } diff --git a/Robust/src/ClassLibrary/SSJava/String.java b/Robust/src/ClassLibrary/SSJava/String.java index 5f963399..35c15053 100644 --- a/Robust/src/ClassLibrary/SSJava/String.java +++ b/Robust/src/ClassLibrary/SSJava/String.java @@ -295,7 +295,7 @@ public class String { return this; } - @LATTICE("OUT