Access this.root.value error

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;
	}
}

Commencez par reproduire l’erreur signalée avec l’exemple complet de MyStackTest et Node présent dans l’issue, en vous concentrant sur l’analyse de this.root.value. Suivez pourquoi cet accès reçoit une valeur symbolique null ; le travail est terminé lorsque l’exemple ne signale plus l’erreur d’affectation et que la comparaison de valeurs existante reste valide.