False error: array length is not known to be non-negative
維護者通常 2 天內回覆
還沒有人認領這個 Issue。
評估
研究方向
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.
由索引模型根據 Issue 內容生成。
描述
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.
- 主要語言
- Java
- 星號
- 67
- 分支
- 36
- 平均合併
- 2 天 2 小時
- 30 天內合併 PR
- 34
環境準備
- 沒有 Dockerfile 或 Docker Compose 檔案
- 有 Pull Request 範本
- 閱讀貢獻指南
從這裡開始
- 先讀完整個 Issue，再讀專案的貢獻指南。
- 在 Issue 下留言說明你要接手 —— 這能避免兩個人做同樣的事。
- Fork 儲存庫，在一個分支上完成修改。
- 送出 Pull Request，並在描述裡引用這個 Issue 編號。
liquid-java/liquidjava 的其他 Issue
-
bug
難度 2/5 1-3 小時 新手友好度 82/100
liquid-java/liquidjava#395 ·
維護者通常 2 天內回覆
-
Verifier crashes on a comparison or other binary operator whose operand types cannot be resolved (classes not on the classpath)可能已有人在做 @CatarinaGamboa 於 1 天前認領。 未關閉bug
難度 2/5 1-3 小時 新手友好度 72/100
liquid-java/liquidjava#388 ·
維護者通常 2 天內回覆
-
enhancement
難度 2/5 1-3 小時 新手友好度 65/100
liquid-java/liquidjava#373 ·
維護者通常 2 天內回覆
-
Soundness: a local variable with a constant's name shadows the constant (Format.JPG read as local JPG)可能已有人在做 @CatarinaGamboa 於 1 天前認領。 未關閉bug
難度 2/5 1-3 小時 新手友好度 78/100
liquid-java/liquidjava#321 ·
維護者通常 2 天內回覆
-
bug
難度 4/5 3-5 天 新手友好度 40/100
liquid-java/liquidjava#405 ·
維護者通常 2 天內回覆
查看 liquid-java/liquidjava 的全部 Issue
相似的 Issue
-
status: waiting-for-triage
難度 2/5 1-3 小時 新手友好度 72/100
-
bug
難度 2/5 1-3 小時 新手友好度 62/100
-
難度 2/5 1-3 小時 新手友好度 74/100
維護者通常 1 天內回覆
-
AOT compilation fails for derived delete queries returning Set可能已有人在做 @ryujungkyun 今天認領。 未關閉status: waiting-for-triage
難度 2/5 1-3 小時 新手友好度 72/100
spring-projects/spring-data-jpa#4387 ·
維護者通常 3 天內回覆
-
難度 2/5 1-3 小時 新手友好度 72/100
apache/rocketmq-dashboard#6636 ·
維護者通常 3 天內回覆