[Javapathfinder-svn] SF.net SVN: javapathfinder:[1840] branches/mango/Mango

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

Revision: 1840
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1840&view=rev
Author:   frankrimlinger
Date:     2009-08-19 04:45:17 +0000 (Wed, 19 Aug 2009)

Log Message:
-----------
Punched in MangoFieldPeer per 1839.  However, what else is out there?  Who knows all the subtle places where the compiler generates instructions with literal class names?  To mitigate,  all calls to gov.nasa.jpf.jvm.bytecode.Instruction.getMethodInfo() from within buildFormaPeer() methods are now piped through MangoMethodPeer.getFormalPeer().  Undoubtedly, there are still other leaks to plug, but we must catch them as we may.  

To help avoid contamination of nominal jpf execution, we introduce MangoInterface.getFormalMethodInfo(), implemented within MangoInstruction and MangoInvokeInstruction.  Since all formal bytecode classes extend from these points, changed getMethodInfo() to getFormalMethodInfo() as appropriate

NEXT BUG: More leaks:
MethodInfo.getFullName, getDescriptor, etc.  All of these need to have the signature munged.  

Instruction.getInstructionName ditto

The reason this is a problem is like so, you have a class X that does not have a formal counterpart.  So Mango must model X.  But then you have a method y in X like so

String y(){}

so the MethodInfo is  for X.y()Ljava.lang.String;  and you don't automatically get munged signatures.  This happens automatically if the class is munged, but if not, you have to run the ball out on the ground. 

Modified Paths:
--------------
    branches/mango/Mango/Mango/src/mango/graph/data/ucon/UconData.java
    branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
    branches/mango/Mango/Mango/src/mango/module/instance/loop/model/LoopInstanceManager.java
    branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
    branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/MethodSym.java
    branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
    branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/Invocation.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoClassPeer.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoFormalInterface.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/GETSTATIC.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTSTATIC.java

Added Paths:
-----------
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoFieldPeer.java


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