wow, this bug has been latent for a long time, easy fix

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index 3f13f4901b268c0adab3040bdd5c70062f6b4f8e..0b981bce7fe1892017ed8f64bcbe7d6d879a3c85 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -290,6 +290,42 @@ public class ReachGraph {
     }
   }
 
+  // this is a common operation in many transfer functions: we want
+  // to add an edge, but if there is already such an edge we should
+  // merge the properties of the existing and the new edges
+  protected void addEdgeOrMergeWithExisting( RefEdge edgeNew ) {
+
+    RefSrcNode src = edgeNew.getSrc();
+    assert belongsToThis( src );
+
+    HeapRegionNode dst = edgeNew.getDst();
+    assert belongsToThis( dst );
+
+    // look to see if an edge with same field exists
+    // and merge with it, otherwise just add the edge
+    RefEdge edgeExisting = src.getReferenceTo( dst, 
+                                               edgeNew.getType(),
+                                               edgeNew.getField() 
+                                               );
+       
+    if( edgeExisting != null ) {
+      edgeExisting.setBeta(
+                           Canonical.unionORpreds( edgeExisting.getBeta(),
+                                                   edgeNew.getBeta()
+                                                   )
+                           );
+      edgeExisting.setPreds(
+                            Canonical.join( edgeExisting.getPreds(),
+                                            edgeNew.getPreds()
+                                            )
+                            );
+       
+    } else {                     
+      addRefEdge( src, dst, edgeNew );
+    }
+  }
+
+
 
   ////////////////////////////////////////////////////
   //
@@ -412,8 +448,8 @@ public class ReachGraph {
                                        Canonical.intersection( betaY, betaHrn ),
                                        predsTrue
                                        );
-       
-       addRefEdge( lnX, hrnHrn, edgeNew );
+
+        addEdgeOrMergeWithExisting( edgeNew );
       }
     }
 
@@ -564,27 +600,7 @@ public class ReachGraph {
                                        predsTrue
                                        );
 
-       // look to see if an edge with same field exists
-       // and merge with it, otherwise just add the edge
-       RefEdge edgeExisting = hrnX.getReferenceTo( hrnY, 
-                                                    tdNewEdge,
-                                                    f.getSymbol() );
-       
-       if( edgeExisting != null ) {
-         edgeExisting.setBeta(
-                               Canonical.unionORpreds( edgeExisting.getBeta(),
-                                                edgeNew.getBeta()
-                                                )
-                               );
-          edgeExisting.setPreds(
-                                Canonical.join( edgeExisting.getPreds(),
-                                                edgeNew.getPreds()
-                                                )
-                                );
-       
-        } else {                         
-         addRefEdge( hrnX, hrnY, edgeNew );
-       }
+        addEdgeOrMergeWithExisting( edgeNew );
       }
     }
 
@@ -2497,8 +2513,6 @@ public class ReachGraph {
                                      predsTrue,                     // predicates
                                      hrnDstCallee.getDescription()  // description
                                      );                                        
-        } else {
-          assert hrnDstCaller.isWiped();
         }
 
         TypeDescriptor tdNewEdge =