[Javapathfinder-svn] SF.net SVN: javapathfinder:[1703] branches/mango/MangoJPF

[<fra...@us...>]

Revision: 1703
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1703&view=rev
Author:   frankrimlinger
Date:     2009-06-30 15:40:38 +0000 (Tue, 30 Jun 2009)

Log Message:
-----------
TheMangoFormal aliased classes in the java package were not being modeled because the java package was specified as a "mango native" package.  This feature was originally introduced to allow selective modeling of a "blended" jpf/formal environment.  Since blending is not a good idea, the jpf environment should always be masked in its entirety, so this feature has  been eliminated.  Instead, all packages in the bootclasspath are designated as mango native, and then classes within a native class are modeled if they contain "_MangoFormal" in their name.  This is a temporary solution.  A better solution is to introduce a "user class loader" to jpf to allow for a "user environment" that can occupy the same namespace as the boot loader.  Then it will not be necessary to alias the class names and many nasty technical issues will go away.  But moving on for now.

Next bug, for some reason, the total vertex for an ASTORE fails to get created during phase1.  Maybe some kind of exception handler bug??

Modified Paths:
--------------
    branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
    branches/mango/MangoJPF/src/mango/intro/ConfigurationDetails.java
    branches/mango/MangoJPF/src/mango/intro/LoginDialog.java


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