Use free instead of write access for realloc

src/analyses/libraryFunctions.ml

@@ -153,6 +153,12 @@ struct
     | `Read  -> o
     | `Free  -> i
 
+  let readsFrees rs fs a x =
+    match a with
+    | `Write -> []
+    | `Read  -> keep rs x
+    | `Free  -> keep fs x
+
   let onlyReads ns a x =
     match a with
     | `Write -> []
@@ -452,7 +458,7 @@ let invalidate_actions = [
     "rand", readsAll; (*safe*)
     "gethostname", writesAll; (*unsafe*)
     "fork", readsAll; (*safe*)
-    "realloc", writes [1];(*unsafe*) (* TODO: replace write with free+read *)
+    "realloc", readsFrees [0; 1] [0]; (* read+free first argument, read second argument *)
     "setrlimit", readsAll; (*safe*)
     "getrlimit", writes [2]; (*keep [2]*)
     "sem_init", readsAll; (*safe*)

tests/regression/02-base/76-realloc.c

@@ -1,3 +1,4 @@
+// PARAM: --enable ana.race.free
 #include <stdlib.h>
 #include <assert.h>
 #include <pthread.h>
@@ -30,8 +31,22 @@ void test2() {
   realloc(p, sizeof(int)); // RACE!
 }
 
+void* test3_f(void *arg) {
+  int *p = arg;
+  int x = *p; // RACE!
+  return NULL;
+}
+
+void test3() {
+  int *p = malloc(sizeof(int));
+  pthread_t id;
+  pthread_create(&id, NULL, test3_f, p);
+  realloc(p, sizeof(int)); // RACE!
+}
+
 int main() {
   test1();
   test2();
+  test3();
   return 0;
 }

tests/regression/02-base/78-realloc-free.c

@@ -0,0 +1,53 @@
+// PARAM: --disable ana.race.free
+// copy of 02-base/76-realloc with different PARAM
+#include <stdlib.h>
+#include <assert.h>
+#include <pthread.h>
+
+void test1_f() {
+  assert(1); // reachable
+}
+
+void test1() {
+  void (**fpp)(void) = malloc(sizeof(void(**)(void)));
+  *fpp = &test1_f;
+
+  fpp = realloc(fpp, sizeof(void(**)(void))); // same size
+
+  // (*fpp)();
+  void (*fp)(void) = *fpp;
+  fp(); // should call test1_f
+}
+
+void* test2_f(void *arg) {
+  int *p = arg;
+  *p = 1; // RACE!
+  return NULL;
+}
+
+void test2() {
+  int *p = malloc(sizeof(int));
+  pthread_t id;
+  pthread_create(&id, NULL, test2_f, p);
+  realloc(p, sizeof(int)); // RACE!
+}
+
+void* test3_f(void *arg) {
+  int *p = arg;
+  int x = *p; // NORACE
+  return NULL;
+}
+
+void test3() {
+  int *p = malloc(sizeof(int));
+  pthread_t id;
+  pthread_create(&id, NULL, test3_f, p);
+  realloc(p, sizeof(int)); // NORACE
+}
+
+int main() {
+  test1();
+  test2();
+  test3();
+  return 0;
+}