a useful example that needs defreach

diff --git a/Robust/src/Tests/disjoint/definite-example/makefile b/Robust/src/Tests/disjoint/definite-example/makefile
new file mode 100644 (file)
index 0000000..048514b
--- /dev/null
+++ b/Robust/src/Tests/disjoint/definite-example/makefile
@@ -0,0 +1,25 @@
+PROGRAM=Test
+
+SOURCE_FILES=test.java
+
+BUILDSCRIPT=../../../buildscript
+
+DISJOINT= -disjoint -disjoint-k 1 -enable-assertions #-do-definite-reach-analysis
+
+BSFLAGS= -justanalyze -mainclass $(PROGRAM) -heapsize-mb 1024 -noloop -joptimize -debug #-flatirusermethods
+
+
+all:
+       $(BUILDSCRIPT) -thread $(BSFLAGS) $(DISJOINT) -o $(PROGRAM)s -builddir sing $(SOURCE_FILES)
+
+clean:
+       rm -f  $(PROGRAM)s.bin
+       rm -fr sing
+       rm -f  *~
+       rm -f  *.dot
+       rm -f  *.png
+       rm -f  *.txt
+       rm -f  aliases.txt
+       rm -f  mlpReport*txt
+       rm -f  results*txt
+       rm -f  coreprof.dat

diff --git a/Robust/src/Tests/disjoint/definite-example/test.java b/Robust/src/Tests/disjoint/definite-example/test.java
new file mode 100644 (file)
index 0000000..a017082
--- /dev/null
+++ b/Robust/src/Tests/disjoint/definite-example/test.java
@@ -0,0 +1,70 @@
+public class Foo {
+  int z;
+}
+
+public class Test {
+
+  
+
+  static public void main( String args[] ) {
+
+    int n = 3;
+
+    Foo[] a = getArray();
+    for( int j = 0; j < n; ++j ) {
+      a[j] = getFoo();
+    }
+
+    //Foo a = getFlagged();
+    //Foo b = getUnflagged();
+    //a.f = b;
+    //
+    //// a is flagged and b is reachable from
+    //// at most one object from that site
+    //gendefreach z0;
+    //genreach z0;
+    //
+    //Foo c = new Foo();
+    //a.g = c;
+    //
+    //Foo t = getFlagged();
+    //t = getFlagged();
+    //
+    //Foo u = getUnflagged();
+    //u = getUnflagged();
+    //
+    //// a is flagged and b is reachable from
+    //// at most one object from that site, even
+    //// though a and b are summarized now.  a
+    //// has a reference to a new object c
+    //gendefreach z1;
+    //genreach z1;
+    //
+    //c.f = b;
+    //
+    //// if we had definite reachability analysis
+    //// we would realize b is already reachable
+    //// from a
+    //gendefreach z3;
+    //genreach z3;
+    //
+    //System.out.println( " "+a+b+c );
+
+    int total = 0;
+    for( int j = 0; j < n; ++j ) {
+      total += a[j].z;
+    }
+    System.out.println( " "+total );
+  }
+
+  static public Foo[] getArray() {
+    return disjoint jupiter new Foo[]();
+  }
+
+  static public Foo getFoo() {
+    Foo f = new Foo();
+    f.z = 1;
+    return f;
+  }
+
+}