diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index e5ea4748e6b3950a654a49ab29c868d7d79db2c9..2453bded6360dc01a4109b3724d32b37fb135586 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1018,6 +1018,7 @@ module RteGen = struct
   let get_pointerCall_status = mk_fun "RteGen.get_pointerCall_status"
   let get_unsignedOv_status = mk_fun "RteGen.get_unsignedOv_status"
   let get_unsignedDownCast_status = mk_fun "RteGen.get_unsignedDownCast_status"
+  let get_pointer_downcast_status = mk_fun "RteGen.get_pointer_downcast_status"
   let get_float_to_int_status = mk_fun "RteGen.get_float_to_int_status"
   let get_finite_float_status = mk_fun "RteGen.get_finite_float_status"
   let get_bool_value_status = mk_fun "RteGen.get_bool_value_status"
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 565c20806a04f78a636ff9dca8a062f9e6af3b87..a54ae74932d0942ba3df7aa1508675e0dda9c5a8 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -900,6 +900,7 @@ module RteGen : sig
   val get_signed_downCast_status : (unit -> status_accessor) ref
   val get_unsignedOv_status : (unit -> status_accessor) ref
   val get_unsignedDownCast_status : (unit -> status_accessor) ref
+  val get_pointer_downcast_status : (unit -> status_accessor) ref
   val get_float_to_int_status : (unit -> status_accessor) ref
   val get_finite_float_status : (unit -> status_accessor) ref
   val get_bool_value_status : (unit -> status_accessor) ref
