Skip to content

Commit 239f996

Browse files
committed
pthread_cond_wait may return spuriously
The man page states: "In general, whenever a condition wait returns, the thread has to re-evaluate the predicate associated with the condition wait to determine whether it can safely proceed, should wait again, or should declare a timeout. A return from the wait does not imply that the associated predicate is either true or false."
1 parent b02b2fd commit 239f996

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/ansi-c/library/pthread_lib.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -636,8 +636,8 @@ inline int pthread_cond_wait(
636636
#endif
637637

638638
__CPROVER_atomic_begin();
639-
__CPROVER_assume(*((unsigned *)cond));
640-
(*((unsigned *)cond))--;
639+
if(*((unsigned *)cond))
640+
(*((unsigned *)cond))--;
641641
__CPROVER_atomic_end();
642642

643643
return 0; // we never fail

0 commit comments

Comments
 (0)