diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 597c08f72f..fde24ac77e 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -58,6 +58,7 @@ type special = | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; } | 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} | 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 index f3c00f9b48..08ec2e2b3e 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -407,7 +407,10 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("sem_timedwait", unknown [drop "sem" [r]; drop "abs_timeout" [r]]); (* no write accesses to sem because sync primitive itself has no race *) ("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]); ("pthread_getaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [w]]); + (* TODO: Remove w as soon as we have proper support for semaphores *) ("sem_init", special [__ "sem" [w]; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value}); + ("sem_wait", special [__ "sem" [w]] @@ fun sem -> SemWait {sem; try_ = false}); + ("sem_trywait", special [__ "sem" [w]] @@ fun sem -> SemWait {sem; try_ = true}); ] (** GCC builtin functions. @@ -1156,7 +1159,6 @@ let invalidate_actions = [ "setrlimit", readsAll; (*safe*) "getrlimit", writes [2]; (*keep [2]*) "sem_destroy", readsAll; (*safe*) - "sem_wait", readsAll; (*safe*) "sem_post", readsAll; (*safe*) "PL_NewHashTable", readsAll; (*safe*) "assert_failed", readsAll; (*safe*)