diff --git a/goblint.opam b/goblint.opam index a9761e2c8e..b7d956738c 100644 --- a/goblint.opam +++ b/goblint.opam @@ -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" ] ] diff --git a/goblint.opam.locked b/goblint.opam.locked index 461ed08fba..78384eb649 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -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" diff --git a/goblint.opam.template b/goblint.opam.template index 7cb4e0eb82..bbca3b4ca6 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -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" ] ] diff --git a/tests/regression/55-loop-unrolling/12-loop-no-overflows.t b/tests/regression/55-loop-unrolling/12-loop-no-overflows.t index d5d2683a09..59ceddd2f9 100644 --- a/tests/regression/55-loop-unrolling/12-loop-no-overflows.t +++ b/tests/regression/55-loop-unrolling/12-loop-no-overflows.t @@ -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) diff --git a/tests/regression/cfg/loops.t/run.t b/tests/regression/cfg/loops.t/run.t index 64a213d061..77ef26b032 100644 --- a/tests/regression/cfg/loops.t/run.t +++ b/tests/regression/cfg/loops.t/run.t @@ -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 │ │ │ │ │ │ │ └───────────────────────────────────┘ │ │ │ @@ -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 │ │ │ │ @@ -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 │ │ │ │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ @@ -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 │ ◀────────────────┘ │ @@ -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 │ │ │ └───────────────────────────────────┘ │ @@ -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 │ @@ -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 @@ -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 │ │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ @@ -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 │ @@ -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 │ │ │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ @@ -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 │ │ @@ -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 │ │ │ │ │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ │ diff --git a/tests/regression/cfg/pr-758.t/run.t b/tests/regression/cfg/pr-758.t/run.t index c2b54eb518..9dc1012233 100644 --- a/tests/regression/cfg/pr-758.t/run.t +++ b/tests/regression/cfg/pr-758.t/run.t @@ -2,89 +2,89 @@ $ graph-easy --as=boxart main.dot - ┌────────────────────────────────────────────────────────────────────────────────────────┐ - │ │ - │ ┌────────────────────────────────────┐ │ - │ │ main() │ │ - │ └────────────────────────────────────┘ │ - │ │ │ - │ │ (body) │ - │ ▼ │ - │ ┌────────────────────────────────────┐ │ - │ │ pr-758.c:5:3-5:13 │ │ - │ │ (pr-758.c:5:7-5:13 (synthetic)) │ │ - │ │ YAML loc: pr-758.c:5:3-5:13 │ │ - │ │ server: false │ │ - │ └────────────────────────────────────┘ │ - │ │ │ x = x + 1 - │ │ x = 42 │ - │ ▼ │ - │ ┌────────────────────────────────────┐ │ - │ │ pr-758.c:6:3-8:3 │ │ - │ │ (pr-758.c:6:7-6:26 (synthetic)) │ │ - │ │ YAML loc: pr-758.c:6:3-8:3 │ │ - │ │ server: false │ │ - │ └────────────────────────────────────┘ │ - │ │ │ - │ │ x = 0 │ - │ ▼ │ - ┌─────────────────────────────────┐ ┌────────────────────────────────────┐ │ - │ │ │ pr-758.c:6:3-8:3 (synthetic) │ │ - │ pr-758.c:6:3-8:3 (synthetic) │ │ (pr-758.c:6:7-6:26 (synthetic)) │ │ - │ (pr-758.c:6:7-6:26 (synthetic)) │ │ [pr-758.c:6:3-8:3 (synthetic) │ │ - │ server: false │ │ (unknown)] │ │ - │ │ Pos(x < 10) │ YAML loop: pr-758.c:6:3-8:3 │ │ - │ │ ◀───────────── │ server: false │ ◀┘ - └─────────────────────────────────┘ └────────────────────────────────────┘ - │ - │ Neg(x < 10) - ▼ - ┌────────────────────────────────────┐ - │ pr-758.c:12:3-12:12 │ - │ (pr-758.c:12:3-12:12) │ - │ YAML loc: pr-758.c:12:3-12:12 │ - │ server: true │ - └────────────────────────────────────┘ - │ - │ k = 0 - ▼ - ┌────────────────────────────────────┐ - │ pr-758.c:12:3-12:12 (synthetic) │ - │ (pr-758.c:12:3-12:12 (synthetic)) │ - │ server: false │ - └────────────────────────────────────┘ - │ - │ i = k - ▼ - ┌────────────────────────────────────┐ - │ pr-758.c:20:3-20:25 │ - │ (pr-758.c:20:15-20:24 (synthetic)) │ - │ YAML loc: pr-758.c:20:3-20:25 │ - │ server: false │ - └────────────────────────────────────┘ - │ - │ a.kaal = 2 - ▼ - ┌────────────────────────────────────┐ - │ pr-758.c:20:3-20:25 (synthetic) │ - │ (pr-758.c:20:15-20:24 (synthetic)) │ - │ server: false │ - └────────────────────────────────────┘ - │ - │ a.hind = 3 - ▼ - ┌────────────────────────────────────┐ - │ pr-758.c:21:3-21:11 │ - │ (pr-758.c:21:10-21:11) │ - │ YAML loc: pr-758.c:21:3-21:11 │ - │ server: true │ - └────────────────────────────────────┘ - │ - │ return 0 - ▼ - ┌────────────────────────────────────┐ - │ return of main() │ - └────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────────────────────────────────────┐ + │ │ + │ ┌────────────────────────────────────┐ │ + │ │ main() │ │ + │ └────────────────────────────────────┘ │ + │ │ │ + │ │ (body) │ + │ ▼ │ + │ ┌────────────────────────────────────┐ │ + │ │ pr-758.c:5:3-5:13 │ │ + │ │ (pr-758.c:5:7-5:13 (synthetic)) │ │ + │ │ YAML loc: pr-758.c:5:3-5:13 │ │ + │ │ server: false │ │ + │ └────────────────────────────────────┘ │ + │ │ │ x = x + 1 + │ │ x = 42 │ + │ ▼ │ + │ ┌────────────────────────────────────┐ │ + │ │ pr-758.c:6:3-8:3 │ │ + │ │ (pr-758.c:6:7-6:13 (synthetic)) │ │ + │ │ YAML loc: pr-758.c:6:3-8:3 │ │ + │ │ server: false │ │ + │ └────────────────────────────────────┘ │ + │ │ │ + │ │ x = 0 │ + │ ▼ │ + ┌──────────────────────────────────┐ ┌────────────────────────────────────┐ │ + │ │ │ pr-758.c:6:3-8:3 (synthetic) │ │ + │ pr-758.c:6:3-8:3 (synthetic) │ │ (pr-758.c:6:13-6:21 (synthetic)) │ │ + │ (pr-758.c:6:21-6:26 (synthetic)) │ │ [pr-758.c:6:3-8:3 (synthetic) │ │ + │ server: false │ │ (unknown)] │ │ + │ │ Pos(x < 10) │ YAML loop: pr-758.c:6:3-8:3 │ │ + │ │ ◀───────────── │ server: false │ ◀┘ + └──────────────────────────────────┘ └────────────────────────────────────┘ + │ + │ Neg(x < 10) + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:12:3-12:12 │ + │ (pr-758.c:12:3-12:12) │ + │ YAML loc: pr-758.c:12:3-12:12 │ + │ server: true │ + └────────────────────────────────────┘ + │ + │ k = 0 + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:12:3-12:12 (synthetic) │ + │ (pr-758.c:12:3-12:12 (synthetic)) │ + │ server: false │ + └────────────────────────────────────┘ + │ + │ i = k + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:20:3-20:25 │ + │ (pr-758.c:20:15-20:24 (synthetic)) │ + │ YAML loc: pr-758.c:20:3-20:25 │ + │ server: false │ + └────────────────────────────────────┘ + │ + │ a.kaal = 2 + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:20:3-20:25 (synthetic) │ + │ (pr-758.c:20:15-20:24 (synthetic)) │ + │ server: false │ + └────────────────────────────────────┘ + │ + │ a.hind = 3 + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:21:3-21:11 │ + │ (pr-758.c:21:10-21:11) │ + │ YAML loc: pr-758.c:21:3-21:11 │ + │ server: true │ + └────────────────────────────────────┘ + │ + │ return 0 + ▼ + ┌────────────────────────────────────┐ + │ return of main() │ + └────────────────────────────────────┘