StringIndexOutOfBoundsException about jpf-core HOT 5 CLOSED

This one may be a bit more difficult to debug. The problem is a logical problem: The native peer requests four bytes (from 0 to 3), but the string is of length 1.
Several possibilities:

• The logic is wrong somewhere and updates internal data incorrectly, so later, more content is requested than what actually exists.
• A conversion/encoding issue results in a discrepancy between the available and expected number of bytes.

Can you create a standalone example from test, with a .jpf file that executes the problematic test through JPF's command line interface? Then, we can try to use the MethodTracker to see what methods are called on the target String.

from jpf-core.

What will the content of example ? I mean what example will test this ?

//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
I tried to find the inner implementation of getBytes(...). And then applied there.

Now our failed tests reduced.

Test Execution: FAILURE
Summary: 1002 tests, 995 passed, 7 failed, 0 skipped

1002 tests completed, 7 failed

> Task :test FAILED

FAILURE: Build failed with an exception.

* What went wrong:
Execution failed for task ':test'.

But why our own logic failed here ?

from jpf-core.

What I meant was the following:

1. Check which class implements the unit test that fails.
2. Check if the source of that unit test also has a main method. Many JPF tests have that, to facilitate running them as a small stand-alone program. If you can't find a main, add one taking a different JPF test class as an example.
3. If you run the test from the command line through its main, you get more information about why it fails.
   There is an internal assumption in the code that no longer holds under Java 11; we first have to find out why the test fails before we can fix it.

from jpf-core.

running jpf with args:
JavaPathfinder core system v8.0 (rev 9e0c527) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test
gov.nasa.jpf.test.java.nio.BufferTest.runTestMethod()

====================================================== search started: 03/06/24, 12:14 pm
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
[WARNING] orphan NativePeer method: java.util.ResourceBundle.getClassContext()[Ljava/lang/Class;
running jpf with args:
JavaPathfinder core system v8.0 (rev 9e0c527) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test
gov.nasa.jpf.test.java.nio.BufferTest.runTestMethod()

====================================================== search started: 03/06/24, 12:14 pm
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
[WARNING] orphan NativePeer method: java.lang.StringCoding.decode([BII)[C
[WARNING] orphan NativePeer method: java.lang.StringCoding.encode([CII)[B

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native jdk.internal.misc.ScopedMemoryAccess.registerNatives
at jdk.internal.misc.ScopedMemoryAccess.registerNatives(no peer)
at jdk.internal.misc.ScopedMemoryAccess.(ScopedMemoryAccess.java:83)
at java.nio.BufferMismatch.(BufferMismatch.java:35)
at java.nio.ByteBuffer.equals(ByteBuffer.java:311)
at gov.nasa.jpf.test.java.nio.BufferTest.testByteBufferConstructor(BufferTest.java:45)
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@2d0,java.lang.Class@2d3
call stack:
at jdk.internal.misc.ScopedMemoryAccess.(ScopedMemoryAccess.java:83)
at java.nio.BufferMismatch.(BufferMismatch.java:35)
at java.nio.ByteBuffer.equals(ByteBuffer.java:311)
at gov.nasa.jpf.test.java.nio.BufferTest.testByteBufferConstructor(BufferTest.java:45)
at java.lang.reflect.Method.invoke(Method.java)
at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

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

====================================================== search finished: 03/06/24, 12:14 pm

from jpf-core.

I see. We first want to understand what has changed in the string contents for the strings created by BufferTest.testCharBufferConstructor. Please use a debugger or add some logging code to see this. (You may have to log the content in hexadecimal to see exactly what the contents are.)

from jpf-core.