Add missing accesses to VLA lengths

src/analyses/accessAnalysis.ml

@@ -56,6 +56,10 @@ struct
 
   (** Transfer functions: *)
 
+  let vdecl ctx v =
+    access_one_top ctx Read false (SizeOf v.vtype);
+    ctx.local
+
   let assign ctx lval rval : D.t =
     (* ignore global inits *)
     if !GU.global_initialization then ctx.local else begin

src/domains/access.ml

@@ -282,13 +282,32 @@ and distribute_access_exp f = function
     distribute_access_exp f b;
     distribute_access_exp f t;
     distribute_access_exp f e
+
+  | SizeOf t ->
+    distribute_access_type f t
+
   | Const _
-  | SizeOf _
   | SizeOfStr _
   | AlignOf _
   | AddrOfLabel _ ->
     ()
 
+and distribute_access_type f = function
+  | TArray (et, len, _) ->
+    Option.may (distribute_access_exp f) len;
+    distribute_access_type f et
+
+  | TVoid _
+  | TInt _
+  | TFloat _
+  | TPtr _
+  | TFun _
+  | TNamed _
+  | TComp _
+  | TEnum _
+  | TBuiltin_va_list _ ->
+    ()
+
 let add side e kind conf vo oo a =
   let ty = get_val_type e vo oo in
   (* let loc = !Tracing.current_loc in *)

tests/regression/04-mutex/68-vla_rc.c

@@ -0,0 +1,17 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+
+void *t_fun(void *arg) {
+  g=g+1; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  int a[g]; // RACE!
+  int b[2][g]; // RACE!
+  return 0;
+}

tests/regression/04-mutex/69-sizeof_rc.c

@@ -0,0 +1,17 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+
+void *t_fun(void *arg) {
+  g=g+1; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  int a = sizeof(int[g]); // RACE!
+  int b = sizeof(int[2][g]); // RACE!
+  return 0;
+}