javapathfinder / jpf-core Goto Github PK

JPF is an extensible software analysis framework for Java bytecode. jpf-core is the basis for all JPF projects; you always need to install it. It contains the basic VM and model checking infrastructure, and can be used to check for concurrency defects like deadlocks, and unhandled exceptions like NullPointerExceptions and AssertionErrors.

Shell 0.01% Batchfile 0.01% Java 99.98%

jpf-core's Introduction

Java PathFinder

An extensible software model checking framework for Java bytecode programs

General Information about JPF

All the latest developments, changes, documentation can be found on our wiki page.

Building and Installing

If you are having problems installing and running JPF, please look at the How to install JPF guide.

Note that we have transitioned to OpenJDK with the new version of JPF (for Java 11), so unlike branch java-8, the new default version for Java 11 no longer compiles using Oracle's JDK.

We have documented on the wiki a lot of common problems during the install and build processes reported by users. If you are facing any issue, please, make sure that we have not addressed it in documentation. Otherwise, feel free to contact us at [email protected] or open an issue on the Issue Tracker.

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 [email protected].

Contributions are welcomed and we encourage you to get involved with the community.

Happy Verification -- the Java PathFinder team

jpf-core's People

Contributors

Stargazers

Watchers

Forkers

anna-20 yannicnoller gayanw upthewaterspout rerui wvisser imfenix chdd heysunk knlsharma jasonpap marstone pedzindm1 leorpoirot tigerqiu712 anton-saurytski utpalmishra21 grzesuav peterschrammel shubhamkr21 uwplse georgeyang95 killxin sudokulover scristalli ngocpq sidb54 mice52221 manishkk durubayram nmhai philipz zqcui manish3499 vladimir95 acferreir4 adhamelshafie mudasirhw miuone ashwinkolhatkar gkumarcoder basanders saranganj shagun26 sang12-2017-18 mithu22 yuvaraj-anbarasan jentsch hayawi hemangandhi alexliu4523 z420 akhilless cpadmanabhuni trungchubao hk321 rupalisain1993 dcato hkcyf369 minxingtang junfus junyewen mariapaquin rtrimana beckersamuel glaciallake sumitdas20 jorajeev cinggs taeyang123456 pansot2 wenlf tsumahmud grese fanfan-yang gipsond wenranlu zitianxie blueskeptical forest1995 lijobs tchigher mfrank2016 aliveon mih475 ankushdesai shlomi643 ashr123 xintao-c javapathfinderextensions hecoz starrysirens dxtkastb mpolitano chnpat dexmagic evanleung08 adarsh-shahi kalyan-kumar thesingleton

jpf-core's Issues

error: [junit] cannot load system class java.lang.Object

When running tests compiled with Java 9 and later, results in the run time errors look like the following:

[junit] Picked up _JAVA_OPTIONS: -Xmx2048m -Xms512m
[junit] Running TypeNameTest
[junit]   running jpf with args:
[junit] [SEVERE] cannot load system class java.lang.Object
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.521 sec
[junit] gov.nasa.jpf.vm.ClassInfoException: class not found: java.lang.Object
[junit] 	at gov.nasa.jpf.vm.ClassLoaderInfo.getResolvedClassInfo(ClassLoaderInfo.java:363)
[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)

Possibly because of the new Module System, the class URI of the generated .class files in the build destination directory are different than previously, which makes JPF classloader to fail resolve the model classes from jpf-classes.jar

JDK 8

build/classes/
├── java
│   ├── io
│   ├── lang
│   │   ├── annotation
│   │   ├── ref
│   │   └── reflect

JDK 9/10

build/classes/
├── java.base
│   ├── java
│   │   ├── io
│   │   ├── lang
│   │   │   ├── annotation
│   │   │   ├── ref
│   │   │   └── reflect

https://travis-ci.org/javapathfinder/jpf-core/builds/381450375#L3059-L3073

JVMClassInfo$Initializer.setBootstrapMethod ArrayIndexOutOfBoundsException

