False error: @StateSet on a nested class gives "Argument Mismatch Error: ... expected Inner, got Inner"

Offen
  • Stimmt etwas nicht?
#469 0 Kommentare 0 Reaktionen 0 zugewiesene Personen Auf GitHub ansehen

Maintainer antworten meist innerhalb von 2 Tagen

Dieses Issue hat noch niemand übernommen.

Bewertung

Schwierigkeit
3/5
Geschätzter Aufwand
1-2 Tage
Anfängerfreundlichkeit
68/100
Issue-Typ
Bug
Klarheit
Klar beschrieben
Aktivitätsstatus
Aktiv
Tech-Stack
java
Bereich
compilers

Rechercherichtung

Start with TypeChecker.createStateGhost, then follow how GhostFunction and Utils handle the nested-class name Outer$Inner; Expression.throwArgumentMismatchError explains the reported type mismatch. Reproduce using the issue's Java example and compare with the top-level Inner case; done when the nested-class example verifies with “Correct! Passed Verification.”

Vom Indexierungsmodell aus dem Issue-Text verfasst.

Beschreibung

bug error messages

Impact: typestates on a nested class cannot be used: every state refinement of it fails with a self-contradictory message (expected Inner, got Inner) and no source location. The same class at top level verifies.

Minimal reproducer

import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

public class Outer {
    @StateSet({"fresh", "ready"})
    static class Inner {
        @StateRefinement(to = "ready(this)")
        public Inner() {}

        @StateRefinement(from = "ready(this)", to = "fresh(this)")
        public void use() {}
    }

    static void ok() {
        Inner i = new Inner();
        i.use();
    }
}

Expected: Correct! Passed Verification., as for the same Inner as a top-level class.

Actual (main @ 0053074e; this is the whole output, with no code snippet):

Argument Mismatch Error: Argument '#this_1' and its respective parameter of ghost 'Outer$Inner.state1' types are incompatible: expected Inner, got Inner

Cause. TypeChecker.createStateGhost gives the stateN ghost the parameter type type.getSimpleName() (Inner). GhostFunction swaps that for the prefix only when it equals Utils.getSimpleName(prefix), which splits on . only, so for Outer$Inner it is Outer$Inner and the swap does not happen. The parameter type stays an unresolved reference to Inner, which is neither equal to nor a supertype of Outer$Inner in Expression.throwArgumentMismatchError; both print as Inner. Related: the $ vs . naming of nested classes also breaks @Ghost on them (Z3 sort mismatch, #467).

🤖 Generated with Claude Code

Vorherrschende Sprache
Java
Sterne
71
Forks
37
Ø Merge
1 T. 19 Std.
Gemergte PRs (30 T.)
46

Entwicklungsumgebung

Erste Schritte

  1. Lesen Sie das ganze Issue und danach den Beitragsleitfaden des Projekts.
  2. Schreiben Sie ins Issue, dass Sie es übernehmen — das erspart doppelte Arbeit.
  3. Forken Sie das Repository und arbeiten Sie in einem Branch.
  4. Öffnen Sie einen Pull Request, der die Issue-Nummer nennt.

Mehr aus liquid-java/liquidjava

Alle Issues in liquid-java/liquidjava

Ähnliche Issues

Weitere Issues zu Java

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.