Do not record accesses to sem

goblint · Oct 3, 2023 · 79d71b8 · 79d71b8
1 parent d855613
commit 79d71b8
Showing 1 changed file with 7 additions and 6 deletions.
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
@@ -435,12 +435,13 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_attr_setschedparam", unknown [drop "attr" [r; w]; drop "param" [r]]);
     ("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]);
     ("pthread_getaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [w]]);
-    ("sem_init", special [__ "sem" [r]; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value});
-    ("sem_wait", special [__ "sem" [r]] @@ fun sem -> SemWait {sem; try_ = false; timeout = None});
-    ("sem_trywait", special [__ "sem" [r]] @@ fun sem -> SemWait {sem; try_ = true; timeout = None});
-    ("sem_timedwait", special [__ "sem" [r]; __ "abs_timeout" [r]] @@ fun sem abs_timeout-> SemWait {sem; try_ = true; timeout = Some abs_timeout}); (* no write accesses to sem because sync primitive itself has no race *)
-    ("sem_post", special [__ "sem" [r]] @@ fun sem -> SemPost sem);
-    ("sem_destroy", special [__ "sem" [r]] @@ fun sem -> SemDestroy sem);
+    (* Not recording read accesses to sem as these are thread-safe anyway not to clutter messages (as for mutexes) **)
+    ("sem_init", special [__ "sem" []; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value});
+    ("sem_wait", special [__ "sem" []] @@ fun sem -> SemWait {sem; try_ = false; timeout = None});
+    ("sem_trywait", special [__ "sem" []] @@ fun sem -> SemWait {sem; try_ = true; timeout = None});
+    ("sem_timedwait", special [__ "sem" []; __ "abs_timeout" [r]] @@ fun sem abs_timeout-> SemWait {sem; try_ = true; timeout = Some abs_timeout}); (* no write accesses to sem because sync primitive itself has no race *)
+    ("sem_post", special [__ "sem" []] @@ fun sem -> SemPost sem);
+    ("sem_destroy", special [__ "sem" []] @@ fun sem -> SemDestroy sem);
   ]
 
 (** GCC builtin functions.