From 010fc9764b1b273ef04fe07f13c4f5e17596df9e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 23 Nov 2021 12:45:18 +0100
Subject: [PATCH] [wp] Fix code semantics float typing
---
src/plugins/wp/CodeSemantics.ml | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/CodeSemantics.ml b/src/plugins/wp/CodeSemantics.ml
index ce024d4c0f5..bc9e93bc1b1 100644
--- a/src/plugins/wp/CodeSemantics.ml
+++ b/src/plugins/wp/CodeSemantics.ml
@@ -82,8 +82,8 @@ struct
| Val e -> p_equal e e_zero
| Loc l -> M.is_null l
- let is_zero_float = function
- | Val e -> p_equal e e_zero_real
+ let is_zero_float ft = function
+ | Val e -> p_equal e @@ Cfloat.float_of_real ft e_zero_real
| Loc l -> M.is_null l
let is_zero_ptr v = M.is_null (cloc v)
@@ -91,7 +91,7 @@ struct
let rec is_zero sigma obj l =
match obj with
| C_int _ -> is_zero_int (M.load sigma obj l)
- | C_float _ -> is_zero_float (M.load sigma obj l)
+ | C_float ft -> is_zero_float ft (M.load sigma obj l)
| C_pointer _ -> is_zero_ptr (M.load sigma obj l)
| C_comp { cfields = None } ->
p_true (* cannot say anything interesting here *)
--
GitLab