Add comment about ana.race.direct-arithmetic

goblint · Aug 22, 2023 · 4e1cf15 · 4e1cf15
1 parent a8a8899
commit 4e1cf15
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
@@ -238,10 +238,11 @@ struct
 
   (** Get immediate type_suffix memo. *)
   let type_suffix_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option =
+    (* No need to make ana.race.direct-arithmetic return None here,
+       because (int) is empty anyway since Access.add_distribute_outer isn't called. *)
     match root, offset with
     | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* global.foo.bar -> (struct S).foo.bar *) (* TODO: Alloc variables void type *)
     | _, `NoOffset -> None (* primitive type *)
-    (* TODO: should handle ana.race.direct-arithmetic special case here? *)
     | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') (* (struct S).foo.bar -> (struct T).bar *)
     | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') (* (int[])[*] -> int *)
     | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *)