[junit] Picked up _JAVA_OPTIONS: -Xmx2048m -Xms512m
[junit] Running TypeNameTest
[junit]   running jpf with args:
[junit] Tests run: 1, Failures: 1, Errors: 0, Skipped: 0, Time elapsed: 0.701 sec
[junit] java.lang.ArrayIndexOutOfBoundsException: 1
[junit] 	at gov.nasa.jpf.jvm.JVMClassInfo$Initializer.setBootstrapMethod(JVMClassInfo.java:93)
[junit] 	at gov.nasa.jpf.jvm.ClassFile.setBootstrapMethod(ClassFile.java:659)
[junit] 	at gov.nasa.jpf.jvm.ClassFile.parseBootstrapMethodAttr(ClassFile.java:1422)
[junit] 	at gov.nasa.jpf.jvm.JVMClassInfo$Initializer.setClassAttribute(JVMClassInfo.java:80)
[junit] 	at gov.nasa.jpf.jvm.ClassFile.setClassAttribute(ClassFile.java:636)
[junit] 	at gov.nasa.jpf.jvm.ClassFile.parseClassAttributes(ClassFile.java:1306)
[junit] 	at gov.nasa.jpf.jvm.ClassFile.parse(ClassFile.java:875)
[junit] 	at gov.nasa.jpf.jvm.JVMClassInfo$Initializer.<init>(JVMClassInfo.java:48)
[junit] 	at gov.nasa.jpf.jvm.JVMClassInfo.<init>(JVMClassInfo.java:619)
[junit] 	at gov.nasa.jpf.jvm.JVMClassFileContainer$JVMClassFileMatch.createClassInfo(JVMClassFileContainer.java:58)
[junit] 	at gov.nasa.jpf.jvm.JVMClassFileContainer$JVMClassFileMatch.createClassInfo(JVMClassFileContainer.java:33)
[junit] 	at gov.nasa.jpf.vm.ClassLoaderInfo.getResolvedClassInfo(ClassLoaderInfo.java:353)
[junit] 	at gov.nasa.jpf.vm.SystemClassLoaderInfo.getResolvedClassInfo(SystemClassLoaderInfo.java:147)
[junit] 	at gov.nasa.jpf.vm.VM.getStartupSystemClassInfos(VM.java:445)
[junit] 	at gov.nasa.jpf.vm.VM.initializeMainThread(VM.java:564)
[junit] 	at gov.nasa.jpf.vm.SingleProcessVM.initialize(SingleProcessVM.java:130)
[junit] 	at gov.nasa.jpf.JPF.run(JPF.java:611)
[junit] 	at gov.nasa.jpf.util.test.TestJPF.createAndRunJPF(TestJPF.java:675)
[junit] 	at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:806)
[junit] 	at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:830)
[junit] 	at TypeNameTest.testArrayCloning(TypeNameTest.java:58)

The ClassFile parser seems to find just single bootstrap method argument, whereas in JVMClassInfo$Initializer.setBootstrapMethod it expects an element with index 1 in the bmArgs array.

https://github.com/javapathfinder/jpf-core/blob/18a0c42de3e80be0c2ddcf0d212e376e576fcda0/src/main/gov/nasa/jpf/jvm/ClassFile.java#L1386-L1422

https://github.com/javapathfinder/jpf-core/blob/18a0c42de3e80be0c2ddcf0d212e376e576fcda0/src/main/gov/nasa/jpf/jvm/JVMClassInfo.java#L91-L93

This seems to happen when trying to create ClassInfo for startupSystemClasses. So for instance sysCl.getResolvedClassInfo("java.lang.Class") would throw java.lang.ArrayIndexOutOfBoundsException' exception.

sysCl.getResolvedClassInfo("java.lang.Object") however resolves fine.

References

Saved diff of Class.class for Java 8 and 10: https://www.diffchecker.com/0A0yIEXK

Travis log: https://travis-ci.org/javapathfinder/jpf-core/builds/381994510#L3057-L3083

The failing test case in #294 seems related to this assert statement. If I remove it, the test passes. But I have no clue how this effects in a side effect the ExchangerTest. If we remove it, everything work on my system.

Any ideas why this is the case?

PolDet@JPF

PolDet (Pollution Detection) implementation using Java PathFinder. This tool detects JUnit tests that pollute the shared program state. For more information, read our paper accepted by JPF workshop 2021: https://y553546436.github.io/files/jpf_sen.pdf .

PolDet implementation

PolDet implementation is in the following three files:

