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

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

Revision: 1545
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1545&view=rev
Author:   frankrimlinger
Date:     2009-05-23 03:15:29 +0000 (Sat, 23 May 2009)

Log Message:
-----------
The entire soundness-ready clinit apparatus has been ported.  The only missing item is the new HasCommutingClinit rule, for just-in-time resolution of the commuting clinit condition.  This will be added just as soon as the rulebase is accessible, right now MangoJPF doesn't run because there is still too much trauma in the code base. 

The clinit-4 rules have all been ported.  Two nice simplifications have occurred with the introduction of jpf.  First, "resolution" as defined in JVM2nd ed for classes, methods, and fields is not performed by the mango formal peer.  All of these considerations are taken care of long before the mango level is reached.  Second, all the required information about resolved class names and types and so on is already computed in advance by bcel and usually exported by the jpf instruction classes.

With exception handling and class initialization and the foundations for method invocation in place, all the big issues are resolved.  It remains only to port the remaining bytecodes along the established patterns and clean up the remaining issues in the backup algorithm.  Then finally phase 1 testing can start.

Modified Paths:
--------------
    branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/BuildAbstractUcon.java
    branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Getandput.java
    branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invocation.java
    branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invoking.java
    branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Linker.java
    branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Newandmisc.java
    branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashMangoModel.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETSTATIC.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTSTATIC.java

Added Paths:
-----------
    branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/clinit/HasCommutingClinit.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/INVOKECLINIT.java

Removed Paths:
-------------
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java


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