From 9420a089fcc1134f289d61f5eb8e45571ca47d23 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Thu, 16 Nov 2023 16:13:29 +0100
Subject: [PATCH 01/28] add sqrt handling in float domain

---
 src/analyses/base.ml               |  1 +
 src/analyses/libraryDesc.ml        |  4 +++-
 src/analyses/libraryFunctions.ml   |  6 +++---
 src/cdomains/floatDomain.ml        | 14 ++++++++++++++
 src/cdomains/floatDomain.mli       |  3 +++
 src/cdomains/floatOps/floatOps.ml  |  3 +++
 src/cdomains/floatOps/floatOps.mli |  1 +
 src/cdomains/floatOps/stubs.c      | 14 ++++++++++++++
 8 files changed, 42 insertions(+), 4 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index a8ad9af95b..86951ab4a5 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2356,6 +2356,7 @@ struct
           | Isunordered (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.unordered x y))
           | Fmax (fd, x ,y) -> Float (apply_binary fd FD.fmax x y)
           | Fmin (fd, x ,y) -> Float (apply_binary fd FD.fmin x y)
+          | Sqrt (fk, x) -> Float (apply_unary fk FD.sqrt x)
         end
       in
       begin match lv with
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
index 72a4261cb5..5403612fae 100644
--- a/src/analyses/libraryDesc.ml
+++ b/src/analyses/libraryDesc.ml
@@ -38,7 +38,8 @@ type math =
   | Atan2 of (CilType.Fkind.t * Basetype.CilExp.t * Basetype.CilExp.t)
   | Cos of (CilType.Fkind.t * Basetype.CilExp.t)
   | Sin of (CilType.Fkind.t * Basetype.CilExp.t)
-  | Tan of (CilType.Fkind.t * Basetype.CilExp.t) [@@deriving eq, ord, hash]
+  | Tan of (CilType.Fkind.t * Basetype.CilExp.t)
+  | Sqrt of (CilType.Fkind.t * Basetype.CilExp.t) [@@deriving eq, ord, hash]
 
 (** Type of special function, or {!Unknown}. *)
 (* Use inline record if not single {!Cil.exp} argument. *)
@@ -170,6 +171,7 @@ module MathPrintable = struct
     | Cos (fk, exp) -> Pretty.dprintf "(%a )cos(%a)" d_fkind fk d_exp exp
     | Sin (fk, exp) -> Pretty.dprintf "(%a )sin(%a)" d_fkind fk d_exp exp
     | Tan (fk, exp) -> Pretty.dprintf "(%a )tan(%a)" d_fkind fk d_exp exp
+    | Sqrt (fk, exp) -> Pretty.dprintf "(%a )sqrt(%a)" d_fkind fk d_exp exp
 
   include Printable.SimplePretty (
     struct
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 117dcbd236..8f8a43cb29 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -944,9 +944,9 @@ let math_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("scalbln", unknown [drop "arg" []; drop "exp" []]);
     ("scalblnf", unknown [drop "arg" []; drop "exp" []]);
     ("scalblnl", unknown [drop "arg" []; drop "exp" []]);
-    ("sqrt", unknown [drop "x" []]);
-    ("sqrtf", unknown [drop "x" []]);
-    ("sqrtl", unknown [drop "x" []]);
+    ("sqrt", special [__ "x" []] @@ fun x -> Math { fun_args = (Sqrt (FDouble, x)) });
+    ("sqrtf", special [__ "x" []] @@ fun x -> Math { fun_args = (Sqrt (FFloat, x)) });
+    ("sqrtl", special [__ "x" []] @@ fun x -> Math { fun_args = (Sqrt (FLongDouble, x)) });
     ("tgamma", unknown [drop "x" []]);
     ("tgammaf", unknown [drop "x" []]);
     ("tgammal", unknown [drop "x" []]);
diff --git a/src/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml
index f52c849111..39d3744401 100644
--- a/src/cdomains/floatDomain.ml
+++ b/src/cdomains/floatDomain.ml
@@ -40,6 +40,8 @@ module type FloatArith = sig
   (** sin(x) *)
   val tan : t -> t
   (** tan(x) *)
+  val sqrt : t -> t
+  (** sqrt(x) *)
 
   (** {inversions of unary functions}*)
   val inv_ceil : ?asPreciseAsConcrete:bool -> t -> t
@@ -670,6 +672,14 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
     | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*tan(0) = 0*)
     | _ -> top () (**could be exact for intervals where l=h, or even for some intervals *)
 
+  let eval_sqrt = function
+    | (l, h) when l = Float_t.zero && h = Float_t.zero -> of_const 0.
+    | (l, h) when l >= Float_t.zero ->
+      let low = Float_t.sqrt Down l in
+      let high = Float_t.sqrt Up h in
+      Interval (low, high)
+    | _ -> top ()
+
   let eval_inv_ceil ?(asPreciseAsConcrete=false) = function
     | (l, h) ->
       if (Float_t.sub Up (Float_t.ceil l) (Float_t.sub Down (Float_t.ceil l) (Float_t.of_float Nearest 1.0)) = (Float_t.of_float Nearest 1.0)) then (
@@ -784,6 +794,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
   let cos = eval_unop eval_cos
   let sin = eval_unop eval_sin
   let tan = eval_unop eval_tan
+  let sqrt = eval_unop eval_sqrt
 
   let inv_ceil ?(asPreciseAsConcrete=false) = eval_unop ~warn:false (eval_inv_ceil ~asPreciseAsConcrete:asPreciseAsConcrete)
   let inv_floor ?(asPreciseAsConcrete=false) = eval_unop ~warn:false (eval_inv_floor ~asPreciseAsConcrete:asPreciseAsConcrete)
@@ -899,6 +910,7 @@ module FloatIntervalImplLifted = struct
   let cos = lift (F1.cos, F2.cos)
   let sin = lift (F1.sin, F2.sin)
   let tan = lift (F1.tan, F2.tan)
+  let sqrt = lift (F1.sqrt, F2.sqrt)
 
   let inv_ceil ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) = function
     | F32 a -> F32 (F1.inv_ceil ~asPreciseAsConcrete:true a)
@@ -1159,6 +1171,8 @@ module FloatDomTupleImpl = struct
     map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.sin); }
   let tan =
     map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.tan); }
+  let sqrt =
+    map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.sqrt); }
 
   (*"asPreciseAsConcrete" has no meaning here*)
   let inv_ceil ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) =
diff --git a/src/cdomains/floatDomain.mli b/src/cdomains/floatDomain.mli
index 06bca69aca..d958e1ee81 100644
--- a/src/cdomains/floatDomain.mli
+++ b/src/cdomains/floatDomain.mli
@@ -57,6 +57,9 @@ module type FloatArith = sig
   val tan : t -> t
   (** tan(x) *)
 
+  val sqrt : t -> t
+  (** sqrt(x) *)
+
   (** {inversions of unary functions}*)
   val inv_ceil : ?asPreciseAsConcrete:bool -> t -> t
   (** (inv_ceil z -> x) if (z = ceil(x)) *)
diff --git a/src/cdomains/floatOps/floatOps.ml b/src/cdomains/floatOps/floatOps.ml
index a951ec08fe..a4e39d930e 100644
--- a/src/cdomains/floatOps/floatOps.ml
+++ b/src/cdomains/floatOps/floatOps.ml
@@ -35,6 +35,7 @@ module type CFloatType = sig
   val sub: round_mode -> t -> t -> t
   val mul: round_mode -> t -> t -> t
   val div: round_mode -> t -> t -> t
+  val sqrt: round_mode -> t -> t
   val atof: round_mode -> string -> t
 end
 
@@ -74,6 +75,7 @@ module CDouble = struct
   external sub: round_mode -> t -> t -> t = "sub_double"
   external mul: round_mode -> t -> t -> t = "mul_double"
   external div: round_mode -> t -> t -> t = "div_double"
+  external sqrt: round_mode -> t -> t = "sqrt_double"
 
   external atof: round_mode -> string -> t = "atof_double"
 end
@@ -107,6 +109,7 @@ module CFloat = struct
   external sub: round_mode -> t -> t -> t = "sub_float"
   external mul: round_mode -> t -> t -> t = "mul_float"
   external div: round_mode -> t -> t -> t = "div_float"
+  external sqrt: round_mode -> t -> t = "sqrt_float"
 
   external atof: round_mode -> string -> t = "atof_float"
 
diff --git a/src/cdomains/floatOps/floatOps.mli b/src/cdomains/floatOps/floatOps.mli
index 05bf363872..cf24f75ed5 100644
--- a/src/cdomains/floatOps/floatOps.mli
+++ b/src/cdomains/floatOps/floatOps.mli
@@ -38,6 +38,7 @@ module type CFloatType = sig
   val sub: round_mode -> t -> t -> t
   val mul: round_mode -> t -> t -> t
   val div: round_mode -> t -> t -> t
+  val sqrt: round_mode -> t -> t
   val atof: round_mode -> string -> t
 end
 
diff --git a/src/cdomains/floatOps/stubs.c b/src/cdomains/floatOps/stubs.c
index e0485883dd..50e4a2fb31 100644
--- a/src/cdomains/floatOps/stubs.c
+++ b/src/cdomains/floatOps/stubs.c
@@ -36,6 +36,20 @@ static void change_round_mode(int mode)
     }
 }
 
