Skip to content

Similar Ghost Variable names in different classes should be allowed #42

@rodrigomilisse

Description

@rodrigomilisse

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 working

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions