Merge pull request #1324 from goblint/alloca

Consider `Alloca` everywhere where `Malloc`, `Calloc` and `Realloc` are handled

src/analyses/mallocFresh.ml

@@ -39,14 +39,16 @@ struct
 
   let special ctx lval f args =
     let desc = LibraryFunctions.find f in
+    let alloc_var on_stack =
+      match ctx.ask (AllocVar {on_stack = on_stack}) with
+      | `Lifted var -> D.add var ctx.local
+      | _ -> ctx.local
+    in
     match desc.special args with
     | Malloc _
     | Calloc _
-    | Realloc _ ->
-      begin match ctx.ask (AllocVar {on_stack = false}) with
-        | `Lifted var -> D.add var ctx.local
-        | _ -> ctx.local
-      end
+    | Realloc _ -> alloc_var false
+    | Alloca _ -> alloc_var true
     | _ ->
       match lval with
       | None -> ctx.local

src/analyses/region.ml

@@ -156,7 +156,7 @@ struct
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     let desc = LibraryFunctions.find f in
     match desc.special arglist with
-    | Malloc _ | Calloc _ | Realloc _ -> begin
+    | Malloc _ | Calloc _ | Realloc _ | Alloca _ -> begin
         match ctx.local, lval with
         | `Lifted reg, Some lv ->
           let old_regpart = ctx.global () in

src/util/loopUnrolling.ml

@@ -316,6 +316,7 @@ class loopUnrollingCallVisitor = object
         | Malloc _
         | Calloc _
         | Realloc _
+        | Alloca _
         | Lock _
         | Unlock _
         | ThreadCreate _

tests/regression/45-escape/49-fresh-alloca.c

@@ -0,0 +1,27 @@
+// PARAM: --set ana.activated[+] mallocFresh --set ana.activated[-] mhp --set ana.thread.domain plain
+#include <pthread.h>
+#include <stdlib.h>
+
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun2(void *arg) {
+  int *i = arg;
+  pthread_mutex_lock(&A);
+  *i = 10; // NORACE
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+int main() {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded
+
+  int *i = alloca(sizeof(int));
+  *i = 5; // NORACE (fresh)
+  pthread_create(&id2, NULL, t_fun2, i);
+  return 0;
+}