Current issue with jpf nas

[Mahmoud-Khawaja]

There was a classpath issue with jpf-nas, referring to #1 in jpf.properties.

1. Classpath Problem
Issue: TestNasJPF.class is located at:

build/classes/java/main/nas/util/test/TestNasJPF.class

But the original jpf.properties only included:

jpf-nas.classpath = \
   ${jpf-nas}/build/libs/jpf-nas-classes.jar;\
   ${jpf-nas}/build/classes/java/test

Missing directories:

build/classes/java/main
build/classes/java/examples

Before the fix, 3 tests appeared to "pass" but were actually never executed. JPF tests use this pattern:

I looked at the tests and I found that the structure looks like:

if (mpVerifyNoPropertyViolation(2, args)) {
    // Test body here
}

What was happening:

• When the if condition returned false:
• The test body was skipped entirely
• JUnit saw the method complete without assertions failing
• Result: "PASSED" (it's tricky because it's never executed)

The two failed tests failed because they probably were hitting the classpath error during JPF setup before the if condition could return false, causing actual test failures.

After the fix:

• All JPF framework calls succeed in starting JPF
• All if conditions return true
• All test bodies actually execute
• But they all hit the Java 11 SharedSecrets issue when JPF tries to create ServerSocket objects

2. Java 11 SharedSecrets Issue

The problem is all the tests failed.

After checking the log I found this:

java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaNetSocketAccess(Ljdk/internal/misc/JavaNetSocketAccess;)V
at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)

This means Java 11 changed the internal networking APIs that JPF-NAS relied on. When ServerSocket tries to initialize, it calls SharedSecrets.setJavaNetSocketAccess().

So, the issue is related to the Java version.

After analyzing the issue I found out that we need to create something to provide access to Java networking implementation for SharedSecrets.

package jdk.internal.misc;

import java.net.SocketImpl;
import java.net.ServerSocket;

public interface JavaNetSocketAccess {
    SocketImpl newSocketImpl(Class<? extends SocketImpl> clazz);
    ServerSocket newServerSocket(SocketImpl impl);  // Returns ServerSocket, not SocketImpl!
}

Purpose: This enables JPF's Network Interception Architecture:

Java 11 Application Code
         |
   JDK Internal APIs (java.net.*)
         |
   SharedSecrets.getJavaNetSocketAccess()
         |
   JPF's JavaNetSocketAccess Implementation  ← **THIS INTERFACE**
        |
   JPF Model Classes (ServerSocket, Socket, etc.)

Without this interface: JPF cannot intercept networking operations, making network verification impossible.

in SharedSecrets.java we added

private static JavaNetSocketAccess javaNetSocketAccess;

public static void setJavaNetSocketAccess(JavaNetSocketAccess jnsa) {
    javaNetSocketAccess = jnsa;
}

public static JavaNetSocketAccess getJavaNetSocketAccess() {
    if (javaNetSocketAccess == null)
        unsafe.ensureClassInitialized(java.net.ServerSocket.class);
    return javaNetSocketAccess;
}

back to jpf nas i added this static block in ServerSocket.java

static {
    try {
        jdk.internal.misc.SharedSecrets.setJavaNetSocketAccess(
            new jdk.internal.misc.JavaNetSocketAccess() {
                @Override
                public SocketImpl newSocketImpl(Class<? extends SocketImpl> clazz) {
                    return new SocketImpl();
                }

                @Override
                public ServerSocket newServerSocket(SocketImpl impl) {
                    return null;
                }
            }
        );
    } catch (Exception e) {
        // Exception ignored for graceful degradation
    }
}

It will execute immediately when JPF-NAS ServerSocket model class loads and must happen before Java's built-in ServerSocket initializes.

JPF Model Class Integration Architecture

Java 11 Application
         |
   Uses ServerSocket/Socket
         |
   JDK Internal Code calls SharedSecrets.getJavaNetSocketAccess()
         |
   Returns OUR implementation (registered by this static block)  
         |
   Calls our newSocketImpl()/newServerSocket() methods
         |
   Returns JPF model objects for verification

now if we tried to run the tests again we get in the output

running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 70c3013c60d627bc8158316abcf82fe503f5ae15) - (C) 2005-2014 United States Government. All rights reserved.

whick means that jpf runs successfully

the problem is we still have this error presist

java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaNetSocketAccess(...)
at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)

this is teh log i have

running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 70c3013c60d627bc8158316abcf82fe503f5ae15) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()

====================================================== search started: 6/30/25, 5:47 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaNetSocketAccess(Ljdk/internal/misc/JavaNetSocketAccess;)V
	at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)
	at net.nas.SocketTest.testTimedoutAccept(SocketTest.java:65)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@230
  call stack:
	at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)
	at net.nas.SocketTest.testTimedoutAccept(SocketTest.java:65)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:1,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:


====================================================== thread ops #1
   1     trans      insn          loc                : stmt
