bug fixes + annotations
authoryeom <yeom>
Tue, 20 Sep 2011 01:41:12 +0000 (01:41 +0000)
committeryeom <yeom>
Tue, 20 Sep 2011 01:41:12 +0000 (01:41 +0000)
17 files changed:
Robust/src/Analysis/SSJava/FlowDownCheck.java
Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java
Robust/src/Benchmarks/SSJava/EyeTracking/EyeDetector.java
Robust/src/Benchmarks/SSJava/EyeTracking/EyePosition.java
Robust/src/Benchmarks/SSJava/EyeTracking/FaceAndEyePosition.java
Robust/src/Benchmarks/SSJava/EyeTracking/Image.java
Robust/src/Benchmarks/SSJava/EyeTracking/ImageReader.java
Robust/src/Benchmarks/SSJava/EyeTracking/IntegralImageData.java
Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java
Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java
Robust/src/Benchmarks/SSJava/EyeTracking/LOC.java [new file with mode: 0644]
Robust/src/Benchmarks/SSJava/EyeTracking/Point.java
Robust/src/Benchmarks/SSJava/EyeTracking/Rectangle2D.java
Robust/src/Benchmarks/SSJava/EyeTracking/ScanArea.java
Robust/src/ClassLibrary/SSJava/Double.java
Robust/src/ClassLibrary/SSJava/Math.java
Robust/src/ClassLibrary/SSJava/String.java

