Use a fresh receiver for a call on a call result

In a.get().m(), when get() has no return refinement its TARGET metadata
is its own receiver (a), not the value it returns, and m() was checked
against a: "Argument Mismatch Error ... expected Door, got Holder". The
receiver is now a fresh value of get()'s type, in an unknown state,
created once per call.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/CorrectCallResultReceiver.java

@@ -0,0 +1,30 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class CorrectCallResultDoor {
+    @StateRefinement(to = "open(this)")
+    public CorrectCallResultDoor() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+
+    @StateRefinement(to = "closed(this)")
+    public void slam() {}
+}
+
+class CorrectCallResultHolder {
+    private final CorrectCallResultDoor door = new CorrectCallResultDoor();
+
+    CorrectCallResultDoor get() {
+        return door;
+    }
+}
+
+public class CorrectCallResultReceiver {
+    static void use(CorrectCallResultHolder holder) {
+        holder.get().slam();
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorCallResultReceiver.java

@@ -0,0 +1,27 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class ErrorCallResultDoor {
+    @StateRefinement(to = "open(this)")
+    public ErrorCallResultDoor() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}
+
+class ErrorCallResultHolder {
+    private final ErrorCallResultDoor door = new ErrorCallResultDoor();
+
+    ErrorCallResultDoor get() {
+        return door;
+    }
+}
+
+public class ErrorCallResultReceiver {
+    static void use(ErrorCallResultHolder holder) {
+        holder.get().close(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -848,6 +848,21 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
             newCall.putMetadata(Keys.RECEIVER, receiver);
             invocation.putMetadata(Keys.TARGET, receiver);
             return name;
+        } else if (target2 instanceof CtInvocation<?> call
+                && call.getMetadata(Keys.RECEIVER)instanceof RefinedVariable receiver) {
+            invocation.putMetadata(Keys.TARGET, receiver);
+            return receiver.getName();
+        } else if (target2 instanceof CtInvocation<?> call && call.getMetadata(Keys.TARGET) != null
+                && !isReturnValue(call)) {
+            // `a.get().method()` where get() has no return refinement: the call's TARGET is its own receiver (a), not
+            // the value it returns, so the receiver is a fresh value of the call's type, in a state not known here
+            String name = String.format(Formats.FRESH, tc.getContext().getCounter());
+            CtTypeReference<?> type = call.getType();
+            RefinedVariable receiver = tc.getContext().addInstanceToContext(name, type, new Predicate(), call);
+            receiver.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
+            call.putMetadata(Keys.RECEIVER, receiver);
+            invocation.putMetadata(Keys.TARGET, receiver);
+            return name;
         } else if (target2.getMetadata(Keys.TARGET) != null) {
             VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET);
             Optional<Variable> v = target2Vi.getParent();
@@ -857,6 +872,12 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
         return null;
     }
 
+    /** Whether a call's TARGET metadata is the value it returns (set when its return refinement is applied). */
+    private static boolean isReturnValue(CtInvocation<?> call) {
+        return call.getMetadata(Keys.TARGET)instanceof VariableInstance vi
+                && vi.getName().equals(call.getMetadata(Keys.RETURN_VAR_NAME));
+    }
+
     static VariableInstance getTarget(CtElement invocation) {
         if (invocation.getMetadata(Keys.TARGET) != null) {
             return (VariableInstance) invocation.getMetadata(Keys.TARGET);