External specs: a @StateSet declared later in the file is not found by an interface earlier in it

Aperta
  • Qualcosa non va?
#452 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub

I maintainer di solito rispondono entro 2 giorni

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
4/5
Tempo stimato
3-5 giorni
Idoneità per principianti
58/100
Tipo di issue
Bug
Chiarezza
Specificata chiaramente
Stato di attività
Attiva
Stack tecnologico
java
Ambito
compilers, testing-qa

Direzione di ricerca

Start with the verifier code that resolves @StateSet declarations and the V32_StateSetDeclaredLater probe in liquid-java/co-specification. Trace why a state declared in a later external refinement interface is unavailable to an earlier interface, then run the probe before and after the change. Done means the reproducer verifies successfully regardless of declaration order.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

When one spec file holds external refinements for several classes of a hierarchy, the interface that declares the @StateSet has to come first in the file. If an interface earlier in the file uses the states, verification fails with Not Found Error: Ghost '...' could not be found, even though the declaration is in the same file. Declaration order should not matter.

Minimal reproducer

FrameRefinements.java:

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

@ExternalRefinementsFor("java.awt.Frame")
public interface FrameRefinements {
    @StateRefinement(to = "notDisplayable(this)")
    void Frame();

    @StateRefinement(from = "notDisplayable(this)")
    void setUndecorated(boolean undecorated);
}

@ExternalRefinementsFor("java.awt.Window")
@StateSet({"notDisplayable", "displayable"})     // declared here, after its first use above
interface WindowRefinements {
    @StateRefinement(to = "displayable(this)")
    void pack();
}

Client.java (correct code):

import java.awt.Frame;

public class Client {
    public static void main(String[] args) {
        Frame f = new Frame();
        f.setUndecorated(true);
        f.pack();
    }
}

Found:

Not Found Error: Ghost 'java.awt.Frame.notDisplayable' could not be found
    @StateRefinement(to = "notDisplayable(this)")

Expected: Correct! Passed Verification., as when the WindowRefinements interface is moved above FrameRefinements (nothing else changed).

Real-world scenario

Frame.setUndecorated throws IllegalComponentStateException: The frame is displayable. once the frame has a peer, and pack()/setVisible(true) (declared in java.awt.Window) create it. A spec for this, used to catch real bugs like calling setUndecorated(true) after pack() in a game window, needs interfaces for Window, Frame, Component and JFrame. The state must be declared on Window, since a state declared on Frame cannot be used by Window.pack() (expected Frame, got Window, which seems right). The natural order, with the class being specified first, then fails as above.

Verifier commit 1a506fe. Reproducer as a verifier probe: liquid-java/co-specification verifier-probes/V32_StateSetDeclaredLater.

Lingua principale
Java
Stelle
71
Fork
37
Merge medio
1g 19h
PR unite (30g)
46

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di liquid-java/liquidjava

Tutte le issue di liquid-java/liquidjava

Issue simili

Altre issue su Java

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.