NullPointerException in `java.util.jar.JarFile.getEntry0` method about jpf-core HOT 5 OPEN

Update:

I have added some native peer methods in gov.nasa.jpf.vm.JPF_java_util_zip_ZipFile peer class so we can allow host JVM to handle methods of ZipFile class. By adding this, I got object of ZipEntry class. Now I am not getting NullPointerException, but I am not able to cast this ZipEntry object into JarEntry object. Here is the stack trace of error:

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ClassCastException: java.util.zip.ZipEntry cannot be cast to java.util.jar.JarEntry
	at java.util.zip.ZipFile$1.getEntry(ZipFile.java:161)
	at java.util.jar.JarFile.getEntry0(JarFile.java:584)
	at java.util.jar.JarFile.getManEntry(JarFile.java:946)
	at java.util.jar.JarFile.getManifestFromReference(JarFile.java:416)
	at java.util.jar.JarFile.getManifest(JarFile.java:408)
	at com.example.JarReader.main(JarReader.java:24)

from jpf-core.

I think the object should be returned as an instance of JarEntry rather than ZipEntry, so the cast to the subclass (JarEntry) succeeds.

from jpf-core.

Update:

I have added some native peer methods in gov.nasa.jpf.vm.JPF_java_util_zip_ZipFile peer class so we can allow host JVM to handle methods of ZipFile class. By adding this, I got object of ZipEntry class. Now I am not getting NullPointerException, but I am not able to cast this ZipEntry object into JarEntry object. Here is the stack trace of error:

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ClassCastException: java.util.zip.ZipEntry cannot be cast to java.util.jar.JarEntry
	at java.util.zip.ZipFile$1.getEntry(ZipFile.java:161)
	at java.util.jar.JarFile.getEntry0(JarFile.java:584)
	at java.util.jar.JarFile.getManEntry(JarFile.java:946)
	at java.util.jar.JarFile.getManifestFromReference(JarFile.java:416)
	at java.util.jar.JarFile.getManifest(JarFile.java:408)
	at com.example.JarReader.main(JarReader.java:24)

@pparizek @cyrille-artho I found a reason for this error.
Please look at this implementation of native peer for getEntry method of ZipFile class:

@MJI
  public int getEntry__Ljava_lang_String_2Ljava_util_function_Function_2__Ljava_util_zip_ZipEntry_2(MJIEnv env, int thisRef, int entryNameRef, int funcRef) {
    ZipFileProxy zfp = getZFP(env, thisRef);
    if (zfp == null) {
      return MJIEnv.NULL;
    }
    String name = env.getStringObject(entryNameRef);
    ZipEntry entry = zfp.zf.getEntry(name);
    if (entry == null) {
      return MJIEnv.NULL;
    }

    return createZipEntryObject(env, entry);

in this method I am calling getEntry(String) which will return object of ZipEntry but I have to call getEntry(String,Function) so we can get object of any class which is extending ZipEntry based on a function we are passing and due to this we were getting ClassCastException.

from jpf-core.

Now my question is, can we somehow get the object of the Function class from the funcRef variable?

from jpf-core.

There are ways to get the application-level objects that correspond to the descriptors (int values) at the JPF-native level. See JPF_java_lang_reflect_Constructor.getMethodInfo. However, it looks like you want to call the function instead? Would code such as the one in class JPF_gov_nasa_jpf_SerializationConstructor.java, method newInstance___3Ljava_lang_Object_2__Ljava_lang_Object_2 work for you (if you adapt it to your circumstance; in that method, a coonstructor is called, so a call on an existing instance is a bit different).

from jpf-core.