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: <pc...@us...> - 2009-04-22 01:18:06
|
Revision: 1434
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1434&view=rev
Author: pcorina
Date: 2009-04-22 01:17:58 +0000 (Wed, 22 Apr 2009)
Log Message:
-----------
some clean-up
Removed Paths:
-------------
trunk/extensions/symbc/src.tar.gz
trunk/extensions/symbc/test.tar.gz
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2009-04-22 01:11:14
|
Revision: 1433
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1433&view=rev
Author: pcorina
Date: 2009-04-22 01:11:08 +0000 (Wed, 22 Apr 2009)
Log Message:
-----------
fixed conflicts, classpath and weird characters in copyright notice
Modified Paths:
--------------
trunk/.classpath
trunk/examples/Termination.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/JPF_gov_nasa_jpf_complexcoverage_Debug.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFile.java
trunk/extensions/symbc/examples/StringTest.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/mixednumstrg/SpecialIntegerExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/mixednumstrg/SpecialRealExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/PathCondition.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringConstant.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringConstraint.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringOperator.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringPathCondition.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringSymbolic.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringBuilder.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExe1.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeMathIAsolver.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestSymbolic.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
Added Paths:
-----------
trunk/TestFileSimpleCoverage.java-trace
trunk/double-test.txt
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun SimpleCoverage.launch
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFileSimpleCoverage.java
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/symbc/JPF_java_lang_String.java
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/symbc/JPF_java_lang_StringBuffer.java
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/symbc/JPF_java_lang_StringBuilder.java
trunk/extensions/symbc/outFile.txt
trunk/extensions/symbc/src.tar.gz
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExDarko.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExMIT.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExStateflow.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeHeap2.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeHeap3.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeSimple.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeStrings.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/symtest.sh
trunk/extensions/symbc/test.tar.gz
trunk/extensions/symbc.tar.gz
trunk/javapathfinder-972.patch.txt
trunk/osm_method.dot
trunk/osm_sequence.dot
trunk/outFile.txt
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-22 00:14:16
|
Revision: 1432
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1432&view=rev
Author: frankrimlinger
Date: 2009-04-22 00:13:59 +0000 (Wed, 22 Apr 2009)
Log Message:
-----------
Successful simulation of itsAWrap using package mango.symbc.bytecode, which models all the bytecodes. This involved a few very minor changes to gov.nasa.jpf.jvm in order to avoid a runtime ClassCastException. I have submitted these changes to Peter for approval.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ReturnInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-21 22:33:11
|
Revision: 1431
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1431&view=rev
Author: frankrimlinger
Date: 2009-04-21 22:33:06 +0000 (Tue, 21 Apr 2009)
Log Message:
-----------
cleanup of bytecode port
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-21 22:27:50
|
Revision: 1430
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1430&view=rev
Author: frankrimlinger
Date: 2009-04-21 22:27:44 +0000 (Tue, 21 Apr 2009)
Log Message:
-----------
Initial port of all bytecodes to javapathfinder-mango-bridge/mango.symbc.bytecode. This includes all the bytecodes of gov.nasa.jpf.symbc.bytecode, with the set completed from the base package gov.nasa.jpf.jvm.bytecode. These bytecodes will now be stripped to the bare minimum required to traverse the forward control-flow diagram from an arbitrary starting point.
Successful opportunistic test of ability to stay in sync with jpf-trunk. Sourcecode updates get picked up automatically via sourcode link, and the new jars automaton.jar and string.jar require just slightly more effort, packaging in a jar plugin, loading into jpf-mango target folder, reloading the workbench target, and updating the plugin manifest and product. I've got the drill down now.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/input/SymbolicExecutionTest/symbolicExecution/SimpleTest.java
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassParsingAlg.java
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/D2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/D2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/F2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/F2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/F2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/GETSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/I2B.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/I2C.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/I2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/I2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/I2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/I2S.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IFEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IFGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IFGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IFLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IFLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IFNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IF_ICMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IINC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ISUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/L2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/L2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/L2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LCMP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LSHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/SwitchInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/TABLESWITCH.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mainArgFile
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/MangoTargetLauncher.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ARETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ArrayInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ArrayLoadInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ArrayStoreInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/BIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/BytecodeUtils.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/CASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DUP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DUP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DUP2_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DUP2_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DUP_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/DUP_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/FSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/GOTO_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IF_ACMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IF_ACMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ILOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INSTANCEOF.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INVOKECG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ISHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ISHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ISTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/IfInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/JSR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/JSR_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LDC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LDC2_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LDC_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LocalVariableInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LockInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LongArrayLoadInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/LongArrayStoreInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/MONITORENTER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/MONITOREXIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/NOP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/POP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/PUTFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/PUTSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/RET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/RETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/RUNSTART.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ReturnInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/SALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/SASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/SIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/SWAP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/VirtualInvocation.java
branches/mango/target_jars/plugins/javapathfinder_trunk_extensions_symbc_lib_update1_1.0.0.jar
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mainArgFile
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/MangoTargetLauncher.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/SymbolicStringHandler.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mainArgFile
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/MangoTargetLauncher.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/BytecodeUtils.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/D2I.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/D2L.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DCMPG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DCMPL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DNEG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DSUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/F2D.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/F2I.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/F2L.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FCMPG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FCMPL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FNEG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FSUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/GETSTATIC.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2B.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2C.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2D.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2F.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2L.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2S.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IAND.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFEQ.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFGE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFGT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFLE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFLT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFNE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPNE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IINC.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INEG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/ISUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IXOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/L2D.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/L2F.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/L2I.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LAND.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LCMP.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LNEG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LOOKUPSWITCH.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LSHL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LSHR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LSUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LUSHR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LXOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/SwitchInstruction.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/SymbolicStringHandler.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/TABLESWITCH.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <wv...@us...> - 2009-04-21 18:49:27
|
Revision: 1429
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1429&view=rev
Author: wvisser
Date: 2009-04-21 18:49:18 +0000 (Tue, 21 Apr 2009)
Log Message:
-----------
the packages to make JSA work as a string solver for jpf
Added Paths:
-----------
trunk/extensions/symbc/lib/automaton.jar
trunk/extensions/symbc/lib/string.jar
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <wv...@us...> - 2009-04-21 18:44:46
|
Revision: 1428
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1428&view=rev
Author: wvisser
Date: 2009-04-21 18:44:34 +0000 (Tue, 21 Apr 2009)
Log Message:
-----------
some additions to treat more of the string operations
this file will disappear soon when we have the peer class place
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <wv...@us...> - 2009-04-21 18:43:12
|
Revision: 1427
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1427&view=rev
Author: wvisser
Date: 2009-04-21 18:43:07 +0000 (Tue, 21 Apr 2009)
Log Message:
-----------
<work in progress>
symbolic string analysis with JSA and Automaton package
for now we have no dependencies so this is not completely working yet
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/DerivedStringExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringComparator.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsGeneral.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <wv...@us...> - 2009-04-21 18:41:43
|
Revision: 1426
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1426&view=rev
Author: wvisser
Date: 2009-04-21 18:41:28 +0000 (Tue, 21 Apr 2009)
Log Message:
-----------
small bug fix where a left should have been a right in an expression evaluation
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicConstraintsGeneral.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-21 17:04:42
|
Revision: 1425
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1425&view=rev
Author: frankrimlinger
Date: 2009-04-21 17:04:29 +0000 (Tue, 21 Apr 2009)
Log Message:
-----------
Test of itsAWrap under symbolic vm^2 execution. Fixed some imported package bugs in my version of the bytecode package. There could be a few more of these bugs still outstanding. With this in place, vm^2 got as far as vm, to a NullPointerException in clear(), as expected. But simulated method invocation appears to be working, so now will proceed to clear out all the simulation functionality other than class loading and invocation. Of course, you will need to add logic for the next pc in the case of branch instructions, and this will get you into choices and backtracking. Not sure how this will play out yet. But goal is to get jpf to traverse the forward control flow as efficiently as possible. Once this happens, the can think about punching in functionality to build control flow graph.
Confirmed that vm^2 does not required a project level dependence on the target project in order to executed the target project code. All this is taken care of through properties, as expected. However, vm obviously DOES require this link, everything else being equal.
Thinking down the road, ideally, the user should just point to a class, then simulation kicks in and travels down all methods in the class to build up the total control flow diagram and the call diagram. Then call diagram can be analyzed with respect to the rulebase to determine plausible next candidates for specification, which can then be presented to the user in a chooser window. This should all happen fast enough for the user to not think anything has happened. This will eliminate a lot of annoying file navigation and start up latency in current mango version.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mainArgFile
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKEVIRTUAL.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/BytecodeUtils.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-21 14:21:19
|
Revision: 1424
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1424&view=rev
Author: frankrimlinger
Date: 2009-04-21 14:21:15 +0000 (Tue, 21 Apr 2009)
Log Message:
-----------
Successful test of MangoTargetLauncher, which uses reflection to invoke the target method for symbolic simulation, eliminating the need to manually create a main() driver. Under this scenario, successfully duplicate the entire run for the MyClass1 example. The trick was to debug the launcher using the vm BEFORE attempting vm^2, because unfortunately cannot step through vm^2 with debugger (maybe you can with VJP?).
In any event, learned about listeners and the model java interface. There is a lot of subtle stuff going on here, and the fact that the launcher works out-of-the-box gives me enormous confidence to proceed.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/MangoTargetLauncher.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-21 10:48:15
|
Revision: 1423
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1423&view=rev
Author: frankrimlinger
Date: 2009-04-21 10:48:00 +0000 (Tue, 21 Apr 2009)
Log Message:
-----------
Work on reflective target launcher in progress. NullPointerException insider of Symboliclistenr.instructionExecuted. This happens during the processing of INVOKEVIRTUAL for the target method. There might be an issue since this instruction was generated by reflection. Hopefully I will not have to tweak anything outside of mango.
I settled on file i/o to pass the arguments to the main() routine. I really wanted to use a listener, but this would still involve modifying the constant pool, and there was just no need to go there.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/MangoTargetLauncher.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mainArgFile
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-20 22:58:44
|
Revision: 1422
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1422&view=rev
Author: frankrimlinger
Date: 2009-04-20 22:58:34 +0000 (Mon, 20 Apr 2009)
Log Message:
-----------
Well, it turns out that jpf can "do reflection" just fine, thank you very much. I was fooled by something both incredibly obvious and totally weird. I passed a static variable to Class.forName() which had been initialized, but not in the jpf virtual machine (the virtual^2 machine, so-to-speak). So I was really passing null, which of course didn't work. Obviously you can't use static intialization accomplished in the virtual machine to feed values to the main() routine running under the virtual^2 machine. I was trying to do this because I could find a way to pass arguments to main through the jpf properties mechanism. Perhaps there is a way. If worst comes to worst, I can do file i/o, which is totally out-of-band.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/MangoTargetLauncher.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-20 16:57:24
|
Revision: 1421
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1421&view=rev
Author: frankrimlinger
Date: 2009-04-20 16:57:17 +0000 (Mon, 20 Apr 2009)
Log Message:
-----------
Brilliant idea to reflect the target method inside target launcher main() for jpf symbolic execution has ended in abject failure:
java.lang.ClassNotFoundException
at java.lang.Class.forName(Native Method)
at mango.symbc.MangoTargetLauncher.getTargetMethod(MangoTargetLauncher.java:37)
at mango.symbc.MangoTargetLauncher.main(MangoTargetLauncher.java:13)
Evidently jpf draws the line at diving into reflection, and who can blame it for that?
Also, any hanky panky with the entrypoint is ruled out: on page 158, section5.2 of JVM2nd Ed., we have
"The Java virtual machine then links the initial class, initializes it, and invokes its public class method void main(String[]).
So it is written, so it must be. This is one of those exquisitely rare occasions when direct alteration of the .class file is required. Therefore, prior to any class loading, I will use my home-grown parser to read in MangoTargetLauncher.class, burn in the call to the targeted method, and write it back out. The trick is just to make sure that no other ClassLoader can find MangoTargetLauncher, and then call the "midnight special" ClassLoader to load it in when it is ready to go.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassParsingAlg.java
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/MangoTargetLauncher.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-20 04:31:54
|
Revision: 1420
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1420&view=rev
Author: frankrimlinger
Date: 2009-04-20 04:31:51 +0000 (Mon, 20 Apr 2009)
Log Message:
-----------
Switcheroo of symbolic execution to produce control flow diagram (as well as building byte code models) in progress. Made a copy of SymbolicInstructionFactory, called MangoInstructionFactory. For sanity test, created a copy of symbc/examples/MyClass1, which I put in the FrankInput project as symbolicExecution/SimpleTest. Discovered that jpf has a little trouble finding classes in remote projects, but there is a trick for this: the last line of the properties just needs to be the fully qualified class name, then all of a sudden jpf is ok with it. From within MangoJPF, fired up symbolic execution of SimpleTest against MangoInstructionFactory, producing the expected output (same as for MyClass1). So, all the plumbing is in place, it is time to bend MangoInstructionFactory to my will, and make it create the control flow diagram.
There is one slighly weird thing. JPF is ever so careful to get static initialization right, and so must be aware of the beginning of time from the get go. Whereas mango just assumes the beginning of time was at some unknown point in the past, and doesn't get stressed about it. The upshot is that I must manufacture a driver to call the targeted method before unleashing jpf. It is theoretically possible to do this, but maybe jpf can allow entrypoints other than main(). Must investigate. Either way, the nominal jpf execution is bogus, since the static initialization is "wrong". So there will always be a problematic element in switching between mango and "real" jpf.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/input/.classpath
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassParsingAlg.java
branches/mango/MangoJPF/html/toc.html
branches/mango/MangoJPF/plugin.xml
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/input/SymbolicExecutionTest/
branches/mango/Mango/mangoUserHome/frank/input/SymbolicExecutionTest/symbolicExecution/
branches/mango/Mango/mangoUserHome/frank/input/SymbolicExecutionTest/symbolicExecution/SimpleTest.java
branches/mango/Mango/mangoUserHome/frank/input/default.properties
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/D2I.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/D2L.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DCMPG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DCMPL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DNEG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DSUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/F2D.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/F2I.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/F2L.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FCMPG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FCMPL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FNEG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FSUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/GETSTATIC.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2B.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2C.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2D.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2F.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2L.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2S.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IAND.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFEQ.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFGE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFGT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFLE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFLT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFNE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPNE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IINC.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INEG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/ISUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IXOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/L2D.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/L2F.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/L2I.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LAND.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LCMP.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LNEG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LOOKUPSWITCH.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LSHL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LSHR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LSUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LUSHR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LXOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/SwitchInstruction.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/SymbolicStringHandler.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/TABLESWITCH.java
branches/mango/MangoJPF/toc/
branches/mango/MangoJPF/toc/tocconcepts.xml
branches/mango/MangoJPF/toc/tocgettingstarted.xml
branches/mango/MangoJPF/toc/tocreference.xml
branches/mango/MangoJPF/toc/tocsamples.xml
branches/mango/MangoJPF/toc/toctasks.xml
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/symbc/
branches/mango/MangoJPF/tocconcepts.xml
branches/mango/MangoJPF/tocgettingstarted.xml
branches/mango/MangoJPF/tocreference.xml
branches/mango/MangoJPF/tocsamples.xml
branches/mango/MangoJPF/toctasks.xml
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-19 04:35:38
|
Revision: 1419
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1419&view=rev
Author: frankrimlinger
Date: 2009-04-19 04:35:28 +0000 (Sun, 19 Apr 2009)
Log Message:
-----------
Used properties from Corina's slides "Symbolic Execution of Bytecodes", e.g., +vm.insn_factory.class=gov.nasa.jpf.symbc.MangoInstructionFactory, to cause JPF to perform symbolic execution. Tested on Racer, which emitted plausible symbolic output. Right now, MangoInstructionFactory is just a copy of SymbolicInstructionFactory, but with this plumbing in place, lots of opportunity opens up. In particular, the instructions can be overriden to
1. perform whatever classloading activities would nominally take place
2. choose each branch exactly once,
3. hook up a corresponding vertex for a control flow graph created on-the-fly.
By this means, simply pointing JPF at the method to be analyzed and running will simultaneously create the bytecode model and the control flow diagram required by mango.
There is probably more to it than just playing with instructions, as the choices for branching and backtracking have to be correct. Probably with the right definition of state, the game will play itself.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassParsingAlg.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/symbc/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/symbc/MangoInstructionFactory.java
Removed Paths:
-------------
branches/mango/target_jars/plugins/jpf_build_jars_1.0.0.jar
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-18 03:51:00
|
Revision: 1418
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1418&view=rev
Author: frankrimlinger
Date: 2009-04-18 03:50:58 +0000 (Sat, 18 Apr 2009)
Log Message:
-----------
Created extension of JPF, called JPF_MIRROR, whose main routine creates the vm but does not fire up a thread and run. Now comes an interesting issue. Mango needs to do an analysis of the "entire" code body in order to convert loops to recursive functions. But jpf pulls in classes on-the-fly, starting out with just enough grist for the mill. This is certainly more elegant, but jpf doesn't necessarily "care" about complete coverage of all paths. It seems quite likely there is an option for such a preference, and I will investigate. In any case, the idea is to give jpf the method to be analyzed as the "main" routine and let it run through though all edges of the forward control flow graph at least once. This will cause all the invovled classes to get pulled in. Once I have all the relevant class models then mango can do its thing, creating "advice" for future jpf runs.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.project
branches/mango/MangoJPF/Mango/src/mango/control/msg/StartRequestMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassParsingAlg.java
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <jt...@us...> - 2009-04-17 23:28:41
|
Revision: 1417
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1417&view=rev
Author: jtzwu
Date: 2009-04-17 23:28:26 +0000 (Fri, 17 Apr 2009)
Log Message:
-----------
Fix bug 1882764. The StateSpaceDot listener was tracking the previous
state of the machine and placing it in the graph when the graph search
ended. If there is only one state, the previous state is null. When
StateSpaceDot attempts to place the previous state into the graph, a
null pointer exception is hit. I placed a guard in front of the add
function to check that the previous state is not null.
Modified Paths:
--------------
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestExJPF.java
trunk/src/gov/nasa/jpf/tools/StateSpaceDot.java
Added Paths:
-----------
trunk/test/gov/nasa/jpf/tools/
trunk/test/gov/nasa/jpf/tools/TestStateSpaceDotJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-17 19:53:46
|
Revision: 1416
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1416&view=rev
Author: frankrimlinger
Date: 2009-04-17 19:53:44 +0000 (Fri, 17 Apr 2009)
Log Message:
-----------
Added some configuration paths to successfully run of "Racer" jpf test inside of MangoRPF. Now comes the fun part. Instead of calling JPF.main(), the idea is to manually handle the initialization sequence. This will accomplish two things. First, it will avoid having main() fire up a thread and run too completion, and second, it will expose the object oriented byte code model to mango. The first step is to use this byte code model to build the mango model. This will involve a lot of replumbing. Once this is done, then have to figure out how to use the mango model to leverage symbolic simulation/backtracking in jpf. Eventually, it might be possible to back-out mango into a true jpf extension, but one thing at a time.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-17 17:48:33
|
Revision: 1415
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1415&view=rev
Author: frankrimlinger
Date: 2009-04-17 17:48:21 +0000 (Fri, 17 Apr 2009)
Log Message:
-----------
The first step to getting jpf code to run is to reproduce the exact environment that it likes. Just bundling the jars that jpf uses into plugins should not affect runtime, so that is still in place. However, instead of attempting to jar the source code that jpf-trunk loads, I just link to this source from MangoJPF. Having done so, all the jpf code compiles inside of MangoJPF, except the java5/6 "compatibility code". Probably breaks as I am running under J2SE6. I filtered out the sun compatibility classes, but now there is a broken calls in env/jpf/jaf.lang.Class and System. Hopefully not a problem, but in any event should go away when the switch to J2SE6 is "official".
But, lots of MangoJPF code is breaking. Certain things can probably be safely thrown overboard. In particular, extensions/ui/env/jpf/java.awt and java.swing are probably stubs for jpf users. Doing this, the rest of the jpf code still compiles, hooray, and the only remaining issues with MangoJPF involve some unsupported methods in env/jpf/java/lang, especially Class and ClassLoader. I rewrite the MangoJPF code to conform. Not a problem since JPF will be taking over this particular MangoJPF functionality anyway.
So, with all of this in place, I get past my initial crash to
[SEVERE] error during VM runtime initialization: wrong model classes (check vm.[boot]classpath)
This looks hopeful, so syncing to lock in current progress. Of course, the link to the jpf-trunk source code is a very temporary expedient. It is not a deployable solution, and it is far too tempting to alter jpf-trunk code this way. Once things settle down I will find a way to jar most if not all of the trunk code.
Modified Paths:
--------------
branches/mango/Mango/content/proofArtifacts.xhtml
branches/mango/Mango/content/specification.xhtml
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.project
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/Mango/src/mango/control/input/JarLoader.java
branches/mango/MangoJPF/Mango/src/mango/control/msg/StartRequestMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/Hash.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupDelegate/BackupDelegate.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/Graph.java
branches/mango/MangoJPF/Mango/src/mango/workstation/RuleResourceManager.java
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-17 04:14:43
|
Revision: 1414
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1414&view=rev
Author: frankrimlinger
Date: 2009-04-17 04:14:38 +0000 (Fri, 17 Apr 2009)
Log Message:
-----------
These jar plugins may be incompatible with the jpf version of java.lang??? Must think about this.
Added Paths:
-----------
branches/mango/target_jars/
branches/mango/target_jars/plugins/
branches/mango/target_jars/plugins/Mango_Jars_1.0.0.jar
branches/mango/target_jars/plugins/jpf_build_jars_1.0.0.jar
branches/mango/target_jars/plugins/jpf_trunk_build_tools_lib_1.0.0.jar
branches/mango/target_jars/plugins/jpf_trunk_extensions_concolic_1.0.0.jar
branches/mango/target_jars/plugins/jpf_trunk_extensions_symbc_1.0.0.jar
branches/mango/target_jars/plugins/jpf_trunk_extensions_symbolic_1.0.0.jar
branches/mango/target_jars/plugins/jpf_trunk_lib_1.0.0.jar
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-17 04:11:10
|
Revision: 1413
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1413&view=rev
Author: frankrimlinger
Date: 2009-04-17 04:11:08 +0000 (Fri, 17 Apr 2009)
Log Message:
-----------
Have realized that jpf really does override java.lang.Class and other fun classes in ways that are significantly incompatible with the rest of the universe. But even loading the jpf versions of these classes, I still crash very early on in the class loader. This could be an incompatibility with the jar plugins?? Perhaps I must convince the jar plugin builder to accept the rogue java.lang code??? Must sleep on this.
Modified Paths:
--------------
branches/mango/Mango/.classpath
branches/mango/Mango/META-INF/MANIFEST.MF
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.project
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-16 19:59:41
|
Revision: 1412
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1412&view=rev
Author: frankrimlinger
Date: 2009-04-16 19:59:37 +0000 (Thu, 16 Apr 2009)
Log Message:
-----------
OK, there probably was nothing wrong with the MangoJPF help mechanism as such. The problem was that the "class path settings" needed to be updated. This is a good one to try whenever plugins don't seem to be kicking in. However, it was just as well to throw out the old hand written table of contents html. The proper thing to do is to use the suppled table of contents html editor to build up the help files. The workings of this editor revealed in detail when you click on its help icon.
To summarize, Mango and MangoJPF are both healthy again. MangoJPF still needs its plugin jars bundling the jars required by jpf. These are now stored in the toplevel directory javapathfinder-mango/"target jars". This is a good place for manufactured plugins to hang out, as they must be loaded into the "target" at the Eclipse preference level. Once so loaded, they easily feed into the MangoJPF plugin. The "repository" concept isn't working for me and so I have abandoned it.
So, plugins should flow from the Eclipse preference target, to the project preference build path, to the plugin manifest, to the produce configuration editor. Don't try to work them upstream, and it's a piece of cake.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/plugin.xml
Added Paths:
-----------
branches/mango/MangoJPF/html/
branches/mango/MangoJPF/html/concepts/
branches/mango/MangoJPF/html/concepts/maintopic.html
branches/mango/MangoJPF/html/concepts/subtopic.html
branches/mango/MangoJPF/html/concepts/subtopic2.html
branches/mango/MangoJPF/html/gettingstarted/
branches/mango/MangoJPF/html/gettingstarted/maintopic.html
branches/mango/MangoJPF/html/gettingstarted/subtopic.html
branches/mango/MangoJPF/html/gettingstarted/subtopic2.html
branches/mango/MangoJPF/html/reference/
branches/mango/MangoJPF/html/reference/maintopic.html
branches/mango/MangoJPF/html/reference/subtopic.html
branches/mango/MangoJPF/html/reference/subtopic2.html
branches/mango/MangoJPF/html/samples/
branches/mango/MangoJPF/html/samples/maintopic.html
branches/mango/MangoJPF/html/samples/subtopic.html
branches/mango/MangoJPF/html/samples/subtopic2.html
branches/mango/MangoJPF/html/tasks/
branches/mango/MangoJPF/html/tasks/maintopic.html
branches/mango/MangoJPF/html/tasks/subtopic.html
branches/mango/MangoJPF/html/tasks/subtopic2.html
branches/mango/MangoJPF/html/toc.html
branches/mango/MangoJPF/toc.xml
branches/mango/MangoJPF/tocconcepts.xml
branches/mango/MangoJPF/tocgettingstarted.xml
branches/mango/MangoJPF/tocreference.xml
branches/mango/MangoJPF/tocsamples.xml
branches/mango/MangoJPF/toctasks.xml
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-16 19:34:15
|
Revision: 1411
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1411&view=rev
Author: frankrimlinger
Date: 2009-04-16 19:34:09 +0000 (Thu, 16 Apr 2009)
Log Message:
-----------
The MangoJPF help mechanism somehow got broken. Clearing it out for a fresh start.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
branches/mango/MangoJPF/content/mangoJPF.xhtml
branches/mango/MangoJPF/content/proofArtifacts.xhtml
branches/mango/MangoJPF/introContent.xml
branches/mango/MangoJPF/plugin.xml
branches/mango/MangoJPF/src/mango/intro/ApplicationWorkbenchWindowAdvisor.java
branches/mango/MangoJPF/src/mango/intro/LoginDialog.java
branches/mango/MangoJPF/src/mango/intro/Perspective.java
Added Paths:
-----------
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/content/aboutHelp.xhtml
branches/mango/MangoJPF/help.bmp
Removed Paths:
-------------
branches/mango/MangoJPF/html/
branches/mango/MangoJPF/toc/
branches/mango/MangoJPF/toc.xml
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-16 17:24:41
|
Revision: 1410
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1410&view=rev
Author: frankrimlinger
Date: 2009-04-16 17:24:30 +0000 (Thu, 16 Apr 2009)
Log Message:
-----------
cleanup of MangoJPF in preparation for product rebuild.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/META-INF/MANIFEST.MF
Removed Paths:
-------------
branches/mango/MangoJPF/MangoJPF.product
branches/mango/MangoJPF/repository/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
