Skip to content

Update CIL for changes to for-loop expression locations #1930

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sim642 merged 2 commits into from
Feb 4, 2026
Merged

Update CIL for changes to for-loop expression locations #1930

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
aad159d
Update dune cram tests affected by more precise for-loop exp locs
karoliineh Jan 21, 2026
c3488ab
Update CIL for improved for loop expression locations
sim642 Feb 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion goblint.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
pin-depends: [
[ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#e21285af8f4408ed5354b1674dab840c43e84712" ]
[ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#abe64c5705d939b34bf08a186661fce4efcbda53" ]
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
[ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
]
Expand Down
2 changes: 1 addition & 1 deletion goblint.opam.locked
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ post-messages: [
pin-depends: [
[
"goblint-cil.2.0.9"
"git+https://github.com/goblint/cil.git#e21285af8f4408ed5354b1674dab840c43e84712"
"git+https://github.com/goblint/cil.git#abe64c5705d939b34bf08a186661fce4efcbda53"
]
[
"apron.v0.9.15"
Expand Down
2 changes: 1 addition & 1 deletion goblint.opam.template
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
pin-depends: [
[ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#e21285af8f4408ed5354b1674dab840c43e84712" ]
[ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#abe64c5705d939b34bf08a186661fce4efcbda53" ]
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
[ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
]
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/55-loop-unrolling/12-loop-no-overflows.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ Should have no overflow warning (on line 32).
Now has NULL dereference warning there still.

$ goblint --enable ana.int.interval_set 12-loop-no-overflows.c
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:32:9-32:550)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:32:346-32:384)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:34:9-34:33)
[Info][Unsound] Unknown address given as function argument (12-loop-no-overflows.c:34:9-34:33)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:20:5-20:45)
Expand Down
26 changes: 13 additions & 13 deletions tests/regression/cfg/loops.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@
│ │ │ ▼ │ │ │
│ │ │ ┌───────────────────────────────────┐ │ │ │
│ │ │ │ loops.c:13:3-15:3 │ │ │ │
│ │ │ │ (loops.c:13:7-13:26 (synthetic)) │ │ │ │
│ │ │ │ (loops.c:13:7-13:13 (synthetic)) │ │ │ │
│ │ │ │ YAML loc: loops.c:13:3-15:3 │ │ i = i + 1 │ │
│ │ │ │ server: false │ │ │ │
│ │ │ └───────────────────────────────────┘ │ │ │
Expand All @@ -50,7 +50,7 @@
│ │ │ ▼ │ │ │
│ │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ │
│ │ │ │ │ │ loops.c:13:3-15:3 (synthetic) │ │ │ │
│ │ │ │ loops.c:14:5-14:23 │ │ (loops.c:13:7-13:26 (synthetic)) │ │ │ │
│ │ │ │ loops.c:14:5-14:23 │ │ (loops.c:13:13-13:21 (synthetic)) │ │ │ │
│ │ │ │ (loops.c:14:5-14:23) │ │ [loops.c:13:3-15:3 (synthetic) │ │ │ │
│ │ │ │ YAML loc: loops.c:14:5-14:23 │ │ (unknown)] │ │ │ │
│ │ │ │ server: true │ Pos(i < 10) │ YAML loop: loops.c:13:3-15:3 │ │ │ │
Expand All @@ -61,7 +61,7 @@
│ │ │ ▼ ▼ │ │
│ │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │
│ │ │ │ loops.c:13:3-15:3 (synthetic) │ │ loops.c:18:3-20:3 │ │ │
│ │ │ │ (loops.c:13:7-13:26 (synthetic)) │ │ (loops.c:18:7-18:26 (synthetic)) │ │ │
│ │ │ │ (loops.c:13:21-13:26 (synthetic)) │ │ (loops.c:18:7-18:13 (synthetic)) │ │ │
│ │ │ │ server: false │ │ YAML loc: loops.c:18:3-20:3 │ │ │
│ │ └─ │ │ │ server: false │ │ │
│ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │
Expand All @@ -70,8 +70,8 @@
│ │ ▼ │ │
│ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │
│ │ │ │ │ loops.c:18:3-20:3 (synthetic) │ │ │
│ │ │ loops.c:18:3-20:3 (synthetic) │ │ (loops.c:18:7-18:26 (synthetic)) │ │ │
│ │ │ (loops.c:18:7-18:26 (synthetic)) │ │ [loops.c:18:3-20:3 (synthetic) │ │ │
│ │ │ loops.c:18:3-20:3 (synthetic) │ │ (loops.c:18:13-18:21 (synthetic)) │ │ │
│ │ │ (loops.c:18:21-18:26 (synthetic)) │ │ [loops.c:18:3-20:3 (synthetic) │ │ │
│ │ │ server: false │ │ (unknown)] │ │ │
│ │ │ │ Pos(i < 10) │ YAML loop: loops.c:18:3-20:3 │ i = i + 1 │ │
│ └────── │ │ ◀───────────── │ server: false │ ◀────────────────┘ │
Expand All @@ -81,7 +81,7 @@
│ ▼ │
│ ┌───────────────────────────────────┐ │
│ │ loops.c:23:3-25:3 │ │
│ │ (loops.c:23:7-23:22 (synthetic)) │ │
│ │ (loops.c:23:7-23:13 (synthetic)) │ │
│ │ YAML loc: loops.c:23:3-25:3 │ │
│ │ server: false │ │
│ └───────────────────────────────────┘ │
Expand All @@ -90,7 +90,7 @@
│ ▼ │
│ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │
│ │ │ │ loops.c:23:3-25:3 (synthetic) │ │
│ │ loops.c:24:5-24:8 │ │ (loops.c:23:7-23:22 (synthetic)) │ │
│ │ loops.c:24:5-24:8 │ │ (loops.c:23:13-23:21 (synthetic)) │ │
│ │ (loops.c:24:5-24:8) │ │ [loops.c:23:3-25:3 (synthetic) │ │
│ │ YAML loc: loops.c:24:5-24:8 │ │ (unknown)] │ │
│ │ server: true │ Pos(i < 10) │ YAML loop: loops.c:23:3-25:3 │ i = i + 1 │
Expand All @@ -110,7 +110,7 @@
▼
┌───────────────────────────────────┐ ┌───────────────────────────────────┐
│ │ │ loops.c:29:3-31:3 (synthetic) │
│ loops.c:30:5-30:23 │ │ (loops.c:29:7-29:21 (synthetic)) │
│ loops.c:30:5-30:23 │ │ (loops.c:29:8-29:16 (synthetic)) │
│ (loops.c:30:5-30:23) │ │ [loops.c:29:3-31:3 (synthetic) │
│ YAML loc: loops.c:30:5-30:23 │ │ (unknown)] │
│ server: true │ Pos(i < 10) │ YAML loop: loops.c:29:3-31:3 │ i = i + 1
Expand All @@ -121,7 +121,7 @@
▼ ▼ │
┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │
│ loops.c:29:3-31:3 (synthetic) │ │ loops.c:34:3-36:3 │ │
│ (loops.c:29:7-29:21 (synthetic)) │ │ (loops.c:34:12-34:17 (synthetic)) │ │
│ (loops.c:29:16-29:21 (synthetic)) │ │ (loops.c:34:12-34:17 (synthetic)) │ │
│ server: false │ │ YAML loc: loops.c:34:3-36:3 │ │
┌────── │ │ │ server: false │ │
│ └───────────────────────────────────┘ └───────────────────────────────────┘ │
Expand All @@ -130,7 +130,7 @@
│ ▼ │
│ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │
│ │ │ │ loops.c:34:3-36:3 (synthetic) │ │
│ │ loops.c:35:5-35:23 │ │ (loops.c:34:7-34:30 (synthetic)) │ │
│ │ loops.c:35:5-35:23 │ │ (loops.c:34:17-34:25 (synthetic)) │ │
│ │ (loops.c:35:5-35:23) │ │ [loops.c:34:3-36:3 (synthetic) │ │
│ │ YAML loc: loops.c:35:5-35:23 │ │ (unknown)] │ │
│ │ server: true │ Pos(j < 10) │ YAML loop: loops.c:34:3-36:3 │ j = j + 1 │
Expand All @@ -141,7 +141,7 @@
│ ▼ ▼ │ │
│ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │
│ │ loops.c:34:3-36:3 (synthetic) │ │ loops.c:39:3-41:3 │ │ │
│ │ (loops.c:34:12-34:17 (synthetic)) │ │ (loops.c:39:12-39:23 (synthetic)) │ │ │
│ │ (loops.c:34:25-34:30 (synthetic)) │ │ (loops.c:39:12-39:23 (synthetic)) │ │ │
│ │ server: false │ │ YAML loc: loops.c:39:3-41:3 │ │ │
│ │ │ │ server: false │ │ │
│ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │
Expand All @@ -158,7 +158,7 @@
│ │ ▼ │ │
│ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │
│ │ │ │ │ loops.c:39:3-41:3 (synthetic) │ │ │
│ │ │ loops.c:40:5-40:23 │ │ (loops.c:39:7-39:36 (synthetic)) │ │ │
│ │ │ loops.c:40:5-40:23 │ │ (loops.c:39:23-39:31 (synthetic)) │ │ │
│ │ │ (loops.c:40:5-40:23) │ │ [loops.c:39:3-41:3 (synthetic) │ │ │
│ │ │ YAML loc: loops.c:40:5-40:23 │ │ (unknown)] │ │ │
│ │ │ server: true │ Pos(i < 10) │ YAML loop: loops.c:39:3-41:3 │ i = i + 1 │ │
Expand All @@ -169,7 +169,7 @@
│ │ ▼ ▼ │ │ │
│ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ │
│ │ │ loops.c:39:3-41:3 (synthetic) │ │ loops.c:44:3-44:8 │ │ │ │
│ │ │ (loops.c:39:12-39:23 (synthetic)) │ │ (loops.c:44:3-44:8) │ │ │ │
│ │ │ (loops.c:39:31-39:36 (synthetic)) │ │ (loops.c:44:3-44:8) │ │ │ │
│ │ │ server: false │ │ YAML loc: loops.c:44:3-44:8 │ │ │ │
│ │ │ │ │ server: true │ │ │ │
│ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ │
Expand Down
Loading
Loading