tests for playing around with analysis with respect to empty reach states
authorjjenista <jjenista>
Wed, 12 Jan 2011 22:46:28 +0000 (22:46 +0000)
committerjjenista <jjenista>
Wed, 12 Jan 2011 22:46:28 +0000 (22:46 +0000)
Robust/src/Tests/disjoint/empty-reach/makefile [new file with mode: 0644]
Robust/src/Tests/disjoint/empty-reach/test.java [new file with mode: 0644]

diff --git a/Robust/src/Tests/disjoint/empty-reach/makefile b/Robust/src/Tests/disjoint/empty-reach/makefile
new file mode 100644 (file)
index 0000000..0e28a60
--- /dev/null
@@ -0,0 +1,28 @@
+PROGRAM=test
+
+SOURCE_FILES=$(PROGRAM).java
+
+BUILDSCRIPT=~/research/Robust/src/buildscript
+BSFLAGS= -joptimize -mainclass Test -justanalyze -disjoint -disjoint-k 1 -enable-assertions \
+#-flatirusermethods -disjoint-write-dots final -disjoint-alias-file aliases.txt normal
+
+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/empty-reach/test.java b/Robust/src/Tests/disjoint/empty-reach/test.java
new file mode 100644 (file)
index 0000000..00b0118
--- /dev/null
@@ -0,0 +1,46 @@
+public class Foo {
+  public Foo() {}
+  public Foo f;
+  public Bar b;
+}
+
+public class Bar {
+  public Bar() {}
+}
+
+public class Test {
+  static public void main( String[] args ) {
+    Foo x =            new Foo();
+    Foo y =            new Foo();
+    Foo z = disjoint Z new Foo();
+    Foo w = disjoint W new Foo();
+    
+    Bar bNoZ  = getNewBar();
+    Bar bYesZ = getNewBar();
+    
+    x.b = bNoZ;
+    y.b = bYesZ;
+
+    genreach q1;
+
+    z.f = x;
+
+    genreach q2;
+
+    w.f = y;
+    
+    genreach q3;
+
+    Bar causeSummary = getNewBar();
+    causeSummary = getNewBar();
+
+    genreach q4;
+
+
+    //genreach q5;
+  }
+
+  static public Bar getNewBar() {
+    return new Bar();
+  }
+}