1. src/tests/PolDet/PolDetMain.java
2. src/peers/JPF_PolDetListener.java
3. src/main/gov/nasa/jpf/vm/serialize/PolDetSerializer.java

File PolDetMain.java contains class PolDetMain, the entry class to run PolDet. It also contains PolDetListener class, a specialized JUnit listener to call our code before and after the test. File JPF_PolDetListener.java contains the peer class for PolDetListener class. File PolDetSerializer.java contains a specialized JPF state serializer which ignores certain irrelevant parts of the state when serializing.

7 example JUnit test methods are in src/tests/PolDet/PolDetExamples.java, which can be used to check the functionality of PolDet.

Note that no existing code is changed in jpf-core, so it is unlikely that some existing functionality breaks with the changes.

Usage

To run PolDet@JPF:

./gradlew runPolDet -PtestClasspath=$CLASSPATH -PtestClass=$CLASSNAME

where $CLASSPATH is the classpath to the test class, and $CLASSNAME is the fully qualified test class name.

To test PolDet@JPF on the 7 example tests in src/tests/PolDet/PolDetExamples.java, run

./gradlew testPolDet

Get the classpath for a Maven project

If you want to run a test class in a Maven project, you can get the classpath containing the class and its dependencies with the following command:

cd $MODULE
CP=$(pwd)/target/classes:$(pwd)/target/test-classes:$(mvn dependency:build-classpath | grep -A1 "\[INFO\] Dependencies classpath:" | tail -1)

