False error: array length is not known to be non-negative
メンテナーはふだん 2 日以内に返信
まだ誰も着手していません。
評価
調査の方向性
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
- スター
- 69
- フォーク
- 36
- 平均マージ
- 2日 1時間
- マージ済み PR（30日）
- 35
環境構築
- Dockerfile・Docker Compose ファイルなし
- プルリクエストのテンプレートあり
- コントリビューションガイドを読む
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- 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 が 6 日前に担当しました。 オープン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 が 6 日前に担当しました。 オープンbug
難易度 2/5 1〜3時間 初心者へのやさしさ 78/100
liquid-java/liquidjava#321 ·
メンテナーはふだん 2 日以内に返信
-
bug
難易度 4/5 3〜5日 初心者へのやさしさ 20/100
liquid-java/liquidjava#406 ·
メンテナーはふだん 2 日以内に返信
liquid-java/liquidjava の issue をすべて見る
似ている issue
-
ToolCallbackProvider AutoConfiguration does not preserve tool order対応中かも このイシューにリンクされたプルリクエストがオープン中、またはマージ済みです。 オープンstatus: waiting-for-triage
難易度 2/5 1〜3時間 初心者へのやさしさ 79/100
spring-projects/spring-ai#7206 ·
メンテナーはふだん 2 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 80/100
eclipse-dirigible/dirigible#7958 ·
メンテナーはふだん 1 日以内に返信
-
bug ci sev-6
難易度 2/5 1〜3時間 初心者へのやさしさ 73/100
-
area/cli
難易度 2/5 半日 初心者へのやさしさ 78/100
quarkusio/quarkus#57623 · コメント 1 件 ·
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
jhipster/prettier-java#1113 ·
メンテナーはふだん 2 日以内に返信