Skip to content

Commit fe60e60

Browse files
author
Daniel Kroening
committed
pthread_create arguments null/nonnull fix
1 parent c125146 commit fe60e60

File tree

1 file changed

+6
-9
lines changed

1 file changed

+6
-9
lines changed

src/ansi-c/library/pthread_lib.c

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -523,22 +523,19 @@ extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
523523
extern unsigned long __CPROVER_next_thread_id;
524524

525525
inline int pthread_create(
526-
pthread_t *thread,
527-
const pthread_attr_t *attr,
528-
void * (*start_routine)(void *),
529-
void *arg)
526+
pthread_t *thread, // must not be null
527+
const pthread_attr_t *attr, // may be null
528+
void * (*start_routine)(void *), // must not be null
529+
void *arg) // may be null
530530
{
531531
__CPROVER_HIDE:;
532532
unsigned long this_thread_id;
533533
__CPROVER_atomic_begin();
534534
this_thread_id=++__CPROVER_next_thread_id;
535535
__CPROVER_atomic_end();
536536

537-
if(thread)
538-
{
539-
// pthread_t is a pointer type on some systems
540-
*thread=(pthread_t)this_thread_id;
541-
}
537+
// pthread_t is a pointer type on some systems
538+
*thread=(pthread_t)this_thread_id;
542539

543540
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
544541
__CPROVER_set_must(thread, "pthread-id");

0 commit comments

Comments
 (0)