From b8009dc5422e34a9ceb04d03377988eb7f75703e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 30 Mar 2021 09:23:08 +0200
Subject: [PATCH] [Eva] Fixes a crash in the automatic loop unrolling.
---
src/kernel_services/abstract_interp/int_set.ml | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 00a4e0fe4bd..333d647b333 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -575,10 +575,10 @@ let complement_under ~min ~max set =
end
done;
let b, e = Int.succ (get (!index-1)), Int.pred (get !index) in
- let card = Int.(to_int (succ (sub e b))) in
- if card <= 0 then `Bottom
- else if card <= !small_cardinal
- then `Set (Array.init card (fun i -> Int.add b (Int.of_int i)))
+ let card = Int.succ (Int.sub e b) in
+ if Int.(le card zero) then `Bottom
+ else if Int.le card (Int.of_int !small_cardinal)
+ then `Set (Array.init (Int.to_int card) (fun i -> Int.add b (Int.of_int i)))
else `Top (b, e, Int.one)
(* ------------------------------ Arithmetics ------------------------------- *)
--
GitLab