From: yeom <yeom>
Date: Tue, 20 Sep 2011 01:41:12 +0000 (+0000)
Subject: bug fixes + annotations
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1b1cd580d16bc4f8b514ce9ff8b88f2b7072c0d7;p=IRC.git
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<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";
}
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<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);
}
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 <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;
+ }
}
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("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) {
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/Image.java b/Robust/src/Benchmarks/SSJava/EyeTracking/Image.java
index 5e83b461..e7c2e825 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/Image.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/Image.java
@@ -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) {
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/ImageReader.java b/Robust/src/Benchmarks/SSJava/EyeTracking/ImageReader.java
index 461971dd..d89c14cd 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/ImageReader.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/ImageReader.java
@@ -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
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/IntegralImageData.java b/Robust/src/Benchmarks/SSJava/EyeTracking/IntegralImageData.java
index 8cc3cbaf..d74880ba 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/IntegralImageData.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/IntegralImageData.java
@@ -22,10 +22,15 @@
*
* @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];
}
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java b/Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java
index 74bccd64..2ed85ef3 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java
@@ -50,14 +50,16 @@
*
* @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);
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java b/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java
index 141cb872..c60c3a8e 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java
@@ -22,26 +22,31 @@
*
* @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
index 00000000..0165516c
--- /dev/null
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/LOC.java
@@ -0,0 +1,7 @@
+public @interface LOC {
+ String value();
+}
+
+public @interface RETURNLOC {
+ String value();
+}
\ No newline at end of file
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/Point.java b/Robust/src/Benchmarks/SSJava/EyeTracking/Point.java
index 2feea59d..edc3f61f 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/Point.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/Point.java
@@ -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;
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/Rectangle2D.java b/Robust/src/Benchmarks/SSJava/EyeTracking/Rectangle2D.java
index ae538162..128a569a 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/Rectangle2D.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/Rectangle2D.java
@@ -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;
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/ScanArea.java b/Robust/src/Benchmarks/SSJava/EyeTracking/ScanArea.java
index a7955960..39109448 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/ScanArea.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/ScanArea.java
@@ -21,10 +21,15 @@
*
* @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;
diff --git a/Robust/src/ClassLibrary/SSJava/Double.java b/Robust/src/ClassLibrary/SSJava/Double.java
index 8af978ab..4a5bdcff 100644
--- a/Robust/src/ClassLibrary/SSJava/Double.java
+++ b/Robust/src/ClassLibrary/SSJava/Double.java
@@ -38,14 +38,13 @@
//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)
@@ -54,36 +53,42 @@
* @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><number></code>" means a string of digits ('0' to '9').
- * "<code><digit></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><number></code>" means
+ * a string of digits ('0' to '9'). "<code><digit></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>[-]<digit>.<number>
- * E[-]<number></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>[-]<digit>.<number>
+ * E[-]<number></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>>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;
}
}
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<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);
}
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<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;