Ignore atomic types in race detection (closes #521)

src/domains/access.ml

@@ -10,9 +10,10 @@ module M = Messages
 
 let is_ignorable_type (t: typ): bool =
   match t with
-  | TNamed (info, attr) -> info.tname = "atomic_t" || info.tname = "pthread_mutex_t" || info.tname = "spinlock_t"
-  | TComp (info, attr) -> info.cname = "lock_class_key"
-  | TInt (IInt, attr) -> hasAttribute "mutex" attr
+  | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "spinlock_t"; _ }, _) -> true
+  | TComp ({ cname = "lock_class_key"; _ }, _) -> true
+  | TInt (IInt, attr) when hasAttribute "mutex" attr -> true
+  | t when hasAttribute "atomic" (typeAttrs t) -> true (* C11 _Atomic *)
   | _ -> false
 
 let is_ignorable = function

tests/regression/04-mutex/62-simple_atomic_nr.c

@@ -0,0 +1,24 @@
+#include <pthread.h>
+#include <stdio.h>
+#include <stdatomic.h>
+
+atomic_int myglobal;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  myglobal=myglobal+1; // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex2);
+  myglobal=myglobal+1; // NORACE
+  pthread_mutex_unlock(&mutex2);
+  pthread_join (id, NULL);
+  return 0;
+}