Check typestate calls made directly on a constructor call

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;
     }