From 77f80af0af3d8aee4057679157085e0b6d93bf8b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 4 Nov 2019 14:23:47 +0100
Subject: [PATCH] [Eva] Fixes the octagon domain with respect to the ival
rewriting.
---
src/plugins/value/domains/octagons.ml | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 48734821cf4..c5a14838419 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -99,7 +99,7 @@ module Arith = struct
let widen =
let hints = Integer.zero,
- (Ival.Widen_Hints.default_widen_hints,
+ (Ival.Widen_Hints.empty,
Fc_float.Widen_Hints.default_widen_hints)
in
Ival.widen hints
@@ -109,9 +109,10 @@ module Arith = struct
if Ival.(equal top ival) then Fval.top
else project_float ival
- let neg = function
- | Float f -> inject_float (Fval.neg f)
- | ival -> neg_int ival
+ let neg ival =
+ if Ival.is_int ival
+ then neg_int ival
+ else inject_float (Fval.neg (project_float ival))
let int_or_float_operation i_op f_op = fun typ ->
match Cil.unrollType typ with
--
GitLab