From 8e18736eaaf3cbeff5ab8a450745580503ea4e95 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 24 Apr 2019 22:28:45 +0200
Subject: [PATCH] [Eva] Eval_term: interprets logic coercions between integer
and boolean types.
---
src/plugins/value/legacy/eval_terms.ml | 14 ++++++++++----
1 file changed, 10 insertions(+), 4 deletions(-)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index ec743004289..c60e4d58b85 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -899,7 +899,8 @@ let rec eval_term ~alarm_mode env t =
nothing to do, AND coercion from an integer type to a floating-point
type, that require a conversion. *)
(match Logic_const.plain_or_set Extlib.id ltyp with
- | Linteger when Logic_typing.is_integral_type t.term_type -> r
+ | Linteger when Logic_typing.is_integral_type t.term_type
+ || Logic_const.is_boolean_type t.term_type -> r
| Ctype typ when Cil.isIntegralOrPointerType typ -> r
| Lreal ->
if Logic_typing.is_integral_type t.term_type
@@ -915,9 +916,14 @@ let rec eval_term ~alarm_mode env t =
ldeps = r.ldeps;
eunder = under_from_over eover;
eover; }
- | _ -> unsupported
- (Format.asprintf "logic coercion %a -> %a@."
- Printer.pp_logic_type t.term_type Printer.pp_logic_type ltyp)
+ | _ ->
+ if Logic_const.is_boolean_type ltyp
+ && Logic_typing.is_integral_type t.term_type
+ then cast_to_bool r
+ else
+ unsupported
+ (Format.asprintf "logic coercion %a -> %a@."
+ Printer.pp_logic_type t.term_type Printer.pp_logic_type ltyp)
)
(* TODO: the meaning of the label in \offset and \base_addr is not obvious
--
GitLab