diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index eb9fe4321f830b2fdbd8cff5674454582dc2c5c5..bc63b51001c4f167093838eece20330d6eeab414 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -232,6 +232,7 @@
         "\\typeof", TYPEOF;
         "\\unallocated", UNALLOCATED;
         "\\union", BSUNION;
+        "\\object_pointer", OBJECT_POINTER;
         "\\valid", VALID;
         "\\valid_read", VALID_READ;
         "\\valid_index", VALID_INDEX;
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index b19f7e478bd77f9e680841b0e5403008695b9a50..9c25360b415d9900542d993ef3d7bbae21e36639 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -243,7 +243,8 @@
 %token INT INTEGER REAL BOOLEAN BOOL FLOAT LT GT LE GE EQ NE COMMA ARROW EQUAL
 %token FORALL EXISTS IFF IMPLIES AND OR NOT SEPARATED
 %token TRUE FALSE OLD AT RESULT
-%token BLOCK_LENGTH BASE_ADDR OFFSET VALID VALID_READ VALID_INDEX VALID_RANGE VALID_FUNCTION
+%token BLOCK_LENGTH BASE_ADDR OFFSET VALID VALID_READ VALID_INDEX VALID_RANGE
+%token OBJECT_POINTER VALID_FUNCTION
 %token ALLOCATION STATIC REGISTER AUTOMATIC DYNAMIC UNALLOCATED
 %token ALLOCABLE FREEABLE FRESH
 %token DOLLAR QUESTION MINUS PLUS STAR AMP SLASH PERCENT LSQUARE RSQUARE EOF
@@ -456,6 +457,7 @@ lexpr_inner:
 | NOT lexpr_inner { info (PLnot $2) }
 | TRUE { info PLtrue }
 | FALSE { info PLfalse }
+| OBJECT_POINTER opt_label_1 LPAR lexpr RPAR { info (PLobject_pointer ($2,$4)) }
 | VALID opt_label_1 LPAR lexpr RPAR { info (PLvalid ($2,$4)) }
 | VALID_READ opt_label_1 LPAR lexpr RPAR { info (PLvalid_read ($2,$4)) }
 | VALID_FUNCTION LPAR lexpr RPAR { info (PLvalid_function $3) }
@@ -1932,6 +1934,7 @@ bs_keyword:
 | TYPEOF { () }
 | BSUNION { () }
 | UNALLOCATED { () }
+| OBJECT_POINTER { () }
 | VALID { () }
 | VALID_INDEX { () }
 | VALID_RANGE { () }
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index 427467329aaa3554457c9b8da2b33502abc7b176..99fd4b2c8a73673792b1a5a65a350c05e0668827 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -800,7 +800,7 @@ to function contracts."
              taken into account by the functions [from_...] below *)
           DoChildren
 
-      | Pvalid_function _ ->
+      | Pobject_pointer _ | Pvalid_function _ ->
           DoChildren
 
       | Papp _ | Pallocable _ | Pfreeable _ | Pfresh _
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 49d3a0fecd3cf710b0bb07a85c27eb5c2ef59877..66327ce7d8cb982cc58b7b00ff61571c72ef2f77 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1569,6 +1569,8 @@ and predicate_node =
   | Pexists of quantifiers * predicate (** existential quantification. *)
   | Pat of predicate * logic_label
   (** predicate refers to a particular program point. *)
+  | Pobject_pointer of logic_label * term
+  (** the given locations can be pointed to. *)
   | Pvalid_read of logic_label * term   (** the given locations are valid for reading. *)
   | Pvalid of logic_label * term   (** the given locations are valid. *)
   | Pvalid_function of term
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 2b8c620ea6b01e18ec5c712bce14e2b39c4ee70f..aef5019984374c17ebe290473bdad37498ef234e 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -231,6 +231,7 @@ module Precedence = struct
     | Pfreeable _
     | Pvalid _
     | Pvalid_read _
