Menu
▾
▴
javapathfinder-svn — source repository related messages (SVN)
You can subscribe to this list here.
| 2008 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(16) |
Jun
(42) |
Jul
(46) |
Aug
(48) |
Sep
(33) |
Oct
(26) |
Nov
(28) |
Dec
(38) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2009 |
Jan
(35) |
Feb
(80) |
Mar
(112) |
Apr
(108) |
May
(102) |
Jun
(126) |
Jul
(89) |
Aug
(82) |
Sep
(36) |
Oct
(7) |
Nov
(1) |
Dec
(4) |
| 2010 |
Jan
(87) |
Feb
|
Mar
(2) |
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: <fra...@us...> - 2009-05-27 20:31:00
|
Revision: 1559
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1559&view=rev
Author: frankrimlinger
Date: 2009-05-27 20:29:45 +0000 (Wed, 27 May 2009)
Log Message:
-----------
Initial import.
Added Paths:
-----------
branches/mango/legacy/ACL2/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-27 19:59:30
|
Revision: 1558
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1558&view=rev
Author: frankrimlinger
Date: 2009-05-27 19:58:56 +0000 (Wed, 27 May 2009)
Log Message:
-----------
Creating home for legacy code
Added Paths:
-----------
branches/mango/legacy/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-27 19:38:47
|
Revision: 1557
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1557&view=rev
Author: frankrimlinger
Date: 2009-05-27 19:37:47 +0000 (Wed, 27 May 2009)
Log Message:
-----------
oops... put project in the wrong place. I don't know how to delete this project but at least I can get rid of its content.
Added Paths:
-----------
mango/.project
Removed Paths:
-------------
mango/destiny3/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-27 19:25:03
|
Revision: 1556
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1556&view=rev
Author: frankrimlinger
Date: 2009-05-27 19:24:54 +0000 (Wed, 27 May 2009)
Log Message:
-----------
Initial import.
Added Paths:
-----------
mango/
mango/destiny3/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-27 02:14:29
|
Revision: 1555
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1555&view=rev
Author: frankrimlinger
Date: 2009-05-27 01:56:07 +0000 (Wed, 27 May 2009)
Log Message:
-----------
Rewired MangoFormalLanguage and MangoInstruction as interfaces to allow multiple inheritance paths through jpf Instruction class. This solved the problem of getting all the mango instructions hooked up with MangoInstructionFactory. BUT, unfortunately, the weird ArrayIndexOutOfBoundsException error was not fixed as expected.
Investigating... My guess now is that one of my bytecodes is corrupting state and this is throwing a curve ball for jpf.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/graph/data/graphic/CodeData.java
branches/mango/MangoJPF/Mango/src/mango/graph/data/ucon/UconData.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/msg/LoopDefinitionLocatorMsg.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/method/MethodDefinitionManager.java
branches/mango/MangoJPF/Mango/src/mango/module/instance/loop/model/LoopInstanceManager.java
branches/mango/MangoJPF/Mango/src/mango/source/agent/msg/SourceViewCreateRequestMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/edge/Edge.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.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/SinkTerminatorSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/ThrowSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/UconOSTerminatorSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/UconSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INVOKECG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/VirtualInvocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BeginningOfTime.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2B.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2C.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2S.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IINC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ILOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INEG.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/IOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IXOR.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/L2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCMP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC2_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOOKUPSWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITORENTER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITOREXIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NOP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/OSplace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SWAP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/InstructionSym.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalInterface.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInterface.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/InvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalLanguage.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-26 21:07:06
|
Revision: 1554
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1554&view=rev
Author: frankrimlinger
Date: 2009-05-26 21:07:04 +0000 (Tue, 26 May 2009)
Log Message:
-----------
Realized that the mango.scanner.bytecodeSythetic package was a really bad idea, because MangoInstructionFactory was not picking up all the bytecodes. This almost certainly led to the weirdness noted in previous comment. Moved these bytecodes to mango.scanner.bytecode.
However, still not out of the woods. The new problem is that the invocation bytecodes are extensions of gov.nasa.jpf.jvm.bytecode_mango_formal_language.InvokeInstruction instead of gov.nasa.jpf.jvm.bytecode.InvokeInstruction. This was done to insert the MangoInstruction class at a lower lever in the inheritance chain. But this is a non-starter because certain jpf routines, like MethodInfo.creatDirectCallStub cast to InvokeInstruction and won't accept any substitutions.
Well, even if you rewrote the jpf codebase with more interfaces, these kinds of problems always come up. My solution is to create MangoInterface and MangoFormalInterface, and have MangoInstruction and MangoFormalLanguage implement these interfaces. I am then free to write other implementations and put them at strategic points in the inheritance chain so that I don't cut off the classes that jpf wants to be able to see. This regrettably involves some code duplication but it is the path of least resistance.
TRICK: when something is given as a MangoInterface, and I need it as a jpf Instruction, just call the asInstruction() method. This is implemented with the following weird code:
Instruction asInstruction(){
return this;
}
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/BuildAbstractUcon.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEngine.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_scanner_ScannerMJI.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.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
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AbstractUconPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BadPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BeginningOfTime.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKETARGET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/OSplace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SyntheticInstruction.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-26 04:01:37
|
Revision: 1553
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1553&view=rev
Author: frankrimlinger
Date: 2009-05-26 04:01:29 +0000 (Tue, 26 May 2009)
Log Message:
-----------
Reinstated entrypoints window. This will allow testing to proceed without any hot-wiring. It will also allow for posting and viewing of control flow graphs, necessary for debugging if nothing else.
Working on strange ArrayIndexOutOfBoundsExecutiveException issue. This happens early on when java.lang.Integer.<clinit> fires. Was not happening before...
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/tree/agent/FolderViewAgent.java
branches/mango/MangoJPF/Mango/src/mango/tree/agent/TreeViewAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalLanguage.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/AbstractUconPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/BadPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/OSplace.java
branches/mango/MangoJPF/plugin.xml
branches/mango/MangoJPF/src/mango/intro/Application.java
branches/mango/MangoJPF/src/mango/intro/ApplicationWorkbenchAdvisor.java
branches/mango/MangoJPF/src/mango/intro/Perspective.java
Added Paths:
-----------
branches/mango/MangoJPF/src/mango/views/GlobalViewWindow.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-25 18:55:39
|
Revision: 1552
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1552&view=rev
Author: frankrimlinger
Date: 2009-05-25 18:55:30 +0000 (Mon, 25 May 2009)
Log Message:
-----------
package cleanup
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-25 18:47:25
|
Revision: 1551
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1551&view=rev
Author: frankrimlinger
Date: 2009-05-25 18:47:13 +0000 (Mon, 25 May 2009)
Log Message:
-----------
javapathfinder-mango-bridge port is now complete. The plan is now to get phase1 working on itsAWrap, and then hot-wire the target method to itsAWrap.clear() and abstract this method. Once this is working, punch in the target select algorithm and port the rest of the baseline tests to MangoJPF. At this point, throw out the Mango project, and rename MangoJPF to Mango. Then copy to MangoBaseline and forge ahead into terra incognita.
The goals for the project are
1. Eliminate stratification from phase2.
2. Add a REWRITER phase to the scanner bytecodes, so that they can be used for rewriting. To greatly reduce load and complexity on the rewriter, DO NOT bind context prior to rewriting. Since the results will be deployed as jpf state-along-a-path, context can be bound after composition occurs. Note this will not completely eliminate rewriting with context, as certain things, in particular garbage collection, require context to perform address comparisons. But the horrible issue of "context resolution" which occurs during composition can be eliminated.
3. Drive the rewriter automatically along the paths, stopping only when translation fails and the user must add new definitions. Store traversed path for each case in the rulebase so jpf can restart cold.
4. And finally, with all this in place, it will be possible to use the backtracking mechanism to produce factorizations for invariant detection. These factorizations should be baked into the cake from step two onward and stored persistently, even as they are now in a very limited and clumsy way.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHash.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ReturnPointLink.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISTORE.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/LASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOOKUPSWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITORENTER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITOREXIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NOP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RUNSTART.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SWAP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Branching.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Getandput.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/Loading.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/LogicAndIntegerInc.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Newandmisc.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/PopDupSwap.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Pushing.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Return.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Storing.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/TypeCasting.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeNames.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-25 01:24:13
|
Revision: 1550
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1550&view=rev
Author: frankrimlinger
Date: 2009-05-25 01:24:10 +0000 (Mon, 25 May 2009)
Log Message:
-----------
many bytecodes ported to bridge, getting close.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Loading.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/LogicAndIntegerInc.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Newandmisc.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IINC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ILOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INSTANCEOF.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC2_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/DFLsyntax_how_clinits_work.rtf
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/DFLsyntax_how_clinits_work.rtf
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-24 05:06:55
|
Revision: 1549
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1549&view=rev
Author: frankrimlinger
Date: 2009-05-24 05:06:46 +0000 (Sun, 24 May 2009)
Log Message:
-----------
All adapter code completed. All invocation instructions ported to bridge.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/BuildAbstractUcon.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/Checkcast.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeException.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeMethod.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeException.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeMethod.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/IsAssignmentCompatible.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/IsInterface.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/IsSuperClass.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/TranslateValueH.java
branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/linearArithmetic/ArithmeticLocalVar.java
branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/symbols/InstructionSymReq.java
branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/symbols/InvocationSymReq.java
branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/typing/ArithmeticFieldType.java
branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/typing/ArithmeticValue.java
branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/typing/IntegralArrayFieldType.java
branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/typing/IntegralFieldType.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Getandput.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/engine/hash/Hitem.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashCoreParser.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/CheckCast_getValueAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/InstanceOfAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/IsAssignmentCompatibleAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapTracer.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/FrameModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/HeapModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/ContextBinderSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/executable/FrameSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/WorkerCommand.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECG.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/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/INVOKECLINIT.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Package.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ReturnPointLink.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/ClassSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/InstructionSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/InvocationSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/JclassSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/JfieldSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/JmethodSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/JnonclassSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/ReturnPointLinkSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/notes on access.rtf
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/trick heap stuff.rtf
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invocation.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Package.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-24 01:27:34
|
Revision: 1548
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1548&view=rev
Author: frankrimlinger
Date: 2009-05-24 01:27:20 +0000 (Sun, 24 May 2009)
Log Message:
-----------
Realized that required jar plugins (other than those in the standard Eclipse distribution) were not physically present in the MangoJPF project. This is undesirable, so copied them in.
Port of method and class adapter utilities complete. But there are issues...
The javadoc for MethodInfo.loadLocalVariableNames is a little misleading. You can't really get "the local variable names for the method" because the variable name is dependent on the pc. So instead of calling the bcel method LocalVariableTable.getLocalVariableTable(), which presumably is some approximation, call the more precise LocalVariableTable.getLocalVariable(index,pc).
It is possible that the javadoc predates the more precise bcel method. That is the charming thing about documentation.
For the record, the old class parser getLocalVarName() contains the following statement:
This is very disturbing, but the local variable appears to be
start_pc-1 to start_pc+length-1 inclusive. Don't know why we are off.
Will this chicken come home to roost?
Modified Paths:
--------------
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
Added Paths:
-----------
branches/mango/MangoJPF/plugins/
branches/mango/MangoJPF/plugins/Mango_Jars_1.0.0.jar
branches/mango/MangoJPF/plugins/javapathfinder_trunk_extensions_symbc_lib_update1_1.0.0.jar
branches/mango/MangoJPF/plugins/jpf_trunk_build_tools_lib_1.0.0.jar
branches/mango/MangoJPF/plugins/jpf_trunk_extensions_concolic_1.0.0.jar
branches/mango/MangoJPF/plugins/jpf_trunk_extensions_symbc_1.0.0.jar
branches/mango/MangoJPF/plugins/jpf_trunk_extensions_symbolic_1.0.0.jar
branches/mango/MangoJPF/plugins/jpf_trunk_lib_1.0.0.jar
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-23 22:03:28
|
Revision: 1547
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1547&view=rev
Author: frankrimlinger
Date: 2009-05-23 22:03:19 +0000 (Sat, 23 May 2009)
Log Message:
-----------
Initial port of BackupAlg complete. The source code graph was dropped because the code was too convoluted to port. Probably this won't be resurrected until it comes for free with the final port to the workbench. For now, it remains to port the rest of the formal instruction peers to the bridge, and to write the required class and method adapters. Then testing and on to the new design for phase2.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/core/RuleResourceManager.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invocation.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/sym/ExpressionSym.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/sym/graphic/MethodSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/ThrowSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.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/CallVertex.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/MethodVertex.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/SuperCpnVertex.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/SuperVertex.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/Vertex.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
Added Paths:
-----------
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-23 18:31:06
|
Revision: 1546
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1546&view=rev
Author: frankrimlinger
Date: 2009-05-23 18:30:58 +0000 (Sat, 23 May 2009)
Log Message:
-----------
BackupAlg port almost complete.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-23 03:15:38
|
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.
|
|
From: <fra...@us...> - 2009-05-22 17:44:28
|
Revision: 1544
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1544&view=rev
Author: frankrimlinger
Date: 2009-05-22 17:44:18 +0000 (Fri, 22 May 2009)
Log Message:
-----------
The instructions that potentially fire clinits are called the clinit-4 instructions, defined in JVM 2nd ed, new, getstatic, putstatic, invokestatic.
The constraints on the problem are like so: if a class has only final data, then it is easy and cheap to punch in these values with rewrite rules. So the clinit for such a class can be ignored. On the other hand, if a class has non final data, then the clinit must fire in an order dependent way with respect to the other clinits that must fire.
Mango detects which clinits must fire by observing, for each modelled class which contains a clinit, if that clinit contains a clinit-4 instruction. Such modelled classes are said to have "commuting clinits".
OK, any clinit-4 instruction which potentially may fire a commuting clinit must be preceded by a conditional clinit invocation. This condition is simply that the clinit is at the "beginning of time". The idea is that these conditional clinit invocations commute backwards through the flow control and bunch up at the beginning of time, where they then can fire in order. As a clinit fires, it propagates the beginning of time property to its immediate successor, who then can also fire.
There are two issues here, performance and soundness. The performance issue is like so: in the old two pass phase1, it was possible to catalogue the classes with commuting clinits during the first pass, so that formal state transition built in the second pass would only have to add the conditional clinit logic to the clinit-4's referencing commuting clinits. However, now that we only have one pass, we are still building the catalogue when the decision of whether or not to add conditional logic comes up. We could cheat, and just inspect each class info for evidence of non-final data, but I think this is fraught with danger. Instead, just go ahead and punch in commuting clinit logic for EVERY clinit-4 instruction. However, enhance the condition to check the catalogue at evaluation time. By this means, the unnecessary conditional invocations will evaporate just-in-time.
As for soundness, the BIG problem is that the survey is only over mango modelled classes, so the procedure is inherently unsound: a clinit-4 that fires an unmodelled commuting clinit will not be modelled correctly. The outstanding example of this is java.lang.System, whose clinit must fire to produce the popular static field java.lang.System.out.
Soundness may be addressed as follows: assume that every mango native method presents an ordered list of clinits which must potentially fire prior to invocation. Now add the invocation instructions (invokestatic, invokevirtual, invokespecial, invokeinterface) to the new invoke-4 list. Now for each invoke-4 instruction, arrange so that the branch condition to a mango native method is preceded by the indicated sequence of potential clinit invocatons. These invocations may now commute back to the beginning of the target method.
Ok, its a little more complicated than that, because the target method may have several cases, so for each case, there must be an ordered list of clinits, but the basic idea is there. It would then be necessary to store these lists in the rulebase, as well as abstracted clinit functionality.
So, even if there was never a beginning of time, there would still be a record of what clinits could affect a given method, and this is good information for informed reasoning about the situation. Notice we can't actually fire the clinits unless we can make some kind of temporal order invariance assumption.
Its hard to imagine what traction a meta-theory for such assumptions could achieve. For example, after java.lang.out is created, it can be reassigned at will to print to this or print to that, so what can an arbitrary method actually "know" about java.lang.out. So at the end of the day, you still just come back to reasoning about abstractions. I guess that the point is, at the very least, you have an inventory of things that need to be abstracted.
This is a scalable idea that really should be implemented some day. For now, punt on soundness, and just say that clinits are "soundness ready".
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-22 05:20:36
|
Revision: 1543
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1543&view=rev
Author: frankrimlinger
Date: 2009-05-22 05:20:26 +0000 (Fri, 22 May 2009)
Log Message:
-----------
Stated porting the so-called "commuting clinits", which are classes non-final static fields. The reason they are called commuting is that their invocation may commute backwards past all instructions other that InvokeClinit, back to the beginning of time, if any. The only issue is to get them to fire in the correct order. In practice this scheme is almost never used, because it is just easier to reason more abstractly about such data. In particular, final stuff is much easier to punch in with rewrite rules. But having come this far, might as well support commuting clinits.
There is a big hole in all this, in that we don't know for unmodelled methods what clinits they potentially may fire and in what order. To really do this right, we need to store this information in the rulebase. This is too much work for now, but must be done some day. Or not. Maybe this idea is just lousy.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Linker.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEngine.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-22 03:42:24
|
Revision: 1542
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1542&view=rev
Author: frankrimlinger
Date: 2009-05-22 03:42:16 +0000 (Fri, 22 May 2009)
Log Message:
-----------
completed port of BackupAlg.method_2_vertices. This involved untangling some very ancient and obscure code for setting up clinit invocations and defining the beginning of time. A hook has been left in the Worker to designate a beginning of time method (or methods, pretty agnostic about this.) However, not bothering to back this all the way up to preferences for now because this is a little used feature. Also used very nice support in jpf Instruction class to set up SourceLineData objects.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/graph/data/graphic/SourceLineData.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.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/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalLanguage.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/BeginningOfTime.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-21 15:03:01
|
Revision: 1541
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1541&view=rev
Author: frankrimlinger
Date: 2009-05-21 15:02:53 +0000 (Thu, 21 May 2009)
Log Message:
-----------
All edge building logic has been ported. This is by far the trickiest step, so apparently the one-pass strategy is going to pan out. It remains to
1. transfer the required functionality in the old ClassParser.Instruction to MangoInstruction to complete the port of the BackupAlg,
2. port the required functionlity from the old ClassParser Method and ClassModel classes to MethodUtil and ClassUtil, resp,
3. finish porting the rest of the mango formal logic to the bridge bytecodes.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/edge/Edge.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-21 04:29:56
|
Revision: 1540
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1540&view=rev
Author: frankrimlinger
Date: 2009-05-21 04:29:42 +0000 (Thu, 21 May 2009)
Log Message:
-----------
Lots of EZ bridge cleanup. Also finished bridge port of ExceptionHandlerUtil.createACatchHandlerBranching. This is one fiendish piece of work. Ran into a little snag in that MethodInfo drops the ball concerning CodeExceptions for finally clauses. So I had to dig into bcel world to get this info.
Modified Paths:
--------------
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/return_terminator/ReturnTerminatorSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/SinkTerminatorSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/ThrowSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/AbstractUconSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/UconOSTerminatorSym.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/CallVertex.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/MethodVertex.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/SuperCpnVertex.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/SuperVertex.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/Vertex.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWCREATOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/AbstractUconPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/BadPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/INVOKETARGET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/OSplace.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/SyntheticInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-05-20 22:15:17
|
Revision: 1539
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1539&view=rev
Author: staats
Date: 2009-05-20 22:15:05 +0000 (Wed, 20 May 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/SymbolicSearchListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-20 21:23:29
|
Revision: 1538
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1538&view=rev
Author: frankrimlinger
Date: 2009-05-20 21:23:18 +0000 (Wed, 20 May 2009)
Log Message:
-----------
Refactored MangoInstruction and MangoFormalLanguage, as these really belong in the mango.scanner package.
Some delicate surgery on the phase1 code to hook it up properly to updateMangoModel(). Some code has been peeled away in a routine called buildSpecialEdges(), which handles some invocation related issues. The MangoInstruction.createXXXBranch methods are now just adaptors for BackupAlg.buildEdge().
It remains just to clean up and accommodate the MangoInstruction proxy for the Vertex dest field of and Edge.
You must hot wire the rest of the automation driver for a specific target (i.e. itsAWrap.clear()) and test before proceeding to adapt phaseII to the new design. There are sure to be phase1 buggies to deal with. You don't want to debug phase1 and phase2 simultaneously.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/graph/data/graphic/CodeData.java
branches/mango/MangoJPF/Mango/src/mango/graph/data/ucon/UconData.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/msg/LoopDefinitionLocatorMsg.java
branches/mango/MangoJPF/Mango/src/mango/module/instance/loop/model/LoopInstanceManager.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/InvocationEdgeSym.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/SinkTerminatorSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/UconOSTerminatorSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ArrayInstruction.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/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/D2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/D2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/D2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DCMPL.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/DDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP2_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP2_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/F2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/F2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/F2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FCMPL.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/FDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FieldInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2B.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2C.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2S.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IINC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INEG.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/INVOKECG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ISHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ISHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ISUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IfInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/InvokeInstruction.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/L2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/L2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/L2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LCMP.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/LDC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LDC2_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LSHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LocalVariableInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LockInstruction.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/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/NOP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/POP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/POP2.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/RUNSTART.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ReturnInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/SIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/SWAP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/SwitchInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2B.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2C.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2S.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCMP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWCREATOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/AbstractUconPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/BadPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/OSplace.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalLanguage.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MangoFormalLanguage.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MangoInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-20 14:22:58
|
Revision: 1537
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1537&view=rev
Author: frankrimlinger
Date: 2009-05-20 14:22:26 +0000 (Wed, 20 May 2009)
Log Message:
-----------
Have finally settled on the code for Mango.updateMangoModel(). This will drive the rest of the bridge port.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/graph/Graph2DViewManager.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-19 18:44:40
|
Revision: 1536
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1536&view=rev
Author: frankrimlinger
Date: 2009-05-19 18:44:26 +0000 (Tue, 19 May 2009)
Log Message:
-----------
Introduced hidden object proxies for ClassInfo and MethodInfo. This competes the bridge port for all code except the BackupAlg, the mango bytecodes, and the MethodUtil and ClassUtil adapters. Hopefully the basic patterns for the port have now settled down.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/WorkerCommand.java
Added Paths:
-----------
branches/mango/MangoJPF/Mango/src/mango/enterprise/model/ClassProxy.java
branches/mango/MangoJPF/Mango/src/mango/enterprise/model/ClassProxyPersistenceDelegate.java
branches/mango/MangoJPF/Mango/src/mango/enterprise/model/MethodProxy.java
branches/mango/MangoJPF/Mango/src/mango/enterprise/model/MethodProxyPersistenceDelegate.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-19 16:03:50
|
Revision: 1535
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1535&view=rev
Author: frankrimlinger
Date: 2009-05-19 16:03:40 +0000 (Tue, 19 May 2009)
Log Message:
-----------
Cleanup for interpolated MangoInstruction class essentially complete, but a new issue has been identified. Unlike Instruction, there is no interpolating MethodInfo. So you have to package a MethodInfo in a MethodProxy extension of HiddenObject for the worker id system. See WorkerCommand class.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/graph/data/graphic/CodeData.java
branches/mango/MangoJPF/Mango/src/mango/graph/data/ucon/UconData.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/msg/LoopDefinitionLocatorMsg.java
branches/mango/MangoJPF/Mango/src/mango/module/instance/loop/model/LoopInstanceManager.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.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/SinkTerminatorSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/UconOSTerminatorSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/SuperCpnVertex.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapTracer.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/LocalItemModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/OpItemModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/StackModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/LineNumberSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/ContextBinderSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/executable/FrameSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/executable/LocalVarSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/LocalVarConditionalEquivalenceAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/model/InvariantModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/WorkerCommand.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
