Make top_ptr function remember current node

src/analyses/base.ml

@@ -310,7 +310,7 @@ struct
         let n = ID.neg (ID.cast_to (Cilfacade.ptrdiff_ikind ()) n) in
         Address (AD.map (addToAddr n) p)
       | Mod -> Int (ID.top_of (Cilfacade.ptrdiff_ikind ())) (* we assume that address is actually casted to int first*)
-      | _ -> Address AD.top_ptr
+      | _ -> Address (AD.top_ptr ())
     in
     (* The main function! *)
     match a1,a2 with
@@ -2302,8 +2302,8 @@ struct
             | Address a -> a
             (* TODO: don't we already have logic for this? *)
             | Int i when ID.to_int i = Some BI.zero -> AD.null_ptr
-            | Int i -> AD.top_ptr
-            | _ -> AD.top_ptr (* TODO: why does this ever happen? *)
+            | Int i -> AD.top_ptr ()
+            | _ -> AD.top_ptr () (* TODO: why does this ever happen? *)
           in
           let p_addr' = AD.remove NullPtr p_addr in (* realloc with NULL is same as malloc, remove to avoid unknown value from NullPtr access *)
           let p_addr_get = get ask gs st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *)

src/cdomains/addressDomain.ml

@@ -264,9 +264,7 @@ struct
   let null_ptr       = singleton Addr.NullPtr
   let unknown_ptr    = singleton (Addr.UnknownPtr {node = None})
   let not_null       = unknown_ptr
-  let top_ptr        = of_list Addr.[UnknownPtr {node = None}; NullPtr]
-
-  let top_ptr_n n    = of_list Addr.[UnknownPtr {node = n}; NullPtr]
+  let top_ptr ()     = of_list Addr.[UnknownPtr {node = !Node.current_node}; NullPtr]
 
   let is_element a x = cardinal x = 1 && Addr.equal (choose x) a
   let is_null x = is_element Addr.NullPtr x
@@ -284,7 +282,7 @@ struct
     | x when GobOption.exists BigIntOps.(equal (one)) x -> not_null
     | _ -> match ID.to_excl_list i with
       | Some (xs, _) when List.exists BigIntOps.(equal (zero)) xs -> not_null
-      | _ -> top_ptr
+      | _ -> top_ptr ()
 
   let to_int x =
     let ik = Cilfacade.ptr_ikind () in
@@ -339,7 +337,7 @@ struct
 
     (* if any of the input address sets contains an element that isn't a StrPtr, return top *)
     if List.mem None haystack' || List.mem None needle' then
-      top_ptr
+      top_ptr ()
     else
       (* else try to find the first occurrence of all strings in needle' in all strings s of haystack',
          collect s starting from that occurrence or if there is none, collect a NULL pointer,
@@ -423,7 +421,7 @@ struct
   *)
 
   let is_top = may_be_unknown
-  let top () = top_ptr
+  let top () = top_ptr ()
 
   let merge uop cop x y =
     let no_null x y =

src/cdomains/addressDomain_intf.ml

@@ -120,10 +120,7 @@ sig
     val not_null: t
     (** Address set containing the unknown pointer, which is non-[NULL]. *)
 
-    val top_ptr: t
-    (** Address set containing any pointer, [NULL] or not. *)
-
-    val top_ptr_n: Node.t option -> t
+    val top_ptr: unit -> t
     (** Address set containing any pointer, [NULL] or not. *)
 
     val is_null: t -> bool

src/cdomains/valueDomain.ml

@@ -175,7 +175,7 @@ struct
     | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.top ())
     | TInt (ik,_) -> Int (ID.top_of ik)
     | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.top_of fkind)
-    | TPtr _ -> Address AD.top_ptr
+    | TPtr _ -> Address (AD.top_ptr ())
     | TComp ({cstruct=true; _} as ci,_) -> Struct (Structs.create (fun fd -> init_value ~varAttr:fd.fattr fd.ftype) ci)
     | TComp ({cstruct=false; _},_) -> Union (Unions.top ())
     | TArray (ai, length, _) ->
@@ -194,7 +194,7 @@ struct
     | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.top ())
     | TInt (ik,_) -> Int (ID.(cast_to ik (top_of ik)))
     | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.top_of fkind)
-    | TPtr _ -> Address AD.top_ptr
+    | TPtr _ -> Address (AD.top_ptr ())
     | TComp ({cstruct=true; _} as ci,_) -> Struct (Structs.create (fun fd -> top_value ~varAttr:fd.fattr fd.ftype) ci)
     | TComp ({cstruct=false; _},_) -> Union (Unions.top ())
     | TArray (ai, length, _) ->
@@ -454,11 +454,11 @@ struct
         | TPtr (t,_) ->
           Address (match v with
               | Int x when ID.to_int x = Some BI.zero -> AD.null_ptr
-              | Int x -> AD.top_ptr
+              | Int x -> AD.top_ptr ()
               (* we ignore casts to void*! TODO report UB! *)
               | Address x -> (match t with TVoid _ -> x | _ -> cast_addr t x)
               (*| Address x -> x*)
-              | _ -> log_top __POS__; AD.top_ptr
+              | _ -> log_top __POS__; AD.top_ptr ()
             )
         | TArray (ta, l, _) -> (* TODO, why is the length exp option? *)
           (* TODO handle casts between different sizes? *)
@@ -542,7 +542,7 @@ struct
     | (Address y, Int x) -> Address (match ID.to_int x with
         | Some x when BI.equal x BI.zero -> AD.join AD.null_ptr y
         | Some x -> AD.(join y not_null)
-        | None -> AD.join y AD.top_ptr)
+        | None -> AD.join y (AD.top_ptr ()))
     | (Address x, Address y) -> Address (AD.join x y)
     | (Struct x, Struct y) -> Struct (Structs.join x y)
     | (Union x, Union y) -> Union (Unions.join x y)
@@ -577,7 +577,7 @@ struct
     | (Address y, Int x) -> Address (match ID.to_int x with
         | Some x when BI.equal x BI.zero -> AD.widen AD.null_ptr (AD.join AD.null_ptr y)
         | Some x -> AD.(widen y (join y not_null))
-        | None -> AD.widen y (AD.join y AD.top_ptr))
+        | None -> AD.widen y (AD.join y (AD.top_ptr ())))
     | (Address x, Address y) -> Address (AD.widen x y)
     | (Struct x, Struct y) -> Struct (Structs.widen x y)
     | (Union x, Union y) -> Union (Unions.widen x y)
@@ -697,7 +697,7 @@ struct
     in
     let array_idx_top = (None, ArrIdxDomain.top ()) in
     match typ, state with
-    |                 _ , Address n    -> Address (AD.join AD.top_ptr n)
+    |                 _ , Address n    -> Address (AD.join (AD.top_ptr ()) n)
     | TComp (ci,_)  , Struct n     -> Struct (invalid_struct ci n)
     |                 _ , Struct n     -> Struct (Structs.map (fun x -> invalidate_value ask voidType x) n)
     | TComp (ci,_)  , Union (`Lifted fd,n) -> Union (`Lifted fd, invalidate_value ask fd.ftype n)