Merge branch 'feature/eva/invalid-pointer' into 'master'

[Eva] New alarms for the creation of invalid pointers

Closes #812 and #625

See merge request frama-c/frama-c!2555

share/libc/signal.h

@@ -46,9 +46,13 @@ typedef void (*__fc_sighandler_t) (int);
 /* for BSD 4.4 */
 typedef __fc_sighandler_t sig_t;
 
-#define SIG_DFL ((__fc_sighandler_t)0)     /* default signal handling */
-#define SIG_IGN ((__fc_sighandler_t)1)     /* ignore signal */
-#define SIG_ERR ((__fc_sighandler_t)-1)    /* error return from signal */
+extern void __fc_sig_dfl(int);
+extern void __fc_sig_ign(int);
+extern void __fc_sig_err(int);
+
+#define SIG_DFL (&__fc_sig_dfl)     /* default signal handling */
+#define SIG_IGN (&__fc_sig_ign)     /* ignore signal */
+#define SIG_ERR (&__fc_sig_err)     /* error return from signal */
 
 #define SIG_BLOCK 0
 #define SIG_UNBLOCK 1

src/kernel_internals/parsing/cparser.mly

@@ -226,11 +226,6 @@ let trd3 (_, _, result) = result
 
 let fourth4 (_,_,_,result) = result
 
-(*
-   transform:  __builtin_offsetof(type, member)
-   into     :  (size_t) (&(type * ) 0)->member
- *)
-
 let sizeofType () =
   let findSpecifier name =
     let convert_one_specifier s =
@@ -253,6 +248,11 @@ let sizeofType () =
   findSpecifier Cil.theMachine.Cil.theMachine.Cil_types.size_t
 
 
+(*
+   transform:  offsetof(type, member)
+   into     :  (size_t) (&(type * ) 0)->member
+ *)
+
 let transformOffsetOf (speclist, dtype) member =
   let mk_expr e = { expr_loc = member.expr_loc; expr_node = e } in
   let rec addPointer = function
@@ -280,7 +280,7 @@ let transformOffsetOf (speclist, dtype) member =
       | INDEX (base, index) ->
 	  INDEX (replaceBase base, index)
       | _ ->
-	Errorloc.parse_error "malformed offset expression in __builtin_offsetof"
+	Errorloc.parse_error "malformed offset expression in offsetof macro"
     in { e with expr_node = node }
   in
   let memberExpr = replaceBase member in
@@ -566,7 +566,14 @@ postfix_expression:                     /*(* 6.5.2 *)*/
                 { expr_loc = loc2; expr_node = TYPE_SIZEOF(b2,d2)}],[]))
       }
 | BUILTIN_OFFSETOF LPAREN type_name COMMA offsetof_member_designator RPAREN
-      { transformOffsetOf $3 $5 }
+    {
+      let loc_f = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 1, Parsing.rhs_end_pos 1) in
+      let arg = transformOffsetOf $3 $5 in
+      let builtin = { expr_loc = loc_f;
+                      expr_node = VARIABLE "__builtin_offsetof" }
+      in
+      make_expr (CALL (builtin, [ arg ], []))
+    }
 | postfix_expression DOT id_or_typename { make_expr (MEMBEROF ($1, $3))}
 | postfix_expression ARROW id_or_typename { make_expr (MEMBEROFPTR ($1, $3)) }
 | postfix_expression PLUS_PLUS { make_expr (UNARY (POSINCR, $1)) }

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;

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 { () }

src/kernel_internals/typing/cabs2cil.ml

@@ -7026,6 +7026,30 @@ and doExp local_env
                   Kernel.warning ~current:true
                     "Invalid call to builtin_constant_p")
              end
+           | "__builtin_offsetof" ->
+             begin
+               match !pargs with
+               | [{ enode = CastE (_, {enode = AddrOf (host, offset)}) } as e] ->
+                 begin
+                   piscall := false;
+                   prestype := Cil.theMachine.Cil.typeOfSizeOf;
+                   let typ = Cil.typeOfLhost host in
+                   try
+                     let start, _width = Cil.bitsOffset typ offset in
+                     if start mod 8 <> 0 then
+                       Kernel.error ~current:true "Using offset of bitfield";
+                     let kind = Cil.theMachine.kindOfSizeOf in
+                     pres := Cil.kinteger ~loc:e.eloc kind (start / 8);
+                   with SizeOfError _ ->
+                     pres := e;
+                     Kernel.error ~once:true ~current:true
+                       "Unable to compute offset %a in type %a"
+                       Cil_datatype.Offset.pretty offset
+                       Cil_datatype.Typ.pretty typ;
+                 end
+               | _ ->
+                 Kernel.abort ~current:true "Invalid call to builtin_offsetof"
+             end
            | "__builtin_types_compatible_p" ->
              begin
                (* Constant-fold the argument and see if it is a constant *)

