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

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Revision: 1449
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1449&view=rev
Author:   frankrimlinger
Date:     2009-04-24 18:50:23 +0000 (Fri, 24 Apr 2009)

Log Message:
-----------
Removed all jpf extensions from MangoJPF classpath.  Changed JPF extension to SCANNER, because SCANNER will be fired to perform the initial scan of the designated class.  For this purpose, SCANNER fires MangoTargetLauncher.main(), which reflectively calls all the methods in the designated class to make sure all code gets traversed.  Moved ported bytecodes to package mango.scanner.bytecode since these bytecodes must be specifically designed to scan.  Because gov.nasa.jpf.symbc is no longer with us, a lot of these bytecodes are no longer compiling, but this is expected and they need to be stripped anyway to implement scanner functionality.  The first step is just to make sure every possible branch choice at the bytecode level is identified.  This includes all possible condition values for branch instructions, and all runtime exceptions for ALL bytecodes. And there are other weirdo exceptions, they all impact control flow so they all get modelled.  OK, not modelling IlletaMonitorStateException, as analysis is single threaded.

Start with ASTORE, you have a long row to hoe.

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/workstation/Workstation.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/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/ArrayInstruction.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ArrayLoadInstruction.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ArrayStoreInstruction.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/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/IfInstruction.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/LocalVariableInstruction.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LockInstruction.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LongArrayLoadInstruction.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LongArrayStoreInstruction.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/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/SwitchInstruction.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/VirtualInvocation.java

Added Paths:
-----------
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoTargetLauncher.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BytecodeUtils.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECG.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ReturnInstruction.java

Removed Paths:
-------------
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/JPF_MIRROR.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BytecodeUtils.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECG.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ReturnInstruction.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/MangoInstructionFactory.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/MangoTargetLauncher.java

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