Address semgrep findings

src/analyses/baseInvariant.ml

@@ -168,7 +168,7 @@ struct
           | Int n -> begin
               let ikind = Cilfacade.get_ikind_exp (Lval lval) in
               let n = ID.cast_to ikind n in
-              let range_from x = if tv then ID.ending ikind (Z.sub x Z.one) else ID.starting ikind x in
+              let range_from x = if tv then ID.ending ikind (Z.pred x) else ID.starting ikind x in
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
               | Some n ->
@@ -183,7 +183,7 @@ struct
           | Int n -> begin
               let ikind = Cilfacade.get_ikind_exp (Lval lval) in
               let n = ID.cast_to ikind n in
-              let range_from x = if tv then ID.ending ikind x else ID.starting ikind (Z.add x Z.one) in
+              let range_from x = if tv then ID.ending ikind x else ID.starting ikind (Z.succ x) in
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
               | Some n ->
@@ -380,8 +380,8 @@ struct
           | _, _ -> a, b
         end
       | Lt | Le | Ge | Gt as op ->
-        let pred x = Z.sub x Z.one in
-        let succ x = Z.add x Z.one in
+        let pred x = Z.pred x in
+        let succ x = Z.succ x in
         (match ID.minimal a, ID.maximal a, ID.minimal b, ID.maximal b with
          | Some l1, Some u1, Some l2, Some u2 ->
            (* if M.tracing then M.tracel "inv" "Op: %s, l1: %Ld, u1: %Ld, l2: %Ld, u2: %Ld\n" (show_binop op) l1 u1 l2 u2; *)

src/cdomain/value/cdomains/arrayDomain.ml

@@ -556,7 +556,7 @@ struct
         | Some l ->
           begin
             match Idx.to_int l with
-            | Some i -> BatOption.map_default (Z.equal (Z.sub i Z.one)) false (exp_value e)
+            | Some i -> BatOption.map_default (Z.equal (Z.pred i)) false (exp_value e)
             | None -> false
           end
         | _ -> false
@@ -596,10 +596,10 @@ struct
             else if Cil.isConstant e && Cil.isConstant i' then
               match Cil.getInteger e, Cil.getInteger i' with
               | Some (e'': Cilint.cilint), Some i'' ->
-                if Z.equal  i'' (Z.add e'' Z.one) then
+                if Z.equal  i'' (Z.succ e'') then
                   (* If both are integer constants and they are directly adjacent, we change partitioning to maintain information *)
                   Partitioned (i', (Val.join xl xm, a, xr))
-                else if Z.equal e'' (Z.add i'' Z.one) then
+                else if Z.equal e'' (Z.succ i'') then
                   Partitioned (i', (xl, a, Val.join xm xr))
                 else
                   default
@@ -673,7 +673,7 @@ struct
         begin
           match Idx.to_int l with
           | Some i ->
-            v = Some (Z.sub i Z.one)
+            v = Some (Z.pred i)
           | None -> false
         end
       | None -> false
@@ -748,7 +748,7 @@ struct
         begin
           match Idx.to_int l with
           | Some i ->
-            v = Some (Z.sub i Z.one)
+            v = Some (Z.pred i)
           | None -> false
         end
       | None -> false

src/cdomain/value/cdomains/intDomain.ml

@@ -1803,7 +1803,7 @@ struct
   type inc = Inc of BISet.t [@@unboxed]
   let max_of_range r = Size.max_from_bit_range (Option.get (R.maximal r))
   let min_of_range r = Size.min_from_bit_range (Option.get (R.minimal r))
-  let cardinality_of_range r = Z.add Z.one (Z.add (Z.neg (min_of_range r)) (max_of_range r))
+  let cardinality_of_range r = Z.succ (Z.add (Z.neg (min_of_range r)) (max_of_range r))
 
   let cardinality_BISet s =
     Z.of_int (BISet.cardinal s)
@@ -1831,13 +1831,13 @@ struct
           let min_b, max_b = min_of_range s, max_of_range s in
           let leq1 = (* check whether the elements in [r_l; s_l-1] are all in xs, i.e. excluded *)
             if Z.compare min_a min_b < 0 then
-              GobZ.for_all_range (fun x -> BISet.mem x xs) (min_a, Z.sub min_b Z.one)
+              GobZ.for_all_range (fun x -> BISet.mem x xs) (min_a, Z.pred min_b)
             else
               true
           in
           let leq2 () = (* check whether the elements in [s_u+1; r_u] are all in xs, i.e. excluded *)
             if Z.compare max_b max_a < 0 then
-              GobZ.for_all_range (fun x -> BISet.mem x xs) (Z.add max_b Z.one, max_a)
+              GobZ.for_all_range (fun x -> BISet.mem x xs) (Z.succ max_b, max_a)
             else
               true
           in
@@ -2651,7 +2651,7 @@ module Enums : S with type int_t = BigInt.t = struct
     | Exc (excl,r) ->
       let rec decrement_while_contained v =
         if BISet.mem v excl
-        then decrement_while_contained (Z.sub v Z.one)
+        then decrement_while_contained (Z.pred v)
         else v
       in
       let range_max = Exclusion.max_of_range r in
@@ -2663,7 +2663,7 @@ module Enums : S with type int_t = BigInt.t = struct
     | Exc (excl,r) ->
       let rec increment_while_contained v =
         if BISet.mem v excl
-        then increment_while_contained (Z.add v Z.one)
+        then increment_while_contained (Z.succ v)
         else v
       in
       let range_min = Exclusion.min_of_range r in
@@ -3008,7 +3008,7 @@ struct
     else
       (* Find largest m'=2^k (for some k) such that m is divisible by m' *)
       let tz = Z.trailing_zeros m in
-      let m' = Z.shift_left (Z.of_int 1) tz in
+      let m' = Z.shift_left Z.one tz in
 
       let max = (snd (Size.range ik)) +: Z.one in
       if m' >=: max then