changes.

diff --git a/Robust/src/Analysis/SSJava/CompositeLocation.java b/Robust/src/Analysis/SSJava/CompositeLocation.java
index 8f396a57f541bea282413e63bc974b7f85c699bb..7baf552d868a7cc490d87fb454730f591353c715 100644 (file)
--- a/Robust/src/Analysis/SSJava/CompositeLocation.java
+++ b/Robust/src/Analysis/SSJava/CompositeLocation.java
@@ -74,4 +74,10 @@ public class CompositeLocation implements TypeExtension {
 
   }
 
+  public CompositeLocation clone() {
+    CompositeLocation clone = new CompositeLocation();
+    clone.getTuple().addAll(locTuple);
+    return clone;
+  }
+
 }

diff --git a/Robust/src/Analysis/SSJava/DeltaLocation.java b/Robust/src/Analysis/SSJava/DeltaLocation.java
index 13f1a6cba8bd8ba83c360e104f29cdd8aedd9496..d4795153db489e7999a838feb120f86568fafc3d 100644 (file)
--- a/Robust/src/Analysis/SSJava/DeltaLocation.java
+++ b/Robust/src/Analysis/SSJava/DeltaLocation.java
@@ -4,15 +4,24 @@ public class DeltaLocation extends CompositeLocation {
 
   private int numDelta;
 
+  public DeltaLocation() {
+    super();
+  }
+
   public DeltaLocation(CompositeLocation comp, int numDelta) {
+    super();
     this.numDelta = numDelta;
-    this.locTuple = comp.getTuple();
+    this.locTuple.addAll(comp.getTuple());
   }
 
   public int getNumDelta() {
     return numDelta;
   }
 
+  public void setNumDelta(int d) {
+    numDelta = d;
+  }
+
   public String toString() {
 
     String rtr = "";
@@ -36,4 +45,11 @@ public class DeltaLocation extends CompositeLocation {
     return rtr;
   }
 
+  public CompositeLocation clone() {
+    DeltaLocation clone = new DeltaLocation();
+    clone.getTuple().addAll(locTuple);
+    clone.setNumDelta(numDelta);
+    return clone;
+  }
+
 }

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 3edbd818ce63d00d942e194ea5b0396d52d32712..65240aa1dffc2879ce329c2f959c27385d0a4f90 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -799,7 +799,7 @@ public class FlowDownCheck {
         VarDescriptor vd = (VarDescriptor) d;
         // localLoc = d2loc.get(vd);
         // the type of var descriptor has a composite location!
-        loc = (CompositeLocation) vd.getType().getExtension();
+        loc = ((CompositeLocation) vd.getType().getExtension()).clone();
       } else if (d instanceof FieldDescriptor) {
         // the type of field descriptor has a location!
         FieldDescriptor fd = (FieldDescriptor) d;
@@ -813,7 +813,6 @@ public class FlowDownCheck {
         loc.addLocation(fieldLoc);
       }
     }
-
     return loc;
   }
 
@@ -851,9 +850,8 @@ public class FlowDownCheck {
     if (!postinc) {
       srcLocation = new CompositeLocation();
       srcLocation = checkLocationFromExpressionNode(md, nametable, an.getSrc(), srcLocation);
-      // System.out.println("an=" + an.printNode(0) + " an.getSrc()=" +
-      // an.getSrc().getClass()
-      // + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
+//      System.out.println("an=" + an.printNode(0) + " an.getSrc()=" + an.getSrc().getClass()
+//          + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation)) {
         throw new Error("The value flow from " + srcLocation + " to " + destLocation
             + " does not respect location hierarchy on the assignment " + an.printNode(0) + " at "
@@ -1054,6 +1052,8 @@ public class FlowDownCheck {
 
     public static boolean isGreaterThan(CompositeLocation loc1, CompositeLocation loc2) {
 
+//      System.out.println("isGreaterThan= " + loc1 + " " + loc2);
+
       int baseCompareResult = compareBaseLocationSet(loc1, loc2);
       if (baseCompareResult == ComparisonResult.EQUAL) {
         if (compareDelta(loc1, loc2) == ComparisonResult.GREATER) {
@@ -1116,17 +1116,36 @@ public class FlowDownCheck {
         SSJavaLattice<String> lattice1 = getLatticeByDescriptor(d1);
         SSJavaLattice<String> lattice2 = getLatticeByDescriptor(d2);
 
+        // check if the spin location is appeared only at the end of the
+        // composite location
+        if (lattice1.getSpinLocSet().contains(loc1.getLocIdentifier())) {
+          if (i != (compLoc1.getSize() - 1)) {
+            throw new Error("The spin location " + loc1.getLocIdentifier()
+                + " cannot be appeared in the middle of composite location.");
+          }
+        }
+
+        if (lattice2.getSpinLocSet().contains(loc2.getLocIdentifier())) {
+          if (i != (compLoc2.getSize() - 1)) {
+            throw new Error("The spin location " + loc2.getLocIdentifier()
+                + " cannot be appeared in the middle of composite location.");
+          }
+        }
+
         if (!lattice1.equals(lattice2)) {
           throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2
               + " because they are not comparable.");
         }
 
         if (loc1.getLocIdentifier().equals(loc2.getLocIdentifier())) {
+          numOfTie++;
           // check if the current location is the spinning location
-          if (lattice1.getSpinLocSet().contains(loc1.getLocIdentifier())) {
+          // note that the spinning location only can be appeared in the last
+          // part of the composite location
+          if (numOfTie == compLoc1.getSize()
+              && lattice1.getSpinLocSet().contains(loc1.getLocIdentifier())) {
             return ComparisonResult.GREATER;
           }
-          numOfTie++;
           continue;
         } else if (lattice1.isGreaterThan(loc1.getLocIdentifier(), loc2.getLocIdentifier())) {
           return ComparisonResult.GREATER;

diff --git a/Robust/src/Tests/ssJava/flowdown/test.java b/Robust/src/Tests/ssJava/flowdown/test.java
index b0e75dadeb66e08e7672e19147e484f7e89b6ae3..605957b3458e6c0828371b82612bdb4404938ab7 100644 (file)
--- a/Robust/src/Tests/ssJava/flowdown/test.java
+++ b/Robust/src/Tests/ssJava/flowdown/test.java
@@ -91,6 +91,7 @@ public class test{
 
     @LATTICE("mL<mH,THISLOC=mL")
     public void doSpinField(){
+       //only last element of the composite location can be the spinning loc
 
        @LOC("mH") int varH;
        @LOC("mL") int varL;
@@ -105,6 +106,7 @@ public class test{
        
        localBar.b1++; // value can be moving among the same location
     }
+
 }