From 99c44caaef5fc816ee397bb1d543dba5858fab5c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 22 Feb 2019 14:17:50 +0100
Subject: [PATCH] [Kernel] Warns when converting a pointer into an integer
without an explicit cast.
Adds the new warning category "typing:int-conversion".
---
src/kernel_internals/typing/cabs2cil.ml | 10 ++++++++--
src/kernel_services/plugin_entry_points/kernel.ml | 3 +++
src/kernel_services/plugin_entry_points/kernel.mli | 2 ++
3 files changed, 13 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index cccda3a9169..9df39736f7c 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2737,7 +2737,6 @@ let rec castTo ?(fromsource=false)
(* Taking numerical address or calling an absolute location. Also
accepted by gcc albeit with a warning. *)
| TInt _, TPtr (TFun _, _) -> result
- | TPtr (TFun _, _), TInt _ -> result
(* pointer to potential function type. Note that we do not
use unrollTypeDeep above in order to avoid needless divergence with
@@ -2770,7 +2769,14 @@ let rec castTo ?(fromsource=false)
| TInt _, TPtr _ -> result
- | TPtr _, TInt _ -> result
+ | TPtr _, TInt _ ->
+ if not fromsource
+ then
+ Kernel.warning
+ ~wkey:Kernel.wkey_int_conversion
+ ~current:true
+ "Conversion from a pointer to an integer without an explicit cast";
+ result
| TArray _, TPtr _ -> result
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 9c0399ad475..0c95ee14a2c 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -145,6 +145,9 @@ let wkey_incompatible_types_call =
let wkey_incompatible_pointer_types =
register_warn_category "typing:incompatible-pointer-types"
+let wkey_int_conversion =
+ register_warn_category "typing:int-conversion"
+
let wkey_cert_exp_46 = register_warn_category "CERT:EXP:46"
let wkey_cert_msc_38 = register_warn_category "CERT:MSC:38"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index bc130617463..06e4720e294 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -138,6 +138,8 @@ val wkey_incompatible_types_call: warn_category
val wkey_incompatible_pointer_types: warn_category
+val wkey_int_conversion: warn_category
+
val wkey_cert_exp_46: warn_category
val wkey_cert_msc_38: warn_category
--
GitLab