False error: array length is not known to be non-negative
I maintainer di solito rispondono entro 2 giorni
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 3/5
- Tempo stimato
- Mezza giornata
- Idoneità per principianti
- 55/100
Direzione di ricerca
The bug is in how length(x) is encoded for the SMT solver, which the payload does not locate, so start by finding where array length is translated. Use the reproducer's size method with @Refinement("_ >= 0") as the test case. Done when that snippet prints Correct! Passed Verification. and existing tests still pass.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
Impact: correct code is rejected (false error).
Description
length(x) is not known to be non-negative, so the solver picks a negative length. Any refinement that needs length(a) >= 0 must be written out by hand.
Minimal reproducer
import liquidjava.specification.Refinement;
class Len {
@Refinement("_ >= 0")
static int size(int[] names) {
return names.length;
}
}
Expected
Correct! Passed Verification.
Actual (main ad055b49)
Refinement Error: #ret⁰ == length(names) is not a subtype of #ret⁰ >= 0
--> Counterexample: names == ((as const (Array Int Int)) (- 1)) && #ret⁰ == -1
Possible fix
Assume length(x) >= 0 for every array variable when it enters the context, or add the axiom in the SMT translation of length.
- Lingua principale
- Java
- Stelle
- 69
- Fork
- 36
- Merge medio
- 2g 1h
- PR unite (30g)
- 35
Preparare l'ambiente
- Nessun Dockerfile né file Docker Compose
- Ha un modello di pull request
- Leggi la guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di liquid-java/liquidjava
-
bug
Difficoltà 2/5 1-3 ore Idoneità per principianti 82/100
liquid-java/liquidjava#395 ·
I maintainer di solito rispondono entro 2 giorni
-
Verifier crashes on a comparison or other binary operator whose operand types cannot be resolved (classes not on the classpath)Forse già presa @CatarinaGamboa l’ha presa 2 giorni fa. Apertabug
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
liquid-java/liquidjava#388 ·
I maintainer di solito rispondono entro 2 giorni
-
enhancement
Difficoltà 2/5 1-3 ore Idoneità per principianti 65/100
liquid-java/liquidjava#373 ·
I maintainer di solito rispondono entro 2 giorni
-
Soundness: a local variable with a constant's name shadows the constant (Format.JPG read as local JPG)Forse già presa @CatarinaGamboa l’ha presa 2 giorni fa. Apertabug
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
liquid-java/liquidjava#321 ·
I maintainer di solito rispondono entro 2 giorni
-
bug
Difficoltà 4/5 3-5 giorni Idoneità per principianti 20/100
liquid-java/liquidjava#406 ·
I maintainer di solito rispondono entro 2 giorni
Tutte le issue di liquid-java/liquidjava
Issue simili
-
agent-java community triage
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
elastic/apm-agent-java#4594 ·
I maintainer di solito rispondono entro 1 giorno
-
area/plugin good first issue
Difficoltà 2/5 1-3 ore Idoneità per principianti 85/100
kestra-io/plugin-soda#137 ·
-
area/plugin good first issue
Difficoltà 2/5 1-3 ore Idoneità per principianti 82/100
kestra-io/plugin-aws#816 ·
I maintainer di solito rispondono entro 2 giorni
-
area/plugin good first issue
Difficoltà 2/5 1-3 ore Idoneità per principianti 88/100
kestra-io/plugin-kestra#200 ·
I maintainer di solito rispondono entro 1 giorno
-
bug untriaged
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 92/100
opensearch-project/search-relevance#618 ·
I maintainer di solito rispondono entro 3 giorni