Assignment of field to parent field giving error

从提供的 MyStackTest 示例开始，检查 typechecking/LatteTypeChecker.java 的第 270 行，其中字段读取路径会对 permV 进行解引用。跟踪父字段赋值的处理方式，然后添加或更新一个回归用例，使该输入不再产生 NullPointerException，并验证 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)