-
Notifications
You must be signed in to change notification settings - Fork 33
Closed
Labels
bugSomething isn't workingSomething isn't working
Description
Reusing Ghost variable names for classes in the same folder generates an error
Example
Currently the following example gives an error:
@ExternalRefinementsFor("java.util.ArrayDeque")
@Ghost("int size")
public interface ArrayDequeRefinements<E> {
}@ExternalRefinementsFor("java.util.ArrayList")
@Ghost("int size")
public interface ListRefinements<E> {
@StateRefinement(to = "size(this) == 0")
void f(); // <-- error here
}The error provided is Sort mismatch at argument #1 for function (declare-fun size (java.util.ArrayDeque) Int) supplied sort is java.util.ArrayList
This error shows up on the function coupled to the first Refinement that references the variable and not on the variable declaration
Intended behavior
Allow different classes to have the same Ghost variable names and disambiguate between them
Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working