------- ---------------------------------------------------
W:d6         0      invokevirtual gov/nasa/jpf/FinalizerThread.java:0

====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodException: jdk.internal.misc..."

====================================================== search finished: 6/30/25, 5:47 AM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 70c3013c60d627bc8158316abcf82fe503f5ae15) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 6/30/25, 5:47 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaNetSocketAccess(Ljdk/internal/misc/JavaNetSocketAccess;)V
	at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)
	at net.nas.SocketTest.testTimedoutRead(SocketTest.java:121)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@304
  call stack:
	at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)
	at net.nas.SocketTest.testTimedoutRead(SocketTest.java:121)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== thread ops #1
   3       2     trans      insn          loc                : stmt
------- ------- ---------------------------------------------------
W:1ac      |         0      invokevirtual gov/nasa/jpf/FinalizerThread.java:0
   |    W:d6         0      invokevirtual gov/nasa/jpf/FinalizerThread.java:0

====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodException: jdk.internal.misc..."

====================================================== search finished: 6/30/25, 5:47 AM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 70c3013c60d627bc8158316abcf82fe503f5ae15) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 6/30/25, 5:47 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaNetSocketAccess(Ljdk/internal/misc/JavaNetSocketAccess;)V
	at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)
	at net.nas.SocketTest.testHash(SocketTest.java:83)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@304
  call stack:
	at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)
	at net.nas.SocketTest.testHash(SocketTest.java:83)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== thread ops #1
   3       2     trans      insn          loc                : stmt
------- ------- ---------------------------------------------------
W:1ac      |         0      invokevirtual gov/nasa/jpf/FinalizerThread.java:0
   |    W:d6         0      invokevirtual gov/nasa/jpf/FinalizerThread.java:0

====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodException: jdk.internal.misc..."

====================================================== search finished: 6/30/25, 5:47 AM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 70c3013c60d627bc8158316abcf82fe503f5ae15) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 6/30/25, 5:47 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaNetSocketAccess(Ljdk/internal/misc/JavaNetSocketAccess;)V
	at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)
	at net.nas.SocketTest.testEstablishingConnection(SocketTest.java:34)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@304
  call stack:
	at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)
	at net.nas.SocketTest.testEstablishingConnection(SocketTest.java:34)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== thread ops #1
   3       2     trans      insn          loc                : stmt
------- ------- ---------------------------------------------------
W:1ac      |         0      invokevirtual gov/nasa/jpf/FinalizerThread.java:0
   |    W:d6         0      invokevirtual gov/nasa/jpf/FinalizerThread.java:0

====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodException: jdk.internal.misc..."

====================================================== search finished: 6/30/25, 5:47 AM
  running jpf with args: +vm.process_finalizers=true
JavaPathfinder core system v8.0 (rev 70c3013c60d627bc8158316abcf82fe503f5ae15) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()

====================================================== search started: 6/30/25, 5:47 AM
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
I am here!!!

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: jdk.internal.misc.SharedSecrets.setJavaNetSocketAccess(Ljdk/internal/misc/JavaNetSocketAccess;)V
	at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)
	at net.nas.SocketTest$FinalizeServer.finalize(SocketTest.java:156)
	at gov.nasa.jpf.FinalizerThread.runFinalizer(gov.nasa.jpf.vm.JPF_gov_nasa_jpf_FinalizerThread)
	at gov.nasa.jpf.FinalizerThread.runAllFinalizers(FinalizerThread.java:44)
	at gov.nasa.jpf.FinalizerThread.processFinalizers(FinalizerThread.java:61)
	at gov.nasa.jpf.FinalizerThread.run(FinalizerThread.java:68)


====================================================== snapshot #1
thread gov.nasa.jpf.FinalizerThread:{id:1,name:finalizer,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@239
  call stack:
	at java.net.ServerSocket.<clinit>(ServerSocket.java:1036)
	at net.nas.SocketTest$FinalizeServer.finalize(SocketTest.java:156)
	at gov.nasa.jpf.FinalizerThread.runFinalizer(FinalizerThread.java)
	at gov.nasa.jpf.FinalizerThread.runAllFinalizers(FinalizerThread.java:44)
	at gov.nasa.jpf.FinalizerThread.processFinalizers(FinalizerThread.java:61)
	at gov.nasa.jpf.FinalizerThread.run(FinalizerThread.java:68)


====================================================== thread ops #1
 trans      insn          loc                : stmt
---------------------------------------------------

====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodException: jdk.internal.misc..."

====================================================== search finished: 6/30/25, 5:47 AM

[cyrille-artho]

Please make a PR to jpf-core with the part that implements the extra method in SharedSecrets.java, the block starting after "in SharedSecrets.java we added".

This PR will go to the Java 11 (currently, master) branch of jpf-core; you can also make another PR to the java-17 branch.

[cyrille-artho]

For the files in src/classes: The files need to be moved from src/classes/java to src/classes/modules/java.base/java.

The compiled files should then end up in build/classes/java.base/java (without "modules"), like in the build for jpf-core and its model classes.

[cyrille-artho]

For the new build with the Java module system, look at build.gradle from jpf-core, where we use the same convention with Java modules being in src/classes/modules/:

            '--patch-module', "java.base=" + file('src/classes/modules/java.base'),             

[Mahmoud-Khawaja]

i found the issue. it was a the wrong path in sites.properties. my bad i spend alot of time on it.

now we have this

 running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/13/25, 8:13 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native java.net.PlainSocketImpl.initProto
	at java.net.PlainSocketImpl.initProto(no peer)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:43)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testTimedoutAccept(SocketTest.java:65)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@245
  call stack:
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:43)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testTimedoutAccept(SocketTest.java:65)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:1,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: cannot find native..."

