diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index cccda3a9169be72d7c7d2202aec9827b2b477ada..9df39736f7c0606adcfe6412e725f8a75669fae7 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 9c0399ad475d798fd4f968f5fae4bf5175b29eb7..0c95ee14a2c78bdc8ccf69d66875628a261e63c9 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 bc130617463ae326596dafb96a28133d71449c03..06e4720e294a3e4c737f3c4adce2f988dbe72670 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