index ab02692..76a9d7f 100644 (file)
@@ -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) {
index 4f5f8f3..53e26e2 100644 (file)
  * 
  * @author Florian
  */
-@LATTICE("V")
+@LATTICE("FACE<V,V<C,C<SCAN,C*,V*")
 @METHODDEFAULT("OUT<V,V<THIS,THIS<C,C<IN,C*,V*,THISLOC=THIS,RETURNLOC=OUT")
 public class Classifier {
 
-  @LOC("V")
+  @LOC("SCAN")
   private ScanArea[] scanAreas;
 
-  @LOC("V")
+  @LOC("FACE")
   private float[] possibilities_FaceYes;
-  @LOC("V")
+  @LOC("FACE")
   private float[] possibilities_FaceNo;
-  @LOC("V")
+  @LOC("FACE")
   private int possibilityFaceYes = 0;
-  @LOC("V")
+  @LOC("FACE")
   private int possibilityFaceNo = 0;
 
   public Classifier(int numScanAreas) {
@@ -74,14 +74,16 @@ public class Classifier {
    * @param translationY
    * @return true if this region was classified as face, else false
    */
-  public boolean classifyFace(@LOC("IN") IntegralImageData image, @LOC("IN") float scaleFactor,
-      @LOC("IN") int translationX, @LOC("IN") int translationY, @LOC("IN") float borderline) {
+  @LATTICE("OUT<V,V<C,C<THIS,THIS<IN,C*,V*,THISLOC=THIS,RETURNLOC=OUT")
+  public boolean classifyFace(@LOC("THIS,Classifier.C") IntegralImageData image,
+      @LOC("IN") float scaleFactor, @LOC("IN") int translationX, @LOC("IN") int translationY,
+      @LOC("IN") float borderline) {
 
-    @LOC("V") long values[] = new long[this.scanAreas.length];
+    @LOC("THIS,Classifier.V") long values[] = new long[scanAreas.length];
 
-    @LOC("V") float avg = 0f;
-    @LOC("V") int avgItems = 0;
-    for (@LOC("C") int i = 0; i < this.scanAreas.length; ++i) {
+    @LOC("THIS,Classifier.V") float avg = 0f;
+    @LOC("THIS,Classifier.C") int avgItems = 0;
+    for (@LOC("THIS,Classifier.C") int i = 0; i < scanAreas.length; ++i) {
       values[i] = 0l;
 
       values[i] +=
@@ -116,8 +118,8 @@ public class Classifier {
     @LOC("OUT") float isFaceNo = 1.0f;// this.possibilityFaceNo /
                                       // (float)amountYesNo;
 
-    for (@LOC("C") int i = 0; i < this.scanAreas.length; ++i) {
-      @LOC("V") boolean bright = (values[i] >= 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";
     }
 
index 2217174..e6bbd02 100644 (file)
  * 
  * @author Florian Frankenberger
  */
+@LATTICE("IMG")
+@METHODDEFAULT("OUT<THIS,THIS<IN,OUT*,THISLOC=THIS,RETURNLOC=OUT")
 class EyeDetector {
 
+  @LOC("IMG")
   private int width;
+  @LOC("IMG")
   private int height;
+  @LOC("IMG")
   private int[] pixelBuffer;
-
+  @LOC("IMG")
   double percent;
 
   public EyeDetector(Image image, Rectangle2D faceRect) {
 
     percent = 0.15 * faceRect.getWidth();
-    faceRect =
+    Rectangle2D adjustedFaceRect =
         new Rectangle2D(faceRect.getX() + percent, faceRect.getY() + percent, faceRect.getWidth()
             - percent, faceRect.getHeight() - 2 * percent);
 
-    width = (int) faceRect.getWidth() / 2;
-    height = (int) faceRect.getHeight() / 2;
+    width = (int) adjustedFaceRect.getWidth() / 2;
+    height = (int) adjustedFaceRect.getHeight() / 2;
     pixelBuffer = new int[width * height];
 
-    int startX = (int) faceRect.getX();
-    int startY = (int) faceRect.getY();
+    int startX = (int) adjustedFaceRect.getX();
+    int startY = (int) adjustedFaceRect.getY();
 
     for (int y = 0; y < height; y++) {
       for (int x = 0; x < width; x++) {
@@ -52,17 +57,18 @@ class EyeDetector {
 
   }
 
+  @LATTICE("OUT,V<THIS,THIS<C,C*,THISLOC=THIS,RETURNLOC=OUT")
   public Point detectEye() {
-    Point eyePosition = null;
-    float brightness = 255f;
-    for (int y = 0; y < height; ++y) {
-      for (int x = 0; x < width; ++x) {
-        final int position = y * width + x;
-        final int[] color =
+    @LOC("OUT") Point eyePosition = null;
+    @LOC("V") float brightness = 255f;
+    for (@LOC("C") int y = 0; y < height; ++y) {
+      for (@LOC("C") int x = 0; x < width; ++x) {
+        @LOC("V") final int position = y * width + x;
+        @LOC("V") final int[] color =
             new int[] { (pixelBuffer[position] & 0xFF0000) >> 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);
   }
index a4bf467..5b4ffd5 100644 (file)
  * along with LEA. If not, see <http://www.gnu.org/licenses/>.
  */
 
-
 /**
  * No description given.
  * 
  * @author Florian Frankenberger
  */
+@LATTICE("POS")
+@METHODDEFAULT("OUT<THIS,THISLOC=THIS,RETURNLOC=OUT")
 public class EyePosition {
-    private int x;
-    private int y;
-    private Rectangle2D faceRect;
+  @LOC("POS")
+  private int x;
+  @LOC("POS")
+  private int y;
+  @LOC("POS")
+  private Rectangle2D faceRect;
+
+  public EyePosition(Point p, Rectangle2D faceRect) {
+    this(p.x, p.y, faceRect);
+  }
+
+  public EyePosition(int x, int y, Rectangle2D faceRect) {
+    this.x = x;
+    this.y = y;
+    this.faceRect = faceRect;
+  }
 
-    public EyePosition(Point p, Rectangle2D faceRect) {
-        this(p.x, p.y, faceRect);
-    }
-    
-    public EyePosition(int x, int y, Rectangle2D faceRect) {
-        this.x = x;
-        this.y = y;
-        this.faceRect = faceRect;
-    }
+  public int getX() {
+    return this.x;
+  }
 
-    public int getX() {
-        return this.x;
-    }
+  public int getY() {
+    return this.y;
+  }
 
-    public int getY() {
-        return this.y;
-    }
-    
-    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);
-//    }
+  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;
+  }
 }
index 83955ec..29e0f6e 100644 (file)
  * 
  * @author Florian Frankenberger
  */
+@LATTICE("POS")
+@METHODDEFAULT("OUT<THIS,THISLOC=THIS,RETURNLOC=OUT")
 public class FaceAndEyePosition {
 
+  @LOC("POS")
   private Rectangle2D facePosition;
+  @LOC("POS")
   private EyePosition eyePosition;
 
   public FaceAndEyePosition(Rectangle2D facePosition, EyePosition eyePosition) {
index 5e83b46..e7c2e82 100644 (file)
@@ -1,7 +1,12 @@
+@LATTICE("IMG")
+@METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
 public class Image {
 
+  @LOC("IMG")
   int width;
+  @LOC("IMG")
   int height;
+  @LOC("IMG")
   int pixel[][];
 
   public Image(int width, int height) {
index 461971d..d89c14c 100644 (file)
@@ -2,7 +2,8 @@ public class ImageReader {
   public ImageReader() {
   }
 
-  public Image readImage(String file) {
+  @TRUST
+  public static Image readImage(String file) {
 
     FileInputStream fs = new FileInputStream(file);
     int bflen = 14; // 14 byte BITMAPFILEHEADER
index 8cc3cba..d74880b 100644 (file)
  * 
  * @author Florian Frankenberger
  */
+@LATTICE("IMG")
+@METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
 public class IntegralImageData {
 
+  @LOC("IMG")
   private long[][] integral;
+  @LOC("IMG")
   private int width;
+  @LOC("IMG")
   private int hegith;
 
   // private Dimension dimension;
@@ -34,27 +39,6 @@ public class IntegralImageData {
     this.integral = new long[bufferedImage.getWidth()][bufferedImage.getHeight()];
     this.width = bufferedImage.getWidth();
     this.hegith = bufferedImage.getHeight();
-    // this.dimension = new Dimension(bufferedImage.getWidth(),
-    // bufferedImage.getHeight());
-
-    // int[] pixelBuffer = new int[bufferedImage.getWidth() *
-    // bufferedImage.getHeight()];
-    // PixelGrabber pg =
-    // new PixelGrabber(bufferedImage, 0, 0, bufferedImage.getWidth(),
-    // bufferedImage.getHeight(),
-    // pixelBuffer, 0, bufferedImage.getWidth());
-    //
-    // try {
-    // pg.grabPixels();
-    // } catch (InterruptedException ie) {
-    // }
-
-//    for (int y = 0; y < bufferedImage.getHeight(); ++y) {
-//      for (int x = 0; x < bufferedImage.getWidth(); ++x) {
-//        System.out.println("(" + x + "," + y + ")=" + (bufferedImage.getPixel(x, y)));
-//      }
-//    }
-//    System.exit(0);
 
     long[][] s = new long[bufferedImage.getWidth()][bufferedImage.getHeight()];
     for (int y = 0; y < bufferedImage.getHeight(); ++y) {
@@ -67,34 +51,7 @@ public class IntegralImageData {
 
   }
 
-  // public IntegralImageData(BufferedImage bufferedImage) {
-  // this.integral = new
-  // long[bufferedImage.getWidth()][bufferedImage.getHeight()];
-  // this.dimension = new Dimension(bufferedImage.getWidth(),
-  // bufferedImage.getHeight());
-  //
-  // int[] pixelBuffer = new
-  // int[bufferedImage.getWidth()*bufferedImage.getHeight()];
-  // PixelGrabber pg = new PixelGrabber(
-  // bufferedImage, 0, 0, bufferedImage.getWidth(), bufferedImage.getHeight(),
-  // pixelBuffer, 0, bufferedImage.getWidth());
-  //
-  // try {
-  // pg.grabPixels();
-  // } catch (InterruptedException ie) {}
-  //
-  // long[][] s = new long[bufferedImage.getWidth()][bufferedImage.getHeight()];
-  // for (int y = 0; y < bufferedImage.getHeight(); ++y) {
-  // for (int x = 0; x < bufferedImage.getWidth(); ++x) {
-  // s[x][y] = (y-1 < 0 ? 0 : s[x][y-1]) +
-  // (pixelBuffer[y*bufferedImage.getWidth() + x] & 0xff);
-  // this.integral[x][y] = (x-1 < 0 ? 0 : this.integral[x-1][y]) + s[x][y];
-  // }
-  // }
-  //
-  // }
-
-  public long getIntegralAt(int x, int y) {
+  public long getIntegralAt(@LOC("IN") int x, @LOC("IN") int y) {
     return this.integral[x][y];
   }
 
index 74bccd6..2ed85ef 100644 (file)
  * 
  * @author Florian Frankenberger
  */
+@LATTICE("LAST<DEV,DEV<POS,POS<IMPL")
+@METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
 public class LEA {
 
-  private boolean shutdown = false;
+  @LOC("IMPL")
   private LEAImplementation implementation;
-
+  @LOC("LAST")
   private FaceAndEyePosition lastPositions = new FaceAndEyePosition(null, null);
+  @LOC("DEV")
   private DeviationScanner deviationScanner = new DeviationScanner();
-  private int counter = 0;
 
   public LEA() {
     // this.imageProcessor = new
@@ -76,8 +78,8 @@ public class LEA {
   }
 
   /**
-   * To test LEA with the first capture device from the
-   * <code>Java Media Framework</code> just start from here.
+   * @METHOD To test LEA with the first capture device from the
+   *         <code>Java Media Framework</code> just start from here.
    * 
    * @param args
    * @throws Exception
@@ -87,15 +89,14 @@ public class LEA {
     lea.doRun();
   }
 
+  @LATTICE("THIS<IMG,IMG<C,C*,THISLOC=THIS")
   public void doRun() {
 
-    int maxCount = 37;
-    int i = 0;
-
-    ImageReader reader = new ImageReader();
+    @LOC("C") int maxCount = 37;
+    @LOC("C") int i = 0;
 
     SSJAVA: while (i < maxCount) {
-      Image image = reader.readImage("data/b" + i + ".bmp");
+      @LOC("IMG") Image image = ImageReader.readImage("data/b" + i + ".bmp");
       i++;
       if (image == null) {
         break;
@@ -107,13 +108,12 @@ public class LEA {
 
   }
 
-  private void processImage(Image image) {
-
-    FaceAndEyePosition positions = implementation.getEyePosition(image);
-
+  private void processImage(@LOC("IN") Image image) {
+    @LOC("THIS,LEA.POS") FaceAndEyePosition positions = implementation.getEyePosition(image);
     if (positions.getEyePosition() != null) {
       deviationScanner.addEyePosition(positions.getEyePosition());
-      int deviation = deviationScanner.scanForDeviation(positions.getFacePosition());// positions.getEyePosition().getDeviation(lastPositions.getEyePosition());
+      @LOC("THIS,LEA.DEV") int deviation =
+          deviationScanner.scanForDeviation(positions.getFacePosition());// positions.getEyePosition().getDeviation(lastPositions.getEyePosition());
       if (deviation != DeviationScanner.NONE) {
         System.out.println("deviation=" + deviationScanner.toStringDeviation(deviation));
         // notifyEyeMovementListenerEyeMoved(deviation);
index 141cb87..c60c3a8 100644 (file)
  * 
  * @author Florian Frankenberger
  */
+@LATTICE("R<CT")
+@METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
 public class LEAImplementation {
 
+  @LOC("CT")
   private ClassifierTree classifierTree;
 
+  @LOC("R")
   private Rectangle2D lastRectangle;
 
   public LEAImplementation() {
     this.loadFaceData();
   }
 
-  public FaceAndEyePosition getEyePosition(Image image) {
+  @LATTICE("OUT<V,V<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
+  public FaceAndEyePosition getEyePosition(@LOC("IN") Image image) {
     if (image == null)
       return null;
 
-    Rectangle2D faceRect = classifierTree.locateFaceRadial(image, lastRectangle);
-    EyePosition eyePosition = null;
+    @LOC("V") Rectangle2D faceRect = classifierTree.locateFaceRadial(image, lastRectangle);
+    @LOC("V") EyePosition eyePosition = null;
     if (faceRect != null) {
       lastRectangle = faceRect;
       faceRect = null;
-      Point point = readEyes(image, lastRectangle);
+      @LOC("V") Point point = readEyes(image, lastRectangle);
       if (point != null) {
         eyePosition = new EyePosition(point, lastRectangle);
       }
@@ -51,8 +56,8 @@ public class LEAImplementation {
     return new FaceAndEyePosition(lastRectangle, eyePosition);
   }
 
-  private Point readEyes(Image image, Rectangle2D rect) {
-    EyeDetector ed = new EyeDetector(image, rect);
+  private Point readEyes(@LOC("IN") Image image, @LOC("IN") Rectangle2D rect) {
+    @LOC("THIS") EyeDetector ed = new EyeDetector(image, rect);
     return ed.detectEye();
   }
 
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/LOC.java b/Robust/src/Benchmarks/SSJava/EyeTracking/LOC.java
new file mode 100644 (file)
index 0000000..0165516
--- /dev/null
@@ -0,0 +1,7 @@
+public @interface LOC {
+  String value();
+}
+
+public @interface RETURNLOC {
+  String value();
+}
\ No newline at end of file
index 2feea59..edc3f61 100644 (file)
@@ -1,7 +1,9 @@
+@LATTICE("POS")
+@METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
 public class Point {
 
-  public int x;
-  public int y;
+  @LOC("POS") public int x;
+  @LOC("POS") public int y;
 
   public Point(int x, int y) {
     this.x = x;
index ae53816..128a569 100644 (file)
@@ -1,9 +1,11 @@
+@LATTICE("POS")
+@METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
 public class Rectangle2D {
 
-  double x;
-  double y;
-  double width;
-  double height;
+  @LOC("POS") double x;
+  @LOC("POS") double y;
+  @LOC("POS") double width;
+  @LOC("POS") double height;
 
   public Rectangle2D(double x, double y, double w, double h) {
     this.x = x;
index a795596..3910944 100644 (file)
  * 
  * @author Florian
  */
+@LATTICE("POS")
+@METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
 public class ScanArea {
 
+  @LOC("POS")
   private Point fromPoint;
+  @LOC("POS")
   private Point toPoint;
+  @LOC("POS")
   private float size;
 
   /**
@@ -52,23 +57,23 @@ public class ScanArea {
     this(new Point(fromX, fromY), new Point(fromX + width, fromY + height));
   }
 
-  public int getFromX(float scaleFactor) {
+  public int getFromX(@LOC("IN") float scaleFactor) {
     return (int) (this.fromPoint.x * scaleFactor);
   }
 
-  public int getFromY(float scaleFactor) {
+  public int getFromY(@LOC("IN") float scaleFactor) {
     return (int) (this.fromPoint.y * scaleFactor);
   }
 
-  public int getToX(float scaleFactor) {
+  public int getToX(@LOC("IN") float scaleFactor) {
     return (int) (this.toPoint.x * scaleFactor);
   }
 
-  public int getToY(float scaleFactor) {
+  public int getToY(@LOC("IN") float scaleFactor) {
     return (int) (this.toPoint.y * scaleFactor);
   }
 
-  public int getSize(float scaleFactor) {
+  public int getSize(@LOC("IN") float scaleFactor) {
     return (int) (this.size * Math.pow(scaleFactor, 2));
   }
 
@@ -105,7 +110,7 @@ public class ScanArea {
   // }
 
   public String toString() {
-    String str = "";
+    @LOC("OUT") String str = "";
     str += "fromPoint=(" + fromPoint.x + "," + fromPoint.y + ")";
     str += "toPoint=(" + toPoint.x + "," + toPoint.y + ")";
     str += "size=" + size;
index 8af978a..4a5bdcf 100644 (file)
 
 //package java.lang;
 
-
 /**
  * Instances of class <code>Double</code> represent primitive
  * <code>double</code> 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)
  * @since 1.0
  * @status partly updated to 1.5
  */
-public final class Double extends Number //implements Comparable<Double>
+@LATTICE("V")
+@METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
+public final class Double extends Number // implements Comparable<Double>
 {
   /**
    * Compatible with JDK 1.0+.
    */
   /**
    * The immutable value of this Double.
-   *
+   * 
    * @serial the wrapped double
    */
+  @LOC("V")
   private final double value;
 
   /**
    * Create a <code>Double</code> from the primitive <code>double</code>
    * specified.
-   *
-   * @param value the <code>double</code> argument
+   * 
+   * @param value
+   *          the <code>double</code> argument
    */
   public Double(double value) {
     this.value = value;
   }
 
   /**
-   * Create a <code>Double</code> from the specified <code>String</code>.
-   * This method calls <code>Double.parseDouble()</code>.
-   *
-   * @param s the <code>String</code> to convert
-   * @throws NumberFormatException if <code>s</code> cannot be parsed as a
-   *         <code>double</code>
-   * @throws NullPointerException if <code>s</code> is null
+   * Create a <code>Double</code> from the specified <code>String</code>. This
+   * method calls <code>Double.parseDouble()</code>.
+   * 
+   * @param s
+   *          the <code>String</code> to convert
+   * @throws NumberFormatException
+   *           if <code>s</code> cannot be parsed as a <code>double</code>
+   * @throws NullPointerException
+   *           if <code>s</code> is null
    * @see #parseDouble(String)
    */
   public Double(String s) {
@@ -91,126 +96,120 @@ public final class Double extends Number //implements Comparable<Double>
   }
 
   /**
-   * Convert the <code>double</code> to a <code>String</code>.
-   * Floating-point string representation is fairly complex: here is a
-   * rundown of the possible values.  "<code>[-]</code>" indicates that a
-   * negative sign will be printed if the value (or exponent) is negative.
-   * "<code>&lt;number&gt;</code>" means a string of digits ('0' to '9').
-   * "<code>&lt;digit&gt;</code>" means a single digit ('0' to '9').<br>
-   *
+   * Convert the <code>double</code> to a <code>String</code>. Floating-point
+   * string representation is fairly complex: here is a rundown of the possible
+   * values. "<code>[-]</code>" indicates that a negative sign will be printed
+   * if the value (or exponent) is negative. "<code>&lt;number&gt;</code>" means
+   * a string of digits ('0' to '9'). "<code>&lt;digit&gt;</code>" means a
+   * single digit ('0' to '9').<br>
+   * 
    * <table border=1>
-   * <tr><th>Value of Double</th><th>String Representation</th></tr>
-   * <tr><td>[+-] 0</td> <td><code>[-]0.0</code></td></tr>
-   * <tr><td>Between [+-] 10<sup>-3</sup> and 10<sup>7</sup>, exclusive</td>
-   *     <td><code>[-]number.number</code></td></tr>
-   * <tr><td>Other numeric value</td>
-   *     <td><code>[-]&lt;digit&gt;.&lt;number&gt;
-   *          E[-]&lt;number&gt;</code></td></tr>
-   * <tr><td>[+-] infinity</td> <td><code>[-]Infinity</code></td></tr>
-   * <tr><td>NaN</td> <td><code>NaN</code></td></tr>
+   * <tr>
+   * <th>Value of Double</th>
+   * <th>String Representation</th>
+   * </tr>
+   * <tr>
+   * <td>[+-] 0</td>
+   * <td><code>[-]0.0</code></td>
+   * </tr>
+   * <tr>
+   * <td>Between [+-] 10<sup>-3</sup> and 10<sup>7</sup>, exclusive</td>
+   * <td><code>[-]number.number</code></td>
+   * </tr>
+   * <tr>
+   * <td>Other numeric value</td>
+   * <td><code>[-]&lt;digit&gt;.&lt;number&gt;
+   *          E[-]&lt;number&gt;</code></td>
+   * </tr>
+   * <tr>
+   * <td>[+-] infinity</td>
+   * <td><code>[-]Infinity</code></td>
+   * </tr>
+   * <tr>
+   * <td>NaN</td>
+   * <td><code>NaN</code></td>
+   * </tr>
    * </table>
-   *
-   * Yes, negative zero <em>is</em> a possible value.  Note that there is
-   * <em>always</em> a <code>.</code> and at least one digit printed after
-   * it: even if the number is 3, it will be printed as <code>3.0</code>.
-   * 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.
-   *
-   * <p>To create other output formats, use {@link java.text.NumberFormat}.
-   *
+   * 
+   * Yes, negative zero <em>is</em> a possible value. Note that there is
+   * <em>always</em> a <code>.</code> and at least one digit printed after it:
+   * even if the number is 3, it will be printed as <code>3.0</code>. 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.
+   * 
+   * <p>
+   * To create other output formats, use {@link java.text.NumberFormat}.
+   * 
    * @XXX specify where we are not in accord with the spec.
-   *
-   * @param d the <code>double</code> to convert
+   * 
+   * @param d
+   *          the <code>double</code> to convert
    * @return the <code>String</code> representing the <code>double</code>
    */
-  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:
    * <ul>
-   * <li> A NaN value is converted to the string "NaN".
-   * <li> Positive infinity is converted to the string "Infinity".
-   * <li> Negative infinity is converted to the string "-Infinity".
-   * <li> 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.
+   * <li>A NaN value is converted to the string "NaN".
+   * <li>Positive infinity is converted to the string "Infinity".
+   * <li>Negative infinity is converted to the string "-Infinity".
+   * <li>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.
    * </ul>
-   * @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 <code>Double</code> object wrapping the value.
-   * In contrast to the <code>Double</code> constructor, this method
-   * may cache some values.  It is used by boxing conversion.
-   *
-   * @param val the value to wrap
+   * Returns a <code>Double</code> object wrapping the value. In contrast to the
+   * <code>Double</code> constructor, this method may cache some values. It is
+   * used by boxing conversion.
+   * 
+   * @param val
+   *          the value to wrap
    * @return the <code>Double</code>
    * @since 1.5
    */
@@ -221,12 +220,14 @@ public final class Double extends Number //implements Comparable<Double>
 
   /**
    * Create a new <code>Double</code> object using the <code>String</code>.
-   *
-   * @param s the <code>String</code> to convert
+   * 
+   * @param s
+   *          the <code>String</code> to convert
    * @return the new <code>Double</code>
-   * @throws NumberFormatException if <code>s</code> cannot be parsed as a
-   *         <code>double</code>
-   * @throws NullPointerException if <code>s</code> is null.
+   * @throws NumberFormatException
+   *           if <code>s</code> cannot be parsed as a <code>double</code>
+   * @throws NullPointerException
+   *           if <code>s</code> is null.
    * @see #parseDouble(String)
    */
   public static Double valueOf(String s) {
@@ -236,6 +237,7 @@ public final class Double extends Number //implements Comparable<Double>
   /**
    * Parse the specified <code>String</code> as a <code>double</code>. The
    * extended BNF grammar is as follows:<br>
+   * 
    * <pre>
    * <em>DecodableString</em>:
    *      ( [ <code>-</code> | <code>+</code> ] <code>NaN</code> )
@@ -252,30 +254,35 @@ public final class Double extends Number //implements Comparable<Double>
    *              [ <code>-</code> | <code>+</code> ] { <em>Digit</em> }+ )
    * <em>Digit</em>: <em><code>'0'</code> through <code>'9'</code></em>
    * </pre>
-   *
-   * <p>NaN and infinity are special cases, to allow parsing of the output
-   * of toString.  Otherwise, the result is determined by calculating
-   * <em>n * 10<sup>exponent</sup></em> 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.
-   *
-   * <p>If an unexpected character is found in the <code>String</code>, a
-   * <code>NumberFormatException</code> will be thrown.  Leading and trailing
-   * 'whitespace' is ignored via <code>String.trim()</code>, but spaces
-   * internal to the actual number are not allowed.
-   *
-   * <p>To parse numbers according to another format, consider using
+   * 
+   * <p>
+   * NaN and infinity are special cases, to allow parsing of the output of
+   * toString. Otherwise, the result is determined by calculating
+   * <em>n * 10<sup>exponent</sup></em> 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.
+   * 
+   * <p>
+   * If an unexpected character is found in the <code>String</code>, a
+   * <code>NumberFormatException</code> will be thrown. Leading and trailing
+   * 'whitespace' is ignored via <code>String.trim()</code>, but spaces internal
+   * to the actual number are not allowed.
+   * 
+   * <p>
+   * 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 <code>String</code> to convert
+   * 
+   * @param str
+   *          the <code>String</code> to convert
    * @return the <code>double</code> value of <code>s</code>
-   * @throws NumberFormatException if <code>s</code> cannot be parsed as a
-   *         <code>double</code>
-   * @throws NullPointerException if <code>s</code> is null
+   * @throws NumberFormatException
+   *           if <code>s</code> cannot be parsed as a <code>double</code>
+   * @throws NullPointerException
+   *           if <code>s</code> is null
    * @see #MIN_VALUE
    * @see #MAX_VALUE
    * @see #POSITIVE_INFINITY
@@ -287,27 +294,30 @@ public final class Double extends Number //implements Comparable<Double>
   }
 
   public static native double nativeparsedouble(String str);
+
   public static native double nativeparsedouble(int start, int length, byte[] str);
 
   /**
-   * Return <code>true</code> if the <code>double</code> has the same
-   * value as <code>NaN</code>, otherwise return <code>false</code>.
-   *
-   * @param v the <code>double</code> to compare
+   * Return <code>true</code> if the <code>double</code> has the same value as
+   * <code>NaN</code>, otherwise return <code>false</code>.
+   * 
+   * @param v
+   *          the <code>double</code> to compare
    * @return whether the argument is <code>NaN</code>.
    */
-  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 <code>true</code> if the <code>double</code> has a value
-   * equal to either <code>NEGATIVE_INFINITY</code> or
-   * <code>POSITIVE_INFINITY</code>, otherwise return <code>false</code>.
-   *
-   * @param v the <code>double</code> to compare
+   * Return <code>true</code> if the <code>double</code> has a value equal to
+   * either <code>NEGATIVE_INFINITY</code> or <code>POSITIVE_INFINITY</code>,
+   * otherwise return <code>false</code>.
+   * 
+   * @param v
+   *          the <code>double</code> 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<Double>
   }
 
   /**
-   * Return <code>true</code> if the value of this <code>Double</code>
-   * is the same as <code>NaN</code>, otherwise return <code>false</code>.
-   *
+   * Return <code>true</code> if the value of this <code>Double</code> is the
+   * same as <code>NaN</code>, otherwise return <code>false</code>.
+   * 
    * @return whether this <code>Double</code> is <code>NaN</code>
    */
   public boolean isNaN() {
@@ -325,10 +335,10 @@ public final class Double extends Number //implements Comparable<Double>
   }
 
   /**
-   * Return <code>true</code> if the value of this <code>Double</code>
-   * is the same as <code>NEGATIVE_INFINITY</code> or
-   * <code>POSITIVE_INFINITY</code>, otherwise return <code>false</code>.
-   *
+   * Return <code>true</code> if the value of this <code>Double</code> is the
+   * same as <code>NEGATIVE_INFINITY</code> or <code>POSITIVE_INFINITY</code>,
+   * otherwise return <code>false</code>.
+   * 
    * @return whether this <code>Double</code> is (-/+) infinity
    */
   public boolean isInfinite() {
@@ -336,10 +346,10 @@ public final class Double extends Number //implements Comparable<Double>
   }
 
   /**
-   * Convert the <code>double</code> value of this <code>Double</code>
-   * to a <code>String</code>.  This method calls
-   * <code>Double.toString(double)</code> to do its dirty work.
-   *
+   * Convert the <code>double</code> value of this <code>Double</code> to a
+   * <code>String</code>. This method calls <code>Double.toString(double)</code>
+   * to do its dirty work.
+   * 
    * @return the <code>String</code> representation
    * @see #toString(double)
    */
@@ -349,7 +359,7 @@ public final class Double extends Number //implements Comparable<Double>
 
   /**
    * Return the value of this <code>Double</code> as a <code>byte</code>.
-   *
+   * 
    * @return the byte value
    * @since 1.1
    */
@@ -359,7 +369,7 @@ public final class Double extends Number //implements Comparable<Double>
 
   /**
    * Return the value of this <code>Double</code> as a <code>short</code>.
-   *
+   * 
    * @return the short value
    * @since 1.1
    */
@@ -369,7 +379,7 @@ public final class Double extends Number //implements Comparable<Double>
 
   /**
    * Return the value of this <code>Double</code> as an <code>int</code>.
-   *
+   * 
    * @return the int value
    */
   public int intValue() {
@@ -378,7 +388,7 @@ public final class Double extends Number //implements Comparable<Double>
 
   /**
    * Return the value of this <code>Double</code> as a <code>long</code>.
-   *
+   * 
    * @return the long value
    */
   public long longValue() {
@@ -387,7 +397,7 @@ public final class Double extends Number //implements Comparable<Double>
 
   /**
    * Return the value of this <code>Double</code> as a <code>float</code>.
-   *
+   * 
    * @return the float value
    */
   public float floatValue() {
@@ -396,7 +406,7 @@ public final class Double extends Number //implements Comparable<Double>
 
   /**
    * Return the value of this <code>Double</code>.
-   *
+   * 
    * @return the double value
    */
   public double doubleValue() {
@@ -404,16 +414,16 @@ public final class Double extends Number //implements Comparable<Double>
   }
 
   /**
-   * Return a hashcode representing this Object. <code>Double</code>'s hash
-   * code is calculated by:<br>
+   * Return a hashcode representing this Object. <code>Double</code>'s hash code
+   * is calculated by:<br>
    * <code>long v = Double.doubleToLongBits(doubleValue());<br>
    *    int hash = (int)(v^(v&gt;&gt;32))</code>.
-   *
+   * 
    * @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<Double>
    * two doubles with <code>==</code>, this treats two instances of
    * <code>Double.NaN</code> as equal, but treats <code>0.0</code> and
    * <code>-0.0</code> as unequal.
-   *
-   * <p>Note that <code>d1.equals(d2)</code> is identical to
+   * 
+   * <p>
+   * Note that <code>d1.equals(d2)</code> is identical to
    * <code>doubleToLongBits(d1.doubleValue()) ==
    *    doubleToLongBits(d2.doubleValue())</code>.
-   *
-   * @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<Double>
 
   /**
    * 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
-   * <code>Double.longBitsToDouble(long)</code> to obtain the original
-   * <code>double</code> value.
-   *
-   * @param value the <code>double</code> 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 <code>Double.longBitsToDouble(long)</code> to obtain the
+   * original <code>double</code> value.
+   * 
+   * @param value
+   *          the <code>double</code> to convert
    * @return the bits of the <code>double</code>
    * @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
-   * <code>Double.longBitsToDouble(long)</code> to obtain the original
-   * <code>double</code> value.
-   *
-   * @param value the <code>double</code> 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 <code>Double.longBitsToDouble(long)</code>
+   * to obtain the original <code>double</code> value.
+   * 
+   * @param value
+   *          the <code>double</code> to convert
    * @return the bits of the <code>double</code>
    * @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 <code>Double.doubleToRawLongBits(double)</code>.
-   *
-   * @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
+   * <code>Double.doubleToRawLongBits(double)</code>.
+   * 
+   * @param bits
+   *          the bits to convert
    * @return the <code>double</code> 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 <code>double</code>
    * 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 <code>POSITIVE_INFINITY</code>, 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 <code>POSITIVE_INFINITY</code>, 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<Double>
   }
 
   /**
-   * Behaves like <code>new Double(x).compareTo(new Double(y))</code>; 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 <code>new Double(x).compareTo(new Double(y))</code>; 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<Double>
 
     // 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;
   }
 }
index b6f4a13..85596dc 100644 (file)
@@ -1,5 +1,5 @@
 @LATTICE("B<T")
-@METHODDEFAULT("OUT<IN,THISLOC=IN")
+@METHODDEFAULT("OUT<IN,THISLOC=IN,RETURNLOC=OUT")
 public class Math {
   @LOC("T")
   static final double PI = 3.14159265358979323846;
@@ -10,7 +10,7 @@ public class Math {
     return PI;
   }
 
-  public static int abs(int x) {
+  public static int abs(@LOC("IN") int x) {
     return (x < 0) ? -x : x;
   }
 
@@ -22,7 +22,7 @@ public class Math {
     return (x < 0) ? -x : x;
   }
 
-  public static float abs(float x) {
+  public static float abs(@LOC("IN") float x) {
     return (x < 0) ? -x : x;
   }
 
@@ -30,11 +30,11 @@ public class Math {
     return (a > 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);
   }
index 5f96339..35c1505 100644 (file)
@@ -295,7 +295,7 @@ public class String {
     return this;
   }
 
-  @LATTICE("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
+  @LATTICE("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT,GLOBALLOC=THIS")
   public static String valueOf(@LOC("THIS") Object o) {
     if (o == null)
       return "null";
@@ -303,7 +303,7 @@ public class String {
       return o.toString();
   }
 
-  public static String valueOf(boolean b) {
+  public static String valueOf(@LOC("IN") boolean b) {
     if (b)
       return new String("true");
     else
@@ -350,9 +350,9 @@ public class String {
     return new String(chararray);
   }
 
-  public static String valueOf(double val) {
-    char[] chararray = new char[20];
-    String s = new String();
+  public static String valueOf(@LOC("IN") double val) {
+    @LOC("C") char[] chararray = new char[20];
+    @LOC("V")  String s = new String();
     s.offset = 0;
     s.count = convertdoubletochar(val, chararray);
     s.value = chararray;