For a single-module maven project, MODULE is the project directory. For a multi-project maven directory, ​MODULE is the specific module directory containing the test class. For example, project httpcomponents-client (https://github.com/apache/httpcomponents-client) contains sub-modules like httpclient5 and httpclient5-cache. If your test class is inside httpclient5 module, you should run the CP=... command in directory httpcomponents-client/httpclient5 to get the correct classpath. To test your classpath, you can run PolDet@JPF on test class org.apache.hc.client5.http.async.methods.SimpleBasicHttpRequests with the script above. There should be one test method named testCreateMethodUriString detected as a polluter test.

Java 8 has introduced a new library to deal with large data structures, Java Streams:

https://docs.oracle.com/javase/8/docs/api/java/util/stream/package-summary.html

We don't have any unit tests for the new Java streams collections (java.util.stream), and thus we don't know how well JPF handles them (if at all). A few examples (unit tests) would be helpful to see if JPF can handle these cases at all (there may be missing native peer classes/methods), and what problems there might be.

FAILURE: Build failed with an exception.

• Where: Build file 'C:\Users\gaura\jpf\jpf-core\build.gradle' line: 24

• What went wrong: A problem occurred evaluating root project 'jpf-core'.

Could not find method testCompile() for arguments [org.ow2.asm:asm:7.1] on object of type org.gradle.api.internal.artifacts.dsl.dependencies.DefaultDependencyHandler.

• Try:

Run with --stacktrace option to get the stack trace. Run with --info or --debug option to get more log output. Run with --scan to get full insights.

• Get more help at https://help.gradle.org

BUILD FAILED in 13s

I have been trying to build java-10-gradle on my Windows 10 OS. With java version : java version "11.0.9" 2020-10-20 LTS Java(TM) SE Runtime Environment 18.9 (build 11.0.9+7-LTS) Java HotSpot(TM) 64-Bit Server VM 18.9 (build 11.0.9+7-LTS, mixed mode). The site.properties file which I have added is

JPF site configuration

jpf-core = $D:\OpenSource\jpf-core extensions=${jpf-core}

When I run gradlew buildJars this is output

Task :compileClassesJava FAILED D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:53: error: cannot find symbol private static JavaUtilJarAccess javaUtilJarAccess; ^ symbol: class JavaUtilJarAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:55: error: cannot find symbol private static JavaLangInvokeAccess javaLangInvokeAccess; ^ symbol: class JavaLangInvokeAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:57: error: cannot find symbol private static JavaNetURLAccess javaNetURLAccess; ^ symbol: class JavaNetURLAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:63: error: cannot find symbol private static JavaObjectInputStreamAccess javaObjectInputStreamAccess; ^ symbol: class JavaObjectInputStreamAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:64: error: cannot find symbol private static JavaObjectInputFilterAccess javaObjectInputFilterAccess; ^ symbol: class JavaObjectInputFilterAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:75: error: cannot find symbol public static void setJavaLangInvokeAccess(JavaLangInvokeAccess jlia) { ^ symbol: class JavaLangInvokeAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:79: error: cannot find symbol public static JavaLangInvokeAccess getJavaLangInvokeAccess() { ^ symbol: class JavaLangInvokeAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:98: error: cannot find symbol public static void setJavaNetURLAccess(JavaNetURLAccess jnua) { ^ symbol: class JavaNetURLAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:102: error: cannot find symbol public static JavaNetURLAccess getJavaNetURLAccess() { ^ symbol: class JavaNetURLAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:108: error: cannot find symbol public static JavaUtilJarAccess javaUtilJarAccess() { ^ symbol: class JavaUtilJarAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:114: error: cannot find symbol public static void setJavaUtilJarAccess(JavaUtilJarAccess access) { ^ symbol: class JavaUtilJarAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:168: error: cannot find symbol public static JavaObjectInputStreamAccess getJavaObjectInputStreamAccess() { ^ symbol: class JavaObjectInputStreamAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:177: error: cannot find symbol public static void setJavaObjectInputStreamAccess(JavaObjectInputStreamAccess access) { ^ symbol: class JavaObjectInputStreamAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:181: error: cannot find symbol public static JavaObjectInputFilterAccess getJavaObjectInputFilterAccess() { ^ symbol: class JavaObjectInputFilterAccess location: class SharedSecrets D:\OpenSource\jpf-core\src\classes\modules\java.base\jdk\internal\misc\SharedSecrets.java:188: error: cannot find symbol public static void setJavaObjectInputFilterAccess(JavaObjectInputFilterAccess access) { ^ symbol: class JavaObjectInputFilterAccess location: class SharedSecrets 15 errors

FAILURE: Build failed with an exception.

• What went wrong:

Execution failed for task ':compileClassesJava'.

Compilation failed; see the compiler error output for details.

• Try:

Run with --stacktrace option to get the stack trace. Run with --info or --debug option to get more log output. Run with --scan to get full insights.

• Get more help at https://help.gradle.org

BUILD FAILED in 2s

4 actionable tasks: 1 executed, 3 up-to-date

I am running this test upon java-10-gradle branch.

I have also tried running gradlew clean check --stacktrace . Check out this file for the errors. gradlew clean check.txt

If anyone has anyone any solutions this do hit me up.

Simple printf statements such as printf("%c", 'a'); do not work at the moment, due to internal problems with formatting that cause exceptions in a native peer class.

The corresponding unit test testPrintCharFormat is in src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java, with the failing code commented out.

It would be desirable to have a more complete unit test (with other printf options), and fixes in the model/peer classes that can support such functionality.

I've updated the gradle version to 5.6.4 didn't notice any specific behavior or errors in plugins/dependencies same for version 6.9 I've also attached the detailed log-file Result Logs.txt

when i run SharedSecrets.java, this error message appears on the screen. How can i fix that? Is depending on jdk version?

......................................... testing testBasic() ......................................... testBasic: Ok

......................................... testing testEnumeration() ......................................... testEnumeration: Ok

......................................... testing testOutOfBounds() java.lang.IndexOutOfBoundsException: BitSet1024 index out of range: 2264 java.lang.IndexOutOfBoundsException: BitSet1024 index out of range: 1256 java.lang.IndexOutOfBoundsException: BitSet1024 index out of range: -1 ......................................... testOutOfBounds: Ok

......................................... execution of testsuite: gov.nasa.jpf.util.BitSet1024Test SUCCEEDED .... [1] testBasic: Ok .... [2] testEnumeration: Ok .... [3] testOutOfBounds: Ok ......................................... tests: 3, failures: 0, errors: 0

The static method java.lang.ThreadLocal.withInitial (added in JDK 1.8) is currently missing. This can be fixed by adding

  public static <S> ThreadLocal<S> withInitial(Supplier<? extends S> supplier) {
    return new SuppliedThreadLocal<>(supplier);
  }

to ThreadLocal here https://github.com/javapathfinder/jpf-core/blob/7e63ebf36369f63a1ddfac7374e7defeb948c8fe/src/classes/java/lang/ThreadLocal.java#L98-L100

Our java.lang.ClassLoader model class references java.lang.CompoundEnumeration which is an auxilary class declared within the java standard class java/lang/ClassLoader.java

This includes CompoundEnumeration class within our model class itself, so to prevent our ClassLoader model class from referencing an auxilary class from outside its own source file.

This fixes: warning: auxiliary class CompoundEnumeration in ClassLoader.java should not be accessed from outside its own source file

Fixes: #90

I have defined a simple bank class which is attached to this issue: bank.zip Basically it's a bank with a map of ids (ints) to accounts (instances of the class Account) and a lock (RentrantReadWriteLock) to control the access to this map. The class Account has a balance (int) and a lock (ReentrantLock) to protect the balance from concurrent accesses. Thus, we have concurrency control for:

• an individual account to prevent, for example, an withdraw and a deposit at the same time for the same account;
• the whole bank to prevent, for example, a removal and a deposit at the same time for the same account.

In the class defined there's a problem with the method transfer: in certain situations it can lead to a deadlock. This happens because the locks for the accounts are not obtained in order: cfrom = accounts.get(from); cto = accounts.get(to);

For instance, if there's a transfer from account0 to account1 in thread1 at the same time as a transfer from account1 to account0 in thread2, the following thread interleaving leads to a deadlock:

• thread1 acquires lock from account0
• thread2 acquires lock from account1
• thread1 tries to acquire lock from account1 but it's taken
• thread2 tries to acquire lock from account0 but it's taken

I have been trying to catch this deadlock with jpf and it does not report it. I have been using the default jpf.properties, the only change I made was remove the gov.nasa.jpf.vm.NoUncaughtExceptionsProperty from search.properties. The application properties is as simple as:

target = BankReadWriteLock classpath=.

I have tried to add to the application properties the gov.nasa.jpf.listener.DeadlockAnalyzer listener but it didn't work either.

This is the output I receive:

I find it to be very strange the fact that it only reports one new state. It seems like different thread interleavings are not being considered.

Is there a problem with the configuration I am using or jpf is really not catching this deadlock?

I have this super minimal reproduction:

public class Input {
  public static void main(String[] args) {
    System.out.println("-------- In main!");

    java.util.logging.Logger.getLogger("blah");
  }
}

I'm running it against the java-10-gradle branch (a8160543fecaee799587c955c429aa7f068a410a) and the first thing I get when calling that is:

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: Calling java.lang.Thread.<init>(Ljava/lang/ThreadGroup;Ljava/lang/Runnable;Ljava/lang/String;JZ)V
	at java.util.logging.LogManager$Cleaner.<init>(LogManager.java:261)
	at java.util.logging.LogManager.<init>(LogManager.java:301)
	at java.util.logging.LogManager.<init>(LogManager.java:294)
	at java.util.logging.LogManager$1.run(LogManager.java:248)
	at java.util.logging.LogManager$1.run(LogManager.java:223)
	at java.security.AccessController.doPrivileged(AccessController.java:34)
	at java.util.logging.LogManager.<clinit>(LogManager.java:223)
	at java.util.logging.Logger.demandLogger(Logger.java:648)
	at java.util.logging.Logger.getLogger(Logger.java:717)
	at java.util.logging.Logger.getLogger(Logger.java:701)
	at Input.main(Input.java:5)

So I added an extra method with an (ignored) boolean to here: https://github.com/javapathfinder/jpf-core/blob/a8160543fecaee799587c955c429aa7f068a410a/src/classes/modules/java.base/java/lang/Thread.java#L118-L121

I then ran into a similar issue from java.security.AccessController and added another dummy overload there.

That got me past the initial issue, but now I'm stuck here:

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native jdk.internal.misc.VM.initializeFromArchive
	at jdk.internal.misc.VM.initializeFromArchive(gov.nasa.jpf.vm.JPF_jdk_internal_misc_VM)
	at java.util.ImmutableCollections$SetN.<clinit>(ImmutableCollections.java:583)
	at java.util.Set.of(Set.java:502)
	at java.nio.file.spi.FileSystemProvider.<clinit>(FileSystemProvider.java:428)
	at sun.nio.fs.DefaultFileSystemProvider.<clinit>(DefaultFileSystemProvider.java:35)
	at java.nio.file.FileSystems.getDefault(FileSystems.java:185)
	at java.nio.file.Path.of(Path.java:147)
	at java.nio.file.Paths.get(Paths.java:69)
	at java.util.logging.LogManager.getConfigurationFileName(LogManager.java:1389)
	at java.util.logging.LogManager.readConfiguration(LogManager.java:1375)
	at java.util.logging.LogManager.readPrimordialConfiguration(LogManager.java:445)
	at java.util.logging.LogManager$2.run(LogManager.java:394)
	at java.security.AccessController.doPrivileged(AccessController.java:39)
	at java.util.logging.LogManager.ensureLogManagerInitialized(LogManager.java:382)
	at java.util.logging.LogManager.getLogManager(LogManager.java:430)
	at java.util.logging.Logger.demandLogger(Logger.java:648)
	at java.util.logging.Logger.getLogger(Logger.java:717)
	at java.util.logging.Logger.getLogger(Logger.java:701)
	at Input.main(Input.java:5)

Which doesn't seem to be as easy to fix as the two above. Anyone have hints for how to get past this?

I see a few old mentions of those classes in old issues but those were closed. I just ran a fresh git clone and got this:

% ./gradlew buildJars                                            

> Task :compileJava FAILED
/Users/dgp/Sandbox/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:21: error: cannot find symbol
import sun.misc.SharedSecrets;
               ^
  symbol:   class SharedSecrets
  location: package sun.misc
/Users/dgp/Sandbox/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:22: error: cannot find symbol
import sun.misc.JavaLangAccess;
               ^
  symbol:   class JavaLangAccess
  location: package sun.misc
/Users/dgp/Sandbox/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:85: error: cannot find symbol
   static final JavaLangAccess JLA = SharedSecrets.getJavaLangAccess();
                ^
  symbol:   class JavaLangAccess
  location: class HashedAllocationContext
/Users/dgp/Sandbox/jpf-core/src/main/gov/nasa/jpf/vm/HashedAllocationContext.java:85: error: cannot find symbol
   static final JavaLangAccess JLA = SharedSecrets.getJavaLangAccess();
                                     ^
  symbol:   variable SharedSecrets
  location: class HashedAllocationContext
Note: Some input files use or override a deprecated API.
Note: Recompile with -Xlint:deprecation for details.
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
4 errors

FAILURE: Build failed with an exception.

* What went wrong:
Execution failed for task ':compileJava'.
> Compilation failed; see the compiler error output for details.

* Try:
Run with --stacktrace option to get the stack trace. Run with --info or --debug option to get more log output. Run with --scan to get full insights.

* Get more help at https://help.gradle.org

Deprecated Gradle features were used in this build, making it incompatible with Gradle 7.0.
Use '--warning-mode all' to show the individual deprecation warnings.
See https://docs.gradle.org/6.9/userguide/command_line_interface.html#sec:command_line_warnings

BUILD FAILED in 2s
3 actionable tasks: 1 executed, 2 up-to-date

% git rev-parse HEAD 
45a4450cd0bd1193df5419f7c9d9b89807d00db6

% java --version
openjdk 11.0.14.1 2022-02-08 LTS
OpenJDK Runtime Environment Corretto-11.0.14.10.1 (build 11.0.14.1+10-LTS)
OpenJDK 64-Bit Server VM Corretto-11.0.14.10.1 (build 11.0.14.1+10-LTS, mixed mode)

Am I doing something wrong?

Backports the Gradle configuration from the java-10-gradle branch to the java-8[-gradle] branch.

I've also updated the .gitignore file to match the current master and removed the now-ignored IDE configuration files, as was done previously for the non-java-8 branches with commits 6b734c1aecd121c7fcaca98a99d43f34fedefdfa and c0c3ef2475f5c20378321e0dc2069744e1a63462.

The GitHub Actions configuration assumes that the target branch will be called "java-8-gradle" rather than "java-8", thereby matching the naming of the "java-10-gradle" branch.

One of the tests initially failed due to a missing method in one of the model classes (I assume the test also failed before adding Gradle support?), though that was simple to fix by adding the missing method to the model class.

I'm getting this error when running JPF. Any idea what it's telling me?

java.lang.ArrayIndexOutOfBoundsException: 1
        at gov.nasa.jpf.vm.NamedFields.setDoubleValue(NamedFields.java:164)
        at gov.nasa.jpf.vm.FunctionObjectFactory.setFuncObjFields(FunctionObjectFactory.java:60)
        at gov.nasa.jpf.vm.FunctionObjectFactory.getFunctionObject(FunctionObjectFactory.java:37)
        at gov.nasa.jpf.jvm.bytecode.INVOKEDYNAMIC.execute(INVOKEDYNAMIC.java:121)
        at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
        at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
        at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
        at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
        at gov.nasa.jpf.search.Search.forward(Search.java:937)
        at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
        at gov.nasa.jpf.JPF.run(JPF.java:613)
        at gov.nasa.jpf.JPF.start(JPF.java:189)
        at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
        at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
        at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
        at java.lang.reflect.Method.invoke(Method.java:498)
        at gov.nasa.jpf.tool.Run.call(Run.java:85)
        at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)