From 840640e0c7f81f016397a375dcf42f9500ae91af Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 18 Sep 2019 15:55:17 +0200
Subject: [PATCH] [Ival] In int_val, fixes [min_max_rem_modu] on singletons.

---
 src/kernel_services/abstract_interp/int_val.ml  | 17 ++++++++---------
 src/kernel_services/abstract_interp/int_val.mli |  3 +--
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index 1b36c133b57..60c1c969c40 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -190,16 +190,15 @@ let inject_set_or_top_or_bottom = function
 (* Computes [min], [max], [rem] and [modu] from an integer set. *)
 let make_top_from_set s =
   let min = Int_set.min s in
-  let modu =
-    Int_set.fold
-      (fun x acc ->
-         if Int.equal x min
-         then acc
-         else Int.pgcd (Int.sub x min) acc)
-      s
-      Int.zero
+  let rem, modu =
+    if Int_set.cardinal s = 1
+    then Int.zero, min
+    else
+      let modu =
+        Int_set.fold (fun x acc -> Int.pgcd (Int.sub x min) acc) s Int.zero
+      in
+      Int.e_rem min modu, modu
   in
-  let rem = Int.e_rem min modu in
   let max = Some (Int_set.max s) in
   let min = Some min in
   min, max, rem, modu
diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli
index 69160f90d05..2f760b0c025 100644
--- a/src/kernel_services/abstract_interp/int_val.mli
+++ b/src/kernel_services/abstract_interp/int_val.mli
@@ -86,8 +86,7 @@ val max_int: t -> Integer.t option
 val min_and_max: t -> Integer.t option * Integer.t option
 
 (** Returns [min, max, rem, modu] such that for all integers [i] represented by
-    the given abstraction, [i] satisfies min ≤ i ≤ max and i ≅ rem [modu].
-    The abstraction must not be a singleton. *)
+    the given abstraction, [i] satisfies min ≤ i ≤ max and i ≅ rem [modu]. *)
 val min_max_rem_modu:
   t -> Integer.t option * Integer.t option * Integer.t * Integer.t
 
-- 
GitLab