bug fix

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index 331a32b52e7fa907b5b2c1423cdfa68a2d3f5b1b..2536171de0ec1049f11cba86a0988f63991ca57f 100644 (file)
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -143,7 +143,6 @@ public class DefinitelyWrittenCheck {
     ClearingSummary result =
         mapMethodDescriptorToCompleteClearingSummary.get(sortedDescriptors.peekFirst());
 
     ClearingSummary result =
         mapMethodDescriptorToCompleteClearingSummary.get(sortedDescriptors.peekFirst());
 

-    System.out.println("checkSharedLocationResult=" + result);

 
     Set<NTuple<Descriptor>> hpKeySet = result.keySet();
     for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) {
 
     Set<NTuple<Descriptor>> hpKeySet = result.keySet();
     for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) {


@@ -166,7 +165,6 @@ public class DefinitelyWrittenCheck {
     // the same time once per the out-most loop
 
     computeReadSharedDescriptorSet();
     // the same time once per the out-most loop
 
     computeReadSharedDescriptorSet();

-    System.out.println("Reading Shared Location=" + mapSharedLocation2DescriptorSet);

 
     methodDescriptorsToVisitStack.clear();
 
 
     methodDescriptorsToVisitStack.clear();
 


@@ -960,6 +958,8 @@ public class DefinitelyWrittenCheck {
         // add <hp,statement,false> in which hp is an element of
         // READ_bound set
         // of callee: callee has 'read' requirement!
         // add <hp,statement,false> in which hp is an element of
         // READ_bound set
         // 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);
         for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) {
           NTuple<Descriptor> read = (NTuple<Descriptor>) iterator.next();
           Hashtable<FlatNode, Boolean> gen = curr.get(read);


@@ -1320,8 +1320,7 @@ public class DefinitelyWrittenCheck {
           }
         }
 
           }
         }
 

-        // need to kill hp(x.f) from WT
-        writtenSet.remove(readingHeapPath);
+        //no need to kill hp(x.f) from WT

       }
 
     }
       }
 
     }


@@ -1368,7 +1367,7 @@ public class DefinitelyWrittenCheck {
 
       if (fc.getThis() != null) {
         bindHeapPathCallerArgWithCaleeParam(fc);
 
       if (fc.getThis() != null) {
         bindHeapPathCallerArgWithCaleeParam(fc);

-
+        

         // add heap path, which is an element of READ_bound set and is not
         // an
         // element of WT set, to the caller's READ set
         // add heap path, which is an element of READ_bound set and is not
         // an
         // element of WT set, to the caller's READ set