Hacktoberfest 2026: le issue che i maintainer hanno segnato per ottobre, aperte e adatte ai principianti. Sfoglia le issue Hacktoberfest

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

Aperta
  • Qualcosa non va?
#316 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
62/100
Tipo di issue
Bug
Chiarezza
Specificata chiaramente
Stato di attività
Attiva
Stack tecnologico
java
Ambito
compilers, testing-qa

Direzione di ricerca

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.

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

Descrizione

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.

Lingua principale
Java
Stelle
67
Fork
36
Merge medio
4g 17h
PR unite (30g)
7

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.