changes.

[IRC.git] / Robust / src / Analysis / SSJava / FlowDownCheck.java

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 375e92e8f65aaff5bf1df5c43cbf7ea6a0e0ec1f..4d949f4df66d143882821569150f4e78c134482b 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -1264,12 +1264,14 @@ public class FlowDownCheck {
       System.out.println("rhsLocation=" + rhsLocation);
       System.out.println("constraint=" + constraint);
 
-      if (constraint != null) {
-        inputGLBSet.add(rhsLocation);
-        inputGLBSet.add(constraint);
-        srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an));
-      } else {
-        srcLocation = rhsLocation;
+      srcLocation = rhsLocation;
+
+      if (!rhsLocation.get(rhsLocation.getSize() - 1).isTop()) {
+        if (constraint != null) {
+          inputGLBSet.add(rhsLocation);
+          inputGLBSet.add(constraint);
+          srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an));
+        }
       }
 
       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
@@ -1595,14 +1597,14 @@ public class FlowDownCheck {
 
         // check if the shared location is appeared only at the end of the
         // composite location
-        if (lattice.getSpinLocSet().contains(loc1.getLocIdentifier())) {
+        if (lattice.getSharedLocSet().contains(loc1.getLocIdentifier())) {
           if (i != (compLoc1.getSize() - 1)) {
             throw new Error("The shared location " + loc1.getLocIdentifier()
                 + " cannot be appeared in the middle of composite location at" + msg);
           }
         }
 
-        if (lattice.getSpinLocSet().contains(loc2.getLocIdentifier())) {
+        if (lattice.getSharedLocSet().contains(loc2.getLocIdentifier())) {
           if (i != (compLoc2.getSize() - 1)) {
             throw new Error("The shared location " + loc2.getLocIdentifier()
                 + " cannot be appeared in the middle of composite location at " + msg);
@@ -1621,7 +1623,7 @@ public class FlowDownCheck {
           // note that the spinning location only can be appeared in the last
           // part of the composite location
           if (awareSharedLoc && numOfTie == compLoc1.getSize()
-              && lattice.getSpinLocSet().contains(loc1.getLocIdentifier())) {
+              && lattice.getSharedLocSet().contains(loc1.getLocIdentifier())) {
             return ComparisonResult.GREATER;
           }
           continue;