src/kernel_services/abstract_interp/base.ml

@@ -306,7 +306,14 @@ let offset_for_validity ~bitfield access base =
 let valid_offset ?(bitfield=true) access base =
   if for_writing access && is_read_only base
   then Ival.bottom
-  else offset_for_validity ~bitfield access base
+  else
+    let offset = offset_for_validity ~bitfield access base in
+    (* When -absolute-valid-range is enabled, the Null base has a Known validity
+       that does not include 0. In this case, adds 0 as possible offset for a
+       pointer without memory access. *)
+    if access = No_access && is_null base
+    then Ival.(join zero offset)
+    else offset
 
 let offset_is_in_validity access base ival =
   let is_valid_for_bounds min_bound max_bound =
@@ -327,7 +334,8 @@ let offset_is_in_validity access base ival =
 let is_valid_offset access base offset =
   Ival.is_bottom offset
   || not (for_writing access && (is_read_only base))
-     && offset_is_in_validity access base offset
+     && (offset_is_in_validity access base offset
+         || access = No_access && is_null base && Ival.(equal zero offset))
 
 let is_function base =
   match base with

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 _

src/kernel_services/ast_data/alarms.ml

@@ -41,6 +41,7 @@ type alarm =
   | Index_out_of_bound of
       exp (* index *)
       * exp option (* None = lower bound is zero; Some up = upper bound *)
+  | Invalid_pointer of exp
   | Invalid_shift of exp * int option (* strict upper bound, if any *)
   | Pointer_comparison of
       exp option (* [None] when implicit comparison to 0 *)
@@ -67,7 +68,7 @@ type alarm =
 
 (* If you add one constructor to this type, make sure to add a dummy value
    in the 'reprs' value below, and increase 'nb_alarms' *)
-let nb_alarm_constructors = 17
+let nb_alarm_constructors = 18
 
 module D =
   Datatype.Make_with_collections
