Assignment of field to parent field giving error

Bắt đầu với ví dụ MyStackTest được cung cấp và kiểm tra typechecking/LatteTypeChecker.java tại dòng 270, nơi đường dẫn đọc trường dereference permV. Theo dõi cách phép gán cho trường cha được xử lý, sau đó thêm hoặc cập nhật một trường hợp hồi quy để đầu vào này không còn tạo ra NullPointerException, và xác minh hành vi kết quả của checker.

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)