Skip to content

Check typestate calls made directly on a constructor call - #361

Open
CatarinaGamboa wants to merge 1 commit into
mainfrom
fix/336-constructor-receiver
Open

CatarinaGamboa wants to merge 1 commit into
mainfrom
fix/336-constructor-receiver

Conversation

@CatarinaGamboa

Copy link
Copy Markdown
Collaborator

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

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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Soundness: a typestate call chained on a constructor (new X(..).m()) is not checked

1 participant