@@ -82,6 +83,7 @@ module D =
         [ Division_by_zero e;
           Memory_access (lv, For_reading);
           Index_out_of_bound (e, None);
+          Invalid_pointer e;
           Invalid_shift (e, None);
           Pointer_comparison (None, e);
           Differing_blocks (e, e);
@@ -102,20 +104,21 @@ module D =
         | Division_by_zero _ -> 0
         | Memory_access _ -> 1
         | Index_out_of_bound _ -> 2
-        | Invalid_shift _ -> 3
-        | Pointer_comparison _ -> 4
-        | Overflow _ -> 5
-        | Not_separated _ -> 6
-        | Overlap _ -> 7
-        | Uninitialized _ -> 8
-        | Is_nan_or_infinite _ -> 9
-        | Is_nan _ -> 10
-        | Float_to_int _ -> 11
-        | Differing_blocks _ -> 12
-        | Dangling _ -> 13
-        | Function_pointer _ -> 14
-        | Uninitialized_union _ -> 15
-        | Invalid_bool _ -> 16
+        | Invalid_pointer _ -> 3
+        | Invalid_shift _ -> 4
+        | Pointer_comparison _ -> 5
+        | Overflow _ -> 6
+        | Not_separated _ -> 7
+        | Overlap _ -> 8
+        | Uninitialized _ -> 9
+        | Is_nan_or_infinite _ -> 10
+        | Is_nan _ -> 11
+        | Float_to_int _ -> 12
+        | Differing_blocks _ -> 13
+        | Dangling _ -> 14
+        | Function_pointer _ -> 15
+        | Uninitialized_union _ -> 16
+        | Invalid_bool _ -> 17
 
       let () = (* Lightweight checks *)
         for i = 0 to nb_alarm_constructors - 1 do
@@ -136,6 +139,7 @@ module D =
         | Index_out_of_bound(e11, e12), Index_out_of_bound(e21, e22) ->
           let n = Exp.compare e11 e21 in
           if n = 0 then Extlib.opt_compare Exp.compare e12 e22 else n
+        | Invalid_pointer e1, Invalid_pointer e2 -> Exp.compare e1 e2
         | Invalid_shift(e1, n1), Invalid_shift(e2, n2) ->
           let n = Exp.compare e1 e2 in
           if n = 0 then Extlib.opt_compare Datatype.Int.compare n1 n2 else n
@@ -187,7 +191,8 @@ module D =
           else Extlib.opt_compare (Extlib.list_compare Exp.compare) l1 l2
         | Invalid_bool lv1, Invalid_bool lv2 -> Lval.compare lv1 lv2
         | _, (Division_by_zero _ | Memory_access _ |
-              Index_out_of_bound _ | Invalid_shift _ | Pointer_comparison _ |
+              Index_out_of_bound _ | Invalid_pointer _ |
+              Invalid_shift _ | Pointer_comparison _ |
               Overflow _ | Not_separated _ | Overlap _ | Uninitialized _ |
               Dangling _ | Is_nan_or_infinite _ | Is_nan _ | Float_to_int _ |
               Differing_blocks _ | Function_pointer _ |
@@ -211,6 +216,7 @@ module D =
             (nb a,
              Exp.hash e1,
              match e2 with None -> 0 | Some e -> 17 + Exp.hash e)
+        | Invalid_pointer e -> Hashtbl.hash (nb a, Exp.hash e)
         | Invalid_shift(e, n) -> Hashtbl.hash (nb a, Exp.hash e, n)
         | Pointer_comparison(e1, e2) ->
           Hashtbl.hash
@@ -255,6 +261,8 @@ module D =
             (match e2 with None -> ">=" | Some _ -> "<")
             Printer.pp_exp
             (match e2 with None -> Cil.zero e1.eloc | Some e -> e)
+        | Invalid_pointer e ->
+          Format.fprintf fmt "Invalid_pointer(@[%a@])" Exp.pretty e
         | Invalid_shift(e, n) ->
           Format.fprintf fmt "Invalid_shift(@[%a@]@ %s)"
             Printer.pp_exp e
@@ -393,6 +401,7 @@ let get_name = function
   | Division_by_zero _ -> "division_by_zero"
   | Memory_access _ -> "mem_access"
   | Index_out_of_bound _ -> "index_bound"
+  | Invalid_pointer _ -> "pointer_value"
   | Invalid_shift _ -> "shift"
   | Pointer_comparison _ -> "ptr_comparison"
   | Differing_blocks _ -> "differing_blocks"
@@ -416,6 +425,7 @@ let get_description = function
   | Division_by_zero _ -> "Integer division by zero"
   | Memory_access _ -> "Invalid pointer dereferencing"
   | Index_out_of_bound _ -> "Array access out of bounds"
+  | Invalid_pointer _ -> "Invalid pointer computation"
   | Invalid_shift _ -> "Invalid shift"
   | Pointer_comparison _ -> "Invalid pointer comparison"
   | Differing_blocks _ -> "Operation on pointers within different blocks"
@@ -503,6 +513,13 @@ let create_predicate ?(loc=Location.unknown) alarm =
          let t2 = Logic_utils.expr_to_term ~cast:true e2 in
          Logic_const.prel ~loc (Rlt, t1, t2))
 
+    | Invalid_pointer e ->
+      let loc = best_loc ~loc e.eloc in
+      let t = Logic_utils.expr_to_term ~cast:true e in
+      if Cil.isFunPtrType (Cil.typeOf e)
+      then Logic_const.pvalid_function ~loc t
+      else Logic_const.pobject_pointer ~loc (Logic_const.here_label, t)
+
     | Invalid_shift(e, n) ->
       (* 0 <= e < n *)
       let loc = best_loc ~loc e.eloc in

src/kernel_services/ast_data/alarms.mli

@@ -40,6 +40,7 @@ type alarm =
   | Index_out_of_bound of
       exp (** index *)
       * exp option (** None = lower bound is zero; Some up = upper bound *)
+  | Invalid_pointer of exp
   | Invalid_shift of exp * int option (** strict upper bound, if any *)
   | Pointer_comparison of
       exp option (** [None] when implicit comparison to NULL pointer *)

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

src/kernel_services/ast_printing/cil_printer.ml

@@ -54,6 +54,20 @@ module Extensions = struct
 end
 let set_extension_handler = Extensions.set_handler
 
+(* for specific builtin functions that act as placeholder for C macros.
+   For each name f below, pretty-printer will replace f and &f with the
+   corresponding name. Be sure to keep the list in sync with share/libc.
+*)
+let rename_builtins = Datatype.String.Hashtbl.create 17
+
+let () =
+  List.iter (fun (x,y) -> Datatype.String.Hashtbl.add rename_builtins x y)
+    [
+      "__fc_sig_dfl", "SIG_DFL";
+      "__fc_sig_ign", "SIG_IGN";
+      "__fc_sig_err", "SIG_ERR";
+    ]
+
 (* Deprecated functions *)
 let set_deprecated_extension_handler = Extensions.set_deprecated_handler
 
@@ -231,6 +245,7 @@ module Precedence = struct
     | Pfreeable _
     | Pvalid _
     | Pvalid_read _
+    | Pobject_pointer _
     | Pvalid_function _
     | Pinitialized _
     | Pdangling _
@@ -641,7 +656,15 @@ class cil_printer () = object (self)
     | CEnum {einame = s} -> self#varname fmt s
 
   (*** VARIABLES ***)
-  method varname fmt v = pp_print_string fmt v
+  method varname fmt v =
+    let v =
+      if not state.print_cil_as_is &&
+         Datatype.String.Hashtbl.mem rename_builtins v
+      then
+        Datatype.String.Hashtbl.find rename_builtins v
+      else v
+    in
+    pp_print_string fmt v
 
   (* variable use *)
   method varinfo fmt v =
@@ -762,6 +785,9 @@ class cil_printer () = object (self)
        Neither cookie nor keyword for you. *)
     | AlignOf t -> fprintf fmt "__alignof__(%a)" (self#typ None) t
     | AlignOfE e -> fprintf fmt "__alignof__(%a)" self#exp_non_decay e
+    | AddrOf ((Var v, NoOffset))
+      when Datatype.String.Hashtbl.mem rename_builtins v.vname ->
+      self#varinfo fmt v
     | AddrOf lv -> fprintf fmt "& %a" (self#lval_prec Precedence.addrOfLevel) lv
     | StartOf(lv) ->
       if state.print_cil_as_is || non_decay then
@@ -1046,6 +1072,23 @@ class cil_printer () = object (self)
         "__builtin_types_compatible_p: cabs2cil should have added sizeof to \
          the arguments."
 
+    | Call(dest, {enode = Lval (Var vi, NoOffset)}, [ arg ], (l, _))
+      when vi.vname = "__builtin_offsetof"
+        && not state.print_cil_as_is ->
+      begin
+        match arg.enode with
+        | CastE (_, { enode = AddrOf (host, offset) }) ->
+          (* Print the destination *)
+          Extlib.may (fprintf fmt "%a = " self#lval) dest;
+          (* Now the call itself *)
+          fprintf fmt "%a(%a, %a)%s"
+            self#varname "offsetof"
+            (self#typ None) (Cil.typeOfLhost host)
+            self#offset offset
+            instr_terminator
+        | _ -> Kernel.fatal ~source:l "__builtin_offsetof: invalid argument."
+      end
+
     | Call(dest,e,args,_) -> pp_call dest e fmt args
 
     | Asm(attrs, tmpls, ext_asm, l) ->
@@ -2727,6 +2770,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"

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) ->

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) ->

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
@@ -4505,19 +4509,6 @@ and constFold (machdep: bool) (e: exp) : exp =
   | AlignOfE _ | AlignOf _ | SizeOfStr _ | SizeOfE _ | SizeOf _ ->
     e (* Depends on machdep. Do not evaluate in this case*)
 
-  (* Special case to handle the C macro 'offsetof' *)
-  | CastE(it,
-          { enode = AddrOf (Mem ({enode = CastE(TPtr(bt, _), z)}), off)})
-    when machdep && isZero z -> begin
-      try
-        let start, _width = bitsOffset bt off in
-        if start mod 8 <> 0 then
-          Kernel.error ~current:true "Using offset of bitfield" ;
-        constFold machdep
-          (new_exp ~loc (CastE(it, (integer ~loc (start / 8)))))
-      with SizeOfError _ -> e
-    end
-
   | CastE (t, e) -> begin
       Kernel.debug ~dkey "ConstFold CAST to %a@." !pp_typ_ref t ;
       let e = constFold machdep e in
@@ -5208,13 +5199,20 @@ let initVABuiltins () =
 let initMsvcBuiltins () : unit =
   (** Take a number of wide string literals *)
   Builtin_functions.add "__annotation" (voidType, [ ], true)
-;;
+
+let init_common_builtins () =
+  add_builtin
+    "offsetof"
+    theMachine.typeOfSizeOf
+    [ theMachine.typeOfSizeOf ]
+    false
 
 let init_builtins () =
   if not (TheMachine.is_computed ()) then
     Kernel.fatal ~current:true "You must call initCIL before init_builtins" ;
   if Builtin_functions.length () <> 0 then
     Kernel.fatal ~current:true "Cil builtins already initialized." ;
+  init_common_builtins ();
   if msvcMode () then
     initMsvcBuiltins ()
   else begin
@@ -6945,7 +6943,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 ->

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 *)

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
 

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

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