From b2cf676d489007cc16e7e5c7f6fc5ded9ebfe378 Mon Sep 17 00:00:00 2001
From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com>
Date: Tue, 6 Oct 2026 20:32:27 +0100
Subject: [PATCH] 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>
---
 .../testSuite/CorrectConstructorReceiver.java | 26 +++++++++++++++++++
 .../testSuite/ErrorConstructorReceiver.java   | 25 ++++++++++++++++++
 .../object_checkers/AuxStateHandler.java      | 11 ++++++++
 3 files changed, 62 insertions(+)
 create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectConstructorReceiver.java
 create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorConstructorReceiver.java

diff --git a/liquidjava-example/src/main/java/testSuite/CorrectConstructorReceiver.java b/liquidjava-example/src/main/java/testSuite/CorrectConstructorReceiver.java
new file mode 100644
index 00000000..e4ad3f3a
--- /dev/null
+++ b/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();
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorConstructorReceiver.java b/liquidjava-example/src/main/java/testSuite/ErrorConstructorReceiver.java
new file mode 100644
index 00000000..92552834
--- /dev/null
+++ b/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
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
index e38cdb0d..2844b21f 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
+++ b/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;
     }