+    | Pobject_pointer _
     | Pvalid_function _
     | Pinitialized _
     | Pdangling _
@@ -2727,6 +2728,10 @@ class cil_printer () = object (self)
       fprintf fmt "@[%a%a(@[%a@])@]"
         self#pp_acsl_keyword "\\valid_read"
         self#labels [l] self#term p
+    | Pobject_pointer (l,p) ->
+      fprintf fmt "@[%a%a(@[%a@])@]"
+        self#pp_acsl_keyword "\\object_pointer"
+        self#labels [l] self#term p
     | Pvalid_function p ->
       fprintf fmt "@[%a(@[%a@])@]"
         self#pp_acsl_keyword "\\valid_function"
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index c059f8110e4fc104336981b6bc0ffd4f4a933eb8..0b4be0a9ac93ec2a8d93fb8a07047eaf2ff7a62e 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -859,6 +859,8 @@ and pp_predicate_node fmt = function
     Format.fprintf fmt "Pexists(%a,%a)"  pp_quantifiers quantifiers  pp_predicate predicate
   | Pat(predicate,logic_label) ->
     Format.fprintf fmt "Pat(%a,%a)"  pp_predicate predicate  pp_logic_label logic_label
+  | Pobject_pointer(logic_label,term) ->
+    Format.fprintf fmt "Pobject_pointer(%a,%a)"  pp_logic_label logic_label  pp_term term
   | Pvalid_read(logic_label,term) ->
     Format.fprintf fmt "Pvalid_read(%a,%a)"  pp_logic_label logic_label  pp_term term
   | Pvalid(logic_label,term) ->
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 998b809f10ec17a8aa0a2aaaebbf8c4a97e95a62..fca0da4953174ea419fd0fe96a21a520e7a80f18 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -129,7 +129,7 @@ let getParenthLevel e =
   | PLapp _ | PLold _ | PLat _
   | PLoffset _ | PLbase_addr _ | PLblock_length _
   | PLupdate _  | PLinitField _ | PLinitIndex _
-  | PLvalid _ | PLvalid_read _ | PLvalid_function _
+  | PLvalid _ | PLvalid_read _ | PLobject_pointer _ | PLvalid_function _
   | PLinitialized _ | PLdangling _
   | PLallocable _ | PLfreeable _ | PLfresh _
   | PLseparated _ | PLunion _ | PLinter _ -> 10
@@ -249,8 +249,12 @@ and print_lexpr_level n fmt e =
     | PLexists(q,e) ->
       fprintf fmt "@[\\exists@ @[%a@];@ %a@]"
         print_quantifiers q print_lexpr e
-    | PLvalid (l,e) -> fprintf fmt "\\valid%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
-    | PLvalid_read (l,e) -> fprintf fmt "\\valid_read%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
+    | PLvalid (l,e) ->
+      fprintf fmt "\\valid%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
+    | PLvalid_read (l,e) ->
+      fprintf fmt "\\valid_read%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
+    | PLobject_pointer (l,e) ->
+      fprintf fmt "\\object_pointer%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
     | PLvalid_function e ->
       fprintf fmt "\\valid_function(@;@[%a@]@;)" print_lexpr_plain e
     | PLinitialized (l,e) ->
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 572e350a44a50bffba9a3b6e407e6c3027cefc39..459570e1be633a25dff4695a87a15ca68b8d94fe 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1868,6 +1868,10 @@ and childrenPredicateNode vis p =
     let s' = visitCilLogicLabel vis s in
     let t' = vTerm t in
     if t' != t || s != s' then Pvalid_read (s',t') else p
+  | Pobject_pointer (s,t) ->
+    let s' = visitCilLogicLabel vis s in
+    let t' = vTerm t in
+    if t' != t || s != s' then Pobject_pointer (s',t') else p
   | Pvalid_function t ->
     let t' = vTerm t in
     if t' != t then Pvalid_function t' else p
