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-19 14:16:49
|
Revision: 1534
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1534&view=rev
Author: frankrimlinger
Date: 2009-05-19 14:16:43 +0000 (Tue, 19 May 2009)
Log Message:
-----------
MangoInstruction interpolation cleanup in progress.
Modified Paths:
--------------
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/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/INVOKETARGET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/OSplace.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 05:57:50
|
Revision: 1533
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1533&view=rev
Author: frankrimlinger
Date: 2009-05-19 05:57:37 +0000 (Tue, 19 May 2009)
Log Message:
-----------
Interpolated the MangoInstruction class, a virtual version of InstructionUtil, between the jpf Instruction class and its direct extensions. This will allow the mango adapter code to take advantage of the jpf Instruction functionality. Also interpolated MangoFormalLanguage as an abstract class between MangoInstruction and Instruction, as this gives some technical advantages.
You must now finish eliminated all the stale code in the ported formal bytecodes, as well as references to obsolete BranchUtil and InstructionUtil, which are now folded into virtual methods of MangoInstruction.
Background:
The decision to extend my bytecodes from the jpf bytecodes causes some trouble. The static adapter methods of InstructionUtil are growing in number and complexity, and have become an unacceptable violation of object oriented programming practice. Evidently I must now adapt a copy of package gov.nasa.jpf.jvm.bytecode as special purpose code that does not belong in the jpf kernel. This ugly duplication of code is the price paid for the elegance and simplicity of the MangoTargetLauncher. I did make attempts to extend my bytecodes directly from Instruction, but this led to lots of little and not so little problems. Abandoning jpf Instruction altogether is not an option, because mango now depends on this functionality.
So for now, I just duplicate and adapt the gov.nasa.jpf.jvm.bytecode. If there is a better solution, well, let it come as it may.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.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/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/engine/hash/Hitem.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEngine.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeNames.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/InstanceOfAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.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/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/SuperCpnSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.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/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/bytecode/AALOAD.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/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.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/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/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/DRETURN.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/FRETURN.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/INVOKECG.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/IRETURN.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/LRETURN.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/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/RETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RUNSTART.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/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/Mango/src/mango/worker/byteCodeModel/Package.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/AASTORE.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/ALOAD.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/ARETURN.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/ASTORE.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/ArrayLoadInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ArrayStoreInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/BASTORE.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/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/CASTORE.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/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DASTORE.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/DLOAD.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/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DSTORE.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/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FASTORE.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/FLOAD.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/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FSTORE.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/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/GETSTATIC.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/GOTO_W.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/IALOAD.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/IASTORE.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/IFEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ACMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ACMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPNE.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/ILOAD.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/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INVOKEINTERFACE.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/INVOKEVIRTUAL.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/IRETURN.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/ISTORE.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/InstanceFieldInstruction.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/LALOAD.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/LASTORE.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/LDC_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/LLOAD.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/LOOKUPSWITCH.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/LRETURN.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/LSTORE.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/LongArrayLoadInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LongArrayStoreInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MONITORENTER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MONITOREXIT.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/MangoFormalLanguage.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MangoInstruction.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/PUTFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/PUTSTATIC.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/RETURN.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/SALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/SASTORE.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/StaticFieldInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/StoreInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/SwitchInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/TABLESWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/VariableAccessor.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/VirtualInvocation.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InstructionUtil.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: <pcm...@us...> - 2009-05-18 21:47:19
|
Revision: 1532
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1532&view=rev
Author: pcmehlitz
Date: 2009-05-18 21:47:10 +0000 (Mon, 18 May 2009)
Log Message:
-----------
* IMPORTANT - Config initialization is now flattened, and values are expanded upon entry. This means that clients that need to process raw values (including var names) would not work anymore, and the order of symbolic entries does now matter (processed sequentially). On the other hand, we didn't have such clients in the distrib, but lots of clients didn't use getExpandedXX() instead of getXX(), so this is going to fix a lot of config problems.
Note that we can also do recursive init now, like in
vm.classpath=my/path,${vm.classpath}
the old '+=' append still works too, but with the same restrictions in property files (no blanks between key and '+') - we should use our own parsing at some point.
* since there is no Config.defaults anymore, the publishers had to be updated. Decided against throwing a Config.Exception if defaults.properties is not found, since a lot of clients do not handle exceptions during Config init, and some of them don't even need default.properties
Modified Paths:
--------------
trunk/examples/launch/basic-random.launch
trunk/examples/launch/conc-1-RA.launch
trunk/extensions/cv/src/gov/nasa/jpf/cv/SCSafetyListener.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SCInspector.java
trunk/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
trunk/src/gov/nasa/jpf/report/HTMLPublisher.java
trunk/src/gov/nasa/jpf/report/XMLPublisher.java
trunk/src/gov/nasa/jpf/tools/JavaJPF.java
trunk/src/gov/nasa/jpf/util/Inspector.java
trunk/test/gov/nasa/jpf/jvm/TestJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-18 18:47:25
|
Revision: 1531
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1531&view=rev
Author: frankrimlinger
Date: 2009-05-18 18:47:16 +0000 (Mon, 18 May 2009)
Log Message:
-----------
bridge port of type casting and branching instructions.
Modified 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/Loading.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Newandmisc.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/bytecode cheat.txt
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/DCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPL.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/FCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPL.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/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/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/LCMP.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-18 16:55:16
|
Revision: 1530
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1530&view=rev
Author: frankrimlinger
Date: 2009-05-18 16:55:05 +0000 (Mon, 18 May 2009)
Log Message:
-----------
update
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Getandput.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-18 04:39:08
|
Revision: 1529
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1529&view=rev
Author: frankrimlinger
Date: 2009-05-18 04:38:59 +0000 (Mon, 18 May 2009)
Log Message:
-----------
Bridge port for lots of broken code
Added MethodUtil, ClassUtil classes. A porting pattern is emerging. Except in simple cases where direct translation is possible, add an adapter method to the appropriate bridge utility, rather than attempt an in-situ fix. This will localize the porting issues in the util classes.
Added a concept of "mangoNative_packages" to indicate the code that will not be modelled by the backup algorithm. This is the latest reincarnation of the "library" concept. It is interesting that the concept of "native" is now three levels deep.
porting createBadBranch, the issue is that we need to determine if we already branched to the badBranch from this vertex. So we need to know how to query the src Instruction to get its vertex to examine its outgoing edges.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/graph/data/graphic/CodeData.java
branches/mango/MangoJPF/Mango/src/mango/graph/data/graphic/MethodData.java
branches/mango/MangoJPF/Mango/src/mango/graph/data/supervertex/SuperVertexData.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/definition/method/msg/CreateMethodStubMsg.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/method/msg/MethodDefinitionLocatorMsg.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/RestoreContextMsg.java
branches/mango/MangoJPF/Mango/src/mango/module/instance/loop/model/LoopInstanceManager.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/coreRewriter/classModel/Is_class_loadable.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/clinit/CallThisClinit.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/clinit/ComposePrependedClinits.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/AmbientLocal.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/source/agent/msg/SourceViewCreateRequestMsg.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/hash/symbolHash/SymbolHashCoreParser.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEngine.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/rule/AssumeEquivRule.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/CheckCast_getValueAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/IsAssignmentCompatibleAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/MethodSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/HeapModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/model/HitemUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InstructionUtil.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/src/mango/intro/ConfigurationDetails.java
branches/mango/MangoJPF/src/mango/intro/LoginDialog.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.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: <st...@us...> - 2009-05-17 17:20:24
|
Revision: 1528
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1528&view=rev
Author: staats
Date: 2009-05-17 17:20:16 +0000 (Sun, 17 May 2009)
Log Message:
-----------
Added Paths:
-----------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/
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-17 05:17:55
|
Revision: 1527
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1527&view=rev
Author: frankrimlinger
Date: 2009-05-17 05:17:30 +0000 (Sun, 17 May 2009)
Log Message:
-----------
Ported the Invocation class. This class generates the formal branch conditions for invocations, now based on the CodeSurvey and the bridge classes BranchUtil and ExceptionHandlerUtil. Also introduced bridge class InstructionUtil to help out with generating various names using existing mango api.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/module/definition/method/MethodDefinitionManager.java
branches/mango/MangoJPF/Mango/src/mango/source/agent/msg/SourceViewCreateRequestMsg.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/byteCodeModel/Invoking.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/InstructionSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/InvocationSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JclassSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JfieldSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JmethodSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JnonclassSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashCoreParser.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.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/InvocationUtil.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
Added Paths:
-----------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/ClassSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InstructionUtil.java
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/ClassSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/ReturnPointLinkSym.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-16 23:54:32
|
Revision: 1526
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1526&view=rev
Author: frankrimlinger
Date: 2009-05-16 23:54:14 +0000 (Sat, 16 May 2009)
Log Message:
-----------
port of phase1 in progress. The old java model symbols have been reinstated. It is too early to try and phase them out. Instead, they must be ported so that they host the underlying jpf classes.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/core/CoreRule.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/BuildAbstractUcon.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/mangoModel/backupAlg/BackupAlg.java
Added Paths:
-----------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/ClassSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/InstructionSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/InvocationSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JclassSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JfieldSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JmethodSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JnonclassSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/ReturnPointLinkSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/notes on access.rtf
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/trick heap stuff.rtf
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/AbstractUconMethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BadMethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/FakeMethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/OSmethod.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
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-16 19:56:14
|
Revision: 1525
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1525&view=rev
Author: frankrimlinger
Date: 2009-05-16 19:56:04 +0000 (Sat, 16 May 2009)
Log Message:
-----------
details of BackupAlg.phase1 migration.
Prior to calling the SCANNER, the BackupAlg instance is created. In particular, the Instructions BadPlace, AbstractUconPlace, and OSplace are set up. I have decided not to use all caps for synthetic instruction classes anymore.
The solution for one-pass graph construction is to use MethodInfo and Instruction objects as proxies for src and destination vertices in the call and total graphs, respectively. This allows the old Branch class to be retired, as edges are created immediately.
Since updateTotalGraph is really doing a lot more than just the total graph, it is now called updateMangoModel
So updateMangoModel is now only passed the src vertex, and provides one-stop shopping for all instructions. in particular, the Mango routines processReturn, processThrow, and processNativeCall now just bounce to updateTotalGraph
The SCANNER pass must accomplish the equivalent functionality of BackupAlg.phaseI.CreateVertices() and LinkVertices(). So Mango. updateMangoModel does the following, only for src vertex.
1. if necessary, call BackupAlg.Method_2_vertices for the corresponding MethodInfo
2. call BackupAlg.instruction_2_vertices() for the src vertex, which becomes the peerVertex member of the src instruction.
3. call buildFormalPeer, creating the state transition and exit edges. Because we create the edges immediately, there is no need for a link phase. Instead of instantiating branches, just fold in the equivalent functionality of BackupAlg.instruction_link and BackupAlg.branch_link.
If all goes well, the graphs we create should be acceptable input for phase2. But you will have to hotwire the 2d graph command so they can at least be inspected.
Modified Paths:
--------------
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/msg/NewWorkerMsg.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/bytecode/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO_W.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/RET.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-15 18:54:50
|
Revision: 1524
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1524&view=rev
Author: frankrimlinger
Date: 2009-05-15 18:54:42 +0000 (Fri, 15 May 2009)
Log Message:
-----------
Detailed work on bridge port of exception handling in progress. But first, need to figure out exactly how the contruction of the total graph is to proceed. The first point is that the intermediate Branch class is to be completely eliminated. There will be a 1-1 binding between Instructions and total graph vertices. Instead of creating branches, just immediately punch in the corresponding edge between vertices. This amounts to wiring in the correct phase1 code at the moment branches are currently created, and creating total vertex peers for the instructions on demand. To avoid calling buildFormalPeer more than once, define an Hitem formalPeer member which represents the state transition. That way we can grab it when necessary and also know when it has already been created.
Start by defining exactly what happens when jpf calls the mango hooks.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/javaModel/jvmSyntax/attributes/Code_attribute.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.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/INVOKETARGET.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-15 06:15:59
|
Revision: 1523
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1523&view=rev
Author: frankrimlinger
Date: 2009-05-15 06:15:50 +0000 (Fri, 15 May 2009)
Log Message:
-----------
Completed migration of ArithmeticOp bytecodes to the bridge. Rough-out of branching for nominal and exceptional cases. Applied regular expressions to all worker bytecodes to prepare for migration.
Modified 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/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/SymbolHashOpcodeSyms.java
branches/mango/MangoJPF/bytecode cheat.txt
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DADD.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/FADD.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/IADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.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/LADD.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
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchUtil.java
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/ArithmeticOp.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <wv...@us...> - 2009-05-14 22:37:10
|
Revision: 1522
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1522&view=rev
Author: wvisser
Date: 2009-05-14 22:37:02 +0000 (Thu, 14 May 2009)
Log Message:
-----------
Example used for HAMPI
Added Paths:
-----------
trunk/extensions/symbc/examples/StringTest2.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <wv...@us...> - 2009-05-14 22:25:24
|
Revision: 1521
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1521&view=rev
Author: wvisser
Date: 2009-05-14 22:25:14 +0000 (Thu, 14 May 2009)
Log Message:
-----------
so file required for HAMPI
Added Paths:
-----------
trunk/extensions/symbc/lib/libSTPJNI.so
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2009-05-14 22:09:08
|
Revision: 1520
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1520&view=rev
Author: pcorina
Date: 2009-05-14 22:08:54 +0000 (Thu, 14 May 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/env/jpf/java/lang/Math.java
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/symbc/JPF_java_lang_Math.java
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/symbc/JPF_java_lang_String.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeMathIAsolver.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestInvokeSTATICandVIRTUAL.java
Added Paths:
-----------
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestTermination.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2009-05-14 22:04:00
|
Revision: 1519
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1519&view=rev
Author: pcorina
Date: 2009-05-14 22:03:51 +0000 (Thu, 14 May 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/.classpath
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-14 21:05:37
|
Revision: 1518
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1518&view=rev
Author: frankrimlinger
Date: 2009-05-14 21:05:17 +0000 (Thu, 14 May 2009)
Log Message:
-----------
port of exception handler code to javapathfinder-mango-bridge in progress
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.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
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/
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/INVOKETARGET.java
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/INVOKETARGET.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2009-05-14 18:55:34
|
Revision: 1517
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1517&view=rev
Author: pcorina
Date: 2009-05-14 18:55:19 +0000 (Thu, 14 May 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsGeneral.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsHAMPI.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-14 18:55:12
|
Revision: 1516
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1516&view=rev
Author: frankrimlinger
Date: 2009-05-14 18:54:50 +0000 (Thu, 14 May 2009)
Log Message:
-----------
package cleanup
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/jvmSyntax/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-14 18:51:47
|
Revision: 1515
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1515&view=rev
Author: frankrimlinger
Date: 2009-05-14 18:51:32 +0000 (Thu, 14 May 2009)
Log Message:
-----------
Created a new set of regular expressions for the formal bytecode port. These have all been tested on the port to AALOAD. Created ExceptionHandlerUtil to take over generation of the creation of flow control for exceptions. This code scattered around but a lot of it is in the obsolete CodeAttribute class. The strategy is to create a mapping of MethodInfo --> HandlerInfo, where HandlerInfo is a private inner class of ExceptionHandlerUtil. This map will allow ExceptionHandlerUtil to service the various requests for ExceptionHandler support.
Also need to create a few synthetic Instructions to support throwing exception. The goal is just to replicate the existing control flow for thrown exceptions, generated as the scanner spins out it data.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalLanguage.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
Added Paths:
-----------
branches/mango/MangoJPF/bytecode cheat.txt
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <wv...@us...> - 2009-05-14 16:16:38
|
Revision: 1514
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1514&view=rev
Author: wvisser
Date: 2009-05-14 16:16:30 +0000 (Thu, 14 May 2009)
Log Message:
-----------
jar files for hampi
Added Paths:
-----------
trunk/extensions/symbc/lib/STPJNI.jar
trunk/extensions/symbc/lib/hampi.jar
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-14 15:26:09
|
Revision: 1513
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1513&view=rev
Author: frankrimlinger
Date: 2009-05-14 15:24:37 +0000 (Thu, 14 May 2009)
Log Message:
-----------
Deleted obsolete hashtables from Mango class.
Deleted the following subpackages of mango.worker.javaModel:
classParser
errorModel
jmvSyntax.attributes
jvmSytax.helper_classes
linkingModel
sym
Needless to say, this severely traumatized the mango codebase. The equivalent jpf functionality must now be wired in.
Since the only remaining subpackage is byteCodeModel, it is now moved to mango.worker.byteCodeModel. This package maps bytecodes to their formal counterparts. The first order of business is to parcel this code out into the mango.scanner.bytecode classes. To this end, these classes will implement the new MangoFormalLanguage interface.
For the purpose of this port, the deleted classes
mango.worker.javaModel.classParser.Field
mango.worker.javaModel.classParser.Instruction
mango.worker.javaModel.classParser.Method
mango.worker.javaModel.classParser.ClassModel
become
gov.nasa.jpf.jvm.FieldInfo
gov.nasa.jpf.jvm.bytecode.Instruction
gov.nasa.jpf.jvm.MethodInfo
gov.nasa.jpf.jvm.ClassInfo
This transformation will effectively bind mango flow control to jpf simulation.
Hopefully the symbol counterparts of the mango classes can be totally eliminated now, but if not, they will be rewritten from scratch.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/BuildAbstractUcon.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/Is_class_loadable.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/clinit/ComposePrependedClinits.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/ArithmeticOp.java
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/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/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/events/LocalMessage.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHash.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/FrameModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/executable/FrameSym.java
Added Paths:
-----------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalLanguage.java
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/byteCodeModel/
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/errorModel/
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/jvmSyntax/attributes/
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/jvmSyntax/helper_classes/
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/linkingModel/
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/sym/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-14 13:12:49
|
Revision: 1512
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1512&view=rev
Author: frankrimlinger
Date: 2009-05-14 13:12:35 +0000 (Thu, 14 May 2009)
Log Message:
-----------
Successful test of automated startup through SCANNER. Prior to coding mango scanner hooks, need to build map MethodInfo<-->Rulebase Tier. Observer that not every MethodInfo will bind to a Tier,and not every Tier will bind to a MethodInfo. This map should be built as the first step of NewWorkerMsg, prior to SCANNER invocation. But first, clean out all the obsolete Worker and Mango front-end objects and code, especially the hashtables that are no longer needed.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-05-13 23:38:55
|
Revision: 1511
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1511&view=rev
Author: pcmehlitz
Date: 2009-05-13 23:38:49 +0000 (Wed, 13 May 2009)
Log Message:
-----------
* had to temporarily comment out HAMPI dependent code - the HAMPI build.xml doesn't work, there is no HAMPI.jar, and Eclipse just silently stops building because of compile errors
>>>>> symbc please fix this <<<<<
* Config.getStringArray() and it's various variants were returning empty arrays for "x.y=" settings, where it should return null / the default values
* mod of ConsolePublisher to print "started"/"finished" markers only if there are "start" or "finished" topics, assuming that users otherwise want no output whatsoever
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsGeneral.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsHAMPI.java
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
trunk/src/gov/nasa/jpf/report/Publisher.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-13 20:48:30
|
Revision: 1510
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1510&view=rev
Author: frankrimlinger
Date: 2009-05-13 20:48:14 +0000 (Wed, 13 May 2009)
Log Message:
-----------
Rulebase image hooked up to automated start up. SCANNER hooked up to automated start up. Promptly crashes because no Mango object setup. Fix this bug and start working on control flow activities that occur during scan.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/core/gui/action/SaveCoreRuleBaseAction.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/OpenDefinitionMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/RulebaseMsg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
