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

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 422-6466

Revision: 1573
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1573&view=rev
Author:   frankrimlinger
Date:     2009-05-29 02:32:46 +0000 (Fri, 29 May 2009)

Log Message:
-----------
Finally figured out the ArrayBoundsOutOfRangeException weirdness.  Another case of taking stupid pills.  Certain instructions needed to access some private fields initialized by the getPeer method of the base Instruction class.  Not realizing these base classes were just COPIES of the original jpf classes, I didn't think I could change the field access to protected.  Instead, I just overloaded the fields and copied the getPeer methods to the extension instruction classes.  Well, this clearly will crash when the clinits try to execute in jpf mode, because the execute routine defers to the base class, whose overloaded fields now have not been initialized!

Deleted the unnecessary setPeer and field overloads, and changed base class access to protected.

Cleaned up a lot of code that was broken with the adoption of MangoInterface.  Scanner now scans all the canned clinits in jpf mode and then survives in SCAN mode until the first branch instruction backtrack.   instruction_2_vertices is being called again for the backtrack src, fix this.  The trouble is you want to set up the new edge, but not the src, which is already set up.

Modified Paths:
--------------
    branches/mango/MangoJPF/META-INF/MANIFEST.MF
    branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
    branches/mango/MangoJPF/Mango/src/mango/worker/engine/sym/AgentSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/engine/sym/ExpressionSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/edge/BackupEdge.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/edge/Edge.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/Graph.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/StrataGraph.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/EdgeSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/SuperVertexClassSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/reflection/StateSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/return_terminator/ReturnTerminatorSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/AssertionSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/SinkTerminatorSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperBlowUpSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperLoopSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperStrataSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/UconSym.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/AcyclicVertex.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/BackupVertex.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/LoopVertex.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/Vertex.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/BIPUSH.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DCONST.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FCONST.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INSTANCEOF.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/JSR.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/JSR_W.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LCONST.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MULTIANEWARRAY.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/RET.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/SIPUSH.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalInterface.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInterface.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BIPUSH.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCONST.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCONST.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INSTANCEOF.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR_W.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCONST.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SIPUSH.java
    branches/mango/MangoJPF/src/mango/intro/ApplicationWorkbenchAdvisor.java

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