====================================================== search finished: 7/13/25, 8:13 AM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/13/25, 8:13 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native java.net.PlainSocketImpl.initProto
	at java.net.PlainSocketImpl.initProto(no peer)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:43)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testTimedoutRead(SocketTest.java:121)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@319
  call stack:
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:43)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testTimedoutRead(SocketTest.java:121)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: cannot find native..."

====================================================== search finished: 7/13/25, 8:13 AM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/13/25, 8:13 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native java.net.PlainSocketImpl.initProto
	at java.net.PlainSocketImpl.initProto(no peer)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:43)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testHash(SocketTest.java:83)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@319
  call stack:
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:43)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testHash(SocketTest.java:83)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: cannot find native..."

====================================================== search finished: 7/13/25, 8:13 AM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/13/25, 8:13 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native java.net.PlainSocketImpl.initProto
	at java.net.PlainSocketImpl.initProto(no peer)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:43)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testEstablishingConnection(SocketTest.java:34)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@319
  call stack:
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:43)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testEstablishingConnection(SocketTest.java:34)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: cannot find native..."

====================================================== search finished: 7/13/25, 8:13 AM
  running jpf with args: +vm.process_finalizers=true
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/13/25, 8:13 AM
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
I am here!!!

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native java.net.PlainSocketImpl.initProto
	at java.net.PlainSocketImpl.initProto(no peer)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:43)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest$FinalizeServer.finalize(SocketTest.java:156)
	at gov.nasa.jpf.FinalizerThread.runFinalizer(gov.nasa.jpf.vm.JPF_gov_nasa_jpf_FinalizerThread)
	at gov.nasa.jpf.FinalizerThread.runAllFinalizers(FinalizerThread.java:44)
	at gov.nasa.jpf.FinalizerThread.processFinalizers(FinalizerThread.java:61)
	at gov.nasa.jpf.FinalizerThread.run(FinalizerThread.java:68)


====================================================== snapshot #1
thread gov.nasa.jpf.FinalizerThread:{id:1,name:finalizer,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@24e
  call stack:
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:43)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest$FinalizeServer.finalize(SocketTest.java:156)
	at gov.nasa.jpf.FinalizerThread.runFinalizer(FinalizerThread.java)
	at gov.nasa.jpf.FinalizerThread.runAllFinalizers(FinalizerThread.java:44)
	at gov.nasa.jpf.FinalizerThread.processFinalizers(FinalizerThread.java:61)
	at gov.nasa.jpf.FinalizerThread.run(FinalizerThread.java:68)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: cannot find native..."

====================================================== search finished: 7/13/25, 8:13 AM

as i can see that we have some missing native peers like PlainSocketImpl.initProto()

[Mahmoud-Khawaja]

i added the new peer class and now we have this

 running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/13/25, 9:37 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NullPointerException: Calling 'startsWith(Ljava/lang/String;)Z' on null object
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.create(ExtendedSocketOptions.java:346)
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.<clinit>(ExtendedSocketOptions.java:353)
	at jdk.net.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:165)
	at java.lang.Class.forName(gov.nasa.jpf.vm.JPF_java_lang_Class)
	at sun.net.ext.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:109)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:59)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testTimedoutAccept(SocketTest.java:65)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@245,java.lang.Class@2ac,java.lang.Class@2b1,java.lang.Class@2c9
  call stack:
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.<clinit>(ExtendedSocketOptions.java:353)
	at jdk.net.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:165)
	at java.lang.Class.forName(Class.java)
	at sun.net.ext.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:109)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:59)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testTimedoutAccept(SocketTest.java:65)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:1,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NullPointerException: Calling 'startsWit..."

====================================================== search finished: 7/13/25, 9:37 AM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/13/25, 9:37 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NullPointerException: Calling 'startsWith(Ljava/lang/String;)Z' on null object
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.create(ExtendedSocketOptions.java:346)
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.<clinit>(ExtendedSocketOptions.java:353)
	at jdk.net.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:165)
	at java.lang.Class.forName(gov.nasa.jpf.vm.JPF_java_lang_Class)
	at sun.net.ext.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:109)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:59)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testTimedoutRead(SocketTest.java:121)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@319,java.lang.Class@380,java.lang.Class@385,java.lang.Class@39d
  call stack:
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.<clinit>(ExtendedSocketOptions.java:353)
	at jdk.net.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:165)
	at java.lang.Class.forName(Class.java)
	at sun.net.ext.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:109)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:59)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testTimedoutRead(SocketTest.java:121)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NullPointerException: Calling 'startsWit..."

