From dd397fefdc95db055d6b8f79aede7392273ad09b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 9 Jun 2021 20:38:41 +0200
Subject: [PATCH] [Eva] Fixes a crash in the octagon domain.
---
src/plugins/value/domains/octagons.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index e45b1c875de..e39c64ae86f 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -349,7 +349,7 @@ module Rewriting = struct
let min_bound = Eval_typ.range_lower_bound range in
let ival_range = Ival.inject_range (Some min_bound) (Some max_bound) in
let aux has_better_bound bound bound_kind alarms =
- if has_better_bound ival ival_range >= 0
+ if Ival.is_bottom ival || has_better_bound ival ival_range >= 0
then
let alarm = Alarms.Overflow (overflow, expr, bound, bound_kind) in
Alarmset.set alarm Alarmset.True alarms
--
GitLab