From 60ac16850b7ecdfd7954b58fe78864704af421b4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 19 Dec 2018 10:52:09 +0100
Subject: [PATCH] [Ival] More precise bitwise operators on unbounded ivals.
---
src/kernel_services/abstract_interp/ival.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 391bc645b63..60c93219ceb 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -2908,7 +2908,8 @@ struct
match result_size v1 v2 ~s1 ~s2 () with
| None ->
(* Unbounded result *)
- None
+ if lower && s = Off then Some Int.zero
+ else if not lower && s = On then Some Int.minus_one else None
| Some n ->
(* The result is bounded: iterate from the rightmost significant bit *)
let rec step r v1 v2 i =
--
GitLab