[Javapathfinder-devel] SF.net SVN: javapathfinder: [395] trunk

[<pcm...@us...>]

Revision: 395
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=395&view=rev
Author:   pcmehlitz
Date:     2007-06-26 17:15:59 -0700 (Tue, 26 Jun 2007)

Log Message:
-----------
* first installment of the Annotation replacement. We now don't use the real annotations anymore,
but model them as AnnotationInfo (created from bcel AnnotationEntries). The main reason for this is
to avoid having to put model types (like the statechart @Params) in the CLASSPATH.

AnnotationLoader/LoadedAnnotations are gone.

reflection support for Annotations (i.e. use in the application) still needs to be done. For now
we are mostly concerned about using annotations to specify JPF properties.

* updated bcel to the latest and greatest for the annotation support

* extended the ObjectTracker to check for @NonShared annotations - if a monitored object that has such
a class annotation is called or modified in another thread than its creator, we report a property
violation

* added a simple TestAnnotationProperties to the regression tests

* factored AnnotationSupport into a InfoObject class, which is the root for ClassInfo, MethodInfo, FieldInfo

* added a generic TestJPF.runJPFError() method

* added some post exec info to MONITOR instructions

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
    trunk/lib/bcel.jar
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/abstraction/filter/IgnoresFromAnnotations.java
    trunk/src/gov/nasa/jpf/jvm/abstraction/filter/IncludesFromAnnotations.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/MONITORENTER.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/MONITOREXIT.java
    trunk/src/gov/nasa/jpf/tools/ExecTracker.java
    trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
    trunk/test/gov/nasa/jpf/jvm/TestJPF.java

Added Paths:
-----------
    trunk/env/jpf/gov/nasa/jpf/NonShared.java
    trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
    trunk/src/gov/nasa/jpf/jvm/InfoObject.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LockInstruction.java
    trunk/test/gov/nasa/jpf/mc/TestAnnotationProperties.java
    trunk/test/gov/nasa/jpf/mc/TestAnnotationPropertiesJPF.java

Removed Paths:
-------------
    trunk/src/gov/nasa/jpf/jvm/AnnotationLoader.java
    trunk/src/gov/nasa/jpf/jvm/LoadedAnnotations.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.