Simplify cardinal > 0 to not is_empty

goblint · Aug 25, 2023 · 57549d0 · 57549d0
1 parent 866f517
commit 57549d0
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
@@ -65,7 +65,7 @@ struct
 
   let mayPointTo ctx exp =
     match ctx.ask (Queries.MayPointTo exp) with
-    | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad > 0 ->
+    | ad when not (Queries.AD.is_top ad) && not (Queries.AD.is_empty ad) ->
       let a' = if Queries.AD.mem UnknownPtr ad then (
           M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
           Queries.AD.remove UnknownPtr ad

diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
@@ -878,7 +878,7 @@ module Spec : Analyses.MCPSpec = struct
   module ExprEval = struct
     let eval_ptr ctx exp =
       let ad = ctx.ask (Queries.MayPointTo exp) in
-      if (not (Queries.AD.is_top ad)) && Queries.AD.cardinal ad > 0 then
+      if (not (Queries.AD.is_top ad)) && not (Queries.AD.is_empty ad) then
         if Queries.AD.mem UnknownPtr ad
         then (* UNSOUND *)
           Queries.AD.remove UnknownPtr ad