Handle <= as well

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

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;