From d69deaaa37e7474abb9d2b0792945bf16b0171b5 Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Fri, 30 Nov 2018 18:00:00 +0100
Subject: [PATCH] Julien's review no.2: useless singleton test
---
src/plugins/e-acsl/quantif.ml | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index ed4d7719e28..bb769665feb 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -115,10 +115,10 @@ let rec has_empty_quantif_with_false_negative = function
| (t1, rel1, _, rel2, t2) :: guards ->
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
- if Ival.is_singleton_int i1 && Ival.is_singleton_int i2 then
- (* we know the precise values of the bounds *)
- let lower_bound, _ = Misc.finite_min_and_max i1 in
- let upper_bound, _ = Misc.finite_min_and_max i2 in
+ let lower_bound, _ = Ival.min_and_max i1 in
+ let _, upper_bound = Ival.min_and_max i2 in
+ match lower_bound, upper_bound with
+ | Some lower_bound, Some upper_bound ->
let res = match rel1, rel2 with
| Rle, Rle -> lower_bound > upper_bound
| Rle, Rlt | Rlt, Rle -> lower_bound >= upper_bound
@@ -126,7 +126,7 @@ let rec has_empty_quantif_with_false_negative = function
| _ -> assert false
in
res (* case 1 *) || has_empty_quantif_with_false_negative guards
- else
+ | None, _ | _, None ->
has_empty_quantif_with_false_negative guards
let () = Typing.compute_quantif_guards_ref := compute_quantif_guards
--
GitLab