vector resize isn't a problem, even without definite reachability, because we have...

diff --git a/Robust/src/Tests/disjoint/definiteVector/makefile b/Robust/src/Tests/disjoint/definiteVector/makefile
new file mode 100644 (file)
index 0000000..048514b
--- /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 (file)
index 0000000..1fc55e5
--- /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();
+  }
+
+}