diff --git a/src/plugins/wp/MemAddr.ml b/src/plugins/wp/MemAddr.ml
index 3ade44f81ba66bb3f5b0f05fd7bf0309a87ffe0e..9a687ca5e9d4b00964ec4cb92b8df556225cb393 100644
--- a/src/plugins/wp/MemAddr.ml
+++ b/src/plugins/wp/MemAddr.ml
@@ -49,13 +49,12 @@ let p_addr_lt = Lang.extern_p ~library ~bool:"addr_lt_bool" ~prop:"addr_lt" ()
 let p_addr_le = Lang.extern_p ~library ~bool:"addr_le_bool" ~prop:"addr_le" ()
 
 let f_addr_of_int = Lang.extern_f
-    ~category:Qed.Logic.Injection
     ~library ~result:t_addr "addr_of_int"
 
 let f_int_of_addr = Lang.extern_f
-    ~category:Qed.Logic.Injection
     ~library ~result:Qed.Logic.Int "int_of_addr"
 
+let p_statically_allocated = Lang.extern_fp ~library "statically_allocated"
 
 let f_table_of_base = Lang.extern_f ~library
     ~category:Qed.Logic.Function ~result:t_table "table_of_base"
@@ -110,6 +109,15 @@ let invalid alloc addr size = p_call p_invalid [ alloc ; addr ; size ]
 let addr_of_int i = e_fun f_addr_of_int [ i ]
 let int_of_addr addr = e_fun f_int_of_addr [ addr ]
 
+let statically_allocated addr = p_call p_statically_allocated [ addr ]
+(* This last function is not exposed, it does not have a particular meaning in
+   ACSL, and is used only for int/addr conversions.
+*)
+
+let in_uintptr_range addr =
+  p_hyps [ statically_allocated @@ base addr ] @@
+  Cint.range (Ctypes.c_ptr ()) @@ int_of_addr addr
+
 (* Table of offsets *)
 
 let base_offset base offset =
diff --git a/src/plugins/wp/MemAddr.mli b/src/plugins/wp/MemAddr.mli
index 1b97aa438030a65e67c78b57361bfb5cbf94dc20..8bfc3a3fbb0e7958c2b8ae0b6357743728e87aa5 100644
--- a/src/plugins/wp/MemAddr.mli
+++ b/src/plugins/wp/MemAddr.mli
@@ -68,6 +68,17 @@ val int_of_addr : term -> term
     Abstract: Conversion from address to integer
 *)
 
+val in_uintptr_range : term -> pred
+(** [in_uintptr_range (a: addr)] =
+    [statically_allocated(a.base) -> in_range(int_of_addr a)]
+
+    Assuming that the base of a statically exists, the conversion of the pointer
+    to a an integer produces a value that fits in [uintptr_t].
+
+    @since Frama-C+dev
+*)
+
+
 val base_offset : term -> term -> term
 (** [base_offset(base: int)(offset: int) : int]
     Converts a {i logic} offset (which is actually the address of a memory cell