diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml
index 629040d5995a1e5fb7d60d8ff15876f72c3aea2d..03c45e5023eafe2b3c686eb96f98e92a1898786f 100644
--- a/src/kernel_internals/typing/logic_builtin.ml
+++ b/src/kernel_internals/typing/logic_builtin.ml
@@ -118,6 +118,7 @@ let init =
           (fun c -> Logic_env.add_builtin_logic_ctor c.ctor_name c) ctors ;
         list.lt_def <- Some (LTsum ctors);
         let _list_of_integer = Ltype (list, [Linteger]) in
+        let l_label = FormalLabel "L" in
         (* predicates *)
         List.iter
           (fun (f,tparams,labels,params)  ->
@@ -154,14 +155,14 @@ let init =
             "\\no_overflow_double", [], [], ["m", rounding_mode; "x", Lreal] ;
             "\\subset", [a_name], [], ["s1", set_of_a_type;
                                        "s2", set_of_a_type];
-            "\\pointer_comparable", [], [], [("p1", object_ptr);
-                                             ("p2", object_ptr)];
-            "\\pointer_comparable", [], [], [("p1", fun_ptr);
-                                             ("p2", fun_ptr)];
-            "\\pointer_comparable", [], [], [("p1", fun_ptr);
-                                             ("p2", object_ptr)];
-            "\\pointer_comparable", [], [], [("p1", object_ptr);
-                                             ("p2", fun_ptr)];
+            "\\pointer_comparable", [], [l_label], [("p1", object_ptr);
+                                                    ("p2", object_ptr)];
+            "\\pointer_comparable", [], [l_label], [("p1", fun_ptr);
+                                                    ("p2", fun_ptr)];
+            "\\pointer_comparable", [], [l_label], [("p1", fun_ptr);
+                                                    ("p2", object_ptr)];
+            "\\pointer_comparable", [], [l_label], [("p1", object_ptr);
+                                                    ("p2", fun_ptr)];
           ];
         (* functions *)
         List.iter
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 0af75114af3d582931d53b4b77dd12730b333c34..02ed9f21ad4de808044cb71e01f3e2b245cc1888 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -2362,7 +2362,7 @@ class complete_types =
 
 let complete_types f = Cil.visitCilFile (new complete_types) f
 
-let pointer_comparable ?loc t1 t2 =
+let pointer_comparable ?loc ?(label=Logic_const.here_label) t1 t2 =
   let preds = Logic_env.find_all_logic_functions "\\pointer_comparable" in
   let cfct_ptr = TPtr (TFun(Cil.voidType,None,false,[]),[]) in
   let fct_ptr = Ctype cfct_ptr in
@@ -2404,7 +2404,7 @@ let pointer_comparable ?loc t1 t2 =
     with Not_found ->
       Kernel.fatal "built-in predicate \\pointer_comparable not found"
   in
-  Logic_const.unamed ?loc (Papp (pi, [], [t1;t2]))
+  Logic_const.unamed ?loc (Papp (pi, [label], [t1;t2]))
 
 let is_min_max_function name li =
   li.l_var_info.lv_name = name &&
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 1e94484c56da83f416155892b65fd691c73a0069..251133446185ff75f6d1c82ceeea63619540ba1b 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -146,9 +146,12 @@ val numeric_coerce: logic_type -> term -> term
 (** \valid_range *)
 (* val mk_pvalid_range: ?loc:location -> term * term * term -> predicate *)
 
-val pointer_comparable: ?loc:location -> term -> term -> predicate
-(** \pointer_comparable
-    @since Fluorine-20130401 *)
+val pointer_comparable:
+  ?loc:location -> ?label:logic_label -> term -> term -> predicate
+(** \pointer_comparable. [label] defaults to {!Logic_const.here_label}
+    @since Fluorine-20130401
+    @before Frama-C+dev no [label] argument, as the builtin did not take a label
+*)
 
 (** {2 Conversion from exp to term} *)