Check typestate calls made directly on a constructor call

Fixes #336. In `new T(args).method()` the receiver had no variable instance,
so the method's from-state was never checked. The constructor call now gets
a fresh instance in the state the constructor gives (with its supertypes),
and the call is checked and transitions it like any other receiver.

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

Author: CatarinaGamboa

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

@@ -0,0 +1,26 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"fresh", "used"})
+class CorrectReceiverToken {
+    @StateRefinement(to = "fresh(this)")
+    public CorrectReceiverToken() {}
+
+    @StateRefinement(to = "used(this)")
+    public CorrectReceiverToken(int spent) {}
+
+    @StateRefinement(from = "fresh(this)", to = "used(this)")
+    public void use() {}
+
+    @StateRefinement(from = "used(this)")
+    public void report() {}
+}
+
+public class CorrectConstructorReceiver {
+    static void chained() {
+        new CorrectReceiverToken().use();
+        new CorrectReceiverToken(1).report();
+    }
+}

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

@@ -0,0 +1,25 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"fresh", "used"})
+class ErrorReceiverToken {
+    @StateRefinement(to = "fresh(this)")
+    public ErrorReceiverToken() {}
+
+    @StateRefinement(to = "used(this)")
+    public ErrorReceiverToken(int spent) {}
+
+    @StateRefinement(from = "fresh(this)", to = "used(this)")
+    public void use() {}
+
+    @StateRefinement(from = "used(this)")
+    public void report() {}
+}
+
+public class ErrorConstructorReceiver {
+    static void chained() {
+        new ErrorReceiverToken(1).use(); // Expect: State Refinement Error
+    }
+}

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

@@ -647,6 +647,17 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
             Optional<Variable> v = target2Vi.getParent();
             invocation.putMetadata(Keys.TARGET, target2Vi);
             return v.map(Refined::getName).orElse(target2Vi.getName());
+        } else if (target2 instanceof CtConstructorCall<?> newCall
+                && newCall.getMetadata(Keys.REFINEMENT)instanceof Predicate state) {
+            // `new T(args).method()`: the receiver is a fresh object in the state the constructor gives
+            String name = String.format(Formats.FRESH, tc.getContext().getCounter());
+            CtTypeReference<?> type = newCall.getType();
+            RefinedVariable receiver = tc.getContext().addInstanceToContext(name, type,
+                    state.substituteVariable(Keys.THIS, name).substituteVariable(Keys.WILDCARD, name), newCall);
+            receiver.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
+            newCall.putMetadata(Keys.TARGET, receiver);
+            invocation.putMetadata(Keys.TARGET, receiver);
+            return name;
         }
         return null;
     }