C library: remove explicit zero initialisers

We initialise (with the default zero) value global variables in multiple
model functions, which can result in spurious warnings about those
variables already having an initial value.

Towards: #8638

Author: tautschnig

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

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);

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 *);

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)

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);