Re-use of Interval.invariant_ikind

As suggested from the conversation: goblint#966 (comment)
BilelGho · Jan 21, 2023 · b8762a8 · b8762a8
1 parent 8eacb08
commit b8762a8
Showing 1 changed file with 3 additions and 13 deletions.
diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
@@ -1290,19 +1290,9 @@ struct
 
   let of_bool _ik = function true -> one | false -> zero
 
-  let invariant_ikind_interval e ik x = match x with
-  | (x1, x2) when Ints_t.compare x1 x2 = 0 ->
-    let x1 = Ints_t.to_bigint x1 in
-    Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x1, intType))
-  | (x1, x2) ->
-    let open Invariant in
-    let (min_ik, max_ik) = range ik in
-    let (x1', x2') = BatTuple.Tuple2.mapn (Ints_t.to_bigint) (x1, x2) in
-    let i1 = if Ints_t.compare min_ik x1 <> 0 then of_exp Cil.(BinOp (Le, kintegerCilint ik x1', e, intType)) else none in
-    let i2 = if Ints_t.compare x2 max_ik <> 0 then of_exp Cil.(BinOp (Le, e, kintegerCilint ik x2', intType)) else none in
-    i1 && i2
-
-  let invariant_ikind e ik xs = List.map (invariant_ikind_interval e ik) xs |> let open Invariant in List.fold_left (||) (bot ())
+  let invariant_ikind e ik xs = 
+    List.map (fun x -> Interval_functor.invariant_ikind e ik (Some x)) xs |> 
+    let open Invariant in List.fold_left (||) (bot ())
 
   let modulo n k =
     let result = Ints_t.rem n k in