Merge pull request #8698 from tautschnig/remove-redundant-init

C library: remove explicit zero initialisers

Author: kroening

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