From ea6292535e5478a0a2c6be93eba985b99d1ed868 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 10 Jan 2020 14:51:11 +0100
Subject: [PATCH] [Eva] Emits pointer downcasts alarms according to option
-warn-pointer-downcast.
---
src/plugins/value/engine/evaluation.ml | 31 +++++++++++++++-----------
1 file changed, 18 insertions(+), 13 deletions(-)
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 43eb4404fe6..ab391eb3546 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -665,7 +665,7 @@ module Make
in
cast_integer Alarms.Signed_downcast expr ~src ~dst value
- let cast_int_to_int expr ~src ~dst value =
+ let cast_int_to_int expr ~ptr ~src ~dst value =
(* Regain some precision in case a transfer function was imprecise.
This should probably be done in the transfer function, though. *)
let value =
@@ -675,16 +675,19 @@ module Make
in
if Eval_typ.range_inclusion src dst
then return value (* Upcast, nothing to check. *)
- else if dst.i_signed then (* Signed downcast. *)
- if Kernel.SignedDowncast.get ()
- then cast_integer Alarms.Signed_downcast expr ~src ~dst value
- else if Value_parameters.WarnSignedConvertedDowncast.get ()
+ else
+ let overflow_kind, warn =
+ if ptr
+ then Alarms.Pointer_downcast, Kernel.PointerDowncast.get
+ else if dst.i_signed
+ then Alarms.Signed_downcast, Kernel.SignedDowncast.get
+ else Alarms.Unsigned_downcast, Kernel.UnsignedDowncast.get
+ in
+ if warn ()
+ then cast_integer overflow_kind expr ~src ~dst value
+ else if dst.i_signed && Value_parameters.WarnSignedConvertedDowncast.get ()
then relaxed_signed_downcast expr ~src ~dst value
else return (Value.rewrap_integer dst value)
- else (* Unsigned downcast. *)
- if Kernel.UnsignedDowncast.get ()
- then cast_integer Alarms.Unsigned_downcast expr ~src ~dst value
- else return (Value.rewrap_integer dst value)
(* Re-export type here *)
type scalar_typ = Eval_typ.scalar_typ =
@@ -728,15 +731,17 @@ module Make
| Some src_type, Some dst_type ->
let value, alarms =
match src_type, dst_type with
- | (TSInt src | TSPtr src), (TSInt dst | TSPtr dst) ->
- cast_int_to_int ~src ~dst expr value
+ | TSPtr src, TSInt dst ->
+ cast_int_to_int ~ptr:true ~src ~dst expr value
+ | TSInt src, (TSInt dst | TSPtr dst) ->
+ cast_int_to_int ~ptr:false ~src ~dst expr value
| TSFloat src, (TSInt dst | TSPtr dst) ->
restrict_float ~reduce:true ~assume_finite:true expr src value >>=
truncate_float src dst expr
| (TSInt _ | TSPtr _), TSFloat _ ->
(* Cannot overflow with 32 bits float. *)
- `Value value, Alarmset.none
- | TSFloat _, TSFloat _ -> `Value value, Alarmset.none
+ return value
+ | TSFloat _, TSFloat _ | TSPtr _, TSPtr _ -> return value
in
value >>- Value.forward_cast ~src_type ~dst_type, alarms
--
GitLab