-
Notifications
You must be signed in to change notification settings - Fork 0
Open
Labels
bugSomething isn't workingSomething isn't working
Description
Code issuing an error of NullPointerException
import java.util.Iterator;
import specification.Unique;
public class MyStackTest {
@Unique int[] a;
@Unique int size;
private class ReverseArrayIterator implements Iterator<Integer> {
public @Unique int i = size - 1;
//(true >> this.i >= 0 -> return )
@Override
public boolean hasNext() { return i >= 0; }
//(this.i >= 0 >> this.i == old(this.i) - 1)
@Override
public Integer next() { return a[i--]; }
}
}
Error message:
Exception in thread "main" java.lang.NullPointerException: Cannot invoke "context.UniquenessAnnotation.isGreaterEqualThan(context.Uniqueness)" because "permV" is null
at typechecking.LatteTypeChecker.visitCtFieldRead(LatteTypeChecker.java:270)
at spoon.support.reflect.code.CtFieldReadImpl.accept(CtFieldReadImpl.java:18)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:194)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:184)
at spoon.reflect.visitor.CtScanner.visitCtBinaryOperator(CtScanner.java:312)
at typechecking.LatteTypeChecker.visitCtBinaryOperator(LatteTypeChecker.java:572)
at spoon.support.reflect.code.CtBinaryOperatorImpl.accept(CtBinaryOperatorImpl.java:34)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:194)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:184)
at spoon.reflect.visitor.CtScanner.visitCtField(CtScanner.java:436)
at spoon.support.reflect.declaration.CtFieldImpl.accept(CtFieldImpl.java:53)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:194)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:184)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:149)
at spoon.reflect.visitor.CtScanner.visitCtClass(CtScanner.java:357)
at typechecking.LatteTypeChecker.visitCtClass(LatteTypeChecker.java:53)
at spoon.support.reflect.declaration.CtClassImpl.accept(CtClassImpl.java:63)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:194)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:184)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:149)
at spoon.reflect.visitor.CtScanner.visitCtClass(CtScanner.java:357)
at typechecking.LatteTypeChecker.visitCtClass(LatteTypeChecker.java:53)
at spoon.support.reflect.declaration.CtClassImpl.accept(CtClassImpl.java:63)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:194)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:184)
at spoon.reflect.visitor.CtScanner.scan(CtScanner.java:149)
at spoon.reflect.visitor.CtScanner.visitCtPackage(CtScanner.java:679)
at spoon.support.reflect.declaration.CtPackageImpl.accept(CtPackageImpl.java:82)
at typechecking.LatteProcessor.process(LatteProcessor.java:31)
at typechecking.LatteProcessor.process(LatteProcessor.java:1)
at spoon.support.visitor.ProcessingVisitor.scan(ProcessingVisitor.java:72)
at spoon.support.QueueProcessingManager.process(QueueProcessingManager.java:118)
at spoon.support.QueueProcessingManager.process(QueueProcessingManager.java:132)
at api.App.launcher(App.java:90)
at api.App.main(App.java:31)
Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working