use different graph writing options to better find reachability problems

diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
index 9310467054a77733f359b6513ef38173435a37b7..fdb092fe7c0838c94f97803549c5242af5c67e9e 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
+++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
@@ -714,11 +714,11 @@ public class DisjointAnalysis {
 
       try {        
        rg.writeGraph( "COMPLETE"+d,
-                       true,   // write labels (variables)
-                       true,   // selectively hide intermediate temp vars
-                       true,   // prune unreachable heap regions
-                       false,  // hide subset reachability states
-                       true ); // hide edge taints
+                       true,   // write labels (variables)                
+                       true,   // selectively hide intermediate temp vars 
+                       true,   // prune unreachable heap regions          
+                       false,  // hide subset reachability states         
+                       true ); // hide edge taints                        
       } catch( IOException e ) {}    
     }
   }

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index cce95f49432da9bf5488e22fc24e54c75afd5626..11b48e075c9970a3a0792926512b55e44cdbf7a4 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -1900,7 +1900,12 @@ public class ReachGraph {
 
     if( writeDebugDOTs ) {    
       try {
-        rg.writeGraph( "calleeview", true, false, false, true, true );
+        rg.writeGraph( "calleeview", 
+                       true,   // write labels (variables)                
+                       true,   // selectively hide intermediate temp vars 
+                       true,   // prune unreachable heap regions          
+                       true,   // hide subset reachability states         
+                       true ); // hide edge taints                        
       } catch( IOException e ) {}
     }
 
@@ -1924,9 +1929,17 @@ public class ReachGraph {
     if( writeDebugDOTs ) {
       try {
         rgCallee.writeGraph( "callee", 
-                             true, false, false, true, true );
+                             true,   // write labels (variables)                  
+                             true,   // selectively hide intermediate temp vars   
+                             true,   // prune unreachable heap regions            
+                             true,   // hide subset reachability states           
+                             true ); // hide edge taints                        
         writeGraph( "caller00In", 
-                    true, false, false, true, true, 
+                    true,  // write labels (variables)                
+                    true,  // selectively hide intermediate temp vars 
+                    true,  // prune unreachable heap regions          
+                    true,  // hide subset reachability states         
+                    true,  // hide edge taints                        
                     callerNodeIDsCopiedToCallee );
       } catch( IOException e ) {}
     }
@@ -2148,7 +2161,11 @@ public class ReachGraph {
     if( writeDebugDOTs ) {
       try {
         writeGraph( "caller20BeforeWipe", 
-                    true, false, false, true, true );
+                    true,   // write labels (variables)                
+                    true,   // selectively hide intermediate temp vars 
+                    true,   // prune unreachable heap regions          
+                    true,   // hide subset reachability states         
+                    true ); // hide edge taints                        
       } catch( IOException e ) {}
     }
 
@@ -2170,7 +2187,11 @@ public class ReachGraph {
     if( writeDebugDOTs ) {
       try {
         writeGraph( "caller30BeforeAddingNodes", 
-                    true, false, false, true, true );
+                    true,   // write labels (variables)                
+                    true,   // selectively hide intermediate temp vars 
+                    true,   // prune unreachable heap regions          
+                    true,   // hide subset reachability states         
+                    true ); // hide edge taints                        
       } catch( IOException e ) {}
     }
 
@@ -2235,7 +2256,11 @@ public class ReachGraph {
     if( writeDebugDOTs ) {
       try {
         writeGraph( "caller31BeforeAddingEdges", 
-                    true, false, false, true, true );
+                    true,   // write labels (variables)                
+                    true,   // selectively hide intermediate temp vars 
+                    true,   // prune unreachable heap regions          
+                    true,   // hide subset reachability states         
+                    true ); // hide edge taints                        
       } catch( IOException e ) {}
     }
 
@@ -2431,7 +2456,11 @@ public class ReachGraph {
     if( writeDebugDOTs ) {
       try {
         writeGraph( "caller35BeforeAssignReturnValue", 
-                    true, false, false, true, true );
+                    true,   // write labels (variables)                
+                    true,   // selectively hide intermediate temp vars 
+                    true,   // prune unreachable heap regions          
+                    true,   // hide subset reachability states         
+                    true ); // hide edge taints                        
       } catch( IOException e ) {}
     }
 
@@ -2513,7 +2542,11 @@ public class ReachGraph {
     if( writeDebugDOTs ) {
       try {
         writeGraph( "caller38propagateReach", 
-                    true, false, false, true, true );
+                    true,   // write labels (variables)                
+                    true,   // selectively hide intermediate temp vars 
+                    true,   // prune unreachable heap regions          
+                    true,   // hide subset reachability states         
+                    true ); // hide edge taints                        
       } catch( IOException e ) {}
     }
 
@@ -2539,7 +2572,11 @@ public class ReachGraph {
     if( writeDebugDOTs ) {
       try {
         writeGraph( "caller40BeforeShadowMerge", 
-                    true, false, false, true, true );
+                    true,   // write labels (variables)                
+                    true,   // selectively hide intermediate temp vars 
+                    true,   // prune unreachable heap regions          
+                    true,   // hide subset reachability states         
+                    true ); // hide edge taints                        
       } catch( IOException e ) {}
     }
     
@@ -2636,7 +2673,11 @@ public class ReachGraph {
     if( writeDebugDOTs ) {
       try {
         writeGraph( "caller45BeforeUnshadow", 
-                    true, false, false, true, true );
+                    true,   // write labels (variables)                
+                    true,   // selectively hide intermediate temp vars 
+                    true,   // prune unreachable heap regions          
+                    true,   // hide subset reachability states         
+                    true ); // hide edge taints                        
       } catch( IOException e ) {}
     }
     
@@ -2660,7 +2701,11 @@ public class ReachGraph {
     if( writeDebugDOTs ) {
       try {
         writeGraph( "caller50BeforeGlobalSweep", 
-                    true, false, false, true, true );
+                    true,   // write labels (variables)                
+                    true,   // selectively hide intermediate temp vars 
+                    true,   // prune unreachable heap regions          
+                    true,   // hide subset reachability states         
+                    true ); // hide edge taints                        
       } catch( IOException e ) {}
     }
 
@@ -2675,7 +2720,11 @@ public class ReachGraph {
     if( writeDebugDOTs ) {
       try {
         writeGraph( "caller90AfterTransfer", 
-                    true, false, false, true, true );
+                    true,   // write labels (variables)                
+                    true,   // selectively hide intermediate temp vars 
+                    true,   // prune unreachable heap regions          
+                    true,   // hide subset reachability states         
+                    true ); // hide edge taints                        
       } catch( IOException e ) {}
     }
   } 

