False error: array length is not known to be non-negative
Los mantenedores suelen responder en 2 días
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 3/5
- Tiempo estimado
- Medio día
- Aptitud para principiantes
- 55/100
Línea de trabajo
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.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
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.
- Lenguaje dominante
- Java
- Estrellas
- 69
- Forks
- 36
- Merge medio
- 2 d 1 h
- PR fusionados (30 d)
- 35
Preparar el entorno
- Sin Dockerfile ni archivo de Docker Compose
- Tiene una plantilla de pull request
- Leer la guía de contribución
Primeros pasos
- Lee el issue completo y luego la guía de contribución del proyecto.
- Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
- Haz un fork del repositorio y trabaja en una rama.
- Abre un pull request que haga referencia al número del issue.
Más de liquid-java/liquidjava
-
bug
Dificultad 2/5 1-3 horas Aptitud para principiantes 82/100
liquid-java/liquidjava#395 ·
Los mantenedores suelen responder en 2 días
-
Verifier crashes on a comparison or other binary operator whose operand types cannot be resolved (classes not on the classpath)Posiblemente ocupada @CatarinaGamboa la tomó hace 7 días. Abiertobug
Dificultad 2/5 1-3 horas Aptitud para principiantes 72/100
liquid-java/liquidjava#388 ·
Los mantenedores suelen responder en 2 días
-
enhancement
Dificultad 2/5 1-3 horas Aptitud para principiantes 65/100
liquid-java/liquidjava#373 ·
Los mantenedores suelen responder en 2 días
-
Soundness: a local variable with a constant's name shadows the constant (Format.JPG read as local JPG)Posiblemente ocupada @CatarinaGamboa la tomó hace 7 días. Abiertobug
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
liquid-java/liquidjava#321 ·
Los mantenedores suelen responder en 2 días
-
bug
Dificultad 4/5 3-5 días Aptitud para principiantes 20/100
liquid-java/liquidjava#406 ·
Los mantenedores suelen responder en 2 días
Todos los issues de liquid-java/liquidjava
Issues similares
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 72/100
federicoiosue/Omni-Notes#1032 ·
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
unitycatalog/unitycatalog#2025 ·
Los mantenedores suelen responder en 4 días
-
Dificultad 1/5 1-3 horas Aptitud para principiantes 78/100
krizaka/krizaka-notifications#22 ·
Los mantenedores suelen responder en 1 día
-
CommandDispatcher.register returns a node that is not in the tree when the literal is already registeredPosiblemente ocupada @auraseb la tomó hoy. Abierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 83/100
-
ToolCallbackProvider AutoConfiguration does not preserve tool orderPosiblemente ocupada Un pull request vinculado a esta issue está abierto o ya se fusionó. Abiertostatus: waiting-for-triage
Dificultad 2/5 1-3 horas Aptitud para principiantes 79/100
spring-projects/spring-ai#7206 ·
Los mantenedores suelen responder en 2 días