Menu
▾
▴
[Javapathfinder-svn] SF.net SVN: javapathfinder:[1420] branches/mango/Mango
|
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.
|
