Hacktoberfest 2026 : les issues que les mainteneurs ont marquées pour octobre, ouvertes et accessibles aux débutants. Parcourir les issues Hacktoberfest

Reading a field of a class declared later in the file loses its refinement

Ouverte
  • Quelque chose ne va pas ?
#316 0 commentaires 0 réactions 0 personnes assignées Voir sur GitHub

Les mainteneurs répondent en général sous 2 jours

Personne n'a encore pris cette issue.

Évaluation

Difficulté
4/5
Temps estimé
3-5 jours
Accessibilité débutants
62/100
Type d'issue
Bug
Clarté
Clairement spécifiée
Activité
Active
Stack technique
java
Domaine
compilers, testing-qa

Piste de recherche

Start with RefinementTypeChecker.visitCtField and visitCtFieldRead, which the issue identifies as the source-order context handling path. Use the supplied ReadBefore reproducer to confirm the false “not enough information” error, then compare it with the version where Job is declared earlier. Done means the reproducer reports “Correct! Passed Verification.” and reads still work when the class is declared later.

Rédigé par le modèle d'indexation à partir du texte de l'issue.

Description

bug

Description

Reading a field of an object whose class is declared later in the file does not pick up the field's refinement, so a correct program fails with a false "not enough information" error. Writes to such fields are handled by #314 (fixing #308); reads are not.

Minimal reproducer

import liquidjava.specification.Refinement;

public class ReadBefore {
    private final Job job = new Job();

    @Refinement("_ >= 0")
    public int get() { return job.port; }

    static class Job { @Refinement("_ >= 0") int port; }
}

Expected

Correct! Passed Verification.

Actual

Refinement Error: true is not a subtype of #ret² >= 0
5 |     public int get() { return job.port; }
  |                        ^^^^^^^^^^^^^^^^
 --> Not enough information to prove the expected refinement. Add a refinement or condition to constrain it.

Moving Job above get makes it pass.

Cause

Fields enter the context only in the second pass (RefinementTypeChecker.visitCtField), in source order. When job.port is read, this#port is not in context yet, so visitCtFieldRead falls through to new Predicate() (no information).

Reproduced on main at fbfb4e23 (liquidjava-verifier 0.0.35), and on the #314 branch.

Langage dominant
Java
Étoiles
67
Forks
36
Merge moyen
4 j 17 h
PR mergées (30 j)
7

Préparer son environnement

Par où commencer

  1. Lisez l'issue en entier, puis le guide de contribution du projet.
  2. Signalez en commentaire que vous la prenez — cela évite que deux personnes fassent le même travail.
  3. Forkez le dépôt et travaillez sur une branche.
  4. Ouvrez une pull request qui référence le numéro de l'issue.

Autres issues de liquid-java/liquidjava

Toutes les issues de liquid-java/liquidjava

Issues similaires

Plus d'issues Java

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.