[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.

jpf-core/src/main/gov/nasa/jpf/jvm/ClassFile.java

Lines 1386 to 1422 in 18a0c42

 /** 

  * BootstrapMethods_attribute { 

  * u2 attribute_name_index; 

  * u4 attribute_length; 

  * u2 num_bootstrap_methods; 

  * { u2 bootstrap_method_ref; -> MethodHandle 

  * u2 num_bootstrap_arguments; 

  * u2 bootstrap_arguments[num_bootstrap_arguments]; 

  * } bootstrap_methods[num_bootstrap_methods]; 

  * } 

  *  

  * pos is at num_bootstrap_methods 

  */ 

 public void parseBootstrapMethodAttr (ClassFileReader reader, Object tag){ 

 int nBootstrapMethods = readU2(); 

 setBootstrapMethodCount(reader, tag, nBootstrapMethods); 

 for (int i=0; i<nBootstrapMethods; i++){ 

 int cpMhIdx = readU2(); 

 int nArgs = readU2(); 

 int[] bmArgs = new int[nArgs]; 

 for (int j=0; j<nArgs; j++){ 

 bmArgs[j] = readU2(); 

 } 

 // kind of this method handle 

 int refKind = mhRefTypeAt(cpMhIdx); 

 // CONSTANT_Methodref_info structure 

 int mrefIdx = mhMethodRefIndexAt(cpMhIdx); 

 String clsName = methodClassNameAt(mrefIdx); 

 String mthName = methodNameAt(mrefIdx); 

 String descriptor = methodDescriptorAt(mrefIdx); 

 setBootstrapMethod(reader, tag, i, refKind, clsName, mthName, descriptor, bmArgs);

jpf-core/src/main/gov/nasa/jpf/jvm/JVMClassInfo.java

Lines 91 to 93 in 18a0c42

 public void setBootstrapMethod (ClassFile cf, Object tag, int idx, int refKind, String cls, String mth, String descriptor, int[] cpArgs) { 

 int lambdaRefKind = cf.mhRefTypeAt(cpArgs[1]);

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

split-package issue when compiling - JDK 10

This happens when two packages having the same name exist in different modules.

This prevents us from compiling native classes, such as the ones we have in jpf-core/src/classes

So for instance if we try to compile a class in java.lang package such as the Object.java, it will give errors like:

[javac] error: package exists in another module: java.base
[javac] package java.lang;

https://travis-ci.org/javapathfinder/jpf-core/builds/375604329#L2749-L2758

.So in order to compile them we have to patch them. To do that it requires that we explicitly mention the module that it belongs like:

javac --patch-module java.base=src -d build \
    src/java.base/java/util/concurrent/ConcurrentHashMap.java

And in jpf-core/src/classes, we got sources for multiple modules in the same tree.

classes
 +- java
    +- io
    +- lang
    +- util
       +- function
       +- logging
              +- FileHandler.java

So for ease of compilation we I’d suggest we restructure these classes based on their respective modules, like:

classes
  +- java.base
      +- java
      +- lang
           +- Object.java

  +- java.logging
      +- java
      +- util
           +- logging
              +- FileHandler.java

Then to patch these, we could do:

javac --module-source-path=src/classes -d build/classes \
       --patch-module java.base=src/classes/java.base \
       --patch-module java.logging=src/classes/java.logging

ClassInfoException when running tests - Java 10

Tests executes through JPF fails with ClassInfoException when running under Java 9/10.

Example: Running gov.nasa.jpf.test.basic.HarnessTest

[junit] gov.nasa.jpf.vm.ClassInfoException: class not found: java.io.Serializable
[junit]     at gov.nasa.jpf.vm.ClassLoaderInfo.getResolvedClassInfo(ClassLoaderInfo.java:363)
[junit]     at gov.nasa.jpf.vm.SystemClassLoaderInfo.getResolvedClassInfo(SystemClassLoaderInfo.java:147)
[junit]     at gov.nasa.jpf.vm.SystemClassLoaderInfo.loadClass(SystemClassLoaderInfo.java:182)
[junit]     at gov.nasa.jpf.vm.ClassInfo.resolveReferencedClass(ClassInfo.java:2414)
[junit]     at gov.nasa.jpf.vm.ClassInfo.loadInterfaces(ClassInfo.java:2366)
[junit]     at gov.nasa.jpf.vm.ClassInfo.resolveClass(ClassInfo.java:2383)
[junit]     at gov.nasa.jpf.vm.ClassInfo.resolveAndLink(ClassInfo.java:548)
[junit]     at gov.nasa.jpf.jvm.JVMClassInfo.<init>(JVMClassInfo.java:624)
[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.unhandledException(TestJPF.java:849)
[junit]     at gov.nasa.jpf.util.test.TestJPF.verifyUnhandledException(TestJPF.java:903)
[junit]     at gov.nasa.jpf.test.basic.HarnessTest.verifyNullPointerException(HarnessTest.java:54)

ClassInfoException is thrown in here:

jpf-core/src/main/gov/nasa/jpf/vm/ClassLoaderInfo.java

Lines 316 to 372 in 18a0c42

 /** 

  * obtain ClassInfo object for given class name 

  * 

  * if the requested class or any of its superclasses and interfaces 

  * is not found this method will throw a ClassInfoException. Loading 

  * of respective superclasses and interfaces happens recursively from here. 

  * 

  * Returned ClassInfo objects are not registered yet, i.e. still have to 

  * be added to the ClassLoaderInfo's statics, and don't have associated java.lang.Class 

  * objects until registerClass(ti) is called. 

  * 

  * Before any field or method access, the class also has to be initialized, 

  * which can include overlayed execution of &lt;clinit&gt; declaredMethods, which is done 

  * by calling initializeClass(ti,insn) 

  * 

  * this is for loading classes from the file system  

  */ 

 public ClassInfo getResolvedClassInfo (String className) throws ClassInfoException { 

 String typeName = Types.getClassNameFromTypeName( className); 

 ClassInfo ci = resolvedClasses.get( typeName); 

 if (ci == null) { 

 if (ClassInfo.isBuiltinClass( typeName)){ 

 ci = loadSystemClass( typeName); 

 } else { 

 ClassFileMatch match = getMatch( typeName); 

 if (match != null){ 

 String url = match.getClassURL(); 

 ci = loadedClasses.get( url); // have we loaded the class from this source before 

 if (ci != null){ 

 if (ci.getClassLoaderInfo() != this){ // might have been loaded by another classloader 

 ci = ci.cloneFor(this); 

 } 

 } else { 

 try { 

 log.info("loading class ", typeName, " from ", url); 

 ci = match.createClassInfo(this); 

 } catch (ClassParseException cpx){ 

 throw new ClassInfoException( "error parsing class", this, "java.lang.NoClassDefFoundError", typeName, cpx); 

 } 

 loadedClasses.put( url, ci); 

 } 

 } else { // no match found 

 throw new ClassInfoException("class not found: " + typeName, this, "java.lang.ClassNotFoundException", typeName); 

 } 

 } 

 setAttributes(ci); 

 resolvedClasses.put(typeName, ci); 

 } 

 return ci; 

 }

Possible causes

As stated in the JDK 9 Release Notes the system property sun.boot.class.path has been removed. This makes JPF to fail resolve standard Java classes.

jpf-core/src/main/gov/nasa/jpf/vm/ClassInfo.java

Lines 1676 to 1680 in 18a0c42

 // finally, we load from the standard Java libraries 

 v = System.getProperty("sun.boot.class.path"); 

 if (v != null) { 

 buf.append(v); 

 }

References
http://www.oracle.com/technetwork/java/javase/9-relnote-issues-3704069.html
https://stackoverflow.com/q/50451536/3647002

Implementation for the class URL generation would also need to be updated.

jpf-core/src/main/gov/nasa/jpf/jvm/JVMClassFileContainer.java

Lines 74 to 77 in a9bc908

 @Override 

 public String getClassURL (String typeName){ 

 return getURL() + typeName.replace('.', '/') + ".class"; 

 }

In the earlier versions path to standard class would be like:

jar:file:/path/to/jjre/lib/rt.jar!/java/lang/Object.class

With the module system:

jrt:/java.base/java/lang/Object.class

error: cannot find symbol URLClassPath

Error when running ant target -compile-classes with javac 10.0.1

[javac] src/classes/modules/java.base/jdk/internal/misc/JavaNetAccess.java:32: error: cannot find symbol
[javac]     URLClassPath getURLClassPath (URLClassLoader ucl);
[javac]     ^
[javac]   symbol:   class URLClassPath
[javac]   location: interface JavaNetAccess

https://travis-ci.org/javapathfinder/jpf-core/builds/377876039#L2755-L2759

Add minimal Gradle support to jpf-core

To kick off the migration to Gradle, the project must have a minimal Gradle support.
Concretely, this means being able to use Gradle as an interface to Ant tasks.
To this end, I need to:

Add the Gradle wrapper (currently targeting version 4.7, as it has some interesting features, including Java 10 support - https://docs.gradle.org/4.7/release-notes.html)
Import the build.xml script, so Ant tasks can be called via Gradle

error: package com.sun.org.apache.bcel.internal.generic does not exist - JDK 10

Error when build against javac 10.0.1

Error: https://travis-ci.org/javapathfinder/jpf-core/builds/371883608#L2444

Remove countStackFrames() in test

Among the many remaining compiler warnings about deprecated code, one stands out:

src/tests/gov/nasa/jpf/test/mc/basic/StackDepthCheckerTest.java:50: warning: [removal] countStackFrames() in Thread has been deprecated and marked for removal

Because this API was marked for removal, it may no longer be part of Java 11, which comes out soon.

Having the stack frame depth in the test case is actually not very important, so I think it is best to simply remove that line. The stack depth count will be off by a constant offset, but that is not important.

While cleaning up that test, I would also remove this code:
n--; // not that we ever get here System.out.print("exited foo() at level "); System.out.println(n);
and replace it with // this function never returns

Add Java Plugin to the Gradle build

The Gradle Java plugin already has common build tasks for Java/JVM project such as generating jars, compiling classes, and so on. Also, it is configurable to support jpf project layout.

More info: https://docs.gradle.org/current/userguide/tutorial_java_projects.html

IllegalAccessError: JPF_java_util_Random cannot access class jdk.internal.misc.Unsafe

Runtime error "java.lang.IllegalAccessError: class gov.nasa.jpf.vm.JPF_java_util_Random (in unnamed module) cannot access class jdk.internal.misc.Unsafe (in module java.base) because module java.base does not export jdk.internal.misc to unnamed module"

[junit] java.lang.IllegalAccessError: class gov.nasa.jpf.vm.JPF_java_util_Random (in unnamed module @0x16f7b4af) cannot access class jdk.internal.misc.Unsafe (in module java.base) because module java.base does not export jdk.internal.misc to unnamed module @0x16f7b4af
[junit]     at gov.nasa.jpf.vm.JPF_java_util_Random.<clinit>(JPF_java_util_Random.java:99)
[junit]     at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
[junit]     at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
[junit]     at java.base/jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
[junit]     at java.base/java.lang.reflect.Constructor.newInstance(Constructor.java:488)
[junit]     at gov.nasa.jpf.vm.NativePeer.getInstance(NativePeer.java:174)
[junit]     at gov.nasa.jpf.vm.NativePeer.getInstance(NativePeer.java:159)
[junit]     at gov.nasa.jpf.vm.NativePeer.getNativePeer(NativePeer.java:145)
[junit]     at gov.nasa.jpf.vm.ClassInfo.loadNativePeer(ClassInfo.java:834)
[junit]     at gov.nasa.jpf.vm.ClassInfo.resolveAndLink(ClassInfo.java:553)
[junit]     at gov.nasa.jpf.jvm.JVMClassInfo.<init>(JVMClassInfo.java:625)

UnsatisfiedLinkError: cannot find native Reflection.getCallerClass

java.lang.UnsatisfiedLinkError: cannot find native jdk.internal.reflect.Reflection.getCallerClass when running gov.nasa.jpf.test.java.concurrent.CountDownLatchTest

[junit] gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
[junit] java.lang.UnsatisfiedLinkError: cannot find native jdk.internal.reflect.Reflection.getCallerClass
[junit]     at jdk.internal.reflect.Reflection.getCallerClass(no peer)
[junit]     at java.lang.invoke.MethodHandles.lookup(MethodHandles.java:112)
[junit]     at java.util.concurrent.locks.AbstractQueuedSynchronizer.<clinit>(AbstractQueuedSynchronizer.java:2300)
[junit]     at java.util.concurrent.CountDownLatch.<init>(CountDownLatch.java:201)
[junit]     at gov.nasa.jpf.test.java.concurrent.CountDownLatchTest.testCountDown(CountDownLatchTest.java:43)
[junit]     at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
[junit]     at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

Improve verbosity level on Travis for Gradle builds

I noticed that Travis is not displaying properly the Gradle output.
This is probably due to some terminal environment on Travis.

Add test to check if the "build.properties" file is missing in jpf.jar

As discussed with @cyrille-artho, we should add a test to verify if an expected build.properties file is missing in jpf.jar file.

warning: ChoiceGeneratorBase() in ChoiceGeneratorBase has been deprecated

Compiler warning "[deprecation] ChoiceGeneratorBase() in ChoiceGeneratorBase has been deprecated" when build with JDK 9 and later.

[javac] /home/travis/build/javapathfinder/jpf-core/src/main/gov/nasa/jpf/vm/choice/PermutationCG.java:35: warning: [deprecation] ChoiceGeneratorBase() in ChoiceGeneratorBase has been deprecated
[javac]   public PermutationCG (PermutationGenerator pg){
[javac]                                                 ^

jpf-core/src/main/gov/nasa/jpf/vm/choice/PermutationCG.java

Lines 30 to 43 in 18a0c42

 public class PermutationCG extends ChoiceGeneratorBase<int[]>{ 

 protected PermutationGenerator pg; 

 protected int[] permutation; 

 public PermutationCG (PermutationGenerator pg){ 

 this.pg = pg; 

 } 

 public PermutationCG (String id, PermutationGenerator pg){ 

 super(id); 

 this.pg = pg; 

 }

Default constructor of the super class 'gov.nasa.jpf.vm.ChoiceGeneratorBase' is marked deprecated, but the constructor PermutationCG (PermutationGenerator) is not, thus resulting in the warning.

jpf-core/src/main/gov/nasa/jpf/vm/ChoiceGeneratorBase.java

Lines 99 to 110 in 18a0c42

 /** 

  * don't use this since it is not safe for cascaded ChoiceGenerators 

  * (we need the 'id' to be as context specific as possible) 

  */ 

 @Deprecated 

 protected ChoiceGeneratorBase() { 

 id = "?"; 

 } 

 protected ChoiceGeneratorBase(String id) { 

 this.id = id; 

 }

Travis log:
https://travis-ci.org/javapathfinder/jpf-core/builds/385707808#L2425-L2427

Suppress "warning: [deprecation] finalize() in Object has been deprecated"

Use an annotation to suppress the warning "warning: [deprecation] finalize() in Object has been deprecated" in src/tests/gov/nasa/jpf/test/mc/threads/FinalizerThreadTest.java:40.

For the time being, we want to keep this functionality to stay compatible with (rare) programs using finalizers. Once finalizers get removed for good (at the earliest, that would be with Java 12), and they are also removed from Android, we can remove this entire test and the JPF feature that supports finalizers.

However, in the near future, we need to keep this feature, so we just want to suppress the warning.

.travis.yml to build against Java 10

Modify .travis.yml so that it builds against Oracle Java 10 instead of Oracle Java 8. This is to support Java 10/11 and may go in a separate branch (eg. java-10)

References:
https://docs.travis-ci.com/user/getting-started/
https://github.com/javapathfinder/jpf-core/wiki/GSoC-2018-Project-Ideas#support-java-9-for-jpf-core

Errors coming with these versions jdk1.8.0_101, _102, _111.

I am using net beans for building it up with the version 101 (basic) and then the following errors encounter

jpf-core-master\src\classes\sun\misc\SharedSecrets.java:60: error: cannot find symbol
private static JavaOISAccess javaOISAccess;
symbol: class JavaOISAccess
location: class SharedSecrets
jpf-core-master\src\classes\sun\misc\SharedSecrets.java:162:
error: cannot find symbol
public static void setJavaOISAccess(JavaOISAccess access) {
symbol: class JavaOISAccess
location: class SharedSecrets
jpf-core-master\src\classes\sun\misc\SharedSecrets.java:166:
error: cannot find symbol
public static JavaOISAccess getJavaOISAccess() {
symbol: class JavaOISAccess
location: class SharedSecrets
Note: Some input files use internal proprietary API that may be removed in a future release.
Note: Recompile with -Xlint:sunapi for details.

Compile failed; see the compiler error output for details.
BUILD FAILED (total time: 18 seconds)

@jeandersonbc thanks for considering and understanding my problem.

Deprecated constructor calls with primitive argument - Xlint warnings

Several deprecation warnings are showing up on the build logs when compiled with JDK 9 and later.

[javac] /home/travis/build/javapathfinder/jpf-core/src/main/gov/nasa/jpf/vm/StackFrame.java:247: warning: [deprecation] Byte(byte) in Byte has been deprecated
[javac]           return new Byte((byte) v);
[javac]                  ^
[javac] /home/travis/build/javapathfinder/jpf-core/src/main/gov/nasa/jpf/vm/StackFrame.java:249: warning: [deprecation] Character(char) in Character has been deprecated
[javac]           return new Character((char) v);
[javac]                  ^
[javac] /home/travis/build/javapathfinder/jpf-core/src/main/gov/nasa/jpf/vm/StackFrame.java:251: warning: [deprecation] Short(short) in Short has been deprecated
[javac]           return new Short((short) v);
[javac]                  ^
[javac] /home/travis/build/javapathfinder/jpf-core/src/main/gov/nasa/jpf/vm/StackFrame.java:253: warning: [deprecation] Integer(int) in Integer has been deprecated
[javac]           return new Integer(v);
[javac]                  ^

https://travis-ci.org/javapathfinder/jpf-core/builds/379204138#L2431

Use git describe --tags instead of git hash for detailed version info

We currently use the git hash to identify the exact version, but the usual way nowadays seems to be the output of git describe --tags. Using this will be simpler and more descriptive than the git hash.

warning: [deprecation] getPackage(String) in ClassLoader has been deprecated

Deprecation warning 'getPackage(String) in ClassLoader has been deprecated' when build with JDK 9 and later:

[javac] /home/travis/build/javapathfinder/jpf-core/src/tests/gov/nasa/jpf/test/java/net/URLClassLoaderTest.java:68: warning: [deprecation] getPackage(String) in ClassLoader has been deprecated
[javac] 	protected Package getPackage(String name) {
[javac] 	                  ^
[javac] /home/travis/build/javapathfinder/jpf-core/src/tests/gov/nasa/jpf/test/java/net/URLClassLoaderTest.java:69: warning: [deprecation] getPackage(String) in ClassLoader has been deprecated
[javac]       return super.getPackage(name);
[javac]                   ^

jpf-core/src/tests/gov/nasa/jpf/test/java/net/URLClassLoaderTest.java

Lines 67 to 70 in 18a0c42

 @Override 

 protected Package getPackage(String name) { 

 return super.getPackage(name); 

 }

Travis log:
https://travis-ci.org/javapathfinder/jpf-core/builds/385707808#L2456-L2461

References:
cr.openjdk.java.net/~iris/se/10/latestSpec/api/java/lang/ClassLoader.html#getPackage(java.lang.String)

Integrate Travis

Integrate Travis CI with this GitHub repository.

add a Travis CI badge into projects README.md, to be able to see the current build status of the project.

As this being a public repository, we could use https://travis-ci.org to configure the hooks. However repository owner/organization should first enable this repository in his/her travis-ci.org profile page . So the assignee could commit the appropriate .travis.yml file.

References:
https://docs.travis-ci.com/user/getting-started/

error: cannot find symbol sun.reflect.ConstantPool

Errors when built with JDK 10.

[javac] src/classes/modules/java.base/java/lang/Class.java:35: error: cannot find symbol
[javac] import sun.reflect.ConstantPool;
[javac]                   ^
[javac]   symbol:   class ConstantPool
[javac]   location: package sun.reflect


[javac] src/classes/modules/java.base/java/lang/Class.java:274: error: cannot find symbol
[javac]   native ConstantPool getConstantPool();
[javac]          ^
[javac]   symbol:   class ConstantPool
[javac]   location: class Class<T>
[javac]   where T is a type-variable:
[javac]     T extends Object declared in class Class


[javac]   location: package sun.misc
[javac] src/classes/modules/java.base/java/lang/System.java:29: error: cannot find symbol
[javac] import sun.reflect.ConstantPool;
[javac]                   ^
[javac]   symbol:   class ConstantPool
[javac]   location: package sun.reflect

https://travis-ci.org/javapathfinder/jpf-core/builds/375815945#L2748-L2751

overrides equals, but neither it nor any superclass overrides hashCode method

Several compiler warnings

"Class * overrides equals, but neither it nor any superclass overrides hashCode method"

when build with JDK 9 and later.

[javac] /home/travis/build/javapathfinder/jpf-core/src/tests/TypeNameTest.java:31: warning: [overrides] Class B overrides equals, but neither it nor any superclass overrides hashCode method
[javac] class B {
[javac] ^
[javac] /home/travis/build/javapathfinder/jpf-core/src/tests/gov/nasa/jpf/test/mc/data/CGCreatorFactoryTest.java:44: warning: [overrides] Class CGCreatorFactoryTest.B overrides equals, but neither it nor any superclass overrides hashCode method
[javac]   class B {
[javac]   ^

Travis log:
https://travis-ci.org/javapathfinder/jpf-core/builds/392100916#L2453-L2477

Download links are missing

This page does not link to the correct place for downloading binaries - https://github.com/javapathfinder/jpf-core/wiki/Downloading-binary-snapshots

Binaries seem to actually be here: https://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-core#no1

Current build fails...

So I have tried to follow the instructions for installing and building from source on the Wiki, but it doesn't work for me.

I am on Mac OS X and Oracle JDK 8.

My steps:

mkdir ~/code/jpf
cd ~/code/jpf
git clone https://github.com/javapathfinder/jpf-core.git
mkdir ~/.jpf

cat <<EOF >> ~/.jpf/site.properties
# JPF site configuration
jpf-core = ${user.home}/code/jpf/jpf-core
# numeric extension
jpf-numeric = ${user.home}/code/jpf/jpf-numeric
# annotation-based program properties extension
jpf-aprop = ${user.home}/code/jpf/jpf-aprop
extensions=${jpf-core},${jpf-aprop}
#... and all your other installed projects
EOF

cd ~/code/jpf/jpf-core
ant test

I then get these errors from Ant:

-compile-classes:
    [mkdir] Created dir: /Users/aretter/code/jpf/jpf-core/build/classes
    [javac] Compiling 84 source files to /Users/aretter/code/jpf/jpf-core/build/classes
    [javac] /Users/aretter/code/jpf/jpf-core/src/classes/sun/misc/SharedSecrets.java:61: error: cannot find symbol
    [javac]   private static JavaObjectInputStreamAccess javaObjectInputStreamAccess;
    [javac]                  ^
    [javac]   symbol:   class JavaObjectInputStreamAccess
    [javac]   location: class SharedSecrets
    [javac] /Users/aretter/code/jpf/jpf-core/src/classes/sun/misc/SharedSecrets.java:142: error: cannot find symbol
    [javac]   public static JavaObjectInputStreamAccess getJavaObjectInputStreamAccess() {
    [javac]                 ^
    [javac]   symbol:   class JavaObjectInputStreamAccess
    [javac]   location: class SharedSecrets
    [javac] /Users/aretter/code/jpf/jpf-core/src/classes/sun/misc/SharedSecrets.java:151: error: cannot find symbol
    [javac]   public static void setJavaObjectInputStreamAccess(JavaObjectInputStreamAccess access) {
    [javac]                                                     ^
    [javac]   symbol:   class JavaObjectInputStreamAccess
    [javac]   location: class SharedSecrets
    [javac] Note: Some input files use internal proprietary API that may be removed in a future release.
    [javac] Note: Recompile with -Xlint:sunapi for details.
    [javac] 3 errors

Seems like there are some source files missing?

jpf to promela

Is there a way to extract a promela file after the code is verified?

Missing build.properties file

The compile task from the Gradle build is not copying the build.properties file to the build directory like the Ant build does here: https://github.com/javapathfinder/jpf-core/blob/master/build.xml#L84

NoSuchMethodException:SharedSecrets.setJavaNetURLAccess(Ljdk/internal/misc/JavaNetURLAccess;)V

Runtime error "java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaNetURLAccess(Ljdk/internal/misc/JavaNetURLAccess;)V" when running ClassLoaderTest.

[junit] java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaNetURLAccess(Ljdk/internal/misc/JavaNetURLAccess;)V
[junit]     at java.net.URL.<clinit>(URL.java:1632)
[junit]     at java.lang.ClassLoader.getResource(ClassLoader.java:62)
[junit]     at java.lang.ClassLoader.getResource(ClassLoader.java:67)
[junit]     at java.lang.ClassLoader.getResourceAsStream(ClassLoader.java:131)
[junit]     at gov.nasa.jpf.test.java.lang.ClassLoaderTest.testGetResourceAsStreamImpl(ClassLoaderTest.java:164)
[junit]     at gov.nasa.jpf.test.java.lang.ClassLoaderTest.testGetResourceAsStream(ClassLoaderTest.java:51)
[junit]     at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
[junit]     at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

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

Following compiler warning shows up in the build logs:

[javac] src/classes/modules/java.base/java/lang/ClassLoader.java:112: warning: auxiliary class CompoundEnumeration in ClassLoader.java should not be accessed from outside its own source file
[javac]     return new CompoundEnumeration<URL>(resEnum);
[javac]                ^

Travis log:
https://travis-ci.org/javapathfinder/jpf-core/builds/393023635#L2444-L2446

error: cannot find symbol sun.misc.CompoundEnumeration

Error when built with javac 10.0.1

[javac] classes/modules/java.base/java/lang/ClassLoader.java:29: error: cannot find symbol
[javac] import sun.misc.CompoundEnumeration;
[javac]                ^
[javac]   symbol:   class CompoundEnumeration
[javac]   location: package sun.misc

https://travis-ci.org/javapathfinder/jpf-core/builds/375815945#L2753-L2757

Errors due to JEP 254: Compact Strings

Building jpf-core against Java 9 or later would result in following errors due to the implementation changes made to String and related classes in JEP 254

[javac] src/classes/modules/java.base/java/lang/String.java:132: error: incompatible types: Result cannot be converted to char[]
[javac] 		this.value =  StringCoding.decode(cset, x, offset, length);
[javac] 		                                 ^

[javac] src/classes/modules/java.base/java/lang/String.java:160: error: incompatible types: byte[] cannot be converted to char[]
[javac] 			this.value = Arrays.copyOf(x.getValue(), x.length());
[javac] 			                          ^

[javac] src/classes/modules/java.base/java/lang/String.java:166: error: incompatible types: byte[] cannot be converted to char[]
[javac] 		this.value = Arrays.copyOf(x.getValue(), x.length());
[javac] 		                          ^

[javac] src/classes/modules/java.base/java/lang/String.java:205: error: no suitable method found for encode(Charset,char[],int,int)
[javac] 		return StringCoding.encode(x, value, 0, value.length);
[javac] 		                   ^
[javac]     method StringCoding.encode(String,byte,byte[]) is not applicable
[javac]       (actual and formal argument lists differ in length)
[javac]     method StringCoding.encode(Charset,byte,byte[]) is not applicable
[javac]       (actual and formal argument lists differ in length)
[javac]     method StringCoding.encode(byte,byte[]) is not applicable
[javac]       (actual and formal argument lists differ in length)

[javac] src/classes/modules/java.base/java/lang/String.java:236: error: incompatible types: byte[] cannot be converted to char[]
[javac]       return equals0( value,  ((AbstractStringBuilder) charSequence).getValue(), value.length);
[javac]                                                                              ^

https://travis-ci.org/javapathfinder/jpf-core/builds/375815945#L2770-L2790

Add missing buildinfo task on Gradle build

Gradle script is missing the buildinfo task and must be ported from the Ant build.

Fails to handle native calls to jdk.internal.misc.Unsafe - Java 10

NoSuchMethodError, and UnsatisfiedLinkError exceptions are thrown while running tests under Java 10

NoSuchMethodError

[junit] gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
[junit] java.lang.NoSuchMethodError: jdk.internal.misc.Unsafe.objectFieldOffset(Ljava/lang/Class;Ljava/lang/String;)J
[junit]     at java.util.concurrent.ConcurrentHashMap.<clinit>(ConcurrentHashMap.java:6377)
[junit]     at java.util.Properties.<init>(Properties.java:201)
[junit]     at java.util.Properties.<init>(Properties.java:168)
[junit]     at java.lang.System.<clinit>(System.java:46)

UnsatisfiedLinkError

[junit] gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
[junit] java.lang.UnsatisfiedLinkError: cannot find native jdk.internal.misc.Unsafe.objectFieldOffset
[junit]     at jdk.internal.misc.Unsafe.objectFieldOffset(gov.nasa.jpf.vm.JPF_jdk_internal_misc_Unsafe)
[junit]     at java.util.concurrent.ConcurrentHashMap.<clinit>(ConcurrentHashMap.java:6377)
[junit]     at java.util.Properties.<init>(Properties.java:201)
[junit]     at java.util.Properties.<init>(Properties.java:168)
[junit]     at java.lang.System.<clinit>(System.java:46)

Exceptions are thrown for the following methods:

public native long objectFieldOffset(Class<?> c, String name);
public final native boolean compareAndSetInt(Object o, long offset, int expected, int x);
public final native boolean compareAndSetLong(Object o, long offset, long expected, long x);
public final native boolean compareAndSetObject(Object o, long offset, Object expected, Object x);
public final native Object getObjectAcquire(Object o, long offset);

Proposed solution:

These two exceptions can be fixed by adding the missing methods in the Unsafe model class and their corresponding native peer methods (in JPF_jdk_internal_misc_Unsafe) subsequently.

error: javac: invalid flag: --sunapi

It seems that sunapi Xlint flag is being removed in JDK 9 and later. Thus result in the build error:

[javac] javac: invalid flag: -Xlint:all,-sunapi,-serial

https://travis-ci.org/javapathfinder/jpf-core/builds/375542872#L2716

References:
https://stackoverflow.com/questions/49134837/javac-invalid-flag-xlint-sunapi-jdk-9

warning: Unsafe is internal proprietary API

Compiler warning 'Unsafe is internal proprietary API and may be removed in a future release' when build with JDK 9 and later:

[javac] /home/travis/build/javapathfinder/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:32: warning: Unsafe is internal proprietary API and may be removed in a future release
[javac] import sun.misc.Unsafe;
[javac]                ^
[javac] /home/travis/build/javapathfinder/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:93: warning: Unsafe is internal proprietary API and may be removed in a future release
[javac]   private static Unsafe unsafe;
[javac]                  ^
[javac] /home/travis/build/javapathfinder/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:99: warning: Unsafe is internal proprietary API and may be removed in a future release
[javac]       Field singletonField = Unsafe.class.getDeclaredField("theUnsafe");
[javac]                              ^
[javac] /home/travis/build/javapathfinder/jpf-core/src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.java:101: warning: Unsafe is internal proprietary API and may be removed in a future release

Travis log:
https://travis-ci.org/javapathfinder/jpf-core/builds/385057883#L2471-L2483

warning: [deprecation] newInstance() in Class has been deprecated

Several compiler warnings saying 'newInstance() in Class has been deprecated' appeared in build logs when compiled with JDK 9 and later,

[javac] /home/travis/build/javapathfinder/jpf-core/src/main/gov/nasa/jpf/vm/ClassInfo.java:402: warning: [deprecation] newInstance() in Class has been deprecated
[javac]             Object attr = attrCls.newInstance(); // needs to have a default ctor
[javac]                                  ^
[javac]   where T is a type-variable:
[javac]     T extends Object declared in class Class

[javac] /home/travis/build/javapathfinder/jpf-core/src/main/gov/nasa/jpf/listener/PathOutputMonitor.java:242: warning: [deprecation] newInstance() in Class has been deprecated
[javac]       return psClass.newInstance();
[javac]                     ^
[javac]   where T is a type-variable:
[javac]     T extends Object declared in class Class

Travis log:
https://travis-ci.org/javapathfinder/jpf-core/builds/384672396#L2431-L2444

warning: Reflection is internal proprietary API and may be removed

Deprecation warning

'Reflection is internal proprietary API and may be removed in a future release'

when build with JDK 9 and later:

[javac] /home/travis/build/javapathfinder/jpf-core/src/tests/gov/nasa/jpf/test/vm/reflection/ReflectionTest.java:34: warning: Reflection is internal proprietary API and may be removed in a future release
[javac]       Class<?> callerCls = sun.reflect.Reflection.getCallerClass(0); // that would be getCallerClass()
[javac]                                       ^

Travis log:
https://travis-ci.org/javapathfinder/jpf-core/builds/389306467#L2485-L2508

References:
https://www.logicbig.com/tutorials/core-java-tutorial/java-9-changes/stack-walker-caller.html

NoSuchMethodException: SharedSecrets.setJavaObjectInputFilterAccess(Ljdk/internal/misc/JavaObjectInputFilterAccess;)V

Runtime error "java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaObjectInputFilterAccess(Ljdk/internal/misc/JavaObjectInputFilterAccess;)V" when running ObjectStreamTest.

[junit] java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaObjectInputFilterAccess(Ljdk/internal/misc/JavaObjectInputFilterAccess;)V
[junit]     at java.io.ObjectInputFilter$Config.<clinit>(ObjectInputFilter.java:271)
[junit]     at java.io.ObjectInputStream.<init>(ObjectInputStream.java:340)
[junit]     at gov.nasa.jpf.test.java.io.ObjectStreamTest.testSimpleReadbackOk(ObjectStreamTest.java:88)
[junit]     at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
[junit]     at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

Add support to Jar tasks on Gradle Build

The current Gradle support covers all original compilation tasks and test execution.
Another important task that must be covered, and it is between compile and test is the build task.
The build task is responsible for generating some important jars.

Improve .gitignore

These files appear on my git status as untracked files .

modified:   .idea/misc.xml
modified:   .idea/vcs.xml
Untracked files:
  (use "git add <file>..." to include in what will be committed)
        .idea/ant.xml

It will be convenient if it ignores all the auto-generated and IDE specific files.

error: cannot find symbol sun.misc.SharedSecrets - JDK 10

Error when build against javac 10.0.1

Error: https://travis-ci.org/javapathfinder/jpf-core/builds/372327507#L2447-L2458

Proposed solutions:

Use StackWalker instread of sun.misc.SharedSecrets, as done previously: gayanW@4852566
Use SharedSecrets from the repackaged jdk.internal.misc package. This will also require us to break the encapsulation by passing command line arguments to the compiler.

References:
http://openjdk.java.net/jeps/261#Breaking-encapsulation

error: cannot find symbol sun.misc.JavaLangAccess

Errors when built with javac 10.0.1

[javac] src/classes/modules/java.base/java/lang/System.java:26: error: cannot find symbol
[javac] import sun.misc.JavaLangAccess;
[javac]                ^
[javac]   symbol:   class JavaLangAccess
[javac]   location: package sun.misc


[javac] src/classes/modules/java.base/java/lang/System.java:68: error: cannot find symbol
[javac]   static JavaLangAccess createJavaLangAccess () {
[javac]          ^
[javac]   symbol:   class JavaLangAccess
[javac]   location: class System


[javac] src/classes/modules/java.base/java/lang/System.java:69: error: cannot find symbol
[javac]     return new JavaLangAccess(){
[javac]                ^
[javac]   symbol:   class JavaLangAccess
[javac]   location: class System

https://travis-ci.org/javapathfinder/jpf-core/builds/375815945#L2791-L2795

building jpf

Building jpf with docker

docker run -v <absolute_path_to_jpfcore>:/var/data -w /var/data --name jpfcore frekele/ant:1.10.1-jdk8u121 ant

Download and install jpf-core : Link Dead

https://github.com/javapathfinder/jpf-core/wiki/NetBeans-Plugin

Download and install jpf-core, the link is dead, can you please update it?
If they aren't working then please delete them coz they are misleading to a 404 error page.

Add all tests for execution on the Gradle build

There is a known issue on the Gradle build, as highlighted in the issue #46 (pull request #52) .
Some tests are failing in the Gradle build due to the incomplete support of the build cycle.
As a temporary fix, I ignored those tests (./failing-tests.txt) on the Gradle build to keep Travis green.
However, those tests must be fully supported.

error: cannot find symbol sun.misc.SharedSecrets

Errors when built with javac 10.0.1

[javac] src/classes/modules/java.base/sun/reflect/annotation/AnnotationType.java:28: error: cannot find symbol
[javac] import sun.misc.SharedSecrets;
[javac]                ^
[javac]   symbol:   class SharedSecrets
[javac]   location: package sun.misc

[javac] src/classes/modules/java.base/java/lang/System.java:27: error: cannot find symbol
[javac] import sun.misc.SharedSecrets;
[javac]                ^
[javac]   symbol:   class SharedSecrets
[javac]   location: package sun.misc

[javac] src/classes/modules/java.base/sun/reflect/annotation/AnnotationType.java:52: error: cannot find [javac]     AnnotationType at = SharedSecrets.getJavaLangAccess().getAnnotationType(annotationClass);
[javac]                         ^
[javac]   symbol:   variable SharedSecrets
[javac]   location: class AnnotationType

[javac] src/classes/modules/java.base/sun/reflect/annotation/AnnotationType.java:97: error: cannot find symbol
[javac]     SharedSecrets.getJavaLangAccess().setAnnotationType(annoCls, this);
[javac]     ^
[javac]   symbol:   variable SharedSecrets
[javac]   location: class AnnotationType

[javac] src/classes/modules/java.base/java/lang/System.java:61: error: cannot find symbol
[javac]     SharedSecrets.setJavaLangAccess( createJavaLangAccess());
[javac]     ^
[javac]   symbol:   variable SharedSecrets
[javac]   location: class System

https://travis-ci.org/javapathfinder/jpf-core/builds/375815945#L2748-L2751

Repository clean up & Refactoring of Gradle Build Script

We should get rid of unnecessary files to keep the repository organized and clean up the Gradle build script before merging into master.

error: cannot find symbol JavaOISAccess

Error when running ant target -compile-classes with javac 10.0.1

[javac] src/classes/modules/java.base/jdk/internal/misc/SharedSecrets.java:60: error: cannot find symbol
[javac]   private static JavaOISAccess javaOISAccess;
[javac]                  ^
[javac]   symbol:   class JavaOISAccess
[javac]   location: class SharedSecrets


[javac] src/classes/modules/java.base/jdk/internal/misc/SharedSecrets.java:162: error: cannot find symbol
[javac]   public static void setJavaOISAccess(JavaOISAccess access) {
[javac]                                       ^
[javac]   symbol:   class JavaOISAccess
[javac]   location: class SharedSecrets


[javac] src/classes/modules/java.base/jdk/internal/misc/SharedSecrets.java:166: error: cannot find symbol
[javac]   public static JavaOISAccess getJavaOISAccess() {
[javac]                 ^
[javac]   symbol:   class JavaOISAccess
[javac]   location: class SharedSecrets

https://travis-ci.org/javapathfinder/jpf-core/builds/376327343#L2748-L2762

Add missing packaging build tasks on Gradle build

The Gradle build script is missing the tasks dist and src-dist

UnsatisfiedLinkError: cannot find native jdk.internal.reflect.Reflection.getClassAccessFlags

Runtime error "java.lang.UnsatisfiedLinkError: cannot find native jdk.internal.reflect.Reflection.getClassAccessFlags" when running CountDownLatchTest

[junit] java.lang.UnsatisfiedLinkError: cannot find native jdk.internal.reflect.Reflection.getClassAccessFlags
[junit]     at jdk.internal.reflect.Reflection.getClassAccessFlags(gov.nasa.jpf.vm.JPF_jdk_internal_reflect_Reflection)
[junit]     at sun.invoke.util.VerifyAccess.getClassModifiers(VerifyAccess.java:156)
[junit]     at sun.invoke.util.VerifyAccess.isClassAccessible(VerifyAccess.java:177)
[junit]     at java.lang.invoke.MethodHandles$Lookup.checkSymbolicClass(MethodHandles.java:2047)
[junit]     at java.lang.invoke.MethodHandles$Lookup.resolveOrFail(MethodHandles.java:2020)
[junit]     at java.lang.invoke.MethodHandles$Lookup.findVarHandle(MethodHandles.java:1516)
[junit]     at java.util.concurrent.locks.AbstractQueuedSynchronizer.<clinit>(AbstractQueuedSynchronizer.java:2301)
[junit]     at java.util.concurrent.CountDownLatch.<init>(CountDownLatch.java:201)
[junit]     at gov.nasa.jpf.test.java.concurrent.CountDownLatchTest.testCountDown(CountDownLatchTest.java:43)

The above error follows after the PR #104

	/**
	* BootstrapMethods_attribute {
	* u2 attribute_name_index;
	* u4 attribute_length;
	* u2 num_bootstrap_methods;
	* { u2 bootstrap_method_ref; -> MethodHandle
	* u2 num_bootstrap_arguments;
	* u2 bootstrap_arguments[num_bootstrap_arguments];
	* } bootstrap_methods[num_bootstrap_methods];
	* }
	*
	* pos is at num_bootstrap_methods
	*/
	public void parseBootstrapMethodAttr (ClassFileReader reader, Object tag){
	int nBootstrapMethods = readU2();

	setBootstrapMethodCount(reader, tag, nBootstrapMethods);

	for (int i=0; i<nBootstrapMethods; i++){
	int cpMhIdx = readU2();
	int nArgs = readU2();
	int[] bmArgs = new int[nArgs];
	for (int j=0; j<nArgs; j++){
	bmArgs[j] = readU2();
	}

	// kind of this method handle
	int refKind = mhRefTypeAt(cpMhIdx);

	// CONSTANT_Methodref_info structure
	int mrefIdx = mhMethodRefIndexAt(cpMhIdx);

	String clsName = methodClassNameAt(mrefIdx);
	String mthName = methodNameAt(mrefIdx);
	String descriptor = methodDescriptorAt(mrefIdx);

	setBootstrapMethod(reader, tag, i, refKind, clsName, mthName, descriptor, bmArgs);

	public void setBootstrapMethod (ClassFile cf, Object tag, int idx, int refKind, String cls, String mth, String descriptor, int[] cpArgs) {

	int lambdaRefKind = cf.mhRefTypeAt(cpArgs[1]);

	/**
	* obtain ClassInfo object for given class name
	*
	* if the requested class or any of its superclasses and interfaces
	* is not found this method will throw a ClassInfoException. Loading
	* of respective superclasses and interfaces happens recursively from here.
	*
	* Returned ClassInfo objects are not registered yet, i.e. still have to
	* be added to the ClassLoaderInfo's statics, and don't have associated java.lang.Class
	* objects until registerClass(ti) is called.
	*
	* Before any field or method access, the class also has to be initialized,
	* which can include overlayed execution of <clinit> declaredMethods, which is done
	* by calling initializeClass(ti,insn)
	*
	* this is for loading classes from the file system
	*/
	public ClassInfo getResolvedClassInfo (String className) throws ClassInfoException {
	String typeName = Types.getClassNameFromTypeName( className);

	ClassInfo ci = resolvedClasses.get( typeName);
	if (ci == null) {
	if (ClassInfo.isBuiltinClass( typeName)){
	ci = loadSystemClass( typeName);

	} else {
	ClassFileMatch match = getMatch( typeName);
	if (match != null){
	String url = match.getClassURL();
	ci = loadedClasses.get( url); // have we loaded the class from this source before
	if (ci != null){
	if (ci.getClassLoaderInfo() != this){ // might have been loaded by another classloader
	ci = ci.cloneFor(this);
	}
	} else {
	try {
	log.info("loading class ", typeName, " from ", url);
	ci = match.createClassInfo(this);

	} catch (ClassParseException cpx){
	throw new ClassInfoException( "error parsing class", this, "java.lang.NoClassDefFoundError", typeName, cpx);
	}

	loadedClasses.put( url, ci);
	}

	} else { // no match found
	throw new ClassInfoException("class not found: " + typeName, this, "java.lang.ClassNotFoundException", typeName);
	}
	}

	setAttributes(ci);
	resolvedClasses.put(typeName, ci);
	}

	return ci;
	}

	// finally, we load from the standard Java libraries
	v = System.getProperty("sun.boot.class.path");
	if (v != null) {
	buf.append(v);
	}

	@Override
	public String getClassURL (String typeName){
	return getURL() + typeName.replace('.', '/') + ".class";
	}

	public class PermutationCG extends ChoiceGeneratorBase<int[]>{

	protected PermutationGenerator pg;
	protected int[] permutation;

	public PermutationCG (PermutationGenerator pg){
	this.pg = pg;
	}

	public PermutationCG (String id, PermutationGenerator pg){
	super(id);
	this.pg = pg;
	}

	/**
	* don't use this since it is not safe for cascaded ChoiceGenerators
	* (we need the 'id' to be as context specific as possible)
	*/
	@Deprecated
	protected ChoiceGeneratorBase() {
	id = "?";
	}

	protected ChoiceGeneratorBase(String id) {
	this.id = id;
	}

	@Override
	protected Package getPackage(String name) {
	return super.getPackage(name);
	}