diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index ae9503e76ad6f3103eb254f1c1ef9ada04b085c8..445efc3204dc7df33fb762f7d61bf317f854ec4e 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -23,7 +23,8 @@
 open Cil_types
 open Cil_datatype
 
-type overflow_kind = Signed | Unsigned | Signed_downcast | Unsigned_downcast
+type overflow_kind =
+    Signed | Unsigned | Signed_downcast | Unsigned_downcast | Pointer_downcast
 type access_kind = For_reading | For_writing
 type bound_kind = Lower_bound | Upper_bound
 
@@ -32,6 +33,7 @@ let string_of_overflow_kind = function
   | Unsigned -> "unsigned_overflow"
   | Signed_downcast -> "signed_downcast"
   | Unsigned_downcast -> "unsigned_downcast"
+  | Pointer_downcast -> "pointer_downcast"
 
 type alarm =
   | Division_by_zero of exp
@@ -549,6 +551,10 @@ let create_predicate ?(loc=Location.unknown) alarm =
       (* n <= e or e <= n according to bound *)
       let loc = best_loc ~loc e.eloc in
       let t = match kind with
+        | Pointer_downcast ->
+          let t = Logic_utils.expr_to_term ~cast:true e in
+          let typ = Cil.theMachine.upointType in
+          Logic_const.tlogic_coerce ~loc t (Ctype typ)
         | Signed_downcast | Unsigned_downcast ->
           Logic_utils.expr_to_term ~cast:true e
         | _ ->
diff --git a/src/kernel_services/ast_data/alarms.mli b/src/kernel_services/ast_data/alarms.mli
index c301b2e797c6de7ed2675f805bfb997c7edecf29..a369dc60f2b76309b0ac2fed63a1474550724a4d 100644
--- a/src/kernel_services/ast_data/alarms.mli
+++ b/src/kernel_services/ast_data/alarms.mli
@@ -25,9 +25,10 @@
 
 open Cil_types
 
-(** Only signed overflows int are really RTEs. The other kinds may be
-    meaningful nevertheless. *)
-type overflow_kind = Signed | Unsigned | Signed_downcast | Unsigned_downcast
+(** Only signed overflows and pointer downcasts are really RTEs.
+    The other kinds may be meaningful nevertheless. *)
+type overflow_kind =
+    Signed | Unsigned | Signed_downcast | Unsigned_downcast | Pointer_downcast
 
 type access_kind = For_reading | For_writing
 type bound_kind = Lower_bound | Upper_bound
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index fa27012f076cd1e98586412b941bcc6c1c9411b8..1738ac4a35a476f78bd46f46e5816d3361d7ef16 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -309,6 +309,7 @@ let emit_alarm kinstr alarm (status:status) =
       | Alarms.Unsigned -> "unsigned overflow"
       | Alarms.Signed_downcast -> "signed downcast"
       | Alarms.Unsigned_downcast -> "unsigned downcast"
+      | Alarms.Pointer_downcast -> "pointer downcast"
     in
     register_alarm str