Merge pull request #1364 from diffblue/phread-create-fix

pthread_create arguments null/nonnull fix
diffblue · Sep 11, 2017 · 4febd10 · 4febd10
2 parents 8782103 + 3ddd377
commit 4febd10
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 33 deletions.
diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c
@@ -523,22 +523,19 @@ extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
 extern unsigned long __CPROVER_next_thread_id;
 
 inline int pthread_create(
-  pthread_t *thread,
-  const pthread_attr_t *attr,
-  void * (*start_routine)(void *),
-  void *arg)
+  pthread_t *thread, // must not be null
+  const pthread_attr_t *attr, // may be null
+  void * (*start_routine)(void *), // must not be null
+  void *arg) // may be null
 {
   __CPROVER_HIDE:;
   unsigned long this_thread_id;
   __CPROVER_atomic_begin();
   this_thread_id=++__CPROVER_next_thread_id;
   __CPROVER_atomic_end();
 
-  if(thread)
-  {
-    // pthread_t is a pointer type on some systems
-    *thread=(pthread_t)this_thread_id;
-  }
+  // pthread_t is a pointer type on some systems
+  *thread=(pthread_t)this_thread_id;
 
   #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_set_must(thread, "pthread-id");

diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c
@@ -298,12 +298,6 @@ inline char *strncat(char *dst, const char *src, size_t n)
 inline int strcmp(const char *s1, const char *s2)
 {
   __CPROVER_HIDE:;
-  #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
-  #else
-  // musl guarantees non-null of s1
-  if(s1==s2) return 0;
-  #endif
   #ifdef __CPROVER_STRING_ABSTRACTION
   int retval;
   __CPROVER_assert(__CPROVER_is_zero_string(s1), "strcmp zero-termination of 1st argument");
@@ -345,12 +339,6 @@ inline int strcmp(const char *s1, const char *s2)
 inline int strcasecmp(const char *s1, const char *s2)
 {
   __CPROVER_HIDE:;
-  #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
-  #else
-  // musl guarantees non-null of s1
-  if(s1==s2) return 0;
-  #endif
   #ifdef __CPROVER_STRING_ABSTRACTION
   int retval;
   __CPROVER_assert(__CPROVER_is_zero_string(s1), "strcasecmp zero-termination of 1st argument");
@@ -395,12 +383,6 @@ inline int strcasecmp(const char *s1, const char *s2)
 inline int strncmp(const char *s1, const char *s2, size_t n)
 {
   __CPROVER_HIDE:;
-  #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
-  #else
-  // musl guarantees non-null of s1
-  if(s1==s2) return 0;
-  #endif
   #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(s1) || __CPROVER_buffer_size(s1)>=n, "strncmp zero-termination of 1st argument");
   __CPROVER_assert(__CPROVER_is_zero_string(s2) || __CPROVER_buffer_size(s2)>=n, "strncmp zero-termination of 2nd argument");
@@ -439,12 +421,6 @@ inline int strncmp(const char *s1, const char *s2, size_t n)
 inline int strncasecmp(const char *s1, const char *s2, size_t n)
 {
   __CPROVER_HIDE:;
-  #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
-  #else
-  // musl guarantees non-null of s1
-  if(s1==s2) return 0;
-  #endif
   #ifdef __CPROVER_STRING_ABSTRACTION
   int retval;
   __CPROVER_assert(__CPROVER_is_zero_string(s1), "strncasecmp zero-termination of 1st argument");