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

Aberta
  • Algo errado?
#469 0 comentários 0 reações 0 responsáveis Ver no GitHub

Mantenedores costumam responder em até 2 dias

Ninguém assumiu esta issue ainda.

Avaliação

Dificuldade
3/5
Tempo estimado
1-2 dias
Facilidade para iniciantes
68/100
Tipo de issue
Bug
Clareza
Claramente especificada
Status de atividade
Ativa
Stack de tecnologia
java
Domínio
compilers

Direção de pesquisa

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.”

Escrita pelo modelo de indexação a partir do texto da issue.

Descrição

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

Linguagem predominante
Java
Estrelas
71
Forks
37
Merge médio
1d 19h
PRs com merge (30d)
46

Preparar o ambiente

Primeiros passos

  1. Leia a issue inteira e depois o guia de contribuição do projeto.
  2. Comente na issue dizendo que vai assumir — evita que duas pessoas façam o mesmo trabalho.
  3. Faça um fork do repositório e trabalhe em uma branch.
  4. Abra um pull request que referencie o número da issue.

Mais de liquid-java/liquidjava

Todas as issues de liquid-java/liquidjava

Issues semelhantes

Mais issues de Java

Receba novas issues na sua caixa de entrada

Um resumo curto de issues do GitHub para quem está começando.