+#define UNARY_OP(name, type, op)                                 \
+    CAMLprim value name##_##type(value mode, value x)            \
+    {                                                            \
+        int old_roundingmode = fegetround();                     \
+        change_round_mode(Int_val(mode));                        \
+        volatile type r, x1 = Double_val(x);                     \
+        r = op(x1);                                              \
+        fesetround(old_roundingmode);                            \
+        return caml_copy_double(r);                              \
+    }
+
+UNARY_OP(sqrt, double, sqrt);
+UNARY_OP(sqrt, float, sqrtf);
+
 #define BINARY_OP(name, type, op)                                \
     CAMLprim value name##_##type(value mode, value x, value y)   \
     {                                                            \

From 0740491dcc290a8e41e693f0b8534af9540ebb37 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Thu, 16 Nov 2023 20:09:24 +0100
Subject: [PATCH 02/28] implement abs function for integers

---
 src/analyses/base.ml             | 18 ++++++++++++++++++
 src/analyses/libraryDesc.ml      |  2 ++
 src/analyses/libraryFunctions.ml |  2 +-
 3 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 86951ab4a5..bca3cb6588 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2328,6 +2328,23 @@ struct
           | _ -> failwith ("non-floating-point argument in call to function "^f.vname)
         end
       in
+      let apply_abs ik x =
+        let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in
+        begin match eval_x with
+          | Int int_x ->
+            let xcast = ID.cast_to ik int_x in
+            (* TODO cover case where x is the MIN value -> undefined *)
+            (match ID.le xcast (ID.of_int ik Z.zero) with
+             | d when d = ID.of_int ik Z.zero -> xcast (* x positive *)
+             | d when d = ID.of_int ik Z.one -> ID.neg xcast (* x negative *)
+             | _ -> (* both possible *)
+               let x1 = ID.neg (ID.meet (ID.ending ik Z.zero) xcast) in
+               let x2 = ID.meet (ID.starting ik Z.zero) xcast in
+               ID.join x1 x2
+            )
+          | _ -> failwith ("non-integer argument in call to function "^f.vname)
+        end
+      in
       let result:value =
         begin match fun_args with
           | Nan (fk, str) when Cil.isPointerType (Cilfacade.typeOf str) -> Float (FD.nan_of fk)
@@ -2357,6 +2374,7 @@ struct
           | Fmax (fd, x ,y) -> Float (apply_binary fd FD.fmax x y)
           | Fmin (fd, x ,y) -> Float (apply_binary fd FD.fmin x y)
           | Sqrt (fk, x) -> Float (apply_unary fk FD.sqrt x)
+          | Abs x -> Int (ID.cast_to IInt (apply_abs IInt x))
         end
       in
       begin match lv with
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
index 5403612fae..8cd3dfa1ba 100644
--- a/src/analyses/libraryDesc.ml
+++ b/src/analyses/libraryDesc.ml
@@ -27,6 +27,7 @@ type math =
   | Islessequal of (Basetype.CilExp.t * Basetype.CilExp.t)
   | Islessgreater of (Basetype.CilExp.t * Basetype.CilExp.t)
   | Isunordered of (Basetype.CilExp.t * Basetype.CilExp.t)
+  | Abs of Basetype.CilExp.t
   | Ceil of (CilType.Fkind.t * Basetype.CilExp.t)
   | Floor of (CilType.Fkind.t * Basetype.CilExp.t)
   | Fabs of (CilType.Fkind.t * Basetype.CilExp.t)
@@ -159,6 +160,7 @@ module MathPrintable = struct
     | Islessequal (exp1, exp2) -> Pretty.dprintf "isLessEqual(%a, %a)" d_exp exp1 d_exp exp2
     | Islessgreater (exp1, exp2) -> Pretty.dprintf "isLessGreater(%a, %a)" d_exp exp1 d_exp exp2
     | Isunordered (exp1, exp2) -> Pretty.dprintf "isUnordered(%a, %a)" d_exp exp1 d_exp exp2
+    | Abs exp -> Pretty.dprintf "abs(%a)" d_exp exp
     | Ceil (fk, exp) -> Pretty.dprintf "(%a )ceil(%a)" d_fkind fk d_exp exp
     | Floor (fk, exp) -> Pretty.dprintf "(%a )floor(%a)" d_fkind fk d_exp exp
     | Fabs (fk, exp) -> Pretty.dprintf "(%a )fabs(%a)" d_fkind fk d_exp exp
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 8f8a43cb29..ae33f57f70 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -130,7 +130,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("wcstombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r]; drop "size" []]);
     ("wcsrtombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r_deep; w]; drop "size" []; drop "ps" [r_deep; w_deep]]);
     ("mbstowcs", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []]);
-    ("abs", unknown [drop "j" []]);
+    ("abs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs j) });
     ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
     ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)

From b9ede51e83b64db87b6a2e0322d3c348c114c07c Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Fri, 17 Nov 2023 11:11:14 +0100
Subject: [PATCH 03/28] implement special case for most-negative value

---
 src/analyses/base.ml | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index bca3cb6588..f25f0a9693 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2333,14 +2333,19 @@ struct
         begin match eval_x with
           | Int int_x ->
             let xcast = ID.cast_to ik int_x in
-            (* TODO cover case where x is the MIN value -> undefined *)
-            (match ID.le xcast (ID.of_int ik Z.zero) with
-             | d when d = ID.of_int ik Z.zero -> xcast (* x positive *)
-             | d when d = ID.of_int ik Z.one -> ID.neg xcast (* x negative *)
-             | _ -> (* both possible *)
-               let x1 = ID.neg (ID.meet (ID.ending ik Z.zero) xcast) in
-               let x2 = ID.meet (ID.starting ik Z.zero) xcast in
-               ID.join x1 x2
+            (* the absolute value of the most-negative value is out of range for 2'complement types *)
+            (match (ID.minimal xcast), (ID.minimal (ID.top_of ik)) with
+             | _, None
+             | None, _ -> ID.top_of ik
+             | Some mx, Some mm when Z.equal mx mm -> ID.top_of ik
+             | _, _ ->
+               match ID.le xcast (ID.of_int ik Z.zero) with
+               | d when d = ID.of_int ik Z.zero -> xcast (* x positive *)
+               | d when d = ID.of_int ik Z.one -> ID.neg xcast (* x negative *)
+               | _ -> (* both possible *)
+                 let x1 = ID.neg (ID.meet (ID.ending ik Z.zero) xcast) in
+                 let x2 = ID.meet (ID.starting ik Z.zero) xcast in
+                 ID.join x1 x2
             )
           | _ -> failwith ("non-integer argument in call to function "^f.vname)
         end

From 9966b873a5d07f5a2c094245312a914ba2130c9d Mon Sep 17 00:00:00 2001
From: oliver <ge96xey@mytum.de>
Date: Fri, 17 Nov 2023 14:49:33 +0100
Subject: [PATCH 04/28] update dune-project and documentation

---
 docs/developer-guide/debugging.md |  5 +++--
 dune-project                      |  4 +++-
 goblint.opam.locked               | 12 ++++++------
 3 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/docs/developer-guide/debugging.md b/docs/developer-guide/debugging.md
index 7875a9b01e..5c1db12227 100644
--- a/docs/developer-guide/debugging.md
+++ b/docs/developer-guide/debugging.md
@@ -85,7 +85,7 @@ The configuration file has to be named `launch.json` and must reside in the `./.
     "configurations": [
       {
         "name": "Goblint",
-        "type": "ocamlearlybird",
+        "type": "ocaml.earlybird",
         "request": "launch",
         "program": "${workspaceFolder}/goblint.byte",
         "arguments": [
@@ -97,7 +97,8 @@ The configuration file has to be named `launch.json` and must reside in the `./.
     ]
 }
 ```
-Note that the individual arguments to Goblint should be passed here as separate strings that do not contain spaces.
+Note that the individual arguments to Goblint should be passed here as separate strings that do not contain spaces. Finally, to enable breakpoints uncomment `(map_workspace_root false)` in the dune-project file.
+
 
 ### Running Goblint in the VS Code Debugger
 
diff --git a/dune-project b/dune-project
index 4a9cd8e3c1..05c7d9418c 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.6)
+(lang dune 3.7)
 (using dune_site 0.1)
 (cram enable)
 (name goblint)
@@ -64,3 +64,5 @@
     (share lib)
     (share conf))
 )
+
+; (map_workspace_root false) ;uncomment to enable breakpoints
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 2744d2fe92..0abe989955 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -50,12 +50,12 @@ depends: [
   "cpu" {= "2.0.0"}
   "csexp" {= "1.5.1"}
   "ctypes" {= "0.20.1"}
-  "dune" {= "3.6.1"}
-  "dune-build-info" {= "3.6.1"}
-  "dune-configurator" {= "3.6.1"}
-  "dune-private-libs" {= "3.6.1"}
-  "dune-site" {= "3.6.1"}
-  "dyn" {= "3.6.1"}
+  "dune" {= "3.7.1"}
+  "dune-build-info" {= "3.7.1"}
+  "dune-configurator" {= "3.7.1"}
+  "dune-private-libs" {= "3.7.1"}
+  "dune-site" {= "3.7.1"}
+  "dyn" {= "3.7.1"}
   "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}

From c8c49a56b60cc90de5f3a0fbed97ed2de8832db1 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 17 Nov 2023 15:35:41 +0100
Subject: [PATCH 05/28] Be more precise for `<<` of Intervals

---
 src/cdomains/intDomain.ml                     | 20 +++++++++++++++-
 .../39-signed-overflows/06-shiftleft.c        | 23 +++++++++++++++++++
 2 files changed, 42 insertions(+), 1 deletion(-)
 create mode 100644 tests/regression/39-signed-overflows/06-shiftleft.c

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index 3bc84ae676..49065b9cc5 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -610,6 +610,11 @@ module IntervalArith(Ints_t : IntOps.IntOps) = struct
     let x2y2 = (Ints_t.mul x2 y2) in
     (min4 x1y1 x1y2 x2y1 x2y2, max4 x1y1 x1y2 x2y1 x2y2)
 
+  let shiftleft (x1,x2) (y1,y2) =
+    let y1p = Ints_t.shift_left Ints_t.one y1 in
+    let y2p = Ints_t.shift_left Ints_t.one y2 in
+    mul (x1, x2) (y1p, y2p)
+
   let div (x1, x2) (y1, y2) =
     let x1y1n = (Ints_t.div x1 y1) in
     let x1y2n = (Ints_t.div x1 y2) in
@@ -851,7 +856,6 @@ struct
 
   let bitnot = bit1 (fun _ik -> Ints_t.bitnot)
   let shift_right = bitcomp (fun _ik x y -> Ints_t.shift_right x (Ints_t.to_int y))
-  let shift_left  = bitcomp (fun _ik x y -> Ints_t.shift_left  x (Ints_t.to_int y))
 
   let neg ?no_ov ik = function None -> (None,{underflow=false; overflow=false}) | Some x -> norm ik @@ Some (IArith.neg x)
 
@@ -864,6 +868,20 @@ struct
   let mul ?no_ov = binary_op_with_norm IArith.mul
   let sub ?no_ov = binary_op_with_norm IArith.sub
 
+  let shift_left ik a b =
+    match is_bot a, is_bot b with
+    | true, true -> (bot_of ik,{underflow=false; overflow=false})
+    | true, _
+    | _   , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show a) (show b)))
+    | _ ->
+      match a, maximal b, minimal b with
+      | Some a, Some bl, Some bu when (Ints_t.compare bl Ints_t.zero >= 0) ->
+        (try
+           let r = IArith.shiftleft a (Ints_t.to_int bl, Ints_t.to_int bu) in
+           norm ik @@ Some r
+         with Z.Overflow -> (top_of ik,{underflow=false; overflow=true}))
+      | _              -> (top_of ik,{underflow=true; overflow=true})
+
   let rem ik x y = match x, y with
     | None, None -> None
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
diff --git a/tests/regression/39-signed-overflows/06-shiftleft.c b/tests/regression/39-signed-overflows/06-shiftleft.c
new file mode 100644
index 0000000000..987775c6f7
--- /dev/null
+++ b/tests/regression/39-signed-overflows/06-shiftleft.c
@@ -0,0 +1,23 @@
+// PARAM: --enable ana.int.interval
+#include <goblint.h>
+int main()
+{
+    int r;
+    int zero_or_one = 0;
+    int top;
+    char c;
+    r = c << 1U; //NOWARN
+
+    r = c << 128U; //WARN
+    r = r << 1U; //WARN
+    r = 8 << -2; //WARN
+
+    if(top) { zero_or_one = 1; }
+
+    r = 8 << zero_or_one;
+
+    __goblint_check(r >= 8);
+    __goblint_check(r <= 16);
+
+    return 0;
+}

From 566348216fff4b119559d907df9b8e2e005fa023 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Fri, 17 Nov 2023 16:14:36 +0100
Subject: [PATCH 06/28] improve values of parameters in abs call

---
 src/analyses/baseInvariant.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 72e00efbb1..73a41bcea1 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -726,6 +726,8 @@ struct
                             | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
                             | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
                             | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
+                            | `Lifted (Abs xInt) ->
+                              inv_exp (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st
                             | _ -> update_lval c x c' ID.pretty
                           end
                         | None -> update_lval c x c' ID.pretty

From 688cff1c28936295f3c084dd5d60f36e70dbd5a1 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Sat, 18 Nov 2023 11:26:38 +0100
Subject: [PATCH 07/28] trying to fix that value is not improved for parameter
 of abs call

---
 src/analyses/baseInvariant.ml | 71 +++++++++++++++++++++--------------
 1 file changed, 42 insertions(+), 29 deletions(-)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 73a41bcea1..b82ab88806 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -562,7 +562,7 @@ struct
       | TFloat (fk, _) -> fk
       | _ -> failwith "value which was expected to be a float is of different type?!"
     in
-    let rec inv_exp c_typed exp (st:D.t): D.t =
+    let rec inv_exp ?(query_special=true) c_typed exp (st:D.t) : D.t =
       (* trying to improve variables in an expression so it is bottom means dead code *)
       if VD.is_bot_value c_typed then contra st
       else
@@ -578,12 +578,12 @@ struct
             | Some false -> ID.of_bool ikind false
             | _ -> ID.top_of ikind
           in
-          inv_exp (Int c') e st
-        | UnOp (Neg, e, _), Float c -> inv_exp (Float (unop_FD Neg c)) e st
-        | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st
+          inv_exp ~query_special (Int c') e st
+        | UnOp (Neg, e, _), Float c -> inv_exp ~query_special (Float (unop_FD Neg c)) e st
+        | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp ~query_special (Int (unop_ID op c)) e st
         (* no equivalent for Float, as VD.is_safe_cast fails for all float types anyways *)
         | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_safe_cast t2 (Cilfacade.typeOf e2) ->
-          inv_exp (Int c) (BinOp (op, e1, e2, t)) st
+          inv_exp ~query_special (Int c) (BinOp (op, e1, e2, t)) st
         | BinOp (LOr, arg1, arg2, typ) as exp, Int c ->
           (* copied & modified from eval_rv_base... *)
           let (let*) = Option.bind in
@@ -631,7 +631,7 @@ struct
               in
               let definite_ad = to_definite_ad vs in
               let c' = VD.Address definite_ad in
-              Some (inv_exp c' e st)
+              Some (inv_exp ~query_special c' e st)
             | Int i ->
               let ik = ID.ikind i in
               let module BISet = IntDomain.BISet in
@@ -648,20 +648,20 @@ struct
               in
               let int_id = to_int_id vs in
               let c' = VD.Int int_id in
-              Some (inv_exp c' e st)
+              Some (inv_exp ~query_special c' e st)
             | _ ->
               None
           in
           begin match eqs_st with
             | Some st -> st
             | None when ID.to_bool c = Some true ->
-              begin match inv_exp (Int c) arg1 st with
+              begin match inv_exp ~query_special (Int c) arg1 st with
                 | st1 ->
-                  begin match inv_exp (Int c) arg2 st with
+                  begin match inv_exp ~query_special (Int c) arg2 st with
                     | st2 -> D.join st1 st2
                     | exception Analyses.Deadcode -> st1
                   end
-                | exception Analyses.Deadcode -> inv_exp (Int c) arg2 st (* Deadcode falls through *)
+                | exception Analyses.Deadcode -> inv_exp ~query_special (Int c) arg2 st (* Deadcode falls through *)
               end
             | None ->
               st (* TODO: not bothering to fall back, no other case can refine LOr anyway *)
@@ -676,15 +676,15 @@ struct
                let ikres = Cilfacade.get_ikind_exp e in (* might be different from argument types, e.g. for LT, GT, EQ, ... *)
                let a', b' = inv_bin_int (a, b) ikind (c_int ikres) op in
                if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a\n" d_exp e ID.pretty (c_int ikind) ID.pretty a' ID.pretty b';
-               let st' = inv_exp (Int a') e1 st in
-               let st'' = inv_exp (Int b') e2 st' in
+               let st' = inv_exp ~query_special (Int a') e1 st in
+               let st'' = inv_exp ~query_special (Int b') e2 st' in
                st''
              | Float a, Float b ->
                let fkind = Cilfacade.get_fkind_exp e1 in (* both operands have the same type *)
                let a', b' = inv_bin_float (a, b) (c_float fkind) op in
                if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a\n" d_exp e FD.pretty (c_float fkind) FD.pretty a' FD.pretty b';
-               let st' = inv_exp (Float a') e1 st in
-               let st'' = inv_exp (Float b') e2 st' in
+               let st' = inv_exp ~query_special (Float a') e1 st in
+               let st'' = inv_exp ~query_special (Float b') e2 st' in
                st''
              (* Mixed Float and Int cases should never happen, as there are no binary operators with one float and one int parameter ?!*)
              | Int _, Float _ | Float _, Int _ -> failwith "ill-typed program";
@@ -712,22 +712,22 @@ struct
               begin match t with
                 | TInt (ik, _) ->
                   begin match x with
-                    | ((Var v), offs) ->
+                    | ((Var v), offs) when query_special ->
                       if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
                       let tv_opt = ID.to_bool c in
                       begin match tv_opt with
                         | Some tv ->
                           begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with
-                            | `Lifted (Isfinite xFloat) when tv -> inv_exp (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st
-                            | `Lifted (Isnan xFloat) when tv -> inv_exp (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st
+                            | `Lifted (Isfinite xFloat) when tv -> inv_exp ~query_special:false (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st
+                            | `Lifted (Isnan xFloat) when tv -> inv_exp ~query_special:false (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st
                             (* should be correct according to C99 standard*)
-                            | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
+                            | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st
+                            | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st
+                            | `Lifted (Isless (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
+                            | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
+                            | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
                             | `Lifted (Abs xInt) ->
-                              inv_exp (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st
+                              inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st
                             | _ -> update_lval c x c' ID.pretty
                           end
                         | None -> update_lval c x c' ID.pretty
@@ -749,17 +749,17 @@ struct
               begin match t with
                 | TFloat (fk, _) ->
                   begin match x with
-                    | ((Var v), offs) ->
+                    | ((Var v), offs) when query_special ->
                       if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
                       begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with
-                        | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st
-                        | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st
+                        | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp ~query_special:false (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st
+                        | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp ~query_special:false (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st
                         | `Lifted (Fabs (ret_fk, xFloat)) ->
                           let inv = FD.inv_fabs (FD.cast_to ret_fk c) in
                           if FD.is_bot inv then
                             raise Analyses.Deadcode
                           else
-                            inv_exp (Float inv) xFloat st
+                            inv_exp ~query_special:false (Float inv) xFloat st
                         | _ -> update_lval c x c' FD.pretty
                       end
                     | _ -> update_lval c x c' FD.pretty
@@ -779,7 +779,7 @@ struct
            | TFloat (FLongDouble as fk, _), FDouble
            | TFloat (fk, _), FLongDouble
            | TFloat (FDouble as fk, _), FDouble
-           | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
+           | TFloat (FFloat as fk, _), FFloat -> inv_exp ~query_special (Float (FD.cast_to fk c)) e st
            | _ -> fallback ("CastE: incompatible types") st)
         | CastE ((TInt (ik, _)) as t, e), Int c
         | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
@@ -792,7 +792,20 @@ struct
                  (* let c' = ID.cast_to ik_e c in *)
                  let c' = ID.cast_to ik_e (ID.meet c (ID.cast_to ik (ID.top_of ik_e))) in (* TODO: cast without overflow, is this right for normal invariant? *)
                  if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a\n" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
-                 inv_exp (Int c') e st
+                 inv_exp ~query_special (Int c') e st
+               | x -> fallback (GobPretty.sprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st
+             else
+               fallback (GobPretty.sprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
+           | Float i ->
+             let i = FD.to_int ik i in
+             if ID.leq i (ID.cast_to ik i) then
+               match unrollType (Cilfacade.typeOf e) with
+               | TInt(ik_e, _)
+               | TEnum ({ekind = ik_e; _ }, _) ->
+                 (* let c' = ID.cast_to ik_e c in *)
+                 let c' = ID.cast_to ik_e (ID.meet c (ID.cast_to ik (ID.top_of ik_e))) in (* TODO: cast without overflow, is this right for normal invariant? *)
+                 if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a\n" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
+                 inv_exp ~query_special (Int c') e st
                | x -> fallback (GobPretty.sprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st
              else
                fallback (GobPretty.sprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st

From 88957a8005c2eff0d51c8bd1402c9d91e2e2a84e Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sat, 18 Nov 2023 11:32:52 +0100
Subject: [PATCH 08/28] Add test which can be run in isolation

---
 tests/regression/39-signed-overflows/06-abs.c | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 tests/regression/39-signed-overflows/06-abs.c

diff --git a/tests/regression/39-signed-overflows/06-abs.c b/tests/regression/39-signed-overflows/06-abs.c
new file mode 100644
index 0000000000..b08a0f2209
--- /dev/null
+++ b/tests/regression/39-signed-overflows/06-abs.c
@@ -0,0 +1,15 @@
+//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial
+#include<math.h>
+int main() {
+    int data;
+    if (data > (-0x7fffffff - 1))
+    {
+        if (abs(data) < 100)
+        {
+            int result = data * data;
+        }
+        
+        int result = data * data;
+    }
+    return 8;
+}
\ No newline at end of file

From 2ea8db4b64f1a55e25b2ae226d5d82815766a80c Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sat, 18 Nov 2023 12:21:30 +0100
Subject: [PATCH 09/28] Wir sind alle Pfuscher vor dem HERRN

---
 src/analyses/base.ml                          | 46 +++++++++++++++----
 src/analyses/baseInvariant.ml                 |  6 +--
 tests/regression/39-signed-overflows/06-abs.c |  2 -
 .../39-signed-overflows/07-abs-sqrt.c         | 10 ++++
 4 files changed, 50 insertions(+), 14 deletions(-)
 create mode 100644 tests/regression/39-signed-overflows/07-abs-sqrt.c

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index f25f0a9693..8b9b232913 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1753,15 +1753,43 @@ struct
   let branch ctx (exp:exp) (tv:bool) : store =
     let valu = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in
     let refine () =
-      let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp tv in
-      if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.EqualSet exp));
-      if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.CondVars exp));
-      if M.tracing then M.traceu "branch" "Invariant enforced!\n";
-      match ctx.ask (Queries.CondVars exp) with
-      | s when Queries.ES.cardinal s = 1 ->
-        let e = Queries.ES.choose s in
-        invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv
-      | _ -> res
+      let refine0 =
+        let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp tv in
+        if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.EqualSet exp));
+        if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.CondVars exp));
+        if M.tracing then M.traceu "branch" "Invariant enforced!\n";
+        match ctx.ask (Queries.CondVars exp) with
+        | s when Queries.ES.cardinal s = 1 ->
+          let e = Queries.ES.choose s in
+          invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv
+        | _ -> res
+      in
+      match exp with
+      | BinOp (Lt, CastE(t,Lval (Var v, NoOffset)), e,_) when tv ->
+        (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with 
+        | `Lifted (Abs arg) -> 
+          (* e.g. |arg| < 40 *)
+          let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in
+          (* arg <= e  (arg <= 40) *)
+          let le = BinOp (Le, CastE(t,arg), e, intType) in
+          (* arg >= -e  (arg >= -40) *)
+          let gt = BinOp(Ge, CastE(t,arg), UnOp (Neg, e, Cilfacade.typeOf e), intType) in
+          let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in
+          invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv
+        | _ -> refine0)
+      | BinOp (Lt, Lval (Var v, NoOffset), e, _) when tv ->
+        (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with 
+        | `Lifted (Abs arg) -> 
+          (* e.g. |arg| < 40 *)
+          let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in
+          (* arg <= e  (arg <= 40) *)
+          let le = BinOp (Le, arg, e, intType) in
+          (* arg >= -e  (arg >= -40) *)
+          let gt = BinOp(Ge, arg, UnOp (Neg, e, Cilfacade.typeOf e), intType) in
+          let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in
+          invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv
+        | _ -> refine0)
+      | _ -> refine0
     in
     if M.tracing then M.traceli "branch" ~subsys:["invariant"] "Evaluating branch for expression %a with value %a\n" d_exp exp VD.pretty valu;
     (* First we want to see, if we can determine a dead branch: *)
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index b82ab88806..397bd1623e 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -712,7 +712,7 @@ struct
               begin match t with
                 | TInt (ik, _) ->
                   begin match x with
-                    | ((Var v), offs) when query_special ->
+                    | ((Var v), offs) ->
                       if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
                       let tv_opt = ID.to_bool c in
                       begin match tv_opt with
@@ -730,7 +730,7 @@ struct
                               inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st
                             | _ -> update_lval c x c' ID.pretty
                           end
-                        | None -> update_lval c x c' ID.pretty
+                        | _ -> update_lval c x c' ID.pretty
                       end
                     | _ -> update_lval c x c' ID.pretty
                   end
@@ -749,7 +749,7 @@ struct
               begin match t with
                 | TFloat (fk, _) ->
                   begin match x with
-                    | ((Var v), offs) when query_special ->
+                    | ((Var v), offs) ->
                       if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
                       begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with
                         | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp ~query_special:false (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st
diff --git a/tests/regression/39-signed-overflows/06-abs.c b/tests/regression/39-signed-overflows/06-abs.c
index b08a0f2209..e87e25d9fe 100644
--- a/tests/regression/39-signed-overflows/06-abs.c
+++ b/tests/regression/39-signed-overflows/06-abs.c
@@ -8,8 +8,6 @@ int main() {
         {
             int result = data * data;
         }
-        
-        int result = data * data;
     }
     return 8;
 }
\ No newline at end of file
diff --git a/tests/regression/39-signed-overflows/07-abs-sqrt.c b/tests/regression/39-signed-overflows/07-abs-sqrt.c
new file mode 100644
index 0000000000..0f8ce396f2
--- /dev/null
+++ b/tests/regression/39-signed-overflows/07-abs-sqrt.c
@@ -0,0 +1,10 @@
+//PARAM: --enable ana.int.interval --enable ana.float.interval --set ana.activated[+] tmpSpecial
+#include<math.h>
+int main() {
+    int data;
+    if (data > (-0x7fffffff - 1) && abs(data) < (long)sqrt((double)0x7fffffff))
+    {
+        int result = data * data;
+    }
+    return 8;
+}
\ No newline at end of file

From 379733825fce688cec97a63a2fa32c951e7d2c10 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sat, 18 Nov 2023 12:28:22 +0100
Subject: [PATCH 10/28] Reset baseInvariant to master

---
 src/analyses/baseInvariant.ml | 69 ++++++++++++++---------------------
 1 file changed, 27 insertions(+), 42 deletions(-)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 397bd1623e..72e00efbb1 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -562,7 +562,7 @@ struct
       | TFloat (fk, _) -> fk
       | _ -> failwith "value which was expected to be a float is of different type?!"
     in
-    let rec inv_exp ?(query_special=true) c_typed exp (st:D.t) : D.t =
+    let rec inv_exp c_typed exp (st:D.t): D.t =
       (* trying to improve variables in an expression so it is bottom means dead code *)
       if VD.is_bot_value c_typed then contra st
       else
@@ -578,12 +578,12 @@ struct
             | Some false -> ID.of_bool ikind false
             | _ -> ID.top_of ikind
           in
-          inv_exp ~query_special (Int c') e st
-        | UnOp (Neg, e, _), Float c -> inv_exp ~query_special (Float (unop_FD Neg c)) e st
-        | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp ~query_special (Int (unop_ID op c)) e st
+          inv_exp (Int c') e st
+        | UnOp (Neg, e, _), Float c -> inv_exp (Float (unop_FD Neg c)) e st
+        | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st
         (* no equivalent for Float, as VD.is_safe_cast fails for all float types anyways *)
         | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_safe_cast t2 (Cilfacade.typeOf e2) ->
-          inv_exp ~query_special (Int c) (BinOp (op, e1, e2, t)) st
+          inv_exp (Int c) (BinOp (op, e1, e2, t)) st
         | BinOp (LOr, arg1, arg2, typ) as exp, Int c ->
           (* copied & modified from eval_rv_base... *)
           let (let*) = Option.bind in
@@ -631,7 +631,7 @@ struct
               in
               let definite_ad = to_definite_ad vs in
               let c' = VD.Address definite_ad in
-              Some (inv_exp ~query_special c' e st)
+              Some (inv_exp c' e st)
             | Int i ->
               let ik = ID.ikind i in
               let module BISet = IntDomain.BISet in
@@ -648,20 +648,20 @@ struct
               in
               let int_id = to_int_id vs in
               let c' = VD.Int int_id in
-              Some (inv_exp ~query_special c' e st)
+              Some (inv_exp c' e st)
             | _ ->
               None
           in
           begin match eqs_st with
             | Some st -> st
             | None when ID.to_bool c = Some true ->
-              begin match inv_exp ~query_special (Int c) arg1 st with
+              begin match inv_exp (Int c) arg1 st with
                 | st1 ->
-                  begin match inv_exp ~query_special (Int c) arg2 st with
+                  begin match inv_exp (Int c) arg2 st with
                     | st2 -> D.join st1 st2
                     | exception Analyses.Deadcode -> st1
                   end
-                | exception Analyses.Deadcode -> inv_exp ~query_special (Int c) arg2 st (* Deadcode falls through *)
+                | exception Analyses.Deadcode -> inv_exp (Int c) arg2 st (* Deadcode falls through *)
               end
             | None ->
               st (* TODO: not bothering to fall back, no other case can refine LOr anyway *)
@@ -676,15 +676,15 @@ struct
                let ikres = Cilfacade.get_ikind_exp e in (* might be different from argument types, e.g. for LT, GT, EQ, ... *)
                let a', b' = inv_bin_int (a, b) ikind (c_int ikres) op in
                if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a\n" d_exp e ID.pretty (c_int ikind) ID.pretty a' ID.pretty b';
-               let st' = inv_exp ~query_special (Int a') e1 st in
-               let st'' = inv_exp ~query_special (Int b') e2 st' in
+               let st' = inv_exp (Int a') e1 st in
+               let st'' = inv_exp (Int b') e2 st' in
                st''
              | Float a, Float b ->
                let fkind = Cilfacade.get_fkind_exp e1 in (* both operands have the same type *)
                let a', b' = inv_bin_float (a, b) (c_float fkind) op in
                if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a\n" d_exp e FD.pretty (c_float fkind) FD.pretty a' FD.pretty b';
-               let st' = inv_exp ~query_special (Float a') e1 st in
-               let st'' = inv_exp ~query_special (Float b') e2 st' in
+               let st' = inv_exp (Float a') e1 st in
+               let st'' = inv_exp (Float b') e2 st' in
                st''
              (* Mixed Float and Int cases should never happen, as there are no binary operators with one float and one int parameter ?!*)
              | Int _, Float _ | Float _, Int _ -> failwith "ill-typed program";
@@ -718,19 +718,17 @@ struct
                       begin match tv_opt with
                         | Some tv ->
                           begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with
-                            | `Lifted (Isfinite xFloat) when tv -> inv_exp ~query_special:false (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st
-                            | `Lifted (Isnan xFloat) when tv -> inv_exp ~query_special:false (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st
+                            | `Lifted (Isfinite xFloat) when tv -> inv_exp (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st
+                            | `Lifted (Isnan xFloat) when tv -> inv_exp (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st
                             (* should be correct according to C99 standard*)
-                            | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Isless (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
-                            | `Lifted (Abs xInt) ->
-                              inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st
+                            | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st
+                            | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st
+                            | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
+                            | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
+                            | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
                             | _ -> update_lval c x c' ID.pretty
                           end
-                        | _ -> update_lval c x c' ID.pretty
+                        | None -> update_lval c x c' ID.pretty
                       end
                     | _ -> update_lval c x c' ID.pretty
                   end
@@ -752,14 +750,14 @@ struct
                     | ((Var v), offs) ->
                       if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
                       begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with
-                        | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp ~query_special:false (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st
-                        | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp ~query_special:false (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st
+                        | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st
+                        | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st
                         | `Lifted (Fabs (ret_fk, xFloat)) ->
                           let inv = FD.inv_fabs (FD.cast_to ret_fk c) in
                           if FD.is_bot inv then
                             raise Analyses.Deadcode
                           else
-                            inv_exp ~query_special:false (Float inv) xFloat st
+                            inv_exp (Float inv) xFloat st
                         | _ -> update_lval c x c' FD.pretty
                       end
                     | _ -> update_lval c x c' FD.pretty
@@ -779,7 +777,7 @@ struct
            | TFloat (FLongDouble as fk, _), FDouble
            | TFloat (fk, _), FLongDouble
            | TFloat (FDouble as fk, _), FDouble
-           | TFloat (FFloat as fk, _), FFloat -> inv_exp ~query_special (Float (FD.cast_to fk c)) e st
+           | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
            | _ -> fallback ("CastE: incompatible types") st)
         | CastE ((TInt (ik, _)) as t, e), Int c
         | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
@@ -792,20 +790,7 @@ struct
                  (* let c' = ID.cast_to ik_e c in *)
                  let c' = ID.cast_to ik_e (ID.meet c (ID.cast_to ik (ID.top_of ik_e))) in (* TODO: cast without overflow, is this right for normal invariant? *)
                  if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a\n" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
-                 inv_exp ~query_special (Int c') e st
-               | x -> fallback (GobPretty.sprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st
-             else
-               fallback (GobPretty.sprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
-           | Float i ->
-             let i = FD.to_int ik i in
-             if ID.leq i (ID.cast_to ik i) then
-               match unrollType (Cilfacade.typeOf e) with
-               | TInt(ik_e, _)
-               | TEnum ({ekind = ik_e; _ }, _) ->
-                 (* let c' = ID.cast_to ik_e c in *)
-                 let c' = ID.cast_to ik_e (ID.meet c (ID.cast_to ik (ID.top_of ik_e))) in (* TODO: cast without overflow, is this right for normal invariant? *)
-                 if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a\n" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
-                 inv_exp ~query_special (Int c') e st
+                 inv_exp (Int c') e st
                | x -> fallback (GobPretty.sprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st
              else
                fallback (GobPretty.sprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st

From 6895ac0cf305747f617d8b4c42f191484f6bc072 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sat, 18 Nov 2023 12:41:37 +0100
Subject: [PATCH 11/28] Make bodge a bit nicer

---
 src/analyses/base.ml | 30 +++++++++++++-----------------
 1 file changed, 13 insertions(+), 17 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 8b9b232913..8497f38615 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1764,30 +1764,26 @@ struct
           invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv
         | _ -> res
       in
+      (* bodge for abs(...); To be removed once we have a clean solution *)
+      let refineAbs absargexp valexp =
+        (* e.g. |arg| < 40 *)
+        (* arg <= e  (arg <= 40) *)
+        let le = BinOp (Le, absargexp, valexp, intType) in
+        (* arg >= -e  (arg >= -40) *)
+        let gt = BinOp(Ge, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in
+        let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in
+        invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv
+      in
       match exp with
-      | BinOp (Lt, CastE(t,Lval (Var v, NoOffset)), e,_) when tv ->
+      | BinOp (Lt, CastE(t, Lval (Var v, NoOffset)), e,_) when tv ->
         (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with 
         | `Lifted (Abs arg) -> 
-          (* e.g. |arg| < 40 *)
-          let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in
-          (* arg <= e  (arg <= 40) *)
-          let le = BinOp (Le, CastE(t,arg), e, intType) in
-          (* arg >= -e  (arg >= -40) *)
-          let gt = BinOp(Ge, CastE(t,arg), UnOp (Neg, e, Cilfacade.typeOf e), intType) in
-          let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in
-          invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv
+          refineAbs (CastE (t, arg)) e
         | _ -> refine0)
       | BinOp (Lt, Lval (Var v, NoOffset), e, _) when tv ->
         (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with 
         | `Lifted (Abs arg) -> 
-          (* e.g. |arg| < 40 *)
-          let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in
-          (* arg <= e  (arg <= 40) *)
-          let le = BinOp (Le, arg, e, intType) in
-          (* arg >= -e  (arg >= -40) *)
-          let gt = BinOp(Ge, arg, UnOp (Neg, e, Cilfacade.typeOf e), intType) in
-          let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in
-          invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv
+          refineAbs arg e
         | _ -> refine0)
       | _ -> refine0
     in

From ba6726a4515ca4873c1abb87b58f7d9a7f535da8 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sat, 18 Nov 2023 12:50:57 +0100
Subject: [PATCH 12/28] Handle <= as well

---
 src/analyses/base.ml                          | 17 +++++++++--------
 tests/regression/39-signed-overflows/06-abs.c | 11 ++++++++++-
 2 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 8497f38615..4911b0d033 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1765,25 +1765,26 @@ struct
         | _ -> res
       in
       (* bodge for abs(...); To be removed once we have a clean solution *)
-      let refineAbs absargexp valexp =
-        (* e.g. |arg| < 40 *)
+      let refineAbs op absargexp valexp =
+        let flip op = match op with | Le -> Ge | Lt -> Gt | _ -> failwith "impossible" in
+        (* e.g. |arg| <= 40 *)
         (* arg <= e  (arg <= 40) *)
-        let le = BinOp (Le, absargexp, valexp, intType) in
+        let le = BinOp (op, absargexp, valexp, intType) in
         (* arg >= -e  (arg >= -40) *)
-        let gt = BinOp(Ge, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in
+        let gt = BinOp(flip op, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in
         let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in
         invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv
       in
       match exp with
-      | BinOp (Lt, CastE(t, Lval (Var v, NoOffset)), e,_) when tv ->
+      | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv ->
         (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with 
         | `Lifted (Abs arg) -> 
-          refineAbs (CastE (t, arg)) e
+          refineAbs op (CastE (t, arg)) e
         | _ -> refine0)
-      | BinOp (Lt, Lval (Var v, NoOffset), e, _) when tv ->
+      | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv ->
         (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with 
         | `Lifted (Abs arg) -> 
-          refineAbs arg e
+          refineAbs op arg e
         | _ -> refine0)
       | _ -> refine0
     in
diff --git a/tests/regression/39-signed-overflows/06-abs.c b/tests/regression/39-signed-overflows/06-abs.c
index e87e25d9fe..e56cc9ff7d 100644
--- a/tests/regression/39-signed-overflows/06-abs.c
+++ b/tests/regression/39-signed-overflows/06-abs.c
@@ -6,7 +6,16 @@ int main() {
     {
         if (abs(data) < 100)
         {
-            int result = data * data;
+            __goblint_check(data < 100);
+            __goblint_check(-100 < data);
+            int result = data * data; //NOWARN
+        }
+
+        if(abs(data) <= 100)
+        {
+            __goblint_check(data <= 100);
+            __goblint_check(-100 <= data);
+            int result = data * data; //NOWARN
         }
     }
     return 8;

From 8ea9ffa726f13f0d764cf2dbd7ee6a1d18270573 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sat, 18 Nov 2023 12:51:32 +0100
Subject: [PATCH 13/28] 39/07: Add NOWARN annotation

---
 tests/regression/39-signed-overflows/07-abs-sqrt.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/39-signed-overflows/07-abs-sqrt.c b/tests/regression/39-signed-overflows/07-abs-sqrt.c
index 0f8ce396f2..13ed863e51 100644
--- a/tests/regression/39-signed-overflows/07-abs-sqrt.c
+++ b/tests/regression/39-signed-overflows/07-abs-sqrt.c
@@ -4,7 +4,7 @@ int main() {
     int data;
     if (data > (-0x7fffffff - 1) && abs(data) < (long)sqrt((double)0x7fffffff))
     {
-        int result = data * data;
+        int result = data * data; //NOWARN
     }
     return 8;
 }
\ No newline at end of file

From f6cef727d38bd2deb0c766d2f8bc6c726024bbbc Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 19 Nov 2023 19:27:55 +0100
Subject: [PATCH 14/28] `<<` Fix wrong order of `minimal`/`maximal`

---
 src/cdomains/intDomain.ml                           | 2 +-
 tests/regression/39-signed-overflows/06-shiftleft.c | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index 49065b9cc5..5a80d67bfe 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -874,7 +874,7 @@ struct
     | true, _
     | _   , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show a) (show b)))
     | _ ->
-      match a, maximal b, minimal b with
+      match a, minimal b, maximal b with
       | Some a, Some bl, Some bu when (Ints_t.compare bl Ints_t.zero >= 0) ->
         (try
            let r = IArith.shiftleft a (Ints_t.to_int bl, Ints_t.to_int bu) in
diff --git a/tests/regression/39-signed-overflows/06-shiftleft.c b/tests/regression/39-signed-overflows/06-shiftleft.c
index 987775c6f7..aff853ee36 100644
--- a/tests/regression/39-signed-overflows/06-shiftleft.c
+++ b/tests/regression/39-signed-overflows/06-shiftleft.c
@@ -19,5 +19,8 @@ int main()
     __goblint_check(r >= 8);
     __goblint_check(r <= 16);
 
+    int regval;
+    unsigned long bla = (unsigned long )((1 << ((int )regval >> 6)) << 20);  //WARN
+
     return 0;
 }

From 85e6fdbfcba3d42bf35b44f1c41171e958890451 Mon Sep 17 00:00:00 2001
From: oliver <ge96xey@mytum.de>
Date: Mon, 20 Nov 2023 01:55:30 +0100
Subject: [PATCH 15/28] bump dune dependencies and rebuild goblint.opam

---
 goblint.opam        | 2 +-
 goblint.opam.locked | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index bf51924626..34912fde26 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -19,7 +19,7 @@ homepage: "https://goblint.in.tum.de"
 doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
-  "dune" {>= "3.6"}
+  "dune" {>= "3.7"}
   "ocaml" {>= "4.10"}
   "goblint-cil" {>= "2.0.2"}
   "batteries" {>= "3.5.0"}
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 0abe989955..6e15ac8900 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -76,7 +76,7 @@ depends: [
   "ocamlfind" {= "1.9.5"}
   "odoc" {= "2.2.0" & with-doc}
   "odoc-parser" {= "2.0.0" & with-doc}
-  "ordering" {= "3.6.1"}
+  "ordering" {= "3.7.1"}
   "ounit2" {= "2.2.6" & with-test}
   "pp" {= "1.1.2"}
   "ppx_derivers" {= "1.2.1"}
@@ -93,7 +93,7 @@ depends: [
   "sexplib0" {= "v0.15.1"}
   "sha" {= "1.15.2"}
   "stdlib-shims" {= "0.3.0"}
-  "stdune" {= "3.6.1"}
+  "stdune" {= "3.7.1"}
   "stringext" {= "1.6.0"}
   "topkg" {= "1.0.6"}
   "tyxml" {= "4.5.0" & with-doc}

From 9d77dec344287d4ad42e723abfa5777dc3d01afc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 20 Nov 2023 11:59:44 +0200
Subject: [PATCH 16/28] Move abs refine to BaseInvariant

---
 src/analyses/base.ml          | 43 ++++++++---------------------------
 src/analyses/baseInvariant.ml | 27 ++++++++++++++++++++++
 2 files changed, 36 insertions(+), 34 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 4911b0d033..f25f0a9693 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1753,40 +1753,15 @@ struct
   let branch ctx (exp:exp) (tv:bool) : store =
     let valu = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in
     let refine () =
-      let refine0 =
-        let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp tv in
-        if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.EqualSet exp));
-        if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.CondVars exp));
-        if M.tracing then M.traceu "branch" "Invariant enforced!\n";
-        match ctx.ask (Queries.CondVars exp) with
-        | s when Queries.ES.cardinal s = 1 ->
-          let e = Queries.ES.choose s in
-          invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv
-        | _ -> res
-      in
-      (* bodge for abs(...); To be removed once we have a clean solution *)
-      let refineAbs op absargexp valexp =
-        let flip op = match op with | Le -> Ge | Lt -> Gt | _ -> failwith "impossible" in
-        (* e.g. |arg| <= 40 *)
-        (* arg <= e  (arg <= 40) *)
-        let le = BinOp (op, absargexp, valexp, intType) in
-        (* arg >= -e  (arg >= -40) *)
-        let gt = BinOp(flip op, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in
-        let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in
-        invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv
-      in
-      match exp with
-      | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv ->
-        (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with 
-        | `Lifted (Abs arg) -> 
-          refineAbs op (CastE (t, arg)) e
-        | _ -> refine0)
-      | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv ->
-        (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with 
-        | `Lifted (Abs arg) -> 
-          refineAbs op arg e
-        | _ -> refine0)
-      | _ -> refine0
+      let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp tv in
+      if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.EqualSet exp));
+      if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.CondVars exp));
+      if M.tracing then M.traceu "branch" "Invariant enforced!\n";
+      match ctx.ask (Queries.CondVars exp) with
+      | s when Queries.ES.cardinal s = 1 ->
+        let e = Queries.ES.choose s in
+        invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv
+      | _ -> res
     in
     if M.tracing then M.traceli "branch" ~subsys:["invariant"] "Evaluating branch for expression %a with value %a\n" d_exp exp VD.pretty valu;
     (* First we want to see, if we can determine a dead branch: *)
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 72e00efbb1..a99e25e7c6 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -821,4 +821,31 @@ struct
             FD.top_of fk
         in
         inv_exp (Float ftv) exp st
+
+  let invariant ctx a gs st exp tv: D.t =
+    let refine0 = invariant ctx a gs st exp tv in
+    (* bodge for abs(...); To be removed once we have a clean solution *)
+    let refineAbs op absargexp valexp =
+      let flip op = match op with | Le -> Ge | Lt -> Gt | _ -> failwith "impossible" in
+      (* e.g. |arg| <= 40 *)
+      (* arg <= e  (arg <= 40) *)
+      let le = BinOp (op, absargexp, valexp, intType) in
+      (* arg >= -e  (arg >= -40) *)
+      let gt = BinOp(flip op, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in
+      let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in
+      invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv
+    in
+    match exp with
+    | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv ->
+      (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with
+      | `Lifted (Abs arg) ->
+        refineAbs op (CastE (t, arg)) e
+      | _ -> refine0)
+    | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv ->
+      (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with
+      | `Lifted (Abs arg) ->
+        refineAbs op arg e
+      | _ -> refine0)
+    | _ -> refine0
+
 end

From 0cb1b7e1135fee97db9d4d7da6a90c1bc8261fa5 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 20 Nov 2023 12:04:21 +0200
Subject: [PATCH 17/28] Fix BaseInvariant abs indentation

---
 src/analyses/baseInvariant.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index a99e25e7c6..86ec0d3bf7 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -837,15 +837,15 @@ struct
     in
     match exp with
     | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv ->
-      (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with
-      | `Lifted (Abs arg) ->
-        refineAbs op (CastE (t, arg)) e
-      | _ -> refine0)
+      begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with
+        | `Lifted (Abs arg) -> refineAbs op (CastE (t, arg)) e
+        | _ -> refine0
+      end
     | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv ->
-      (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with
-      | `Lifted (Abs arg) ->
-        refineAbs op arg e
-      | _ -> refine0)
+      begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with
+        | `Lifted (Abs arg) -> refineAbs op arg e
+        | _ -> refine0
+      end
     | _ -> refine0
 
 end

From 19190ca63d43aaf14ae462823b3878ce65b25606 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Mon, 20 Nov 2023 11:09:26 +0100
Subject: [PATCH 18/28] remove special cases handled by general case

---
 src/analyses/base.ml | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index f25f0a9693..2a729c685e 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2339,13 +2339,9 @@ struct
              | None, _ -> ID.top_of ik
              | Some mx, Some mm when Z.equal mx mm -> ID.top_of ik
              | _, _ ->
-               match ID.le xcast (ID.of_int ik Z.zero) with
-               | d when d = ID.of_int ik Z.zero -> xcast (* x positive *)
-               | d when d = ID.of_int ik Z.one -> ID.neg xcast (* x negative *)
-               | _ -> (* both possible *)
-                 let x1 = ID.neg (ID.meet (ID.ending ik Z.zero) xcast) in
-                 let x2 = ID.meet (ID.starting ik Z.zero) xcast in
-                 ID.join x1 x2
+               let x1 = ID.neg (ID.meet (ID.ending ik Z.zero) xcast) in
+               let x2 = ID.meet (ID.starting ik Z.zero) xcast in
+               ID.join x1 x2
             )
           | _ -> failwith ("non-integer argument in call to function "^f.vname)
         end

From 5784ffeb5f0e26b4da059a0d762480a0ce999505 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 20 Nov 2023 14:44:56 +0200
Subject: [PATCH 19/28] Update Gobview submodule for dune 3.7.1 lock

---
 gobview | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/gobview b/gobview
index 42b07f8253..b4467d820f 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit 42b07f825316052ec030370daf0d00ebe28ec092
+Subproject commit b4467d820f28bac578fc0baf7f81393c67f6b82b

From 631f4fc69cf667a957a7575f653210a3702135c6 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Mon, 20 Nov 2023 16:25:47 +0100
Subject: [PATCH 20/28] Do not set overflow flag on cast.

---
 src/cdomains/intDomain.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index 3bc84ae676..0a98e57a29 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -3410,14 +3410,14 @@ module IntDomTupleImpl = struct
     | Some(_, {underflow; overflow}) -> not (underflow || overflow)
     | _ -> false
 
-  let check_ov ik intv intv_set =
+  let check_ov ~cast ik intv intv_set =
     let no_ov = (no_overflow ik intv) || (no_overflow ik intv_set) in
     if not no_ov && ( BatOption.is_some intv || BatOption.is_some intv_set) then (
       let (_,{underflow=underflow_intv; overflow=overflow_intv}) = match intv with None -> (I2.bot (), {underflow= true; overflow = true}) | Some x -> x in
       let (_,{underflow=underflow_intv_set; overflow=overflow_intv_set}) = match intv_set with None -> (I5.bot (), {underflow= true; overflow = true}) | Some x -> x in
       let underflow = underflow_intv && underflow_intv_set in
       let overflow = overflow_intv && overflow_intv_set in
-      set_overflow_flag ~cast:false ~underflow ~overflow ik;
+      set_overflow_flag ~cast ~underflow ~overflow ik;
     );
     no_ov
 
@@ -3426,7 +3426,7 @@ module IntDomTupleImpl = struct
     let map x = Option.map fst x in
     let intv =  f p2 @@ r.fi2_ovc (module I2) in
     let intv_set = f p5 @@ r.fi2_ovc (module I5) in
-    ignore (check_ov ik intv intv_set);
+    ignore (check_ov ~cast:false ik intv intv_set);
     map @@ f p1 @@ r.fi2_ovc (module I1), map @@ f p2 @@ r.fi2_ovc (module I2), map @@ f p3 @@ r.fi2_ovc (module I3), map @@ f p4 @@ r.fi2_ovc (module I4), map @@ f p5 @@ r.fi2_ovc (module I5)
 
   let create2_ovc ik r x = (* use where values are introduced *)
@@ -3607,7 +3607,7 @@ module IntDomTupleImpl = struct
     let map f ?no_ov = function Some x -> Some (f ?no_ov x) | _ -> None  in
     let intv = map (r.f1_ovc (module I2)) b in
     let intv_set = map (r.f1_ovc (module I5)) e in
-    let no_ov = check_ov ik intv intv_set in
+    let no_ov = check_ov ~cast ik intv intv_set in
     let no_ov = no_ov || should_ignore_overflow ik in
     refine ik
       ( map (fun ?no_ov x -> r.f1_ovc ?no_ov (module I1) x |> fst) a
@@ -3617,10 +3617,10 @@ module IntDomTupleImpl = struct
       , BatOption.map fst intv_set )
 
   (* map2 with overflow check *)
-  let map2ovc ik r (xa, xb, xc, xd, xe) (ya, yb, yc, yd, ye) =
+  let map2ovc ?(cast=false) ik r (xa, xb, xc, xd, xe) (ya, yb, yc, yd, ye) =
     let intv = opt_map2 (r.f2_ovc (module I2)) xb yb in
     let intv_set = opt_map2 (r.f2_ovc (module I5)) xe ye in
-    let no_ov = check_ov ik intv intv_set in
+    let no_ov = check_ov ~cast ik intv intv_set in
     let no_ov = no_ov || should_ignore_overflow ik in
     refine ik
       ( opt_map2 (fun ?no_ov x y -> r.f2_ovc ?no_ov (module I1) x y |> fst) xa ya

From 4f7eb52a54b75e01740f065eb4e3eccf783adabb Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Mon, 20 Nov 2023 16:33:28 +0100
Subject: [PATCH 21/28] Add test case for cast.

---
 tests/regression/29-svcomp/32-no-ov.c | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 tests/regression/29-svcomp/32-no-ov.c

diff --git a/tests/regression/29-svcomp/32-no-ov.c b/tests/regression/29-svcomp/32-no-ov.c
new file mode 100644
index 0000000000..0167098c29
--- /dev/null
+++ b/tests/regression/29-svcomp/32-no-ov.c
@@ -0,0 +1,7 @@
+// PARAM: --enable ana.int.interval --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )"
+
+int main(){
+	// This is not an overflow, just implementation defined behavior on a cast
+	int data = ((int)(rand() & 1 ? (((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand()) : -(((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand()) - 1));
+	return 0;
+}
\ No newline at end of file

From 5a8863089b4526f51f997b58c22bba77427ac4e3 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 20 Nov 2023 16:58:57 +0100
Subject: [PATCH 22/28] Unify naming

---
 src/cdomains/intDomain.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index 5a80d67bfe..fde09a797a 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -610,7 +610,7 @@ module IntervalArith(Ints_t : IntOps.IntOps) = struct
     let x2y2 = (Ints_t.mul x2 y2) in
     (min4 x1y1 x1y2 x2y1 x2y2, max4 x1y1 x1y2 x2y1 x2y2)
 
-  let shiftleft (x1,x2) (y1,y2) =
+  let shift_left (x1,x2) (y1,y2) =
     let y1p = Ints_t.shift_left Ints_t.one y1 in
     let y2p = Ints_t.shift_left Ints_t.one y2 in
     mul (x1, x2) (y1p, y2p)
@@ -877,7 +877,7 @@ struct
       match a, minimal b, maximal b with
       | Some a, Some bl, Some bu when (Ints_t.compare bl Ints_t.zero >= 0) ->
         (try
-           let r = IArith.shiftleft a (Ints_t.to_int bl, Ints_t.to_int bu) in
+           let r = IArith.shift_left a (Ints_t.to_int bl, Ints_t.to_int bu) in
            norm ik @@ Some r
          with Z.Overflow -> (top_of ik,{underflow=false; overflow=true}))
       | _              -> (top_of ik,{underflow=true; overflow=true})

From c9be89e68cd01a189f336f350cf8cae12c505b43 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Mon, 20 Nov 2023 19:40:40 +0100
Subject: [PATCH 23/28] add support for labs and llabs

---
 src/analyses/base.ml                          |  2 +-
 src/analyses/baseInvariant.ml                 |  4 ++--
 src/analyses/libraryDesc.ml                   |  4 ++--
 src/analyses/libraryFunctions.ml              |  4 +++-
 .../regression/39-signed-overflows/08-labs.c  | 22 +++++++++++++++++++
 .../39-signed-overflows/09-labs-sqrt.c        | 10 +++++++++
 6 files changed, 40 insertions(+), 6 deletions(-)
 create mode 100644 tests/regression/39-signed-overflows/08-labs.c
 create mode 100644 tests/regression/39-signed-overflows/09-labs-sqrt.c

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 2a729c685e..84be8c7a19 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2375,7 +2375,7 @@ struct
           | Fmax (fd, x ,y) -> Float (apply_binary fd FD.fmax x y)
           | Fmin (fd, x ,y) -> Float (apply_binary fd FD.fmin x y)
           | Sqrt (fk, x) -> Float (apply_unary fk FD.sqrt x)
-          | Abs x -> Int (ID.cast_to IInt (apply_abs IInt x))
+          | Abs (ik, x) -> Int (ID.cast_to ik (apply_abs ik x))
         end
       in
       begin match lv with
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 86ec0d3bf7..f391231628 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -838,12 +838,12 @@ struct
     match exp with
     | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv ->
       begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with
-        | `Lifted (Abs arg) -> refineAbs op (CastE (t, arg)) e
+        | `Lifted (Abs (ik, arg)) -> refineAbs op (CastE (t, arg)) e
         | _ -> refine0
       end
     | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv ->
       begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with
-        | `Lifted (Abs arg) -> refineAbs op arg e
+        | `Lifted (Abs (ik, arg)) -> refineAbs op arg e
         | _ -> refine0
       end
     | _ -> refine0
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
index 8cd3dfa1ba..45887b9c6b 100644
--- a/src/analyses/libraryDesc.ml
+++ b/src/analyses/libraryDesc.ml
@@ -27,7 +27,7 @@ type math =
   | Islessequal of (Basetype.CilExp.t * Basetype.CilExp.t)
   | Islessgreater of (Basetype.CilExp.t * Basetype.CilExp.t)
   | Isunordered of (Basetype.CilExp.t * Basetype.CilExp.t)
-  | Abs of Basetype.CilExp.t
+  | Abs of (CilType.Ikind.t * Basetype.CilExp.t)
   | Ceil of (CilType.Fkind.t * Basetype.CilExp.t)
   | Floor of (CilType.Fkind.t * Basetype.CilExp.t)
   | Fabs of (CilType.Fkind.t * Basetype.CilExp.t)
@@ -160,7 +160,7 @@ module MathPrintable = struct
     | Islessequal (exp1, exp2) -> Pretty.dprintf "isLessEqual(%a, %a)" d_exp exp1 d_exp exp2
     | Islessgreater (exp1, exp2) -> Pretty.dprintf "isLessGreater(%a, %a)" d_exp exp1 d_exp exp2
     | Isunordered (exp1, exp2) -> Pretty.dprintf "isUnordered(%a, %a)" d_exp exp1 d_exp exp2
-    | Abs exp -> Pretty.dprintf "abs(%a)" d_exp exp
+    | Abs (ik, exp) -> Pretty.dprintf "(%a )abs(%a)" d_ikind ik d_exp exp
     | Ceil (fk, exp) -> Pretty.dprintf "(%a )ceil(%a)" d_fkind fk d_exp exp
     | Floor (fk, exp) -> Pretty.dprintf "(%a )floor(%a)" d_fkind fk d_exp exp
     | Fabs (fk, exp) -> Pretty.dprintf "(%a )fabs(%a)" d_fkind fk d_exp exp
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index ae33f57f70..838d1817a9 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -130,7 +130,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("wcstombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r]; drop "size" []]);
     ("wcsrtombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r_deep; w]; drop "size" []; drop "ps" [r_deep; w_deep]]);
     ("mbstowcs", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []]);
-    ("abs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs j) });
+    ("abs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (IInt, j)) });
+    ("labs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) });
+    ("llabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILongLong, j)) });
     ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
     ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
diff --git a/tests/regression/39-signed-overflows/08-labs.c b/tests/regression/39-signed-overflows/08-labs.c
new file mode 100644
index 0000000000..a9c6773d11
--- /dev/null
+++ b/tests/regression/39-signed-overflows/08-labs.c
@@ -0,0 +1,22 @@
+//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial
+#include<stdlib.h>
+int main() {
+    long data;
+    if (data > (-0xffffffff - 1))
+    {
+        if (labs(data) < 100)
+        {
+            __goblint_check(data < 100);
+            __goblint_check(-100 < data);
+            int result = data * data; //NOWARN
+        }
+
+        if(labs(data) <= 100)
+        {
+            __goblint_check(data <= 100);
+            __goblint_check(-100 <= data);
+            int result = data * data; //NOWARN
+        }
+    }
+    return 8;
+}
diff --git a/tests/regression/39-signed-overflows/09-labs-sqrt.c b/tests/regression/39-signed-overflows/09-labs-sqrt.c
new file mode 100644
index 0000000000..3a4b20a82b
--- /dev/null
+++ b/tests/regression/39-signed-overflows/09-labs-sqrt.c
@@ -0,0 +1,10 @@
+//PARAM: --enable ana.int.interval --enable ana.float.interval --set ana.activated[+] tmpSpecial
+#include<math.h>
+int main() {
+    int data;
+    if (data > (-0x7fffffff - 1) && llabs(data) < (long)sqrt((double)0x7fffffff))
+    {
+        int result = data * data; //NOWARN
+    }
+    return 8;
+}

From 75b3b83e1500f515ca6f3c4fecb3fe4908507fca Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Mon, 20 Nov 2023 20:19:07 +0100
Subject: [PATCH 24/28] add autotuner for math functions (activates tmpSpecial
 and float domain)

---
 src/autoTune.ml                     | 14 ++++++++++++++
 src/common/util/options.schema.json |  2 +-
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 7ddc1aee43..77d91f9652 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -458,6 +458,17 @@ let wideningOption factors file =
       print_endline "Enabled widening thresholds";
   }
 
+let activateTmpSpecialAnalysis () =
+  let isMathFun = function
+    | LibraryDesc.Math _ -> true
+    | _ -> false
+  in
+  let hasMathFunctions = hasFunction isMathFun in
+  if hasMathFunctions then (
+    print_endline @@ "math function -> enabling tmpSpecial analysis and floating-point domain";
+    enableAnalyses ["tmpSpecial"];
+    set_bool "ana.float.interval" true;
+  )
 
 let estimateComplexity factors file =
   let pathsEstimate = factors.loops + factors.controlFlowStatements / 90 in
@@ -518,6 +529,9 @@ let chooseConfig file =
   if isActivated "arrayDomain" then
     selectArrayDomains file;
 
+  if isActivated "tmpSpecialAnalysis" then
+    activateTmpSpecialAnalysis ();
+
   let options = [] in
   let options = if isActivated "congruence" then (congruenceOption factors file)::options else options in
   let options = if isActivated "octagon" then (apronOctagonOption factors file)::options else options in
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 4e282b19a4..b392f56cd6 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -544,7 +544,7 @@
               "type": "array",
               "items": { "type": "string" },
               "default": [
-                "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds", "memsafetySpecification"
+                "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds", "memsafetySpecification", "tmpSpecialAnalysis"
               ]
             }
           },

From 464cdd35d3fb7b3358e9be0902035be0358511ea Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Tue, 21 Nov 2023 09:01:33 +0100
Subject: [PATCH 25/28] Add cram test for sv-comp no-ov verdict.

---
 tests/regression/29-svcomp/32-no-ov.t | 16 ++++++++++++++++
 tests/regression/29-svcomp/dune       |  2 ++
 2 files changed, 18 insertions(+)
 create mode 100644 tests/regression/29-svcomp/32-no-ov.t
 create mode 100644 tests/regression/29-svcomp/dune

diff --git a/tests/regression/29-svcomp/32-no-ov.t b/tests/regression/29-svcomp/32-no-ov.t
new file mode 100644
index 0000000000..92e53a914c
--- /dev/null
+++ b/tests/regression/29-svcomp/32-no-ov.t
@@ -0,0 +1,16 @@
+  $ goblint --enable ana.int.interval --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )"  32-no-ov.c
+  SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
+  [Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (32-no-ov.c:5:6-5:159)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 3
+    dead: 0
+    total lines: 3
+  SV-COMP result: true
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
diff --git a/tests/regression/29-svcomp/dune b/tests/regression/29-svcomp/dune
new file mode 100644
index 0000000000..23c0dd3290
--- /dev/null
+++ b/tests/regression/29-svcomp/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c)))

From 746014d9f9610afb4750c60fb50770a5d6f9cfb9 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Tue, 21 Nov 2023 12:01:35 +0100
Subject: [PATCH 26/28] Extend test case.

---
 tests/regression/39-signed-overflows/06-shiftleft.c | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/tests/regression/39-signed-overflows/06-shiftleft.c b/tests/regression/39-signed-overflows/06-shiftleft.c
index aff853ee36..a8cb83381c 100644
--- a/tests/regression/39-signed-overflows/06-shiftleft.c
+++ b/tests/regression/39-signed-overflows/06-shiftleft.c
@@ -1,5 +1,6 @@
 // PARAM: --enable ana.int.interval
 #include <goblint.h>
+#include <limits.h>
 int main()
 {
     int r;
@@ -19,8 +20,12 @@ int main()
     __goblint_check(r >= 8);
     __goblint_check(r <= 16);
 
-    int regval;
-    unsigned long bla = (unsigned long )((1 << ((int )regval >> 6)) << 20);  //WARN
+    int regval = INT_MAX;
+    int shift = ((int )regval >> 6); //NOWARN
+    int blub = 1 << shift; //WARN
+
+    int regval2;
+    unsigned long bla = (unsigned long )((1 << ((int )regval2 >> 6)) << 20);  //WARN
 
     return 0;
 }

From 4e330e49d44226eaa1fb77d22f767d6af162c01c Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Tue, 21 Nov 2023 12:03:12 +0100
Subject: [PATCH 27/28] Remove unnecessary cast and parantheses.

---
 tests/regression/39-signed-overflows/06-shiftleft.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/39-signed-overflows/06-shiftleft.c b/tests/regression/39-signed-overflows/06-shiftleft.c
index a8cb83381c..7e790306ca 100644
--- a/tests/regression/39-signed-overflows/06-shiftleft.c
+++ b/tests/regression/39-signed-overflows/06-shiftleft.c
@@ -21,7 +21,7 @@ int main()
     __goblint_check(r <= 16);
 
     int regval = INT_MAX;
-    int shift = ((int )regval >> 6); //NOWARN
+    int shift = regval >> 6; //NOWARN
     int blub = 1 << shift; //WARN
 
     int regval2;

From f6c9a52fb5c9fae1564ee038fd1c8ef374fa0304 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Tue, 21 Nov 2023 12:30:35 +0100
Subject: [PATCH 28/28] Add tmpSpecialAnalysis to ana.autotune.activated in
 svcomp.json.

---
 conf/svcomp.json | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/conf/svcomp.json b/conf/svcomp.json
index 73f99500b9..c915620987 100644
--- a/conf/svcomp.json
+++ b/conf/svcomp.json
@@ -71,7 +71,8 @@
         "octagon",
         "wideningThresholds",
         "loopUnrollHeuristic",
-        "memsafetySpecification"
+        "memsafetySpecification",
+        "tmpSpecialAnalysis"
       ]
     }
   },