Fix undefined modulo operation constFold in CIL

Author: sim642

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#d4ff56f4994f8acbe1544f15a103748942645961" ]
   # 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" ]
 ]

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#d4ff56f4994f8acbe1544f15a103748942645961"
   ]
   [
     "apron.v0.9.15"

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#d4ff56f4994f8acbe1544f15a103748942645961" ]
   # 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" ]
 ]

tests/regression/39-signed-overflows/17-mod-minus-1.c

@@ -2,7 +2,7 @@
 #include <limits.h>
 
 int main() {
-    int bad = INT_MIN % -1; // TODO WARN (overflow)
+    int bad = INT_MIN % -1; // WARN (overflow)
     int x, y;
     bad = x % y; // WARN (div by zero and overflow, distinguished in cram test)
     if (y != 0) {

tests/regression/39-signed-overflows/17-mod-minus-1.t

@@ -1,5 +1,6 @@
 TODO: should warn about overflow in all three %-s
   $ goblint --enable warn.deterministic --enable ana.int.interval 17-mod-minus-1.c
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in % (17-mod-minus-1.c:5:9-5:26)
   [Warning][Integer > Overflow][CWE-190] Signed integer overflow in % (17-mod-minus-1.c:7:5-7:16)
   [Warning][Integer > Overflow][CWE-190] Signed integer overflow in % (17-mod-minus-1.c:9:9-9:20)
   [Warning][Integer > DivByZero][CWE-369] Second argument of modulo might be zero (17-mod-minus-1.c:7:5-7:16)
@@ -10,6 +11,7 @@ TODO: should warn about overflow in all three %-s
 
 TODO: should warn about overflow in all three %-s
   $ goblint --enable warn.deterministic --enable ana.int.interval_set 17-mod-minus-1.c
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in % (17-mod-minus-1.c:5:9-5:26)
   [Warning][Integer > Overflow][CWE-190] Signed integer overflow in % (17-mod-minus-1.c:7:5-7:16)
   [Warning][Integer > Overflow][CWE-190] Signed integer overflow in % (17-mod-minus-1.c:9:9-9:20)
   [Warning][Integer > DivByZero][CWE-369] Second argument of modulo might be zero (17-mod-minus-1.c:7:5-7:16)