bug fix.

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index 6cf343e48ab21384776b3ffd59143ff9433506b5..f23e0f0c2ea94a84d59f080952c1b2a0c94af35e 100644 (file)
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -1422,6 +1422,7 @@ public class DefinitelyWrittenCheck {
       case FKind.FlatFieldNode:
       case FKind.FlatElementNode: {
 
+
         if (fn.kind() == FKind.FlatFieldNode) {
           FlatFieldNode ffn = (FlatFieldNode) fn;
           lhs = ffn.getDst();
@@ -1442,7 +1443,14 @@ public class DefinitelyWrittenCheck {
 
         // read field
         NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
-        NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
+        System.out.println("rhs=" + rhs);
+        NTuple<Descriptor> fldHeapPath;
+        if (srcHeapPath != null) {
+          fldHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
+        } else {
+          // if srcHeapPath is null, it is static reference
+          fldHeapPath = new NTuple<Descriptor>();
+        }
         fldHeapPath.add(fld);
 
         if (fld.getType().isImmutable()) {

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 78d82df1aaa314f81a8ef5a6d38a9da3493672e2..9a7855c3a72f87fff54886c993dda5b8414f6f9f 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -1298,7 +1298,6 @@ public class FlowDownCheck {
       inputSet.add(rightLoc);
       CompositeLocation glbCompLoc =
           CompositeLattice.calculateGLB(inputSet, generateErrorMessage(cd, on));
-      // System.out.println("# glbCompLoc=" + glbCompLoc);
       return glbCompLoc;
 
     default:
@@ -1381,7 +1380,7 @@ public class FlowDownCheck {
         loc.addLocation(fieldLoc);
       } else if (d == null) {
         // access static field
-        ClassDescriptor cd = nn.getClassDesc();
+        FieldDescriptor fd = nn.getField();
 
         MethodLattice<String> localLattice = ssjava.getMethodLattice(md);
         String globalLocId = localLattice.getGlobalLoc();
@@ -1390,6 +1389,10 @@ public class FlowDownCheck {
               + generateErrorMessage(md.getClassDesc(), nn));
         }
         loc.addLocation(new Location(md, globalLocId));
+
+        Location fieldLoc = (Location) fd.getType().getExtension();
+        loc.addLocation(fieldLoc);
+
         return loc;
 
       }