Skip to content

Commit 297343d

Browse files
committed
Simplify int comparisons in def_exc and enums domains
1 parent d393f28 commit 297343d

File tree

2 files changed

+9
-9
lines changed

2 files changed

+9
-9
lines changed

src/cdomain/value/cdomains/int/defExcDomain.ml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -466,7 +466,7 @@ struct
466466
| `Excluded (s, ((min, max) as r)) ->
467467
let s' = S.map Z.lognot s in
468468
let r' =
469-
if Int.compare (-max) 0 <= 0 && Int.compare (-min) 0 > 0 then
469+
if -max <= 0 && -min > 0 then
470470
(-max, -min)
471471
else
472472
apply_range Z.lognot r
@@ -483,7 +483,7 @@ struct
483483
else if Z.equal i Z.one then
484484
of_interval IBool (Z.zero, Z.one)
485485
else (
486-
match Z.compare i Z.zero >= 0, Int.compare r1 0 >= 0 with
486+
match Z.compare i Z.zero >= 0, r1 >= 0 with
487487
| true, true -> `Excluded (S.empty (), (0, Int.min r2 (Z.numbits i)))
488488
| true, _ -> `Excluded (S.empty (), (0, Z.numbits i))
489489
| _, true -> `Excluded (S.empty (), (0, r2))
@@ -492,7 +492,7 @@ struct
492492
`Excluded (S.empty (), (-b, b))
493493
)
494494
| `Excluded (_, ((p1, p2) as p)), `Excluded (_, ((r1, r2) as r)) ->
495-
begin match Int.compare p1 0 >= 0, Int.compare r1 0 >= 0 with
495+
begin match p1 >= 0, r1 >= 0 with
496496
| true, true -> `Excluded (S.empty (), (0, Int.min p2 r2))
497497
| true, _ -> `Excluded (S.empty (), (0, p2))
498498
| _, true -> `Excluded (S.empty (), (0, r2))
@@ -527,12 +527,12 @@ struct
527527
| `Definite i, `Excluded (_, (r1, r2))
528528
| `Excluded (_, (r1, r2)), `Definite i ->
529529
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
530-
if Int.compare r1 0 >= 0 && Z.compare i Z.zero >= 0 then
530+
if r1 >= 0 && Z.compare i Z.zero >= 0 then
531531
`Excluded (S.empty (), (0, b))
532532
else
533533
`Excluded (S.empty (), (-b, b))
534534
| `Excluded (_, (p1, p2)), `Excluded (_, (r1, r2)) ->
535-
if Int.compare p1 0 >= 0 && Int.compare r1 0 >= 0 then
535+
if p1 >= 0 && r1 >= 0 then
536536
`Excluded (S.empty (), (0, Int.max p2 r2))
537537
else (
538538
let b = List.fold_left Int.max 0 (List.map Int.abs [p1; p2; r1; r2]) in

src/cdomain/value/cdomains/int/enumsDomain.ml

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -244,7 +244,7 @@ module Enums : S with type int_t = Z.t = struct
244244
| Inc x, Exc (s, (r1, r2))
245245
| Exc (s, (r1, r2)), Inc x ->
246246
let f i =
247-
match Z.compare i Z.zero >= 0, Int.compare r1 0 >= 0 with
247+
match Z.compare i Z.zero >= 0, r1 >= 0 with
248248
| true, true -> (0, Int.min r2 (Z.numbits i))
249249
| true, _ -> (0, Z.numbits i)
250250
| _, true -> (0, r2)
@@ -255,7 +255,7 @@ module Enums : S with type int_t = Z.t = struct
255255
let r' = BISet.reduce (fun i acc -> R.join (f i) acc) x in (* reduce is safe because arguments are not bot here *)
256256
Exc (BISet.empty (), r')
257257
| Exc (_, ((p1, p2) as p)), Exc (_, ((r1, r2) as r)) ->
258-
begin match Int.compare p1 0 >= 0, Int.compare r1 0 >= 0 with
258+
begin match p1 >= 0, r1 >= 0 with
259259
| true, true -> Exc (BISet.empty (), (0, Int.min p2 r2))
260260
| true, _ -> Exc (BISet.empty (), (0, p2))
261261
| _, true -> Exc (BISet.empty (), (0, r2))
@@ -292,15 +292,15 @@ module Enums : S with type int_t = Z.t = struct
292292
| Exc (_, (r1, r2)), Inc x ->
293293
let f i =
294294
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
295-
if Int.compare r1 0 >= 0 && Z.compare i Z.zero >= 0 then
295+
if r1 >= 0 && Z.compare i Z.zero >= 0 then
296296
(0, b)
297297
else
298298
(-b, b)
299299
in
300300
let r' = BISet.reduce (fun i acc -> R.join (f i) acc) x in (* reduce is safe because arguments are not bot here *)
301301
Exc (BISet.empty (), r')
302302
| Exc (_, (p1, p2)), Exc (_, (r1, r2)) ->
303-
if Int.compare p1 0 >= 0 && Int.compare r1 0 >= 0 then
303+
if p1 >= 0 && r1 >= 0 then
304304
Exc (BISet.empty (), (0, Int.max p2 r2))
305305
else (
306306
let b = List.fold_left Int.max 0 (List.map Int.abs [p1; p2; r1; r2]) in

0 commit comments

Comments
 (0)