@@ -6945,7 +6949,7 @@ and free_vars_predicate bound_vars p = match p.pred_content with
          Logic_var.Set.union (free_vars_term bound_vars t) acc)
       Logic_var.Set.empty tl
   | Pallocable (_,t) | Pfreeable (_,t)
-  | Pvalid (_,t) | Pvalid_read (_,t) | Pvalid_function t
+  | Pvalid (_,t) | Pvalid_read (_,t) | Pobject_pointer (_, t) | Pvalid_function t
   | Pinitialized (_,t) | Pdangling (_,t) ->
     free_vars_term bound_vars t
   | Pseparated seps ->
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index e9417dd0256ab638e8fe3f476d30be8edbac6c0f..8ee64b0b36651d60f18a87251d73e9db53d5a161 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -425,6 +425,7 @@ let pallocable ?(loc=Cil_datatype.Location.unknown) (l,p) = unamed ~loc (Palloca
 let pfreeable ?(loc=Cil_datatype.Location.unknown) (l,p) = unamed ~loc (Pfreeable (l,p))
 let pvalid ?(loc=Cil_datatype.Location.unknown) (l,p) = unamed ~loc (Pvalid (l,p))
 let pvalid_read ?(loc=Cil_datatype.Location.unknown) (l,p) = unamed ~loc (Pvalid_read (l,p))
+let pobject_pointer ?(loc=Cil_datatype.Location.unknown) (l,p) = unamed ~loc (Pobject_pointer (l,p))
 let pvalid_function ?(loc=Cil_datatype.Location.unknown) p = unamed ~loc (Pvalid_function p)
 
 (* the index should be an integer or a range of integers *)
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 280661c522f5e0027260323c72bf8ba1eb32da41..51759d05c132490f56e7b7a7644677cc944c9fac 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -170,6 +170,9 @@ val pvalid_read: ?loc:location -> logic_label * term -> predicate
 (** \valid *)
 val pvalid: ?loc:location -> logic_label * term -> predicate
 
+(** \object_pointer *)
+val pobject_pointer: ?loc:location -> logic_label * term -> predicate
+
 (** \valid_function *)
 val pvalid_function: ?loc:location -> term -> predicate
 
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 9cab004b334e452e6f82d6ec6a4785fb998c179a..f6a1c015fb927e32d3da67b28201a434314b48f7 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1049,7 +1049,8 @@ struct
       | Pimplies(p1,p2) | Piff(p1,p2) -> needs_at_pred p1 || needs_at_pred p2
       | Pnot p | Plet (_,p) | Pforall(_,p) | Pexists(_,p) -> needs_at_pred p
       | Pif(t,p1,p2) -> needs_at t || needs_at_pred p1 || needs_at_pred p2
-      | Pvalid (_,t) | Pvalid_read (_,t) | Pvalid_function t
+      | Pvalid (_,t) | Pvalid_read (_,t)
+      | Pobject_pointer (_,t) | Pvalid_function t
       | Pinitialized (_,t) | Pdangling (_, t)
       | Pallocable(_,t) | Pfreeable(_,t)-> needs_at t
       | Pfresh (_,_,t,n) -> (needs_at t) && (needs_at n)
@@ -3003,7 +3004,7 @@ struct
       let t2,ty2 = type_num_term_option ctxt env t2 in
       (Trange(t1,t2),
        Ltype(ctxt.find_logic_type "set", [arithmetic_conversion ty1 ty2]))
-    | PLvalid _ | PLvalid_read _ | PLvalid_function _
+    | PLvalid _ | PLvalid_read _ | PLobject_pointer _ | PLvalid_function _
     | PLfresh _ | PLallocable _ | PLfreeable _
     | PLinitialized _ | PLdangling _ | PLexists _ | PLforall _
     | PLimplies _ | PLiff _
@@ -3357,6 +3358,8 @@ struct
       predicate_label_ptr ~check_non_void:true pvalid_read l t
     | PLvalid (l,t) ->
       predicate_label_ptr ~check_non_void:true pvalid l t
+    | PLobject_pointer (l,t) ->
+      predicate_label_ptr ~check_non_void:false pobject_pointer l t
     | PLvalid_function t ->
       let t = term env t in
       if isLogicPointer t then begin
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 41237fee5871725c0547b3203b220c9d155189ef..ea652d98361c8868f61b4ba6454c76db096fbb98 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -935,6 +935,7 @@ and is_same_predicate_node p1 p2 =
   | Pfreeable (l1,t1), Pfreeable (l2,t2)
   | Pvalid (l1,t1), Pvalid (l2,t2)
   | Pvalid_read (l1,t1), Pvalid_read (l2,t2)
+  | Pobject_pointer (l1,t1), Pobject_pointer (l2,t2)
   | Pinitialized (l1,t1), Pinitialized (l2,t2) ->
     is_same_logic_label l1 l2 && is_same_term t1 t2
   | Pvalid_function t1, Pvalid_function t2 ->
@@ -949,7 +950,7 @@ and is_same_predicate_node p1 p2 =
      with Invalid_argument _ -> false)
   | (Pfalse | Ptrue | Papp _ | Prel _ | Pand _ | Por _ | Pimplies _
     | Piff _ | Pnot _ | Pif _ | Plet _ | Pforall _ | Pexists _
-    | Pat _ | Pvalid _ | Pvalid_read _ | Pvalid_function _
+    | Pat _ | Pvalid _ | Pvalid_read _ | Pobject_pointer _ | Pvalid_function _
     | Pinitialized _ | Pdangling _
     | Pfresh _ | Pallocable _ | Pfreeable _ | Pxor _ | Pseparated _
     ), _ -> false
