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.

Sign up for GitHub

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

Jump to bottom

test-verify and test-dist-long Ant targets both fail #905

Closed
ahelwer opened this issue Apr 10, 2024 · 4 comments
Closed

test-verify and test-dist-long Ant targets both fail #905

ahelwer opened this issue Apr 10, 2024 · 4 comments
Labels
DevEnvironment Everything related to the Toolbox development environment help wanted We need your help Tools The command line tools - TLC, SANY, ...

Comments

@ahelwer
Copy link
Contributor

ahelwer commented Apr 10, 2024 •
edited
Loading

These don't appear to be checked in any CI so it isn't surprising that they've started failing. Should they be fixed or just removed from the Ant build file? The benchmark target still works but I won't be surprised if that starts failing eventually since it isn't being exercised in the CI anymore.

test-verify error:

ant -f tlatools/org.lamport.tlatools/customBuild.xml test-verify
Buildfile: /home/ahelwer/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/customBuild.xml

test-verify:
    [junit] Running tlc2.tool.fp.OffHeapDiskFPSetJPFTest
    [junit] Tests run: 1, Failures: 1, Errors: 0, Skipped: 0, Time elapsed: 0.093 sec
    [junit] Test tlc2.tool.fp.OffHeapDiskFPSetJPFTest FAILED
    [junit] Running tlc2.tool.queue.StateQueueJPFTest
    [junit] Tests run: 1, Failures: 1, Errors: 0, Skipped: 0, Time elapsed: 0.098 sec
    [junit] Test tlc2.tool.queue.StateQueueJPFTest FAILED

BUILD SUCCESSFUL
Total time: 0 seconds

test-dist-long error:

ant -f tlatools/org.lamport.tlatools/customBuild.xml test-dist-long
Buildfile: /home/ahelwer/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/customBuild.xml

test-dist-long:
    [javac] Compiling 8 source files to /home/ahelwer/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/test-class
    [javac] /home/ahelwer/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java:47: error: cannot find symbol
    [javac] import tlc2.tool.WorkerMonitor;
    [javac]                 ^
    [javac]   symbol:   class WorkerMonitor
    [javac]   location: package tlc2.tool
    [javac] /home/ahelwer/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java:157: error: package WorkerMonitor does not exist
    [javac] 		WorkerMonitor.addThreadListener(new WorkerMonitor.ThreadListener() {
    [javac] 		                                                 ^
    [javac] /home/ahelwer/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java:157: error: cannot find symbol
    [javac] 		WorkerMonitor.addThreadListener(new WorkerMonitor.ThreadListener() {
    [javac] 		^
    [javac]   symbol:   variable WorkerMonitor
    [javac]   location: class MultiThreadedSpecTest
    [javac] Note: /home/ahelwer/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java uses or overrides a deprecated API.
    [javac] Note: Recompile with -Xlint:deprecation for details.
    [javac] 3 errors

BUILD FAILED
/home/ahelwer/src/tlaplus/java-tools/tlatools/org.lamport.tlatools/customBuild.xml:1086: Compile failed; see the compiler error output for details.

Total time: 0 seconds
@lemmy lemmy added Tools The command line tools - TLC, SANY, ... DevEnvironment Everything related to the Toolbox development environment labels May 8, 2024
@lemmy
Copy link
Member

lemmy commented May 8, 2024

Re test-verify: My money is on a JPF incompatibility (sun/misc/SharedSecrets) with newer versions of Java:

  <testcase classname="tlc2.tool.fp.OffHeapDiskFPSetJPFTest" name="test" time="0.033">
    <failure message="JPF internal exception executing: +listener=.listener.AssertionProperty,.listener.ErrorTraceGenerator :gov.nasa.jpf.JPF$ExitException: JPF configuration error: error instantiating class gov.nasa.jpf.vm.OVHeap for entry &quot;vm.heap.class&quot;:&#xa;&gt; exception in gov.nasa.jpf.vm.OVHeap(gov.nasa.jpf.Config,gov.nasa.jpf.
vm.KernelState):&#xa;&gt;&gt; java.lang.NoClassDefFoundError: sun/misc/SharedSecrets&#xa;&gt; used within &quot;vm.class&quot; instantiation of class gov.nasa.jpf.vm.SingleProcessVM" type="junit.framework.AssertionFailedError">junit.framework.AssertionFailedError: JPF internal exception executing: +listener=.listener.AssertionProperty,.listener.ErrorTraceGenerator :gov.nasa.jpf.JPF$ExitException: JPF configuration error: error instantiating class gov.nasa.jpf.vm.OVHeap for entry &quot;vm.heap.class&quot;:
&gt; exception in gov.nasa.jpf.vm.OVHeap(gov.nasa.jpf.Config,gov.nasa.jpf.vm.KernelState):
&gt;&gt; java.lang.NoClassDefFoundError: sun/misc/SharedSecrets
&gt; used within &quot;vm.class&quot; instantiation of class gov.nasa.jpf.vm.SingleProcessVM
	at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:164)
	at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:156)
	at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:810)
	at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:830)
	at tlc2.tool.fp.OffHeapDiskFPSetJPFTest.test(OffHeapDiskFPSetJPFTest.java:44)
	at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
