False error: array length is not known to be non-negative
Mantenedores costumam responder em até 2 dias
Ninguém assumiu esta issue ainda.
Avaliação
- Dificuldade
- 3/5
- Tempo estimado
- Meio dia
- Facilidade para iniciantes
- 55/100
Direção de pesquisa
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.
Escrita pelo modelo de indexação a partir do texto da issue.
Descrição
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.
- Linguagem predominante
- Java
- Estrelas
- 67
- Forks
- 36
- Merge médio
- 2d 1h
- PRs com merge (30d)
- 35
Preparar o ambiente
- Sem Dockerfile nem arquivo Docker Compose
- Tem um modelo de pull request
- Ler o guia de contribuição
Primeiros passos
- Leia a issue inteira e depois o guia de contribuição do projeto.
- Comente na issue dizendo que vai assumir — evita que duas pessoas façam o mesmo trabalho.
- Faça um fork do repositório e trabalhe em uma branch.
- Abra um pull request que referencie o número da issue.
Mais de liquid-java/liquidjava
-
bug
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 82/100
liquid-java/liquidjava#395 ·
Mantenedores costumam responder em até 2 dias
-
Verifier crashes on a comparison or other binary operator whose operand types cannot be resolved (classes not on the classpath)Talvez já em andamento @CatarinaGamboa assumiu há 1 dia. Abertabug
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 72/100
liquid-java/liquidjava#388 ·
Mantenedores costumam responder em até 2 dias
-
enhancement
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 65/100
liquid-java/liquidjava#373 ·
Mantenedores costumam responder em até 2 dias
-
Soundness: a local variable with a constant's name shadows the constant (Format.JPG read as local JPG)Talvez já em andamento @CatarinaGamboa assumiu há 1 dia. Abertabug
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 78/100
liquid-java/liquidjava#321 ·
Mantenedores costumam responder em até 2 dias
-
bug
Dificuldade 4/5 3-5 dias Facilidade para iniciantes 20/100
liquid-java/liquidjava#406 ·
Mantenedores costumam responder em até 2 dias
Todas as issues de liquid-java/liquidjava
Issues semelhantes
-
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 62/100
NationalSecurityAgency/ghidra#9884 ·
Mantenedores costumam responder em até 2 dias
-
Status: Pending Review Type: Feature Request
Dificuldade 1/5 Menos de uma hora Facilidade para iniciantes 82/100
OpenRefine/OpenRefine#8019 ·
Mantenedores costumam responder em até 1 dia
-
`timer` rule rejects dates the engine acceptsTalvez já em andamento @MFA-G assumiu hoje. Abertabug ready
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 72/100
camunda/bpmnlint-plugin-camunda-compat#281 · 3 comentários ·
Mantenedores costumam responder em até 1 dia
-
status: waiting-for-triage
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 72/100
-
bug
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 62/100