an example showing empty reach state propagation that we considered for CC submission...

diff --git a/Robust/src/Tests/disjoint/cc-submission-example/makefile b/Robust/src/Tests/disjoint/cc-submission-example/makefile
new file mode 100644 (file)
index 0000000..75b09b4
--- /dev/null
+++ b/Robust/src/Tests/disjoint/cc-submission-example/makefile
@@ -0,0 +1,30 @@
+PROGRAM=test
+
+SOURCE_FILES=$(PROGRAM).java
+
+BUILDSCRIPT=~/research/Robust/src/buildscript
+
+BSFLAGS= -mainclass Test -joptimize -justanalyze -disjoint -disjoint-k 1 -enable-assertions
+DEBUGFLAGS= -disjoint-debug-snap-method graphLoop 0 10 true #-disjoint-write-dots all #-disjoint-write-initial-contexts -disjoint-write-ihms 
+
+all: $(PROGRAM).bin
+
+view: PNGs
+       eog *.png &
+
+PNGs: DOTs
+       d2p *COMPLETE*.dot
+
+DOTs: $(PROGRAM).bin
+
+$(PROGRAM).bin: $(SOURCE_FILES)
+       $(BUILDSCRIPT) $(BSFLAGS) $(DEBUGFLAGS) -o $(PROGRAM) $(SOURCE_FILES)
+
+clean:
+       rm -f  $(PROGRAM).bin
+       rm -fr tmpbuilddirectory
+       rm -f  *~
+       rm -f  *.dot
+       rm -f  *.png
+       rm -f  aliases.txt
+       rm -f  effects.txt

diff --git a/Robust/src/Tests/disjoint/cc-submission-example/test.java b/Robust/src/Tests/disjoint/cc-submission-example/test.java
new file mode 100644 (file)
index 0000000..a52b275
--- /dev/null
+++ b/Robust/src/Tests/disjoint/cc-submission-example/test.java
@@ -0,0 +1,48 @@
+public class Graph {
+  public Graph() {}
+  public Vertex vertex;
+}
+
+public class Vertex {
+  public Vertex() {}
+  public Vertex f;
+  public boolean marked;
+  public void updateVertex();
+}
+
+
+public class Test {
+
+  static public void main( String[] args ) {
+    Test.graphLoop( 2 );
+  }
+
+
+  static public void graphLoop( int nGraphs ) {
+
+    Graph[] a = new Graph[nGraphs];
+
+    for( int i = 0; i < nGraphs; i++ ) {
+
+      Graph g = disjoint graphs new Graph();
+      Vertex v1 = new Vertex();
+      g.vertex = v1;
+      Vertex v2 = new Vertex();
+      v2.f = v1; v1.f = v2 ;
+      a[i] = g;
+    }
+    /*
+    for( int i = 0; i < nGraphs; i++ ) {
+      
+      Graph  g = a[i];
+      Vertex v = g.vertex;
+
+      while( !v.marked ) {
+        v.marked = true;
+        v.updateVertex();
+        v=v.f;
+      } 
+    }
+    */
+  }
+}

diff --git a/Robust/src/Tests/disjoint/tiny/makefile b/Robust/src/Tests/disjoint/tiny/makefile
new file mode 100644 (file)
index 0000000..5f210ca
--- /dev/null
+++ b/Robust/src/Tests/disjoint/tiny/makefile
@@ -0,0 +1,27 @@
+PROGRAM=test
+
+SOURCE_FILES=$(PROGRAM).java
+
+BUILDSCRIPT=~/research/Robust/src/buildscript
+BSFLAGS= -mainclass Test -disjoint -disjoint-k 1 -disjoint-alias-file aliases.txt normal -enable-assertions -justanalyze #-joptimize #-disjoint-write-dots final
+
+all: $(PROGRAM).bin
+
+view: PNGs
+       eog *.png &
+
+PNGs: DOTs
+       d2p *COMPLETE*.dot
+
+DOTs: $(PROGRAM).bin
+
+$(PROGRAM).bin: $(SOURCE_FILES)
+       $(BUILDSCRIPT) $(BSFLAGS) -o $(PROGRAM) $(SOURCE_FILES)
+
+clean:
+       rm -f  $(PROGRAM).bin
+       rm -fr tmpbuilddirectory
+       rm -f  *~
+       rm -f  *.dot
+       rm -f  *.png
+       rm -f  aliases.txt

diff --git a/Robust/src/Tests/disjoint/tiny/test.java b/Robust/src/Tests/disjoint/tiny/test.java
new file mode 100644 (file)
index 0000000..730ed86
--- /dev/null
+++ b/Robust/src/Tests/disjoint/tiny/test.java
@@ -0,0 +1,17 @@
+public class Foo {
+  public Foo() {}
+}
+
+public class Test {
+  static public void main( String[] args ) {
+    Foo[] x = new Foo[10];
+
+    genreach yo;
+
+    for( int i = 0; i < 10; i++ ) {
+      x[i] = new Foo();
+    }
+
+    System.out.println( x[0] );
+  }
+}