Skip to content

pthread_create arguments null/nonnull fix #1364

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Sep 11, 2017
Merged

pthread_create arguments null/nonnull fix #1364

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fe60e60
pthread_create arguments null/nonnull fix
Sep 10, 2017
3ddd377
clean-out ill-modeled optimization in string comparisons
Sep 11, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 6 additions & 9 deletions src/ansi-c/library/pthread_lib.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand Down
24 changes: 0 additions & 24 deletions src/ansi-c/library/string.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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");
Expand Down