X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=Robust%2Fsrc%2FAnalysis%2FSSJava%2FSSJavaLattice.java;h=be1a342ec9ff6d2630cf5cc7d0b8908829c48559;hb=031636263ce6e4b6f35f3d9162460eb0ef536c2a;hp=cbbae46c8ffb2ae6a59c547a615a10bbd6fcb8ff;hpb=f0aec2e998d39bd8474da2e98da70bbf7a4f5b15;p=IRC.git

diff --git a/Robust/src/Analysis/SSJava/SSJavaLattice.java b/Robust/src/Analysis/SSJava/SSJavaLattice.java
index cbbae46c..be1a342e 100644
--- a/Robust/src/Analysis/SSJava/SSJavaLattice.java
+++ b/Robust/src/Analysis/SSJava/SSJavaLattice.java
@@ -1,16 +1,15 @@
 package Analysis.SSJava;
 
 import java.util.HashSet;
+import java.util.Iterator;
 import java.util.Set;
 
 import Util.Lattice;
 
 public class SSJavaLattice<T> extends Lattice<T> {
 
-  public static final String TOP = "_top_";
-  public static final String BOTTOM = "_bottom_";
-
   Set<T> sharedLocSet;
+  public static int seed = 0;
 
   public SSJavaLattice(T top, T bottom) {
     super(top, bottom);
@@ -36,4 +35,32 @@ public class SSJavaLattice<T> extends Lattice<T> {
     return put(higher, lower);
   }
 
+  public void insertNewLocationAtOneLevelHigher(T lowerLoc, T newLoc) {
+    // first identifying which location is connected to the input loc
+    Set<T> keySet = getKeySet();
+    Set<T> oneLevelHigherLocSet = new HashSet<T>();
+
+    for (Iterator iterator = keySet.iterator(); iterator.hasNext();) {
+      T locKey = (T) iterator.next();
+      Set<T> conntectedSet = get(locKey);
+      for (Iterator iterator2 = conntectedSet.iterator(); iterator2.hasNext();) {
+        T connectedLoc = (T) iterator2.next();
+        if (connectedLoc.equals(lowerLoc)) {
+          oneLevelHigherLocSet.add(locKey);
+        }
+      }
+    }
+
+    put(newLoc);
+    addRelationHigherToLower(newLoc, lowerLoc);
+
+    for (Iterator iterator = oneLevelHigherLocSet.iterator(); iterator.hasNext();) {
+      T higherLoc = (T) iterator.next();
+      // remove an existing edge between the higher loc and the input loc
+      get(higherLoc).remove(lowerLoc);
+      // add a new edge from the higher loc to the new location
+      put(higherLoc, newLoc);
+    }
+
+  }
 }