From a5e144cbd299e81d645cfd9c199bd02a032f256d Mon Sep 17 00:00:00 2001
From: jjenista <jjenista>
Date: Fri, 18 Nov 2011 21:41:47 +0000
Subject: [PATCH] vector resize isn't a problem, even without definite
 reachability, because we have a special case of def reach just for array
 references

---
 .../Tests/disjoint/definiteVector/makefile    | 25 +++++++++++
 .../Tests/disjoint/definiteVector/test.java   | 42 +++++++++++++++++++
 2 files changed, 67 insertions(+)
 create mode 100644 Robust/src/Tests/disjoint/definiteVector/makefile
 create mode 100644 Robust/src/Tests/disjoint/definiteVector/test.java

diff --git a/Robust/src/Tests/disjoint/definiteVector/makefile b/Robust/src/Tests/disjoint/definiteVector/makefile
new file mode 100644
index 00000000..048514bb
--- /dev/null
+++ b/Robust/src/Tests/disjoint/definiteVector/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/definiteVector/test.java b/Robust/src/Tests/disjoint/definiteVector/test.java
new file mode 100644
index 00000000..1fc55e52
--- /dev/null
+++ b/Robust/src/Tests/disjoint/definiteVector/test.java
@@ -0,0 +1,42 @@
+public class Foo {
+  public Foo f;
+  public Foo g;
+}
+
+public class Test {
+
+  static public void main( String args[] ) {
+
+    Vector v = new Vector();
+
+    for( int i = 0; i < 3; ++i ) {
+      Foo a = getFlagged();
+      Foo b = getUnflagged();
+      a.f = b;
+
+      // At this point it is clear all b's are
+      // reachable from at most one a
+      gendefreach z0;
+      genreach z0;
+
+      v.addElement( a );
+    }
+
+    // However, the v.addElement may resize the
+    // vector, so analysis takes resize into account
+    // and ruins the precision
+    gendefreach z1;
+    genreach z1;
+
+    System.out.println( v.elementAt( 0 ).toString() );
+  }
+
+  static public Foo getFlagged() {
+    return disjoint jupiter new Foo();
+  }
+
+  static public Foo getUnflagged() {
+    return new Foo();
+  }
+
+}
-- 
2.34.1