sem_destroy

goblint · Oct 1, 2023 · 92528b1 · 92528b1
1 parent 9fae0dc
commit 92528b1
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
@@ -60,6 +60,7 @@ type special =
   | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; }
   | SemWait of { sem: Cil.exp; try_:bool; timeout: Cil.exp option;}
   | SemPost of Cil.exp
+  | SemDestroy of Cil.exp
   | Wait of { cond: Cil.exp; mutex: Cil.exp; }
   | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) }
   | Math of { fun_args: math; }

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
@@ -411,6 +411,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("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);
   ]
 
 (** GCC builtin functions.
@@ -1158,7 +1159,6 @@ let invalidate_actions = [
     "fork", readsAll; (*safe*)
     "setrlimit", readsAll; (*safe*)
     "getrlimit", writes [2]; (*keep [2]*)
-    "sem_destroy", readsAll; (*safe*)
     "PL_NewHashTable", readsAll; (*safe*)
     "assert_failed", readsAll; (*safe*)
     "munmap", readsAll;(*safe*)