Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

java.net.URI.toURI broken #460

Merged
merged 4 commits into from
Jun 7, 2024
Merged

Conversation

Harsh4902
Copy link
Contributor

@Harsh4902 Harsh4902 commented Jun 3, 2024

@Harsh4902
Copy link
Contributor Author

@cyrille-artho please review this PR.

Copy link
Member

@cyrille-artho cyrille-artho left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good job!
As this test will fail without a fix in jpf-core, let's wait with merging the PR until Part 2 (the fix) is also ready.

src/tests/gov/nasa/jpf/test/java/io/FileTest.java Outdated Show resolved Hide resolved
@cyrille-artho
Copy link
Member

Thanks for the update. This test is a good way to verify an upcoming fix of toURI. Once you have a fix for toURI, we can merge the PR.

@Harsh4902
Copy link
Contributor Author

@cyrille-artho what should be the standard output of toURI method based on our use case in modbat?

@cyrille-artho
Copy link
Member

We always use the regular JVM as a baseline. In this case, your test may fail because toURI seems to include the absolute path in the filename. Try to adapt the test case so that the assertion holds when you execute it on the regular JVM (without JPF), as we want the behavior under JPF to be equivalent.

output.txt Outdated Show resolved Hide resolved
Copy link
Member

@cyrille-artho cyrille-artho left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You seem to have accidentally included an extra file.

@cyrille-artho
Copy link
Member

Strange that the test passes while a simple program using toURI fails with JPF:
With this being Test.java:

import java.io.*;

public class Test {
  public final static void main(String[] args) throws Exception {
    File f = new File("test");
    System.out.println(f.toURI().toURL());
  }

I have run this with jpf +classpath=. Test and get the following:

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaNetUriAccess(Ljdk/internal/misc/JavaNetUriAccess;)V
	at java.net.URI.<clinit>(URI.java:3626)
	at java.io.File.toURI(File.java:131)
	at Test.main(Test.java:6)

@cyrille-artho
Copy link
Member

Make sure the tests run on JPF, not the host JVM:
https://github.com/javapathfinder/jpf-core/wiki/Writing-JPF-tests

@Harsh4902
Copy link
Contributor Author

@cyrille-artho Please review it. Hopefully its resolved now.

@cyrille-artho cyrille-artho merged commit 0916082 into javapathfinder:master Jun 7, 2024
2 checks passed
@cyrille-artho
Copy link
Member

Thanks, looks good!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants