Add TODOs about AddressDomain queries usage

goblint · Sep 11, 2023 · c8cc6c4 · c8cc6c4
1 parent 5938225
commit c8cc6c4
Show file tree

Hide file tree

Showing 8 changed files with 10 additions and 10 deletions.
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
@@ -72,7 +72,7 @@ struct
         ) else ad
       in
       List.filter_map (function
-          | ValueDomain.Addr.Addr (v,o) -> Some (v, ValueDomain.Addr.Offs.to_exp o)
+          | ValueDomain.Addr.Addr (v,o) -> Some (v, ValueDomain.Addr.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *)
           | _ -> None
         ) (Queries.AD.elements a')
     | _ -> []

diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
@@ -99,7 +99,7 @@ struct
         | ad when not (Queries.AD.is_top ad) ->
           let to_extra addr ads =
             match addr with
-            | Queries.AD.Addr.Addr mval -> AD.of_mval mval :: ads
+            | Queries.AD.Addr.Addr mval -> AD.of_mval mval :: ads (* TODO: why list of singleton AD-s? *)
             | _ -> ads
           in
           Queries.AD.fold to_extra ad []

diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
@@ -57,7 +57,7 @@ struct
             | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.singleton v
             | _ -> D.empty ()
           in
-          D.diff state unique_pointed_to_heap_vars
+          D.diff state unique_pointed_to_heap_vars (* TODO: use D.remove instead of diffing singleton *)
         | _ -> state
       end
     | Abort ->

diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml
@@ -18,7 +18,7 @@ struct
   module O = Offset.Unit
 
   module V = struct
-    include Printable.Prod(CilType.Varinfo)(O)
+    include Printable.Prod(CilType.Varinfo)(O) (* TODO: use Mval.Unit *)
     let is_write_only _ = false
   end
 
@@ -56,7 +56,7 @@ struct
       let attr = ctx.ask (Queries.EvalMutexAttr attr) in
       let mutexes = ctx.ask (Queries.MayPointTo mutex) in
       (* It is correct to iter over these sets here, as mutexes need to be intialized before being used, and an analysis that detects usage before initialization is a different analysis. *)
-      Queries.AD.iter (function addr -> 
+      Queries.AD.iter (function addr ->
         match addr with
         | Queries.AD.Addr.Addr (v,o) -> ctx.sideg (v,O.of_offs o) attr
         | _ -> ()

diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
@@ -103,7 +103,7 @@ struct
         | ad ->
           Queries.AD.fold (fun addr vs ->
               match addr with
-              | Queries.AD.Addr.Addr (v,o) -> rem_mval vs (v, ValueDomain.Offs.to_exp o)
+              | Queries.AD.Addr.Addr (v,o) -> rem_mval vs (v, ValueDomain.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *)
               | _ -> vs
             ) ad ctx.local
       end

diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
@@ -12,7 +12,7 @@ let to_mvals ad =
   (* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *)
   Queries.AD.fold (fun addr mvals ->
       match addr with
-      | Queries.AD.Addr.Addr (v,o) -> D.add (v, ValueDomain.Offs.to_exp o) mvals
+      | Queries.AD.Addr.Addr (v,o) -> D.add (v, ValueDomain.Offs.to_exp o) mvals (* TODO: use unconverted addrs in domain? *)
       | _ -> mvals
     ) ad (D.empty ())
 

diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
@@ -198,7 +198,7 @@ struct
         | ad when not (Queries.AD.is_top ad) ->
           let to_extra ad ads =
             match ad with
-            | Queries.AD.Addr.Addr mval -> AD.of_mval mval :: ads
+            | Queries.AD.Addr.Addr mval -> AD.of_mval mval :: ads (* TODO: why list of singleton AD-s? *)
             | _ -> ads
           in
           Queries.AD.fold to_extra ad []

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
@@ -258,7 +258,7 @@ struct
         if Queries.AD.is_top aad
         then false
         else Queries.AD.exists (function
-            | Addr (u,s) -> CilType.Varinfo.equal v u && oleq o (Addr.Offs.to_exp s)
+            | Addr (u,s) -> CilType.Varinfo.equal v u && oleq o (Addr.Offs.to_exp s) (* TODO: avoid conversion? *)
             | _ -> false
           ) aad
       in
@@ -298,7 +298,7 @@ struct
       else if Queries.AD.is_top bad
       then ((*Messages.warn ~category:Analyzer "No PT-set: switching to types ";*) type_may_change_apt a )
       else Queries.AD.exists (function
-          | Addr (v,o) -> lval_may_change_pt a (v, Addr.Offs.to_exp o)
+          | Addr (v,o) -> lval_may_change_pt a (v, Addr.Offs.to_exp o) (* TODO: avoid conversion? *)
           | _ -> false
         ) bad
     in