@@ -1288,6 +1289,7 @@ and is_same_lexpr l1 l2 =
   | PLfreeable (l1,e1), PLfreeable (l2,e2)
   | PLvalid (l1,e1), PLvalid (l2,e2)
   | PLvalid_read (l1,e1), PLvalid_read (l2,e2)
+  | PLobject_pointer (l1,e1), PLobject_pointer (l2,e2)
   | PLbase_addr (l1,e1), PLbase_addr (l2,e2)
   | PLoffset (l1,e1), PLoffset (l2,e2)
   | PLblock_length (l1,e1), PLblock_length (l2,e2)
@@ -1316,7 +1318,8 @@ and is_same_lexpr l1 l2 =
     | PLupdate _ | PLinitIndex _ | PLtype _ | PLfalse
     | PLtrue | PLinitField _ | PLrel _ | PLand _ | PLor _ | PLxor _
     | PLimplies _ | PLiff _ | PLnot _ | PLif _ | PLforall _
-    | PLexists _ | PLvalid _ | PLvalid_read _ | PLvalid_function _
+    | PLexists _ | PLvalid _ | PLvalid_read _
+    | PLobject_pointer _ | PLvalid_function _
     | PLfreeable _ | PLallocable _
     | PLinitialized _ | PLdangling _ | PLseparated _ | PLfresh _ | PLnamed _
     | PLcomprehension _ | PLunion _ | PLinter _
@@ -1523,6 +1526,8 @@ and hash_predicate (acc,depth,tot) p =
       hash_predicate (acc + 173 + hash_label l, depth - 1, tot - 1) p
     | Pvalid_read (l, t) ->
       hash_term (acc + 187 + hash_label l, depth - 1, tot - 1) t
+    | Pobject_pointer (l, t) ->
+      hash_term (acc + 181 + hash_label l, depth - 1, tot - 1) t
     | Pvalid (l, t) ->
       hash_term (acc + 193 + hash_label l, depth - 1, tot - 1) t
     | Pvalid_function t -> hash_term (acc + 203, depth - 1, tot - 1) t
