diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 0087501ed6c..0edb8052543 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -7,11 +7,11 @@ #define __CPROVER_contracts_library_defined // external dependencies -const void *__CPROVER_alloca_object = 0; +const void *__CPROVER_alloca_object; extern const void *__CPROVER_deallocated; -const void *__CPROVER_new_object = 0; +const void *__CPROVER_new_object; extern const void *__CPROVER_memory_leak; -__CPROVER_bool __CPROVER_malloc_is_new_array = 0; +__CPROVER_bool __CPROVER_malloc_is_new_array; #if defined(_WIN32) && defined(_M_X64) int __builtin_clzll(unsigned long long); #else diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c index 3066b14a256..b858153dcdd 100644 --- a/src/ansi-c/library/getopt.c +++ b/src/ansi-c/library/getopt.c @@ -5,7 +5,7 @@ #define __CPROVER_STRING_H_INCLUDED #endif -char *optarg = NULL; +char *optarg; int optind = 1; __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void); diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index 87a60a463a4..3b408b27f34 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -341,7 +341,7 @@ __CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; #ifndef LIBRARY_CHECK __CPROVER_thread_local unsigned long __CPROVER_thread_id = 0; #endif -unsigned long __CPROVER_next_thread_id = 0; +unsigned long __CPROVER_next_thread_id; int pthread_join(pthread_t thread, void **value_ptr) { @@ -379,7 +379,7 @@ __CPROVER_HIDE:; __CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; # ifndef LIBRARY_CHECK __CPROVER_thread_local unsigned long __CPROVER_thread_id = 0; -unsigned long __CPROVER_next_thread_id = 0; +unsigned long __CPROVER_next_thread_id; # endif int _pthread_join(pthread_t thread, void **value_ptr) @@ -615,7 +615,7 @@ __CPROVER_HIDE:; #endif #ifndef LIBRARY_CHECK -unsigned long __CPROVER_next_thread_id = 0; +unsigned long __CPROVER_next_thread_id; # if 0 __CPROVER_thread_local void ( *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *); diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index d50cfc2518e..c82b495e256 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -141,7 +141,7 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void); #ifndef __GNUC__ _Bool __builtin_mul_overflow(); #endif -__CPROVER_bool __CPROVER_malloc_is_new_array = 0; +__CPROVER_bool __CPROVER_malloc_is_new_array; void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size) { @@ -204,7 +204,7 @@ __CPROVER_HIDE:; __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void); #ifndef LIBRARY_CHECK -__CPROVER_bool __CPROVER_malloc_is_new_array = 0; +__CPROVER_bool __CPROVER_malloc_is_new_array; #endif // malloc is marked "inline" for the benefit of goto-analyzer. Really, @@ -262,9 +262,9 @@ __CPROVER_HIDE:; /* FUNCTION: __builtin_alloca */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void); -const void *__CPROVER_alloca_object = 0; +const void *__CPROVER_alloca_object; #ifndef LIBRARY_CHECK -__CPROVER_bool __CPROVER_malloc_is_new_array = 0; +__CPROVER_bool __CPROVER_malloc_is_new_array; #endif void *__builtin_alloca(__CPROVER_size_t alloca_size) @@ -307,11 +307,11 @@ __CPROVER_HIDE:; void __CPROVER_deallocate(void *); __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void); #ifndef LIBRARY_CHECK -const void *__CPROVER_alloca_object = 0; +const void *__CPROVER_alloca_object; #endif -const void *__CPROVER_new_object = 0; +const void *__CPROVER_new_object; #ifndef LIBRARY_CHECK -__CPROVER_bool __CPROVER_malloc_is_new_array = 0; +__CPROVER_bool __CPROVER_malloc_is_new_array; #endif void free(void *ptr) diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c index f9f26267b8b..5dbc17d8e5f 100644 --- a/src/ansi-c/library/unistd.c +++ b/src/ansi-c/library/unistd.c @@ -83,7 +83,7 @@ int unlink(const char *s) extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; -unsigned __CPROVER_pipe_count = 0; +unsigned __CPROVER_pipe_count; __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);