changeset 0:61d41facf527

initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children f6886b2bda4a
files .classpath .hgignore .project LICENSE-2.0.txt README bin/javajpf bin/jpf bin/jpf.bat bin/print_class bin/print_class.bat bin/print_events bin/test bin/test.bat build.properties build.xml doc/devel/attributes.md doc/devel/bytecode_factory.md doc/devel/choicegenerator.md doc/devel/coding_conventions.md doc/devel/create_project.md doc/devel/design.md doc/devel/eclipse_plugin_update.md doc/devel/embedded.md doc/devel/index.md doc/devel/jpf_tests.md doc/devel/listener.md doc/devel/logging.md doc/devel/mercurial.md doc/devel/mji.md doc/devel/mji/mangling.md doc/devel/modules.md doc/devel/partial_order_reduction.md doc/devel/report.md doc/graphics/DFSListener.svg doc/graphics/app-types.svg doc/graphics/attributes.svg doc/graphics/bc-factory.svg doc/graphics/cg-impl.svg doc/graphics/cg-motivation.svg doc/graphics/cg-ontology.svg doc/graphics/cg-sequence.svg doc/graphics/choicegen-example.svg doc/graphics/genpeer.svg doc/graphics/interleavings.svg doc/graphics/jpf-abstractions.svg doc/graphics/jpf-basic.svg doc/graphics/jpf-intro-new.svg doc/graphics/jpf-layers.svg doc/graphics/jpf-project.svg doc/graphics/listener-overview.svg doc/graphics/listeners.svg doc/graphics/mji-call.svg doc/graphics/mji-functions.svg doc/graphics/mji-mangling.svg doc/graphics/new-testing.svg doc/graphics/por-mark.svg doc/graphics/por-scheduling-relevance.svg doc/graphics/properties.svg doc/graphics/report.svg doc/graphics/states-mc.svg doc/graphics/states-testing.svg doc/graphics/sw-model-checking-2.svg doc/graphics/sw-model-checking.svg doc/index.md doc/install/build.md doc/install/eclipse-jpf.md doc/install/eclipse-plugin.md doc/install/eclipse-plugin/update.md doc/install/eclipse-plugin/update/features.md doc/install/eclipse-plugin/update/plugins.md doc/install/index.md doc/install/netbeans-jpf.md doc/install/netbeans-plugin.md doc/install/repo_shell.md doc/install/repositories.md doc/install/requirements.md doc/install/site-properties.md doc/install/snapshot.md doc/intro/classification.md doc/intro/index.md doc/intro/race_example.md doc/intro/random_example.md doc/intro/testing_vs_model_checking.md doc/intro/what_is_jpf.md doc/jpf-core/AssertionProperty.md doc/jpf-core/ErrorTraceGenerator.md doc/jpf-core/ExceptionInjector.md doc/jpf-core/IdleFilter.md doc/jpf-core/index.md doc/papers/chicago-author-date.csl doc/papers/index.md doc/papers/references.bib doc/user/api.md doc/user/application_types.md doc/user/components.md doc/user/config.md doc/user/config/random.md doc/user/index.md doc/user/output.md doc/user/run.md doc/user/run_eclipse.md doc/user/run_eclipse_plugin.md doc/user/run_nb.md doc/user/run_nb_plugin.md eclipse/AntBuilder.launch eclipse/run-JPF.launch eclipse/test-JPF.launch eclipse/update-JPF-siteproperties.launch jpf.properties nbproject/ide-file-targets.xml nbproject/project.xml src/annotations/gov/nasa/jpf/annotation/FilterField.java src/annotations/gov/nasa/jpf/annotation/FilterFrame.java src/annotations/gov/nasa/jpf/annotation/JPFConfig.java src/annotations/gov/nasa/jpf/annotation/JPFOption.java src/annotations/gov/nasa/jpf/annotation/JPFOptions.java src/annotations/gov/nasa/jpf/annotation/MJI.java src/annotations/gov/nasa/jpf/annotation/NeverBreak.java src/classes/gov/nasa/jpf/AnnotationProxyBase.java src/classes/gov/nasa/jpf/BoxObjectCaches.java src/classes/gov/nasa/jpf/CachedROHttpConnection.java src/classes/gov/nasa/jpf/ConsoleOutputStream.java src/classes/gov/nasa/jpf/EventProducer.java src/classes/gov/nasa/jpf/FinalizerThread.java src/classes/gov/nasa/jpf/SerializationConstructor.java src/classes/java/io/File.java src/classes/java/io/FileDescriptor.java src/classes/java/io/FileInputStream.java src/classes/java/io/FileOutputStream.java src/classes/java/io/InputStreamReader.java src/classes/java/io/OutputStreamWriter.java src/classes/java/io/RandomAccessFile.java src/classes/java/lang/Class.java src/classes/java/lang/ClassLoader.java src/classes/java/lang/InheritableThreadLocal.java src/classes/java/lang/Object.java src/classes/java/lang/StackTraceElement.java src/classes/java/lang/String.java src/classes/java/lang/System.java src/classes/java/lang/Thread.java src/classes/java/lang/ThreadGroup.java src/classes/java/lang/ThreadLocal.java src/classes/java/lang/Throwable.java src/classes/java/lang/annotation/Inherited.java src/classes/java/lang/annotation/Retention.java src/classes/java/lang/ref/Reference.java src/classes/java/lang/ref/ReferenceQueue.java src/classes/java/lang/ref/WeakReference.java src/classes/java/lang/reflect/AccessibleObject.java src/classes/java/lang/reflect/Constructor.java src/classes/java/lang/reflect/Field.java src/classes/java/lang/reflect/InvocationTargetException.java src/classes/java/lang/reflect/Method.java src/classes/java/net/URLClassLoader.java src/classes/java/nio/Buffer.java src/classes/java/nio/BufferUnderflowException.java src/classes/java/nio/ByteBuffer.java src/classes/java/nio/ByteOrder.java src/classes/java/nio/channels/FileChannel.java src/classes/java/nio/package-info.java src/classes/java/security/AccessController.java src/classes/java/security/MessageDigest.java src/classes/java/security/SecureClassLoader.java src/classes/java/text/DecimalFormat.java src/classes/java/text/Format.java src/classes/java/text/NumberFormat.java src/classes/java/text/SimpleDateFormat.java src/classes/java/util/Random.java src/classes/java/util/TimeZone.java src/classes/java/util/concurrent/BrokenBarrierException.java src/classes/java/util/concurrent/CyclicBarrier.java src/classes/java/util/concurrent/Exchanger.java src/classes/java/util/concurrent/atomic/AtomicIntegerArray.java src/classes/java/util/concurrent/atomic/AtomicIntegerFieldUpdater.java src/classes/java/util/concurrent/atomic/AtomicLongArray.java src/classes/java/util/concurrent/atomic/AtomicLongFieldUpdater.java src/classes/java/util/concurrent/atomic/AtomicReferenceArray.java src/classes/java/util/concurrent/atomic/AtomicReferenceFieldUpdater.java src/classes/java/util/function/Supplier.java src/classes/java/util/logging/FileHandler.java src/classes/java/util/regex/Matcher.java src/classes/java/util/regex/Pattern.java src/classes/org/junit/After.java src/classes/org/junit/AfterClass.java src/classes/org/junit/Before.java src/classes/org/junit/BeforeClass.java src/classes/org/junit/Ignore.java src/classes/org/junit/Test.java src/classes/sun/misc/AtomicLong.java src/classes/sun/misc/JavaAWTAccess.java src/classes/sun/misc/JavaIOAccess.java src/classes/sun/misc/JavaIODeleteOnExitAccess.java src/classes/sun/misc/JavaIOFileDescriptorAccess.java src/classes/sun/misc/JavaLangAccess.java src/classes/sun/misc/JavaNetAccess.java src/classes/sun/misc/JavaNioAccess.java src/classes/sun/misc/SharedSecrets.java src/classes/sun/misc/Unsafe.java src/classes/sun/net/www/protocol/http/Handler.java src/classes/sun/nio/ch/Interruptible.java src/classes/sun/reflect/ConstantPool.java src/classes/sun/reflect/annotation/AnnotationType.java src/examples/BoundedBuffer.java src/examples/BoundedBuffer.jpf src/examples/Crossing.java src/examples/Crossing.jpf src/examples/DiningPhil.java src/examples/DiningPhil.jpf src/examples/HelloWorld.java src/examples/HelloWorld.jpf src/examples/NumericValueCheck.java src/examples/NumericValueCheck.jpf src/examples/Racer.java src/examples/Racer.jpf src/examples/Rand.java src/examples/Rand.jpf src/examples/RobotManager-replay-nt.jpf src/examples/RobotManager-replay-ot.jpf src/examples/RobotManager.java src/examples/RobotManager.jpf src/examples/StopWatch.java src/examples/StopWatch.jpf src/examples/TestExample-coverage.jpf src/examples/TestExample.java src/examples/oldclassic-da.jpf src/examples/oldclassic.java src/examples/oldclassic.jpf src/main/gov/nasa/jpf/$coreTag.java src/main/gov/nasa/jpf/Config.java src/main/gov/nasa/jpf/ConfigChangeListener.java src/main/gov/nasa/jpf/Error.java src/main/gov/nasa/jpf/GenericProperty.java src/main/gov/nasa/jpf/JPF.java src/main/gov/nasa/jpf/JPFClassLoader.java src/main/gov/nasa/jpf/JPFConfigException.java src/main/gov/nasa/jpf/JPFErrorException.java src/main/gov/nasa/jpf/JPFException.java src/main/gov/nasa/jpf/JPFListener.java src/main/gov/nasa/jpf/JPFListenerException.java src/main/gov/nasa/jpf/JPFNativePeerException.java src/main/gov/nasa/jpf/JPFShell.java src/main/gov/nasa/jpf/ListenerAdapter.java src/main/gov/nasa/jpf/Property.java src/main/gov/nasa/jpf/PropertyListenerAdapter.java src/main/gov/nasa/jpf/State.java src/main/gov/nasa/jpf/StateExtension.java src/main/gov/nasa/jpf/SystemAttribute.java src/main/gov/nasa/jpf/jvm/ClassFile.java src/main/gov/nasa/jpf/jvm/ClassFilePrinter.java src/main/gov/nasa/jpf/jvm/ClassFileReader.java src/main/gov/nasa/jpf/jvm/ClassFileReaderAdapter.java src/main/gov/nasa/jpf/jvm/DirClassFileContainer.java src/main/gov/nasa/jpf/jvm/JVMAnnotationParser.java src/main/gov/nasa/jpf/jvm/JVMByteCodePrinter.java src/main/gov/nasa/jpf/jvm/JVMByteCodeReader.java src/main/gov/nasa/jpf/jvm/JVMByteCodeReaderAdapter.java src/main/gov/nasa/jpf/jvm/JVMClassFileContainer.java src/main/gov/nasa/jpf/jvm/JVMClassInfo.java src/main/gov/nasa/jpf/jvm/JVMCodeBuilder.java src/main/gov/nasa/jpf/jvm/JVMDirectCallStackFrame.java src/main/gov/nasa/jpf/jvm/JVMInstructionFactory.java src/main/gov/nasa/jpf/jvm/JVMNativeStackFrame.java src/main/gov/nasa/jpf/jvm/JVMStackFrame.java src/main/gov/nasa/jpf/jvm/JVMSystemClassLoaderInfo.java src/main/gov/nasa/jpf/jvm/JarClassFileContainer.java src/main/gov/nasa/jpf/jvm/bytecode/AALOAD.java src/main/gov/nasa/jpf/jvm/bytecode/AASTORE.java src/main/gov/nasa/jpf/jvm/bytecode/ACONST_NULL.java src/main/gov/nasa/jpf/jvm/bytecode/ALOAD.java src/main/gov/nasa/jpf/jvm/bytecode/ANEWARRAY.java src/main/gov/nasa/jpf/jvm/bytecode/ARETURN.java src/main/gov/nasa/jpf/jvm/bytecode/ARRAYLENGTH.java src/main/gov/nasa/jpf/jvm/bytecode/ASTORE.java src/main/gov/nasa/jpf/jvm/bytecode/ATHROW.java src/main/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/BALOAD.java src/main/gov/nasa/jpf/jvm/bytecode/BASTORE.java src/main/gov/nasa/jpf/jvm/bytecode/BIPUSH.java src/main/gov/nasa/jpf/jvm/bytecode/CALOAD.java src/main/gov/nasa/jpf/jvm/bytecode/CASTORE.java src/main/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java src/main/gov/nasa/jpf/jvm/bytecode/D2F.java src/main/gov/nasa/jpf/jvm/bytecode/D2I.java src/main/gov/nasa/jpf/jvm/bytecode/D2L.java src/main/gov/nasa/jpf/jvm/bytecode/DADD.java src/main/gov/nasa/jpf/jvm/bytecode/DALOAD.java src/main/gov/nasa/jpf/jvm/bytecode/DASTORE.java src/main/gov/nasa/jpf/jvm/bytecode/DCMPG.java src/main/gov/nasa/jpf/jvm/bytecode/DCMPL.java src/main/gov/nasa/jpf/jvm/bytecode/DCONST.java src/main/gov/nasa/jpf/jvm/bytecode/DDIV.java src/main/gov/nasa/jpf/jvm/bytecode/DIRECTCALLRETURN.java src/main/gov/nasa/jpf/jvm/bytecode/DLOAD.java src/main/gov/nasa/jpf/jvm/bytecode/DMUL.java src/main/gov/nasa/jpf/jvm/bytecode/DNEG.java src/main/gov/nasa/jpf/jvm/bytecode/DREM.java src/main/gov/nasa/jpf/jvm/bytecode/DRETURN.java src/main/gov/nasa/jpf/jvm/bytecode/DSTORE.java src/main/gov/nasa/jpf/jvm/bytecode/DSUB.java src/main/gov/nasa/jpf/jvm/bytecode/DUP.java src/main/gov/nasa/jpf/jvm/bytecode/DUP2.java src/main/gov/nasa/jpf/jvm/bytecode/DUP2_X1.java src/main/gov/nasa/jpf/jvm/bytecode/DUP2_X2.java src/main/gov/nasa/jpf/jvm/bytecode/DUP_X1.java src/main/gov/nasa/jpf/jvm/bytecode/DUP_X2.java src/main/gov/nasa/jpf/jvm/bytecode/DoubleCompareInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/EXECUTENATIVE.java src/main/gov/nasa/jpf/jvm/bytecode/F2D.java src/main/gov/nasa/jpf/jvm/bytecode/F2I.java src/main/gov/nasa/jpf/jvm/bytecode/F2L.java src/main/gov/nasa/jpf/jvm/bytecode/FADD.java src/main/gov/nasa/jpf/jvm/bytecode/FALOAD.java src/main/gov/nasa/jpf/jvm/bytecode/FASTORE.java src/main/gov/nasa/jpf/jvm/bytecode/FCMPG.java src/main/gov/nasa/jpf/jvm/bytecode/FCMPL.java src/main/gov/nasa/jpf/jvm/bytecode/FCONST.java src/main/gov/nasa/jpf/jvm/bytecode/FDIV.java src/main/gov/nasa/jpf/jvm/bytecode/FLOAD.java src/main/gov/nasa/jpf/jvm/bytecode/FMUL.java src/main/gov/nasa/jpf/jvm/bytecode/FNEG.java src/main/gov/nasa/jpf/jvm/bytecode/FREM.java src/main/gov/nasa/jpf/jvm/bytecode/FRETURN.java src/main/gov/nasa/jpf/jvm/bytecode/FSTORE.java src/main/gov/nasa/jpf/jvm/bytecode/FSUB.java src/main/gov/nasa/jpf/jvm/bytecode/GETFIELD.java src/main/gov/nasa/jpf/jvm/bytecode/GETSTATIC.java src/main/gov/nasa/jpf/jvm/bytecode/GOTO.java src/main/gov/nasa/jpf/jvm/bytecode/GOTO_W.java src/main/gov/nasa/jpf/jvm/bytecode/GetHelper.java src/main/gov/nasa/jpf/jvm/bytecode/I2B.java src/main/gov/nasa/jpf/jvm/bytecode/I2C.java src/main/gov/nasa/jpf/jvm/bytecode/I2D.java src/main/gov/nasa/jpf/jvm/bytecode/I2F.java src/main/gov/nasa/jpf/jvm/bytecode/I2L.java src/main/gov/nasa/jpf/jvm/bytecode/I2S.java src/main/gov/nasa/jpf/jvm/bytecode/IADD.java src/main/gov/nasa/jpf/jvm/bytecode/IALOAD.java src/main/gov/nasa/jpf/jvm/bytecode/IAND.java src/main/gov/nasa/jpf/jvm/bytecode/IASTORE.java src/main/gov/nasa/jpf/jvm/bytecode/ICONST.java src/main/gov/nasa/jpf/jvm/bytecode/IDIV.java src/main/gov/nasa/jpf/jvm/bytecode/IFEQ.java src/main/gov/nasa/jpf/jvm/bytecode/IFGE.java src/main/gov/nasa/jpf/jvm/bytecode/IFGT.java src/main/gov/nasa/jpf/jvm/bytecode/IFLE.java src/main/gov/nasa/jpf/jvm/bytecode/IFLT.java src/main/gov/nasa/jpf/jvm/bytecode/IFNE.java src/main/gov/nasa/jpf/jvm/bytecode/IFNONNULL.java src/main/gov/nasa/jpf/jvm/bytecode/IFNULL.java src/main/gov/nasa/jpf/jvm/bytecode/IF_ACMPEQ.java src/main/gov/nasa/jpf/jvm/bytecode/IF_ACMPNE.java src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPEQ.java src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPGE.java src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPGT.java src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPLE.java src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPLT.java src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPNE.java src/main/gov/nasa/jpf/jvm/bytecode/IINC.java src/main/gov/nasa/jpf/jvm/bytecode/ILOAD.java src/main/gov/nasa/jpf/jvm/bytecode/IMUL.java src/main/gov/nasa/jpf/jvm/bytecode/INEG.java src/main/gov/nasa/jpf/jvm/bytecode/INSTANCEOF.java src/main/gov/nasa/jpf/jvm/bytecode/INVOKECG.java src/main/gov/nasa/jpf/jvm/bytecode/INVOKECLINIT.java src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java src/main/gov/nasa/jpf/jvm/bytecode/INVOKEINTERFACE.java src/main/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java src/main/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java src/main/gov/nasa/jpf/jvm/bytecode/INVOKEVIRTUAL.java src/main/gov/nasa/jpf/jvm/bytecode/IOR.java src/main/gov/nasa/jpf/jvm/bytecode/IREM.java src/main/gov/nasa/jpf/jvm/bytecode/IRETURN.java src/main/gov/nasa/jpf/jvm/bytecode/ISHL.java src/main/gov/nasa/jpf/jvm/bytecode/ISHR.java src/main/gov/nasa/jpf/jvm/bytecode/ISTORE.java src/main/gov/nasa/jpf/jvm/bytecode/ISUB.java src/main/gov/nasa/jpf/jvm/bytecode/IUSHR.java src/main/gov/nasa/jpf/jvm/bytecode/IXOR.java src/main/gov/nasa/jpf/jvm/bytecode/IfInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/InstanceInvocation.java src/main/gov/nasa/jpf/jvm/bytecode/InstructionFactory.java src/main/gov/nasa/jpf/jvm/bytecode/JSR.java src/main/gov/nasa/jpf/jvm/bytecode/JSR_W.java src/main/gov/nasa/jpf/jvm/bytecode/JVMArrayElementInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/JVMFieldInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/JVMInstanceFieldInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/JVMInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/JVMInstructionVisitor.java src/main/gov/nasa/jpf/jvm/bytecode/JVMInstructionVisitorAdapter.java src/main/gov/nasa/jpf/jvm/bytecode/JVMInvokeInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/JVMLocalVariableInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/JVMReturnInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/JVMStaticFieldInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/L2D.java src/main/gov/nasa/jpf/jvm/bytecode/L2F.java src/main/gov/nasa/jpf/jvm/bytecode/L2I.java src/main/gov/nasa/jpf/jvm/bytecode/LADD.java src/main/gov/nasa/jpf/jvm/bytecode/LALOAD.java src/main/gov/nasa/jpf/jvm/bytecode/LAND.java src/main/gov/nasa/jpf/jvm/bytecode/LASTORE.java src/main/gov/nasa/jpf/jvm/bytecode/LCMP.java src/main/gov/nasa/jpf/jvm/bytecode/LCONST.java src/main/gov/nasa/jpf/jvm/bytecode/LDC.java src/main/gov/nasa/jpf/jvm/bytecode/LDC2_W.java src/main/gov/nasa/jpf/jvm/bytecode/LDC_W.java src/main/gov/nasa/jpf/jvm/bytecode/LDIV.java src/main/gov/nasa/jpf/jvm/bytecode/LLOAD.java src/main/gov/nasa/jpf/jvm/bytecode/LMUL.java src/main/gov/nasa/jpf/jvm/bytecode/LNEG.java src/main/gov/nasa/jpf/jvm/bytecode/LOOKUPSWITCH.java src/main/gov/nasa/jpf/jvm/bytecode/LOR.java src/main/gov/nasa/jpf/jvm/bytecode/LREM.java src/main/gov/nasa/jpf/jvm/bytecode/LRETURN.java src/main/gov/nasa/jpf/jvm/bytecode/LSHL.java src/main/gov/nasa/jpf/jvm/bytecode/LSHR.java src/main/gov/nasa/jpf/jvm/bytecode/LSTORE.java src/main/gov/nasa/jpf/jvm/bytecode/LSUB.java src/main/gov/nasa/jpf/jvm/bytecode/LUSHR.java src/main/gov/nasa/jpf/jvm/bytecode/LXOR.java src/main/gov/nasa/jpf/jvm/bytecode/LockInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/LongArrayLoadInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/LongArrayStoreInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/LongReturn.java src/main/gov/nasa/jpf/jvm/bytecode/MONITORENTER.java src/main/gov/nasa/jpf/jvm/bytecode/MONITOREXIT.java src/main/gov/nasa/jpf/jvm/bytecode/MULTIANEWARRAY.java src/main/gov/nasa/jpf/jvm/bytecode/NATIVERETURN.java src/main/gov/nasa/jpf/jvm/bytecode/NEW.java src/main/gov/nasa/jpf/jvm/bytecode/NEWARRAY.java src/main/gov/nasa/jpf/jvm/bytecode/NOP.java src/main/gov/nasa/jpf/jvm/bytecode/NewArrayInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/POP.java src/main/gov/nasa/jpf/jvm/bytecode/POP2.java src/main/gov/nasa/jpf/jvm/bytecode/PUTFIELD.java src/main/gov/nasa/jpf/jvm/bytecode/PUTSTATIC.java src/main/gov/nasa/jpf/jvm/bytecode/PutHelper.java src/main/gov/nasa/jpf/jvm/bytecode/RET.java src/main/gov/nasa/jpf/jvm/bytecode/RETURN.java src/main/gov/nasa/jpf/jvm/bytecode/RUNSTART.java src/main/gov/nasa/jpf/jvm/bytecode/SALOAD.java src/main/gov/nasa/jpf/jvm/bytecode/SASTORE.java src/main/gov/nasa/jpf/jvm/bytecode/SIPUSH.java src/main/gov/nasa/jpf/jvm/bytecode/SWAP.java src/main/gov/nasa/jpf/jvm/bytecode/StaticFieldInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/SwitchInstruction.java src/main/gov/nasa/jpf/jvm/bytecode/TABLESWITCH.java src/main/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java src/main/gov/nasa/jpf/jvm/bytecode/WIDE.java src/main/gov/nasa/jpf/listener/AssertionProperty.java src/main/gov/nasa/jpf/listener/BudgetChecker.java src/main/gov/nasa/jpf/listener/CGMonitor.java src/main/gov/nasa/jpf/listener/CGRemover.java src/main/gov/nasa/jpf/listener/CallMonitor.java src/main/gov/nasa/jpf/listener/ChoiceSelector.java src/main/gov/nasa/jpf/listener/ChoiceTracker.java src/main/gov/nasa/jpf/listener/CoverageAnalyzer.java src/main/gov/nasa/jpf/listener/DeadlockAnalyzer.java src/main/gov/nasa/jpf/listener/DistributedSimpleDot.java src/main/gov/nasa/jpf/listener/EndlessLoopDetector.java src/main/gov/nasa/jpf/listener/ErrorTraceGenerator.java src/main/gov/nasa/jpf/listener/ExceptionInjector.java src/main/gov/nasa/jpf/listener/ExecTracker.java src/main/gov/nasa/jpf/listener/HeapTracker.java src/main/gov/nasa/jpf/listener/IdleFilter.java src/main/gov/nasa/jpf/listener/InsnCounter.java src/main/gov/nasa/jpf/listener/LockedStackDepth.java src/main/gov/nasa/jpf/listener/LogConsole.java src/main/gov/nasa/jpf/listener/MethodAnalyzer.java src/main/gov/nasa/jpf/listener/MethodTracker.java src/main/gov/nasa/jpf/listener/NoStateCycles.java src/main/gov/nasa/jpf/listener/NullTracker.java src/main/gov/nasa/jpf/listener/NumericValueChecker.java src/main/gov/nasa/jpf/listener/OOMEInjector.java src/main/gov/nasa/jpf/listener/ObjectTracker.java src/main/gov/nasa/jpf/listener/OverlappingMethodAnalyzer.java src/main/gov/nasa/jpf/listener/PathOutputMonitor.java src/main/gov/nasa/jpf/listener/Perturbator.java src/main/gov/nasa/jpf/listener/PreciseRaceDetector.java src/main/gov/nasa/jpf/listener/ReferenceLocator.java src/main/gov/nasa/jpf/listener/SearchStats.java src/main/gov/nasa/jpf/listener/SimpleDot.java src/main/gov/nasa/jpf/listener/SimpleIdleFilter.java src/main/gov/nasa/jpf/listener/StackDepthChecker.java src/main/gov/nasa/jpf/listener/StackTracker.java src/main/gov/nasa/jpf/listener/StateCountEstimator.java src/main/gov/nasa/jpf/listener/StateSpaceAnalyzer.java src/main/gov/nasa/jpf/listener/StateSpaceDot.java src/main/gov/nasa/jpf/listener/StateTracker.java src/main/gov/nasa/jpf/listener/StopWatchFuzzer.java src/main/gov/nasa/jpf/listener/TraceStorer.java src/main/gov/nasa/jpf/listener/VarRecorder.java src/main/gov/nasa/jpf/listener/VarTracker.java src/main/gov/nasa/jpf/perturb/GenericDataAbstractor.java src/main/gov/nasa/jpf/perturb/IntOverUnder.java src/main/gov/nasa/jpf/perturb/OperandPerturbator.java src/main/gov/nasa/jpf/report/ConsolePublisher.java src/main/gov/nasa/jpf/report/Publisher.java src/main/gov/nasa/jpf/report/PublisherExtension.java src/main/gov/nasa/jpf/report/PublisherExtensionAdapter.java src/main/gov/nasa/jpf/report/Reporter.java src/main/gov/nasa/jpf/report/Statistics.java src/main/gov/nasa/jpf/report/XMLPublisher.java src/main/gov/nasa/jpf/search/DFSearch.java src/main/gov/nasa/jpf/search/PathSearch.java src/main/gov/nasa/jpf/search/RandomSearch.java src/main/gov/nasa/jpf/search/Search.java src/main/gov/nasa/jpf/search/SearchListener.java src/main/gov/nasa/jpf/search/SearchListenerAdapter.java src/main/gov/nasa/jpf/search/SearchState.java src/main/gov/nasa/jpf/search/Simulation.java src/main/gov/nasa/jpf/search/heuristic/BFSHeuristic.java src/main/gov/nasa/jpf/search/heuristic/DFSHeuristic.java src/main/gov/nasa/jpf/search/heuristic/GlobalSwitchThread.java src/main/gov/nasa/jpf/search/heuristic/HeuristicSearch.java src/main/gov/nasa/jpf/search/heuristic/HeuristicState.java src/main/gov/nasa/jpf/search/heuristic/Interleaving.java src/main/gov/nasa/jpf/search/heuristic/MinimizePreemption.java src/main/gov/nasa/jpf/search/heuristic/MostBlocked.java src/main/gov/nasa/jpf/search/heuristic/PreferThreads.java src/main/gov/nasa/jpf/search/heuristic/PrioritizedState.java src/main/gov/nasa/jpf/search/heuristic/RandomHeuristic.java src/main/gov/nasa/jpf/search/heuristic/SimplePriorityHeuristic.java src/main/gov/nasa/jpf/search/heuristic/StaticPriorityQueue.java src/main/gov/nasa/jpf/search/heuristic/UserHeuristic.java src/main/gov/nasa/jpf/tool/GenPeer.java src/main/gov/nasa/jpf/tool/PrintEvents.java src/main/gov/nasa/jpf/tool/Run.java src/main/gov/nasa/jpf/tool/RunJPF.java src/main/gov/nasa/jpf/tool/RunTest.java src/main/gov/nasa/jpf/util/ArrayByteQueue.java src/main/gov/nasa/jpf/util/ArrayIntSet.java src/main/gov/nasa/jpf/util/ArrayObjectQueue.java src/main/gov/nasa/jpf/util/Attributable.java src/main/gov/nasa/jpf/util/AvailableBufferedInputStream.java src/main/gov/nasa/jpf/util/BailOut.java src/main/gov/nasa/jpf/util/BinaryClassSource.java src/main/gov/nasa/jpf/util/BitArray.java src/main/gov/nasa/jpf/util/BitSet1024.java src/main/gov/nasa/jpf/util/BitSet256.java src/main/gov/nasa/jpf/util/BitSet64.java src/main/gov/nasa/jpf/util/BitSetN.java src/main/gov/nasa/jpf/util/ClassInfoFilter.java src/main/gov/nasa/jpf/util/CloneableObject.java src/main/gov/nasa/jpf/util/Cloner.java src/main/gov/nasa/jpf/util/CommitOutputStream.java src/main/gov/nasa/jpf/util/ConsoleStream.java src/main/gov/nasa/jpf/util/ConstGrowth.java src/main/gov/nasa/jpf/util/CountDown.java src/main/gov/nasa/jpf/util/DevNullPrintStream.java src/main/gov/nasa/jpf/util/DynamicIntArray.java src/main/gov/nasa/jpf/util/DynamicObjectArray.java src/main/gov/nasa/jpf/util/ElementCreator.java src/main/gov/nasa/jpf/util/ExpGrowth.java src/main/gov/nasa/jpf/util/FeatureSpec.java src/main/gov/nasa/jpf/util/FieldSpec.java src/main/gov/nasa/jpf/util/FieldSpecMatcher.java src/main/gov/nasa/jpf/util/FileUtils.java src/main/gov/nasa/jpf/util/FinalBitSet.java src/main/gov/nasa/jpf/util/FixedBitSet.java src/main/gov/nasa/jpf/util/Growth.java src/main/gov/nasa/jpf/util/HashData.java src/main/gov/nasa/jpf/util/HashPool.java src/main/gov/nasa/jpf/util/IdentityArrayObjectSet.java src/main/gov/nasa/jpf/util/IdentityObjectSet.java src/main/gov/nasa/jpf/util/ImmutableList.java src/main/gov/nasa/jpf/util/IndexIterator.java src/main/gov/nasa/jpf/util/InstructionState.java src/main/gov/nasa/jpf/util/IntArray.java src/main/gov/nasa/jpf/util/IntIterator.java src/main/gov/nasa/jpf/util/IntSet.java src/main/gov/nasa/jpf/util/IntTable.java src/main/gov/nasa/jpf/util/IntVector.java src/main/gov/nasa/jpf/util/Invocation.java src/main/gov/nasa/jpf/util/JPFLogger.java src/main/gov/nasa/jpf/util/JPFSiteUtils.java src/main/gov/nasa/jpf/util/Left.java src/main/gov/nasa/jpf/util/LimitedInputStream.java src/main/gov/nasa/jpf/util/LinkedObjectQueue.java src/main/gov/nasa/jpf/util/LocationSpec.java src/main/gov/nasa/jpf/util/LogHandler.java src/main/gov/nasa/jpf/util/LogManager.java src/main/gov/nasa/jpf/util/LongVector.java src/main/gov/nasa/jpf/util/MethodInfoRegistry.java src/main/gov/nasa/jpf/util/MethodSpec.java src/main/gov/nasa/jpf/util/MethodSpecMatcher.java src/main/gov/nasa/jpf/util/Misc.java src/main/gov/nasa/jpf/util/MutableInteger.java src/main/gov/nasa/jpf/util/MutableIntegerRestorer.java src/main/gov/nasa/jpf/util/OATHash.java src/main/gov/nasa/jpf/util/ObjArray.java src/main/gov/nasa/jpf/util/ObjVector.java src/main/gov/nasa/jpf/util/ObjectConverter.java src/main/gov/nasa/jpf/util/ObjectList.java src/main/gov/nasa/jpf/util/ObjectQueue.java src/main/gov/nasa/jpf/util/ObjectSet.java src/main/gov/nasa/jpf/util/PSIntMap.java src/main/gov/nasa/jpf/util/Pair.java src/main/gov/nasa/jpf/util/PathnameExpander.java src/main/gov/nasa/jpf/util/Permutation.java src/main/gov/nasa/jpf/util/Predicate.java src/main/gov/nasa/jpf/util/PrintUtils.java src/main/gov/nasa/jpf/util/Printable.java src/main/gov/nasa/jpf/util/Processor.java src/main/gov/nasa/jpf/util/ReadOnlyObjList.java src/main/gov/nasa/jpf/util/Reflection.java src/main/gov/nasa/jpf/util/RepositoryEntry.java src/main/gov/nasa/jpf/util/Result.java src/main/gov/nasa/jpf/util/Right.java src/main/gov/nasa/jpf/util/RunListener.java src/main/gov/nasa/jpf/util/RunRegistry.java src/main/gov/nasa/jpf/util/SimplePool.java src/main/gov/nasa/jpf/util/SortedArrayIntSet.java src/main/gov/nasa/jpf/util/SortedArrayObjectSet.java src/main/gov/nasa/jpf/util/Source.java src/main/gov/nasa/jpf/util/SourceRef.java src/main/gov/nasa/jpf/util/SparseClusterArray.java src/main/gov/nasa/jpf/util/SparseIntVector.java src/main/gov/nasa/jpf/util/SparseObjVector.java src/main/gov/nasa/jpf/util/SplitInputStream.java src/main/gov/nasa/jpf/util/SplitOutputStream.java src/main/gov/nasa/jpf/util/StateExtensionClient.java src/main/gov/nasa/jpf/util/StateExtensionListener.java src/main/gov/nasa/jpf/util/StringExpander.java src/main/gov/nasa/jpf/util/StringMatcher.java src/main/gov/nasa/jpf/util/StringSetMatcher.java src/main/gov/nasa/jpf/util/StructuredPrinter.java src/main/gov/nasa/jpf/util/Trace.java src/main/gov/nasa/jpf/util/TraceElement.java src/main/gov/nasa/jpf/util/Transformer.java src/main/gov/nasa/jpf/util/TwoTypeComparator.java src/main/gov/nasa/jpf/util/TypeRef.java src/main/gov/nasa/jpf/util/TypeSpec.java src/main/gov/nasa/jpf/util/TypeSpecMatcher.java src/main/gov/nasa/jpf/util/UnsortedArrayIntSet.java src/main/gov/nasa/jpf/util/VarSpec.java src/main/gov/nasa/jpf/util/WeakPool.java src/main/gov/nasa/jpf/util/automaton/Automaton.java src/main/gov/nasa/jpf/util/automaton/State.java src/main/gov/nasa/jpf/util/automaton/Transition.java src/main/gov/nasa/jpf/util/event/CheckEvent.java src/main/gov/nasa/jpf/util/event/Event.java src/main/gov/nasa/jpf/util/event/EventChoiceGenerator.java src/main/gov/nasa/jpf/util/event/EventConstructor.java src/main/gov/nasa/jpf/util/event/EventForest.java src/main/gov/nasa/jpf/util/event/EventTree.java src/main/gov/nasa/jpf/util/event/NoEvent.java src/main/gov/nasa/jpf/util/event/TestEventTree.java src/main/gov/nasa/jpf/util/json/AbstractValue.java src/main/gov/nasa/jpf/util/json/ArrayValue.java src/main/gov/nasa/jpf/util/json/BooleanValue.java src/main/gov/nasa/jpf/util/json/CGCall.java src/main/gov/nasa/jpf/util/json/CGCreator.java src/main/gov/nasa/jpf/util/json/CGCreatorFactory.java src/main/gov/nasa/jpf/util/json/Creator.java src/main/gov/nasa/jpf/util/json/CreatorsFactory.java src/main/gov/nasa/jpf/util/json/DoubleValue.java src/main/gov/nasa/jpf/util/json/JSONLexer.java src/main/gov/nasa/jpf/util/json/JSONObject.java src/main/gov/nasa/jpf/util/json/JSONObjectValue.java src/main/gov/nasa/jpf/util/json/JSONParser.java src/main/gov/nasa/jpf/util/json/NullValue.java src/main/gov/nasa/jpf/util/json/StringValue.java src/main/gov/nasa/jpf/util/json/Token.java src/main/gov/nasa/jpf/util/json/Value.java src/main/gov/nasa/jpf/util/script/Alternative.java src/main/gov/nasa/jpf/util/script/ESParser.java src/main/gov/nasa/jpf/util/script/ElementProcessor.java src/main/gov/nasa/jpf/util/script/Event.java src/main/gov/nasa/jpf/util/script/EventFactory.java src/main/gov/nasa/jpf/util/script/EventGenerator.java src/main/gov/nasa/jpf/util/script/EventGeneratorFactory.java src/main/gov/nasa/jpf/util/script/Repetition.java src/main/gov/nasa/jpf/util/script/Script.java src/main/gov/nasa/jpf/util/script/ScriptElement.java src/main/gov/nasa/jpf/util/script/ScriptElementContainer.java src/main/gov/nasa/jpf/util/script/ScriptEnvironment.java src/main/gov/nasa/jpf/util/script/Section.java src/main/gov/nasa/jpf/util/script/SequenceInterpreter.java src/main/gov/nasa/jpf/util/script/StringExpander.java src/main/gov/nasa/jpf/util/script/StringSetGenerator.java src/main/gov/nasa/jpf/util/test/JPF_gov_nasa_jpf_util_test_TestJPF.java src/main/gov/nasa/jpf/util/test/JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF.java src/main/gov/nasa/jpf/util/test/TestJPF.java src/main/gov/nasa/jpf/util/test/TestMultiProcessJPF.java src/main/gov/nasa/jpf/vm/AbstractRestorer.java src/main/gov/nasa/jpf/vm/AbstractSerializer.java src/main/gov/nasa/jpf/vm/AbstractTypeAnnotationInfo.java src/main/gov/nasa/jpf/vm/AllRunnablesSyncPolicy.java src/main/gov/nasa/jpf/vm/Allocation.java src/main/gov/nasa/jpf/vm/AllocationContext.java src/main/gov/nasa/jpf/vm/AnnotationInfo.java src/main/gov/nasa/jpf/vm/AnnotationParser.java src/main/gov/nasa/jpf/vm/ApplicationContext.java src/main/gov/nasa/jpf/vm/ArrayAccess.java src/main/gov/nasa/jpf/vm/ArrayFields.java src/main/gov/nasa/jpf/vm/ArrayIndexOutOfBoundsExecutiveException.java src/main/gov/nasa/jpf/vm/ArrayOffset.java src/main/gov/nasa/jpf/vm/AtomicData.java src/main/gov/nasa/jpf/vm/Attributor.java src/main/gov/nasa/jpf/vm/Backtracker.java src/main/gov/nasa/jpf/vm/BooleanArrayFields.java src/main/gov/nasa/jpf/vm/BooleanChoiceGenerator.java src/main/gov/nasa/jpf/vm/BooleanFieldInfo.java src/main/gov/nasa/jpf/vm/BootstrapMethodInfo.java src/main/gov/nasa/jpf/vm/BoxObjectCacheManager.java src/main/gov/nasa/jpf/vm/ByteArrayFields.java src/main/gov/nasa/jpf/vm/ByteFieldInfo.java src/main/gov/nasa/jpf/vm/BytecodeAnnotationInfo.java src/main/gov/nasa/jpf/vm/BytecodeTypeParameterAnnotationInfo.java src/main/gov/nasa/jpf/vm/CharArrayFields.java src/main/gov/nasa/jpf/vm/CharFieldInfo.java src/main/gov/nasa/jpf/vm/ChoiceGenerator.java src/main/gov/nasa/jpf/vm/ChoiceGeneratorBase.java src/main/gov/nasa/jpf/vm/ChoicePoint.java src/main/gov/nasa/jpf/vm/ClassChangeException.java src/main/gov/nasa/jpf/vm/ClassFileContainer.java src/main/gov/nasa/jpf/vm/ClassFileMatch.java src/main/gov/nasa/jpf/vm/ClassInfo.java src/main/gov/nasa/jpf/vm/ClassInfoException.java src/main/gov/nasa/jpf/vm/ClassLoaderInfo.java src/main/gov/nasa/jpf/vm/ClassLoaderList.java src/main/gov/nasa/jpf/vm/ClassParseException.java src/main/gov/nasa/jpf/vm/ClassPath.java src/main/gov/nasa/jpf/vm/ClinitRequired.java src/main/gov/nasa/jpf/vm/ClosedMemento.java src/main/gov/nasa/jpf/vm/CollapsePools.java src/main/gov/nasa/jpf/vm/ConstInsnPathTime.java src/main/gov/nasa/jpf/vm/DebugJenkinsStateSet.java src/main/gov/nasa/jpf/vm/DebugStateSerializer.java src/main/gov/nasa/jpf/vm/DefaultBacktracker.java src/main/gov/nasa/jpf/vm/DefaultFieldsFactory.java src/main/gov/nasa/jpf/vm/DefaultMementoRestorer.java src/main/gov/nasa/jpf/vm/DelegatingScheduler.java src/main/gov/nasa/jpf/vm/DirectCallStackFrame.java src/main/gov/nasa/jpf/vm/DoubleArrayFields.java src/main/gov/nasa/jpf/vm/DoubleChoiceGenerator.java src/main/gov/nasa/jpf/vm/DoubleFieldInfo.java src/main/gov/nasa/jpf/vm/DoubleSlotFieldInfo.java src/main/gov/nasa/jpf/vm/DynamicElementInfo.java src/main/gov/nasa/jpf/vm/ElementInfo.java src/main/gov/nasa/jpf/vm/ExceptionHandler.java src/main/gov/nasa/jpf/vm/ExceptionInfo.java src/main/gov/nasa/jpf/vm/ExceptionParameterAnnotationInfo.java src/main/gov/nasa/jpf/vm/FieldInfo.java src/main/gov/nasa/jpf/vm/FieldLockInfo.java src/main/gov/nasa/jpf/vm/FieldLockInfoFactory.java src/main/gov/nasa/jpf/vm/Fields.java src/main/gov/nasa/jpf/vm/FieldsFactory.java src/main/gov/nasa/jpf/vm/FinalizerThreadInfo.java src/main/gov/nasa/jpf/vm/FloatArrayFields.java src/main/gov/nasa/jpf/vm/FloatChoiceGenerator.java src/main/gov/nasa/jpf/vm/FloatFieldInfo.java src/main/gov/nasa/jpf/vm/FormalParameterAnnotationInfo.java src/main/gov/nasa/jpf/vm/FullStateSet.java src/main/gov/nasa/jpf/vm/FunctionObjectFactory.java src/main/gov/nasa/jpf/vm/GenericHeap.java src/main/gov/nasa/jpf/vm/GenericSGOIDHeap.java src/main/gov/nasa/jpf/vm/GenericSharednessPolicy.java src/main/gov/nasa/jpf/vm/GenericSignatureHolder.java src/main/gov/nasa/jpf/vm/GlobalSchedulingPoint.java src/main/gov/nasa/jpf/vm/GlobalSharednessPolicy.java src/main/gov/nasa/jpf/vm/HandlerContext.java src/main/gov/nasa/jpf/vm/HashedAllocationContext.java src/main/gov/nasa/jpf/vm/Heap.java src/main/gov/nasa/jpf/vm/IncrementalChangeTracker.java src/main/gov/nasa/jpf/vm/InfoObject.java src/main/gov/nasa/jpf/vm/Instruction.java src/main/gov/nasa/jpf/vm/IntArrayFields.java src/main/gov/nasa/jpf/vm/IntChoiceGenerator.java src/main/gov/nasa/jpf/vm/IntegerFieldInfo.java src/main/gov/nasa/jpf/vm/IsEndStateProperty.java src/main/gov/nasa/jpf/vm/JPFOutputStream.java src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java src/main/gov/nasa/jpf/vm/JenkinsStateSet.java src/main/gov/nasa/jpf/vm/KernelState.java src/main/gov/nasa/jpf/vm/LoadOnJPFRequired.java src/main/gov/nasa/jpf/vm/LocalVarInfo.java src/main/gov/nasa/jpf/vm/LockSetThresholdFli.java src/main/gov/nasa/jpf/vm/LongArrayFields.java src/main/gov/nasa/jpf/vm/LongChoiceGenerator.java src/main/gov/nasa/jpf/vm/LongFieldInfo.java src/main/gov/nasa/jpf/vm/MJIEnv.java src/main/gov/nasa/jpf/vm/Memento.java src/main/gov/nasa/jpf/vm/MementoFactory.java src/main/gov/nasa/jpf/vm/MementoRestorer.java src/main/gov/nasa/jpf/vm/MethodInfo.java src/main/gov/nasa/jpf/vm/MethodLocator.java src/main/gov/nasa/jpf/vm/Monitor.java src/main/gov/nasa/jpf/vm/MultiProcessVM.java src/main/gov/nasa/jpf/vm/NamedFields.java src/main/gov/nasa/jpf/vm/NativeMethodInfo.java src/main/gov/nasa/jpf/vm/NativePeer.java src/main/gov/nasa/jpf/vm/NativeStackFrame.java src/main/gov/nasa/jpf/vm/NativeStateHolder.java src/main/gov/nasa/jpf/vm/NoOutOfMemoryErrorProperty.java src/main/gov/nasa/jpf/vm/NoUncaughtExceptionsProperty.java src/main/gov/nasa/jpf/vm/NotDeadlockedProperty.java src/main/gov/nasa/jpf/vm/OVHeap.java src/main/gov/nasa/jpf/vm/OVStatics.java src/main/gov/nasa/jpf/vm/ObjRef.java src/main/gov/nasa/jpf/vm/PSIMHeap.java src/main/gov/nasa/jpf/vm/Path.java src/main/gov/nasa/jpf/vm/PathSharednessPolicy.java src/main/gov/nasa/jpf/vm/PersistentLockSetThresholdFli.java src/main/gov/nasa/jpf/vm/PersistentSingleLockThresholdFli.java src/main/gov/nasa/jpf/vm/PersistentTidSet.java src/main/gov/nasa/jpf/vm/PreciseAllocationContext.java src/main/gov/nasa/jpf/vm/PredicateMap.java src/main/gov/nasa/jpf/vm/PriorityRunnablesSyncPolicy.java src/main/gov/nasa/jpf/vm/ReferenceArrayFields.java src/main/gov/nasa/jpf/vm/ReferenceChoiceGenerator.java src/main/gov/nasa/jpf/vm/ReferenceFieldInfo.java src/main/gov/nasa/jpf/vm/ReferenceProcessor.java src/main/gov/nasa/jpf/vm/ReleaseAction.java src/main/gov/nasa/jpf/vm/Restorable.java src/main/gov/nasa/jpf/vm/RestorableVMState.java src/main/gov/nasa/jpf/vm/Scheduler.java src/main/gov/nasa/jpf/vm/SerializingStateSet.java src/main/gov/nasa/jpf/vm/SharednessPolicy.java src/main/gov/nasa/jpf/vm/ShortArrayFields.java src/main/gov/nasa/jpf/vm/ShortFieldInfo.java src/main/gov/nasa/jpf/vm/SingleLockThresholdFli.java src/main/gov/nasa/jpf/vm/SingleProcessVM.java src/main/gov/nasa/jpf/vm/SingleSlotFieldInfo.java src/main/gov/nasa/jpf/vm/StackFrame.java src/main/gov/nasa/jpf/vm/StateRestorer.java src/main/gov/nasa/jpf/vm/StateSerializer.java src/main/gov/nasa/jpf/vm/StateSet.java src/main/gov/nasa/jpf/vm/StaticElementInfo.java src/main/gov/nasa/jpf/vm/Statics.java src/main/gov/nasa/jpf/vm/StatisticFieldLockInfoFactory.java src/main/gov/nasa/jpf/vm/Step.java src/main/gov/nasa/jpf/vm/Storable.java src/main/gov/nasa/jpf/vm/SuperTypeAnnotationInfo.java src/main/gov/nasa/jpf/vm/SyncPolicy.java src/main/gov/nasa/jpf/vm/SystemClassLoaderInfo.java src/main/gov/nasa/jpf/vm/SystemState.java src/main/gov/nasa/jpf/vm/SystemTime.java src/main/gov/nasa/jpf/vm/ThreadChoiceGenerator.java src/main/gov/nasa/jpf/vm/ThreadData.java src/main/gov/nasa/jpf/vm/ThreadInfo.java src/main/gov/nasa/jpf/vm/ThreadInfoSet.java src/main/gov/nasa/jpf/vm/ThreadList.java src/main/gov/nasa/jpf/vm/ThresholdFieldLockInfo.java src/main/gov/nasa/jpf/vm/ThrowsAnnotationInfo.java src/main/gov/nasa/jpf/vm/TidSet.java src/main/gov/nasa/jpf/vm/TimeModel.java src/main/gov/nasa/jpf/vm/Transition.java src/main/gov/nasa/jpf/vm/TypeAnnotationInfo.java src/main/gov/nasa/jpf/vm/TypeParameterAnnotationInfo.java src/main/gov/nasa/jpf/vm/TypeParameterBoundAnnotationInfo.java src/main/gov/nasa/jpf/vm/Types.java src/main/gov/nasa/jpf/vm/UncaughtException.java src/main/gov/nasa/jpf/vm/VM.java src/main/gov/nasa/jpf/vm/VMListener.java src/main/gov/nasa/jpf/vm/VariableAnnotationInfo.java src/main/gov/nasa/jpf/vm/Verify.java src/main/gov/nasa/jpf/vm/bytecode/ArrayElementInstruction.java src/main/gov/nasa/jpf/vm/bytecode/FieldInstruction.java src/main/gov/nasa/jpf/vm/bytecode/InstanceFieldInstruction.java src/main/gov/nasa/jpf/vm/bytecode/InstanceInvokeInstruction.java src/main/gov/nasa/jpf/vm/bytecode/InstructionInterface.java src/main/gov/nasa/jpf/vm/bytecode/InvokeInstruction.java src/main/gov/nasa/jpf/vm/bytecode/LocalVariableInstruction.java src/main/gov/nasa/jpf/vm/bytecode/LookupSwitchInstruction.java src/main/gov/nasa/jpf/vm/bytecode/NewInstruction.java src/main/gov/nasa/jpf/vm/bytecode/ReadInstruction.java src/main/gov/nasa/jpf/vm/bytecode/ReadOrWriteInstruction.java src/main/gov/nasa/jpf/vm/bytecode/ReturnInstruction.java src/main/gov/nasa/jpf/vm/bytecode/ReturnValueInstruction.java src/main/gov/nasa/jpf/vm/bytecode/StaticFieldInstruction.java src/main/gov/nasa/jpf/vm/bytecode/StoreInstruction.java src/main/gov/nasa/jpf/vm/bytecode/TableSwitchInstruction.java src/main/gov/nasa/jpf/vm/bytecode/WriteInstruction.java src/main/gov/nasa/jpf/vm/choice/BreakGenerator.java src/main/gov/nasa/jpf/vm/choice/CompoundChoiceGenerator.java src/main/gov/nasa/jpf/vm/choice/DoubleChoiceFromList.java src/main/gov/nasa/jpf/vm/choice/DoubleChoiceFromSet.java src/main/gov/nasa/jpf/vm/choice/DoubleSpec.java src/main/gov/nasa/jpf/vm/choice/DoubleThresholdGenerator.java src/main/gov/nasa/jpf/vm/choice/ExceptionThreadChoiceFromSet.java src/main/gov/nasa/jpf/vm/choice/ExposureCG.java src/main/gov/nasa/jpf/vm/choice/FloatChoiceFromList.java src/main/gov/nasa/jpf/vm/choice/IntChoiceFromList.java src/main/gov/nasa/jpf/vm/choice/IntChoiceFromSet.java src/main/gov/nasa/jpf/vm/choice/IntIntervalGenerator.java src/main/gov/nasa/jpf/vm/choice/InvocationCG.java src/main/gov/nasa/jpf/vm/choice/LongChoiceFromList.java src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java src/main/gov/nasa/jpf/vm/choice/RandomIntIntervalGenerator.java src/main/gov/nasa/jpf/vm/choice/RandomOrderIntCG.java src/main/gov/nasa/jpf/vm/choice/RandomOrderLongCG.java src/main/gov/nasa/jpf/vm/choice/ThreadChoiceFromSet.java src/main/gov/nasa/jpf/vm/choice/TypedObjectChoice.java src/main/gov/nasa/jpf/vm/serialize/Abstraction.java src/main/gov/nasa/jpf/vm/serialize/AbstractionAdapter.java src/main/gov/nasa/jpf/vm/serialize/AdaptiveSerializer.java src/main/gov/nasa/jpf/vm/serialize/AmmendableFilterConfiguration.java src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java src/main/gov/nasa/jpf/vm/serialize/DebugCFSerializer.java src/main/gov/nasa/jpf/vm/serialize/DebugFilteringSerializer.java src/main/gov/nasa/jpf/vm/serialize/DefaultFilterConfiguration.java src/main/gov/nasa/jpf/vm/serialize/DynamicAbstractionSerializer.java src/main/gov/nasa/jpf/vm/serialize/FieldAmmendmentByName.java src/main/gov/nasa/jpf/vm/serialize/FilterConfiguration.java src/main/gov/nasa/jpf/vm/serialize/FilterFrame.java src/main/gov/nasa/jpf/vm/serialize/FilteringSerializer.java src/main/gov/nasa/jpf/vm/serialize/FramePolicy.java src/main/gov/nasa/jpf/vm/serialize/IgnoreConstants.java src/main/gov/nasa/jpf/vm/serialize/IgnoreReflectiveNames.java src/main/gov/nasa/jpf/vm/serialize/IgnoreThreadNastiness.java src/main/gov/nasa/jpf/vm/serialize/IgnoreUtilSilliness.java src/main/gov/nasa/jpf/vm/serialize/Ignored.java src/main/gov/nasa/jpf/vm/serialize/IgnoresFromAnnotations.java src/main/gov/nasa/jpf/vm/serialize/IncludesFromAnnotations.java src/main/gov/nasa/jpf/vm/serialize/TopFrameSerializer.java src/main/gov/nasa/jpf/vm/serialize/UnfilterField.java src/peers/gov/nasa/jpf/vm/AtomicFieldUpdater.java src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_AnnotationProxyBase.java src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_CachedROHttpConnection.java src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_ConsoleOutputStream.java src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_DelegatingTimeZone.java src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_EventProducer.java src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_FinalizerThread.java src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_SerializationConstructor.java src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_test_MemoryGoal.java src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_tools_MethodTester.java src/peers/gov/nasa/jpf/vm/JPF_java_io_File.java src/peers/gov/nasa/jpf/vm/JPF_java_io_FileDescriptor.java src/peers/gov/nasa/jpf/vm/JPF_java_io_InputStreamReader.java src/peers/gov/nasa/jpf/vm/JPF_java_io_ObjectInputStream.java src/peers/gov/nasa/jpf/vm/JPF_java_io_ObjectOutputStream.java src/peers/gov/nasa/jpf/vm/JPF_java_io_ObjectStreamClass.java src/peers/gov/nasa/jpf/vm/JPF_java_io_OutputStreamWriter.java src/peers/gov/nasa/jpf/vm/JPF_java_io_RandomAccessFile.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Boolean.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Byte.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Character.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_ClassLoader.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Double.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Float.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Integer.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Long.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Math.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Object.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Runtime.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Short.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringBuffer.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringBuilder.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringCoding.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_System.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Thread.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_ThreadLocal.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_Throwable.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Array.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Constructor.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Field.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Proxy.java src/peers/gov/nasa/jpf/vm/JPF_java_net_URLClassLoader.java src/peers/gov/nasa/jpf/vm/JPF_java_net_URLDecoder.java src/peers/gov/nasa/jpf/vm/JPF_java_net_URLEncoder.java src/peers/gov/nasa/jpf/vm/JPF_java_security_MessageDigest.java src/peers/gov/nasa/jpf/vm/JPF_java_text_Bidi.java src/peers/gov/nasa/jpf/vm/JPF_java_text_DateFormat.java src/peers/gov/nasa/jpf/vm/JPF_java_text_DateFormatSymbols.java src/peers/gov/nasa/jpf/vm/JPF_java_text_DecimalFormat.java src/peers/gov/nasa/jpf/vm/JPF_java_text_DecimalFormatSymbols.java src/peers/gov/nasa/jpf/vm/JPF_java_text_Format.java src/peers/gov/nasa/jpf/vm/JPF_java_text_SimpleDateFormat.java src/peers/gov/nasa/jpf/vm/JPF_java_util_Calendar.java src/peers/gov/nasa/jpf/vm/JPF_java_util_Date.java src/peers/gov/nasa/jpf/vm/JPF_java_util_Locale.java src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java src/peers/gov/nasa/jpf/vm/JPF_java_util_ResourceBundle.java src/peers/gov/nasa/jpf/vm/JPF_java_util_TimeZone.java src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_Exchanger.java src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicInteger.java src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicIntegerArray.java src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.java src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicLong.java src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicLongArray.java src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.java src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicReferenceArray.java src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.java src/peers/gov/nasa/jpf/vm/JPF_java_util_logging_Level.java src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Pattern.java src/peers/gov/nasa/jpf/vm/JPF_sun_misc_Unsafe.java src/peers/gov/nasa/jpf/vm/JPF_sun_misc_VM.java src/peers/gov/nasa/jpf/vm/JPF_sun_net_www_protocol_http_Handler.java src/peers/gov/nasa/jpf/vm/JPF_sun_reflect_Reflection.java src/peers/gov/nasa/jpf/vm/JPF_sun_reflect_ReflectionFactory.java src/tests/TypeNameTest.java src/tests/classloader_specific_tests/Class1.java src/tests/classloader_specific_tests/Class2.java src/tests/classloader_specific_tests/Class3.java src/tests/classloader_specific_tests/Interface1.java src/tests/classloader_specific_tests/Interface2.java src/tests/gov/nasa/jpf/ConfigTest.java src/tests/gov/nasa/jpf/configTestApp.jpf src/tests/gov/nasa/jpf/configTestCommon.jpf src/tests/gov/nasa/jpf/configTestIncludes.jpf src/tests/gov/nasa/jpf/configTestRequires.jpf src/tests/gov/nasa/jpf/configTestRequiresFail.jpf src/tests/gov/nasa/jpf/configTestSite.properties src/tests/gov/nasa/jpf/jvm/ClassInfoTest.java src/tests/gov/nasa/jpf/jvm/JVMStackFrameTest.java src/tests/gov/nasa/jpf/jvm/MethodInfoTest.java src/tests/gov/nasa/jpf/jvm/NonResolvedClassInfo.java src/tests/gov/nasa/jpf/test/basic/HarnessTest.java src/tests/gov/nasa/jpf/test/basic/InstructionFactoryTest.java src/tests/gov/nasa/jpf/test/basic/JPF_gov_nasa_jpf_test_basic_MJITest.java src/tests/gov/nasa/jpf/test/basic/ListenerTest.java src/tests/gov/nasa/jpf/test/basic/MJITest.java src/tests/gov/nasa/jpf/test/basic/TestJPFMainTest.java src/tests/gov/nasa/jpf/test/basic/TestJPFNoMainTest.java src/tests/gov/nasa/jpf/test/java/concurrent/AtomicIntegerFieldUpdaterTest.java src/tests/gov/nasa/jpf/test/java/concurrent/AtomicLongFieldUpdaterTest.java src/tests/gov/nasa/jpf/test/java/concurrent/AtomicReferenceFieldUpdaterTest.java src/tests/gov/nasa/jpf/test/java/concurrent/CountDownLatchTest.java src/tests/gov/nasa/jpf/test/java/concurrent/ExchangerTest.java src/tests/gov/nasa/jpf/test/java/concurrent/ExecutorServiceTest.java src/tests/gov/nasa/jpf/test/java/concurrent/SemaphoreTest.java src/tests/gov/nasa/jpf/test/java/io/BufferedInputStreamTest.java src/tests/gov/nasa/jpf/test/java/io/FileIOStreamTest.java src/tests/gov/nasa/jpf/test/java/io/FileIOTest.java src/tests/gov/nasa/jpf/test/java/io/FileTest.java src/tests/gov/nasa/jpf/test/java/io/ObjectStreamTest.java src/tests/gov/nasa/jpf/test/java/lang/BoxObjectCacheTest.java src/tests/gov/nasa/jpf/test/java/lang/ClassLoaderTest.java src/tests/gov/nasa/jpf/test/java/lang/ClassTest.java src/tests/gov/nasa/jpf/test/java/lang/CloneTest.java src/tests/gov/nasa/jpf/test/java/lang/RuntimeTest.java src/tests/gov/nasa/jpf/test/java/lang/StringTest.java src/tests/gov/nasa/jpf/test/java/lang/SystemTest.java src/tests/gov/nasa/jpf/test/java/lang/ref/WeakReferenceTest.java src/tests/gov/nasa/jpf/test/java/lang/reflect/ConstructorTest.java src/tests/gov/nasa/jpf/test/java/lang/reflect/FieldTest.java src/tests/gov/nasa/jpf/test/java/lang/reflect/MethodTest.java src/tests/gov/nasa/jpf/test/java/math/BigIntegerTest.java src/tests/gov/nasa/jpf/test/java/net/LoadUtility.java src/tests/gov/nasa/jpf/test/java/net/URLClassLoaderTest.java src/tests/gov/nasa/jpf/test/java/net/URLEncoderTest.java src/tests/gov/nasa/jpf/test/java/text/DateFormatTest.java src/tests/gov/nasa/jpf/test/java/text/DecimalFormatTest.java src/tests/gov/nasa/jpf/test/java/text/SimpleDateFormatTest.java src/tests/gov/nasa/jpf/test/mc/basic/AttrsTest.java src/tests/gov/nasa/jpf/test/mc/basic/BreakTest.java src/tests/gov/nasa/jpf/test/mc/basic/CGNotificationTest.java src/tests/gov/nasa/jpf/test/mc/basic/CGRemoverTest.java src/tests/gov/nasa/jpf/test/mc/basic/CGReorderTest.java src/tests/gov/nasa/jpf/test/mc/basic/CascadedCGTest.java src/tests/gov/nasa/jpf/test/mc/basic/ExceptionInjectorTest.java src/tests/gov/nasa/jpf/test/mc/basic/FinalBreakTest.java src/tests/gov/nasa/jpf/test/mc/basic/FinalFieldChoiceTest.java src/tests/gov/nasa/jpf/test/mc/basic/IdleLoopTest.java src/tests/gov/nasa/jpf/test/mc/basic/InvokeListenerTest.java src/tests/gov/nasa/jpf/test/mc/basic/JPF_gov_nasa_jpf_test_mc_basic_AttrsTest.java src/tests/gov/nasa/jpf/test/mc/basic/JPF_gov_nasa_jpf_test_mc_basic_InvokeListenerTest.java src/tests/gov/nasa/jpf/test/mc/basic/JPF_gov_nasa_jpf_test_mc_basic_RestorerTest$X.java src/tests/gov/nasa/jpf/test/mc/basic/LocalVarInfoTest.java src/tests/gov/nasa/jpf/test/mc/basic/MethodListenerTest.java src/tests/gov/nasa/jpf/test/mc/basic/NullTrackerTest.java src/tests/gov/nasa/jpf/test/mc/basic/OOMEInjectorTest.java src/tests/gov/nasa/jpf/test/mc/basic/OVHeapTest.java src/tests/gov/nasa/jpf/test/mc/basic/RecursiveLockTest.java src/tests/gov/nasa/jpf/test/mc/basic/RestorerTest.java src/tests/gov/nasa/jpf/test/mc/basic/SearchMultipleTest.java src/tests/gov/nasa/jpf/test/mc/basic/SharedPropagationTest.java src/tests/gov/nasa/jpf/test/mc/basic/SharedRefTest.java src/tests/gov/nasa/jpf/test/mc/basic/SkipInstructionTest.java src/tests/gov/nasa/jpf/test/mc/basic/StackDepthCheckerTest.java src/tests/gov/nasa/jpf/test/mc/basic/StatelessTest.java src/tests/gov/nasa/jpf/test/mc/basic/TraceTest.java src/tests/gov/nasa/jpf/test/mc/basic/TransitionLengthTest.java src/tests/gov/nasa/jpf/test/mc/basic/UnlockNonSharedTest.java src/tests/gov/nasa/jpf/test/mc/basic/VerifyTest.java src/tests/gov/nasa/jpf/test/mc/data/CGCreatorFactoryTest.java src/tests/gov/nasa/jpf/test/mc/data/CrossingTest.java src/tests/gov/nasa/jpf/test/mc/data/DataChoiceTest.java src/tests/gov/nasa/jpf/test/mc/data/DynamicAbstractionTest.java src/tests/gov/nasa/jpf/test/mc/data/EventGeneratorTest.java src/tests/gov/nasa/jpf/test/mc/data/JSONTest.java src/tests/gov/nasa/jpf/test/mc/data/NativeStateHolderTest.java src/tests/gov/nasa/jpf/test/mc/data/NumericValueCheckerTest.java src/tests/gov/nasa/jpf/test/mc/data/ObjectStreamTest.java src/tests/gov/nasa/jpf/test/mc/data/PerturbatorTest.java src/tests/gov/nasa/jpf/test/mc/data/RandomTest.java src/tests/gov/nasa/jpf/test/mc/data/StopWatchFuzzerTest.java src/tests/gov/nasa/jpf/test/mc/data/TimeModelTest.java src/tests/gov/nasa/jpf/test/mc/threads/AtomicTest.java src/tests/gov/nasa/jpf/test/mc/threads/ClinitTest.java src/tests/gov/nasa/jpf/test/mc/threads/DaemonTest.java src/tests/gov/nasa/jpf/test/mc/threads/DeadlockTest.java src/tests/gov/nasa/jpf/test/mc/threads/ExceptionalThreadChoiceTest.java src/tests/gov/nasa/jpf/test/mc/threads/FinalizerThreadTest.java src/tests/gov/nasa/jpf/test/mc/threads/HORaceTest.java src/tests/gov/nasa/jpf/test/mc/threads/JPF_gov_nasa_jpf_test_mc_threads_ExceptionalThreadChoiceTest.java src/tests/gov/nasa/jpf/test/mc/threads/MinimizePreemptionTest.java src/tests/gov/nasa/jpf/test/mc/threads/MissedPathTest.java src/tests/gov/nasa/jpf/test/mc/threads/OldClassicTest.java src/tests/gov/nasa/jpf/test/mc/threads/RaceTest.java src/tests/gov/nasa/jpf/test/mc/threads/SchedulesTest-output src/tests/gov/nasa/jpf/test/mc/threads/SchedulesTest.java src/tests/gov/nasa/jpf/test/vm/basic/AnnotationTest.java src/tests/gov/nasa/jpf/test/vm/basic/ArrayTest.java src/tests/gov/nasa/jpf/test/vm/basic/AssertTest.java src/tests/gov/nasa/jpf/test/vm/basic/CastTest.java src/tests/gov/nasa/jpf/test/vm/basic/EndStateListener.java src/tests/gov/nasa/jpf/test/vm/basic/EndStateTest.java src/tests/gov/nasa/jpf/test/vm/basic/EnumTest.java src/tests/gov/nasa/jpf/test/vm/basic/ExceptionHandlingTest.java src/tests/gov/nasa/jpf/test/vm/basic/FieldTest.java src/tests/gov/nasa/jpf/test/vm/basic/InitializeInterfaceClassObjectRefTest.java src/tests/gov/nasa/jpf/test/vm/basic/LargeCodeTest.java src/tests/gov/nasa/jpf/test/vm/basic/MethodTest.java src/tests/gov/nasa/jpf/test/vm/basic/OutOfMemoryErrorTest.java src/tests/gov/nasa/jpf/test/vm/basic/RecursiveClinitTest.java src/tests/gov/nasa/jpf/test/vm/reflection/ArrayTest.java src/tests/gov/nasa/jpf/test/vm/reflection/ConstructorTest.java src/tests/gov/nasa/jpf/test/vm/reflection/FieldTest.java src/tests/gov/nasa/jpf/test/vm/reflection/MethodTest.java src/tests/gov/nasa/jpf/test/vm/reflection/ProxyTest.java src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java src/tests/gov/nasa/jpf/test/vm/threads/InterruptTest.java src/tests/gov/nasa/jpf/test/vm/threads/JoinTest.java src/tests/gov/nasa/jpf/test/vm/threads/LockedStackDepthTest.java src/tests/gov/nasa/jpf/test/vm/threads/SuspendResumeTest.java src/tests/gov/nasa/jpf/test/vm/threads/ThreadExceptionHandlerTest.java src/tests/gov/nasa/jpf/test/vm/threads/ThreadStopTest.java src/tests/gov/nasa/jpf/test/vm/threads/ThreadTest.java src/tests/gov/nasa/jpf/test/vm/threads/WaitTest.java src/tests/gov/nasa/jpf/test/xerces/SAXParserTest.java src/tests/gov/nasa/jpf/test/xerces/http%^^www.puppycrawl.com^dtds^configuration_1_3.dtd src/tests/gov/nasa/jpf/test/xerces/sun_checks.xml src/tests/gov/nasa/jpf/util/ArrayIntSetTestBase.java src/tests/gov/nasa/jpf/util/ArrayObjectQueueTest.java src/tests/gov/nasa/jpf/util/AvailableBufferedInputStreamTest.java src/tests/gov/nasa/jpf/util/BitSet1024Test.java src/tests/gov/nasa/jpf/util/BitSet256Test.java src/tests/gov/nasa/jpf/util/BitSet64Test.java src/tests/gov/nasa/jpf/util/CommitOutputStreamTest.java src/tests/gov/nasa/jpf/util/IdentityArrayObjectSetTest.java src/tests/gov/nasa/jpf/util/IntTableTest.java src/tests/gov/nasa/jpf/util/IntVectorTest.java src/tests/gov/nasa/jpf/util/LimitedInputStreamTest.java src/tests/gov/nasa/jpf/util/LocationSpecTest.java src/tests/gov/nasa/jpf/util/MethodSpecTest.java src/tests/gov/nasa/jpf/util/OATHashTest.java src/tests/gov/nasa/jpf/util/ObjVectorTest.java src/tests/gov/nasa/jpf/util/ObjectListTest.java src/tests/gov/nasa/jpf/util/PSIntMapTest.java src/tests/gov/nasa/jpf/util/SortedArrayIntSetTest.java src/tests/gov/nasa/jpf/util/SortedArrayObjectSetTest.java src/tests/gov/nasa/jpf/util/SparseClusterArrayTest.java src/tests/gov/nasa/jpf/util/SparseIntVectorTest.java src/tests/gov/nasa/jpf/util/SplitInputStreamTest.java src/tests/gov/nasa/jpf/util/SplitOutputStreamTest.java src/tests/gov/nasa/jpf/util/UnsortedArrayIntSetTest.java src/tests/gov/nasa/jpf/util/event/EventTreeTest.java src/tests/gov/nasa/jpf/util/json/JSONLexerTest.java src/tests/gov/nasa/jpf/util/json/JSONParserTest.java src/tests/gov/nasa/jpf/vm/AnnotationInfoTest.java src/tests/gov/nasa/jpf/vm/ClassLoaderInfoTest.java src/tests/gov/nasa/jpf/vm/ElementInfoTest.java src/tests/gov/nasa/jpf/vm/SystemStateTest.java src/tests/gov/nasa/jpf/vm/TypesTest.java src/tests/gov/nasa/jpf/vm/choice/IntChoiceFromListTest.java src/tests/gov/nasa/jpf/vm/choice/IntChoiceFromSetTest.java src/tests/gov/nasa/jpf/vm/multiProcess/FinalizerThreadTest.java src/tests/gov/nasa/jpf/vm/multiProcess/JPF_gov_nasa_jpf_vm_multiProcess_MethodTest.java src/tests/gov/nasa/jpf/vm/multiProcess/JPF_gov_nasa_jpf_vm_multiProcess_NativePeerTest.java src/tests/gov/nasa/jpf/vm/multiProcess/JPF_gov_nasa_jpf_vm_multiProcess_ThreadTest.java src/tests/gov/nasa/jpf/vm/multiProcess/JPF_gov_nasa_jpf_vm_multiProcess_TypeSeparationTest.java src/tests/gov/nasa/jpf/vm/multiProcess/MethodTest.java src/tests/gov/nasa/jpf/vm/multiProcess/NativePeerTest.java src/tests/gov/nasa/jpf/vm/multiProcess/StringTest.java src/tests/gov/nasa/jpf/vm/multiProcess/ThreadTest.java src/tests/gov/nasa/jpf/vm/multiProcess/TypeSeparationTest.java src/tests/java8/DefaultMethodTest.java src/tests/java8/LambdaTest.java src/tests/java8/TypeAnnotationTest.java
diffstat 1186 files changed, 182080 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/.classpath	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,11 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<classpath>
+	<classpathentry kind="src" output="build/main" path="src/main"/>
+	<classpathentry kind="src" output="build/peers" path="src/peers"/>
+	<classpathentry kind="src" output="build/classes" path="src/classes"/>
+	<classpathentry kind="src" output="build/annotations" path="src/annotations"/>
+	<classpathentry kind="src" output="build/examples" path="src/examples"/>
+	<classpathentry kind="src" output="build/tests" path="src/tests"/>
+	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
+	<classpathentry kind="output" path="build"/>
+</classpath>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/.hgignore	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,13 @@
+syntax: glob
+
+local.properties
+.version
+nbproject/private/*
+build/*
+dist/*
+tmp/*
+trace
+activity*.png
+*.class
+*~
+*.DS_Store
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/.project	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,26 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>jpf-core</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+    <buildCommand>
+      <name>org.eclipse.jdt.core.javabuilder</name>
+      <arguments>
+      </arguments>
+    </buildCommand>
+ 		<buildCommand>
+			<name>org.eclipse.ui.externaltools.ExternalToolBuilder</name>
+			<arguments>
+				<dictionary>
+					<key>LaunchConfigHandle</key>
+					<value>&lt;project&gt;/eclipse/AntBuilder.launch</value>
+				</dictionary>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>org.eclipse.jdt.core.javanature</nature>
+	</natures>
+</projectDescription>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/LICENSE-2.0.txt	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,202 @@
+
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/README	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,36 @@
+                          Java PathFinder README
+                          ======================
+
+========General Information about JPF ===================
+
+All the latest developments, changes, documentation can
+be found at: 
+
+http://babelfish.arc.nasa.gov/trac/jpf/wiki
+
+
+========Building and Installing =========================
+
+If you are having problems installing and running JPF
+please look at the documentation on the wiki at:
+
+http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/start
+
+A lot of the commonly problems during the install and build
+process have been documented on the wiki. Please make sure
+that the the issue you are running into is not addressed
+there; if is not then feel free to contact us at
+java-pathfinder@googlegroups.com
+
+
+======Documentation======================================
+
+There is a constant effort to update and add JPF
+documentation on the wiki. If you would like to contribute
+in that, please contact us at
+java-pathfinder@googlegroups.com
+
+
+
+Happy Verification
+-- the Java PathFinder team
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/javajpf	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,10 @@
+# shell script to start arbitrary classes through a JPFClassLoader
+
+JPF_HOME=`dirname "$0"`/..
+
+if test -z "$JVM_FLAGS"; then
+  JVM_FLAGS="-Xmx1024m -ea"
+fi
+
+
+java -ea -cp "$JPF_HOME/build/main:$JPF_HOME/build/peers:$JPF_HOME/build/annotations:$JPF_HOME/build/tests:$JPF_HOME/lib/bcel.jar:$JPF_HOME/lib/junit-4.10.jar" gov.nasa.jpf.Main -a "$@"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/jpf	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,13 @@
+#!/bin/bash
+#
+# unix shell script to run jpf
+#
+
+JPF_HOME=`dirname "$0"`/..
+
+if test -z "$JVM_FLAGS"; then
+  JVM_FLAGS="-Xmx1024m -ea"
+fi
+
+java $JVM_FLAGS -jar "$JPF_HOME/build/RunJPF.jar" "$@"
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/jpf.bat	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,13 @@
+REM
+REM overly simplified batch file to start JPF from a command prompt
+REM
+
+@echo off
+
+REM Set the JPF_HOME directory
+set JPF_HOME=%~dp0..
+
+set JVM_FLAGS=-Xmx1024m -ea
+
+java %JVM_FLAGS% -jar "%JPF_HOME%\build\RunJPF.jar" %*
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/print_class	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+JPF_HOME=`dirname "$0"`/..
+
+java -classpath "$JPF_HOME/build/jpf.jar" gov.nasa.jpf.jvm.ClassFilePrinter "$@"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/print_class.bat	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,8 @@
+
+@echo off
+
+REM Set the JPF_HOME directory
+set JPF_HOME=%~dp0..
+
+java -classpath "%JPF_HOME%\build\jpf.jar" gov.nasa.jpf.classfile.ClassFilePrinter %*
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/print_events	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+JPF_HOME=`dirname "$0"`/..
+
+java -classpath "$JPF_HOME/build/jpf.jar" gov.nasa.jpf.tool.PrintEvents "$@"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/test	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,13 @@
+#!/bin/bash
+#
+# unix shell script to run jpf
+#
+
+JPF_HOME=`dirname "$0"`/..
+
+if test -z "$JVM_FLAGS"; then
+  JVM_FLAGS="-Xmx1024m -ea"
+fi
+
+java $JVM_FLAGS -jar "$JPF_HOME/build/RunTest.jar" "$@"
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/test.bat	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,13 @@
+REM
+REM overly simplified batch file to start JPF tests from a command prompt
+REM
+
+@echo off
+
+REM Set the JPF_HOME directory
+set JPF_HOME=%~dp0..
+
+set JVM_FLAGS=-Xmx1024m -ea
+
+java %JVM_FLAGS% -jar "%JPF_HOME%\build\RunTest.jar" %*
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/build.properties	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,22 @@
+#JPF core build info
+#Fri Jan 13 13:32:58 PST 2012
+
+revision=647\:b8b86ac8f503
+
+date.tip=2012-01-13 13\:30 -0800
+
+author=Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
+
+repository=file\://flyer/Users/pmehlitz/projects/eclipse/jpf-core
+
+upstream=http\://babelfish.arc.nasa.gov/hg/jpf/jpf-core
+
+java.version=1.6.0_26
+
+os.arch=x86_64
+
+os.name=Mac OS X
+
+os.version=10.5.8
+
+user.country=US
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/build.xml	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,456 @@
+<?xml version="1.0" ?>
+
+<!--
+  build.xml - the JPF core build script
+              using Ant (http://jakarta.apache.org/ant)
+  public targets:
+
+    build (default)   compile classes and build JPF jar files
+    compile           compile JPF and its specific (modeled) environment libraries
+    test              run all JPF tests
+    clean             remove the files that have been generated by the build process
+    buildinfo         create buildinfo properties file
+-->
+
+<project name="jpf-core" default="build" basedir=".">
+
+  <!-- ===================== ===== COMMON SECTION ========================== -->
+
+  <!-- 
+    local props have to come first, because Ant properties are immutable
+    NOTE: this file is local - it is never in the repository!
+  -->
+  <property file="local.properties"/>
+  <property environment="env"/>
+  
+  <!-- compiler settings -->
+  <property name="debug"         value="on"/>
+  <property name="deprecation"   value="on"/>
+
+  <uptodate property="build_uptodate" targetfile="build/main/gov/nasa/jpf/build.properties" srcfile="build.properties"/>
+
+
+  <!-- generic classpath settings -->
+  <path id="lib.path">
+    <pathelement location="build/main"/>
+    <pathelement location="build/peers"/>
+    <pathelement location="build/annotations"/>
+    <fileset dir=".">
+  	  <include name="lib/*.jar"/>
+    </fileset>
+  </path>
+
+
+  <!-- init: common initialization -->
+  <target name="-init">
+    <tstamp/>
+
+    <mkdir dir="build"/>               <!-- the build root -->
+    
+    <!-- the things that have to be in the classpath of whatever runs Ant -->
+    <available property="have_javac" classname="com.sun.tools.javac.Main"/>
+    <fail unless="have_javac">no javac was found __or__ check http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/build for possible solutions</fail>
+
+
+    <available file="src/main"        type="dir" property="have_main"/>
+    <available file="src/annotations" type="dir" property="have_annotations"/>
+    <available file="src/peers"       type="dir" property="have_peers"/>
+    <available file="src/classes"     type="dir" property="have_classes"/>
+    <available file="src/tests"       type="dir" property="have_tests"/>
+    <available file="src/examples"    type="dir" property="have_examples"/>
+
+    <available file=".hg"             type="dir" property="have_hg"/>
+
+    <!-- for the core, it's a fail if any of these is missing -->
+    <fail unless="have_main">no src/main</fail>
+    <fail unless="have_annotations">no src/annotations</fail>
+    <fail unless="have_peers">no src/peers</fail>
+    <fail unless="have_classes">no src/classes</fail>
+    <fail unless="have_tests">no src/tests</fail>
+    <fail unless="have_examples">no src/examples</fail>
+
+    <condition property="have_java8">
+        <equals arg1="${ant.java.version}" arg2="1.8"/>
+    </condition>
+
+  </target>
+
+
+  <!-- ======================= COMPILE SECTION ============================= -->
+    
+  <!-- public compile -->
+  <target name="compile" depends="-init,-compile-annotations,-compile-main,-compile-peers,-compile-classes,-compile-tests,-compile-examples"
+          description="compile all JPF core sources" >
+	  <copy file="build.properties" todir="build/main/gov/nasa/jpf" failonerror="false"/>
+  </target>
+
+  <target name="-compile-annotations" if="have_annotations">
+    <mkdir dir="build/annotations"/>
+    <javac srcdir="src/annotations" destdir="build/annotations" includeantruntime="false"
+           debug="${debug}" deprecation="${deprecation}" classpath=""/>
+  </target>
+
+  <target name="-compile-main" if="have_main">
+    <mkdir dir="build/main"/>
+    <javac srcdir="src/main" destdir="build/main" includeantruntime="false"
+           debug="${debug}" deprecation="${deprecation}" classpathref="lib.path">
+    	<!--
+        <compilerarg value="-XDenableSunApiLintControl"/>
+        <compilerarg value="-Xlint:all"/>
+        -->
+    </javac>
+
+  </target>
+  
+  <target name="-compile-peers" if="have_peers" depends="-compile-main" >
+    <mkdir dir="build/peers"/>
+    <javac srcdir="src/peers" destdir="build/peers" includeantruntime="false"
+           debug="${debug}" deprecation="${deprecation}" classpathref="lib.path">
+    	<compilerarg value="-XDenableSunApiLintControl"/>
+    	<compilerarg value="-Xlint:all,-sunapi,-serial"/>    	
+     </javac>
+  </target>
+  
+  <target name="-compile-classes" if="have_classes" depends="-compile-annotations,-compile-main" >
+    <mkdir dir="build/classes"/>
+    <javac srcdir="src/classes" destdir="build/classes" includeantruntime="false"
+           debug="${debug}" deprecation="${deprecation}">
+      <compilerarg value="-XDenableSunApiLintControl"/>
+      <compilerarg value="-Xlint:all,-sunapi"/>   
+      <classpath>
+        <path refid="lib.path"/>
+        <pathelement location="build/annotations"/>
+      </classpath>
+    </javac>
+  </target>
+  
+  <target name="-compile-tests" if="have_tests" depends="-compile-annotations,-compile-main,-compile-classes">
+    <mkdir dir="build/tests"/>
+
+    <javac sourcepath="" srcdir="src/tests" destdir="build/tests" includeantruntime="false"
+           debug="${debug}" deprecation="${deprecation}"
+           includes="*,gov/nasa/jpf/**,classloader_specific_tests/**">
+      <compilerarg value="-XDenableSunApiLintControl"/>
+      <compilerarg value="-Xlint:all,-sunapi,-serial,-rawtypes,-unchecked"/>
+
+      <include name="*gov/nasa/jpf/**"/>
+      <include name="classloader_specific_tests/**"/>
+      <include name="java8/**" if="have_java8"/>
+
+      <classpath>
+        <path refid="lib.path"/>
+        <pathelement location="build/annotations"/>
+        <pathelement location="build/classes"/>
+      </classpath>       
+    </javac>
+  </target>
+
+  <target name="-compile-examples" if="have_examples" depends="-compile-annotations,-compile-main">
+    <mkdir dir="build/examples" />
+    <javac srcdir="src/examples" destdir="build/examples" includeantruntime="false"
+           debug="${debug}" deprecation="${deprecation}"
+           classpathref="lib.path"/>
+  </target>
+
+  
+  <!-- ======================= MISC SECTION ================================ -->
+  
+  <target name="-version" if="have_hg">
+    <exec executable="hg" outputproperty="version" searchpath="true" failonerror="false" failifexecutionfails="false">
+      <arg value="identify"/>
+      <arg value="-n"/> 
+    </exec>
+  	
+    <!-- .version is in .hgignore -->
+    <echo message="${version}${line.separator}" file=".version"/>
+  </target>
+	
+  <!-- build jars -->
+  <target name="build" depends="-cond-clean,compile,-version"
+        description="generate the core JPF jar files" >
+
+    <copy file=".version" todir="build/main/gov/nasa/jpf" failonerror="false"/>
+
+    <jar jarfile="build/jpf-classes.jar">
+      <fileset dir="build/classes"/>
+      <fileset dir="build/annotations"/>
+
+      <fileset dir="build/main">
+          <!-- we need this one in case a SUT uses the Verify API -->
+          <include name="gov/nasa/jpf/vm/Verify.class"/>
+
+          <!-- these are required if we run TestJPF derived test classes -->
+          <include name="gov/nasa/jpf/JPFShell.class"/>
+          <include name="gov/nasa/jpf/util/TypeRef.class"/>
+          <include name="gov/nasa/jpf/util/test/TestJPF.class"/>
+          <include name="gov/nasa/jpf/util/test/TestMultiProcessJPF.class"/>
+          <include name="gov/nasa/jpf/util/test/TestJPFHelper.class"/>
+      </fileset>
+    </jar>
+
+    <jar jarfile="build/jpf.jar" index="true">
+      <fileset dir="build/main"/>
+      <fileset dir="build/peers"/>
+      <!-- this is redundant, but if JPF is executed from java.class.path it wouldn't find annotations -->
+      <fileset dir="build/annotations"/>
+      
+      <!-- this is for annotations used by JPF regression tests, which can also be executed outside of junit -->
+      <fileset dir="build/classes">
+          <include name="org/junit/*.class"/>
+      </fileset>
+      
+      <manifest>
+        <attribute name="Built-By" value="${user.name}"/>
+        <attribute name="Implementation-Vendor" value="NASA Ames Research Center"/>
+        <attribute name="Implementation-Title" value="Java Pathfinder core system"/>
+        <attribute name="Implementation-Version" value="${jpf.version}"/>
+      </manifest>
+    </jar>
+
+    <!-- optional jar that contains annotations to be used in non-JPF dependent apps -->
+    <jar jarfile="build/jpf-annotations.jar">
+      <fileset dir="build/annotations"/>
+    </jar>
+
+    <!-- this jar is needed to test classloaders, it is used by URLClassLoaderTest -->
+    <jar jarfile="build/classloader_specific_tests.jar">
+      <fileset dir="build/tests">
+        <include name="classloader_specific_tests/*.class"/>
+  	  </fileset>
+    </jar>
+
+    <jar jarfile="build/RunJPF.jar">
+      <fileset dir="build/main">
+        <include name="gov/nasa/jpf/tool/Run.class"/>
+        <include name="gov/nasa/jpf/tool/RunJPF.class"/>
+        <include name="gov/nasa/jpf/Config.class"/>
+        <include name="gov/nasa/jpf/ConfigChangeListener.class"/>
+        <include name="gov/nasa/jpf/Config$MissingRequiredKeyException.class"/>
+        <include name="gov/nasa/jpf/JPFClassLoader.class"/>
+        <include name="gov/nasa/jpf/JPFShell.class"/>
+        <include name="gov/nasa/jpf/JPFException.class"/>
+        <include name="gov/nasa/jpf/JPFConfigException.class"/>
+        <include name="gov/nasa/jpf/JPFTargetException.class"/>
+        <include name="gov/nasa/jpf/util/JPFSiteUtils.class"/>
+        <include name="gov/nasa/jpf/util/FileUtils.class"/>
+        <include name="gov/nasa/jpf/util/StringMatcher.class"/>
+        <include name="gov/nasa/jpf/util/Pair.class"/>        
+      </fileset>
+      
+      <manifest>
+        <attribute name="Built-By" value="${user.name}"/>
+        <attribute name="Implementation-Vendor" value="NASA Ames Research Center"/>
+        <attribute name="Implementation-Title" value="Java Pathfinder core launch system"/>
+        <attribute name="Implementation-Version" value="${jpf.version}"/>
+        <attribute name="Main-Class" value="gov.nasa.jpf.tool.RunJPF"/>
+      </manifest>
+    </jar>
+
+    <jar jarfile="build/RunTest.jar">
+      <fileset dir="build/main">
+        <include name="gov/nasa/jpf/tool/Run.class"/>
+        <include name="gov/nasa/jpf/tool/RunTest.class"/>
+        <include name="gov/nasa/jpf/tool/RunTest$Failed.class"/>
+        <include name="gov/nasa/jpf/Config.class"/>
+        <include name="gov/nasa/jpf/ConfigChangeListener.class"/>
+        <include name="gov/nasa/jpf/Config$MissingRequiredKeyException.class"/>
+        <include name="gov/nasa/jpf/JPFClassLoader.class"/>
+        <include name="gov/nasa/jpf/JPFException.class"/>
+        <include name="gov/nasa/jpf/JPFConfigException.class"/>
+        <include name="gov/nasa/jpf/util/JPFSiteUtils.class"/>
+        <include name="gov/nasa/jpf/util/FileUtils.class"/>
+        <include name="gov/nasa/jpf/util/StringMatcher.class"/>
+        <include name="gov/nasa/jpf/util/DevNullPrintStream.class"/>
+      </fileset>
+      <manifest>
+        <attribute name="Built-By" value="${user.name}"/>
+        <attribute name="Implementation-Vendor" value="NASA Ames Research Center"/>
+        <attribute name="Implementation-Title" value="Java Pathfinder test launch system"/>
+        <attribute name="Implementation-Version" value="${jpf.version}"/>
+        <attribute name="Main-Class" value="gov.nasa.jpf.tool.RunTest"/>
+      </manifest>
+    </jar>
+
+  </target>
+
+
+  <!-- public clean: cleanup from previous tasks/builds -->
+  <target name="clean"
+          description="remove all build artifacts and temporary files">
+    <delete dir="build" failonerror="false"/>
+    <delete dir="tmp" failonerror="false"/>
+    <delete>
+      <fileset dir="." includes="**/*~" defaultexcludes="no" />
+      <fileset dir="." includes="**/*.bak" defaultexcludes="no" />
+      <fileset dir="." includes="**/error.xml" />
+    </delete>
+  </target>
+
+  <target name="-cond-clean" unless="build_uptodate"
+          description="remove all build artifacts and temporaries if build.properties has been changed">
+    <antcall target="clean"/>
+  </target>
+
+
+  <!-- generate buildinfo file  -->
+  <target name="buildinfo" description="create buildinfo properties">
+
+    <!-- make this fail if there are uncommitted changes -->
+    <exec executable="hg" outputproperty="uncommitted_changes" failifexecutionfails="true">
+      <arg value="status"/>
+    </exec>
+    <condition property="have_uncommitted_changes">
+      <length string="${uncommitted_changes}" trim="true" when="greater" length="0"/>
+    </condition>
+<!--
+    <fail if="have_uncommitted_changes">hg status shows uncommitted changes:
+      ${uncommitted_changes}
+    </fail>
+-->
+    <exec executable="hg" outputproperty="hg.tip.id" failifexecutionfails="false">
+      <arg value="tip"/>
+      <arg value="--template"/>
+      <arg value="{rev}:{node|short}\n"/>
+    </exec>
+    <exec executable="hg" outputproperty="hg.author" failifexecutionfails="false">
+      <arg value="tip"/>
+      <arg value="--template"/>
+      <arg value="{author}\n"/>
+    </exec>
+    <exec executable="hg" outputproperty="hg.tip.date" failifexecutionfails="false">
+      <arg value="tip"/>
+      <arg value="--template"/>
+      <arg value="{date|isodate}\n"/>
+    </exec>
+    <exec executable="hg" outputproperty="hg.paths.default" failifexecutionfails="false">
+      <arg value="showconfig"/>
+      <arg value="paths.default"/>
+    </exec>
+    
+    <exec executable="hostname" failifexecutionfails="false" outputproperty="env.COMPUTERNAME"/>
+    <property name="hostname" value="${env.COMPUTERNAME}"/>  <!-- Windows doesn't have hostname -->
+
+    <!-- it seems the 'propertyfile' task just appends -->
+    <delete file="build.properties" failonerror="false"/>
+
+    <propertyfile file="build.properties" comment="JPF core build info">
+      <entry key="revision" value="${hg.tip.id}"/>
+      <entry key="date.tip" value="${hg.tip.date}"/>
+
+      <entry key="author" value="${hg.author}"/>
+      <entry key="repository" value="file://${hostname}${basedir}"/>
+      <entry key="upstream" value="${hg.paths.default}"/>
+
+      <entry key="java.version" value="${java.version}"/>
+
+      <entry key="os.arch" value="${os.arch}"/>
+      <entry key="os.name" value="${os.name}"/>
+      <entry key="os.version" value="${os.version}"/>
+      <entry key="user.country" value="${user.country}"/>
+
+    </propertyfile>
+
+  </target>
+
+  <target name="dist" description="build binary distribution">
+    <delete file="build/${ant.project.name}*.zip"/>
+  	
+    <exec executable="hg" outputproperty="hg.tip.rev" failifexecutionfails="false">
+      <arg value="tip"/>
+      <arg value="--template"/>
+      <arg value="-r{rev}"/>
+    </exec>
+  	
+    <!-- 2do this seems stupid - there needs to be a better way to re-base (zip basedir fails miserably) -->
+    <zip destfile="build/${ant.project.name}${hg.tip.rev}.zip" update="false" excludes="*">
+      <zipfileset file="jpf.properties"  prefix="${ant.project.name}"/>
+      <zipfileset file="build.properties"  prefix="${ant.project.name}"/>
+      <zipfileset dir="lib"  prefix="${ant.project.name}/lib"/>
+      <zipfileset dir="bin"  prefix="${ant.project.name}/bin" filemode="754"/>
+      <zipfileset dir="build" includes="*.jar" prefix="${ant.project.name}/build"/>
+    </zip>
+  </target>
+
+  <target name="src-dist" description="build source distribution">
+    <delete file="build/${ant.project.name}*-src.zip"/>
+    
+    <exec executable="hg" outputproperty="hg.tip.rev" failifexecutionfails="false">
+      <arg value="tip"/>
+      <arg value="--template"/>
+      <arg value="-r{rev}"/>
+    </exec>
+  	
+    <zip destfile="build/${ant.project.name}${hg.tip.rev}-src.zip" update="false" excludes="*" whenempty="skip">
+      <zipfileset file="jpf.properties"  prefix="${ant.project.name}"/>
+      <zipfileset file="build.properties"  prefix="${ant.project.name}"/>
+      <zipfileset file="build.xml"  prefix="${ant.project.name}"/>
+    	<zipfileset file="LICENSE-2.0.txt"  prefix="${ant.project.name}"/>
+      <zipfileset file="README"  prefix="${ant.project.name}"/>
+      <zipfileset dir="src" prefix="${ant.project.name}/src"/>
+      <zipfileset dir="lib"  prefix="${ant.project.name}/lib" erroronmissingdir="false"/>
+      <zipfileset dir="bin"  prefix="${ant.project.name}/bin" filemode="754"/>
+      <zipfileset dir="tools" prefix="${ant.project.name}/tools" erroronmissingdir="false"/>
+
+      <!-- IDE related configuration files -->
+      <zipfileset file=".project"  prefix="${ant.project.name}"/>
+      <zipfileset file=".classpath"  prefix="${ant.project.name}"/>
+      <zipfileset dir="eclipse" prefix="${ant.project.name}/eclipse"/>
+
+      <zipfileset dir="nbproject" prefix="${ant.project.name}/nbproject"/>
+    </zip>
+  </target>
+
+  <!-- ======================= TEST SECTION ================================ -->
+
+
+
+  <target name="test" depends="build"
+          description="run core regression tests" if="have_tests">
+          
+    <!-- note this can be directly set in local.properties, which overrides this setting -->
+    <property name="junit.home" value="${env.JUNIT_HOME}"/>
+    
+    <condition property="junit.usefile">
+      <!-- don't set if this is running from within an IDE that collects output -->
+      <not>
+        <isset property="netbeans.home"/>  
+      </not>
+    </condition>
+    
+    <junit printsummary="on" showoutput="off" 
+           haltonfailure="no" logfailedtests="true" failureproperty="test.failed" 
+           dir="${basedir}" fork="yes" forkmode="perTest" maxmemory="1024m" outputtoformatters="true">
+      <formatter type="plain" usefile="${junit.usefile}"/>
+
+      <assertions>
+        <enable/>
+      </assertions>
+
+      <classpath>
+        <path refid="lib.path"/>
+        <pathelement location="build/tests"/>
+        <pathelement location="build/classes"/>
+        <pathelement location="build/annotations"/>
+        
+        <fileset dir="${junit.home}">
+          <include name="**/*.jar"/>
+        </fileset>  
+      </classpath>
+
+      <batchtest todir="build/tests">
+        <fileset dir="build/tests">
+          <exclude name="**/JPF_*.class"/>
+          <include name="**/*Test.class"/>
+        	
+          <exclude name="**/SplitInputStreamTest.class"/>
+        </fileset>
+      </batchtest>
+
+    </junit>
+
+    <fail if="test.failed" />
+   
+  </target>
+
+  
+</project>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/attributes.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,18 @@
+# The Attribute System #
+
+While JPF stores values for operands, local variables and fields very similar to a normal VM, it also features a storage extension mechanism that lets you associate arbitrary objects with stack slots (operands and locals), fields, and whole objects (ElementInfos). The attribute objects can be set/used in [native peers](mji) or [listeners](listener) to add state stored/restored information that automatically follows the data flow.
+
+Note that JPF does not restore attribute object values upon backtracking per default, only attribute references. If you need to make sure attribute values are restored, you have to use copy-on-write and then store back when accessing and modifying such attributes. 
+
+![Figure: JPF Attribute System](../graphics/attributes.svg){align=center width=650}
+
+JPF provides an API to set/access these attributes, which is located in `gov.nasa.jpf.vm.Fields` (for field attributes) and `gov.nasa.jpf.vm.StackFrame` (for local variables and operands). Once set, the VM copies the attributes each time it reads/writes the associated field or stackframe slot. 
+
+## Usage ##
+
+For example, such attributes can be used to represent symbolic values or numeric error bounds. It should be noted though that attributes impose additional runtime costs, which is also why we don't treat normal, concrete values just as a special kind of attribute (normal values are still stored separately as builtin types like `int`). The upside of this is that your attributes coexist with normal, concrete values, which for instance allows things like mixed symbolic and concrete execution.
+
+> **Note:** JPF now can associate attributes not only with fields of an object, but with the object as a whole. See the `gov.nasa.jpf.vm.ElementInfo` API for details.
+
+> **Note:** while there is an API to set/retrieve attributes based on type, there is no implementation
+yet that allows multiple attributes to be stored.
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/bytecode_factory.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,70 @@
+# Bytecode Factories #
+Normally, a VM defines the semantics of it's programming language. In case of Java, the corresponding instruction set represents a multi-threaded stack machine, where values are kept on the heap, or inside of local and/or operand slots within stack frames. The effect of Java bytecode instructions with respect to heap, locals and operands are described in [Sun's Java virtual machine specifications](http://java.sun.com/docs/books/jvms/second_edition/html/VMSpecTOC.doc.html/).
+JPF is different. The VM of JPF and its associated constructs like `ThreadInfo`, `ClassInfo`, `ElementInfo` etc. provide all the necessary means to implement a normal Java interpreter. However, JPF delegates the use of these means to the instructions. Every bytecode that gets executed by JPF is represented by a corresponding `Instruction` object, which normally gets instantiated during class load time. The `Instruction` classes of the standard execution mode can be found in package `gov.nasa.jpf.jvm.bytecode`.
+
+When it comes to executing a bytecode, the VM simply calls the `execute()` method of this `Instruction` instance. The implementation of this method defines the execution semantics.
+
+The trick is now that JPF uses a configurable [abstract factory](http://en.wikipedia.org/wiki/Abstract_factory_pattern) to choose and instantiate the `Instruction` classes. By providing your own concrete `InstructionFactory`, together with a set of related `Instruction` classes, you can change the execution semantics of Java.
+
+![Figure: Bytecode Factories](../graphics/bc-factory.svg){align=center width=850}
+
+## Usages ##
+
+Why would it be useful to change the standard semantics? One reason is to extend normal semantics with additional checks. For example, this is performed by the JPF extension jpf-numeric which overrides numeric bytecode classes with versions that check for over-/underflow and silent NaN propagation (among other things). A much more involved example is the JPF extension jpf-symbc, which implements a symbolic execution mode for Java, e.g. to automatically generate test cases based on the program structure of an application. It does so by overriding branch instructions, turning them into state space branches represented by their own [ChoiceGenerators](choicegenerator), collecting the path conditions on the way, and feeding them to an external SAT solver.
+
+## Implementation ##
+
+Since there is a large number of Java bytecode instructions, it would be tedious having to implement all 250+ Instruction classes in order to override just a couple of them. You can reduce the effort in three ways:
+
+
+### GenericInstructionFactory ###
+
+
+Using the `GenericInstructionFactory` as a base class for your `InstructionFactory`. This only requires you to specify an alternative package where your bytecode classes reside, together with the set of bytecodes that should be overridden. The resulting code can be quite short, as can be seen in the *numeric* extension example:
+
+~~~~~~~~ {.java}
+public class NumericInstructionFactory extends GenericInstructionFactory {
+ 
+  // which bytecodes do we replace
+  static final String[] BC_NAMES = {
+    "DCMPG", "DCMPL",  "DADD", "DSUB", "DMUL", "DDIV",
+    "FCMPG", "FCMPL",  "FADD", "FSUB", "FMUL", "FDIV",
+                       "IADD", "ISUB", "IMUL", "IDIV",  "IINC", 
+                       "LADD", "LSUB", "LMUL", "LDIV"   
+  };
+  
+  // where do they reside
+  protected static final String BC_PREFIX = "gov.nasa.jpf.numeric.bytecode.";
+  
+  // what classes should use them
+  protected static final String[] DEFAULT_EXCLUDES = { "java.*", "javax.*" };
+  
+  public  NumericInstructionFactory (Config conf){    
+    super(conf, BC_PREFIX, BC_NAMES, null, DEFAULT_EXCLUDES);
+    
+    NumericUtils.init(conf);
+  }
+}
+~~~~~~~~
+
+
+### Super Delegation ###
+
+You can derive your overriding bytecode classes from the ones in `gov.nasa.jpf.jvm.bytecode`. If you just want to add some checks before or after performing the "normal" operation, you can use the standard `Instruction` classes as base classes, and call `super.execute(..)` from within your derived classes. 
+
+
+### Attributes ###
+
+As your execution semantics get more complex, you probably need to store and restore additional information that is associated with variables. JPF provides an automatically managed [attribute system](attributes) for this purpose. You can attach objects to locals, operands and fields, and JPF takes care of propagating these attribute objects whenever it manipulates stackframes or heap objects.
+
+
+## Configuration ##
+
+
+Configuring your bytecode factory just requires one JPF property, e.g.
+
+~~~~~~~~ {.bash}
+vm.insn_factory.class = gov.nasa.jpf.numeric.NumericInstructionFactory
+~~~~~~~~
+
+which can be either done from the command line or from within a *.jpf property file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/choicegenerator.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,212 @@
+# ChoiceGenerators #
+
+The goal of every model checker is to check if certain properties hold in states of the system under test. The way that choices are computed is a fundamental part of model checking, since they determine which states are checked. We refer to the mechanism used by JPF to capture choices as ChoiceGenerators.
+
+ChoiceGenerators can be approached from an application perspective, or from the JPF implementation perspective. In this section, we cover both perspectives.
+
+## Motivation ##
+
+Whenever the model checker reaches non-determinism in code, it needs to compute choices. Non-determinism can be due to thread scheduling or non-deterministic data acquisitions. Here, we present an example including data non-determinism to justify our implementation approach. JPF provides support for "random" data acquisition, using the interface `gov.nasa.jpf.jvm.Verify`.
+
+~~~~~~~~ {.java}
+...
+boolean b = Verify.getBoolean(); // evaluated by JPF for both `true` and `false`
+...
+~~~~~~~~
+
+This worked nicely for small sets of choice values (such as `{true,false}` for boolean), but the mechanism for enumerating all choices from a type specific interval becomes already questionable for large intervals (e.g. `Verify.getInt(0,10000)`), and fails completely if the data type does not allow finite choice sets at all (such as floating point types):
+
+![Figure 1: Motivation behind ChoiceGenerator](../graphics/cg-motivation.svg){align=center width=750}
+
+To handle this case, we have to leave the ideal world of model checking (that considers all possible choices), and make use of what we know about the real world - we have to use heuristics to make the set of choices finite and manageable. However, heuristics are application and domain specific, and it would be a bad idea to hardcode them into the test drivers we give JPF to analyze. This leads to a number of requirements for the JPF choice mechanism:
+
+  * choice mechanisms have to be decoupled (i.e. thread choices should be independent of data choices, double choices from int choices etc.)
+  * choice sets and enumeration should be encapsulated in dedicated, type specific objects. The VM should only know about the most basic types, and otherwise use a generic interface to obtain choices
+  * selection of classes representing (domain specific) heuristics, and parametrization of ChoiceGenerator instances should be possible at runtime, i.e. via JPF's configuration mechanism (properties)
+
+The diagram shown above depicts this with an example that uses a "randomly" chosen velocity value of type double. As an example heuristic we use a threshold model, i.e. we want to know how the system reacts below, at, and above a certain application specific value (threshold). We reduce an infinite set of choices to only three "interesting" ones. Of course, "interesting" is quite subjective, and we probably want to play with the values (delta, threshold, or even used heuristic) efficiently, without having to rebuild the application each time we run JPF.
+
+The code example does not mention the used `ChoiceGenerator` class (`DoubleThresholdGenerator`) at all, it just specifies a symbolic name `"velocity"`, which JPF uses to look up an associated class name from its configuration data (initialized via property files or the command line - see Configuring JPF Runtime Options). But it doesn't stop there. Most heuristics need further parameterization (e.g. threshold, delta), and we provide that by passing the JPF configuration data into the `ChoiceGenerator` constructors (e.g. the `velocity.threshold` property). Each `ChoiceGenerator` instance knows its symbolic name (e.g. `"velocity"`), and can use this name to look up whatever parameters it needs.
+
+## The JPF Perspective ##
+
+Having such a mechanism is nice to avoid test driver modification. But it would be much nicer to consistently use the same mechanism not just for data acquisition choices, but also scheduling choices (i.e. functionality that is not controlled by the test application). JPF's ChoiceGenerator mechanism does just this, but in order to understand it from an implementation perspective we have to take one step back and look at some JPF terminology:
+
+![Figure 2: States, Transitions and Choices](../graphics/cg-ontology.svg){align=center width=650}
+
+
+*State* is a snapshot of the current execution status of the application (mostly thread and heap states), plus the execution history (path) that lead to this state. Every state has a unique id number. State is encapsulated in the `SystemState` instance (almost, there is some execution history which is just kept by the JVM object). This includes three components:
+
+  * KernelState - the application snapshot (threads, heap)
+  * trail - the last Transition (execution history)
+  * current and next ChoiceGenerator - the objects encapsulating the choice enumeration that produces different transitions (but not necessarily new states)
+
+*Transition* is the sequence of instructions that leads from one state to the next. There is no context switch within a transition, it's all in the same thread. There can be multiple transitions leading out of one state (but not necessarily to a new state).
+
+*Choice* is what starts a new transition. This can be a different thread (i.e. scheduling choice), or different "random" data value.
+
+In other words, possible existence of choices is what terminates the last transition, and selection of a choice value precludes the next transition. The first condition corresponds to creating a new `ChoiceGenerator`, and letting the `SystemState` know about it. The second condition means to query the next choice value from this `ChoiceGenerator` (either internally within the VM, or in an instruction or native method).
+
+## How it comes to Life ##
+With this terminology, we are ready to have a look at how it all works. Let's assume we are in a transition that executes a `getfield` bytecode instruction (remember, JPF executes Java bytecode), and the corresponding object that owns this field is shared between threads. For simplicity's sake, let's further assume there is no synchronization when accessing this object, (or we have turned off the property `vm.sync_detection`). Let's also assume there are other runnable threads at this point. Then we have a choice - the outcome of the execution might depend on the order in which we schedule threads, and hence access this field. There might be a data race.
+
+![Figure 3: ChoiceGenerator Sequence](../graphics/cg-sequence.svg){align=center width=550}
+
+Consequently, when JPF executes this `getfield` instruction, the `gov.nasa.jpf.jvm.bytecode.GETFIELD.execute()` method does three things:
+
+  1. create a new `ChoiceGenerator` (`ThreadChoiceGenerator` in this case), that has all runnable threads at this point as possible choices
+  2. registers this `ChoiceGenerator` via calling `SystemState.setNextChoiceGenerator()`
+  3. schedules itself for re-execution (just returns itself as the next instruction to execute within the currently running thread)
+
+At this point, JPF ends this transition (which is basically a loop inside `ThreadInfo.executeStep()`), stores a snapshot of the current State, and then starts the next transition (let's ignore the search and possible backtracks for a moment). The `ChoiceGenerator` created and registered at the end of the previous transition becomes the new current `ChoiceGenerator`. Every state has exactly one current `ChoiceGenerator` object that is associated with it, and every transition has exactly one choice value of this `ChoiceGenerator` that kicks it off. Every transition ends in an instruction that produces the next `ChoiceGenerator`.
+
+The new transition is started by the `SystemState` by setting the previously registered `ChoiceGenerator` as the current one, and calling its `ChoiceGenerator.advance()` method to position it on its next choice. Then the `SystemState` checks if the current `ChoiceGenerator` is a scheduling point (just a `ThreadChoiceGenerator` used to encapsulate threads scheduling), and if so, it gets the next thread to execute from it (i.e. the `SystemState` itself consumes the choice). Then it starts the next transition by calling `ThreadInfo.executeStep()` on it.
+
+The `ThreadInfo.executeStep()` basically loops until an Instruction.execute() returns itself, i.e. has scheduled itself for re-execution with a new `ChoiceGenerator`. When a subsequent `ThreadInfo.executeStep()` re-executes this instruction (e.g. `GETFIELD.execute()`), the instruction notices that it is the first instruction in a new transition, and hence does not have to create a `ChoiceGenerator` but proceeds with it's normal operations.
+
+If there is no next instruction, or the Search determines that the state has been seen before, the VM backtracks. The `SystemState` is restored to the old state, and checks for not-yet-explored choices of its associated ChoiceGenerator by calling `ChoiceGenerator.hasMoreChoices()`. If there are more choices, it positions the `ChoiceGenerator` on the next one by calling `ChoiceGenerator.advance()`. If all choices have been processed, the system backtracks again (until it's first `ChoiceGenerator` is done, at which point we terminate the search).
+
+![Figure 4: ChoiceGenerator Implementation](../graphics/cg-impl.svg){align=center width=850}
+
+The methods that create `ChoiceGenerators` have a particular structure, dividing their bodies into two parts:
+
+  1. *top half* - (potentially) creates and registers a new `ChoiceGenerator`. This marks the end of a transition
+  2. *bottom half* - which does the real work, and might depend on acquiring a new choice value. This is executed at the beginning of the next transition
+
+To determine which branch you are in, you can call `ThreadInfo.isFirstStepInsn()`. This will return `true` if the currently executed instruction is the first one in the transition, which corresponds to the *bottom half* mentioned above.
+
+The only difference between scheduling choices and data acquisition choices is that the first ones are handled internally by the VM (more specifically: used by the `SystemState` to determine the next thread to execute), and the data acquisition is handled in the bottom half of `Instruction.execute()`, native method, or listener callback method (in which case it has to acquire the current `ChoiceGenerator` from the `SystemState`, and then explicitly call `ChoiceGenerator.getNextChoice()` to obtain the choice value). For a real example, look at the `JPF.gov_nasa_jpf_jvm_Verify.getBoolean()` implementation.
+
+As an implementation detail, creation of scheduling points are delegated to a `Scheduler` instance, which encapsulates a scheduling policy by providing a consistent set of `ThreadChoiceGenerators` for the fixed number of instructions that are scheduling relevant (`monitor_enter`, synchronized method calls, `Object.wait()` etc.). Clients of this `Scheduler` therefore have to be aware of that the policy object might not return a new `ChoiceGenerator`, in which case the client directly proceeds with the bottom half execution, and does not break the current transition.
+
+The standard classes and interfaces for the ChoiceGenerator mechanism can be found in package `gov.nasa.jpf.vm`, and include:
+
+  * `ChoiceGenerator`
+  * `BooleanChoiceGenerator`
+  * `IntChoiceGenerator`
+  * `DoublechoiceGenerator`
+  * `ThreadChoiceGenerator`
+  * `SchedulingPoint`
+  * `SchedulerFactory`
+  * `DefaultSchedulerFactory`
+
+Concrete implementations can be found in package `gov.nasa.jpf.vm.choice`, and include classes like:
+
+  * `IntIntervalGenerator`
+  * `IntChoiceFromSet`
+  * `DoubleChoiceFromSet`
+  * `DoubleThresholdGenerator`
+  * `ThreadChoiceFromSet`
+
+As the number of useful generic heuristics increases, we expect this package to be expanded.
+
+
+## Cascaded ChoiceGenerators ##
+There can be more than one `ChoiceGenerator` object associated with a transition. Such ChoiceGenerators are referred to as *cascaded*, since they give us a set of choice combinations for such transitions. 
+
+For example, assume that we want to create a listener that perturbs certain field values, i.e. it replaces the result operand that is pushed by a `getfield` instruction. This is easy to do from a listener, but the VM (more specifically our on-the-fly [partial order reduction](partial_order_reduction)) might already create a `ThreadChoiceGenerator` (scheduling point) for this `getfield` if it refers to a shared object, and the instruction might cause a data race. Without cascaded `ChoiceGenerators` we could only have the perturbation listener **or** the race detection, but not both. This is clearly a limitation we want to overcome, since you might not even know when JPF - or some of the other [listeners](listener) or [bytecode_factories](bytecode_factory) - create `ChoiceGenerators` that would collide with the ones you want to create in your listener.
+
+Using cascaded ChoiceGenerators requires little more than what we have already seen above. It only involves changes to two steps:
+
+ 1. ChoiceGenerator creation - you need to identify `ChoiceGenerators` with a `String` id. We can't use the type of the `ChoiceGenerator` - or it's associated choice type - to identify a particular instance, since different listeners might use different `ChoiceGenerator` instances of same types for different purposes. Resolving through unique types would throw us back to where we would have to know about all the other `ChoiceGenerators` created by all the other JPF components. We can't use the associated instruction either, because the whole point is that we can have more than one `ChoiceGenerator` for each of them. So we have to give our `ChoiceGenerator` instances names when we create them, as in
+ 
+~~~~~~~~ {.java}
+...
+IntChoiceFromSet cg = new IntChoiceFromSet("fieldPerturbator", 42, 43);
+~~~~~~~~
+
+The name should be reasonably unique, describing the context in which this choice is used. Don't go with "generic" names like "myChoice". In case of doubt, use the method name that creates the `ChoiceGenerator`. The reason why we need the *id* in the first place is that we later-on want to be able to retrieve a specific instance. Which brings us to:
+
+ 2. ChoiceGenerator retrieval - at some point we want to process the choice (usually within the *bottom half* of the method that created the `ChoiceGenerator`), so we need to tell JPF all we know about the `ChoiceGenerator` instance, namely id and type. The simple `SystemState.getChoiceGenerator()` we used above will only give us the last registered one, which might or might not be the one we registered ourselves. Retrieval is done with a new method `SystemState.getCurrentChoiceGenerator(id,cgType)`, which in the above case would look like:
+ 
+~~~~~~~~ {.java}
+...
+IntChoiceFromSet cg = systemState.getCurrentChoiceGenerator("fieldPerturbator", IntChoiceFromSet.class);
+assert cg != null : "required IntChoiceGenerator not found";
+...
+~~~~~~~~
+
+This method returns `null` if there is no `ChoiceGenerator` of the specified id and type associated with the currently executed instruction. If this is the bottom half of a method that created the instance, this is most likely an error condition that should be checked with an assertion. If the retrieval is in another method, existence of such a `ChoiceGenerator` instance could be optional and you therefore have it checked in an `if (cg != null) {..}' expression.
+
+This is all there is to it in case you don't refer to a particular execution state of an instruction. As an example, assume that you want to add some int choices on top of each `Verify.getInt(..)` call. Your listener would look like this:
+
+~~~~~~~~ {.java}
+  @Override
+  public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+    SystemState ss = vm.getSystemState();
+
+    if (executedInsn instanceof EXECUTENATIVE) { // break on method call
+      EXECUTENATIVE exec = (EXECUTENATIVE) executedInsn;
+
+      if (exec.getExecutedMethodName().equals("getInt")){ // Verify.getInt(..) - this insn did create a CG on its own
+        if (!ti.isFirstStepInsn()){ // top half - first execution
+          IntIntervalGenerator cg = new IntIntervalGenerator("instrumentVerifyGetInt", 3,4);
+          ss.setNextChoiceGenerator(cg);
+          ...
+
+        } else { // bottom half - re-execution at the beginning of the next transition
+          IntIntervalGenerator cg = ss.getCurrentChoiceGenerator("instrumentVerifyGetInt", IntIntervalGenerator.class);
+          assert cg != null : "no 'instrumentVerifyGetInt' IntIntervalGenerator found";
+          int myChoice = cg.getNextChoice();
+          ... // process choice
+        }
+      }
+    }
+  }
+~~~~~~~~
+
+
+Sometimes what you do with your choice depends on the execution state of the instruction this `ChoiceGenerator` was created for, and you have to be aware of that the instruction might get re-executed (e.g. after processing the top half of another `ChoiceGenerator` creating method) before it has done what you depend on for your local choice processing. Consider our previous example of the field perturbation. Simply speaking, all we want to do in our listener is just swap operand stack values after a certain `getfield`. However, the partial order reduction of the VM might get in our way because it reschedules the instruction *before* it pushes the value if execution of this instruction might constitute a data race, and therefore required creation of a `ThreadChoiceGenerator` instance. What is worse is that the VM might do this conditionally - if there is only one runnable thread, there is no need for a scheduling point since there can't be a data race. Our own perturbator listener has to account for all that. Luckily, we can use `SystemState.getCurrentChoiceGenerator(id,type)` to unify all these cases, and we just have to restore execution state in case we want to re-execute the instruction ourselves. Here is an example:
+
+~~~~~~~~ {.java}
+  @Override
+  public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+    SystemState ss = vm.getSystemState();
+
+    if (executedInsn instanceof GETFIELD){
+      GETFIELD getInsn = (GETFIELD) executedInsn;
+      FieldInfo fi = getInsn.getFieldInfo();
+      if (fi.getName().equals("perturbedFieldName")){
+
+        IntChoiceFromSet cg = ss.getCurrentChoiceGenerator("fieldReplace", IntChoiceFromSet.class);
+        StackFrame frame = ti.getModifiableTopFrame();
+        if (cg == null){
+
+          // we might get here after a preceding rescheduling exec, i.e.
+          // partial execution (with successive re-execution), or after
+          // non-rescheduling exec has been completed (only one runnable thread).
+          // In the first case we have to restore the operand stack so that
+          // we can re-execute
+          if (!ti.willReExecuteInstruction()){
+            // restore old operand stack contents
+            frame.pop();
+            frame.push(getInsn.getLastThis());
+          }
+
+          cg = new IntChoiceFromSet("fieldReplace", 42, 43);
+          ss.setNextChoiceGenerator(cg);
+          ti.reExecuteInstruction();
+
+        } else {
+          int v = cg.getNextChoice();
+          int n = frame.pop();
+          frame.push(v);
+        }
+      }
+    }
+  }
+~~~~~~~~
+
+These examples show you that at the beginning of each transition, there is a choice value for all the cascaded `ChoiceGenerators` associated with it. If you would add `choiceGeneratorAdvanced()` notifications to your listener, you would also see that JPF processes all related choice combinations.
+
+If you really want to see the context, there are a number of additional methods in `SystemState` that might help you:
+
+ * `getChoiceGenerator()` - returns only the last registered one
+ * `getChoiceGenerators()` - returns an array of all `ChoiceGenerators` in the current execution path
+ * `getLastChoiceGeneratorOfType(cgType)` - returns the last registered `ChoiceGenerator` in the path that is of the specified type
+ * `getCurrentChoiceGenerators()` - returns array of all cascaded `ChoiceGenerators` associated with the current transition
+ * `getCurrentChoiceGenerator(id)` - returns last registered `ChoiceGenerator` of cascade with specified *id*
+ * `getCurrentChoiceGenerator(id,cgType)` - our workhorse: last registered `ChoiceGenerator` of cascade with specified *id* and *cgType* (which can be a supertype of the actual one)
+ * etc.
+
+How does the system detect if a `ChoiceGenerator` is cascaded or not? Very simple - within `SystemState.setNextChoiceGenerator(cg)`, we just check if `SystemState` already had a registered next `ChoiceGenerator`, and if so, we set a cascaded attribute for this one. Other than that, we just maintain normal linear `ChoiceGenerator` linkage, which is accessible through `ChoiceGenerator.getPreviousChoiceGenerator()`. If you want to iterate through a cascade yourself, use the `ChoiceGenerator.getCascadedParent()` method, which returns `null` if there is none. Just be aware of that the last registered `ChoiceGenerator` (i.e. what `SystemState.getChoiceGenerator()` returns) does *not* have the cascaded attribute set (i.e. `ChoiceGenerator.isCascaded()` returns `false`).    
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/coding_conventions.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,41 @@
+# Coding Conventions #
+JPF is an open system. In order to keep the source format reasonably consistent, we strive to keep the following minimal set of conventions
+
+  * Two space indentation (no tabs)
+  * Opening brackets in same line (class declaration, method declaration, control statements)
+  * No spaces after opening '(', or before closing ')'
+  * Method declaration parameters indent on column
+  * All files start with copyright and license information
+  * All public class and method declarations have preceding Javadoc comments
+  * We use *camelCase* instead of *underscore_names* for identifiers
+  * Type names are upper case 
+
+The following code snippet illustrates these rules.
+
+~~~~~~~~ {.java}
+/* <copyright notice goes here>
+ * <license referral goes here>
+ */
+
+/**
+ * this is my class declaration example
+ */
+    
+public class MyClass {
+   
+  /**
+   * this is my public method example
+   */
+  public void foo (int arg1, int arg2,
+                   int arg3) {
+    if (bar) {
+      ..
+    } else {
+      ..
+    }
+  }
+   ..
+}
+~~~~~~~~
+
+We consider modularity to be of greater importance than source format. With its new configuration scheme, there is no need to introduce dependencies of core classes towards optional extensions anymore. If you add something that is optional, and does not seamlessly fit into an existing directory, keep it separate by adding new directories. The core JPF classes should not contain any additional dependencies to external code.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/create_project.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,91 @@
+# Creating a New JPF Module #
+
+So what do you have to do to create a new JPF module? For a quick shortcut to setting up *most* things,  use the `create_project` script of the [jpf-template module](wiki:projects/jpf-template).  
+
+However, jpf-template cannot do everything for you, so see below for more information on how to finish setting up your new project.
+
+Several steps are involved:
+
+### 1. get familiar with the JPF configuration ###
+You need to understand how your project will be looked up and initialized during JPF startup, and the place to learn that is the [JPF configuration](../user/config) page. Once you know what *[site properties](../install/site-properties)* and *project properties* are, you can proceed.
+
+### 2. get familiar with the standard JPF project layout ###
+Although this is mostly convention, and you can deviate if you really need to, please try hard not to.
+
+You can get the details from the [JPF Runtime Modules](modules) page, but the essence is that each project has two (possible) major build artifacts:
+
+ * `jpf-<module>.jar` - executed by the host (platform) VM (contains main classes and peers)
+ * `jpf-<module>-classes.jar` - executed by JPF (contains modeled classes)
+
+Consequently, your sources are kept in `src/main`, `src/peers`, `src/classes`, `src/annotations`, `src/tests` and `src/examples`. You might only have some of these, but please provide regression tests so that people can check if your project works as expected. 
+
+All 3rd party code that is required at runtime goes into a `lib` directory.
+
+We keep potential annotations separate (and provide additional `jpf-<module>-annotations.jar`) so that external projects (systems under test) can use them without relying on all JPF classes to be in their `classpath`. The idea is that this jar does not contain any code which could alter the system under test behavior if you execute it outside of JPF. 
+
+<The `tools` directory contains 3rd party libraries and tools that are used at build-time. For convenience reasons, we usually copy the small `RunJPF.jar` from the jpf-core in here, so that you can easily run JPF from the command line without the need for platform specific scripts or links, but that is completely optional.>
+
+### 3. create a jpf.properties file ###
+Within the root directory of each JPF module a project properties file is needed which is named `jpf.properties`. It contains the path settings the host VM and JPF need to know about at runtime. It looks like this:
+
+~~~~~~~~ {.bash}
+# standard header
+<module-name> = ${config_path}
+
+# classpath elements for the host VM (java)
+<module-name>.native_classpath = build/<module-name>.jar;lib/...
+
+# classpath elements for JPF
+<module-name>.classpath = build/<module-name>-classes.jar;...
+
+# sources JPF should know about when creating traces etc.
+<module-name>.sourcepath = src/classes;...
+~~~~~~~~
+
+You can add other JPF properties, but be aware of that this is always processed during JPF startup if you add your module to the `extensions` list in your [site.properties](../install/site-properties), and might conflict with other JPF modules. For this reason you should only add your module to `extensions` if you know it will always be used.
+
+
+### 4. create your build.xml ###
+Our build process is [Ant](http://ant.apache.org/) based, hence we need a `build.xml` file. The standard targets are
+
+ * `clean`
+ * `compile`
+ * `build` (the default, creates the jars and hence depends on compile)
+ * `test` (run JUnit regression tests, depends on build)
+ * `dist` (creates a binary-only distribution) 
+
+If you stick to the general layout, you can use a template like the one attached to this page (of course you need to replace `<your-project-name>`).
+
+Please note how `site.properties` and `jpf.properties` can be used from within the `build.xml` (Ant understands a subset of the JPF property syntax), which means you don't have to explicitly add the jars of other JPF components you depend on (at least jpf-core). You can reference them symbolically like this:
+
+~~~~~~~~ {.xml}
+  <property file="${user.home}/.jpf/site.properties"/>
+  <property file="${jpf-core}/jpf.properties"/>
+  ..
+  <!-- generic classpath settings -->
+  <path id="lib.path">
+
+    <!-- our own classes and libs come first -->
+    <pathelement location="build/main"/>
+    ...
+    <fileset dir=".">
+  	    <include name="lib/*.jar"/>
+    </fileset>
+
+    <!-- add in what we need from the core -->
+    <pathelement path="${jpf-core.native_classpath}"/>
+  </path>
+  ...
+~~~~~~~~
+
+### 5. add your module to your site.properties ###
+This is optional, you only need to do this if you want to be able to run your JPF module outside its own directory. If so, add an entry to your [site properties file](../install/site-properties) that looks like this:
+
+~~~~~~~~ {.bash}
+...
+<module-name> = <path to your JPF extension module>
+...
+~~~~~~~~
+
+### 6. publish your repository ###
+You can publish this wherever you want ([sourceforge](http://sourceforge.net), [bitbucket](http://bitbucket.org), [google code](http://code.google.com), or [github](http://github.com) are suitable free site supporting Mercurial), or ask us to host it on the JPF server. If you decide to use a 3rd party hosting service, please let us/the JPF community know about it (e.g. by posting to the mailing list at [java-pathfinder@googlegroups.com](https://groups.google.com/forum/#!forum/java-pathfinder).
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/design.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,52 @@
+# JPF Top-level Design #
+
+JPF was designed around two major abstractions: (1) the *VM*, and (2) the *Search* component.
+
+## Virtual Machine (VM) ##
+
+The VM is the state generator. By executing bytecode instructions, the VM generates state representations that can be
+
+  * checked for equality (if a state has been visited before)
+  * queried (thread states, data values etc.)
+  * stored
+  * restored
+
+The main VM parameterizations are classes that implement the state management (matching, storing, backtracking). Most of the execution scheme is delegated to `SystemState`, which in turn uses `Scheduler`  to generate scheduling sequences of interest.
+
+There are three key methods of the VM employed by the Search component:
+
+  * `forward` - generate the next state, report if the generated state has a successor. If yes, store on a backtrack stack for efficient restoration.
+  * `backtrack` - restore the last state on the backtrack stack
+  * `restoreState` - restore an arbitrary state (not necessarily on the backtrack stack)
+
+![Figure: JPF top-level design](../graphics/jpf-abstractions.svg){align=center width=720}
+
+## Search Strategy ##
+
+At any state, the Search component is responsible for selecting the next state from which the VM should proceed, either by directing the VM to generate the next state (`forward`), or by telling it to backtrack to a previously generated one (`backtrack`). The Search component works as a driver for the VM.
+
+The Search component can be configured to check for certain properties by evaluating property objects (e.g. `NotDeadlockedProperty`, `NoAssertionsViolatedProperty`).
+
+The object encapsulating this component includes a search method which implements a strategy used to traverse the state space. The state space exploration continues until it is completely explored, or a property violation is found.
+ The Search component can be configured to use different strategies, such as depth-first search (`DFSearch`), and priority-queue based search that can be parameterized to do various search types based on selecting the most interesting state out of the set of all successors of a given state (`HeuristicSearch`).
+
+## Package Structure ##
+
+The implementation of the JPF core is partitioned into the following packages:
+
+### `gov.nasa.jpf` ###
+The main responsibility of this package is configuration and instantiation of the core JPF objects, namely the Search and VM. The configuration itself is encapsulated by the `Config` class, which contains various methods to create objects or read values from a hierarchy of property files and command line options (see Configuring JPF Runtime Options). Beyond the configuration, the JPF object has little own functionality. It is mainly a convenience construct to start JPF from inside a Java application without having to bother with its complex configuration.
+
+### `gov.nasa.jpf.vm` ###
+This package constitutes the main body of the core code, including the various constructs that implement the Java state generator. Conceptually, the major class is VM, but again this class delegates most of the work to a set of second level classes that together implement the major functionality of JPF. These classes can be roughly divided into three categories:
+
+(1) class management - classes are encapsulated by `ClassInfo` which mostly includes invariant information about fields and methods captured by `FieldInfo` and `MethodInfo`, respectively.
+
+(2) object model - all object data in JPF is stored as integer arrays encapsulated by `Fields` objects. The execution specific lock state of objects is captured by `Monitor` instances. `Fields` and `Monitor` instances together form the objects, which are stored as `ElementInfo`. The heap contains a dynamic array of `ElementInfo` objects where the array indices being used as object reference values
+
+(3) bytecode execution - the execution of bytecode instructions is performed through a collaboration of `SystemState` and `ThreadInfo`, which is also delegated to policy objects implementing the partial order reduction (POR). It starts with the `VM` object calling `SystemState.nextSuccessor()`, which descends into `ThreadInfo.executeStep()` (together, these two methods encapsulate the on-the-fly POR), which in turn calls `ThreadInfo.executeInstruction()` to perform the bytecode execution.
+The actual execution is again delegated to bytecode specific Instruction instances that per default reside in a sub-package `gov.nasa.jpf.vm.bytecode` (the set of bytecode classes to use can be configured via a `InstructionFactory` class which allows the user to define a different execution semantics)
+
+### `gov.nasa.jpf.search` ### 
+This package is relatively small and mainly contains the `Search` class, which is an abstract base for search policies. The major method that encapsulates the policy is `Search.search()`, which is the VM driver (that calls the methods`forward`, `backtrack` and `restore`). This package also contains the plain-vanilla depth-first search policy `DFSearch`.
+More policies can be found in the sub-package `gov.nasa.jpf.search.heuristic`, which uses a `HeuristicSearch` class in conjunction with configurable heuristic objects to prioritize a queue of potential successor states.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/eclipse_plugin_update.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,36 @@
+## Hosting an Eclipse plugin update site ##
+
+The first step is to create the local version of the update site.  For example, chapter 18, section 3 of "Eclipse Plug-ins, 3rd edition" will explain how to do this.
+  
+> **Tip:** do not attempt to put the update site in the code repository.  
+
+The plugin and feature files are treated like binaries and bad things will happen.  Here is a sample update site for the mango plugin.
+
+![Local Site](../graphics/localsite.jpg){align=center width=430}
+
+Now you will re-create this directory structure within the wiki.  For the purpose of this discussion, let's pin down the jpf site:
+
+~~~~~~~~ {.bash}
+JPFHOME=http://babelfish.arc.nasa.gov/trac/jpf
+~~~~~~~~
+
+Now chose a home directory, say `HOME`.  For the mango plugin, 
+
+~~~~~~~~ {.bash}
+HOME=wiki/projects/jpf-mango
+~~~~~~~~
+
+Whatever choice of `HOME` you make, the update site you advertise to the world will be `JPFHOME/raw-attachment/HOME/update/`.
+
+
+The `raw-attachment` segment is the *trick* that makes everything work out.  The next step is to create the directory structure for the mirrored update site.  Within `JPFHOME/HOME`, create a link to `JPFHOME/HOME/update`.  Now go to the update page and add the attachments artifacts.jar, content.jar, and site.xml from your local update site.  Create links within `JPFHOME/HOME/update` to `JPFHOME/HOME/update/features` and `JPFHOME/HOME/update/plugins`.  
+
+Attach your feature jar to the features page, and your plugin jar to the plugins page.  That's all there is to it.
+
+> **Tip:** when updating your update site, be sure to sync your plugin and feature with new, higher, revision numbers.  Now rebuild the local site.  Delete all the corresponding attachments in the wiki, and repopulate with the updated versions.
+
+> **Bonus tip:** Once everything is working, you can delete the link to the update site.  This will prevent your visitors from accidentally going to an uninteresting page.  You can always access this page directly from the browser by entering `JPFHOME/HOME/update`.
+
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/embedded.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,27 @@
+# Embedded JPF #
+JPF can also be used embedded, i.e. called from another Java application. A basic code sequence to start JPF looks like this:
+
+~~~~~~~~ {.java}
+import gov.nasa.jpf.JPF;
+import gov.nasa.jpf.Config;
+
+void runJPF (String[] args) {
+   ..
+   MyListener listener = new MyListener(..);
+
+   // [optionally] if you pass through command line args, 
+   // 'null' any consumed args not to be JPF-processed
+   listener.filterArgs( args);
+   ..
+
+   Config config = JPF.createConfig( args);
+   // set special config key/value pairs here..
+
+   JPF jpf = new JPF( config);
+   jpf.addListener( listener);
+   jpf.run();
+   ..
+}
+~~~~~~~~
+
+Of course, you can also call `gov.nasa.jpf.JPF.main(args)` from within your application, if you don't need to control JPF's configuration or process it's output. 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/index.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,23 @@
+# JPF Developer Guide #
+
+From the previous two sections, you have learned that JPF has one recurring, major theme: it is not a monolithic system, but rather a configured collection of components that implement different functions like state space search strategies, report generation and much more. Being adaptive is JPF's answer to the scalability problem of software model checking.
+
+This not only makes JPF a suitable system for research, but chances are that if are you serious enough about JPF application, you sooner or later end up extending it. This section includes the following topics which describe the different mechanisms that can be used to extend JPF.
+
+ * [Top-level design](design)
+ * Key mechanisms, such as 
+     - [ChoiceGenerators](choicegenerator)
+     - [Partial order reduction](partial_order_reduction)
+     - [Slot and field attributes](attributes)
+ * Extension mechanisms, such as
+     - [Listeners](listener)
+     - [Search Strategies](design)
+     - [Model Java Interface (MJI)](mji)
+     - [Bytecode Factories](bytecode_factory)
+ * Common utility infrastructures, such as
+     - [Logging system](loggin)
+     - [Reporting system](report)
+ * [Running JPF from within your application](embedded)
+ * [Writing JPF tests](jpf_tests)
+ * [Coding conventions](coding_conventions)
+ * [Hosting an Eclipse plugin update site](eclipse_plugin_update) 
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/jpf_tests.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,148 @@
+# Writing JPF Tests #
+
+As a complex runtime system for (almost) arbitrary Java programs, it goes without saying that JPF needs a lot of regression tests. You can find these under the `src/tests` directories in (hopefully) all JPF projects. All tests follow the same scheme, which is motivated by the need to run tests in a number of different ways:
+
+  1. as part of the Ant-based build system, i.e. from build.xml
+  1. as explicitly invoked JUnit tests
+  1. by directly running JPF on the test application (i.e. without JUnit, either as a JPF `shell` or via RunTest.jar)
+  1. by running the test application on a normal JVM
+
+The rationale for this is to support various levels of inspection and debugging. 
+
+Each test conceptually consists of a test driver (e.g. executed under JUnit) which starts JPF from within its `@Test` annotated methods, and a class that is executed by JPF in order to check the verification goals. For convenience reasons, jpf-core provides infrastructure that enables you to implement both parts in the same class. This can be confusing at first - **the test class is used to start JPF on itself**.
+
+![Figure: Unit Testing in JPF](../graphics/new-testing.svg){align=center width=870}
+
+The `main()` method of `TestJPF` derived classes always look the same and can be safely copied between tests:
+
+~~~~~~~~ {.java}
+public static void main(String[] testMethods){
+  runTestsOfThisClass(testMethods);
+}
+~~~~~~~~
+
+This method serves two purposes. First, it is used to start the test outside JUnit, either on all `@Test` annotated instance methods, or just on the ones which names are provided as arguments. Second, it serves as the entry point for JPF when it executes the class. In this case, `TestJPF` takes care of invoking JPF on the test class and providing the name of the test method this was executed from.
+
+Other than that, test classes just consist of (almost) normal `@Test` annotated JUnit test methods, which all share the same structure
+
+~~~~~~~~ {.java}
+import org.junit.Test;
+
+@Test public void testX () {
+  if (verifyNoPropertyViolation(JPF_ARGS){
+    .. code to verify by JPF
+  }
+}
+~~~~~~~~
+
+The trick is the call to `verifyNoPropertyViolation()`, or any of the other `verifyXX()` methods of `TestJPF`. If executed by the host VM, i.e. from JUnit, it starts JPF on the same class and the containing method, and returns `false`. This means the corresponding `if` block is **not** executed by the host VM.
+
+When JPF is invoked, the argument to the main() method is set to the method name from which JPF got invoked, which causes `runTestsOfThisMethod()` to execute exactly this method again, but this time under JPF. Instead of re-executing the same `TestJPF.verifyX()` method again (and becoming infinitely recursive), we use a native peer `JPF_gov_nasa_jpf_util_test_TestJPF` which intercepts the `verifyX()` call and simply returns true, i.e. this time *only* the `if` block gets executed.
+
+The rest of the host VM executed `TestJPF.verifyX()` checks the results of the JPF run, and accordingly throws an `AssertionError` in case it does not correspond to the expected result. The most common goals are
+
+ * `verifyNoPropertyViolation` - JPF is not supposed to find an error
+ * `verifyPropertyViolation` - JPF is supposed to find the specified property violation
+ * `verifyUnhandledException` - JPF is supposed to detect an unhandled exception of the specified type
+ * `verifyAssertionError` - same for AssertionErrors
+ * `verifyDeadlock` - JPF is supposed to find a deadlock
+
+Each of these methods actually delegate running JPF to a corresponding method whose name does not start with 'verify..'. These workhorse methods expect explicit specification of the JPF arguments (including SUT main class name and method names), but they return JPF objects, and therefore can be used for more sophisticated JPF inspection (e.g. to find out about the number of states).
+
+`TestJPF` also provides some convenience methods that can be used within test methods to find out which environment the code is executed from:
+
+ * `isJPFRun()` - returns true if the code is executed under JPF
+ * `isJUnitRun()` - returns true if the code is executed under JUnit by the host VM
+ * `isRunTestRun()` - returns true if the code is executed by RunTest.jar
+
+Here is an example of a typical test method that uses some of these features:
+
+~~~~~~~~ {.java}
+  @Test public void testIntFieldPerturbation() {
+
+    if (!isJPFRun()){ // run this outside of JPF
+      Verify.resetCounter(0);
+    }
+
+    if (verifyNoPropertyViolation("+listener=.listener.Perturbator",
+                                  "+perturb.fields=data",
+                                  "+perturb.data.class=.perturb.IntOverUnder",...
+                                  "+perturb.data.delta=1")){
+      // run this under JPF
+      System.out.println("instance field perturbation test");
+
+      int d = data; // this should be perturbated
+      System.out.println("d = " + d);
+
+      Verify.incrementCounter(0);
+
+    } else { // run this outside of JPF
+      assert Verify.getCounter(0) == 3;
+    }
+  }
+~~~~~~~~
+
+## Running JPF tests from command line ##
+To run JPF tests from the command line, use the RunTest.jar either from `jpf-core/build`, or the one that is distributed with your project containing the tests (`tools/RunTest.jar` for JPF projects). This is an executable jar that expects the test class and (optional) method test names as arguments. If no method names are provided, all `@Test` annotated methods are executed. Most projects have a convenience script `bin/test` to execute RunTest.jar.
+
+~~~~~~~~ {.bash}
+> bin/test gov.nasa.jpf.test.mc.data.PerturbatorTest testIntFieldPerturbation
+
+......................................... testing testIntFieldPerturbation
+  running jpf with args: +listener=.listener.Perturbator +perturb.fields=data +perturb.data.class=.perturb.IntOverUnder +perturb.data.field=gov.nasa.jpf.test.mc.data.PerturbatorTest.data +perturb.data.delta=1 gov.nasa.jpf.test.mc.data.PerturbatorTest testIntFieldPerturbation
+JavaPathfinder v5.x - (C) RIACS/NASA Ames Research Center
+
+
+====================================================== system under test
+application: gov/nasa/jpf/test/mc/data/PerturbatorTest.java
+arguments:   testIntFieldPerturbation 
+
+====================================================== search started: 9/10/10 7:03 PM
+instance field perturbation test
+d = 43
+d = 42
+...
+====================================================== search finished: 9/10/10 7:03 PM
+......................................... testIntFieldPerturbation: Ok
+
+......................................... execution of testsuite: gov.nasa.jpf.test.mc.data.PerturbatorTest SUCCEEDED
+.... [1] testIntFieldPerturbation: Ok
+......................................... tests: 1, failures: 0, errors: 0
+~~~~~~~~
+
+## Running JPF tests under JUnit ##
+
+This is the preferred way to execute JPF regression tests, which is usually done from an Ant build.xml script containing a standard target such as
+
+~~~~~~~~ {.xml}
+  ...
+  <target name="test" depends="build" description="run core regression tests" if="have_tests">
+     ...
+     <junit printsummary="on" showoutput="off" haltonfailure="yes"
+            fork="yes" forkmode="perTest" maxmemory="1024m" outputtoformatters="true">
+       <classpath>
+         <path refid="lib.path"/>
+         <pathelement location="build/tests"/>
+         ...
+       </classpath>
+       <batchtest todir="build/tests">
+          <fileset dir="build/tests">
+            <exclude name="**/JPF_*.class"/>
+            <include name="**/*Test.class"/>
+          </fileset>
+      </batchtest>
+    </junit>
+  </target>
+~~~~~~~~
+
+Most JPF projects have build.xml files you can use as examples.
+
+Please note this means that you should not have any inner classes, interfaces, annotation types etc. with a name ending with `"Test"` since JUnit would interpret these as test cases and most likely complain about missing constructors and `main()` methods.
+
+## Debugging tests ##
+
+Typically, JPF tests are only executed from within an IDE if they fail and need to be debugged. 
+
+Under NetBeans, this can be done by selecting the test class, and then executing the *Debug File* command from the context menu. This will pop up a dialog that lets you enter a specific test method to debug. This method requires a properly set up ide-file-target.xml, which comes with most JPF projects.
+
+Under Eclipse, you can select the test class and then execute **Debug As..** -> **Java Application**.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/listener.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,332 @@
+# Listeners #
+Listeners are perhaps the most important extension mechanism of JPF. They provide a way to observe, interact with and extend JPF execution with your own classes. Since listeners are dynamically configured at runtime, they do not require any modification to the JPF core. Listeners are executed at the same level like JPF, so there is hardly any limit of what you can do with them.
+
+![Figure 1: JPF Listeners](../graphics/listener-overview.svg){align=center width=800}
+
+The general principle is simple: JPF provides an observer pattern implementation that notifies registered observer instances about certain events at the search level and the VM level. These notifications cover a broad spectrum of JPF operations, from low level events like `instructionExecuted` to high level events like `searchFinished`. Each notification is parameterized with the corresponding source (either the `Search` or the `VM` instance), which can be then used by the notified listener to obtain more information about the event and the JPF's internal state.
+
+Configuration is usually done with the `listener` property, either from the command line, or a .jpf property file. Listeners can also be associated with annotations, to be automatically loaded whenever JPF encounters such an annotation. Applications can use the `@JPFConfig` annotation to explicitly specify JPF listeners. Lastly, if JPF is used in an embedded mode, listeners can be registered with an API.
+
+
+## Listener Types ##
+
+
+There are two basic listener interfaces, depending on corresponding event sources: `SearchListeners` and `VMListeners`. Since these interfaces are quite large, and listeners often need to implement both, we also provide "adapter" classes, i.e. implementors that contain all required method definitions with empty method bodies. Concrete listeners that extend these adapters therefore only have to override the notification methods they are interested in.
+
+The adapter classes are used for the majority of listener implementations, especially since they also support two other interfaces/extension mechanisms that are often used in conjunction with `Search` and `VMListeners`: 
+
+ 1. `Property` - to define program properties
+ 2. `PublisherExtension` - to produce output within [the JPF reporting system](report)
+
+`ListenerAdapter` is the bare adapter implementation for `SearchListener`, `VMListener` and `PublisherExtension`. This is what is mostly used to collect information during JPF execution (e.g. `CoverageAnalyzer` and `DeadlockAnalyzer`).
+
+`PropertyListenerAdapter` is used in case the listener implements a program property, i.e. it can terminate the search process. A prominent example of this category is `PreciseRaceDetector`.
+
+![Figure 2: Listener Types](../graphics/listeners.svg){align=center width=800}
+
+Choosing the right type for your listener is important, since JPF automatically registers listeners (and properties) based on this type. You can bypass and directly implement single listener interfaces, but then you also have to do the proper registrations.
+
+Usually, the notification alone is not enough, and the listener needs to acquire more information from JPF. For this purpose, we provide either the `Search` or the `VM` instance as notification arguments, and the listener has to use these as "Facades" to query or interact JPF. It therefore matters to implement the listener within the right package.
+
+
+## SearchListener ##
+
+
+`SearchListener` instances are used to monitor the state space search process, e.g. to create graphical representations of the state-graph. They provide notification methods for all major Search actions.
+
+~~~~~~~~ {.java}
+package gov.nasa.jpf.search;
+public interface SearchListener extends JPFListener {
+  void searchStarted (Search search);  
+  void stateAdvanced (Search search);       // got next state
+  void stateProcessed (Search search);      // state is fully explored
+  void stateBacktracked (Search search);    // state was backtracked one step (same path)
+  void stateStored (Search search);         // somebody stored the state
+  void stateRestored (Search search);       // previously generated state was restored (any path)
+  void propertyViolated (Search search);    // JPF encountered a property violation
+  void searchConstraintHit (Search search); // e.g. max search depth
+  void searchFinished (Search search);
+}}
+~~~~~~~~
+
+
+For the standard depth first search (`gov.nasa.jpf.search.DFSearch`), listener implementations can assume the following notification model:
+
+
+![Figure 3: Depth first listener notifications](../graphics/DFSListener.svg){align=center width=500}
+
+The most frequently used notifications are:
+
+`stateAdvanced` - to store additional, backtrackable state information in an associative array
+
+`stateBacktracked` - to restore additional state information
+
+`searchFinished` - to process listener results
+
+
+## VMListener ##
+
+
+This is a fat interface, reflecting various VM operations
+
+~~~~~~~~ {.java}
+package gov.nasa.jpf.jvm;
+public interface VMListener extends JPFListener {
+  //--- basic bytecode execution
+  void executeInstruction (JVM vm);  // JVM is about to execute the next instruction
+  void instructionExecuted (JVM vm); // JVM has executed an instruction
+
+  //--- thread operations (scheduling)
+  void threadStarted (JVM vm);       // new Thread entered run()
+  void threadBlocked (JVM vm);       // thread waits to acquire a lock
+  void threadWaiting (JVM vm);       // thread is waiting for signal
+  void threadNotified (JVM vm);      // thread got notified
+  void threadInterrupted (JVM vm);   // thread got interrupted
+  void threadTerminated (JVM vm);    // Thread exited run()
+  void threadScheduled (JVM vm);     // new thread was scheduled by JVM
+
+  //--- class management
+  void classLoaded (JVM vm);         // new class was loaded
+
+  //--- object operations
+  void objectCreated (JVM vm);       // new object was created
+  void objectReleased (JVM vm);      // object was garbage collected
+  void objectLocked (JVM vm);        // object lock acquired
+  void objectUnlocked (JVM vm);      // object lock released
+  void objectWait (JVM vm);          // somebody waits for object lock
+  void objectNotify (JVM vm);        // notify single waiter for object lock
+  void objectNotifyAll (JVM vm);     // notify all waiters for object lock
+
+  void gcBegin (JVM vm);             // start garbage collection
+  void gcEnd (JVM vm);               // garbage collection finished
+
+  void exceptionThrown (JVM vm);     // exception was thrown
+
+  //--- ChoiceGenerator operations  
+  void choiceGeneratorSet (JVM vm);  // new ChoiceGenerator registered
+  void choiceGeneratorAdvanced (JVM vm); // new choice from current ChoiceGenerator
+  void choiceGeneratorProcessed (JVM vm); // current ChoiceGenerator processed all choices  
+}
+~~~~~~~~
+
+
+The most commonly used methods are the instruction notifications:
+
+`executeInstruction` - is called before a bytecode instruction gets executed by the VM. The listener can even use this to skip and/or replace this instruction, which is useful for non-invasive instrumentation.
+
+`instructionExecuted` - is the post-execution notification, which is suitable to keep track of execution results (method invocations, assigned field values, branch results etc.)
+
+
+## Example ##
+
+The following example is a slightly abbreviated form our race detector. The basic idea is simple: every time we encounter a new scheduling point (i.e. new `ThreadChoiceGenerator` object) that is due to a field access on a shared object, we check if any of the other runnable threads is currently accessing the same field on the same object. If at least one operation is a `putfield`, we have a potential race.
+
+The example shows three aspects that are quite typical: 
+
+  1. listeners often use only a small number of notification methods
+
+  2. they often do not require a huge amount of code (most expensive operations are performed by the `VM` and the `Search` objects)
+
+  3. sometimes you have to dig deep into JPF internal constructs, to extract things like `ThreadInfo`, `FieldInfo` and `ChoiceGenerator` instances
+
+~~~~~~~~ {.java}
+public class PreciseRaceDetector extends PropertyListenerAdapter {
+  FieldInfo raceField;
+  ...
+  //--- the Property part
+  public boolean check(Search search, JVM vm) {
+    return (raceField == null);
+  }
+
+  //--- the VMListener part
+  public void choiceGeneratorSet(JVM vm) {
+    ChoiceGenerator<?> cg = vm.getLastChoiceGenerator();
+
+    if (cg instanceof ThreadChoiceFromSet) {
+      ThreadInfo[] threads = ((ThreadChoiceFromSet)cg).getAllThreadChoices();
+      ElementInfo[eiCandidates = new ElementInfo[threads.length](]);
+      FieldInfo[fiCandidates = new FieldInfo[threads.length](]);
+
+      for (int i=0; i<threads.length; i++) {
+        ThreadInfo ti = threads[i];
+        Instruction insn = ti.getPC();
+        
+        if (insn instanceof FieldInstruction) { // Ok, its a get/putfield
+          FieldInstruction finsn = (FieldInstruction)insn;
+          FieldInfo fi = finsn.getFieldInfo();
+
+          if (StringSetMatcher.isMatch(fi.getFullName(), includes, excludes)) {
+            ElementInfo ei = finsn.peekElementInfo(ti);
+
+            // check if we have seen it before from another thread
+            int idx=-1;
+            for (int j=0; j<i; j++) {
+              if ((ei ## eiCandidates[&& (fi ## fiCandidates[j](j])))) {
+                idx = j;
+                break;
+              }
+            }
+
+            if (idx >= 0){ // yes, we have multiple accesses on the same object/field
+              Instruction otherInsn = threads[idx].getPC();
+              if (isPutInsn(otherInsn) || isPutInsn(insn)) {
+                raceField = ((FieldInstruction)insn).getFieldInfo();
+                ..
+                return;
+              }
+            } else {
+              eiCandidates[i] = ei;
+              fiCandidates[i] = fi;
+            }
+          }
+        }
+      }
+    }
+  }
+
+  public void executeInstruction (JVM jvm) {
+    if (raceField != null) {  // we're done, report as quickly as possible
+      ThreadInfo ti = jvm.getLastThreadInfo();
+      ti.breakTransition();
+    }
+  }
+}
+~~~~~~~~
+
+## Instantiation ##
+
+Explicit instantiation of a listener (e.g. from a JPF shell) can be done in any way. If the listener is specified as a JPF property, it's class either needs to have a default constructor, or a constructor that takes a single `gov.nasa.jpf.Config` argument. The `Config` object that is passed into this constructor by JPF is the same that was used for the initialization of JPF itself. This is the preferred method if the listener has to be parameterized. In case of the `PreciseRaceDetector` example, this can be used to filter relevant fields with regular expressions:
+
+~~~~~~~~ {.java}
+public class PreciseRaceDetector extends PropertyListenerAdapter {
+  ...
+  StringSetMatcher includes = null;
+  StringSetMatcher excludes = null;
+  
+  public PreciseRaceDetector (Config conf) {
+    includes = StringSetMatcher.getNonEmpty(conf.getStringArray("race.include"));
+    excludes = StringSetMatcher.getNonEmpty(conf.getStringArray("race.exclude"));
+  }
+  ...
+  public void choiceGeneratorSet(JVM vm) {
+    ...
+        FieldInfo fi =..
+        if (StringSetMatcher.isMatch(fi.getFullName(), includes, excludes))
+     ...
+  }
+~~~~~~~~
+
+
+## Configuration ##
+
+Listener configuration can be done in a number of ways: via JPF properties from the command line or a .jpf file, via JPF APIs from a JPF shell (a program invoking JPF), or from the system under test by using Java annotations (i.e. without code modification).
+
+Since listeners are executed by the host VM, they have to be in the `CLASSPATH` (`jpf-core.native_classpath` property).
+
+
+### command line ###
+
+
+the *listener* property can be used to specify a colon separated list of listener class names:
+
+~~~~~~~~ {.bash}
+bin/jpf ... +listener=x.y.MyFirstListener,x.z.MySecondListener ...
+~~~~~~~~
+
+
+### .jpf property file ###
+
+
+If you have several listeners and/or a number of other JPF options, it is more convenient to add the `listener` property to a .jpf file:
+
+~~~~~~~~ {.bash}
+# Racer-listener.jpf - JPF mode property file to detect data races in jpftest.Racer
+target = jpftest.Racer
+listener=gov.nasa.jpf.tools.PreciseRaceDetector
+~~~~~~~~
+
+
+### Autoload Annotations ###
+
+
+Consider your system under test is marked up with a Java annotation that represent properties. For example, you can use the `@NonNull` annotation to express that a method is not allowed to return a `null` value:
+
+~~~~~~~~ {.java}
+import gov.nasa.jpf.NonNull; 
+  ...
+  @NonNull X computeX (..) {
+    //.. some complex computation
+  }
+  ...
+~~~~~~~~
+
+You can use .jpf property files (or the command line, if you love to type) to tell JPF that it should automatically load and register a corresponding listener (e.g. `NonNullChecker`) if it encounters such a `@NonNull` annotation during class loading:
+
+~~~~~~~~ {.bash}
+..
+listener.autoload = gov.nasa.jpf.NonNull,...
+listener.gov.nasa.jpf.NonNull = gov.nasa.jpf.tools.NonNullChecker
+...
+~~~~~~~~
+
+
+### @JPFConfig annotation (SuT) ###
+
+
+You can also explicitly direct JPF to load the listener from within your application by using the `@JPFConfig` annotation:
+
+~~~~~~~~ {.java}
+import gov.nasa.jpf.JPFConfig;
+..
+// set JPF properties via properties at class load time
+@JPFConfig ({"listener+=.tools.SharedChecker", ..})
+public class TestNonShared implements Runnable {
+  ...
+}
+~~~~~~~~
+
+However, this is not recommended outside JPF tests - the application would run, but not compile without JPF.
+
+
+### Verify API (SuT) ###
+
+
+A less often used method is to set listeners is to use the `gov.nasa.jpf.vm.Verify` API from within your application. With this, you can control the exact load time of the listener (but be aware of backtracking). With this, the above example would become
+
+~~~~~~~~ {.java}
+import gov.nasa.jpf.vm.Verify;
+..
+public class TestNonShared implements Runnable {
+  ...
+  public static void main (String[] args){
+    
+    // set JPF properties programmatically
+    Verify.setProperties("listener+=.tools.SharedChecker", ...);
+    ..
+  }
+}
+~~~~~~~~
+
+This method should only be used in special cases (models written explicitly for JPF verification), since it does not run outside JPF.
+
+
+### JPF API (embedded mode) ###
+
+
+If JPF is explicitly started from within another application, listeners can be instantiated at will and configured via the `JPF.addListener(..)` API:
+
+~~~~~~~~ {.java}
+MyListener listener=new MyListener(..);
+..
+Config config = JPF.createConfig( args);
+JPF jpf = new JPF( config);
+jpf.addListener(listener);
+jpf.run();
+..
+~~~~~~~~
+
+Most listeners tend to fall into three major categories: 
+
+1. system class (e.g. for logging) - is usually configured via the default.properties.
+2. complex properties - is configured with an application specific mode property file.
+3. JPF debugging - is specified via the command line (`+key=value` overrides).
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/logging.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,31 @@
+# The JPF Logging API #
+There is one simple rule: do not use `System.out` or `System.err` for any permanent logging
+
+
+Of course we all do this temporarily during debugging, but it really shouldn't stay in the code. The logging infrastructure is quite easy to use. Just declare a static `Logger` instance with an appropriate id (either package or logging topic) at the top of your class, and then use the `Logger` API to create output:
+
+~~~~~~~~ {.java}
+...
+import java.util.logging.Level;
+import java.util.logging.Logger;
+
+package x.y.z;
+
+class MyClass .. {
+  static Logger log = JPF.getLogger("x.y.z");
+  ...
+    log.severe("there was an error");
+  ...
+    log.warning("there was a problem");
+  ...
+    log.info("something FYI");
+  ...
+    if (log.isLoggable(Level.FINE)){    // (1) don't create garbage
+        log.fine("this is some detailed info about: " + something);
+    }
+  ...
+}
+~~~~~~~~
+
+Note that there is only one instance for each `Logger` ID, i.e. you can have a corresponding static field in all your relevant classes, and don't have to share the fields. Another aspect that is mostly important for the lower log levels (e.g. `FINE`) is that you should't concatenate log messages in operations that occur frequently, since the corresponding `StringBuilder` instances can cause performance degradations even if the log level is not set (the arguments still get evaluated). In this case, encapsulate the logging in `log.isLoggable(level){..}` blocks.
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/mercurial.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,56 @@
+# Mercurial in 5 Minutes #
+
+[Mercurial](http://www.selenic.com/mercurial) is a *distributed version control system* (DVCS) of the same category such as the likes of [Git](http://git-scm.com/) or [Bazaar](http://bazaar.canonical.com/en/). If you know nothing else about DVCS, this means mostly one thing - **all repositories are created equal**. There is no such thing as a different repository format for public and private repositories. All repositories (that are synchronized) have the same, stored history information.
+
+Yes, this means you can finally synchronize your working repos with more than one "master" repository, e.g. with several local ones, closed workgroup repos, and a public master repo (that just happens to be designated as such).
+
+Each Mercurial repository consists of an (optional) working copy of your files, and a `.hg` directory in your repo root dir that holds all the version control info. Be careful not to delete the `.hg` dir, otherwise your repo is reduced to just a snapshot of your current working files.
+
+A central concept of DVCS is the *change set* - think of it as the diff of all files that have been changed when you do a commit. This is what DVCS store (e.g. Mercurial in the `.hg` dir) and compare between different repositories. One implication of this is that you can't do partial commits like in CVS or SVN (e.g. by just committing changes within a certain subdirectory). You always have to execute the Mercurial commands in the top dir of the repository you are working in.
+
+If you have previously worked with CVS or SVN, another difference you have to wrap your head around is that there are commands that work locally, and commands that interact with the remote repo. __The `commit` and `update` commands are only local__. The `push` and `pull` commands synchronize your local repo with an external one (like commit and update did in CVS/SVN).
+
+Here are the main commands to interact with Mercurial:
+
+![](mercurial.png)
+
+**hg clone <url>** - this is the first command that clones an external repository (either from `file:///...` or `http://...` URLs). It creates both a working copy and the `.hg` directory (with contents)
+
+**hg init** - is what you do if you create a local repository for which there is no external one yet. Just create your files, `cd` into the top directory, and execute the command (which will create the `.hg` for you)
+
+**hg pull [-u] <url>** - updates the repo you are currently in from the provided URL. Note that your working copy is only updated if you use the `-u` option
+
+**hg incoming <url>** - is the little brother of `pull`. It just tells you if there are changesets in the remote repository you would pull
+
+**hg status** - tells you if there are uncommitted changes in your working copy that have to be committed to the local `.hg` directory before you can `push` or `pull`
+
+**hg diff** - does a bit more, it also shows you a diff file with the uncommitted changes
+
+**hg add <file>** - adds a file to the repo
+
+**hg remove <file>** - removes a file from the repo
+
+**hg addremove** - adds all new files of the working copy that are not in the repository yet, and removes all which are not in the working copy anymore
+
+**hg commit** - saves changes in your working copy to your local `.hg`. Do this early and often, this is now just a local operation that doesn't change anything outside the repo you are working with
+
+**hg update** - would update your working copy from your local `.hg`. It is rarely used if you pull with the `-u` option
+
+**hg push <url>** - pushes the relevant changesets of your local `.hg` back to the external repo with the provided URL. Make sure you have no uncommitted changes (Mercurial would refuse to push), and - in case the external repo is shared - that you pulled/merged all changesets of the external repo before you push
+
+**hg outgoing <url>** - is the dry run version of a push, it tells you if there are changesets that would have to be pushed  
+
+**hg revert** - reverts your working copy to a previous version stored in your local `.hg`
+
+**hg heads** - tells you if there are branches in your repo, which usually happens if you pull from a changed external repo while having un-pushed local changes that are committed
+
+**hg merge** - gets rid of multiple heads. Make sure to get rid of these by merging as soon as you detect them, it only gets more difficult with more external and local changes. Once there are collisions, you are back to the CVS/SVN merge mess
+
+You can always obtain more information by executing
+~~~~~~~~
+#!sh
+> hg help [command]
+~~~~~~~~
+If you don't list a command, all available ones will be displayed.
+
+Commands that refer to external repos take URLs such as `http://babelfish.arc.nasa.gov/hg/jpf/jpf-core` as arguments.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/mji.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,214 @@
+# Model Java Interface (MJI) #
+## Purpose ##
+
+Even if it is just a Java application (i.e. solely consists of Java classes), JPF can be viewed as a Java Virtual Machine (JVM) in itself. The consequence is that (*.class) class files, and even the same files at times, are processed in two different ways in a JVM running JPF
+
+  * as ordinary Java classes managed and executed by the host JVM (standard Java library classes, JPF implementation classes)
+  * as "modeled" classes managed and processed (verified) by JPF
+
+Class lookup in both layers is based on the CLASSPATH environment variable / command line parameter, but this should not obfuscate the fact that we have to clearly distinguish between these two modes. In particular, JPF (i.e. the "Model" layer) has its own class and object model, which is completely different and incompatible to the (hidden) class and object models of the underlying host JVM executing JPF
+
+![Figure 1: JPF Layers](../graphics/jpf-layers.svg){align=center width=560}
+
+Each standard JVM supports a so called Java Native Interface (JNI), that is used to delegate execution from the Java level (i.e. JVM controlled bytecode) down into the (platform dependent) native layer (machine code). This is normally used to interface certain functionalities to the platform OS / architecture (e.g. I/O or graphics).
+
+Interestingly enough, there exists a analogous need to lower the "execution" level in JPF, from JPF controlled bytecode into JVM controlled bytecode. According to this analogy, the JPF specific interface is called Model Java interface (MJI).
+
+Even though MJI offers a wide range of applications, there are three major usages for delegating bytecode execution into the host JVM:
+
+ 1. Interception of native methods - without a abstraction lowering mechanism, JPF would be forced to completely ignore native methods, i.e. would fail on applications relying on the side effects of such methods, which is not acceptable (even if  many native methods indeed can be ignored if we restrict the set of verification targets)
+
+ 2. Interfacing of JPF system level functionality - some system level functions of standard library classes (esp. java.lang.Class, java.lang.Thread) have to be intercepted even if they are not native because they have to affect the JPF internal class, object and thread model (etc. loading classes, creating / starting threads). It should be noted that MJI can also be used to extend the functionality of JPF without changing its implementation.
+
+3. State space reduction - by delegating bytecode execution into the non-state-tracked host JVM, we can cut off large parts of the state space, provided that we know the corresponding method side effects are not relevant for property verification (e.g. `System.out.println(..)`)
+
+Besides these standard usages, there exist more exotic applications like collecting information about JPF state space exploration and making it available both to JPF and the verification target.
+
+
+## MJI Components ##
+
+
+The basic functionality of MJI consists of a mechanism to intercept method invocations, and delegate them by means of Java reflection calls to dedicated classes. There are two types of classes involved, residing at different layers:
+
+  * Model Classes - these classes execute by the VM of JPF, which might be completely unknown to the host JVM
+  * Native Peers - these classes, implemented by `NativePeer` subclasses, contain the implementations of the methods to intercept, and to execute by the host JVM
+
+As part of the JPF implementation, MJI automatically takes care of determining which method invocations have to be intercepted by looking up the corresponding native peer methods
+
+![Figure 2: MJI Functions](../graphics/mji-functions.svg){align=center width=600}
+
+This would not be very useful without being able to access the JPF object model (or other JPF intrinsics), from inside the native peer methods. Instead of requiring all native peers implementation to reside in a JPF internal package, there exists an interface class `MJIEnv` that provide access to the JPF internal structure in a controlled way. `NativePeer` classes  residing in `gov.nasa.jpf.vm` (i.e. the same package as `MJIEnv`) can reach all internal JPF features. Outside this package, the available API in `MJIEnv` is mostly restricted to the access JPF object (getting and setting values).
+
+![Figure 3: MJI Call Sequence](../graphics/mji-call.svg){align=center width=580}
+
+Before a native peer method can be used, JPF has to establish the correspondence between the model class and the native peer. This takes place at load time of the model class. MJI uses a special name mangling scheme to lookup native peers, using the model class package name and class name to deduce the native peer class name.
+
+![Figure 3: MJI name mangling](../graphics/mji-mangling.svg){align=center width=560}
+
+Since the model class package is encoded in the native peer name, the package of the native peer can be chosen freely. In analogy to JNI, native peers methods names include the signature of the model method by encoding its parameter types. If there is no potential ambiguity, i.e. mapping from native peer methods to model class methods is unique, signature encoding is not required.
+
+Each native peer, which is an instance of a `NativePeer` subclass, is associated with exactly one `ClassInfo` instance.
+All the native peer methods to be intercepted have to be `public` and annotated with `gov.nasa.jpf.annotation.MJI`. 
+Moreover, MJI requires them to have two parameters: 
+
+  * An instance of `MJIEnv` which can be used to access JPF internal constructs
+  * An integer which is a handle for the corresponding JPF `this` object (or the `java.lang.Class` object in case of a static method) including the method to be intercepted
+
+See [Mangling for MJI](mji/mangling) for more details and examples of mangling.
+
+Going beyond the JNI analogy, MJI can also be used to intercept
+
+  * non-native methods (i.e. the lookup process is driven by the methods found in the native peer, not the `native` attributes in the model class. This can be particularly useful in case the class is used from both as a model class and a JVM class (e.g. `gov.nasa.jpf.vm.Verify`), using a method body that directly refers to the native peer
+  * class initialization (the corresponding native peer method has to be named `$clinit(MJIEnv env, int clsRef)`)
+  * constructors (the corresponding native peer method has to be named `$init__<sig>(MJIEnv env,int objRef, <ctor-params>)` and the normal signature mangling rules apply)
+
+
+It is important to note that type correspondence does NOT include references. All references (object types) on the JPF side are transformed in handles (int values) on the JVM side. The passed in `MJIEnv` parameter has to be used to convert/analyze the JPF object. Since MJI per default uses the standard Java reflection call mechanism, there is a significant speed penalty (lookup, parameter conversion etc.), which again is a analogy to JNI.
+
+Even if it is not directly related to MJI, it should be mentioned that some JPF specific model classes cannot be loaded via the CLASSPATH (e.g. `java.lang.Class`), since they contain JPF based code that is not compatible with the host JVM (e.g. relying on native methods that refer to JPF functionality). Such classes should be kept in separate directories / jars that are specified with the JPF command line option `-jpf-bootclasspath` or `-jpf-classpath`. This is mostly the case for system classes. On the other hand, model classes don't have to be JPF specific. It is perfectly fine to provide a native peer for a standard Java class (e.g. `java.lang.Character`), if only certain methods from that standard class needs to be intercepted. Native peers can contain any number of non-"native" methods and fields, but those should not be annotated with `@MJI` to avoid lookup problems.
+
+## Tools ##
+
+To ease the tedious process of manually mangle method names, MJI includes a tool to automatically create skeletons of native peers from a given Model class, called `GenPeer`. The translation process uses Java reflection, i.e. the model class needs to be in the CLASSPATH and is specified in normal dot notation (i.e. not as a file).
+
+![Figure 4: The GenPeer tool](../graphics/genpeer.svg){align=center width=470}
+
+There exist a number of command line options that can be displayed by calling `GenPeer` without arguments. `GenPeer` per default writes to stdout, i.e. the output has to be redirected into a file.
+
+Since method invocation by reflection used to be a slow operation, we previously also had a tool called `GenPeerDispatcher`, which used method signature hash-codes to explicitly dispatch native peer methods. With recent improvements in JVM performance, this tool became obsolete.
+
+
+## Example ##
+
+
+The following example is an excerpt of a JPF regression test, showing how to intercept various different method types, and using `MJIEnv` to access JPF objects.
+
+
+### Model class (JPF side) ###
+
+
+This is executed by JPF, which means it needs to be in JPF's  `vm.classpath` setting. 
+
+~~~~~~~~ {.java}
+public class TestNativePeer {
+    static int sdata;
+    
+    static {
+      // only here to be intercepted
+    }
+    
+    int idata;
+    
+    TestNativePeer (int data) {
+      // only here to be intercepted
+
+    }
+  
+    public void testClInit () {
+      if (sdata != 42) {
+        throw new RuntimeException("native 'clinit' failed");
+      }
+    }
+
+    public void testInit () {
+      TestNativePeer t = new TestNativePeer(42);
+
+      if (t.idata != 42) {
+        throw new RuntimeException("native 'init' failed");
+      }
+    }
+
+    native int nativeInstanceMethod (double d, char c, boolean b, int i);
+
+    public void testNativeInstanceMethod () {
+
+      int res = nativeInstanceMethod(2.0, '?', true, 40);
+      if (res != 42) {
+        throw new RuntimeException("native instance method failed");
+      }
+    }
+    
+    native long nativeStaticMethod (long l, String s);
+
+    public void testNativeStaticMethod () {
+      long res =  nativeStaticMethod(40, "Blah");
+
+      if (res != 42) {
+        throw new RuntimeException("native instance method failed");
+
+      }
+    }
+    
+    native void nativeException ();
+    
+    public void testNativeException () {
+      try {
+        nativeException();
+      } catch (UnsupportedOperationException ux) {
+        String details = ux.getMessage();
+
+        if ("caught me".equals(details)) {
+          return;
+        } else {
+          throw new RuntimeException("wrong native exception details: " +
+                                     details);
+        }
+      } catch (Throwable t) {
+        throw new RuntimeException("wrong native exception type: " +
+                                   t.getClass());
+      }
+
+      throw new RuntimeException("no native exception thrown");
+    }
+  }
+~~~~~~~~
+
+
+### Native Peer class (host VM side) ###
+
+
+This is executed by the host VM (i.e. at the same level like JPF itself), so make sure it is in your CLASSPATH.
+
+~~~~~~~~ {.java}
+public class JPF_gov_nasa_jpf_vm_TestNativePeer {
+
+    @MJI
+    public static void $clinit (MJIEnv env, int rcls) {
+      env.setStaticIntField(rcls, "sdata", 42);
+    }
+
+    @MJI
+    public static void $init__I (MJIEnv env, int robj, int i) {
+      env.setIntField(robj, "idata", i);
+    }
+
+    // preferably use full signature mangling
+    @MJI
+    public static int nativeInstanceMethod__DCZI__I (MJIEnv env, int robj,
+                                            double d, char c,
+                                            boolean b, int i) {
+      if ((d ## 2.0) && (c  ## '?') && b) {
+        return i + 2;
+      }
+      return 0;
+    }
+
+    //..but it also works without, if there is no overloading (don't be lazy!) 
+    @MJI
+    public static long nativeStaticMethod (MJIEnv env, int rcls,
+                                           long l, int stringRef) {
+      String s = env.getStringObject(stringRef);
+      if ("Blah".equals(s)) {
+        return l + 2;
+      }
+      return 0;
+    }
+
+    @MJI
+    public static void nativeException____V (MJIEnv env, int robj) {
+      env.throwException("java.lang.UnsupportedOperationException",
+                         "caught me");
+    }
+  }
+~~~~~~~~
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/mji/mangling.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,200 @@
+# Mangling for MJI #
+## Mangling Methods ##
+Suppose your method looks like 
+
+~~~~~~~~ {.java}
+T1 foo(T2 x, T3 y, ...)
+~~~~~~~~
+
+where the `Ti` are Java types.
+
+If `T1` is a primitive type or `void`, then the mangled MJI method looks
+like
+
+~~~~~~~~ {.java}
+public static T1 foo__MT2MT3...__MT1(...)
+~~~~~~~~
+
+where the `MTi` are the mangled versions of the `Ti`.  
+Mangling of types is described in the Mangling Types section below. 
+Note that `T1` appears twice, once not mangled (`T1`) and once mangled
+(`MT1`).  The `__` is two consecutive underscores: `_` followed by
+`_`.
+
+As a not-so-special case, if `foo` has no arguments, then the mangled method
+will have four consecutive underscores:
+
+~~~~~~~~ {.java}
+  `T1 foo()`[[br]]
+~~~~~~~~
+
+goes to
+
+~~~~~~~~ {.java}
+  `public static T1 foo____MT1(...)`
+~~~~~~~~
+
+If `T1` is not a primitive type, then the mangled `MJI` method looks like 
+
+~~~~~~~~ {.java}
+  `public static int foo__MT2MT3...__MT1`
+~~~~~~~~
+
+where the `MTi` are as above.  Note that `T1` only appears once in this
+case.  The method's return type is `int`.  As before, a method with no
+arguments gets mangled to something with four consecutive underscores.
+
+Also, the use of generics is ignored when mangling names.
+
+
+## Mangling Constructors ##
+Constructors are treated as methods named `$init` with return type `void`.
+
+
+## Mangling Static Initializers ##
+Static initializers are treated as methods named `$clinit` with no
+arguments and return type `void`.  Thus, their MJI versions always
+have the mangled signature:
+
+~~~~~~~~ {.java}
+public static void $clinit____V (MJIEnv env, int clsObjRef)
+~~~~~~~~
+
+or the equivalent unmangled signature:
+
+~~~~~~~~ {.java}
+public static void $clinit (MJIEnv env, int clsObjRef)
+~~~~~~~~
+
+
+## Mangling Types ##
+  - Convert primitives and `void` as follows
+
+    |Java Type|Mangled Type|
+    | ------- |:---:|
+    |`boolean`|`Z`|
+    |`byte`   |`B`|
+    |`char`   |`C`|
+    |`short`  |`S`|
+    |`int`    |`I`|
+    |`long`   |`J`|
+    |`float`  |`F`|
+    |`double` |`D`|
+    |`void`   |`V`|
+
+  - Convert a non-array reference type `T` in package `x.y`
+    (e.g. `java.lang.String`) as follows
+    - `x.y.T`   --> `Lx_y_T_2`
+    - Example: `java.lang.String` --> `Ljava_lang_String_2`
+
+  - Convert an array of primitive type `T`
+    (e.g. `byte[]`) as follows:
+    - `T[]` --> `_3MT`  where `MT` is the mangled version of `T`
+      (e.g. for `T=byte`, `MT=B`)
+    - Example: `byte[]` --> `_3B`
+
+  - Convert an array of reference type `T` in package `x.y`
+    (e.g. `java.lang.String[]`) as follows:
+    - `x.y.T[]` --> `_3Lx_y_T_2`
+    - Example: `java.lang.String[]` --> `_3Ljava_lang_String_2`
+
+
+## Method Examples ##
+
+ `void` return type, single primitive argument:
+
+~~~~~~~~ {.java}
+  public static void resetCounter(int id)
+-->
+  public static final void resetCounter__I__V(MJIEnv env, int objref, int id)
+~~~~~~~~
+
+ Primitive return type, no arguments:
+
+~~~~~~~~ {.java}
+  public native boolean isArray()
+-->
+  public static boolean isArray____Z(MJIEnv env, int objref)
+~~~~~~~~
+
+ Primitive return type, single primitive argument:
+
+~~~~~~~~ {.java}
+  public static double abs(double a)
+-->
+  public static double abs__D__D(MJIEnv env, int clsObjRef, double a)
+~~~~~~~~
+
+ Primitive return type, two primitive arguments:
+
+~~~~~~~~ {.java}
+  public static long min(long a, long b)
+--> 
+  public static long min__JJ__J(MJIEnv env, int clsObjRef, long a, long b)
+~~~~~~~~
+
+
+ `void` return type, arguments include an array of a primitive type:
+
+~~~~~~~~ {.java}
+  public native void write (byte[] buf, int off, int len);
+-->
+  public static void write___3BII__V(MJIEnv env, int objref,
+                                     int bufRef, int off, int len)
+~~~~~~~~
+
+
+ `void` return type, argument is an array of a reference type: 
+
+~~~~~~~~ {.java}
+   public static void print(String s)
+-->
+  public static void print___3Ljava_lang_String_2__V(MJIEnv env, int clsRef, int argsRef)
+~~~~~~~~
+
+ Array of reference types returned, no arguments: 
+ 
+~~~~~~~~ {.java}
+  public native Annotation[] getAnnotations()
+-->
+  public static int getAnnotations_____3Ljava_lang_annotation_Annotation_2(MJIEnv env, int robj)
+~~~~~~~~
+   Notice there are 5 underscores before the `3L`: two marking the
+   arguments, two marking the return type, and one from the `_3`
+   signalling an array.
+
+ Array of reference types using generics returned, no arguments:
+
+~~~~~~~~ {.java}
+  public native Class<?>[] getParameterTypes()
+-->
+  public static int getParameterTypes_____3Ljava_lang_Class_2(MJIEnv env, int objref)
+~~~~~~~~
+    
+Note: the use of generics is ignored in the mangling.
+
+
+
+## Constructor Examples ##
+
+Constructors are treated as though they were methods named `$init`
+returning `void`, so the method examples above should also be helpful
+for constructors.  Here are a few more examples.
+
+In the class `ConsoleOutputStream`:
+
+~~~~~~~~ {.java}
+  public ConsoleOutputStream()
+-->
+  public static void $init____V(MJIEnv env, int objref)
+~~~~~~~~
+
+In the class `AtomicLongFieldUpdater`:
+
+~~~~~~~~ {.java}
+  protected AtomicLongFieldUpdater(Class<T> objClass, String fieldName)
+-->
+  public static void $init__Ljava_lang_Class_2Ljava_lang_String_2__V
+                         (MJIEnv env, int objRef,
+                          int tClsObjRef, int fNameRef)
+~~~~~~~~
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/modules.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,21 @@
+# JPF Runtime Modules #
+
+JPF is partitioned into separate projects that all follow the same directory layout and build process. Modules can be distributed as source or binary distributions. Binary distributions are just slices through the directory tree of a source distribution that preserve the permanent build artifact, i.e. both distribution forms are runtime-compatible.
+
+![Figure: JPF Modules](../graphics/jpf-project.svg){align=center width=750}
+ 
+The main artifacts are the *.jar files created and stored in the `build` directory. We can divide this into classes that are executed by the host VM (i.e. have to be in JPF's `native_classpath` setting), and classes that are executed by JPF itself (i.e. have to be in JPF's `classpath` setting). The first category includes [listeners](listener) and [native peers](mji), the second one model classes (compiled from `src/classes`) and annotations, i.e. the system under test code.
+
+The build process is [Ant](http://ant.apache.org/) based, which means every source distribution comes with a build.xml script that implements the basic build targets `clean`, `compile`, `build` and `test`.
+
+We do not include required 3rd party runtime and build libraries in the project distributions.
+The `compile` Ant target uses the standard `javac` command which requires a full JDK installation. `test` generally executes a JUnit based regression test suite. Both JUnit and Ant libraries are also need to be installed.
+
+<included in the jpf-core distribution, which also contains the minimal RunAnt.jar executable jar which can be distributed with other JPF projects to use the jpf-core provided 3rd party build tools.>
+
+<The `lib` directory contains 3rd party libraries that are required at runtime of the project (like bcel.jar in jpf-core).>
+
+<tools contains programs and libraries that are used by the build process (like ant.jar and junit.jar in jpf-core).>
+
+For convenience reasons, JPF modules come with corresponding NetBeans and Eclipse configurations, i.e. can be directly opened as projects within these IDEs.
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/partial_order_reduction.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,67 @@
+# On-the-fly Partial Order Reduction #
+
+The number of different scheduling combinations is the prevalent factor for the state space size of concurrent programs. Fortunately, for most practical purposes it is not necessary to explore all possible instruction interleavings for all threads. The number of scheduling induced states can be significantly reduced by grouping all instruction sequences in a thread that cannot have effects outside this thread itself, collapsing them into a single transition. This technique is called partial order reduction (POR), and typically results in more than 70% reduction of state spaces.
+
+JPF employs an on-the-fly POR that does not rely on user instrumentation or static analysis. JPF automatically determines at runtime which instructions have to be treated as state transition boundaries. If POR is enabled (configured via `vm.por` property), a forward request to the VM executes all instructions in the current thread until one of the following conditions is met:
+
+ - the next instruction is scheduling relevant
+ - the next instruction yields a "nondeterministic" result (i.e. simulates random value data acquisition)
+
+Detection of both conditions are delegated to the instruction object itself (`Instruction.execute()`), passing down information about the current VM execution state and threading context. If the instruction is a transition breaker, it creates a ChoiceGenerator and schedules itself for re-execution.
+
+~~~~~~~~ {.java}
+executeStep () {
+  ..
+  do {
+    if ((nextPc # executeInstruction()) #= pc) {
+      break;
+    } else {
+      pc = nextPc;
+    }
+    ..
+  } while (pc != null);
+  ..
+}
+~~~~~~~~
+
+Each bytecode instruction type corresponds to a concrete gov.nasa.jpf.Instruction subclass that determines scheduling relevance based on the following factors:
+
+ * **Instruction Type** - due to the stack based nature of the JVM, only about 10% of the Java bytecode instructions are scheduling relevant, i.e. can have effects across thread boundaries. The interesting instructions include direct synchronization (`monitorEnter`, `monitorexit`, `invokeX` on synchronized methods), field access (`putX`, `getX`), array element access (`Xaload`, `Xastore`), and invoke calls of certain Thread (`start()`, `sleep()`, `yield()`, `join()`) and Object methods (`wait()`, `notify()`).
+ * **Object Reachability** - besides direct synchronization instructions, field access is the major type of interaction between threads. However, not all putX / getX instructions have to be considered, only the ones referring to objects that are reachable by at least two threads can cause data races. While reachability analysis is an expensive operation, the VM already performs a similar task during garbage collection, which is extended to support POR.
+ * **Thread and Lock Information** - even if the instruction type and the object reachability suggest scheduling relevance, there is no need to break the current transition in case there is no other runnable thread. In addition, lock acquisition and release (`monitorenter`, `monitorexit`) do not have to be considered as transition boundaries if there they happen recursively - only the first and the last lock operation can lead to rescheduling.
+
+![Figure 1: Scheduling Relevance Filters](../graphics/por-scheduling-relevance.svg){align=center width=650}
+
+While JPF uses these informations to automatically deduce scheduling relevance, there exist three mechanisms to explicitly control transition boundaries (i.e. potential thread interleavings)
+
+ 1. `Attributor` - a configurable concrete class of this type is used by JPF during class loading to determine object, method and field attributes of selected classes and class sets. The most important attributes with respect to POR are method atomicity and scheduling relevance levels: (a) never relevant, (b) always scheduling relevant, (c) only relevant in the context of other runnables. (d) only relevant of top-level lock. The default Attributor executes all java code atomically, which is can be too aggressive (i.e. can cause `BlockedAtomicExceptions`).
+
+ 2. `VMListener` - a listener can explicitly request a reschedule by calling `ThreadInfo.yield()` in response of a instruction execution notification.
+
+ 3. `Verify` - a class that serves as an API to communicate between the test application and JPF, and contains `beginAtomic()`, `endAtomic()` functions to control thread interleaving
+
+The main effort of JPFs POR support relates to extending its precise mark and sweep collector. POR reachability is a subset of collector reachability, hence the mechanism piggybacks on the mark phase object traversal. It is complicated by the fact that certain reference chains exist only in the (hidden) VM implementation layer. For instance, every thread has a reference to its ThreadGroup, and the ThreadGroup objects in turn have references to all included threads, hence - from a garbage collection perspective - all threads within a group are mutually reachable. If the application under test does not use Java reflection and runtime queries like thread enumeration, POR reachability should follow accessibility rules as closely as possible. While JPF's POR does not yet support protected and private access modifiers, it includes a mechanism to specify that certain fields should not be used to promote POR reachability. This attribute is set via the configured Attributor at class load time.
+
+![Figure 2: Mark Phase of Reachability Analysis](../graphics/por-mark.svg){align=center width=460}
+
+With this mechanism, calculating POR reachability becomes a straight forward approach that is divided into two phases. Phase 1 non-recursively marks all objects of the root set (mostly static fields and thread stacks), recording the id of the referencing thread. In case an object is reachable from a static field, or from two threads, it's status is set to shared. Phase 2 recursively traverses all heap objects, propagating either a set shared status or the referencing thread id through all reference fields that are not marked as reachability firewalls. Again, if the traversal hits an object that is already marked as referenced by another thread, it promotes the object status to shared, and from there propagates the shared status instead of the thread id.
+
+To further reduce irrelevant context switches, JPF can check for lock protection to determine if a field access is scheduling relevant. If the property `vm.por.sync_detection` is set to true, JPF looks for potential lock candidates when analyzing `GET_x/SET_x` instructions. The policy of detecting lock candidates is configurable with the property `vm.por.fieldlockinfo.class`, the default `gov.nasa.jpf.jvm.StatisticFieldLockInfo` just defers the decision by recording the set of locks held when executing the field instruction, computing the set intersection at subsequent accesses. If the set does not get empty for a configurable number of field accesses, the field is marked as lock protected, and henceforth not treated as transition boundary. If however the set should afterwards become empty, a warning like
+
+~~~~~~~~ {.bash}
+Warning: unprotected field access of: Event@70.count in thread: "Thread-1" oldclassic.java:107
+   sync-detection assumed to be protected by: Event@70
+   found to be protected by: {}
+   >>> re-run with 'vm.por.sync_detection=false' or exclude field from checks <<<
+~~~~~~~~
+
+is issued, and the field access is again treated as transition breaker.
+
+The set of fields to be analyzed can be specified with the properties `vm.por.include_fields` and `vm.por.exclude_fields`. Per default, fields of system library classes are not analyzed (this is esp. useful to avoid context switches for global objects like `System.out`).
+
+Even with all these optimizations, some unwanted transition breakers are likely to remain. This is mostly due to two constraints:
+
+ * JPF only considers reachability, not accessibility
+ * write once, read multiple conditions cannot be detected a priori for fields that are not final, or inside immutable objects (like `java.lang.String`)
+
+Especially the last issue might be subject to further enhancements
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/devel/report.md	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,70 @@
+# The JPF Report API #
+The JPF report system consists of three major components: 
+
+  - the `Reporter`
+  - any number of format specific `Publisher` objects
+  - any number of tool-, property-, Publisher-specific `PublisherExtension` objects
+
+Here is the blueprint:
+
+![Figure: JPF Report System](../graphics/report.svg){align=center width=800}
+
+The `Reporter` is the data collector. It also manages and notifies `Publisher` extensions when a certain output phase is reached. The `Publishers` are the format (e.g. text, XML) specific output producers, the most prominent one being the `ConsolePublisher` (for normal, readable text output on consoles). `PublisherExtensions` can be registered for specific `Publishers` at startup time, e.g. from Listeners implementing properties or analysis modes such as `DeadlockAnalyzer`. This is so common that the `ListenerAdapter` actually implements all the required interface methods so that you just have to override the ones you are interested in.
+
+Configuration is quite easy, and involves only a handful of JPF properties that are all in the report category. The first property specifies the Reporter class itself, but is not likely to be redefined unless you have to implement different data collection modes.
+
+~~~~~~~~ {.bash}
+report.class=gov.nasa.jpf.report.Reporter
+~~~~~~~~
+
+The next setting specifies a list of Publisher instances to use, using symbolic names:
+
+~~~~~~~~ {.bash}
+report.publisher=console,xml
+~~~~~~~~
+
+Each of these symbolic names has to have a corresponding class name defined:
+
+~~~~~~~~ {.bash}
+report.console.class=gov.nasa.jpf.report.ConsolePublisher
+~~~~~~~~
+
+Finally, we have to specify for each symbolic publisher name and output phase what topics should be processed in which order, e.g.
+
+~~~~~~~~ {.bash}
+report.console.property_violation=error,trace,snapshot
+~~~~~~~~
+
+Again, the order of these topics matters, and gives you complete control over the report format. As usual, please refer to `defaults.properties` for default values.
+
+Publisher classes can have their own, additional properties. For instance, the `ConsolePublisher` implementation can be further configured with respect to the information that is included in traces (bytecodes, method names etc.), and to redirect output (file, socket). Please refer to the constructor of this class for further details.
+
+~~~~~~~~ {.bash}
+# save report to file
+report.console.file=My_JPF_report
+~~~~~~~~
+
+All of the involved core classes and interfaces reside in the `gov.nasa.jpf.report` package. The most common way to extend the system is to use your own `PublisherExtension` implementation, which involves two steps:
+
+  - implement the required phase and format specific methods
+  - register the extension for a specific Publisher class
+
+
+The `DeadlockAnalyzer` (which is a listener to analyze concurrency defects) can be used as an example of how to do this:
+
+~~~~~~~~ {.java}
+public class DeadlockAnalyzer extends ListenerAdapter {
+  ...
+  public DeadlockAnalyzer (Config config, JPF jpf){
+    jpf.addPublisherExtension(ConsolePublisher.class, this);  // (1)
+    ...
+  }
+  ...
+  public void publishPropertyViolation (Publisher publisher) { // (2)
+    PrintWriter pw = publisher.getOut();
+    publisher.publishTopicStart("thread ops " + publisher.getLastErrorId());
+    
+    ... // use 'pw' to generate the output
+  }
+}
+~~~~~~~~
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/graphics/DFSListener.svg	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,3 @@
+<?xml version="1.0" encoding="utf-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="62 54 384 228" width="32pc" height="19pc" xmlns:dc="http://purl.org/dc/elements/1.1/"><metadata> Produced by OmniGraffle 6.1 <dc:date>2005-10-21 18:50:44 +0000</dc:date></metadata><defs><filter id="Shadow" filterUnits="userSpaceOnUse"><feGaussianBlur in="SourceAlpha" result="blur" stdDeviation="1.308"/><feOffset in="blur" result="offset" dx="0" dy="2"/><feFlood flood-color="black" flood-opacity=".5" result="flood"/><feComposite in="flood" in2="offset" operator="in"/></filter><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"><g><path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Helvetica" font-size="11" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"><font-face-src><font-face-name name="Helvetica"/></font-face-src></font-face></defs><g stroke="none" stroke-opacity="1" stroke-dasharray="none" fill="none" fill-opacity="1"><title>Canvas 1</title><rect fill="white" width="588.0188" height="768.0188"/><g><title>Layer 1</title><g><xl:use xl:href="#id26_Graphic" filter="url(#Shadow)"/><xl:use xl:href="#id27_Graphic" filter="url(#Shadow)"/><xl:use xl:href="#id28_Graphic" filter="url(#Shadow)"/><xl:use xl:href="#id29_Graphic" filter="url(#Shadow)"/><xl:use xl:href="#id30_Graphic" filter="url(#Shadow)"/><xl:use xl:href="#id31_Graphic" filter="url(#Shadow)"/></g><g id="id26_Graphic"><path d="M 91.05 67 L 155.45 67 C 163.0676 67 169.25 71.704 169.25 77.5 C 169.25 83.296 163.0676 88 155.45 88 L 91.05 88 C 83.4324 88 77.25 83.296 77.25 77.5 C 77.25 71.704 83.4324 67 91.05 67" fill="white"/><path d="M 91.05 67 L 155.45 67 C 163.0676 67 169.25 71.704 169.25 77.5 C 169.25 83.296 163.0676 88 155.45 88 L 91.05 88 C 83.4324 88 77.25 83.296 77.25 77.5 C 77.25 71.704 83.4324 67 91.05 67" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g id="id27_Graphic"><path d="M 352.55 67 L 416.95 67 C 424.5676 67 430.75 71.704 430.75 77.5 C 430.75 83.296 424.5676 88 416.95 88 L 352.55 88 C 344.9324 88 338.75 83.296 338.75 77.5 C 338.75 71.704 344.9324 67 352.55 67" fill="white"/><path d="M 352.55 67 L 416.95 67 C 424.5676 67 430.75 71.704 430.75 77.5 C 430.75 83.296 424.5676 88 416.95 88 L 352.55 88 C 344.9324 88 338.75 83.296 338.75 77.5 C 338.75 71.704 344.9324 67 352.55 67" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g id="id28_Graphic"><path d="M 136.475 118 L 211.025 118 C 219.8432 118 227 122.704 227 128.5 C 227 134.296 219.8432 139 211.025 139 L 136.475 139 C 127.6568 139 120.5 134.296 120.5 128.5 C 120.5 122.704 127.6568 118 136.475 118" fill="white"/><path d="M 136.475 118 L 211.025 118 C 219.8432 118 227 122.704 227 128.5 C 227 134.296 219.8432 139 211.025 139 L 136.475 139 C 127.6568 139 120.5 134.296 120.5 128.5 C 120.5 122.704 127.6568 118 136.475 118" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g id="id29_Graphic"><path d="M 231.1125 183 L 301.6375 183 C 309.9796 183 316.75 187.704 316.75 193.5 C 316.75 199.296 309.9796 204 301.6375 204 L 231.1125 204 C 222.7704 204 216 199.296 216 193.5 C 216 187.704 222.7704 183 231.1125 183" fill="white"/><path d="M 231.1125 183 L 301.6375 183 C 309.9796 183 316.75 187.704 316.75 193.5 C 316.75 199.296 309.9796 204 301.6375 204 L 231.1125 204 C 222.7704 204 216 199.296 216 193.5 C 216 187.704 222.7704 183 231.1125 183" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g id="id30_Graphic"><path d="M 247.55 148.5 L 311.95 148.5 C 319.5676 148.5 325.75 153.204 325.75 159 C 325.75 164.796 319.5676 169.5 311.95 169.5 L 247.55 169.5 C 239.9324 169.5 233.75 164.796 233.75 159 C 233.75 153.204 239.9324 148.5 247.55 148.5" fill="white"/><path d="M 247.55 148.5 L 311.95 148.5 C 319.5676 148.5 325.75 153.204 325.75 159 C 325.75 164.796 319.5676 169.5 311.95 169.5 L 247.55 169.5 C 239.9324 169.5 233.75 164.796 233.75 159 C 233.75 153.204 239.9324 148.5 247.55 148.5" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g id="id31_Graphic"><path d="M 202.55 231 L 284.45 231 C 294.1376 231 302 235.704 302 241.5 C 302 247.296 294.1376 252 284.45 252 L 202.55 252 C 192.8624 252 185 247.296 185 241.5 C 185 235.704 192.8624 231 202.55 231" fill="white"/><path d="M 202.55 231 L 284.45 231 C 294.1376 231 302 235.704 302 241.5 C 302 247.296 294.1376 252 284.45 252 L 202.55 252 C 192.8624 252 185 247.296 185 241.5 C 185 235.704 192.8624 231 202.55 231" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><path d="M 131.82329 138.16666 C 132.88209 140.61086 134.72058 143.048855 135 145.5 C 135.27942 147.951145 134.72904 151.04185 133.5 152.875 C 132.27096 154.70815 129.874775 156.1667 127.625 156.5 C 125.375225 156.8333 121.604006 156.31236 120 154.875 C 118.395994 153.43764 117.02568 150.964375 118 147.875 C 118.33188 146.82268 119.04462 145.594735 119.94362 144.28092" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 300.2699 236.20079 C 302.39772 235.01331 304.5007 234.23864 306.654 232.638 C 308.8073 231.03736 312.13694 229.05675 313.191 226.596 C 314.24506 224.13525 314.7705 221.5729 312.979 217.872 C 312.15253 216.16467 310.59337 214.11944 308.80859 211.9702" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(89.5 71.125)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="500" x=".25927734" y="10" textLength="68.481445">searchStarted</tspan></text><text transform="translate(349.5 70.125)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="500" x=".203125" y="10" textLength="74.59375">searchFinished</tspan></text><text transform="translate(127 121.125)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="500" x="4.6135254" y="10" textLength="72.77295">stateAdvanced</tspan></text><text transform="translate(241 152.125)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="500" x=".044433594" y="10" textLength="47.68994">propertyV</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="47.541016" y="10" textLength="32.41455">iolated</tspan></text><text transform="translate(224.5 187.125)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="500" x=".31274414" y="10" textLength="84.37451">stateBacktracked</tspan></text><text transform="translate(194.5 234.125)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="500" x=".203125" y="10" textLength="96.59375">searchConstraintHit</tspan></text><path d="M 168.67215 76.98571 L 180.57215 76.98571 L 190.47357 76.98571 C 195.94198 76.98571 200.375 81.41873 200.375 86.88714 L 200.375 106.1 L 200.375 108.1" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 226.33107 127.98571 L 238.23107 127.98571 L 272.23107 127.98571 C 277.75392 127.98571 282.23107 123.50856 282.23107 117.98571 L 282.23107 87.5 C 282.23107 81.977153 286.70823 77.5 292.23107 77.5 L 326.85 77.5 L 328.85 77.5" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 200.375 139 L 200.375 150.9 L 200.375 154.54757 C 200.375 156.56207 202.00807 158.19515 204.02257 158.19515 L 221.89 158.19515 L 223.89 158.19515" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 325.17215 158.48571 L 337.07215 158.48571 L 375.7735 158.48571 C 381.29635 158.48571 385.7735 154.00856 385.7735 148.48571 L 385.7735 99.9 L 385.7735 97.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 316.11719 192.98571 L 328.01719 192.98571 L 388.22082 192.98571 C 393.74367 192.98571 398.22082 188.50856 398.22082 182.98571 L 398.22082 99.9 L 398.22082 97.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 301.26512 240.98571 L 313.16512 240.98571 L 400.5722 240.98571 C 406.09504 240.98571 410.5722 236.50856 410.5722 230.98571 L 410.5722 99.9 L 410.5722 97.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 173.23588 139 L 173.23588 150.9 L 173.23588 182.69515 C 173.23588 188.218 177.71303 192.69515 183.23588 192.69515 L 204.1438 192.69515 L 206.1438 192.69515" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 146.75778 139 L 146.75778 150.9 L 146.75778 230.69515 C 146.75778 236.218 151.23493 240.69515 156.75778 240.69515 L 173.15087 240.69515 L 175.15087 240.69515" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 242.93519 252 L 242.93519 263.9 L 242.93519 267.45 C 242.93519 269.41061 241.3458 271 239.38519 271 L 109 271 C 103.47715 271 99 266.52285 99 261 L 99 132.5183 C 99 129.854546 101.1594 127.69515 103.82315 127.69515 L 108.646305 127.69515 L 110.646305 127.69515" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 226.71194 203.16666 C 227.59954 205.40255 229.22284 207.77799 229.375 209.875 C 229.52716 211.97201 228.85404 214.12516 227.625 215.75 C 226.39596 217.37484 224.22894 219.08339 222 219.625 C 219.77106 220.16661 215.89567 220.14572 214.25 219 C 212.60433 217.85428 210.99047 215.69356 212.125 212.75 C 212.54779 211.65307 213.48253 210.31699 214.64302 208.87548" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g></g></svg>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/graphics/app-types.svg	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,3 @@
+<?xml version="1.0" encoding="utf-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="20 24 747 537" width="747pt" height="537pt" xmlns:dc="http://purl.org/dc/elements/1.1/"><metadata> Produced by OmniGraffle 6.1 <dc:date>2015-01-05 22:17:29 +0000</dc:date></metadata><defs><filter id="Shadow" filterUnits="userSpaceOnUse"><feGaussianBlur in="SourceAlpha" result="blur" stdDeviation="1.308"/><feOffset in="blur" result="offset" dx="0" dy="2"/><feFlood flood-color="black" flood-opacity=".5" result="flood"/><feComposite in="flood" in2="offset" operator="in"/></filter><filter id="Shadow_2" filterUnits="userSpaceOnUse"><feGaussianBlur in="SourceAlpha" result="blur" stdDeviation="1.308"/><feOffset in="blur" result="offset" dx="0" dy="2"/><feFlood flood-color="black" flood-opacity=".5" result="flood"/><feComposite in="flood" in2="offset" operator="in" result="color"/><feMerge><feMergeNode in="color"/><feMergeNode in="SourceGraphic"/></feMerge></filter><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="Arrow_Marker" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"><g><path d="M 8 0 L 0 -3 L 0 3 Z" fill="none" stroke="currentColor" stroke-width="1"/></g></marker><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="Arrow_Marker_2" viewBox="-9 -4 10 8" markerWidth="10" markerHeight="8" color="black"><g><path d="M -8 0 L 0 3 L 0 -3 Z" fill="none" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Helvetica" font-size="11" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="532.22656" cap-height="719.72656" ascent="770.01953" descent="-229.98047" font-weight="bold"><font-face-src><font-face-name name="Helvetica-Bold"/></font-face-src></font-face><font-face font-family="Helvetica" font-size="11" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"><font-face-src><font-face-name name="Helvetica"/></font-face-src></font-face><font-face font-family="Lucida Grande" font-size="11" panose-1="2 11 6 0 4 5 2 2 2 4" units-per-em="1000" underline-position="-97.65625" underline-thickness="48.828125" slope="0" x-height="530.27344" cap-height="722.65625" ascent="966.7969" descent="-210.9375" font-weight="500"><font-face-src><font-face-name name="LucidaGrande"/></font-face-src></font-face><font-face font-family="Helvetica" font-size="15" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="-800" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-style="italic" font-weight="500"><font-face-src><font-face-name name="Helvetica-Oblique"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" viewBox="-1 -4 8 8" markerWidth="8" markerHeight="8" color="black"><g><path d="M 5.5999994 0 L 0 -2.0999998 L 0 2.0999998 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Helvetica" font-size="10" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"><font-face-src><font-face-name name="Helvetica"/></font-face-src></font-face><font-face font-family="Times New Roman" font-size="20" panose-1="2 2 8 3 7 5 5 2 3 4" units-per-em="1000" underline-position="-108.88672" underline-thickness="95.214844" slope="0" x-height="456.54297" cap-height="662.10938" ascent="891.1133" descent="-216.3086" font-weight="bold"><font-face-src><font-face-name name="TimesNewRomanPS-BoldMT"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" viewBox="-1 -2 4 4" markerWidth="4" markerHeight="4" color="black"><g><path d="M 1.6 0 L 0 -.6 L 0 .6 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker></defs><g stroke="none" stroke-opacity="1" stroke-dasharray="none" fill="none" fill-opacity="1"><title>App Types</title><rect fill="white" width="768.0188" height="588.0188"/><g><title>Layer 1</title><g><xl:use xl:href="#id50_Graphic" filter="url(#Shadow)"/><xl:use xl:href="#id65_Graphic" filter="url(#Shadow)"/></g><g filter="url(#Shadow_2)"><path d="M 327.333 77.9986 L 474.333 77.9986 C 480.40813 77.9986 485.333 82.92347 485.333 88.9986 L 485.333 311.5916 C 485.333 317.66673 480.40813 322.5916 474.333 322.5916 L 327.333 322.5916 C 321.25787 322.5916 316.333 317.66673 316.333 311.5916 L 316.333 88.9986 C 316.333 82.92347 321.25787 77.9986 327.333 77.9986 Z" stroke="red" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/></g><g id="id50_Graphic"><path d="M 282.2563 114.6481 C 282.2563 109.43795 281.63467 108.79335 277.09383 103.6371 L 277.04586 103.58375 C 272.48103 98.3736 272.43356 98.3736 267.74881 98.3736 C 261.51097 98.3736 233.309 98.3736 233.309 98.3736 L 233.309 153.3736 L 282.2563 153.3736 L 282.2563 114.6481 Z" fill="white"/><path d="M 282.2563 114.6481 C 282.2563 109.43795 281.63467 108.79335 277.09383 103.6371 L 277.04586 103.58375 C 272.48103 98.3736 272.43356 98.3736 267.74881 98.3736 C 261.51097 98.3736 233.309 98.3736 233.309 98.3736 L 233.309 153.3736 L 282.2563 153.3736 L 282.2563 114.6481 Z M 282.2563 114.3797 C 282.2563 109.43795 282.20833 109.43795 272.43356 109.43795 L 272.43356 109.43795 C 272.43356 98.4275 272.43356 98.3736 268.03564 98.3736" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><line x1="31.2632" y1="385.317" x2="755.896" y2="385.317" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="16,9,1,9"/><line x1="300.567" y1="128.5" x2="506.433" y2="128.5" marker-end="url(#Arrow_Marker)" marker-start="url(#Arrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(118.333 406.626)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="133.21924">non-functional properties</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="110.08594"> unhandled exceptions</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="37" textLength="41.561523">     (incl. </tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="40.95996" y="37" textLength="73.95996">AssertionError)</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="51" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="51" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="51" textLength="52.58838"> deadlocks</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="65" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="65" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="65" textLength="29.95459"> races</tspan></text><text transform="translate(118.333 318.229)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="119.8291">restricted choice types</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="111.91211"> scheduling sequences</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="38" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="38" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="38" textLength="88.04297"> java.util.Random </tspan></text><text transform="translate(118.333 478.959)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="107.572266">improved inspection</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="93.5376"> coverage statistics</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="38" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="38" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="38" textLength="97.22217"> exact object counts</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="52" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="52" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="52" textLength="78.87451"> execution costs</tspan></text><text transform="translate(36.33314 309.333) rotate(-90)" fill="black"><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="15" textLength="72.53174">constraints</tspan></text><text transform="translate(38.9582 487.959) rotate(-90)" fill="black"><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="15" textLength="40.86914">benefi</tspan><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="40.86914" y="15" textLength="11.6674805">ts</tspan></text><text transform="translate(527.5 202)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="152.81836">restricted application models</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="26.280762"> UML</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="37.952148" y="24" textLength="73.981445"> statemachines</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="38" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="38" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="38" textLength="151.620605"> does not run w/o JPF libraries </tspan></text><text transform="translate(118.666 200.667)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="72.12842">runtime costs</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="130.23291"> order of magnitude slower</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="38" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="38" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="38" textLength="109.430664"> state storage memory</tspan></text><text transform="translate(118.333 244.97)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="127.13379">standard library support</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="116.77832"> java.net, javax.swing, ..</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="37" textLength="151.01367">     (needs abstraction models) </tspan></text><text transform="translate(528.197 437.293)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="158.89307">functional (domain) properties</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="120.430664"> built-in into JPF libraries</tspan></text><text transform="translate(118.666 288.728)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="160.74072">functional property impl. costs</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="123.49756"> listeners, MJI knowledge</tspan></text><text transform="translate(528.197 467.96)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="6.7192383">fl</tspan><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="6.7192383" y="10" textLength="94.166016">exible state space</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="73.36914"> domain specifi</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="85.44336" y="24" textLength="45.853027">c choices</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="37" textLength="63.572266">     (e.g. UML</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="63.169434" y="37" textLength="91.58789"> &quot;enabling events&quot;)</tspan></text><text transform="translate(528.864 511.294)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="163.80762">runtime costs &amp; library support</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="149.80518"> usually not a problem, domain</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="37" textLength="147.96289">     libs can control state space</tspan></text><text transform="translate(142 114.334)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="10" textLength="57.481445">runs on any</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="23" textLength="22">JVM</tspan></text><text transform="translate(597.018 112.38)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="10" textLength="44.63379">runs only</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="23" textLength="50.746094">under JPF</tspan></text><text transform="translate(528.197 406.626)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="102.066895">low modeling costs</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="165.08594"> statemachine w/o layout hassle,..</tspan></text><text transform="translate(527.833 247.333)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="131.40918">initial domain impl. costs</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="126.55371"> domain libs can be tricky </tspan></text><text transform="translate(408 85.8125)" fill="black"><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="0" y="11" textLength="65.5542">&quot;sweet spot&quot;</tspan></text><text transform="translate(345.41 172.334)" fill="red"><tspan font-family="Helvetica" font-size="11" font-weight="bold" fill="red" x="0" y="10" textLength="93.51074">annotate program</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="24" textLength="67.251465"> requirements</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="38" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="38" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="38" textLength="89.86914"> sequences (UML)</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="52" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="52" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="52" textLength="79.46533"> contracts (PbC)</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="66" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="66" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="66" textLength="26.286133"> tests</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="79" textLength="23.22461">    …</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="92" textLength="3.0561523"> </tspan></text><text transform="translate(345.41 259.291)" fill="red"><tspan font-family="Helvetica" font-size="11" font-weight="bold" fill="red" x="0" y="10" textLength="87.41992">analyze program</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="24" textLength="72.13379"> symbolic exec</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="38" textLength="15.280762">     </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="15.280762" y="38" textLength="11">→</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="26.280762" y="38" textLength="45.251465"> test data</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="52" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="52" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="52" textLength="105.77295"> thread safety / races </tspan></text><path d="M 443.077 271.319 C 448.50012 269.28287 455.12626 268.07605 459.348 265.21 C 463.56974 262.34395 467.8014 258.03911 468.41 254.121 C 469.0186 250.20289 466.9996 245.38813 463 241.699 C 460.3534 239.25783 455.78244 237.2113 451.19748 235.16785" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(241.566 140.124)" fill="black"><tspan font-family="Helvetica" font-size="10" font-weight="500" x="0" y="10" textLength="29.453125">*.class</tspan></text><g id="id65_Graphic"><path d="M 424.2383 117.1085 C 424.2383 111.89835 423.61667 111.25375 419.07583 106.0975 L 419.02786 106.04415 C 414.46303 100.834 414.41556 100.834 409.7308 100.834 C 403.49297 100.834 375.291 100.834 375.291 100.834 L 375.291 155.834 L 424.2383 155.834 L 424.2383 117.1085 Z" fill="white"/><path d="M 424.2383 117.1085 C 424.2383 111.89835 423.61667 111.25375 419.07583 106.0975 L 419.02786 106.04415 C 414.46303 100.834 414.41556 100.834 409.7308 100.834 C 403.49297 100.834 375.291 100.834 375.291 100.834 L 375.291 155.834 L 424.2383 155.834 L 424.2383 117.1085 Z M 424.2383 116.8401 C 424.2383 111.89835 424.19033 111.89835 414.41556 111.89835 L 414.41556 111.89835 C 414.41556 100.8879 414.41556 100.834 410.01764 100.834" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><text transform="translate(385.548 142.585)" fill="black"><tspan font-family="Helvetica" font-size="10" font-weight="500" x="0" y="10" textLength="25.014648">*.java</tspan></text><text transform="translate(381.548 115.758)" fill="blue"><tspan font-family="Times New Roman" font-size="20" font-weight="bold" fill="blue" x="0" y="18" textLength="33.046875">@V</tspan></text><path d="M 574.3423 117.1085 C 574.3423 111.89835 573.72067 111.25375 569.17983 106.0975 L 569.13186 106.04415 C 564.56703 100.834 564.51956 100.834 559.8348 100.834 C 553.59697 100.834 525.395 100.834 525.395 100.834 L 525.395 155.834 L 574.3423 155.834 L 574.3423 117.1085 Z" fill="white"/><path d="M 574.3423 117.1085 C 574.3423 111.89835 573.72067 111.25375 569.17983 106.0975 L 569.13186 106.04415 C 564.56703 100.834 564.51956 100.834 559.8348 100.834 C 553.59697 100.834 525.395 100.834 525.395 100.834 L 525.395 155.834 L 574.3423 155.834 L 574.3423 117.1085 Z M 574.3423 116.8401 C 574.3423 111.89835 574.29433 111.89835 564.51956 111.89835 L 564.51956 111.89835 C 564.51956 100.8879 564.51956 100.834 560.12164 100.834" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><ellipse cx="543.737" cy="113.0895" rx="5.3750086" ry="4.0625065" fill="yellow"/><ellipse cx="543.737" cy="113.0895" rx="5.3750086" ry="4.0625065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><ellipse cx="556.987" cy="126.2145" rx="5.3750086" ry="4.0625065" fill="red"/><ellipse cx="556.987" cy="126.2145" rx="5.3750086" ry="4.0625065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><ellipse cx="538.987" cy="135.2145" rx="5.3750086" ry="4.0625065" fill="blue"/><ellipse cx="538.987" cy="135.2145" rx="5.3750086" ry="4.0625065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 549.51266 113.920245 C 550.629 114.080814 551.84554 113.92592 552.862 114.402 C 553.87846 114.87808 555.03463 115.563874 555.612 116.777 C 555.80122 117.17458 555.9176 117.662774 555.9969 118.19702" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 559.38672 130.37215 C 560.37838 132.09026 562.65776 134.17099 562.362 135.527 C 562.06624 136.88301 560.5531 138.39227 557.612 138.509 C 555.40905 138.596435 551.6817 137.6995 548.14292 136.92421" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 538.68525 130.65814 C 538.5775 129.031255 537.41597 126.75709 538.362 125.777 C 539.30803 124.79691 542.22674 124.81438 544.362 124.777 C 545.42796 124.75834 546.5616 124.8872 547.71222 125.05311" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(535.842 142.467)" fill="black"><tspan font-family="Helvetica" font-size="10" font-weight="500" x="0" y="10" textLength="25.014648">*.java</tspan></text><text transform="translate(198.618 42.3331)" fill="black"><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="15" textLength="88.374023">JPF unaware</tspan><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="33" textLength="63.354492">programs</tspan></text><text transform="translate(354.033 33.4506)" fill="black"><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="15" textLength="84.22119">JPF enabled</tspan><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="33" textLength="63.354492">programs</tspan></text><text transform="translate(498.368 43.1018)" fill="black"><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="15" textLength="101.74072">JPF dependent</tspan><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="33" textLength="63.354492">programs</tspan></text></g></g></svg>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/graphics/attributes.svg	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,3 @@
+<?xml version="1.0" encoding="utf-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="98 7 445 412" width="445pt" height="412pt" xmlns:dc="http://purl.org/dc/elements/1.1/"><metadata> Produced by OmniGraffle 6.1 <dc:date>2011-05-16 18:21:11 +0000</dc:date></metadata><defs><filter id="Shadow" filterUnits="userSpaceOnUse"><feGaussianBlur in="SourceAlpha" result="blur" stdDeviation="1.308"/><feOffset in="blur" result="offset" dx="0" dy="2"/><feFlood flood-color="black" flood-opacity=".5" result="flood"/><feComposite in="flood" in2="offset" operator="in" result="color"/><feMerge><feMergeNode in="color"/><feMergeNode in="SourceGraphic"/></feMerge></filter><font-face font-family="Helvetica" font-size="8" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"><font-face-src><font-face-name name="Helvetica"/></font-face-src></font-face><font-face font-family="Helvetica" font-size="8" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="532.22656" cap-height="719.72656" ascent="770.01953" descent="-229.98047" font-weight="bold"><font-face-src><font-face-name name="Helvetica-Bold"/></font-face-src></font-face><filter id="Shadow_2" filterUnits="userSpaceOnUse"><feGaussianBlur in="SourceAlpha" result="blur" stdDeviation=".75079507"/><feOffset in="blur" result="offset" dx=".5" dy=".5"/><feFlood flood-color="black" flood-opacity=".5" result="flood"/><feComposite in="flood" in2="offset" operator="in" result="color"/><feMerge><feMergeNode in="color"/><feMergeNode in="SourceGraphic"/></feMerge></filter><filter id="Shadow_3" filterUnits="userSpaceOnUse"><feGaussianBlur in="SourceAlpha" result="blur" stdDeviation=".75079507"/><feOffset in="blur" result="offset" dx="1" dy="1"/><feFlood flood-color="black" flood-opacity=".5" result="flood"/><feComposite in="flood" in2="offset" operator="in" result="color"/><feMerge><feMergeNode in="color"/><feMergeNode in="SourceGraphic"/></feMerge></filter><font-face font-family="Helvetica" font-size="9" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"><font-face-src><font-face-name name="Helvetica"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" viewBox="-1 -3 7 6" markerWidth="7" markerHeight="6" color="black"><g><path d="M 4.7999992 0 L 0 -1.7999997 L 0 1.7999997 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Courier New" font-size="9" panose-1="2 7 6 9 2 2 5 2 4 4" units-per-em="1000" underline-position="-232.91016" underline-thickness="100.097656" slope="0" x-height="443.35938" cap-height="591.79688" ascent="832.51953" descent="-300.29297" font-weight="bold"><font-face-src><font-face-name name="CourierNewPS-BoldMT"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" viewBox="-1 -3 6 6" markerWidth="6" markerHeight="6" color="black"><g><path d="M 4 0 L 0 -1.5 L 0 1.5 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledBall_Marker" viewBox="-4 -3 5 6" markerWidth="5" markerHeight="6" color="black"><g><circle cx="-1.4999993" cy="0" r="1.4999987" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Courier New" font-size="10" panose-1="2 7 6 9 2 2 5 2 4 4" units-per-em="1000" underline-position="-232.91016" underline-thickness="100.097656" slope="0" x-height="443.35938" cap-height="591.79688" ascent="832.51953" descent="-300.29297" font-weight="bold"><font-face-src><font-face-name name="CourierNewPS-BoldMT"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_3" viewBox="-6 -3 7 6" markerWidth="7" markerHeight="6" color="black"><g><path d="M -4.8000002 0 L 0 1.8000001 L 0 -1.8000001 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Helvetica" font-size="11" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="-1090.9091" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-style="italic" font-weight="500"><font-face-src><font-face-name name="Helvetica-Oblique"/></font-face-src></font-face><font-face font-family="Helvetica" font-size="10" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="-1200" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-style="italic" font-weight="500"><font-face-src><font-face-name name="Helvetica-Oblique"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_4" viewBox="-1 -3 6 6" markerWidth="6" markerHeight="6" color="#404040"><g><path d="M 4 0 L 0 -1.5 L 0 1.5 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledBall_Marker_2" viewBox="-4 -3 5 6" markerWidth="5" markerHeight="6" color="#404040"><g><circle cx="-1.4999993" cy="0" r="1.4999987" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker></defs><g stroke="none" stroke-opacity="1" stroke-dasharray="none" fill="none" fill-opacity="1"><title>Canvas 1</title><rect fill="white" width="768.0188" height="588.0188"/><g><title>Layer 1</title><path d="M 129.05398 137.779 L 521.01013 137.779 C 526.53298 137.779 531.01013 142.25615 531.01013 147.779 C 531.01013 147.78732 531.01012 147.795646 531.0101 147.80397 L 530.5015 351.50493 C 530.4877 357.02776 525.99938 361.49372 520.47655 361.47993 C 520.47598 361.47993 520.4754 361.47993 520.47483 361.47992 L 319.923 360.94463 C 314.40018 360.92988 309.935 356.4408 309.94973 350.91797 C 309.94984 350.8784 309.95018 350.83881 309.95075 350.79924 L 310.80437 292.10691 C 310.88469 286.58465 306.47312 282.04286 300.95085 281.96255 C 300.923 281.96214 300.89516 281.96185 300.86732 281.96168 L 130.49925 280.90729 C 125.04834 280.87355 120.62861 276.48048 120.56189 271.02987 L 119.05473 147.9014 C 118.98713 142.37896 123.40915 137.84735 128.93158 137.77975 C 128.97238 137.77925 129.01318 137.779 129.05398 137.779 Z" fill="#fcffec"/><path d="M 129.05398 137.779 L 521.01013 137.779 C 526.53298 137.779 531.01013 142.25615 531.01013 147.779 C 531.01013 147.78732 531.01012 147.795646 531.0101 147.80397 L 530.5015 351.50493 C 530.4877 357.02776 525.99938 361.49372 520.47655 361.47993 C 520.47598 361.47993 520.4754 361.47993 520.47483 361.47992 L 319.923 360.94463 C 314.40018 360.92988 309.935 356.4408 309.94973 350.91797 C 309.94984 350.8784 309.95018 350.83881 309.95075 350.79924 L 310.80437 292.10691 C 310.88469 286.58465 306.47312 282.04286 300.95085 281.96255 C 300.923 281.96214 300.89516 281.96185 300.86732 281.96168 L 130.49925 280.90729 C 125.04834 280.87355 120.62861 276.48048 120.56189 271.02987 L 119.05473 147.9014 C 118.98713 142.37896 123.40915 137.84735 128.93158 137.77975 C 128.97238 137.77925 129.01318 137.779 129.05398 137.779 Z" stroke="#dabc2a" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><g filter="url(#Shadow)"><rect x="335.637" y="278.727" width="102.191" height="50.5717" fill="#faffc4"/><rect x="335.637" y="278.727" width="102.191" height="50.5717" stroke="#ffc189" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow)"><rect x="335.805" y="149.616" width="102.191" height="119.14" fill="#faffc4"/><rect x="335.805" y="149.616" width="102.191" height="119.14" stroke="#ffc189" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow)"><rect x="131.795" y="149.616" width="97.7571" height="95.5241" fill="#faffc4"/><rect x="131.795" y="149.616" width="97.7571" height="95.5241" stroke="#ffc189" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><path d="M 119.83489 292.59206 L 291.39527 293.14156 C 296.91809 293.15925 301.38088 297.65072 301.36319 303.17354 C 301.36314 303.18956 301.36305 303.2056 301.36292 303.22162 L 300.91446 359.19774 C 300.87032 364.707 305.2906 369.21415 310.79969 369.2772 L 430.69996 370.6495 C 436.17774 370.7122 440.58542 375.17053 440.58552 380.64867 L 440.58582 397.60582 C 440.58592 403.12867 436.10885 407.6059 430.586 407.606 C 430.58594 407.606 430.58588 407.606 430.58582 407.606 L 120.528715 407.606 C 115.03568 407.606 110.57097 403.17527 110.52901 397.6824 L 109.80315 302.6684 C 109.76096 297.14571 114.20378 292.63449 119.72647 292.5923 C 119.76261 292.59202 119.79875 292.59194 119.83489 292.59206 Z" fill="#e5ffe3"/><path d="M 119.83489 292.59206 L 291.39527 293.14156 C 296.91809 293.15925 301.38088 297.65072 301.36319 303.17354 C 301.36314 303.18956 301.36305 303.2056 301.36292 303.22162 L 300.91446 359.19774 C 300.87032 364.707 305.2906 369.21415 310.79969 369.2772 L 430.69996 370.6495 C 436.17774 370.7122 440.58542 375.17053 440.58552 380.64867 L 440.58582 397.60582 C 440.58592 403.12867 436.10885 407.6059 430.586 407.606 C 430.58594 407.606 430.58588 407.606 430.58582 407.606 L 120.528715 407.606 C 115.03568 407.606 110.57097 403.17527 110.52901 397.6824 L 109.80315 302.6684 C 109.76096 297.14571 114.20378 292.63449 119.72647 292.5923 C 119.76261 292.59202 119.79875 292.59194 119.83489 292.59206 Z" stroke="#0e9319" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><rect x="337.865" y="68.4215" width="102.191" height="60" fill="white"/><rect x="337.865" y="68.4215" width="102.191" height="60" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(342.865 68.4215)" fill="black"><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="8" textLength="77.808594">dup(), push(), pop(), ..</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="18" textLength="15.984375">------</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" fill="blue" x="0" y="28" textLength="70.253906">getOperandAttr(idx)</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" fill="blue" x="0" y="38" textLength="82.703125">setOperandAttr(idx,obj)</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" fill="blue" x="0" y="48" textLength="58.246094">getLocalAttr(idx)</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" fill="blue" x="0" y="58" textLength="70.695312">setLocalAttr(idx,obj)</tspan></text><rect x="337.865" y="28.4215" width="102.191" height="40" fill="white"/><rect x="337.865" y="28.4215" width="102.191" height="40" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(342.865 28.4215)" fill="black"><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="8" textLength="35.570312">int[] locals</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="18" textLength="58.6875">Object[] localAttr</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="28" textLength="48.476562">int[] operands</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="38" textLength="71.59375">Object[] operandAttr</tspan></text><rect x="337.865" y="18.4215" width="102.191" height="10" fill="white"/><rect x="337.865" y="18.4215" width="102.191" height="10" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(342.865 18.4215)" fill="black"><tspan font-family="Helvetica" font-size="8" font-weight="bold" x="23.415812" y="8" textLength="45.359375">StackFrame</tspan></text><rect x="133.561" y="59.0283" width="102.191" height="70" fill="white"/><rect x="133.561" y="59.0283" width="102.191" height="70" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(138.561 59.0283)" fill="black"><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="8" textLength="25.351562">getIntV</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" x="24.761719" y="8" textLength="41.792969">alue(idx), ...</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="18" textLength="24.902344">setIntV</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" x="24.3125" y="18" textLength="50.23828">alue(idx, v), ...</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="28" textLength="15.984375">------</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" fill="blue" x="0" y="38" textLength="56.460938">getFieldAttr(idx)</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" fill="blue" x="0" y="48" textLength="68.910156">setFieldAttr(idx,obj)</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" fill="blue" x="0" y="58" textLength="52.015625">getObjectAttr()</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" fill="blue" x="0" y="68" textLength="62.242188">setObjectAttr(obj)</tspan></text><rect x="133.561" y="29.0283" width="102.191" height="30" fill="white"/><rect x="133.561" y="29.0283" width="102.191" height="30" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(138.561 29.0283)" fill="black"><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="8" textLength="38.242188">int[] values</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="18" textLength="33.789062">Object[] fi</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" x="33.789062" y="18" textLength="27.121094">eldAttrs</tspan><tspan font-family="Helvetica" font-size="8" font-weight="500" x="0" y="28" textLength="59.13672">Object objectAttr</tspan></text><rect x="133.561" y="19.0283" width="102.191" height="10" fill="white"/><rect x="133.561" y="19.0283" width="102.191" height="10" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(138.561 19.0283)" fill="black"><tspan font-family="Helvetica" font-size="8" font-weight="bold" x="34.536906" y="8" textLength="23.117188">Fields</tspan></text><rect x="350.285" y="163.457" width="75.3187" height="100" fill="white"/><rect x="350.285" y="163.457" width="75.3187" height="100" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="330.498" y1="193.894" x2="425.604" y2="193.894" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="387.872" y1="153.139" x2="387.872" y2="263.946" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><g filter="url(#Shadow_2)"><rect x="353.396" y="167.278" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="353.396" y="167.278" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="390.198" y="167.048" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="390.198" y="167.048" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="353.396" y="178.857" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="353.396" y="178.857" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="390.198" y="178.627" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="390.198" y="178.627" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_2)"><rect x="353.396" y="199.952" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="353.396" y="199.952" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="390.198" y="199.722" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="390.198" y="199.722" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="353.396" y="211.531" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="353.396" y="211.531" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="390.198" y="211.301" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="390.198" y="211.301" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="353.396" y="223.11" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="353.396" y="223.11" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="390.198" y="222.88" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="390.198" y="222.88" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><text transform="translate(335.377 190.062) rotate(-90)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="9" textLength="23.009766">locals</tspan></text><text transform="translate(355.071 149.616)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="9" textLength="26.015625">values</tspan></text><text transform="translate(393.961 149.616)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="9" textLength="37.019531">attributes</tspan></text><text transform="translate(335.474 236.5) rotate(-90)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="9" textLength="37.529297">operands</tspan></text><text transform="translate(309.594 187.863)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="9" textLength="18.505371">slots</tspan></text><rect x="144.642" y="183.546" width="75.3187" height="55.3838" fill="white"/><rect x="144.642" y="183.546" width="75.3187" height="55.3838" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="182.229" y1="173.228" x2="182.229" y2="239.159" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><g filter="url(#Shadow_2)"><rect x="147.753" y="187.367" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="147.753" y="187.367" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="184.555" y="187.137" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="184.555" y="187.137" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="147.753" y="198.946" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="147.753" y="198.946" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="184.555" y="198.716" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="184.555" y="198.716" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_2)"><rect x="147.753" y="211.041" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="147.753" y="211.041" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="184.555" y="210.811" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="184.555" y="210.811" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="147.753" y="222.62" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="147.753" y="222.62" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="184.555" y="222.39" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="184.555" y="222.39" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><text transform="translate(134.303 169.705)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="9" textLength="4.5">fi</tspan><tspan font-family="Helvetica" font-size="9" font-weight="500" x="4.5" y="9" textLength="41.02295">eld-values</tspan></text><text transform="translate(188.318 169.705)" fill="black"><tspan font-family="Helvetica" font-size="9" font-weight="500" x="0" y="9" textLength="37.019531">attributes</tspan></text><line x1="234.498" y1="231.537" x2="322.887" y2="231.537" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="329.357" y1="206.886" x2="240.379" y2="206.886" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(259.457 194.858)" fill="black"><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="7" textLength="43.20703">putfield</tspan></text><path d="M 428.964 210.165 L 447.019 210.165 L 447.019 228.737 L 435.664 228.737" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(259.457 221.198)" fill="black"><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="7" textLength="43.20703">getfield</tspan></text><text transform="translate(449.973 209.928)" fill="black"><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="7" textLength="16.202637">dup</tspan><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="17" textLength="10.801758">..</tspan></text><path d="M 428.169 168.156 L 497.385 168.156 L 497.385 237.983 L 434.869 237.983" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(500.669 202.849)" fill="black"><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="7" textLength="27.004395">iload</tspan><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="17" textLength="10.801758">..</tspan></text><path d="M 429.803 200.798 L 456.803 200.798 L 456.803 180.798 L 434.503 180.798" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(458.813 182.982)" fill="black"><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="7" textLength="32.405273">istore</tspan><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="17" textLength="10.801758">..</tspan></text><g filter="url(#Shadow_3)"><rect x="353.166" y="236.151" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="353.166" y="236.151" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="389.968" y="235.921" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="389.968" y="235.921" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><rect x="350.674" y="286.352" width="75.3187" height="34.5028" fill="white"/><rect x="350.674" y="286.352" width="75.3187" height="34.5028" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><g filter="url(#Shadow_2)"><rect x="353.785" y="290.173" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="353.785" y="290.173" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="390.587" y="289.943" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="390.587" y="289.943" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="353.785" y="301.752" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="353.785" y="301.752" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="390.587" y="301.522" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="390.587" y="301.522" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><path d="M 428.734 249.545 L 489.176 249.545 L 489.176 306.698 L 434.116 306.698" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><g filter="url(#Shadow_3)"><rect x="352.936" y="248.531" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="352.936" y="248.531" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><g filter="url(#Shadow_3)"><rect x="389.738" y="248.301" width="31.437" height="7.22235" fill="#e6e6e6"/><rect x="389.738" y="248.301" width="31.437" height="7.22235" stroke="#646464" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><text transform="translate(454.692 309.299)" fill="black"><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="7" textLength="70.211426">invokevirtual</tspan><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="17" textLength="10.801758">..</tspan></text><path d="M 428.603 291.278 L 446.659 291.278 L 446.659 259.189 L 434.503 259.189" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(448.227 265.618)" fill="black"><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="7" textLength="32.405273">return</tspan><tspan font-family="Courier New" font-size="9" font-weight="bold" x="0" y="17" textLength="10.801758">..</tspan></text><g filter="url(#Shadow)"><rect x="214.377" y="301.379" width="54" height="34" fill="white"/><rect x="214.377" y="301.379" width="54" height="34" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(219.377 308.379)" fill="black"><tspan font-family="Helvetica" font-size="8" font-weight="bold" x="6" y="8" textLength="32">attribute</tspan><tspan font-family="Helvetica" font-size="8" font-weight="bold" x="10.220703" y="18" textLength="23.558594">object</tspan></text></g><path d="M 199.193 249.815 L 199.193 318.925 L 207.97754 318.8113" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 406.74574 294.90896 L 406.242 315.583 L 272.50995 315.01889" marker-end="url(#FilledArrow_Marker_2)" marker-start="url(#FilledBall_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(118.282 316.108)" fill="blue"><tspan font-family="Courier New" font-size="10" font-weight="bold" fill="blue" x="0" y="8" textLength="72.01172">setAttr(i,o)</tspan></text><text transform=&