@@ -1823,6 +1828,7 @@ and compare_predicate_node p1 p2 =
   | Pfreeable (l1,t1), Pfreeable (l2,t2)
   | Pvalid (l1,t1), Pvalid (l2,t2)
   | Pvalid_read (l1,t1), Pvalid_read (l2,t2)
+  | Pobject_pointer (l1,t1), Pobject_pointer (l2,t2)
   | Pinitialized (l1,t1), Pinitialized (l2,t2)
   | Pdangling (l1,t1), Pdangling (l2,t2) ->
     let res = compare_logic_label l1 l2 in
@@ -1835,6 +1841,8 @@ and compare_predicate_node p1 p2 =
   | _, Pvalid _ -> -1
   | Pvalid_read _, _ -> 1
   | _, Pvalid_read _ -> -1
+  | Pobject_pointer _, _ -> 1
+  | _, Pobject_pointer _ -> -1
   | Pinitialized _, _ -> 1
   | _, Pinitialized _ -> -1
   | Pdangling _, _ -> 1
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index 30364e00fa181dc989a779455f5a49f82e3d2077..adde2634144cb07084ca310b5ea944ea7ed119c8 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -132,6 +132,7 @@ and lexpr_node =
                                 expression. *)
   | PLvalid of string option * lexpr (** pointer is valid. *)
   | PLvalid_read of string option * lexpr (** pointer is valid for reading. *)
+  | PLobject_pointer of string option * lexpr (** object pointer can be created. *)
   | PLvalid_function of lexpr (** function pointer is compatible with pointed type. *)
   | PLallocable of string option * lexpr (** pointer is valid for malloc. *)
   | PLfreeable of string option * lexpr (** pointer is valid for free. *)
diff --git a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
index 36e0eab772110d3428c89c680e387ca5058b62b8..3b655683995066f05739e1669e5e359c33ed4ddd 100644
--- a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
@@ -359,7 +359,8 @@ module rec Transfer
   let register_object kf state_ref = object
     inherit Visitor.frama_c_inplace
     method !vpredicate_node = function
-    | Pvalid(_, t) | Pvalid_read(_, t) | Pvalid_function t
+    | Pvalid(_, t) | Pvalid_read(_, t)
+    | Pobject_pointer(_, t) | Pvalid_function t
     | Pinitialized(_, t) | Pfreeable(_, t) ->
       (*	Options.feedback "REGISTER %a" Cil.d_term t;*)
       state_ref := register_term kf !state_ref t;
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 91904e682a942c36581cfb89f4b3401d385c524f..075d6bfa4a714d0da483b492d5c9d7b83d86f6c0 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -676,6 +676,7 @@ let rec type_predicate p =
     | Pallocable(_, t)
     | Pvalid(_, t)
     | Pvalid_read(_, t)
+    | Pobject_pointer(_,t)
     | Pvalid_function t ->
       ignore (type_term ~use_gmp_opt:false ~ctx:Nan t);
       c_int
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index e3d5580ba81fbc0c585be56ad3ecfe12e29ca38a..6a77b6530dfb5e6fd13a9a96e9878c3b5d48c6c9 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -708,6 +708,7 @@ and named_predicate_content_to_exp ?name kf env p =
     e, env
   | Pseparated _ -> not_yet env "\\separated"
   | Pdangling _ -> not_yet env "\\dangling"
+  | Pobject_pointer _ -> not_yet env "\\object_pointer"
   | Pvalid_function _ -> not_yet env "\\valid_function"
   | Prel(rel, t1, t2) ->
     let ity = Typing.get_integer_op_of_predicate p in
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index cb9450bce91d295514451eb251dd97f45eb31443..968ec99416cd4f3ae03a543e14c9fc1d4603b9e3 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -2144,6 +2144,7 @@ let rec reduce_by_predicate ~alarm_mode env positive p =
     | _,Pvalid_read (_label,tsets) ->
       reduce_by_valid env positive Read tsets
 