diff --git a/Robust/src/Tests/disjoint/predicateTest3/makefile b/Robust/src/Tests/disjoint/predicateTest3/makefile
index b4cecea7779e5b4026ba39f93ea94b9bb5046dd6..42058b05c1455a1a5bef7ccb36ecaa8909d41d2e 100644 (file)
--- a/Robust/src/Tests/disjoint/predicateTest3/makefile
+++ b/Robust/src/Tests/disjoint/predicateTest3/makefile
@@ -8,10 +8,10 @@ BUILDSCRIPT=~/research/Robust/src/buildscript
 #DEBUGFLAGS= -disjoint-debug-callsite Foo main 1
 
 #DEBUGFLAGS= -disjoint-debug-callsite main analysisEntryMethod 1
-#DEBUGFLAGS= -disjoint-debug-callsite addSomething main 1
+DEBUGFLAGS= -disjoint-debug-callsite addSomething main 100
 #DEBUGFLAGS= -disjoint-debug-callsite addBar addSomething 1
 #DEBUGFLAGS= -disjoint-debug-callsite Bar addBar 1
-DEBUGFLAGS=
+#DEBUGFLAGS=
 
 BSFLAGS= -mainclass Test -justanalyze -disjoint -disjoint-k 2 -disjoint-write-dots final -disjoint-write-ihms -disjoint-alias-file aliases.txt normal -enable-assertions
 

diff --git a/Robust/src/Tests/disjoint/predicateTest3/test.java b/Robust/src/Tests/disjoint/predicateTest3/test.java
index 7bbce921e2149eb8155ee0d2e379bdde822be21e..ba6896951d6209f23abd33f15a21d127461bde48 100644 (file)
--- a/Robust/src/Tests/disjoint/predicateTest3/test.java
+++ b/Robust/src/Tests/disjoint/predicateTest3/test.java
@@ -16,7 +16,7 @@ public class Test {
   }   
 
   public static void addSomething( Foo x ) {
-    x.f = disjoint added new Foo();
+    //x.f = disjoint added new Foo();
   }
 
   public static Foo getAFoo() {