From: jjenista <jjenista>
Date: Fri, 6 Jan 2012 18:14:26 +0000 (+0000)
Subject: a useful example that needs defreach
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=0d042a64d55f4c14047f85e9cdba462ac1b49e0d;p=IRC.git

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
index 00000000..048514bb
--- /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
index 00000000..a017082d
--- /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;
+  }
+
+}