====================================================== search finished: 7/13/25, 9:37 AM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/13/25, 9:37 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NullPointerException: Calling 'startsWith(Ljava/lang/String;)Z' on null object
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.create(ExtendedSocketOptions.java:346)
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.<clinit>(ExtendedSocketOptions.java:353)
	at jdk.net.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:165)
	at java.lang.Class.forName(gov.nasa.jpf.vm.JPF_java_lang_Class)
	at sun.net.ext.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:109)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:59)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testHash(SocketTest.java:83)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@319,java.lang.Class@380,java.lang.Class@385,java.lang.Class@39d
  call stack:
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.<clinit>(ExtendedSocketOptions.java:353)
	at jdk.net.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:165)
	at java.lang.Class.forName(Class.java)
	at sun.net.ext.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:109)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:59)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testHash(SocketTest.java:83)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NullPointerException: Calling 'startsWit..."

====================================================== search finished: 7/13/25, 9:37 AM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/13/25, 9:37 AM
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NullPointerException: Calling 'startsWith(Ljava/lang/String;)Z' on null object
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.create(ExtendedSocketOptions.java:346)
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.<clinit>(ExtendedSocketOptions.java:353)
	at jdk.net.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:165)
	at java.lang.Class.forName(gov.nasa.jpf.vm.JPF_java_lang_Class)
	at sun.net.ext.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:109)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:59)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testEstablishingConnection(SocketTest.java:34)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@319,java.lang.Class@380,java.lang.Class@385,java.lang.Class@39d
  call stack:
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.<clinit>(ExtendedSocketOptions.java:353)
	at jdk.net.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:165)
	at java.lang.Class.forName(Class.java)
	at sun.net.ext.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:109)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:59)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest.testEstablishingConnection(SocketTest.java:34)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NullPointerException: Calling 'startsWit..."

====================================================== search finished: 7/13/25, 9:37 AM
  running jpf with args: +vm.process_finalizers=true
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/13/25, 9:37 AM
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
I am here!!!

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NullPointerException: Calling 'startsWith(Ljava/lang/String;)Z' on null object
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.create(ExtendedSocketOptions.java:346)
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.<clinit>(ExtendedSocketOptions.java:353)
	at jdk.net.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:165)
	at java.lang.Class.forName(gov.nasa.jpf.vm.JPF_java_lang_Class)
	at sun.net.ext.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:109)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:59)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest$FinalizeServer.finalize(SocketTest.java:156)
	at gov.nasa.jpf.FinalizerThread.runFinalizer(gov.nasa.jpf.vm.JPF_gov_nasa_jpf_FinalizerThread)
	at gov.nasa.jpf.FinalizerThread.runAllFinalizers(FinalizerThread.java:44)
	at gov.nasa.jpf.FinalizerThread.processFinalizers(FinalizerThread.java:61)
	at gov.nasa.jpf.FinalizerThread.run(FinalizerThread.java:68)


====================================================== snapshot #1
thread gov.nasa.jpf.FinalizerThread:{id:1,name:finalizer,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@24e,java.lang.Class@2b5,java.lang.Class@2ba,java.lang.Class@2d2
  call stack:
	at jdk.net.ExtendedSocketOptions$PlatformSocketOptions.<clinit>(ExtendedSocketOptions.java:353)
	at jdk.net.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:165)
	at java.lang.Class.forName(Class.java)
	at sun.net.ext.ExtendedSocketOptions.<clinit>(ExtendedSocketOptions.java:109)
	at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:59)
	at java.net.ServerSocket.setImpl(ServerSocket.java:308)
	at java.net.ServerSocket.<init>(ServerSocket.java:250)
	at java.net.ServerSocket.<init>(ServerSocket.java:149)
	at net.nas.SocketTest$FinalizeServer.finalize(SocketTest.java:156)
	at gov.nasa.jpf.FinalizerThread.runFinalizer(FinalizerThread.java)
	at gov.nasa.jpf.FinalizerThread.runAllFinalizers(FinalizerThread.java:44)
	at gov.nasa.jpf.FinalizerThread.processFinalizers(FinalizerThread.java:61)
	at gov.nasa.jpf.FinalizerThread.run(FinalizerThread.java:68)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NullPointerException: Calling 'startsWit..."

====================================================== search finished: 7/13/25, 9:37 AM

now we have a problem with ExtendedSocketOptions initialization i dont really understand what is this about. any advice?

[cyrille-artho]

