-
Notifications
You must be signed in to change notification settings - Fork 0
Open
Labels
bugSomething isn't workingSomething isn't working
Description
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;
}
}Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working