diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 045236f50856988505304ba646d240e06a8243ae..742b5c26528ecaa01b59f948db601f221c025f8c 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3304,6 +3304,18 @@ let isIntegralOrPointerType t =
   | TInt _ | TEnum _ | TPtr _ -> true
   | _ -> false
 
+(* Don't completely unroll here, as we do not want to identify
+   intptr_t with its supporting integer type. *)
+let rec is_intptr_t = function
+  | TNamed(t,_) ->
+    t.tname = "intptr_t" || is_intptr_t t.ttype
+  | _ -> false
+
+let rec is_uintptr_t = function
+  | TNamed (t,_) ->
+    t.tname = "uintptr_t" || is_uintptr_t t.ttype
+  | _ -> false
+
 let rec isLogicBooleanType t =
   match t with
   | Ctype ty -> isIntegralType ty
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index dd36accd6a0acfd37d7bb16c61bc41b5cc36539e..5f654d34907b9cb1a67fc42e9a3c3b182b34a9bf 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -416,6 +416,16 @@ val isIntegralType: typ -> bool
 *)
 val isBoolType: typ -> bool
 
+(** True if the argument is [intptr_t] (but _not_ its underlying integer type)
+    @since Frama-C+dev
+*)
+val is_intptr_t: typ -> bool
+
+(** True if the argument is [uintptr_t] (but _not_ its underlying integer type)
+    @since Frama-C+dev
+*)
+val is_uintptr_t: typ -> bool
+
 (** True if the argument is [_Bool] or [boolean].
     @since 19.0-Potassium
 *)
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index e64f4ee5f0be842a8f2531ebb9a1e59d6b255d45..06c1daa44ce5840a433e7793feb222aa697d56a2 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -169,11 +169,6 @@ let rec signed_counterpart typ =
   | TPtr _ -> signed_counterpart ((Machine.uintptr_type ()))
   | _ -> assert false
 
-let rec is_intptr_type = function
-  | TNamed ({torig_name = name} as t, _) ->
-    name = "intptr_t" || name = "uintptr_t" || is_intptr_type t.ttype
-  | _ -> false
-
 let return t = `Value t, Alarmset.none
 
 (* Intersects [alarms] with the only possible alarms from the dereference of
@@ -797,7 +792,11 @@ module Make
       let& value =
         match src_type, dst_type with
         | TSPtr src, TSInt dst ->
-          let alarm = if is_intptr_type dst_typ then NoAlarm else PtrDowncast in
+          let alarm =
+            if Cil.is_intptr_t dst_typ || Cil.is_uintptr_t dst_typ
+            then NoAlarm
+            else PtrDowncast
+          in
           cast_int_to_int context ~alarm ~src ~dst expr value
         | TSInt src, (TSInt dst | TSPtr dst) ->
           cast_int_to_int context ~alarm:IntDowncast ~src ~dst expr value
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index b4d94c63bb7bc72fa1b209888a2e87cc58b7da98..b5be2f5975cc336e795b8cf523b2584f2db96b62 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -330,10 +330,6 @@ let shift_overflow_assertion ~signed ~remove_trivial ~on_alarm (exp, op, lexp, r
     end
     else overflow_alarm ()
 
-let rec is_intptr_t = function
-  | Cil_types.TNamed(t,_) -> t.tname = "intptr_t" || is_intptr_t t.ttype
-  | _ -> false
-
 (* Assertion for downcasts. *)
 let downcast_assertion ~remove_trivial ~on_alarm (dst_type, exp) =
   let src_type = Cil.typeOf exp in
@@ -342,7 +338,8 @@ let downcast_assertion ~remove_trivial ~on_alarm (dst_type, exp) =
   let src_size = Cil.bitsSizeOf src_type in
   let dst_size = Cil.bitsSizeOfBitfield dst_type in
   if (dst_size < src_size || dst_size == src_size && dst_signed <> src_signed)
-  && not (Cil.isPointerType src_type && is_intptr_t dst_type)
+  && not (Cil.isPointerType src_type &&
+          (Cil.is_intptr_t dst_type || Cil.is_uintptr_t dst_type))
   then
     let dst_min, dst_max =
       if dst_signed