sem_post

goblint · Oct 1, 2023 · 9fae0dc · 9fae0dc
1 parent e0e11b1
commit 9fae0dc
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
@@ -59,6 +59,7 @@ type special =
   | MutexInit of { mutex:Cil.exp; attr: Cil.exp; }
   | 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
   | 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
@@ -410,6 +410,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("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);
   ]
 
 (** GCC builtin functions.
@@ -1158,7 +1159,6 @@ let invalidate_actions = [
     "setrlimit", readsAll; (*safe*)
     "getrlimit", writes [2]; (*keep [2]*)
     "sem_destroy", readsAll; (*safe*)
-    "sem_post", readsAll; (*safe*)
     "PL_NewHashTable", readsAll; (*safe*)
     "assert_failed", readsAll; (*safe*)
     "munmap", readsAll;(*safe*)