bug fix: no need to check flow down rule for abstract method

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index c108946be42299ec8ed682bd3269abf7442fc4ee..1f4c7fc59500bd8a8ba3045000e44c016ecbeb19 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -1018,43 +1018,46 @@ public class FlowDownCheck {
 
     ClassDescriptor cd = md.getClassDesc();
     Vector<AnnotationDescriptor> annotationVec = vd.getType().getAnnotationMarkers();
 
     ClassDescriptor cd = md.getClassDesc();
     Vector<AnnotationDescriptor> annotationVec = vd.getType().getAnnotationMarkers();

+    
+    if(!md.getModifiers().isAbstract()){
+      // currently enforce every variable to have corresponding location
+      if (annotationVec.size() == 0) {
+        throw new Error("Location is not assigned to variable " + vd.getSymbol() + " in the method "
+            + md.getSymbol() + " of the class " + cd.getSymbol());
+      }

 
 

-    // currently enforce every variable to have corresponding location
-    if (annotationVec.size() == 0) {
-      throw new Error("Location is not assigned to variable " + vd.getSymbol() + " in the method "
-          + md.getSymbol() + " of the class " + cd.getSymbol());
-    }
+      if (annotationVec.size() > 1) { // variable can have at most one location
+        throw new Error(vd.getSymbol() + " has more than one location.");
+      }

 
 

-    if (annotationVec.size() > 1) { // variable can have at most one location
-      throw new Error(vd.getSymbol() + " has more than one location.");
-    }
+      AnnotationDescriptor ad = annotationVec.elementAt(0);

 
 

-    AnnotationDescriptor ad = annotationVec.elementAt(0);
+      if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {

 
 

-    if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
+        if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
+          String locDec = ad.getValue(); // check if location is defined

 
 

-      if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
-        String locDec = ad.getValue(); // check if location is defined
+          if (locDec.startsWith(SSJavaAnalysis.DELTA)) {
+            DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec);
+            d2loc.put(vd, deltaLoc);
+            addLocationType(vd.getType(), deltaLoc);
+          } else {
+            CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);

 
 

-        if (locDec.startsWith(SSJavaAnalysis.DELTA)) {
-          DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec);
-          d2loc.put(vd, deltaLoc);
-          addLocationType(vd.getType(), deltaLoc);
-        } else {
-          CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
+            Location lastElement = compLoc.get(compLoc.getSize() - 1);
+            if (ssjava.isSharedLocation(lastElement)) {
+              ssjava.mapSharedLocation2Descriptor(lastElement, vd);
+            }

 
 

-          Location lastElement = compLoc.get(compLoc.getSize() - 1);
-          if (ssjava.isSharedLocation(lastElement)) {
-            ssjava.mapSharedLocation2Descriptor(lastElement, vd);
+            d2loc.put(vd, compLoc);
+            addLocationType(vd.getType(), compLoc);

           }
 
           }
 

-          d2loc.put(vd, compLoc);
-          addLocationType(vd.getType(), compLoc);

         }
         }

-

       }
     }
 
       }
     }
 

+

   }
 
   private DeltaLocation parseDeltaDeclaration(MethodDescriptor md, TreeNode n, String locDec) {
   }
 
   private DeltaLocation parseDeltaDeclaration(MethodDescriptor md, TreeNode n, String locDec) {