Inconsistent Function Invocation Qualified Names

[rcosta358]

Description

Refined class ghost invocations are not always assigned consistent qualified names.

When a ghost function is called on an instance of a refined class, the invocation should use the qualified name associated with that instance's class. However, in some cases, LiquidJava uses the qualified name of the class where the instance is being used instead.

Because of this, equivalent ghost invocations may be represented with different qualified names. As a workaround for the VCFunctionSubstitution, the FunctionInvocation.equals() currently compares only simple names, but this can be problematic.

Minimal reproducer

public class Example {
  public static void main(String[] args) {
    Stack<Integer> stack = new Stack<>(); // java.util.Stack.size()
    if (stack.empty()) { // com.example.Example.size()
      stack.push(1); // java.util.Stack.size()
    }
    stack.pop(); // java.util.Stack.size()
  }
}

Environment

• LiquidJava version / commit: 0.0.27
• Java version: 20
• OS: macOS 26