With the missing peer class now added, what seems to happen is that the code in JPF (jpf-core and/or jpf-nas) does not follow the same assumptions/conventions as the code on the host JVM and its Java library.
Perhaps a class is not found (in the dynamic class lookup using Class.forName) or a string has the wrong content or is null. Later on, this ends up in a string being null when calling startsWith on it.
Try to add some logging code to trace what's happening in the lower part of the stack trace where the code being executed is from JPF's model classes or native peer classes. Perhaps we get some insight into what is looking unusual.
Perhaps you can also get some insight by looking into the source of ExtendedSocketOptions.java (from OpenJDK 11) to see what the string is expected to contain.

[Mahmoud-Khawaja]

now we got this

 running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JPF_java_io_OutputStream loaded
[WARNING] orphan NativePeer method: java.lang.ref.Reference.enqueue()Z
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/19/25, 2:10 PM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
JPF_java_net_PlainSocketImpl loaded
[WARNING] orphan NativePeer method: java.net.PlainSocketImpl.socketGetOption(II)I
PlainSocketImpl static initialization intercepted
JPF_java_net_InetAddress loaded
[WARNING] orphan NativePeer method: java.net.InetAddress.getAllByName0(Ljava/lang/String;Ljava/net/InetAddress;Z)[Ljava/net/InetAddress;
[WARNING] orphan NativePeer method: java.net.InetAddress.getAddress()3B
[WARNING] orphan NativePeer method: java.net.InetAddress.getLocalHostName()Ljava/lang/String;
[WARNING] orphan NativePeer method: java.net.InetAddress.lookupHostByName(Ljava/lang/String;)I
[WARNING] orphan NativePeer method: java.net.InetAddress.getHostByAddr([B)Ljava/lang/String;
[WARNING] orphan NativePeer method: java.net.InetAddress.isReachable0([BII[BII)Z
InetAddress static initialization intercepted
Created anyLocalAddress InetAddress object
PlainSocketImpl.socketCreate() intercepted - stream: true
socketCreate: field setting failed, using minimal mode
JPF_jdk_internal_ref_PhantomCleanable loaded
[WARNING] orphan NativePeer method: jdk.internal.ref.PhantomCleanable.<clinit>
[WARNING] orphan NativePeer method: jdk.internal.ref.PhantomCleanable.<init>(Ljava/lang/Object;Ljava/lang/ref/Cleaner;Ljava/lang/Runnable;)V
JPF_java_net_SocketCleanable loaded
[WARNING] orphan NativePeer method: java.net.SocketCleanable.register(Ljava/io/FileDescriptor;)Ljava/lang/ref/Cleaner/Cleanable;
SocketCleanable static initialization intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
PlainSocketImpl.socketBind() intercepted - port: 1024
PlainSocketImpl.socketListen() intercepted
PlainSocketImpl.socketSetOption() intercepted - option: 4102
Set socket timeout: 10ms
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
PlainSocketImpl.socketAccept() intercepted
SocketCleanable.register(void) bypassed for JPF-NAS

====================================================== results
no errors detected

====================================================== search finished: 7/19/25, 2:10 PM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
[WARNING] orphan NativePeer method: java.lang.ref.Reference.enqueue()Z
[WARNING] orphan NativePeer method: java.lang.ref.Reference.enqueue()Z
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/19/25, 2:10 PM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.PlainSocketImpl.socketGetOption(II)I
PlainSocketImpl static initialization intercepted
[WARNING] orphan NativePeer method: java.net.InetAddress.getAllByName0(Ljava/lang/String;Ljava/net/InetAddress;Z)[Ljava/net/InetAddress;
[WARNING] orphan NativePeer method: java.net.InetAddress.getAddress()3B
[WARNING] orphan NativePeer method: java.net.InetAddress.getLocalHostName()Ljava/lang/String;
[WARNING] orphan NativePeer method: java.net.InetAddress.lookupHostByName(Ljava/lang/String;)I
[WARNING] orphan NativePeer method: java.net.InetAddress.getHostByAddr([B)Ljava/lang/String;
[WARNING] orphan NativePeer method: java.net.InetAddress.isReachable0([BII[BII)Z
InetAddress static initialization intercepted
Created anyLocalAddress InetAddress object
PlainSocketImpl.socketCreate() intercepted - stream: true
socketCreate: field setting failed, using minimal mode
[WARNING] orphan NativePeer method: jdk.internal.ref.PhantomCleanable.<clinit>
[WARNING] orphan NativePeer method: jdk.internal.ref.PhantomCleanable.<init>(Ljava/lang/Object;Ljava/lang/ref/Cleaner;Ljava/lang/Runnable;)V
[WARNING] orphan NativePeer method: java.net.SocketCleanable.register(Ljava/io/FileDescriptor;)Ljava/lang/ref/Cleaner/Cleanable;
SocketCleanable static initialization intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
PlainSocketImpl.socketBind() intercepted - port: 1024
PlainSocketImpl.socketListen() intercepted
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
PlainSocketImpl.socketAccept() intercepted
SocketCleanable.register(void) bypassed for JPF-NAS

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.AssertionError: 
	at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:164)
	at gov.nasa.jpf.util.test.TestJPF.assertTrue(TestJPF.java:1174)
	at gov.nasa.jpf.util.test.TestJPF.assertTrue(TestJPF.java:1179)
	at net.nas.SocketTest.testTimedoutRead(SocketTest.java:130)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.AssertionError:   at gov.nasa.jpf.util.t..."

====================================================== search finished: 7/19/25, 2:10 PM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
[WARNING] orphan NativePeer method: java.lang.ref.Reference.enqueue()Z
[WARNING] orphan NativePeer method: java.lang.ref.Reference.enqueue()Z
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/19/25, 2:10 PM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.PlainSocketImpl.socketGetOption(II)I
PlainSocketImpl static initialization intercepted
[WARNING] orphan NativePeer method: java.net.InetAddress.getAllByName0(Ljava/lang/String;Ljava/net/InetAddress;Z)[Ljava/net/InetAddress;
[WARNING] orphan NativePeer method: java.net.InetAddress.getAddress()3B
[WARNING] orphan NativePeer method: java.net.InetAddress.getLocalHostName()Ljava/lang/String;
[WARNING] orphan NativePeer method: java.net.InetAddress.lookupHostByName(Ljava/lang/String;)I
[WARNING] orphan NativePeer method: java.net.InetAddress.getHostByAddr([B)Ljava/lang/String;
[WARNING] orphan NativePeer method: java.net.InetAddress.isReachable0([BII[BII)Z
InetAddress static initialization intercepted
Created anyLocalAddress InetAddress object
PlainSocketImpl.socketCreate() intercepted - stream: true
socketCreate: field setting failed, using minimal mode
[WARNING] orphan NativePeer method: jdk.internal.ref.PhantomCleanable.<clinit>
[WARNING] orphan NativePeer method: jdk.internal.ref.PhantomCleanable.<init>(Ljava/lang/Object;Ljava/lang/ref/Cleaner;Ljava/lang/Runnable;)V
[WARNING] orphan NativePeer method: java.net.SocketCleanable.register(Ljava/io/FileDescriptor;)Ljava/lang/ref/Cleaner/Cleanable;
SocketCleanable static initialization intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
PlainSocketImpl.socketBind() intercepted - port: 1024
PlainSocketImpl.socketListen() intercepted
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
PlainSocketImpl.socketAccept() intercepted
SocketCleanable.register(void) bypassed for JPF-NAS

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NullPointerException: array length of null object
	at java.io.ByteArrayOutputStream.ensureCapacity(ByteArrayOutputStream.java:94)
	at java.io.ByteArrayOutputStream.write(ByteArrayOutputStream.java:137)
	at net.nas.SocketTest.testHash(SocketTest.java:99)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NullPointerException: array length of nu..."

====================================================== search finished: 7/19/25, 2:10 PM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
[WARNING] orphan NativePeer method: java.lang.ref.Reference.enqueue()Z
[WARNING] orphan NativePeer method: java.lang.ref.Reference.enqueue()Z
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/19/25, 2:10 PM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
[WARNING] orphan NativePeer method: java.net.PlainSocketImpl.socketGetOption(II)I
PlainSocketImpl static initialization intercepted
[WARNING] orphan NativePeer method: java.net.InetAddress.getAllByName0(Ljava/lang/String;Ljava/net/InetAddress;Z)[Ljava/net/InetAddress;
[WARNING] orphan NativePeer method: java.net.InetAddress.getAddress()3B
[WARNING] orphan NativePeer method: java.net.InetAddress.getLocalHostName()Ljava/lang/String;
[WARNING] orphan NativePeer method: java.net.InetAddress.lookupHostByName(Ljava/lang/String;)I
[WARNING] orphan NativePeer method: java.net.InetAddress.getHostByAddr([B)Ljava/lang/String;
[WARNING] orphan NativePeer method: java.net.InetAddress.isReachable0([BII[BII)Z
InetAddress static initialization intercepted
Created anyLocalAddress InetAddress object
PlainSocketImpl.socketCreate() intercepted - stream: true
socketCreate: field setting failed, using minimal mode
[WARNING] orphan NativePeer method: jdk.internal.ref.PhantomCleanable.<clinit>
[WARNING] orphan NativePeer method: jdk.internal.ref.PhantomCleanable.<init>(Ljava/lang/Object;Ljava/lang/ref/Cleaner;Ljava/lang/Runnable;)V
[WARNING] orphan NativePeer method: java.net.SocketCleanable.register(Ljava/io/FileDescriptor;)Ljava/lang/ref/Cleaner/Cleanable;
SocketCleanable static initialization intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
PlainSocketImpl.socketBind() intercepted - port: 1024
PlainSocketImpl.socketListen() intercepted
PlainSocketImpl.socketSetOption() intercepted - option: 4102
Set socket timeout: 10ms
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
PlainSocketImpl.socketAccept() intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V

====================================================== results
no errors detected

====================================================== search finished: 7/19/25, 2:10 PM
  running jpf with args: +vm.process_finalizers=true
[WARNING] orphan NativePeer method: java.lang.ref.Reference.enqueue()Z
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/19/25, 2:10 PM
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
[WARNING] orphan NativePeer method: java.net.ServerSocket.CheckForAddressAlreadyInUse(I)V
I am here!!!
[WARNING] orphan NativePeer method: java.net.PlainSocketImpl.socketGetOption(II)I
PlainSocketImpl static initialization intercepted
[WARNING] orphan NativePeer method: java.net.InetAddress.getAllByName0(Ljava/lang/String;Ljava/net/InetAddress;Z)[Ljava/net/InetAddress;
[WARNING] orphan NativePeer method: java.net.InetAddress.getAddress()3B
[WARNING] orphan NativePeer method: java.net.InetAddress.getLocalHostName()Ljava/lang/String;
[WARNING] orphan NativePeer method: java.net.InetAddress.lookupHostByName(Ljava/lang/String;)I
[WARNING] orphan NativePeer method: java.net.InetAddress.getHostByAddr([B)Ljava/lang/String;
[WARNING] orphan NativePeer method: java.net.InetAddress.isReachable0([BII[BII)Z
InetAddress static initialization intercepted
Created anyLocalAddress InetAddress object
PlainSocketImpl.socketCreate() intercepted - stream: true
socketCreate: field setting failed, using minimal mode
[WARNING] orphan NativePeer method: jdk.internal.ref.PhantomCleanable.<clinit>
[WARNING] orphan NativePeer method: jdk.internal.ref.PhantomCleanable.<init>(Ljava/lang/Object;Ljava/lang/ref/Cleaner;Ljava/lang/Runnable;)V
[WARNING] orphan NativePeer method: java.net.SocketCleanable.register(Ljava/io/FileDescriptor;)Ljava/lang/ref/Cleaner/Cleanable;
SocketCleanable static initialization intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
PlainSocketImpl.socketBind() intercepted - port: 1024
PlainSocketImpl.socketListen() intercepted
PlainSocketImpl.socketAccept() intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
DONE!

====================================================== results
no errors detected

====================================================== search finished: 7/19/25, 2:10 PM

[Mahmoud-Khawaja]

we have 1/5 passing tests. the main issue that we have right now is test integration issues. i dont see in the log and java 11 compatibility issue. its all assertion faliure or ByteArrayOutputStream initialization. what do you think avout it?

[cyrille-artho]

Thank you for the update. The orphan NativePeer method warnings are about methods in model classes that are declared to be native, but there is no @MJI counterpart among the native peers.
This can happen because the counterpart is missing or has a slightly mismatched signature so it is not found. (JPF does not emit a warning about extraneous native peers that cannot be matched to a method in the corresponding model class.)
For simple stubs, the easiest way to eliminate these warnings is to remove the keyword native in the model class, because in that case, no native peer is needed, and the functionality can be implemented directly in the model class. I would recommend this over adding native peer methods, because it is simpler to keep functionality inside the model classes if no native-level functionality is needed. Of course, to simulate actual I/O, native peers are likely necessary.
I'll have to look into the rest later. Again, on my computer, only two tests fail, so there is another issue there.

[cyrille-artho]

Regarding the layout of the source files, please try to adapt the convention of jpf-core, i.e., use src/classes/modules (followed by the module name) to make it easier to find library classes for a certain module and to keep the build logic uniform among jpf-core and its extensions.

[Mahmoud-Khawaja]

now we have this error

 running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/21/25, 3:34 PM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
JPF_java_net_PlainSocketImpl loaded
PlainSocketImpl static initialization intercepted
Created anyLocalAddress InetAddress object
PlainSocketImpl.socketCreate() intercepted - stream: true
socketCreate: field setting failed, using minimal mode
JPF_java_net_SocketCleanable loaded
SocketCleanable static initialization intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
PlainSocketImpl.socketBind() intercepted - port: 1024
PlainSocketImpl.socketListen() intercepted
PlainSocketImpl.socketSetOption() intercepted - option: 4102
Set socket timeout: 10ms
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
PlainSocketImpl.socketAccept() intercepted
SocketCleanable.register(void) bypassed for JPF-NAS

====================================================== results
no errors detected

====================================================== search finished: 7/21/25, 3:34 PM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/21/25, 3:34 PM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
PlainSocketImpl static initialization intercepted
Created anyLocalAddress InetAddress object
PlainSocketImpl.socketCreate() intercepted - stream: true
socketCreate: field setting failed, using minimal mode
SocketCleanable static initialization intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
PlainSocketImpl.socketBind() intercepted - port: 1024
PlainSocketImpl.socketListen() intercepted
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
PlainSocketImpl.socketAccept() intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
Socket initialization: using minimal mode with fallback hash storage

====================================================== results
no errors detected

====================================================== search finished: 7/21/25, 3:34 PM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/21/25, 3:34 PM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
PlainSocketImpl static initialization intercepted
Created anyLocalAddress InetAddress object
PlainSocketImpl.socketCreate() intercepted - stream: true
socketCreate: field setting failed, using minimal mode
SocketCleanable static initialization intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
PlainSocketImpl.socketBind() intercepted - port: 1024
PlainSocketImpl.socketListen() intercepted
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
PlainSocketImpl.socketAccept() intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
DEBUG: SocketOutputStream.write() called with value=10
DEBUG: socketRef=959, conn=null
Fallback hash updated for data write: 0 -> 10 (data: 10)
DEBUG: Hash update completed for value=10
DEBUG: No connection - hash updated but no I/O performed

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.AssertionError: 
	at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:164)
	at gov.nasa.jpf.util.test.TestJPF.assertTrue(TestJPF.java:1174)
	at gov.nasa.jpf.util.test.TestJPF.assertTrue(TestJPF.java:1179)
	at net.nas.SocketTest.testHash(SocketTest.java:101)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread gov.nasa.jpf.FinalizerThread:{id:2,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@d6
  call stack:

thread java.lang.Thread:{id:1,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:

thread gov.nasa.jpf.FinalizerThread:{id:3,name:finalizer,status:WAITING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  waiting on: java.lang.Object@1ac
  call stack:


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.AssertionError:   at gov.nasa.jpf.util.t..."

====================================================== search finished: 7/21/25, 3:34 PM
  running jpf with args: +search.multiple_errors = true +vm.process_finalizers = true +vm.nas.initiating_target = 0
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()+net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/21/25, 3:34 PM
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
PlainSocketImpl static initialization intercepted
Created anyLocalAddress InetAddress object
PlainSocketImpl.socketCreate() intercepted - stream: true
socketCreate: field setting failed, using minimal mode
SocketCleanable static initialization intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
PlainSocketImpl.socketBind() intercepted - port: 1024
PlainSocketImpl.socketListen() intercepted
PlainSocketImpl.socketSetOption() intercepted - option: 4102
Set socket timeout: 10ms
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
PlainSocketImpl.socketAccept() intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
Socket initialization: using minimal mode with fallback hash storage

====================================================== results
no errors detected

====================================================== search finished: 7/21/25, 3:34 PM
  running jpf with args: +vm.process_finalizers=true
JavaPathfinder core system v8.0 (rev 9134e4a676e52ee9599fb321f6a275a120fc1660) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
net.nas.SocketTest.runTestMethod()

====================================================== search started: 7/21/25, 3:34 PM
[WARNING] orphan NativePeer method: java.net.Socket.connect(Ljava/lang/String;I)V
[WARNING] orphan NativePeer method: java.net.ServerSocket.accept0()Ljava/net/Socket;
I am here!!!
PlainSocketImpl static initialization intercepted
Created anyLocalAddress InetAddress object
PlainSocketImpl.socketCreate() intercepted - stream: true
socketCreate: field setting failed, using minimal mode
SocketCleanable static initialization intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
PlainSocketImpl.socketBind() intercepted - port: 1024
PlainSocketImpl.socketListen() intercepted
PlainSocketImpl.socketAccept() intercepted
SocketCleanable.register(void) bypassed for JPF-NAS
DONE!

====================================================== results
no errors detected

====================================================== search finished: 7/21/25, 3:34 PM

we now have 2/5 passing tests. but the problem is jpf is not loading our socket model class even though its compiled in the build

you can see this in the log

Socket initialization: using minimal mode with fallback hash storage

Fallback hash updated for data write: 0 -> 10 (data: 10)

we already have the hash filed property declaed in socket and also the getHash function
im still investigating in what is the problem with it. any ideas?

[Mahmoud-Khawaja]

I'm also curious about what results you’re getting on your machine, because having 3 out of 5 tests passing is a bit strange, to be honest. I'm not sure which tests are passing on your end, but we now only have 2 passing on GitHub Actions.

[cyrille-artho]

My test results are:

SocketTest > testTimedoutAccept FAILED
    java.lang.AssertionError at SocketTest.java:63

SocketTest > testTimedoutRead PASSED

SocketTest > testHash PASSED

SocketTest > testEstablishingConnection PASSED

SocketTest > testDeadlockForBlockedFinalizer_MulitProcessVM FAILED
    java.lang.AssertionError at SocketTest.java:173

[cyrille-artho]

The reason for the tests failing is that the model classes and perhaps also the native peers are not found by JPF. With Java 11, JPF places the compiled model classes in build/classes/<module>/<package>/<classname>, but jpf-nas currently puts them in build/classes/<package>/... without the module name as another directory right in classes.
This does not seem to apply to the native peers, so they can probably remain where they are.