</failure>
  </testcase>
  <system-out><![CDATA[  running jpf with args: +listener=.listener.AssertionProperty,.listener.ErrorTraceGenerator
[SEVERE] JPF configuration error: error instantiating class gov.nasa.jpf.vm.OVHeap for entry "vm.heap.class":
> exception in gov.nasa.jpf.vm.OVHeap(gov.nasa.jpf.Config,gov.nasa.jpf.vm.KernelState):
>> java.lang.NoClassDefFoundError: sun/misc/SharedSecrets
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
]]></system-out>
  <system-err><![CDATA[gov.nasa.jpf.JPF$ExitException: JPF configuration error: error instantiating class gov.nasa.jpf.vm.OVHeap for entry "vm.heap.class":
> exception in gov.nasa.jpf.vm.OVHeap(gov.nasa.jpf.Config,gov.nasa.jpf.vm.KernelState):
>> java.lang.NoClassDefFoundError: sun/misc/SharedSecrets
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
	at gov.nasa.jpf.JPF.initialize(JPF.java:293)
	at gov.nasa.jpf.JPF.<init>(JPF.java:251)
	at gov.nasa.jpf.util.test.TestJPF.createJPF(TestJPF.java:729)
	at gov.nasa.jpf.util.test.TestJPF.createAndRunJPF(TestJPF.java:673)
	at gov.nasa.jpf.util.test.TestJPF.noPropertyViolation(TestJPF.java:806)
	at gov.nasa.jpf.util.test.TestJPF.verifyNoPropertyViolation(TestJPF.java:830)
	at tlc2.tool.fp.OffHeapDiskFPSetJPFTest.test(OffHeapDiskFPSetJPFTest.java:44)
	at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
	at java.base/java.lang.reflect.Method.invoke(Method.java:580)
	at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:50)
	at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
	at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:47)
	at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
	at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:325)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:78)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:57)
	at org.junit.runners.ParentRunner$3.run(ParentRunner.java:290)
	at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:71)
	at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:288)
	at org.junit.runners.ParentRunner.access$000(ParentRunner.java:58)
	at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:268)
	at org.junit.runners.ParentRunner.run(ParentRunner.java:363)
	at junit.framework.JUnit4TestAdapter.run(JUnit4TestAdapter.java:38)
	at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.run(JUnitTestRunner.java:535)
	at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.launch(JUnitTestRunner.java:1197)
	at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.main(JUnitTestRunner.java:1042)
Caused by: JPF configuration error: error instantiating class gov.nasa.jpf.vm.OVHeap for entry "vm.heap.class":
> exception in gov.nasa.jpf.vm.OVHeap(gov.nasa.jpf.Config,gov.nasa.jpf.vm.KernelState):
>> java.lang.NoClassDefFoundError: sun/misc/SharedSecrets
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
	at gov.nasa.jpf.Config.getInstance(Config.java:2011)
	at gov.nasa.jpf.Config.getEssentialInstance(Config.java:1933)
	at gov.nasa.jpf.JPF.initialize(JPF.java:269)
	... 25 more
]]></system-err>
</testsuite>

@lemmy
Copy link
Member

lemmy commented May 8, 2024

https://github.com/javapathfinder/jpf-core?tab=readme-ov-file#building-and-installing

@lemmy lemmy added the help wanted We need your help label May 8, 2024
@FedericoPonzi
Copy link
Contributor

I'll take a look at this one

@FedericoPonzi FedericoPonzi mentioned this issue Jun 12, 2024
Merged
@lemmy
Copy link
Member

lemmy commented Jun 21, 2024

Done

@lemmy lemmy closed this as completed Jun 21, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
DevEnvironment Everything related to the Toolbox development environment help wanted We need your help Tools The command line tools - TLC, SANY, ...
Milestone
No milestone
Development

No branches or pull requests
3 participants
@lemmy @ahelwer @FedericoPonzi