+    | _,Pobject_pointer (_label, _tsets) -> env (* TODO *)
     | _,Pvalid_function _tsets -> env (* TODO *)
 
     | _,(Pinitialized (lbl_initialized,tsets)
@@ -2291,6 +2292,8 @@ and eval_predicate env pred =
       ignore (env_state env lbl);
       do_eval { env with e_cur = lbl } p
 
+    | Pobject_pointer (_label, _tsets) -> Unknown (* TODO *)
+
     | Pvalid (_label, tsets) | Pvalid_read (_label, tsets) ->
       (* TODO: see same constructor in reduce_by_predicate *)
       let kind = match p.pred_content with Pvalid_read _ -> Read | _ -> Write in
@@ -2579,7 +2582,8 @@ let predicate_deps env pred =
     | Pat (p, lbl) ->
       do_eval { env with e_cur = lbl } p
 
-    | Pvalid (_, tsets) | Pvalid_read (_, tsets) | Pvalid_function tsets->
+    | Pvalid (_, tsets) | Pvalid_read (_, tsets)
+    | Pobject_pointer (_, tsets) | Pvalid_function tsets ->
       (eval_term_as_lval ~alarm_mode env tsets).ldeps
 
     | Pinitialized (lbl, tsets) | Pdangling (lbl, tsets) ->
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index d513d5172bab625d546e835a6ded6be9867d9cde..825ace458d1358d5db7fc9ec043ce37e8c8e6a04 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -872,6 +872,11 @@ struct
     | Pvalid(label,t) -> valid env RW label t
     | Pvalid_read(label,t) -> valid env RD label t
 
+    | Pobject_pointer(_label,_t) ->
+        Warning.error
+          "\\object_pointer not yet implemented@\n\
+           @[<hov 0>(%a)@]" Printer.pp_predicate p
+
     | Pvalid_function _t ->
         Warning.error
           "\\valid_function not yet implemented@\n\
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 1841ce516fbf2b39c668bc9b45845a86eadefe35..642686f82636b7213cdff0c9538c43e0c5696971 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -535,7 +535,8 @@ and pred (env:ctx) p : value = match p.pred_content with
   (* No escape *)
   | Pinitialized(_, t) | Pdangling(_,t)
   | Pallocable(_, t) | Pfreeable(_, t)
-  | Pvalid(_,t) | Pvalid_read (_,t) | Pvalid_function t ->
+  | Pvalid(_,t) | Pvalid_read (_,t)
+  | Pobject_pointer (_,t) | Pvalid_function t ->
       unescape ((term env) t)
   | Pseparated ts ->
       E.fcup (fun t -> unescape ((term env) t)) ts
diff --git a/src/plugins/wp/RegionAccess.ml b/src/plugins/wp/RegionAccess.ml
index 642f9c3fd9ba218a4dfca7a1715bdb5f9b6c11a9..4f87b246b7ffffc2baf728bcb7136919ce7bf22b 100644
--- a/src/plugins/wp/RegionAccess.ml
+++ b/src/plugins/wp/RegionAccess.ml
@@ -369,7 +369,7 @@ and cc_pred (map:map) (p:predicate) =
   | Pforall(_,p) | Pexists(_,p) -> cc_pred map p
 
   | Pseparated ts -> List.iter (cc_term map) ts
-  | Pvalid(_,t) | Pvalid_read(_,t) | Pvalid_function t
+  | Pvalid(_,t) | Pvalid_read(_,t) | Pobject_pointer(_,t) | Pvalid_function t
   | Pinitialized(_,t) | Pdangling(_,t) | Pallocable(_,t)
   | Pfreeable(_,t) -> cc_term map t
   | Pfresh(_,_,ptr,n) -> cc_term map ptr ; cc_term map n