False error in external specs: a @Ghost the constructor does not set gives "Ghost 'old' could not be found" at the next from-only call
Les mainteneurs répondent en général sous 2 jours
Personne n'a encore pris cette issue.
Évaluation
- Difficulté
- 4/5
- Temps estimé
- 1-2 jours
- Accessibilité débutants
- 58/100
Piste de recherche
Start with the external refinement spec and client in the minimal reproducer, then trace how the external @Ghost declaration is handled when checking the constructor and the following canUndo() call. Compare that path with the in-source example described in the issue. Done means the reproducer reports “Correct! Passed Verification.” while preserving the reported behavior for the other examples.
Rédigé par le modèle d'indexation à partir du texte de l'issue.
Description
Impact: adding a @Ghost to an external spec breaks correct programs, unless every constructor sets the ghost. The error names a ghost called old, which is internal and not in the spec.
Minimal reproducer (an external spec and a client, in one directory)
// EditRefinements.java
@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit")
@StateSet({"done", "undone"})
@Ghost("int supported")
public interface EditRefinements {
@StateRefinement(to = "done(this)")
void AbstractUndoableEdit();
@StateRefinement(from = "done(this)")
boolean canUndo();
}
// Client.java
public class Client {
public static void main(String[] args) {
AbstractUndoableEdit e = new AbstractUndoableEdit();
e.canUndo();
}
}
Expected: Correct! Passed Verification.
Actual (main @ f7f366c, and 1a506fe):
Not Found Error: Ghost 'old' could not be found
The same shape written in-source (an annotated class with the same @Ghost) verifies. So does the external spec when the constructor's to also sets the ghost: to = "done(this) && supported(this) == 0".
Real-world scenario. I was writing a spec for javax.management.modelmbean.RequiredModelMBean with a ghost to refuse load()/store(), which always throw; from = "false" doesn't work (#449). With the ghost unset, every correct call such as m.setModelMBeanInfo(info) failed with this error.
- Langage dominant
- Java
- Étoiles
- 71
- Forks
- 37
- Merge moyen
- 1 j 19 h
- PR mergées (30 j)
- 57
Préparer son environnement
- Aucun Dockerfile ni fichier Docker Compose
- Propose un modèle de pull request
- Lire le guide de contribution
Par où commencer
- Lisez l'issue en entier, puis le guide de contribution du projet.
- Signalez en commentaire que vous la prenez — cela évite que deux personnes fassent le même travail.
- Forkez le dépôt et travaillez sur une branche.
- Ouvrez une pull request qui référence le numéro de l'issue.
Autres issues de liquid-java/liquidjava
-
Difficulté 2/5 1-3 heures Accessibilité débutants 72/100
liquid-java/liquidjava#443 ·
Les mainteneurs répondent en général sous 2 jours
-
bug real-world-finding
Difficulté 2/5 1-3 heures Accessibilité débutants 82/100
liquid-java/liquidjava#395 ·
Les mainteneurs répondent en général sous 2 jours
-
enhancement
Difficulté 2/5 1-3 heures Accessibilité débutants 65/100
liquid-java/liquidjava#373 ·
Les mainteneurs répondent en général sous 2 jours
-
External specs: a @StateSet declared later in the file is not found by an interface earlier in itOuverte
Difficulté 4/5 3-5 jours Accessibilité débutants 58/100
liquid-java/liquidjava#452 ·
Les mainteneurs répondent en général sous 2 jours
-
Difficulté 4/5 3-5 jours Accessibilité débutants 52/100
liquid-java/liquidjava#451 ·
Les mainteneurs répondent en général sous 2 jours
Toutes les issues de liquid-java/liquidjava
Issues similaires
-
Difficulté 2/5 1-3 heures Accessibilité débutants 82/100
Les mainteneurs répondent en général sous 1 jour
-
Difficulté 1/5 Moins d'une heure Accessibilité débutants 88/100
quarkusio/quarkus-agent-mcp#302 ·
Les mainteneurs répondent en général sous 2 jours
-
build
Difficulté 1/5 Moins d'une heure Accessibilité débutants 85/100
MetricsHub/metricshub-community#1472 ·
Les mainteneurs répondent en général sous 1 jour
-
Difficulté 2/5 1-3 heures Accessibilité débutants 82/100
Les mainteneurs répondent en général sous 1 jour
-
IdentityArrayObjectSet iterator remove may throw ArrayIndexOutOfBoundsExceptionPeut-être pris @jiteshkhatri11 l’a pris aujourd’hui. Ouverte
Difficulté 2/5 1-3 heures Accessibilité débutants 72/100
javapathfinder/jpf-core#660 · 1 commentaire ·