diff src/main/gov/nasa/jpf/vm/ClassInfo.java @ 7:b822e7665585

added a @JPFAttribute(TYPE_NAME,...) annotation for model classes (class, field and method target), which causes JPF to automatically set attribute objects that are instantiated from the provided type name args. Note that the respective attribute classes need to have a public default constructor. Added a JPFAttrAnnotationTest to show how to use it. This is the generic mechanism to use if we need to mark ClassInfos, MethodInfos and FieldInfos either from sources (using annotations), or from config files (type names/matchers used from listeners etc.) - base the processing on attributes, and set them from annotations via @JPFAttribute Refactored MethodInfo linking to happen from Initializer.setMethodDone() so that annotations are already parsed (setMethod() is too early since none of the classfile method attributes are parsed at this point)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 06 Feb 2015 17:28:55 -0800
parents 61d41facf527
children e15b03204dc7
line wrap: on
line diff
--- a/src/main/gov/nasa/jpf/vm/ClassInfo.java	Fri Feb 06 10:12:12 2015 -0800
+++ b/src/main/gov/nasa/jpf/vm/ClassInfo.java	Fri Feb 06 17:28:55 2015 -0800
@@ -362,6 +362,8 @@
         } else {
           instanceFields[iInstance++] = fi;
         }
+        
+        processJPFAttrAnnotation(fi);
       }
 
       iFields = instanceFields;
@@ -371,19 +373,48 @@
     }
   }
 
-  public void setMethods (MethodInfo[] methods) {
-    if (methods != null && methods.length > 0) {
-      HashMap<String, MethodInfo> map = new LinkedHashMap<String, MethodInfo>();
+  protected void setMethod (MethodInfo mi){
+    mi.linkToClass(this);
+    methods.put( mi.getUniqueName(), mi);
+    processJPFAttrAnnotation(mi);
+  }
+  
+  public void setMethods (MethodInfo[] newMethods) {
+    if (newMethods != null && newMethods.length > 0) {
+      methods = new LinkedHashMap<String, MethodInfo>();
 
-      for (int i = 0; i < methods.length; i++) {
-        MethodInfo mi = methods[i];
-        mi.linkToClass(this);
-        map.put(mi.getUniqueName(), mi);
+      for (int i = 0; i < newMethods.length; i++) {
+        setMethod( newMethods[i]);
       }
-      
-      this.methods = map;
     }
   }
+ 
+  protected void processJPFAttrAnnotation(InfoObject infoObj){
+    AnnotationInfo ai = infoObj.getAnnotation("gov.nasa.jpf.annotation.JPFAttribute");
+    if (ai != null){
+      String[] attrTypes = ai.getValueAsStringArray();
+      if (attrTypes != null){
+        ClassLoader loader = config.getClassLoader();
+
+        for (String clsName : attrTypes){
+          try {
+            Class<?> attrCls = loader.loadClass(clsName);
+            Object attr = attrCls.newInstance(); // needs to have a default ctor
+            infoObj.addAttr(attr);
+            
+          } catch (ClassNotFoundException cnfx){
+            logger.warning("attribute class not found: " + clsName);
+            
+          } catch (IllegalAccessException iax){
+            logger.warning("attribute class has no public default ctor: " + clsName);            
+            
+          } catch (InstantiationException ix){
+            logger.warning("attribute class has no default ctor: " + clsName);            
+          }
+        }
+      }
+    }    
+  }
 
   public AnnotationInfo getResolvedAnnotationInfo (String typeName){
     return classLoader.getResolvedAnnotationInfo( typeName);
@@ -511,6 +542,7 @@
     
     setAssertionStatus();
     processJPFConfigAnnotation();
+    processJPFAttrAnnotation(this);
     loadAnnotationListeners();    
   }