From 890c448e14fd7e016be47cb82859402b4211b013 Mon Sep 17 00:00:00 2001
From: yeom <yeom>
Date: Tue, 20 Sep 2011 21:11:08 +0000
Subject: [PATCH] passes the flow down rule

---
 Robust/src/Analysis/SSJava/FlowDownCheck.java | 50 +++++++++----------
 .../SSJava/EyeTracking/Classifier.java        |  6 +--
 .../SSJava/EyeTracking/ClassifierTree.java    | 39 ++++++++-------
 .../SSJava/EyeTracking/DeviationScanner.java  | 43 +++++++++-------
 .../SSJava/EyeTracking/EyeDetector.java       |  9 ++--
 .../Benchmarks/SSJava/EyeTracking/LEA.java    |  2 +-
 .../SSJava/EyeTracking/LEAImplementation.java | 10 ++--
 Robust/src/ClassLibrary/SSJava/Math.java      |  4 +-
 Robust/src/ClassLibrary/SSJava/Object.java    |  1 +
 Robust/src/ClassLibrary/SSJava/SSJAVA.java    | 13 ++++-
 10 files changed, 98 insertions(+), 79 deletions(-)

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 76a9d7fa..78d82df1 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -544,15 +544,20 @@ public class FlowDownCheck {
           checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation(),
               constraint, false);
 
+      // System.out.println("# RETURN VALUE LOC=" + returnValueLoc +
+      // " with constraint=" + constraint);
+
+      // TODO: do we need to check here?
       // if this return statement is inside branch, return value has an implicit
       // flow from conditional location
-      if (constraint != null) {
-        Set<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
-        inputGLB.add(returnValueLoc);
-        inputGLB.add(constraint);
-        returnValueLoc =
-            CompositeLattice.calculateGLB(inputGLB, generateErrorMessage(md.getClassDesc(), rn));
-      }
+      // if (constraint != null) {
+      // Set<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
+      // inputGLB.add(returnValueLoc);
+      // inputGLB.add(constraint);
+      // returnValueLoc =
+      // CompositeLattice.calculateGLB(inputGLB,
+      // generateErrorMessage(md.getClassDesc(), rn));
+      // }
 
       // check if return value is equal or higher than RETRUNLOC of method
       // declaration annotation
@@ -841,9 +846,12 @@ 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);
+    // 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()
@@ -896,7 +904,6 @@ 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) {
@@ -908,11 +915,11 @@ public class FlowDownCheck {
           String thisLocId = ssjava.getMethodLattice(md).getThisLoc();
           baseLocation = new CompositeLocation(new Location(md, thisLocId));
         }
-
       }
 
