[Javapathfinder-svn] SF.net SVN: javapathfinder:[1020] trunk

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

Revision: 1020
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1020&view=rev
Author:   pcmehlitz
Date:     2008-09-24 18:45:18 +0000 (Wed, 24 Sep 2008)

Log Message:
-----------
* added JPF.addUniqueTypeListener(..), to better support autoload capabilities (somebody might also load
those listeners explicitly). This required inclusion checks in Search/VM and the Multicasters

* fixed bug in Classnfo autoload mechanism (should keep own registry nonetheless)

* extended NonNullChecker to also support static and instance field checks. Semantics are debatable, but
at least consistent: throw AssertionErrors if

 - a class with declared @NonNull ref fields doesn't have a ctor or clinit
 - if a declared @NonNull reference field is not initialized at the end of a ctor or clinit execution
 - if a PUTFIELD/PUTSTATIC nullifies a @NonNull field
 
 maybe the ctor/clinit checks should only be performed at the end of the concrete type clinit/ctor, but I'd
 rather keep attributes class local
  

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/JPF.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/VMListenerMulticaster.java
    trunk/src/gov/nasa/jpf/search/Search.java
    trunk/src/gov/nasa/jpf/search/SearchListenerMulticaster.java
    trunk/src/gov/nasa/jpf/tools/NonNullChecker.java
    trunk/test/gov/nasa/jpf/test/TestNonNull.java


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