Access this.root.value error

首先，使用 issue 中完整的 MyStackTest 和 Node 示例重现报告的错误，重点分析 this.root.value。追踪该访问为何会接收到 null 符号值；当示例不再报告赋值错误且现有的值比较仍然有效时，即可完成。

Error when accessing this.root.value.

@Unique Node test(@Borrowed Node n){
    Object value1 = n.value;
    Object value2 = this.root.value;
    if (value1.equals(value2)) {
        return n;
    } else {
        return null;
    }
}

Error:
Local variable value2 = this.root.value has assignment with null symbolic value

Let's try to fix it.

Full example to test:

package examples;
import specification.Borrowed;
import specification.Free;
import specification.Unique;


public class MyStackTest {
    @Unique Node root;		
            
    public MyStackTest(@Free Node root) {
        this.root = root;
    }

    @Unique Node test(@Borrowed Node n){
        Object value1 = n.value;
        Object value2 = this.root.value;
        if (value1.equals(value2)) {
            return n;
        } else {
            return null;
        }
    }
}

/**
 * Node class for the stack example
 * Uses @Unique annotations to specify that the value and next fields are unique
 * in the scope of the Node class
 * @author catarina gamboa
 *
 */
class Node {
	
	@Unique Object value;
	@Unique Node next;

	/**
	 * Constructor for the Node class using @Free value and next nodes
	 * @param value
	 * @param next
	 */
	public Node (@Free Object value, @Free Node next) {
		this.value = value;
		this.next = next;
	}
}