From 6c354a5dc8df3812d06b2f5e807cd56830ef11d2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Jul 2025 14:54:43 +0000
Subject: [PATCH] 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
---
 src/ansi-c/library/cprover_contracts.c |  6 +++---
 src/ansi-c/library/getopt.c            |  2 +-
 src/ansi-c/library/pthread_lib.c       |  6 +++---
 src/ansi-c/library/stdlib.c            | 14 +++++++-------
 src/ansi-c/library/unistd.c            |  2 +-
 5 files changed, 15 insertions(+), 15 deletions(-)

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