-      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 =
@@ -1141,11 +1148,11 @@ public class FlowDownCheck {
             int callerResult =
                 CompositeLattice.compare(callerLoc1, callerLoc2, true,
                     generateErrorMessage(md.getClassDesc(), min));
-            System.out.println("callerResult=" + callerResult);
+            // System.out.println("callerResult=" + callerResult);
             int calleeResult =
                 CompositeLattice.compare(calleeLoc1, calleeLoc2, true,
                     generateErrorMessage(md.getClassDesc(), min));
-            System.out.println("calleeResult=" + calleeResult);
+            // System.out.println("calleeResult=" + calleeResult);
 
             if (callerResult == ComparisonResult.EQUAL) {
               if (ssjava.isSharedLocation(callerLoc1.get(callerLoc1.getSize() - 1))
@@ -1156,15 +1163,6 @@ public class FlowDownCheck {
               }
             }
 
-            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) {
               // If calleeLoc1 is higher than calleeLoc2
@@ -1821,7 +1819,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 53e26e23..87ada5b5 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java
@@ -76,8 +76,8 @@ public class Classifier {
    */
   @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("THIS,Classifier.C") float scaleFactor, @LOC("THIS,Classifier.C") int translationX,
+      @LOC("THIS,Classifier.C") int translationY, @LOC("THIS,Classifier.C") float borderline) {
 
     @LOC("THIS,Classifier.V") long values[] = new long[scanAreas.length];
 
@@ -163,7 +163,7 @@ public class Classifier {
   public String toString() {
 
     @LOC("OUT") String str = "";
-    for (@LOC("THIS,Classifier.C") int i = 0; i < scanAreas.length; i++) {
+    for (@LOC("C") int i = 0; i < scanAreas.length; i++) {
       str += scanAreas[i].toString() + "\n";
     }
 
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/ClassifierTree.java b/Robust/src/Benchmarks/SSJava/EyeTracking/ClassifierTree.java
index 54e19f70..d63e3dc6 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/ClassifierTree.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/ClassifierTree.java
@@ -21,11 +21,11 @@
  * 
  * @author Florian
  */
-@LATTICE("C")
+@LATTICE("CS<C,C*")
 @METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
 public class ClassifierTree {
 
-  @LOC("C")
+  @LOC("CS")
   private Classifier classifiers[];
 
   public ClassifierTree(int size) {
@@ -50,16 +50,16 @@ public class ClassifierTree {
    * @return an rectangle representing the actual face position on success or
    *         null if no face could be detected
    */
-  @LATTICE("OUT,THIS<CXY,CXY<V,V<IMG,IMG<C,C<IN,C*,FACTOR*,CXY*,THISLOC=THIS,RETURNLOC=OUT")
+  @LATTICE("OUT<CXY,CXY<THIS,THIS<V,V<IMG,IMG<C,C<IN,C*,V*,FACTOR*,CXY*,THISLOC=THIS,RETURNLOC=OUT,GLOBALLOC=IN")
   public Rectangle2D locateFaceRadial(@LOC("IN") Image smallImage,
-      @LOC("C") Rectangle2D lastCoordinates) {
+      @LOC("THIS,ClassifierTree.C") Rectangle2D lastCoordinates) {
 
     @LOC("IMG") IntegralImageData imageData = new IntegralImageData(smallImage);
     @LOC("IN") float originalImageFactor = 1;
 
     if (lastCoordinates == null) {
       // if we don't have a last coordinate we just begin in the center
-      @LOC("C") int smallImageMaxDimension =
+      @LOC("THIS,ClassifierTree.C") int smallImageMaxDimension =
           Math.min(smallImage.getWidth(), smallImage.getHeight());
       lastCoordinates =
           new Rectangle2D((smallImage.getWidth() - smallImageMaxDimension) / 2.0,
@@ -76,43 +76,43 @@ public class ClassifierTree {
               (lastCoordinates.getHeight() * (1 / originalImageFactor)));
     }
 
-    @LOC("V") float startFactor = (float) (lastCoordinates.getWidth() / 100.0f);
+    @LOC("THIS,ClassifierTree.C") float startFactor = (float) (lastCoordinates.getWidth() / 100.0f);
 
     // first we calculate the maximum scale factor for our 200x200 image
-    @LOC("V") float maxScaleFactor =
+    @LOC("THIS,ClassifierTree.C") float maxScaleFactor =
         Math.min(imageData.getWidth() / 100f, imageData.getHeight() / 100f);
     // maxScaleFactor = 1.0f;
 
     // we simply won't recognize faces that are smaller than 40x40 px
-    @LOC("V") float minScaleFactor = 0.5f;
+    @LOC("THIS,ClassifierTree.C") float minScaleFactor = 0.5f;
 
-    @LOC("V") float maxScaleDifference =
+    @LOC("THIS,ClassifierTree.C") float maxScaleDifference =
         Math.max(Math.abs(maxScaleFactor - startFactor), Math.abs(minScaleFactor - startFactor));
 
     // border for faceYes-possibility must be greater that that
-    @LOC("V") float maxBorder = 0.999f;
+    @LOC("THIS,ClassifierTree.C") float maxBorder = 0.999f;
 
-    @LOC("V") int startPosX = (int) lastCoordinates.getX();
-    @LOC("V") int startPosY = (int) lastCoordinates.getX();
+    @LOC("THIS,ClassifierTree.C") int startPosX = (int) lastCoordinates.getX();
+    @LOC("THIS,ClassifierTree.C") int startPosY = (int) lastCoordinates.getX();
 
-    for (@LOC("C") float factorDiff = 0.0f; Math.abs(factorDiff) <= maxScaleDifference; factorDiff =
+    for (@LOC("THIS,ClassifierTree.C") float factorDiff = 0.0f; Math.abs(factorDiff) <= maxScaleDifference; factorDiff =
         (factorDiff + sgn(factorDiff) * 0.1f) * -1 // we alternate between
                                                    // negative and positiv
                                                    // factors
     ) {
 
-      @LOC("V") float factor = startFactor + factorDiff;
+      @LOC("THIS,ClassifierTree.C") float factor = startFactor + factorDiff;
       // System.out.println("factor=" + factor);
       if (factor > maxScaleFactor || factor < minScaleFactor)
         continue;
 
       // now we calculate the actualDimmension
-      @LOC("V") int actualDimmension = (int) (100 * factor);
-      @LOC("V") int maxX = imageData.getWidth() - actualDimmension;
-      @LOC("V") int maxY = imageData.getHeight() - actualDimmension;
+      @LOC("THIS,ClassifierTree.C") int actualDimmension = (int) (100 * factor);
+      @LOC("THIS,ClassifierTree.C") int maxX = imageData.getWidth() - actualDimmension;
+      @LOC("THIS,ClassifierTree.C") int maxY = imageData.getHeight() - actualDimmension;
 
-      @LOC("V") int maxDiffX = Math.max(Math.abs(startPosX - maxX), startPosX);
-      @LOC("V") int maxDiffY = Math.max(Math.abs(startPosY - maxY), startPosY);
+      @LOC("THIS,ClassifierTree.C") int maxDiffX = Math.max(Math.abs(startPosX - maxX), startPosX);
+      @LOC("THIS,ClassifierTree.C") int maxDiffY = Math.max(Math.abs(startPosY - maxY), startPosY);
 
       for (@LOC("CXY") float xDiff = 0.1f; Math.abs(xDiff) <= maxDiffX; xDiff =
           (xDiff + sgn(xDiff) * 0.5f) * -1) {
@@ -164,6 +164,7 @@ public class ClassifierTree {
 
   }
 
+  @LATTICE("OUT<IN,OUT<THIS,THISLOC=THIS,RETURNLOC=OUT")
   private static int sgn(@LOC("IN") float value) {
     return (value < 0 ? -1 : (value > 0 ? +1 : 1));
   }
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/DeviationScanner.java b/Robust/src/Benchmarks/SSJava/EyeTracking/DeviationScanner.java
index b5308f50..052c7f4b 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/DeviationScanner.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/DeviationScanner.java
@@ -22,11 +22,11 @@
  * 
  * @author Florian Frankenberger
  */
-@LATTICE("SIZE<POS,SIZE*")
+@LATTICE("DEV<C,C<SIZE,SIZE*,C*,DEV*")
 @METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
 public class DeviationScanner {
 
-  @LOC("POS")
+  @LOC("DEV")
   private EyePosition eyePositions[];
 
   // LEFT_UP(+1, -1), UP(0, -1), RIGHT_UP(-1, -1), LEFT(+1, 0), NONE(0, 0),
@@ -43,7 +43,7 @@ public class DeviationScanner {
   public static final int DOWN = 7;
   public static final int RIGHT_DOWN = 8;
 
-  @LOC("SIZE")
+  @LOC("DEV")
   private int size;
 
   public DeviationScanner() {
@@ -54,30 +54,36 @@ public class DeviationScanner {
   @LATTICE("THIS<C,C<IN,THISLOC=THIS")
   public void addEyePosition(@LOC("IN") EyePosition eyePosition) {
 
-    for (@LOC("C") int i = 1; i < eyePositions.length; i++) {
-      eyePositions[i - 1] = eyePositions[i];
-      eyePositions[i] = null;
-    }
-    eyePositions[eyePositions.length - 1] = eyePosition;
+    // for (@LOC("THIS,DeviationScanner.C") int i = 1; i < 3; i++) {
+    // eyePositions[i - 1] = eyePositions[i];
+    // eyePositions[i] = null;
+    // }
+    // eyePositions[eyePositions.length - 1] = eyePosition;
+
+    SSJAVA.append(eyePositions, eyePosition);
 
     if (size < eyePositions.length) {
       size++;
     }
+
   }
 
+  @RETURNLOC("THIS,DeviationScanner.DEV")
   public int getEyePositionsSize() {
     return size;
   }
 
-  @LATTICE("OUT<DEV,DEV<THIS,THIS<C,C<IN,C*,DEV*,OUT*,THISLOC=THIS,RETURNLOC=OUT")
+  // @LATTICE("OUT<DEV,DEV<C,C<THIS,THIS<IN,C*,DEV*,OUT*,THISLOC=THIS,RETURNLOC=OUT")
+  @LATTICE("THIS<IN,THISLOC=THIS")
+  @RETURNLOC("THIS,DeviationScanner.DEV")
   public int scanForDeviation(@LOC("IN") Rectangle2D faceRect) {
-    @LOC("OUT") int deviation = NONE;
+    @LOC("THIS,DeviationScanner.DEV") int deviation = NONE;
     if (getEyePositionsSize() >= 3) {
-      @LOC("DEV") double deviationX = 0;
-      @LOC("DEV") double deviationY = 0;
+      @LOC("THIS,DeviationScanner.DEV") double deviationX = 0;
+      @LOC("THIS,DeviationScanner.DEV") double deviationY = 0;
 
-      @LOC("DEV") int lastIdx = -1;
-      for (@LOC("C") int i = 0; i < 3; ++i) {
+      @LOC("THIS,DeviationScanner.DEV") int lastIdx = -1;
+      for (@LOC("THIS,DeviationScanner.DEV") int i = 0; i < 3; ++i) {
         if (lastIdx != -1) {
           deviationX += (eyePositions[i].getX() - eyePositions[lastIdx].getX());
           deviationY += (eyePositions[i].getY() - eyePositions[lastIdx].getY());
@@ -85,14 +91,14 @@ public class DeviationScanner {
         lastIdx = i;
       }
 
-      @LOC("DEV") final double deviationPercentX = 0.04;
-      @LOC("DEV") final double deviationPercentY = 0.04;
+      @LOC("THIS,DeviationScanner.DEV") final double deviationPercentX = 0.04;
+      @LOC("THIS,DeviationScanner.DEV") final double deviationPercentY = 0.04;
 
       deviationX /= faceRect.getWidth();
       deviationY /= faceRect.getWidth();
 
-      @LOC("DEV") int deviationAbsoluteX = 0;
-      @LOC("DEV") int deviationAbsoluteY = 0;
+      @LOC("THIS,DeviationScanner.DEV") int deviationAbsoluteX = 0;
+      @LOC("THIS,DeviationScanner.DEV") int deviationAbsoluteY = 0;
       if (deviationX > deviationPercentX)
         deviationAbsoluteX = 1;
       if (deviationX < -deviationPercentX)
@@ -117,6 +123,7 @@ public class DeviationScanner {
     return deviation;
   }
 
+  @LATTICE("OUT<IN,OUT<THIS,THISLOC=THIS,RETURNLOC=OUT")
   public int getDirectionFor(@LOC("IN") int directionX, @LOC("IN") int directionY) {
 
     if (directionX == +1 && directionY == -1) {
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/EyeDetector.java b/Robust/src/Benchmarks/SSJava/EyeTracking/EyeDetector.java
index e6bbd029..88620a48 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/EyeDetector.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/EyeDetector.java
@@ -23,7 +23,7 @@
  * @author Florian Frankenberger
  */
 @LATTICE("IMG")
-@METHODDEFAULT("OUT<THIS,THIS<IN,OUT*,THISLOC=THIS,RETURNLOC=OUT")
+@METHODDEFAULT("OUT<THIS,THIS<IN,OUT*,THISLOC=THIS,RETURNLOC=OUT,GLOBALLOC=THIS")
 class EyeDetector {
 
   @LOC("IMG")
@@ -57,7 +57,7 @@ class EyeDetector {
 
   }
 
-  @LATTICE("OUT,V<THIS,THIS<C,C*,THISLOC=THIS,RETURNLOC=OUT")
+  @LATTICE("OUT<V,V<C,C<THIS,C*,V*,THISLOC=THIS,RETURNLOC=OUT,GLOBALLOC=THIS")
   public Point detectEye() {
     @LOC("OUT") Point eyePosition = null;
     @LOC("V") float brightness = 255f;
@@ -80,9 +80,10 @@ class EyeDetector {
     return eyePosition;
   }
 
+  @LATTICE("OUT<V,V<G,G<IN,G<THIS,THISLOC=THIS,GLOBALLOC=G,RETURNLOC=OUT")
   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]);
+    @LOC("V") int min = Math.min(Math.min(color[0], color[1]), color[2]);
+    @LOC("V") 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/LEA.java b/Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java
index 2ed85ef3..587a59f9 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java
@@ -112,7 +112,7 @@ public class LEA {
     @LOC("THIS,LEA.POS") FaceAndEyePosition positions = implementation.getEyePosition(image);
     if (positions.getEyePosition() != null) {
       deviationScanner.addEyePosition(positions.getEyePosition());
-      @LOC("THIS,LEA.DEV") int deviation =
+      @LOC("THIS,LEA.DEV,DeviationScanner.DEV") int deviation =
           deviationScanner.scanForDeviation(positions.getFacePosition());// positions.getEyePosition().getDeviation(lastPositions.getEyePosition());
       if (deviation != DeviationScanner.NONE) {
         System.out.println("deviation=" + deviationScanner.toStringDeviation(deviation));
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java b/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java
index c60c3a8e..bbdf2ba6 100644
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java
@@ -22,7 +22,7 @@
  * 
  * @author Florian Frankenberger
  */
-@LATTICE("R<CT")
+@LATTICE("R<CT,R*")
 @METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
 public class LEAImplementation {
 
@@ -36,12 +36,13 @@ public class LEAImplementation {
     this.loadFaceData();
   }
 
-  @LATTICE("OUT<V,V<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
+  @LATTICE("OUT<V,V<THIS,THIS<IN,V*,THISLOC=THIS,RETURNLOC=OUT")
   public FaceAndEyePosition getEyePosition(@LOC("IN") Image image) {
     if (image == null)
       return null;
 
-    @LOC("V") Rectangle2D faceRect = classifierTree.locateFaceRadial(image, lastRectangle);
+    @LOC("THIS,LEAImplementation.R") Rectangle2D faceRect =
+        classifierTree.locateFaceRadial(image, lastRectangle);
     @LOC("V") EyePosition eyePosition = null;
     if (faceRect != null) {
       lastRectangle = faceRect;
@@ -56,8 +57,9 @@ public class LEAImplementation {
     return new FaceAndEyePosition(lastRectangle, eyePosition);
   }
 
+  @LATTICE("OUT<IN,OUT<THIS,THISLOC=THIS,RETURNLOC=OUT")
   private Point readEyes(@LOC("IN") Image image, @LOC("IN") Rectangle2D rect) {
-    @LOC("THIS") EyeDetector ed = new EyeDetector(image, rect);
+    @LOC("OUT") EyeDetector ed = new EyeDetector(image, rect);
     return ed.detectEye();
   }
 
diff --git a/Robust/src/ClassLibrary/SSJava/Math.java b/Robust/src/ClassLibrary/SSJava/Math.java
index 85596dc0..3cb7eb10 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,RETURNLOC=OUT")
+@METHODDEFAULT("OUT<IN,OUT<THIS,,IN*,THISLOC=THIS,RETURNLOC=OUT")
 public class Math {
   @LOC("T")
   static final double PI = 3.14159265358979323846;
@@ -52,7 +52,7 @@ public class Math {
     return (a < b) ? a : b;
   }
 
-  @RETURNLOC("IN")
+  @RETURNLOC("OUT")
   public static int min(@LOC("IN") int a, @LOC("IN") int b) {
     return (a < b) ? a : b;
   }
diff --git a/Robust/src/ClassLibrary/SSJava/Object.java b/Robust/src/ClassLibrary/SSJava/Object.java
index 8e128c52..f399e89a 100644
--- a/Robust/src/ClassLibrary/SSJava/Object.java
+++ b/Robust/src/ClassLibrary/SSJava/Object.java
@@ -17,6 +17,7 @@ public class Object {
     return false;
   }
 
+  @TRUST
   @RETURNLOC("TH")
   public String toString() {
     return "Object" + hashCode();
diff --git a/Robust/src/ClassLibrary/SSJava/SSJAVA.java b/Robust/src/ClassLibrary/SSJava/SSJAVA.java
index ebb3e41a..8e49e948 100644
--- a/Robust/src/ClassLibrary/SSJava/SSJAVA.java
+++ b/Robust/src/ClassLibrary/SSJava/SSJAVA.java
@@ -1,3 +1,5 @@
+import Benchmarks.SSJava.EyeTracking.LOC;
+
 public class SSJAVA {
 
   // Definitely written analysis assumes that the first parameter may have write
@@ -31,7 +33,7 @@ public class SSJAVA {
       }
     }
   }
-  
+
   static void arrayinit(float array[][], int size_1, int size_2, float value) {
 
     for (int idx1 = 0; idx1 < size_1; idx1++) {
@@ -43,7 +45,6 @@ public class SSJAVA {
       }
     }
   }
-  
 
   static void arraycopy(float array[][], float src[][], int size_1, int size_2) {
 
@@ -57,4 +58,12 @@ public class SSJAVA {
     }
   }
 
+  static void append(Object array[], Object item) {
+    for (int i = 1; i < array.length; i++) {
+      array[i - 1] = array[i];
+      array[i]=null;
+    }
+    array[array.length - 1] = item;
+  }
+
 }
-- 
2.34.1