JPF is an extensible software analysis framework for Java bytecode. jpf-core is the basis for all JPF projects; you always need to install it. It contains the basic VM and model checking infrastructure, and can be used to check for concurrency defects like deadlocks, and unhandled exceptions like NullPointerExceptions and AssertionErrors.
517
stars
326
forks
source link
Java 17: BufferMismatch now depends on native code: JPF crashes (missing native peer) if byte buffers differ #458
We currently have a unit test in BufferTest that fails due to string contents no longer matching with Java 17 due to different string encodings. This reveals a new problem: BufferMismatch now depends on a new internal class ScopedMemoryAccess, which we do not model (and want to avoid modeling if possible).
Once the string encoding issue if fixed (https://github.com/javapathfinder/jpf-core/issues/456), we need an additional unit test to make the BufferMismatch (used by ByteBuffer.equals) visible.
After that, we probably will replace the call to BufferMismatch.mismatch with a small loop that performs the comparison directly in ByteBuffer.equals.
We currently have a unit test in
BufferTestthat fails due to string contents no longer matching with Java 17 due to different string encodings. This reveals a new problem:BufferMismatchnow depends on a new internal classScopedMemoryAccess, which we do not model (and want to avoid modeling if possible). Once the string encoding issue if fixed (https://github.com/javapathfinder/jpf-core/issues/456), we need an additional unit test to make theBufferMismatch(used byByteBuffer.equals) visible. After that, we probably will replace the call toBufferMismatch.mismatchwith a small loop that performs the comparison directly inByteBuffer.equals.