False error: array length is not known to be non-negative
Les mainteneurs répondent en général sous 2 jours
Personne n'a encore pris cette issue.
Évaluation
- Difficulté
- 3/5
- Temps estimé
- Une demi-journée
- Accessibilité débutants
- 55/100
Piste de recherche
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.
Rédigé par le modèle d'indexation à partir du texte de l'issue.
Description
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.
- Langage dominant
- Java
- Étoiles
- 69
- Forks
- 36
- Merge moyen
- 2 j 1 h
- PR mergées (30 j)
- 35
Préparer son environnement
- Aucun Dockerfile ni fichier Docker Compose
- Propose un modèle de pull request
- Lire le guide de contribution
Par où commencer
- Lisez l'issue en entier, puis le guide de contribution du projet.
- Signalez en commentaire que vous la prenez — cela évite que deux personnes fassent le même travail.
- Forkez le dépôt et travaillez sur une branche.
- Ouvrez une pull request qui référence le numéro de l'issue.
Autres issues de liquid-java/liquidjava
-
bug
Difficulté 2/5 1-3 heures Accessibilité débutants 82/100
liquid-java/liquidjava#395 ·
Les mainteneurs répondent en général sous 2 jours
-
Verifier crashes on a comparison or other binary operator whose operand types cannot be resolved (classes not on the classpath)Peut-être pris @CatarinaGamboa l’a pris il y a 1 jour. Ouvertebug
Difficulté 2/5 1-3 heures Accessibilité débutants 72/100
liquid-java/liquidjava#388 ·
Les mainteneurs répondent en général sous 2 jours
-
enhancement
Difficulté 2/5 1-3 heures Accessibilité débutants 65/100
liquid-java/liquidjava#373 ·
Les mainteneurs répondent en général sous 2 jours
-
Soundness: a local variable with a constant's name shadows the constant (Format.JPG read as local JPG)Peut-être pris @CatarinaGamboa l’a pris il y a 1 jour. Ouvertebug
Difficulté 2/5 1-3 heures Accessibilité débutants 78/100
liquid-java/liquidjava#321 ·
Les mainteneurs répondent en général sous 2 jours
-
bug
Difficulté 4/5 3-5 jours Accessibilité débutants 20/100
liquid-java/liquidjava#406 ·
Les mainteneurs répondent en général sous 2 jours
Toutes les issues de liquid-java/liquidjava
Issues similaires
-
Difficulté 2/5 1-3 heures Accessibilité débutants 72/100
Les mainteneurs répondent en général sous 1 jour
-
bug new windows
Difficulté 2/5 1-3 heures Accessibilité débutants 62/100
Les mainteneurs répondent en général sous 1 jour
-
iOS podspec depends on `React-Codegen`, which resolves to an unrelated pod on CocoaPods trunkOuverte
Difficulté 2/5 1-3 heures Accessibilité débutants 75/100
GantMan/jail-monkey#380 ·
-
Difficulté 2/5 1-3 heures Accessibilité débutants 72/100
objectionary/jucs#145 ·
Les mainteneurs répondent en général sous 1 jour
-
Difficulté 2/5 1-3 heures Accessibilité débutants 82/100
objectionary/lints#1559 ·
Les mainteneurs répondent en général sous 2 jours