From fe60e60a5bfdad28ec64790e816b812692dc8666 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 10 Sep 2017 09:01:37 +0100 Subject: [PATCH 1/2] pthread_create arguments null/nonnull fix --- src/ansi-c/library/pthread_lib.c | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index 71af169c91b..97194052a54 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -523,10 +523,10 @@ 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; @@ -534,11 +534,8 @@ inline int pthread_create( 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"); From 3ddd377ca6d4c10149997889717d317b4705900c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 11 Sep 2017 11:25:35 +0100 Subject: [PATCH 2/2] clean-out ill-modeled optimization in string comparisons --- src/ansi-c/library/string.c | 24 ------------------------ 1 file changed, 24 deletions(-) diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c index 35cf46f7f66..0dabca6ebc5 100644 --- 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");