Skip to content

Commit 321a732

Browse files
Check typestate calls made directly on a constructor call (#361)
Fixes #336. ## Problem `new Token(1).use()` passed although `Token(int)` leaves the object in `used` and `use()` requires `fresh`; the same call through a local was reported. `prepareInvocationTarget` only knew variable reads and targets that already had an instance, so a constructor-call receiver had none and `checkTargetChanges` skipped it. Real code does this often (`new ServerSocket(port).accept()`, `new IOException(msg).initCause(e)`). ## Change `AuxStateHandler.prepareInvocationTarget`: when the target is a constructor call carrying its state (the constructor's to-state, or the class's default state, as `getConstructorInvocationRefinements` already records), it creates a fresh variable instance in that state, records the type's supertypes on it (so a spec on a supertype applies), and makes it the invocation's target. The usual from-state check and transition then apply. ## Tests - `ErrorConstructorReceiver`: `new ErrorReceiverToken(1).use()` gives `found used(#fresh) but expected fresh(#fresh)`; passed on main. - `CorrectConstructorReceiver`: `new …().use()` and `new …(1).report()` pass. - `mvn test` passes. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
1 parent 2e8d227 commit 321a732

3 files changed

Lines changed: 62 additions & 0 deletions

File tree

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
@StateSet({"fresh", "used"})
7+
class CorrectReceiverToken {
8+
@StateRefinement(to = "fresh(this)")
9+
public CorrectReceiverToken() {}
10+
11+
@StateRefinement(to = "used(this)")
12+
public CorrectReceiverToken(int spent) {}
13+
14+
@StateRefinement(from = "fresh(this)", to = "used(this)")
15+
public void use() {}
16+
17+
@StateRefinement(from = "used(this)")
18+
public void report() {}
19+
}
20+
21+
public class CorrectConstructorReceiver {
22+
static void chained() {
23+
new CorrectReceiverToken().use();
24+
new CorrectReceiverToken(1).report();
25+
}
26+
}
Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
@StateSet({"fresh", "used"})
7+
class ErrorReceiverToken {
8+
@StateRefinement(to = "fresh(this)")
9+
public ErrorReceiverToken() {}
10+
11+
@StateRefinement(to = "used(this)")
12+
public ErrorReceiverToken(int spent) {}
13+
14+
@StateRefinement(from = "fresh(this)", to = "used(this)")
15+
public void use() {}
16+
17+
@StateRefinement(from = "used(this)")
18+
public void report() {}
19+
}
20+
21+
public class ErrorConstructorReceiver {
22+
static void chained() {
23+
new ErrorReceiverToken(1).use(); // Expect: State Refinement Error
24+
}
25+
}

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -719,6 +719,17 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
719719
Optional<Variable> v = target2Vi.getParent();
720720
invocation.putMetadata(Keys.TARGET, target2Vi);
721721
return v.map(Refined::getName).orElse(target2Vi.getName());
722+
} else if (target2 instanceof CtConstructorCall<?> newCall
723+
&& newCall.getMetadata(Keys.REFINEMENT)instanceof Predicate state) {
724+
// `new T(args).method()`: the receiver is a fresh object in the state the constructor gives
725+
String name = String.format(Formats.FRESH, tc.getContext().getCounter());
726+
CtTypeReference<?> type = newCall.getType();
727+
RefinedVariable receiver = tc.getContext().addInstanceToContext(name, type,
728+
state.substituteVariable(Keys.THIS, name).substituteVariable(Keys.WILDCARD, name), newCall);
729+
receiver.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
730+
newCall.putMetadata(Keys.TARGET, receiver);
731+
invocation.putMetadata(Keys.TARGET, receiver);
732+
return name;
722733
}
723734
return null;
724735
}

0 commit comments

Comments
 (0)