Check calls on a constructor call whose constructor has refined parameters

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

@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"unbound", "bound"})
+class CorrectRefinedArgListener {
+    @StateRefinement(to = "unbound(this)")
+    public CorrectRefinedArgListener() {}
+
+    @StateRefinement(to = "bound(this)")
+    public CorrectRefinedArgListener(@Refinement("0 <= _ && _ <= 65535") int port) {}
+
+    @StateRefinement(from = "bound(this)")
+    public void accept() {}
+}
+
+public class CorrectConstructorReceiverRefinedArgument {
+    static void chained() {
+        new CorrectRefinedArgListener(8080).accept();
+    }
+}

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

@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"unbound", "bound"})
+class ErrorRefinedArgListener {
+    @StateRefinement(to = "unbound(this)")
+    public ErrorRefinedArgListener() {}
+
+    @StateRefinement(to = "bound(this)")
+    public ErrorRefinedArgListener(@Refinement("0 <= _ && _ <= 65535") int port) {}
+
+    @StateRefinement(from = "unbound(this)", to = "bound(this)")
+    public void bind() {}
+}
+
+public class ErrorConstructorReceiverRefinedArgument {
+    static void chained() {
+        new ErrorRefinedArgListener(8080).bind(); // Expect: State Refinement Error
+    }
+}

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

@@ -744,24 +744,30 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
             }
 
             return name;
-        } else if (target2.getMetadata(Keys.TARGET) != null) {
-            // invocation is in
-            // who did put the metadata here then?
-            VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET);
-            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.RECEIVER)instanceof RefinedVariable receiver) {
+            invocation.putMetadata(Keys.TARGET, receiver);
+            return receiver.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
+            // `new T(args).method()`: the receiver is a fresh object in the state the constructor gives. Checked
+            // before the TARGET metadata, which a constructor with refined parameters sets to its (void) return value
             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);
+            newCall.putMetadata(Keys.RECEIVER, receiver);
             invocation.putMetadata(Keys.TARGET, receiver);
             return name;
+        } else if (target2.getMetadata(Keys.TARGET) != null) {
+            // invocation is in
+            // who did put the metadata here then?
+            VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET);
+            Optional<Variable> v = target2Vi.getParent();
+            invocation.putMetadata(Keys.TARGET, target2Vi);
+            return v.map(Refined::getName).orElse(target2Vi.getName());
         }
         return null;
     }

liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java

@@ -4,6 +4,7 @@ public final class Keys {
     public static final String REFINEMENT = "refinement";
     public static final String REFINEMENT_SAT_CHECK = "refinement_sat_check";
     public static final String TARGET = "target";
+    public static final String RECEIVER = "receiver";
     public static final String RETURN_VAR_NAME = "return_var_name";
     public static final String THIS = "this";
     public static final String WILDCARD = "_";