Initial import
authorNastaran Shafiei <nastaran.shafiei@nasa.gov>
Wed, 31 May 2017 00:46:11 +0000 (17:46 -0700)
committerNastaran Shafiei <nastaran.shafiei@nasa.gov>
Wed, 31 May 2017 00:46:11 +0000 (17:46 -0700)
1239 files changed:
.classpath [new file with mode: 0644]
.gitignore [new file with mode: 0644]
.idea/.name [new file with mode: 0644]
.idea/annotations.iml [new file with mode: 0644]
.idea/artifacts/RunJPF.xml [new file with mode: 0644]
.idea/artifacts/jpf.xml [new file with mode: 0644]
.idea/artifacts/jpf_annotations.xml [new file with mode: 0644]
.idea/artifacts/jpf_classes.xml [new file with mode: 0644]
.idea/classes.iml [new file with mode: 0644]
.idea/codeStyleSettings.xml [new file with mode: 0644]
.idea/compiler.xml [new file with mode: 0644]
.idea/copyright/profiles_settings.xml [new file with mode: 0644]
.idea/encodings.xml [new file with mode: 0644]
.idea/examples.iml [new file with mode: 0644]
.idea/main.iml [new file with mode: 0644]
.idea/misc.xml [new file with mode: 0644]
.idea/modules.xml [new file with mode: 0644]
.idea/peers.iml [new file with mode: 0644]
.idea/runConfigurations/run_example_jpf.xml [new file with mode: 0644]
.idea/runConfigurations/run_test.xml [new file with mode: 0644]
.idea/scopes/scope_settings.xml [new file with mode: 0644]
.idea/tests.iml [new file with mode: 0644]
.idea/vcs.xml [new file with mode: 0644]
.project [new file with mode: 0644]
LICENSE-2.0.txt [new file with mode: 0644]
META-INF/RunJPF/MANIFEST.MF [new file with mode: 0644]
README [new file with mode: 0644]
bin/javajpf [new file with mode: 0755]
bin/jpf [new file with mode: 0755]
bin/jpf.bat [new file with mode: 0755]
bin/print_class [new file with mode: 0755]
bin/print_class.bat [new file with mode: 0755]
bin/print_events [new file with mode: 0755]
bin/test [new file with mode: 0755]
bin/test.bat [new file with mode: 0755]
build.properties [new file with mode: 0644]
build.xml [new file with mode: 0644]
doc/devel/attributes.md [new file with mode: 0644]
doc/devel/bytecode_factory.md [new file with mode: 0644]
doc/devel/choicegenerator.md [new file with mode: 0644]
doc/devel/coding_conventions.md [new file with mode: 0644]
doc/devel/create_project.md [new file with mode: 0644]
doc/devel/design.md [new file with mode: 0644]
doc/devel/eclipse_plugin_update.md [new file with mode: 0644]
doc/devel/embedded.md [new file with mode: 0644]
doc/devel/index.md [new file with mode: 0644]
doc/devel/jpf_tests.md [new file with mode: 0644]
doc/devel/listener.md [new file with mode: 0644]
doc/devel/logging.md [new file with mode: 0644]
doc/devel/mercurial.md [new file with mode: 0644]
doc/devel/mji.md [new file with mode: 0644]
doc/devel/mji/mangling.md [new file with mode: 0644]
doc/devel/modules.md [new file with mode: 0644]
doc/devel/partial_order_reduction.md [new file with mode: 0644]
doc/devel/report.md [new file with mode: 0644]
doc/graphics/DFSListener.svg [new file with mode: 0644]
doc/graphics/app-types.svg [new file with mode: 0644]
doc/graphics/attributes.svg [new file with mode: 0644]
doc/graphics/bc-factory.svg [new file with mode: 0644]
doc/graphics/cg-impl.svg [new file with mode: 0644]
doc/graphics/cg-motivation.svg [new file with mode: 0644]
doc/graphics/cg-ontology.svg [new file with mode: 0644]
doc/graphics/cg-sequence.svg [new file with mode: 0644]
doc/graphics/choicegen-example.svg [new file with mode: 0644]
doc/graphics/genpeer.svg [new file with mode: 0644]
doc/graphics/interleavings.svg [new file with mode: 0644]
doc/graphics/jpf-abstractions.svg [new file with mode: 0644]
doc/graphics/jpf-basic.svg [new file with mode: 0644]
doc/graphics/jpf-intro-new.svg [new file with mode: 0644]
doc/graphics/jpf-layers.svg [new file with mode: 0644]
doc/graphics/jpf-project.svg [new file with mode: 0644]
doc/graphics/listener-overview.svg [new file with mode: 0644]
doc/graphics/listeners.svg [new file with mode: 0644]
doc/graphics/mji-call.svg [new file with mode: 0644]
doc/graphics/mji-functions.svg [new file with mode: 0644]
doc/graphics/mji-mangling.svg [new file with mode: 0644]
doc/graphics/new-testing.svg [new file with mode: 0644]
doc/graphics/por-mark.svg [new file with mode: 0644]
doc/graphics/por-scheduling-relevance.svg [new file with mode: 0644]
doc/graphics/properties.svg [new file with mode: 0644]
doc/graphics/report.svg [new file with mode: 0644]
doc/graphics/states-mc.svg [new file with mode: 0644]
doc/graphics/states-testing.svg [new file with mode: 0644]
doc/graphics/sw-model-checking-2.svg [new file with mode: 0644]
doc/graphics/sw-model-checking.svg [new file with mode: 0644]
doc/index.md [new file with mode: 0644]
doc/install/build.md [new file with mode: 0644]
doc/install/eclipse-jpf.md [new file with mode: 0644]
doc/install/eclipse-plugin.md [new file with mode: 0644]
doc/install/eclipse-plugin/update.md [new file with mode: 0644]
doc/install/eclipse-plugin/update/features.md [new file with mode: 0644]
doc/install/eclipse-plugin/update/plugins.md [new file with mode: 0644]
doc/install/index.md [new file with mode: 0644]
doc/install/netbeans-jpf.md [new file with mode: 0644]
doc/install/netbeans-plugin.md [new file with mode: 0644]
doc/install/repo_shell.md [new file with mode: 0644]
doc/install/repositories.md [new file with mode: 0644]
doc/install/requirements.md [new file with mode: 0644]
doc/install/site-properties.md [new file with mode: 0644]
doc/install/snapshot.md [new file with mode: 0644]
doc/intro/classification.md [new file with mode: 0644]
doc/intro/index.md [new file with mode: 0644]
doc/intro/race_example.md [new file with mode: 0644]
doc/intro/random_example.md [new file with mode: 0644]
doc/intro/testing_vs_model_checking.md [new file with mode: 0644]
doc/intro/what_is_jpf.md [new file with mode: 0644]
doc/jpf-core/AssertionProperty.md [new file with mode: 0644]
doc/jpf-core/ErrorTraceGenerator.md [new file with mode: 0644]
doc/jpf-core/ExceptionInjector.md [new file with mode: 0644]
doc/jpf-core/IdleFilter.md [new file with mode: 0644]
doc/jpf-core/index.md [new file with mode: 0644]
doc/papers/chicago-author-date.csl [new file with mode: 0644]
doc/papers/index.md [new file with mode: 0644]
doc/papers/references.bib [new file with mode: 0644]
doc/user/api.md [new file with mode: 0644]
doc/user/application_types.md [new file with mode: 0644]
doc/user/components.md [new file with mode: 0644]
doc/user/config.md [new file with mode: 0644]
doc/user/config/random.md [new file with mode: 0644]
doc/user/index.md [new file with mode: 0644]
doc/user/output.md [new file with mode: 0644]
doc/user/run.md [new file with mode: 0644]
doc/user/run_eclipse.md [new file with mode: 0644]
doc/user/run_eclipse_plugin.md [new file with mode: 0644]
doc/user/run_nb.md [new file with mode: 0644]
doc/user/run_nb_plugin.md [new file with mode: 0644]
eclipse/AntBuilder.launch [new file with mode: 0644]
eclipse/run-JPF.launch [new file with mode: 0644]
eclipse/test-JPF.launch [new file with mode: 0644]
eclipse/update-JPF-siteproperties.launch [new file with mode: 0644]
jpf.properties [new file with mode: 0644]
nbproject/ide-file-targets.xml [new file with mode: 0644]
nbproject/project.xml [new file with mode: 0644]
src/annotations/gov/nasa/jpf/annotation/FilterField.java [new file with mode: 0644]
src/annotations/gov/nasa/jpf/annotation/FilterFrame.java [new file with mode: 0644]
src/annotations/gov/nasa/jpf/annotation/JPFAttribute.java [new file with mode: 0644]
src/annotations/gov/nasa/jpf/annotation/JPFConfig.java [new file with mode: 0644]
src/annotations/gov/nasa/jpf/annotation/JPFOption.java [new file with mode: 0644]
src/annotations/gov/nasa/jpf/annotation/JPFOptions.java [new file with mode: 0644]
src/annotations/gov/nasa/jpf/annotation/MJI.java [new file with mode: 0644]
src/annotations/gov/nasa/jpf/annotation/NeverBreak.java [new file with mode: 0644]
src/annotations/gov/nasa/jpf/annotation/NoJPFExecution.java [new file with mode: 0644]
src/annotations/gov/nasa/jpf/annotation/NonShared.java [new file with mode: 0644]
src/classes/gov/nasa/jpf/AnnotationProxyBase.java [new file with mode: 0644]
src/classes/gov/nasa/jpf/BoxObjectCaches.java [new file with mode: 0644]
src/classes/gov/nasa/jpf/CachedROHttpConnection.java [new file with mode: 0644]
src/classes/gov/nasa/jpf/ConsoleOutputStream.java [new file with mode: 0644]
src/classes/gov/nasa/jpf/EventProducer.java [new file with mode: 0644]
src/classes/gov/nasa/jpf/FinalizerThread.java [new file with mode: 0644]
src/classes/gov/nasa/jpf/SerializationConstructor.java [new file with mode: 0644]
src/classes/java/io/File.java [new file with mode: 0644]
src/classes/java/io/FileDescriptor.java [new file with mode: 0644]
src/classes/java/io/FileInputStream.java [new file with mode: 0644]
src/classes/java/io/FileOutputStream.java [new file with mode: 0644]
src/classes/java/io/InputStreamReader.java [new file with mode: 0644]
src/classes/java/io/OutputStreamWriter.java [new file with mode: 0644]
src/classes/java/io/RandomAccessFile.java [new file with mode: 0644]
src/classes/java/lang/Class.java [new file with mode: 0644]
src/classes/java/lang/ClassLoader.java [new file with mode: 0644]
src/classes/java/lang/InheritableThreadLocal.java [new file with mode: 0644]
src/classes/java/lang/Object.java [new file with mode: 0644]
src/classes/java/lang/StackTraceElement.java [new file with mode: 0644]
src/classes/java/lang/String.java [new file with mode: 0644]
src/classes/java/lang/System.java [new file with mode: 0644]
src/classes/java/lang/Thread.java [new file with mode: 0644]
src/classes/java/lang/ThreadGroup.java [new file with mode: 0644]
src/classes/java/lang/ThreadLocal.java [new file with mode: 0644]
src/classes/java/lang/Throwable.java [new file with mode: 0644]
src/classes/java/lang/annotation/Inherited.java [new file with mode: 0644]
src/classes/java/lang/annotation/Retention.java [new file with mode: 0644]
src/classes/java/lang/ref/Reference.java [new file with mode: 0644]
src/classes/java/lang/ref/ReferenceQueue.java [new file with mode: 0644]
src/classes/java/lang/ref/WeakReference.java [new file with mode: 0644]
src/classes/java/lang/reflect/AccessibleObject.java [new file with mode: 0644]
src/classes/java/lang/reflect/Constructor.java [new file with mode: 0644]
src/classes/java/lang/reflect/Field.java [new file with mode: 0644]
src/classes/java/lang/reflect/InvocationTargetException.java [new file with mode: 0644]
src/classes/java/lang/reflect/Method.java [new file with mode: 0644]
src/classes/java/net/URLClassLoader.java [new file with mode: 0644]
src/classes/java/nio/Buffer.java [new file with mode: 0644]
src/classes/java/nio/BufferUnderflowException.java [new file with mode: 0644]
src/classes/java/nio/ByteBuffer.java [new file with mode: 0644]
src/classes/java/nio/ByteOrder.java [new file with mode: 0644]
src/classes/java/nio/channels/FileChannel.java [new file with mode: 0644]
src/classes/java/nio/package-info.java [new file with mode: 0644]
src/classes/java/security/AccessController.java [new file with mode: 0644]
src/classes/java/security/MessageDigest.java [new file with mode: 0644]
src/classes/java/security/SecureClassLoader.java [new file with mode: 0644]
src/classes/java/text/DecimalFormat.java [new file with mode: 0644]
src/classes/java/text/Format.java [new file with mode: 0644]
src/classes/java/text/NumberFormat.java [new file with mode: 0644]
src/classes/java/text/SimpleDateFormat.java [new file with mode: 0644]
src/classes/java/util/Random.java [new file with mode: 0644]
src/classes/java/util/TimeZone.java [new file with mode: 0644]
src/classes/java/util/concurrent/BrokenBarrierException.java [new file with mode: 0644]
src/classes/java/util/concurrent/CyclicBarrier.java [new file with mode: 0644]
src/classes/java/util/concurrent/Exchanger.java [new file with mode: 0644]
src/classes/java/util/concurrent/atomic/AtomicIntegerArray.java [new file with mode: 0644]
src/classes/java/util/concurrent/atomic/AtomicIntegerFieldUpdater.java [new file with mode: 0644]
src/classes/java/util/concurrent/atomic/AtomicLongArray.java [new file with mode: 0644]
src/classes/java/util/concurrent/atomic/AtomicLongFieldUpdater.java [new file with mode: 0644]
src/classes/java/util/concurrent/atomic/AtomicReferenceArray.java [new file with mode: 0644]
src/classes/java/util/concurrent/atomic/AtomicReferenceFieldUpdater.java [new file with mode: 0644]
src/classes/java/util/function/Supplier.java [new file with mode: 0644]
src/classes/java/util/logging/FileHandler.java [new file with mode: 0644]
src/classes/java/util/regex/Matcher.java [new file with mode: 0644]
src/classes/java/util/regex/Pattern.java [new file with mode: 0644]
src/classes/org/junit/After.java [new file with mode: 0644]
src/classes/org/junit/AfterClass.java [new file with mode: 0644]
src/classes/org/junit/Before.java [new file with mode: 0644]
src/classes/org/junit/BeforeClass.java [new file with mode: 0644]
src/classes/org/junit/Ignore.java [new file with mode: 0644]
src/classes/org/junit/Test.java [new file with mode: 0644]
src/classes/sun/misc/AtomicLong.java [new file with mode: 0644]
src/classes/sun/misc/JavaAWTAccess.java [new file with mode: 0644]
src/classes/sun/misc/JavaIOAccess.java [new file with mode: 0644]
src/classes/sun/misc/JavaIODeleteOnExitAccess.java [new file with mode: 0644]
src/classes/sun/misc/JavaIOFileDescriptorAccess.java [new file with mode: 0644]
src/classes/sun/misc/JavaLangAccess.java [new file with mode: 0644]
src/classes/sun/misc/JavaNetAccess.java [new file with mode: 0644]
src/classes/sun/misc/JavaNioAccess.java [new file with mode: 0644]
src/classes/sun/misc/SharedSecrets.java [new file with mode: 0644]
src/classes/sun/misc/Unsafe.java [new file with mode: 0644]
src/classes/sun/net/www/protocol/http/Handler.java [new file with mode: 0644]
src/classes/sun/nio/ch/Interruptible.java [new file with mode: 0644]
src/classes/sun/reflect/ConstantPool.java [new file with mode: 0644]
src/classes/sun/reflect/annotation/AnnotationType.java [new file with mode: 0644]
src/examples/BoundedBuffer.java [new file with mode: 0644]
src/examples/BoundedBuffer.jpf [new file with mode: 0644]
src/examples/Crossing.java [new file with mode: 0644]
src/examples/Crossing.jpf [new file with mode: 0644]
src/examples/DiningPhil.java [new file with mode: 0644]
src/examples/DiningPhil.jpf [new file with mode: 0644]
src/examples/HelloWorld.java [new file with mode: 0644]
src/examples/HelloWorld.jpf [new file with mode: 0644]
src/examples/NumericValueCheck.java [new file with mode: 0644]
src/examples/NumericValueCheck.jpf [new file with mode: 0644]
src/examples/Racer.java [new file with mode: 0644]
src/examples/Racer.jpf [new file with mode: 0644]
src/examples/Rand.java [new file with mode: 0644]
src/examples/Rand.jpf [new file with mode: 0644]
src/examples/RobotManager-replay-nt.jpf [new file with mode: 0644]
src/examples/RobotManager-replay-ot.jpf [new file with mode: 0644]
src/examples/RobotManager.java [new file with mode: 0644]
src/examples/RobotManager.jpf [new file with mode: 0644]
src/examples/StopWatch.java [new file with mode: 0644]
src/examples/StopWatch.jpf [new file with mode: 0644]
src/examples/TestExample-coverage.jpf [new file with mode: 0644]
src/examples/TestExample.java [new file with mode: 0644]
src/examples/oldclassic-da.jpf [new file with mode: 0644]
src/examples/oldclassic.java [new file with mode: 0644]
src/examples/oldclassic.jpf [new file with mode: 0644]
src/main/gov/nasa/jpf/$coreTag.java [new file with mode: 0644]
src/main/gov/nasa/jpf/Config.java [new file with mode: 0644]
src/main/gov/nasa/jpf/ConfigChangeListener.java [new file with mode: 0644]
src/main/gov/nasa/jpf/Error.java [new file with mode: 0644]
src/main/gov/nasa/jpf/GenericProperty.java [new file with mode: 0644]
src/main/gov/nasa/jpf/JPF.java [new file with mode: 0644]
src/main/gov/nasa/jpf/JPFClassLoader.java [new file with mode: 0644]
src/main/gov/nasa/jpf/JPFConfigException.java [new file with mode: 0644]
src/main/gov/nasa/jpf/JPFErrorException.java [new file with mode: 0644]
src/main/gov/nasa/jpf/JPFException.java [new file with mode: 0644]
src/main/gov/nasa/jpf/JPFListener.java [new file with mode: 0644]
src/main/gov/nasa/jpf/JPFListenerException.java [new file with mode: 0644]
src/main/gov/nasa/jpf/JPFNativePeerException.java [new file with mode: 0644]
src/main/gov/nasa/jpf/JPFShell.java [new file with mode: 0644]
src/main/gov/nasa/jpf/ListenerAdapter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/Property.java [new file with mode: 0644]
src/main/gov/nasa/jpf/PropertyListenerAdapter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/State.java [new file with mode: 0644]
src/main/gov/nasa/jpf/StateExtension.java [new file with mode: 0644]
src/main/gov/nasa/jpf/SystemAttribute.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/ClassFile.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/ClassFilePrinter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/ClassFileReader.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/ClassFileReaderAdapter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/DirClassFileContainer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMAnnotationParser.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMByteCodePrinter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMByteCodeReader.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMByteCodeReaderAdapter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMClassFileContainer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMClassInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMCodeBuilder.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMDirectCallStackFrame.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMInstructionFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMNativeStackFrame.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMStackFrame.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JVMSystemClassLoaderInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/JarClassFileContainer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/AALOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/AASTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ACONST_NULL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ALOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ANEWARRAY.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ARETURN.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ARRAYLENGTH.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ASTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ATHROW.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/BALOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/BASTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/BIPUSH.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/CALOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/CASTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/D2F.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/D2I.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/D2L.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DADD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DALOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DASTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DCMPG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DCMPL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DCONST.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DDIV.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DIRECTCALLRETURN.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DLOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DMUL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DNEG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DREM.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DRETURN.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DSTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DSUB.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DUP.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DUP2.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DUP2_X1.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DUP2_X2.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DUP_X1.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DUP_X2.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/DoubleCompareInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/EXECUTENATIVE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/F2D.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/F2I.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/F2L.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FADD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FALOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FASTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FCMPG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FCMPL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FCONST.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FDIV.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FINISHCLINIT.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FLOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FMUL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FNEG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FREM.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FRETURN.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FSTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/FSUB.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/GETFIELD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/GETSTATIC.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/GOTO.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/GOTO_W.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/GetHelper.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/I2B.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/I2C.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/I2D.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/I2F.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/I2L.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/I2S.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IADD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IALOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IAND.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IASTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ICONST.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IDIV.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IFEQ.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IFGE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IFGT.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IFLE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IFLT.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IFNE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IFNONNULL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IFNULL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IF_ACMPEQ.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IF_ACMPNE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPEQ.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPGE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPGT.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPLE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPLT.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IF_ICMPNE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IINC.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ILOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IMUL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/INEG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/INSTANCEOF.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/INVOKECG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/INVOKECLINIT.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/INVOKEINTERFACE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/INVOKEVIRTUAL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IOR.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IREM.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IRETURN.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ISHL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ISHR.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ISTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/ISUB.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IUSHR.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IXOR.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/IfInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/InstanceInvocation.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/InstructionFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JSR.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JSR_W.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JVMArrayElementInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JVMFieldInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JVMInstanceFieldInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JVMInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JVMInstructionVisitor.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JVMInstructionVisitorAdapter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JVMInvokeInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JVMLocalVariableInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JVMReturnInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/JVMStaticFieldInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/L2D.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/L2F.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/L2I.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LADD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LALOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LAND.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LASTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LCMP.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LCONST.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LDC.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LDC2_W.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LDC_W.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LDIV.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LLOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LMUL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LNEG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LOOKUPSWITCH.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LOR.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LREM.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LRETURN.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LSHL.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LSHR.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LSTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LSUB.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LUSHR.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LXOR.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LockInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LongArrayLoadInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LongArrayStoreInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/LongReturn.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/MONITORENTER.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/MONITOREXIT.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/MULTIANEWARRAY.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/NATIVERETURN.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/NEW.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/NEWARRAY.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/NOP.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/NewArrayInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/POP.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/POP2.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/PUTFIELD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/PUTSTATIC.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/PutHelper.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/RET.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/RETURN.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/RUNSTART.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/SALOAD.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/SASTORE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/SIPUSH.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/SWAP.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/StaticFieldInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/SwitchInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/TABLESWITCH.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java [new file with mode: 0644]
src/main/gov/nasa/jpf/jvm/bytecode/WIDE.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/AssertionProperty.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/BudgetChecker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/CGMonitor.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/CGRemover.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/CallMonitor.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/ChoiceSelector.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/ChoiceTracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/CoverageAnalyzer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/DeadlockAnalyzer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/DistributedSimpleDot.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/EndlessLoopDetector.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/ErrorTraceGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/ExceptionInjector.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/ExecTracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/HeapTracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/IdleFilter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/InsnCounter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/LockedStackDepth.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/LogConsole.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/MethodAnalyzer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/MethodTracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/NoStateCycles.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/NonSharedChecker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/NullTracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/NumericValueChecker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/OOMEInjector.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/ObjectTracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/OverlappingMethodAnalyzer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/PathOutputMonitor.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/Perturbator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/PreciseRaceDetector.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/ReferenceLocator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/SearchStats.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/SimpleDot.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/SimpleIdleFilter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/StackDepthChecker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/StackTracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/StateCountEstimator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/StateSpaceAnalyzer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/StateSpaceDot.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/StateTracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/StopWatchFuzzer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/TraceStorer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/VarRecorder.java [new file with mode: 0644]
src/main/gov/nasa/jpf/listener/VarTracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/perturb/GenericDataAbstractor.java [new file with mode: 0644]
src/main/gov/nasa/jpf/perturb/IntOverUnder.java [new file with mode: 0644]
src/main/gov/nasa/jpf/perturb/OperandPerturbator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/report/ConsolePublisher.java [new file with mode: 0644]
src/main/gov/nasa/jpf/report/Publisher.java [new file with mode: 0644]
src/main/gov/nasa/jpf/report/PublisherExtension.java [new file with mode: 0644]
src/main/gov/nasa/jpf/report/PublisherExtensionAdapter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/report/Reporter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/report/Statistics.java [new file with mode: 0644]
src/main/gov/nasa/jpf/report/XMLPublisher.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/DFSearch.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/PathSearch.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/RandomSearch.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/Search.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/SearchListener.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/SearchListenerAdapter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/SearchState.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/Simulation.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/BFSHeuristic.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/DFSHeuristic.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/GlobalSwitchThread.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/HeuristicSearch.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/HeuristicState.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/Interleaving.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/MinimizePreemption.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/MostBlocked.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/PreferThreads.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/PrioritizedState.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/RandomHeuristic.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/SimplePriorityHeuristic.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/StaticPriorityQueue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/search/heuristic/UserHeuristic.java [new file with mode: 0644]
src/main/gov/nasa/jpf/tool/GenPeer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/tool/LogConsole.java [new file with mode: 0644]
src/main/gov/nasa/jpf/tool/PrintEvents.java [new file with mode: 0644]
src/main/gov/nasa/jpf/tool/Run.java [new file with mode: 0644]
src/main/gov/nasa/jpf/tool/RunJPF.java [new file with mode: 0644]
src/main/gov/nasa/jpf/tool/RunTest.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ArrayByteQueue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ArrayIntSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ArrayObjectQueue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Attributable.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/AvailableBufferedInputStream.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/BailOut.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/BinaryClassSource.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/BitArray.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/BitSet1024.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/BitSet256.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/BitSet64.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/BitSetN.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ClassInfoFilter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/CloneableObject.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Cloner.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/CommitOutputStream.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ConsoleStream.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ConstGrowth.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/CountDown.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/DevNullPrintStream.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/DynamicIntArray.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/DynamicObjectArray.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ElementCreator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ExpGrowth.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/FeatureSpec.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/FieldSpec.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/FieldSpecMatcher.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/FileUtils.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/FinalBitSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/FixedBitSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Growth.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/HashData.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/HashPool.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/IdentityArrayObjectSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/IdentityObjectSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ImmutableList.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/IndexIterator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/InstructionState.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/IntArray.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/IntIterator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/IntSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/IntTable.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/IntVector.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Invocation.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/JPFLogger.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/JPFSiteUtils.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Left.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/LimitedInputStream.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/LinkedObjectQueue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/LocationSpec.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/LogHandler.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/LogManager.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Loggable.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/LongVector.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/MethodInfoRegistry.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/MethodSpec.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/MethodSpecMatcher.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Misc.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/MutableInteger.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/MutableIntegerRestorer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/OATHash.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ObjArray.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ObjVector.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ObjectConverter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ObjectList.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ObjectQueue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ObjectSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/PSIntMap.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Pair.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/PairPermutationGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/PathnameExpander.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/PermutationGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Predicate.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/PrintStreamable.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/PrintUtils.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Printable.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Processor.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/RandomPermutationGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/ReadOnlyObjList.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Reflection.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/RepositoryEntry.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Result.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Right.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/RunListener.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/RunRegistry.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/SimplePool.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/SingleElementList.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/SortedArrayIntSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/SortedArrayObjectSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Source.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/SourceRef.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/SparseClusterArray.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/SparseIntVector.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/SparseObjVector.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/SplitInputStream.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/SplitOutputStream.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/StateExtensionClient.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/StateExtensionListener.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/StringExpander.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/StringMatcher.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/StringSetMatcher.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/StructuredPrinter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/TotalPermutationGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Trace.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/TraceElement.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/Transformer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/TwoTypeComparator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/TypeRef.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/TypeSpec.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/TypeSpecMatcher.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/UniqueRandomPermGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/UnsortedArrayIntSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/VarSpec.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/WeakPool.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/automaton/Automaton.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/automaton/State.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/automaton/Transition.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/CheckEvent.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/ControlEvent.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/Event.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/EventChoiceGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/EventConstructor.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/EventContext.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/EventForest.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/EventTree.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/NoEvent.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/PropagatingEventContext.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/SystemEvent.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/event/TestEventTree.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/AbstractValue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/ArrayValue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/BooleanValue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/CGCall.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/CGCreator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/CGCreatorFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/Creator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/CreatorsFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/DoubleValue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/JSONLexer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/JSONObject.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/JSONObjectValue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/JSONParser.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/NullValue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/StringValue.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/Token.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/json/Value.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/Alternative.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/ESParser.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/ElementProcessor.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/Event.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/EventFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/EventGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/EventGeneratorFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/Repetition.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/Script.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/ScriptElement.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/ScriptElementContainer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/ScriptEnvironment.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/Section.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/SequenceInterpreter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/script/StringSetGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/test/JPF_gov_nasa_jpf_util_test_TestJPF.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/test/JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/test/TestJPF.java [new file with mode: 0644]
src/main/gov/nasa/jpf/util/test/TestMultiProcessJPF.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/AbstractRestorer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/AbstractSerializer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/AbstractTypeAnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/AllRunnablesSyncPolicy.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Allocation.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/AllocationContext.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/AnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/AnnotationParser.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ApplicationContext.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ArrayAccess.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ArrayFields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ArrayIndexOutOfBoundsExecutiveException.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ArrayOffset.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/AtomicData.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Attributor.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Backtracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/BooleanArrayFields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/BooleanChoiceGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/BooleanFieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/BootstrapMethodInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/BoxObjectCacheManager.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ByteArrayFields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ByteFieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/BytecodeAnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/BytecodeTypeParameterAnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/CharArrayFields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/CharFieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/CheckExtendTransition.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ChoiceGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ChoiceGeneratorBase.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ChoicePoint.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ClassChangeException.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ClassFileContainer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ClassFileMatch.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ClassInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ClassInfoException.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ClassLoaderInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ClassLoaderList.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ClassParseException.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ClassPath.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ClinitRequired.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ClosedMemento.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/CollapsePools.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ConstInsnPathTime.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DebugJenkinsStateSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DebugStateSerializer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DefaultBacktracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DefaultFieldsFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DefaultMementoRestorer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DelegatingScheduler.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DirectCallStackFrame.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DoubleArrayFields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DoubleChoiceGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DoubleFieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DoubleSlotFieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/DynamicElementInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ElementInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ExceptionHandler.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ExceptionInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ExceptionParameterAnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/FieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/FieldLockInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/FieldLockInfoFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Fields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/FieldsFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/FinalizerThreadInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/FloatArrayFields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/FloatChoiceGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/FloatFieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/FormalParameterAnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/FullStateSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/FunctionObjectFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/GenericHeap.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/GenericSGOIDHeap.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/GenericSharednessPolicy.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/GenericSignatureHolder.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/GlobalSchedulingPoint.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/GlobalSharednessPolicy.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/HandlerContext.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/HashedAllocationContext.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Heap.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/IncrementalChangeTracker.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/InfoObject.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Instruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/IntArrayFields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/IntChoiceGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/IntegerFieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/IsEndStateProperty.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/JPFOutputStream.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/JenkinsStateSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/KernelState.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/LoadOnJPFRequired.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/LocalVarInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/LockSetThresholdFli.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/LongArrayFields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/LongChoiceGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/LongFieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/MJIEnv.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Memento.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/MementoFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/MementoRestorer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/MethodInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/MethodLocator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Monitor.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/MultiProcessVM.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/NamedFields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/NativeMethodInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/NativePeer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/NativeStackFrame.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/NativeStateHolder.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/NoJPFExec.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/NoOutOfMemoryErrorProperty.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/NoUncaughtExceptionsProperty.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/NotDeadlockedProperty.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/OVHeap.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/OVStatics.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ObjRef.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/PSIMHeap.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Path.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/PathSharednessPolicy.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/PersistentLockSetThresholdFli.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/PersistentSingleLockThresholdFli.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/PersistentTidSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/PreciseAllocationContext.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/PredicateMap.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/PriorityRunnablesSyncPolicy.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ReferenceArrayFields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ReferenceChoiceGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ReferenceFieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ReferenceProcessor.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ReleaseAction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Restorable.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/RestorableVMState.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Scheduler.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/SerializingStateSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/SharednessPolicy.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ShortArrayFields.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ShortFieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/SingleLockThresholdFli.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/SingleProcessVM.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/SingleSlotFieldInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/StackFrame.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/StateRestorer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/StateSerializer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/StateSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/StaticElementInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Statics.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/StatisticFieldLockInfoFactory.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Step.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Storable.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/SuperTypeAnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/SyncPolicy.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/SystemClassLoaderInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/SystemState.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/SystemTime.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ThreadChoiceGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ThreadData.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ThreadInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ThreadInfoSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ThreadList.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ThresholdFieldLockInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/ThrowsAnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/TidSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/TimeModel.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Transition.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/TypeAnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/TypeParameterAnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/TypeParameterBoundAnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Types.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/UncaughtException.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/VM.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/VMListener.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/VariableAnnotationInfo.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/Verify.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/ArrayElementInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/FieldInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/InstanceFieldInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/InstanceInvokeInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/InstructionInterface.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/InvokeInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/LocalVariableInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/LookupSwitchInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/NewInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/ReadInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/ReadOrWriteInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/ReturnInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/ReturnValueInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/StaticFieldInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/StoreInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/TableSwitchInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/bytecode/WriteInstruction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/BreakGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/CompoundChoiceGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/DoubleChoiceFromList.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/DoubleChoiceFromSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/DoubleSpec.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/DoubleThresholdGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/ExceptionThreadChoiceFromSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/ExposureCG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/FloatChoiceFromList.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/IntChoiceFromList.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/IntChoiceFromSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/IntIntervalGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/InvocationCG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/LongChoiceFromList.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/PermutationCG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/RandomIntIntervalGenerator.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/RandomOrderIntCG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/RandomOrderLongCG.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/ThreadChoiceFromSet.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/choice/TypedObjectChoice.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/Abstraction.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/AbstractionAdapter.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/AdaptiveSerializer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/AmmendableFilterConfiguration.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/DebugCFSerializer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/DebugFilteringSerializer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/DefaultFilterConfiguration.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/DynamicAbstractionSerializer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/FieldAmmendmentByName.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/FilterConfiguration.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/FilterFrame.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/FilteringSerializer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/FramePolicy.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/IgnoreConstants.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/IgnoreReflectiveNames.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/IgnoreThreadNastiness.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/IgnoreUtilSilliness.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/Ignored.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/IgnoresFromAnnotations.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/IncludesFromAnnotations.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/TopFrameSerializer.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/UnfilterField.java [new file with mode: 0644]
src/main/gov/nasa/jpf/vm/serialize/UnknownJPFClass.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/AtomicFieldUpdater.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_AnnotationProxyBase.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_CachedROHttpConnection.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_ConsoleOutputStream.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_DelegatingTimeZone.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_EventProducer.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_FinalizerThread.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_SerializationConstructor.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_test_MemoryGoal.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_tools_MethodTester.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_io_File.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_io_FileDescriptor.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_io_InputStreamReader.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_io_ObjectInputStream.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_io_ObjectOutputStream.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_io_ObjectStreamClass.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_io_OutputStreamWriter.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_io_RandomAccessFile.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Boolean.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Byte.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Character.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_ClassLoader.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Double.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Float.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Integer.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Long.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Math.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Object.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Runtime.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Short.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringBuffer.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringBuilder.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringCoding.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_System.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Thread.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_ThreadLocal.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_Throwable.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Array.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Constructor.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Field.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Method.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Proxy.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_net_URLClassLoader.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_net_URLDecoder.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_net_URLEncoder.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_security_MessageDigest.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_text_Bidi.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_text_DateFormat.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_text_DateFormatSymbols.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_text_DecimalFormat.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_text_DecimalFormatSymbols.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_text_Format.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_text_SimpleDateFormat.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_Calendar.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_Date.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_Locale.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_ResourceBundle.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_TimeZone.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_Exchanger.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicInteger.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicIntegerArray.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicLong.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicLongArray.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicReferenceArray.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_logging_Level.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Pattern.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_sun_misc_Unsafe.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_sun_misc_VM.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_sun_net_www_protocol_http_Handler.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_sun_reflect_Reflection.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/JPF_sun_reflect_ReflectionFactory.java [new file with mode: 0644]
src/peers/gov/nasa/jpf/vm/LoggablePeer.java [new file with mode: 0644]
src/tests/TypeNameTest.java [new file with mode: 0644]
src/tests/classloader_specific_tests/Class1.java [new file with mode: 0644]
src/tests/classloader_specific_tests/Class2.java [new file with mode: 0644]
src/tests/classloader_specific_tests/Class3.java [new file with mode: 0644]
src/tests/classloader_specific_tests/Interface1.java [new file with mode: 0644]
src/tests/classloader_specific_tests/Interface2.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/ConfigTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/configTestApp.jpf [new file with mode: 0644]
src/tests/gov/nasa/jpf/configTestCommon.jpf [new file with mode: 0644]
src/tests/gov/nasa/jpf/configTestIncludes.jpf [new file with mode: 0644]
src/tests/gov/nasa/jpf/configTestRequires.jpf [new file with mode: 0644]
src/tests/gov/nasa/jpf/configTestRequiresFail.jpf [new file with mode: 0644]
src/tests/gov/nasa/jpf/configTestSite.properties [new file with mode: 0644]
src/tests/gov/nasa/jpf/jvm/ClassInfoTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/jvm/JVMStackFrameTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/jvm/MethodInfoTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/jvm/NonResolvedClassInfo.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/basic/HarnessTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/basic/InstructionFactoryTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/basic/JPF_gov_nasa_jpf_test_basic_MJITest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/basic/ListenerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/basic/MJITest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/basic/TestJPFMainTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/basic/TestJPFNoMainTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/concurrent/AtomicIntegerFieldUpdaterTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/concurrent/AtomicLongFieldUpdaterTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/concurrent/AtomicReferenceFieldUpdaterTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/concurrent/CountDownLatchTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/concurrent/ExchangerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/concurrent/ExecutorServiceTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/concurrent/SemaphoreTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/io/BufferedInputStreamTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/io/FileIOStreamTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/io/FileIOTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/io/FileTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/io/ObjectStreamTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/lang/BoxObjectCacheTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/lang/ClassLoaderTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/lang/ClassTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/lang/CloneTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/lang/RuntimeTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/lang/StringTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/lang/SystemTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/lang/ref/WeakReferenceTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/lang/reflect/ConstructorTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/lang/reflect/FieldTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/lang/reflect/MethodTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/math/BigIntegerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/net/LoadUtility.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/net/URLClassLoaderTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/net/URLEncoderTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/text/DateFormatTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/text/DecimalFormatTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/text/SimpleDateFormatTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/AttrsTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/BreakTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/CGNotificationTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/CGRemoverTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/CGReorderTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/CascadedCGTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/ExceptionInjectorTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/ExtendTransitionTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/FinalBreakTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/FinalFieldChoiceTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/IdleLoopTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/InvokeListenerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/JPF_gov_nasa_jpf_test_mc_basic_AttrsTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/JPF_gov_nasa_jpf_test_mc_basic_InvokeListenerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/JPF_gov_nasa_jpf_test_mc_basic_NoJPFExecTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/JPF_gov_nasa_jpf_test_mc_basic_RestorerTest$X.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/LocalVarInfoTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/MethodListenerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/NoJPFExecTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/NullTrackerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/OOMEInjectorTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/OVHeapTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/RecursiveLockTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/RestorerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/SearchMultipleTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/SharedPropagationTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/SharedRefTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/SkipInstructionTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/StackDepthCheckerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/StatelessTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/TraceTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/TransitionLengthTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/UnlockNonSharedTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/basic/VerifyTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/CGCreatorFactoryTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/CrossingTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/DataChoiceTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/DynamicAbstractionTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/EventGeneratorTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/JSONTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/NativeStateHolderTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/NumericValueCheckerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/ObjectStreamTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/PerturbatorTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/RandomTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/StopWatchFuzzerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/TimeModelTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/data/TypedObjectChoiceTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/AtomicTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/ClinitTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/DaemonTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/DeadlockTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/ExceptionalThreadChoiceTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/FinalizerThreadTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/HORaceTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/JPF_gov_nasa_jpf_test_mc_threads_ExceptionalThreadChoiceTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/MinimizePreemptionTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/MissedPathTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/NestedInitTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/OldClassicTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/RaceTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/SchedulesTest-output [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/mc/threads/SchedulesTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/AnnotationTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/ArrayTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/AssertTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/CastTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/ClassInitTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/EndStateListener.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/EndStateTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/EnumTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/ExceptionHandlingTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/FieldTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/InitializeInterfaceClassObjectRefTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/JPFAttrAnnotationTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/LargeCodeTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/MethodTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/OutOfMemoryErrorTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/basic/RecursiveClinitTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/reflection/ArrayTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/reflection/ConstructorTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/reflection/FieldTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/reflection/MethodTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/reflection/ProxyTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/threads/InterruptTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/threads/JoinTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/threads/LockedStackDepthTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/threads/SuspendResumeTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/threads/ThreadExceptionHandlerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/threads/ThreadStopTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/threads/ThreadTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/vm/threads/WaitTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/xerces/SAXParserTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/xerces/http%^^www.puppycrawl.com^dtds^configuration_1_3.dtd [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/xerces/sun_checks.xml [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/ArrayIntSetTestBase.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/ArrayObjectQueueTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/AvailableBufferedInputStreamTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/BitSet1024Test.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/BitSet256Test.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/BitSet64Test.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/CommitOutputStreamTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/IdentityArrayObjectSetTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/IntTableTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/IntVectorTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/LimitedInputStreamTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/LocationSpecTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/MethodSpecTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/OATHashTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/ObjVectorTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/ObjectListTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/PSIntMapTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/PermutationGeneratorTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/SortedArrayIntSetTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/SortedArrayObjectSetTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/SparseClusterArrayTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/SparseIntVectorTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/SplitInputStreamTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/SplitOutputStreamTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/StringSetMatcherTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/UnsortedArrayIntSetTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/event/EventTreeTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/json/JSONLexerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/util/json/JSONParserTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/AnnotationInfoTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/ClassLoaderInfoTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/ElementInfoTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/SystemStateTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/TypesTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/choice/IntChoiceFromListTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/choice/IntChoiceFromSetTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/multiProcess/FinalizerThreadTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/multiProcess/JPF_gov_nasa_jpf_vm_multiProcess_MethodTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/multiProcess/JPF_gov_nasa_jpf_vm_multiProcess_NativePeerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/multiProcess/JPF_gov_nasa_jpf_vm_multiProcess_ThreadTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/multiProcess/JPF_gov_nasa_jpf_vm_multiProcess_TypeSeparationTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/multiProcess/MethodTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/multiProcess/NativePeerTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/multiProcess/StringTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/multiProcess/ThreadTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/vm/multiProcess/TypeSeparationTest.java [new file with mode: 0644]
src/tests/java8/DefaultMethodTest.java [new file with mode: 0644]
src/tests/java8/JPF_java8_DefaultMethodTest$G1.java [new file with mode: 0644]
src/tests/java8/LambdaTest.java [new file with mode: 0644]
src/tests/java8/TypeAnnotationTest.java [new file with mode: 0644]

diff --git a/.classpath b/.classpath
new file mode 100644 (file)
index 0000000..2721217
--- /dev/null
@@ -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>
diff --git a/.gitignore b/.gitignore
new file mode 100644 (file)
index 0000000..345194d
--- /dev/null
@@ -0,0 +1,17 @@
+.hg
+.hgignore
+local.properties
+.version
+.idea/workspace.xml
+.idea/fileColors.xml
+.idea/uiDesigner.xml
+nbproject/private/*
+build/*
+dist/*
+tmp/*
+trace
+activity*.png
+*.class
+*.orig
+*~
+*.DS_Store
diff --git a/.idea/.name b/.idea/.name
new file mode 100644 (file)
index 0000000..3836a03
--- /dev/null
@@ -0,0 +1 @@
+jpf-core
\ No newline at end of file
diff --git a/.idea/annotations.iml b/.idea/annotations.iml
new file mode 100644 (file)
index 0000000..f8666fe
--- /dev/null
@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<module type="JAVA_MODULE" version="4">
+  <component name="NewModuleRootManager" inherit-compiler-output="false">
+    <output url="file://$MODULE_DIR$/build/annotations" />
+    <output-test url="file://$MODULE_DIR$/build/annotations" />
+    <exclude-output />
+    <content url="file://$MODULE_DIR$/src/annotations">
+      <sourceFolder url="file://$MODULE_DIR$/src/annotations" isTestSource="false" />
+    </content>
+    <orderEntry type="inheritedJdk" />
+    <orderEntry type="sourceFolder" forTests="false" />
+  </component>
+</module>
diff --git a/.idea/artifacts/RunJPF.xml b/.idea/artifacts/RunJPF.xml
new file mode 100644 (file)
index 0000000..71c8dfa
--- /dev/null
@@ -0,0 +1,33 @@
+<component name="ArtifactManager">
+  <artifact type="jar" build-on-make="true" name="RunJPF">
+    <output-path>$PROJECT_DIR$/build</output-path>
+    <root id="archive" name="RunJPF.jar">
+      <element id="directory" name="META-INF">
+        <element id="file-copy" path="$PROJECT_DIR$/META-INF/RunJPF/MANIFEST.MF" />
+      </element>
+      <element id="directory" name="gov">
+        <element id="directory" name="nasa">
+          <element id="directory" name="jpf">
+            <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/Config.class" />
+            <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/Config$MissingRequiredKeyException.class" />
+            <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/JPFClassLoader.class" />
+            <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/JPFConfigException.class" />
+            <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/JPFShell.class" />
+            <element id="directory" name="tool">
+              <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/tool/Run.class" />
+              <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/tool/RunJPF.class" />
+            </element>
+            <element id="directory" name="util">
+              <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/util/JPFSiteUtils.class" />
+              <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/util/FileUtils.class" />
+              <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/util/StringMatcher.class" />
+              <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/util/Pair.class" />
+            </element>
+            <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/JPFException.class" />
+            <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/ConfigChangeListener.class" />
+          </element>
+        </element>
+      </element>
+    </root>
+  </artifact>
+</component>
\ No newline at end of file
diff --git a/.idea/artifacts/jpf.xml b/.idea/artifacts/jpf.xml
new file mode 100644 (file)
index 0000000..d43581a
--- /dev/null
@@ -0,0 +1,21 @@
+<component name="ArtifactManager">
+  <artifact type="jar" build-on-make="true" name="jpf">
+    <output-path>$PROJECT_DIR$/build</output-path>
+    <root id="archive" name="jpf.jar">
+      <element id="module-output" name="main" />
+      <element id="module-output" name="peers" />
+      <element id="module-output" name="annotations" />
+      <element id="directory" name="org">
+        <element id="directory" name="junit">
+          <element id="file-copy" path="$PROJECT_DIR$/build/classes/org/junit/After.class" />
+          <element id="file-copy" path="$PROJECT_DIR$/build/classes/org/junit/AfterClass.class" />
+          <element id="file-copy" path="$PROJECT_DIR$/build/classes/org/junit/Before.class" />
+          <element id="file-copy" path="$PROJECT_DIR$/build/classes/org/junit/BeforeClass.class" />
+          <element id="file-copy" path="$PROJECT_DIR$/build/classes/org/junit/Ignore.class" />
+          <element id="file-copy" path="$PROJECT_DIR$/build/classes/org/junit/Test$None.class" />
+          <element id="file-copy" path="$PROJECT_DIR$/build/classes/org/junit/Test.class" />
+        </element>
+      </element>
+    </root>
+  </artifact>
+</component>
\ No newline at end of file
diff --git a/.idea/artifacts/jpf_annotations.xml b/.idea/artifacts/jpf_annotations.xml
new file mode 100644 (file)
index 0000000..0e485a2
--- /dev/null
@@ -0,0 +1,8 @@
+<component name="ArtifactManager">
+  <artifact type="jar" build-on-make="true" name="jpf-annotations">
+    <output-path>$PROJECT_DIR$/build</output-path>
+    <root id="archive" name="jpf-annotations.jar">
+      <element id="module-output" name="annotations" />
+    </root>
+  </artifact>
+</component>
\ No newline at end of file
diff --git a/.idea/artifacts/jpf_classes.xml b/.idea/artifacts/jpf_classes.xml
new file mode 100644 (file)
index 0000000..42eabbb
--- /dev/null
@@ -0,0 +1,25 @@
+<component name="ArtifactManager">
+  <artifact type="jar" build-on-make="true" name="jpf-classes">
+    <output-path>$PROJECT_DIR$/build</output-path>
+    <root id="archive" name="jpf-classes.jar">
+      <element id="module-output" name="classes" />
+      <element id="module-output" name="annotations" />
+      <element id="directory" name="gov">
+        <element id="directory" name="nasa">
+          <element id="directory" name="jpf">
+            <element id="directory" name="vm">
+              <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/vm/Verify.class" />
+            </element>
+            <element id="directory" name="util">
+              <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/util/TypeRef.class" />
+              <element id="directory" name="test">
+                <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/util/test/TestJPF.class" />
+                <element id="file-copy" path="$PROJECT_DIR$/build/main/gov/nasa/jpf/util/test/TestMultiProcessJPF.class" />
+              </element>
+            </element>
+          </element>
+        </element>
+      </element>
+    </root>
+  </artifact>
+</component>
\ No newline at end of file
diff --git a/.idea/classes.iml b/.idea/classes.iml
new file mode 100644 (file)
index 0000000..d41594e
--- /dev/null
@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<module type="JAVA_MODULE" version="4">
+  <component name="NewModuleRootManager" inherit-compiler-output="false">
+    <output url="file://$MODULE_DIR$/build/classes" />
+    <output-test url="file://$MODULE_DIR$/build/classes" />
+    <exclude-output />
+    <content url="file://$MODULE_DIR$/src/classes">
+      <sourceFolder url="file://$MODULE_DIR$/src/classes" isTestSource="false" />
+    </content>
+    <orderEntry type="inheritedJdk" />
+    <orderEntry type="sourceFolder" forTests="false" />
+    <orderEntry type="module" module-name="annotations" />
+    <orderEntry type="module" module-name="main" />
+  </component>
+</module>
diff --git a/.idea/codeStyleSettings.xml b/.idea/codeStyleSettings.xml
new file mode 100644 (file)
index 0000000..7fb8ed0
--- /dev/null
@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project version="4">
+  <component name="ProjectCodeStyleSettingsManager">
+    <option name="PER_PROJECT_SETTINGS">
+      <value>
+        <XML>
+          <option name="XML_LEGACY_SETTINGS_IMPORTED" value="true" />
+        </XML>
+      </value>
+    </option>
+    <option name="PREFERRED_PROJECT_CODE_STYLE" value="Default (1)" />
+  </component>
+</project>
\ No newline at end of file
diff --git a/.idea/compiler.xml b/.idea/compiler.xml
new file mode 100644 (file)
index 0000000..8e650cc
--- /dev/null
@@ -0,0 +1,23 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project version="4">
+  <component name="CompilerConfiguration">
+    <option name="DEFAULT_COMPILER" value="Javac" />
+    <resourceExtensions />
+    <wildcardResourcePatterns>
+      <entry name="!?*.java" />
+      <entry name="!?*.form" />
+      <entry name="!?*.class" />
+      <entry name="!?*.groovy" />
+      <entry name="!?*.scala" />
+      <entry name="!?*.flex" />
+      <entry name="!?*.kt" />
+      <entry name="!?*.clj" />
+    </wildcardResourcePatterns>
+    <annotationProcessing>
+      <profile default="true" name="Default" enabled="false">
+        <processorPath useClasspath="true" />
+      </profile>
+    </annotationProcessing>
+    <bytecodeTargetLevel target="1.8" />
+  </component>
+</project>
\ No newline at end of file
diff --git a/.idea/copyright/profiles_settings.xml b/.idea/copyright/profiles_settings.xml
new file mode 100644 (file)
index 0000000..e7bedf3
--- /dev/null
@@ -0,0 +1,3 @@
+<component name="CopyrightManager">
+  <settings default="" />
+</component>
\ No newline at end of file
diff --git a/.idea/encodings.xml b/.idea/encodings.xml
new file mode 100644 (file)
index 0000000..d821048
--- /dev/null
@@ -0,0 +1,4 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project version="4">
+  <component name="Encoding" useUTFGuessing="true" native2AsciiForPropertiesFiles="false" />
+</project>
\ No newline at end of file
diff --git a/.idea/examples.iml b/.idea/examples.iml
new file mode 100644 (file)
index 0000000..1d41ef7
--- /dev/null
@@ -0,0 +1,16 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<module type="JAVA_MODULE" version="4">
+  <component name="NewModuleRootManager" inherit-compiler-output="false">
+    <output url="file://$MODULE_DIR$/build/examples" />
+    <output-test url="file://$MODULE_DIR$/build/examples" />
+    <exclude-output />
+    <content url="file://$MODULE_DIR$/src/examples">
+      <sourceFolder url="file://$MODULE_DIR$/src/examples" isTestSource="false" />
+    </content>
+    <orderEntry type="inheritedJdk" />
+    <orderEntry type="sourceFolder" forTests="false" />
+    <orderEntry type="module" module-name="annotations" />
+    <orderEntry type="module" module-name="main" />
+    <orderEntry type="module" module-name="peers" />
+  </component>
+</module>
diff --git a/.idea/main.iml b/.idea/main.iml
new file mode 100644 (file)
index 0000000..c393d6a
--- /dev/null
@@ -0,0 +1,14 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<module type="JAVA_MODULE" version="4">
+  <component name="NewModuleRootManager" inherit-compiler-output="false">
+    <output url="file://$MODULE_DIR$/build/main" />
+    <output-test url="file://$MODULE_DIR$/build/main" />
+    <exclude-output />
+    <content url="file://$MODULE_DIR$/src/main">
+      <sourceFolder url="file://$MODULE_DIR$/src/main" isTestSource="false" />
+    </content>
+    <orderEntry type="inheritedJdk" />
+    <orderEntry type="sourceFolder" forTests="false" />
+    <orderEntry type="module" module-name="annotations" />
+  </component>
+</module>
diff --git a/.idea/misc.xml b/.idea/misc.xml
new file mode 100644 (file)
index 0000000..4bda5bf
--- /dev/null
@@ -0,0 +1,57 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project version="4">
+  <component name="ClientPropertiesManager">
+    <properties class="javax.swing.AbstractButton">
+      <property name="hideActionText" class="java.lang.Boolean" />
+    </properties>
+    <properties class="javax.swing.JComponent">
+      <property name="html.disable" class="java.lang.Boolean" />
+    </properties>
+    <properties class="javax.swing.JEditorPane">
+      <property name="JEditorPane.w3cLengthUnits" class="java.lang.Boolean" />
+      <property name="JEditorPane.honorDisplayProperties" class="java.lang.Boolean" />
+      <property name="charset" class="java.lang.String" />
+    </properties>
+    <properties class="javax.swing.JList">
+      <property name="List.isFileList" class="java.lang.Boolean" />
+    </properties>
+    <properties class="javax.swing.JPasswordField">
+      <property name="JPasswordField.cutCopyAllowed" class="java.lang.Boolean" />
+    </properties>
+    <properties class="javax.swing.JSlider">
+      <property name="Slider.paintThumbArrowShape" class="java.lang.Boolean" />
+      <property name="JSlider.isFilled" class="java.lang.Boolean" />
+    </properties>
+    <properties class="javax.swing.JTable">
+      <property name="Table.isFileList" class="java.lang.Boolean" />
+      <property name="JTable.autoStartsEdit" class="java.lang.Boolean" />
+      <property name="terminateEditOnFocusLost" class="java.lang.Boolean" />
+    </properties>
+    <properties class="javax.swing.JToolBar">
+      <property name="JToolBar.isRollover" class="java.lang.Boolean" />
+    </properties>
+    <properties class="javax.swing.JTree">
+      <property name="JTree.lineStyle" class="java.lang.String" />
+    </properties>
+    <properties class="javax.swing.text.JTextComponent">
+      <property name="caretAspectRatio" class="java.lang.Double" />
+      <property name="caretWidth" class="java.lang.Integer" />
+    </properties>
+  </component>
+  <component name="EntryPointsManager">
+    <entry_points version="2.0" />
+  </component>
+  <component name="ProjectLevelVcsManager" settingsEditedManually="false">
+    <OptionsSetting value="true" id="Add" />
+    <OptionsSetting value="true" id="Remove" />
+    <OptionsSetting value="true" id="Checkout" />
+    <OptionsSetting value="true" id="Update" />
+    <OptionsSetting value="true" id="Status" />
+    <OptionsSetting value="true" id="Edit" />
+    <ConfirmationsSetting value="0" id="Add" />
+    <ConfirmationsSetting value="0" id="Remove" />
+  </component>
+  <component name="ProjectRootManager" version="2" languageLevel="JDK_1_8" default="false" assert-keyword="true" jdk-15="true" project-jdk-name="1.8" project-jdk-type="JavaSDK">
+    <output url="file://$PROJECT_DIR$/build" />
+  </component>
+</project>
\ No newline at end of file
diff --git a/.idea/modules.xml b/.idea/modules.xml
new file mode 100644 (file)
index 0000000..769a3f3
--- /dev/null
@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project version="4">
+  <component name="ProjectModuleManager">
+    <modules>
+      <module fileurl="file://$PROJECT_DIR$/.idea/annotations.iml" filepath="$PROJECT_DIR$/.idea/annotations.iml" />
+      <module fileurl="file://$PROJECT_DIR$/.idea/classes.iml" filepath="$PROJECT_DIR$/.idea/classes.iml" />
+      <module fileurl="file://$PROJECT_DIR$/.idea/examples.iml" filepath="$PROJECT_DIR$/.idea/examples.iml" />
+      <module fileurl="file://$PROJECT_DIR$/.idea/main.iml" filepath="$PROJECT_DIR$/.idea/main.iml" />
+      <module fileurl="file://$PROJECT_DIR$/.idea/peers.iml" filepath="$PROJECT_DIR$/.idea/peers.iml" />
+      <module fileurl="file://$PROJECT_DIR$/.idea/tests.iml" filepath="$PROJECT_DIR$/.idea/tests.iml" />
+    </modules>
+  </component>
+</project>
\ No newline at end of file
diff --git a/.idea/peers.iml b/.idea/peers.iml
new file mode 100644 (file)
index 0000000..23675dd
--- /dev/null
@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<module type="JAVA_MODULE" version="4">
+  <component name="NewModuleRootManager" inherit-compiler-output="false">
+    <output url="file://$MODULE_DIR$/build/peers" />
+    <output-test url="file://$MODULE_DIR$/build/peers" />
+    <exclude-output />
+    <content url="file://$MODULE_DIR$/src/peers">
+      <sourceFolder url="file://$MODULE_DIR$/src/peers" isTestSource="false" />
+    </content>
+    <orderEntry type="inheritedJdk" />
+    <orderEntry type="sourceFolder" forTests="false" />
+    <orderEntry type="module" module-name="main" />
+    <orderEntry type="module" module-name="annotations" />
+  </component>
+</module>
diff --git a/.idea/runConfigurations/run_example_jpf.xml b/.idea/runConfigurations/run_example_jpf.xml
new file mode 100644 (file)
index 0000000..78a37b9
--- /dev/null
@@ -0,0 +1,25 @@
+<component name="ProjectRunConfigurationManager">
+  <configuration default="false" name="run-example-jpf" type="ContextRunConfiguration" factoryName="ContextRun">
+    <extension name="coverage" enabled="false" merge="false" sample_coverage="true" runner="idea" />
+    <option name="MAIN_CLASS_NAME" value="gov.nasa.jpf.JPF" />
+    <option name="VM_PARAMETERS" value="-Xmx1024m -ea" />
+    <option name="PROGRAM_PARAMETERS" value="$FilePath$" />
+    <option name="WORKING_DIRECTORY" value="" />
+    <option name="ALTERNATIVE_JRE_PATH_ENABLED" value="false" />
+    <option name="ALTERNATIVE_JRE_PATH" value="" />
+    <option name="ENABLE_SWING_INSPECTOR" value="false" />
+    <option name="ENV_VARIABLES" />
+    <option name="PASS_PARENT_ENVS" value="true" />
+    <module name="examples" />
+    <envs />
+    <RunnerSettings RunnerId="Debug">
+      <option name="DEBUG_PORT" value="" />
+      <option name="TRANSPORT" value="0" />
+      <option name="LOCAL" value="true" />
+    </RunnerSettings>
+    <RunnerSettings RunnerId="Run" />
+    <ConfigurationWrapper RunnerId="Debug" />
+    <ConfigurationWrapper RunnerId="Run" />
+    <method />
+  </configuration>
+</component>
\ No newline at end of file
diff --git a/.idea/runConfigurations/run_test.xml b/.idea/runConfigurations/run_test.xml
new file mode 100644 (file)
index 0000000..fa0eace
--- /dev/null
@@ -0,0 +1,19 @@
+<component name="ProjectRunConfigurationManager">
+  <configuration default="false" name="run-test" type="ContextRunConfiguration" factoryName="ContextRun">
+    <extension name="coverage" enabled="false" merge="false" sample_coverage="true" runner="idea" />
+    <option name="MAIN_CLASS_NAME" value="gov.nasa.jpf.tool.RunTest" />
+    <option name="VM_PARAMETERS" value="-Xmx1024m -ea" />
+    <option name="PROGRAM_PARAMETERS" value="$FileClass$ $SelectedText$" />
+    <option name="WORKING_DIRECTORY" value="" />
+    <option name="ALTERNATIVE_JRE_PATH_ENABLED" value="false" />
+    <option name="ALTERNATIVE_JRE_PATH" value="" />
+    <option name="ENABLE_SWING_INSPECTOR" value="false" />
+    <option name="ENV_VARIABLES" />
+    <option name="PASS_PARENT_ENVS" value="true" />
+    <module name="tests" />
+    <envs />
+    <RunnerSettings RunnerId="Run" />
+    <ConfigurationWrapper RunnerId="Run" />
+    <method />
+  </configuration>
+</component>
\ No newline at end of file
diff --git a/.idea/scopes/scope_settings.xml b/.idea/scopes/scope_settings.xml
new file mode 100644 (file)
index 0000000..922003b
--- /dev/null
@@ -0,0 +1,5 @@
+<component name="DependencyValidationManager">
+  <state>
+    <option name="SKIP_IMPORT_STATEMENTS" value="false" />
+  </state>
+</component>
\ No newline at end of file
diff --git a/.idea/tests.iml b/.idea/tests.iml
new file mode 100644 (file)
index 0000000..ac9f595
--- /dev/null
@@ -0,0 +1,17 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<module type="JAVA_MODULE" version="4">
+  <component name="NewModuleRootManager" inherit-compiler-output="false">
+    <output url="file://$MODULE_DIR$/build/tests" />
+    <output-test url="file://$MODULE_DIR$/build/tests" />
+    <exclude-output />
+    <content url="file://$MODULE_DIR$/src/tests">
+      <sourceFolder url="file://$MODULE_DIR$/src/tests" isTestSource="false" />
+    </content>
+    <orderEntry type="inheritedJdk" />
+    <orderEntry type="sourceFolder" forTests="false" />
+    <orderEntry type="module" module-name="annotations" />
+    <orderEntry type="module" module-name="main" />
+    <orderEntry type="module" module-name="classes" />
+    <orderEntry type="module" module-name="peers" />
+  </component>
+</module>
diff --git a/.idea/vcs.xml b/.idea/vcs.xml
new file mode 100644 (file)
index 0000000..e161617
--- /dev/null
@@ -0,0 +1,6 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project version="4">
+  <component name="VcsDirectoryMappings">
+    <mapping directory="$PROJECT_DIR$" vcs="hg4idea" />
+  </component>
+</project>
\ No newline at end of file
diff --git a/.project b/.project
new file mode 100644 (file)
index 0000000..d43fdf8
--- /dev/null
+++ b/.project
@@ -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>
diff --git a/LICENSE-2.0.txt b/LICENSE-2.0.txt
new file mode 100644 (file)
index 0000000..d645695
--- /dev/null
@@ -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.
diff --git a/META-INF/RunJPF/MANIFEST.MF b/META-INF/RunJPF/MANIFEST.MF
new file mode 100644 (file)
index 0000000..a270c0c
--- /dev/null
@@ -0,0 +1,3 @@
+Manifest-Version: 1.0
+Main-Class: gov.nasa.jpf.tool.RunJPF
+
diff --git a/README b/README
new file mode 100644 (file)
index 0000000..8fbfa95
--- /dev/null
+++ b/README
@@ -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
diff --git a/bin/javajpf b/bin/javajpf
new file mode 100755 (executable)
index 0000000..cc3fe37
--- /dev/null
@@ -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 "$@"
diff --git a/bin/jpf b/bin/jpf
new file mode 100755 (executable)
index 0000000..6db4727
--- /dev/null
+++ b/bin/jpf
@@ -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" "$@"
+
diff --git a/bin/jpf.bat b/bin/jpf.bat
new file mode 100755 (executable)
index 0000000..a891c21
--- /dev/null
@@ -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" %*
+
diff --git a/bin/print_class b/bin/print_class
new file mode 100755 (executable)
index 0000000..31534ef
--- /dev/null
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+JPF_HOME=`dirname "$0"`/..
+
+java -classpath "$JPF_HOME/build/jpf.jar" gov.nasa.jpf.jvm.ClassFilePrinter "$@"
diff --git a/bin/print_class.bat b/bin/print_class.bat
new file mode 100755 (executable)
index 0000000..643790a
--- /dev/null
@@ -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 %*
+
diff --git a/bin/print_events b/bin/print_events
new file mode 100755 (executable)
index 0000000..3c95eb7
--- /dev/null
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+JPF_HOME=`dirname "$0"`/..
+
+java -classpath "$JPF_HOME/build/jpf.jar" gov.nasa.jpf.tool.PrintEvents "$@"
diff --git a/bin/test b/bin/test
new file mode 100755 (executable)
index 0000000..c2d1c5d
--- /dev/null
+++ b/bin/test
@@ -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" "$@"
+
diff --git a/bin/test.bat b/bin/test.bat
new file mode 100755 (executable)
index 0000000..c4351c3
--- /dev/null
@@ -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" %*
+
diff --git a/build.properties b/build.properties
new file mode 100644 (file)
index 0000000..6602f96
--- /dev/null
@@ -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
diff --git a/build.xml b/build.xml
new file mode 100644 (file)
index 0000000..ca73885
--- /dev/null
+++ b/build.xml
@@ -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>
diff --git a/doc/devel/attributes.md b/doc/devel/attributes.md
new file mode 100644 (file)
index 0000000..69c7f83
--- /dev/null
@@ -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
diff --git a/doc/devel/bytecode_factory.md b/doc/devel/bytecode_factory.md
new file mode 100644 (file)
index 0000000..6fb8c2c
--- /dev/null
@@ -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
diff --git a/doc/devel/choicegenerator.md b/doc/devel/choicegenerator.md
new file mode 100644 (file)
index 0000000..e8272eb
--- /dev/null
@@ -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`
+  *