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.
The model class implements toURI, but this function was not tested with a unit test. We therefore need a unit test and then a fix.
Create a unit test that constructs a simple URI from a File with a String that has the right URI syntax.
Look into ways to obtain a working URI by fixing a dependency in the JPF model classes, most likely by adding setJavaNetURIAccess, which is probably going to resemble setJavaNetURLAccess.
Also look into the class description JavaDoc of src/classes/modules/java.base/jdk/internal/misc/SharedSecrets, which still refers to Java 1.5/Java 6 and is therefore seriously outdated.
If the model class for SharedSecrets can indeed be removed, we want a careful review of its use of Unsafe and whether removal might cause problems later.
The model class implements
toURI, but this function was not tested with a unit test. We therefore need a unit test and then a fix.Create a unit test that constructs a simple
URIfrom aFilewith aStringthat has the right URI syntax.Look into ways to obtain a working URI by fixing a dependency in the JPF model classes, most likely by adding
setJavaNetURIAccess, which is probably going to resemblesetJavaNetURLAccess.Also look into the class description JavaDoc of
src/classes/modules/java.base/jdk/internal/misc/SharedSecrets, which still refers to Java 1.5/Java 6 and is therefore seriously outdated.If the model class for
SharedSecretscan indeed be removed, we want a careful review of its use ofUnsafeand whether removal might cause problems later.