Skip to content

Access this.root.value error #25

Description

@CatarinaGamboa

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

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions