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

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

Revision: 562
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=562&view=rev
Author:   pcmehlitz
Date:     2007-09-12 12:09:22 -0700 (Wed, 12 Sep 2007)

Log Message:
-----------
* better support for Enums - added a ClassInfo.isEnum to easily identify enum const objects

* <sigh> had to add a "longjmp" exception (gov.nasa.jpf.jvm.ClinitRequired) to handle clinit
requests from deep inside of the stack, where we can't simply use a return value or even know
what the executed insn was that caused the request. This is for instance required if we reference
class fields & arrays of Annotation proxy objects (how obvious!). It's used in the
getAnnotation()/getAnnotations() methods

Not so nice.

Also refactored some of the repeatInvocation() handling into MJIEnv, since it's most likely
going to be used from native peer methods (the bytecodes are mostly simple)

* and with all this, implemented Enum and Class and Class[] Annotation elements, both on the JPF
(AnnotationInfo) and the modeling side. AnnotationInfo stores class elements as ClassInfo references,
and Enums as FieldInfo references (not sure if there could be other field refs in Annotations, but
assume not). This was quite a tour de force

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_AnnotationProxyBase.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/jvm/ClinitRequired.java


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