Referencing ghost variable names within function parameter refinements should be allowed

[rodrigomilisse]

Currently, referencing Ghost variables within function parameters generates an error

Example

Currently the following example gives an error:

@ExternalRefinementsFor("java.util.ArrayList")
@Ghost("int size")
public interface ListRefinements<E> {

	@StateRefinement(to = "size(this) == 0")
	public void ArrayList();

	public E get(@Refinement("_ < size(this)") int index);
}

	public static void main(String[] args) {
		ArrayList<Integer> list = new ArrayList<>();
		list.get(0); <-- error
	} 

The error provided is Variable 'this' not foundtrue && #index_44 == 0 (#index_44 < size2(this))

This error shows up on the function call that is unable to resolve the ghost variable and not on the refinement definition

Intended behavior

It should be possible to refine method parameters according to Ghost variables and state refinements