bug fix on the definitely written check: Field read does not need to remove OW set.

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index c6d2b3589579494c2bc40cff6ba9cc2f648e5fd7..331a32b52e7fa907b5b2c1423cdfa68a2d3f5b1b 100644 (file)
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -962,7 +962,6 @@ public class DefinitelyWrittenCheck {
         // of callee: callee has 'read' requirement!
         for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) {
           NTuple<Descriptor> read = (NTuple<Descriptor>) iterator.next();
-
           Hashtable<FlatNode, Boolean> gen = curr.get(read);
           if (gen == null) {
             gen = new Hashtable<FlatNode, Boolean>();
@@ -1029,7 +1028,6 @@ public class DefinitelyWrittenCheck {
     // transform all READ/OVERWRITE set from the any possible
     // callees to the
     // caller
-
     calleeUnionBoundReadSet.clear();
     calleeIntersectBoundOverWriteSet.clear();
 
@@ -1380,7 +1378,6 @@ public class DefinitelyWrittenCheck {
             readSet.add(read);
           }
         }
-        writtenSet.removeAll(calleeUnionBoundReadSet);
 
         // add heap path, which is an element of OVERWRITE_bound set, to the
         // caller's WT set
@@ -1388,7 +1385,7 @@ public class DefinitelyWrittenCheck {
           NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
           writtenSet.add(write);
         }
-      }
+      } 
 
     }
       break;