diff --git a/src/plugins/rte/flags.ml b/src/plugins/rte/flags.ml
index 5a5efb9c60c333de0bf18346135e72ea20f3f04d..7d17b15a3a9577579b409c2396f89060023f48a8 100644
--- a/src/plugins/rte/flags.ml
+++ b/src/plugins/rte/flags.ml
@@ -36,6 +36,7 @@ type t = {
   unsigned_overflow: bool;
   signed_downcast: bool;
   unsigned_downcast: bool;
+  pointer_downcast: bool;
   float_to_int: bool;
   finite_float: bool;
   pointer_call: bool;
@@ -54,6 +55,7 @@ let all = {
   unsigned_overflow = true;
   signed_downcast = true;
   unsigned_downcast = true;
+  pointer_downcast = true;
   float_to_int = true;
   finite_float = true;
   pointer_call = true;
@@ -72,6 +74,7 @@ let none = {
   unsigned_overflow = false;
   signed_downcast = false;
   unsigned_downcast = false;
+  pointer_downcast = false;
   float_to_int = false;
   finite_float = false;
   pointer_call = false;
@@ -95,6 +98,7 @@ let default
     ?unsigned_overflow
     ?signed_downcast
     ?unsigned_downcast
+    ?pointer_downcast
     ?float_to_int
     ?finite_float
     ?pointer_call
@@ -112,6 +116,7 @@ let default
     unsigned_overflow = option Kernel.UnsignedOverflow.get unsigned_overflow ;
     signed_downcast = option Kernel.SignedDowncast.get signed_downcast ;
     unsigned_downcast = option Kernel.UnsignedDowncast.get unsigned_downcast ;
+    pointer_downcast = option Kernel.PointerDowncast.get pointer_downcast ;
     float_to_int = option Options.DoFloatToInt.get float_to_int ;
     finite_float = option (fun () -> Kernel.SpecialFloat.get () <> "none") finite_float ;
     pointer_call = option Options.DoPointerCall.get pointer_call ;
diff --git a/src/plugins/rte/flags.mli b/src/plugins/rte/flags.mli
index f90a63a3afa4e02c1b7bb15b94c0a68857ae633a..3ea19d53f367e367c1a0e414871403d5bef54d1b 100644
--- a/src/plugins/rte/flags.mli
+++ b/src/plugins/rte/flags.mli
@@ -38,6 +38,7 @@ type t = {
   unsigned_overflow: bool;
   signed_downcast: bool;
   unsigned_downcast: bool;
+  pointer_downcast: bool;
   float_to_int: bool;
   finite_float: bool;
   pointer_call: bool;
@@ -57,6 +58,7 @@ val default :
   ?unsigned_overflow:bool ->
   ?signed_downcast:bool ->
   ?unsigned_downcast:bool ->
+  ?pointer_downcast:bool ->
   ?float_to_int:bool ->
   ?finite_float:bool ->
   ?pointer_call:bool ->
diff --git a/src/plugins/rte/generator.ml b/src/plugins/rte/generator.ml
index 67214fae804fe5ab58da7821c3507b3f8aebb3cd..8c8e697d4dcf846db06cb7c6062fc9b5fd9847a1 100644
--- a/src/plugins/rte/generator.ml
+++ b/src/plugins/rte/generator.ml
@@ -155,6 +155,14 @@ module Unsigned_downcast =
       let additional_parameters = []
     end)
 
+module Pointer_downcast =
+  Make
+    (struct
+      let name = "pointer_downcast"
+      let parameter = Kernel.PointerDowncast.parameter
+      let additional_parameters = []
+    end)
+
 module Float_to_int =
   Make
     (struct
diff --git a/src/plugins/rte/generator.mli b/src/plugins/rte/generator.mli
index 1e1c61ccd3a87124d5ef785ef2ef72e73f23d123..1518a0acc67f22908320d834bb54b1f99c22eec4 100644
--- a/src/plugins/rte/generator.mli
+++ b/src/plugins/rte/generator.mli
@@ -39,6 +39,7 @@ module Signed_overflow: S
 module Signed_downcast: S
 module Unsigned_overflow: S
 module Unsigned_downcast: S
+module Pointer_downcast: S
 module Float_to_int: S
 module Finite_float: S
 module Bool_value: S
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index ed9296659abc8dc7463e90a2c1ec372b45cd1c8e..8b5afe27c054f83e273da685237efc10d5899d2d 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -93,6 +93,7 @@ let () =
   nojournal_register get_pointerCall_status Pointer_call.accessor;
   nojournal_register get_unsignedOv_status Unsigned_overflow.accessor;
   nojournal_register get_unsignedDownCast_status Unsigned_downcast.accessor;
+  nojournal_register get_pointer_downcast_status Pointer_downcast.accessor;
   nojournal_register get_float_to_int_status Float_to_int.accessor;
   nojournal_register get_finite_float_status Finite_float.accessor;
   nojournal_register get_bool_value_status Bool_value.accessor ;
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index 4d77766b988eea59d5549224cf79f63637d645c0..467d65f1ffd919d19c5ef4f4784c8cef98e9b490 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -372,7 +372,11 @@ let downcast_assertion ~remove_trivial ~on_alarm (dst_type, exp) =
       else Integer.zero, Cil.max_unsigned_number dst_size
     in
     let overflow_kind =
-      if dst_signed then Alarms.Signed_downcast else Alarms.Unsigned_downcast
+      if Cil.isPointerType src_type
+      then Alarms.Pointer_downcast
+      else if dst_signed
+      then Alarms.Signed_downcast
+      else Alarms.Unsigned_downcast
     in
     let alarm ?(invalid=false) bound bound_kind =
       let a = Alarms.Overflow (overflow_kind, exp, bound, bound_kind) in
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 4919cfdef8106b34ae4cc4b5ecefcb24009da2db..61dafe98471f4ed4f86338f62319019ef54b5c44 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -86,6 +86,10 @@ class annot_visitor kf flags on_alarm = object (self)
     flags.Flags.unsigned_downcast
     && not (Generator.Unsigned_downcast.is_computed kf)
 
+  method private do_pointer_downcast () =
+    flags.Flags.pointer_downcast
+    && not (Generator.Pointer_downcast.is_computed kf)
+
   method private do_float_to_int () =
     flags.Flags.float_to_int && not (Generator.Float_to_int.is_computed kf)
 
@@ -307,6 +311,9 @@ class annot_visitor kf flags on_alarm = object (self)
         | CastE (ty, e) ->
           (match Cil.unrollType ty, Cil.unrollType (Cil.typeOf e) with
            (* to , from *)
+           | TInt _, TPtr _ when self#do_pointer_downcast () ->
+             self#generate_assertion Rte.downcast_assertion (ty, e)
+
            | TInt(kind,_), TInt (_, _) ->
              let signed = Cil.isSigned kind in
              if signed && self#do_signed_downcast ()
@@ -453,6 +460,7 @@ let annotate ?flags kf =
        comp Signed_downcast.accessor flags.signed_downcast |||
        comp Unsigned_overflow.accessor flags.unsigned_overflow |||
        comp Unsigned_downcast.accessor flags.unsigned_downcast |||
+       comp Pointer_downcast.accessor flags.pointer_downcast |||
        comp Float_to_int.accessor flags.float_to_int |||
        comp Finite_float.accessor flags.finite_float |||
        comp Bool_value.accessor flags.bool_value
diff --git a/tests/rte/oracle/castoncall.0.res.oracle b/tests/rte/oracle/castoncall.0.res.oracle
index 430827699b37879782d59e6e4e9c4193b0079fc3..5bee127b54a1cdc4bc55cc45abba81fd07275144 100644
--- a/tests/rte/oracle/castoncall.0.res.oracle
+++ b/tests/rte/oracle/castoncall.0.res.oracle
@@ -16,6 +16,8 @@ void *nondet_ptr(void *a, void *b)
 {
   void *__retres;
   int tmp;
+  /*@ assert rte: pointer_downcast: (unsigned int)a ≤ 2147483647; */
+  /*@ assert rte: pointer_downcast: (unsigned int)b ≤ 2147483647; */
   tmp = nondet((int)a,(int)b);
   __retres = (void *)tmp;
   return __retres;
diff --git a/tests/rte/oracle/castoncall.1.res.oracle b/tests/rte/oracle/castoncall.1.res.oracle
index 430827699b37879782d59e6e4e9c4193b0079fc3..5bee127b54a1cdc4bc55cc45abba81fd07275144 100644
--- a/tests/rte/oracle/castoncall.1.res.oracle
+++ b/tests/rte/oracle/castoncall.1.res.oracle
@@ -16,6 +16,8 @@ void *nondet_ptr(void *a, void *b)
 {
   void *__retres;
   int tmp;
+  /*@ assert rte: pointer_downcast: (unsigned int)a ≤ 2147483647; */
+  /*@ assert rte: pointer_downcast: (unsigned int)b ≤ 2147483647; */
   tmp = nondet((int)a,(int)b);
   __retres = (void *)tmp;
   return __retres;
diff --git a/tests/rte/oracle/twofunc.res.oracle b/tests/rte/oracle/twofunc.res.oracle
index 58f6280ce2a0652e9d51261289831067a286bf40..5d0a80d5f3847f4511ec8b4104f59014643e42ae 100644
--- a/tests/rte/oracle/twofunc.res.oracle
+++ b/tests/rte/oracle/twofunc.res.oracle
@@ -133,6 +133,7 @@ int main(void)
 [kernel] - bool_value = true
 [kernel] - finite_float = true
 [kernel] - float_to_int = true
+[kernel] - pointer_downcast = true
 [kernel] - unsigned_downcast = false
 [kernel] - unsigned_overflow = false
 [kernel] - downcast = true
@@ -148,6 +149,7 @@ int main(void)
 [kernel] - bool_value = true
 [kernel] - finite_float = true
 [kernel] - float_to_int = true
+[kernel] - pointer_downcast = true
 [kernel] - unsigned_downcast = false
 [kernel] - unsigned_overflow = false
 [kernel] - downcast = true
@@ -225,6 +227,7 @@ int main(void)
 [kernel] - bool_value = true
 [kernel] - finite_float = true
 [kernel] - float_to_int = true
+[kernel] - pointer_downcast = true
 [kernel] - unsigned_downcast = false
 [kernel] - unsigned_overflow = false
 [kernel] - downcast = true
@@ -240,6 +243,7 @@ int main(void)
 [kernel] - bool_value = true
 [kernel] - finite_float = true
 [kernel] - float_to_int = true
+[kernel] - pointer_downcast = true
 [kernel] - unsigned_downcast = false
 [kernel] - unsigned_overflow = false
 [kernel] - downcast = true
diff --git a/tests/value/oracle/div.1.res.oracle b/tests/value/oracle/div.1.res.oracle
index 02145cd0576656b2032952be91796fdb578146cb..d052fa034e4dc04e49f23648ea6732c0ed0bd286 100644
--- a/tests/value/oracle/div.1.res.oracle
+++ b/tests/value/oracle/div.1.res.oracle
@@ -50,6 +50,8 @@
 [eva:alarm] tests/value/div.i:32: Warning: 
   assertion 'rte,division_by_zero' got status unknown.
 [eva:alarm] tests/value/div.i:32: Warning: division by zero. assert Z2 ≢ 0;
+[eva:alarm] tests/value/div.i:33: Warning: 
+  assertion 'rte,pointer_downcast' got status unknown.
 [eva:alarm] tests/value/div.i:33: Warning: 
   assertion 'rte,division_by_zero' got status unknown.
 [eva:alarm] tests/value/div.i:33: Warning: 
@@ -64,6 +66,8 @@
 [eva] tests/value/div.i:33: 
   Assigning imprecise value to b.
   The imprecision originates from Arithmetic {tests/value/div.i:33}
+[eva:alarm] tests/value/div.i:34: Warning: 
+  assertion 'rte,pointer_downcast' got status unknown.
 [eva:alarm] tests/value/div.i:34: Warning: 
   assertion 'rte,division_by_zero' got status unknown.
 [eva:alarm] tests/value/div.i:34: Warning: 
@@ -77,6 +81,8 @@
 [eva] tests/value/div.i:34: 
   Assigning imprecise value to d2.
   The imprecision originates from Arithmetic {tests/value/div.i:34}
+[eva:alarm] tests/value/div.i:35: Warning: 
+  assertion 'rte,pointer_downcast' got status unknown.
 [eva] tests/value/div.i:35: assertion 'rte,division_by_zero' got status valid.
 [eva:alarm] tests/value/div.i:35: Warning: 
   pointer downcast. assert (unsigned int)&X + 1 ≤ 2147483647;
@@ -87,6 +93,8 @@
 [eva] tests/value/div.i:35: 
   Assigning imprecise value to d1.
   The imprecision originates from Arithmetic {tests/value/div.i:35}
+[eva:alarm] tests/value/div.i:36: Warning: 
+  assertion 'rte,pointer_downcast' got status unknown.
 [eva] tests/value/div.i:36: assertion 'rte,division_by_zero' got status valid.
 [eva:alarm] tests/value/div.i:36: Warning: 
   pointer downcast. assert (unsigned int)&X ≤ 2147483647;
@@ -97,6 +105,8 @@
 [eva] tests/value/div.i:36: 
   Assigning imprecise value to d0.
   The imprecision originates from Arithmetic {tests/value/div.i:36}
+[eva:alarm] tests/value/div.i:37: Warning: 
+  assertion 'rte,pointer_downcast' got status unknown.
 [eva:alarm] tests/value/div.i:37: Warning: 
   assertion 'rte,signed_overflow' got status unknown.
 [eva:alarm] tests/value/div.i:37: Warning: