Skip to content

C library: remove explicit zero initialisers #8698

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 1 commit into from
Jul 26, 2025
Merged

C library: remove explicit zero initialisers #8698

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
6 changes: 3 additions & 3 deletions src/ansi-c/library/cprover_contracts.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/library/getopt.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
6 changes: 3 additions & 3 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 @@ -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)
{
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 *);
Expand Down
14 changes: 7 additions & 7 deletions src/ansi-c/library/stdlib.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/library/unistd.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand Down
Loading