Repository navigation
Field use triggers RuntimeException #238
Description
Description
Runtime exception in the next case.
Minimal reproducer
Client:
public class ByteBufTest {
public static final int TEST_BUFFER_SIZE = 128;
private ByteBuffer mDirectBuffer;
public ByteBufTest() {
mDirectBuffer = ByteBuffer.allocateDirect(TEST_BUFFER_SIZE);
byte[] buf = mDirectBuffer.array();
}
}Refinements:
@Ghost("boolean arrayBacked")
@ExternalRefinementsFor("java.nio.ByteBuffer")
public interface ByteBufferRefinements {
// ---- Backing array access ----
@StateRefinement(to="_ ? arrayBacked() : !arrayBacked()")
boolean hasArray();
@StateRefinement(from="arrayBacked()")
byte[] array();
@StateRefinement(from="arrayBacked()")
int arrayOffset();
}Expected behavior
Not RuntimeException. Also within the method we shuold be able to know the state of the object even if it is a field if that state is introduced in this scope.
Actual behavior
StackTrace:
java.lang.RuntimeException:
Error while checking CtConstructorImpl
on ByteBufTest() {
at /Users/cgamboa/git/task-examples/liquidjava-tasks/src/main/java/com/example/so_clients/bytebuffer48582520/ByteBufTest.java:14
with
Error while checking CtBlockImpl
on {
at /Users/cgamboa/git/task-examples/liquidjava-tasks/src/main/java/com/example/so_clients/bytebuffer48582520/ByteBufTest.java:14
with
Error while checking CtLocalVariableImpl
on buf = mDirectBuffer.array();
at /Users/cgamboa/git/task-examples/liquidjava-tasks/src/main/java/com/example/so_clients/bytebuffer48582520/ByteBufTest.java:20
with
Error while checking CtInvocationImpl
on mDirectBuffer.array();
at /Users/cgamboa/git/task-examples/liquidjava-tasks/src/main/java/com/example/so_clients/bytebuffer48582520/ByteBufTest.java:20
with Cannot invoke "liquidjava.processor.context.RefinedVariable.getType()" because "var" is null
at liquidjava.processor.refinement_checker.TypeChecker.scan (TypeChecker.java:78)
at spoon.reflect.visitor.CtScanner.scan (CtScanner.java:184)
Environment
- LiquidJava version / commit: verifier 0.0.26, Add Element Context to Exceptions #237
- Java version (
java -version): - OS:
Activity