Add get_unknownptrs and has_unknownptr and use remove_unknownptrs ins…

…tead of remove

src/analyses/base.ml

@@ -1325,10 +1325,11 @@ struct
         | Bot -> Queries.Result.bot q (* TODO: remove *)
         | Address a ->
           let a' = AD.remove_unknownptrs a in (* run reachable_vars without unknown just to be safe: TODO why? *)
+          let u = AD.get_unknownptrs a in
           let addrs = reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local in
           let addrs' = List.fold_left (AD.join) (AD.empty ()) addrs in
           if AD.may_be_unknown a then
-            AD.add UnknownPtr addrs' (* add unknown back *)
+            AD.union u addrs' (* add unknowns back *)
           else
             addrs'
         | Int i ->

src/analyses/condVars.ml

@@ -65,9 +65,9 @@ struct
 
   let mayPointTo ctx exp =
     let ad = ctx.ask (Queries.MayPointTo exp) in
-    let a' = if Queries.AD.mem UnknownPtr ad then (
+    let a' = if Queries.AD.has_unknownptr ad then (
         M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
-        Queries.AD.remove UnknownPtr ad
+        Queries.AD.remove_unknownptrs ad
       ) else ad
     in
     List.filter_map (function

src/analyses/extractPthread.ml

@@ -878,7 +878,7 @@ module Spec : Analyses.MCPSpec = struct
   module ExprEval = struct
     let eval_ptr ctx exp =
       ctx.ask (Queries.MayPointTo exp)
-      |> Queries.AD.remove UnknownPtr (* UNSOUND *)
+      |> Queries.AD.remove_unknownptrs (* UNSOUND *)
       |> Queries.AD.to_var_may
 
     let eval_var ctx exp =

src/cdomains/addressDomain.ml

@@ -469,6 +469,18 @@ struct
       | UnknownPtr _ -> false
       | _ -> true
     ) ad
+
+  let get_unknownptrs ad = filter (function
+      | UnknownPtr _ -> true
+      | _ -> false
+    ) ad
+
+  let has_unknownptr ad = fold (fun a acc ->
+      match a with
+      | UnknownPtr _ -> true
+      | _ -> acc
+    ) ad false
+
   let unknownptrs_origins doc ad =
     fold (fun addr acc ->
         match addr with

src/cdomains/addressDomain_intf.ml

@@ -195,6 +195,8 @@ sig
     val string_comparison: t -> t -> int option -> ID.t
     val string_writing_defined: t -> bool
     val remove_unknownptrs: t -> t
+    val get_unknownptrs: t -> t
+    val has_unknownptr: t -> bool
     val unknownptrs_origins: GoblintCil.Pretty.doc -> t -> (GoblintCil.Pretty.doc * Messages.Location.t option) list
   end
 end