Remove exp.lower-constants

goblint.opam

@@ -58,7 +58,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#19dd76823c870b621942ef980282dc1abf0d4f89" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#9b348e9024aea825b80efa3d55c65e62b8eab18e" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

goblint.opam.locked

@@ -98,7 +98,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#19dd76823c870b621942ef980282dc1abf0d4f89"
+    "git+https://github.com/goblint/cil.git#9b348e9024aea825b80efa3d55c65e62b8eab18e"
   ]
   [
     "apron.v0.9.13"

goblint.opam.template

@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#19dd76823c870b621942ef980282dc1abf0d4f89" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#9b348e9024aea825b80efa3d55c65e62b8eab18e" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

src/analyses/base.ml

@@ -686,7 +686,7 @@ struct
     in
     let r =
       (* query functions were no help ... now try with values*)
-      match (if get_bool "exp.lower-constants" then constFold true exp else exp) with
+      match constFold true exp with
       (* Integer literals *)
       (* seems like constFold already converts CChr to CInt *)
       | Const (CChr x) -> eval_rv a gs st (Const (charConstToInt x)) (* char becomes int, see Cil doc/ISO C 6.4.4.4.10 *)

src/maingoblint.ml

@@ -489,10 +489,6 @@ let main () =
 
     Sys.set_signal (Goblintutil.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *)
 
-    (* Cil.lowerConstants assumes wrap-around behavior for signed intger types, which conflicts with checking
-      for overflows, as this will replace potential overflows with constants after wrap-around *)
-    (if GobConfig.get_bool "ana.sv-comp.enabled" && Svcomp.Specification.of_option () = NoOverflow then
-      set_bool "exp.lower-constants" false);
     Cilfacade.init ();
 
     handle_extraspecials ();

src/util/cilfacade.ml

@@ -34,7 +34,7 @@ let get_stmtLoc stmt =
 
 let init () =
   initCIL ();
-  lowerConstants := GobConfig.get_bool "exp.lower-constants";
+  lowerConstants := true;
   Mergecil.ignore_merge_conflicts := true;
   (* lineDirectiveStyle := None; *)
   Rmtmps.keepUnused := true;

src/util/defaults.ml

@@ -202,7 +202,6 @@ let _ = ()
 
 (* {4 category [Experimental]} *)
 let _ = ()
-      ; reg Experimental "exp.lower-constants"   "true"  "Use Cil.lowerConstants to simplify some constant? (assumes wrap-around for signed int)"
       (* TODO: priv subobject *)
       ; reg Experimental "exp.privatization"     "'protection-read'" "Which privatization to use? none/protection-old/mutex-oplus/mutex-meet/protection/protection-read/protection-vesal/mine/mine-nothread/mine-W/mine-W-noinit/lock/write/write+lock"
       ; reg Experimental "exp.priv-prec-dump"    "''"    "File to dump privatization precision data to."

tests/regression/39-signed-overflows/05-lower-constants.c

@@ -0,0 +1,10 @@
+#include<limits.h>
+
+int main(void) {
+    int x = INT_MAX + 1;
+    assert(x == INT_MIN); //UNKNOWN!
+
+    int r = - INT_MIN;
+
+    assert(r == INT_MIN); //UNKNOWN!
+}