C library: make functions with zero parameters proper declarations

tautschnig · tautschnig · commit 374c4a8e7ece · 2023-02-13T14:27:18.000Z
C uses '(void)' to denote this, not an empty list of parameters.
diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c
@@ -14,8 +14,8 @@ const void *__CPROVER_new_object = 0;
 extern const void *__CPROVER_memory_leak;
 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
 int __builtin_clzll(unsigned long long);
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-__CPROVER_size_t __VERIFIER_nondet_size();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+__CPROVER_size_t __VERIFIER_nondet_size(void);
 
 /// \brief A conditionally writable range of bytes.
 typedef struct
diff --git a/src/ansi-c/library/fcntl.c b/src/ansi-c/library/fcntl.c
@@ -5,7 +5,7 @@
 #define __CPROVER_FCNTL_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int fcntl(int fd, int cmd, ...)
 {
diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c
@@ -8,8 +8,8 @@ extern int optind;
 #define __CPROVER_STRING_H_INCLUDED
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-size_t __VERIFIER_nondet_size_t();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+size_t __VERIFIER_nondet_size_t(void);
 
 int getopt(int argc, char *const argv[], const char *optstring)
 {
diff --git a/src/ansi-c/library/inet.c b/src/ansi-c/library/inet.c
@@ -7,7 +7,7 @@
 #define __CPROVER_INET_H_INCLUDED
 #endif
 
-in_addr_t __VERIFIER_nondet_in_addr_t();
+in_addr_t __VERIFIER_nondet_in_addr_t(void);
 
 in_addr_t inet_addr(const char *cp)
 {
@@ -33,7 +33,7 @@ in_addr_t inet_addr(const char *cp)
 #define __CPROVER_INET_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int inet_aton(const char *cp, struct in_addr *pin)
 {
@@ -60,7 +60,7 @@ int inet_aton(const char *cp, struct in_addr *pin)
 #define __CPROVER_INET_H_INCLUDED
 #endif
 
-in_addr_t __VERIFIER_nondet_in_addr_t();
+in_addr_t __VERIFIER_nondet_in_addr_t(void);
 
 in_addr_t inet_network(const char *cp)
 {
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
@@ -465,7 +465,7 @@ int __fpclassify(double d)
 
 /* FUNCTION: sin */
 
-double __VERIFIER_nondet_double();
+double __VERIFIER_nondet_double(void);
 
 double sin(double x)
 {
@@ -486,7 +486,7 @@ double sin(double x)
 
 /* FUNCTION: sinl */
 
-long double __VERIFIER_nondet_long_double();
+long double __VERIFIER_nondet_long_double(void);
 
 long double sinl(long double x)
 {
@@ -507,7 +507,7 @@ long double sinl(long double x)
 
 /* FUNCTION: sinf */
 
-float __VERIFIER_nondet_float();
+float __VERIFIER_nondet_float(void);
 
 float sinf(float x)
 {
@@ -528,7 +528,7 @@ float sinf(float x)
 
 /* FUNCTION: cos */
 
-double __VERIFIER_nondet_double();
+double __VERIFIER_nondet_double(void);
 
 double cos(double x)
 {
@@ -549,7 +549,7 @@ double cos(double x)
 
 /* FUNCTION: cosl */
 
-long double __VERIFIER_nondet_long_double();
+long double __VERIFIER_nondet_long_double(void);
 
 long double cosl(long double x)
 {
@@ -570,7 +570,7 @@ long double cosl(long double x)
 
 /* FUNCTION: cosf */
 
-float __VERIFIER_nondet_float();
+float __VERIFIER_nondet_float(void);
 
 float cosf(float x)
 {
@@ -833,7 +833,7 @@ __CPROVER_hide:;
 
 float nextUpf(float f);
 
-float __VERIFIER_nondet_float();
+float __VERIFIER_nondet_float(void);
 
 float sqrtf(float f)
 {
@@ -920,7 +920,7 @@ float sqrtf(float f)
 
 double nextUp(double d);
 
-double __VERIFIER_nondet_double();
+double __VERIFIER_nondet_double(void);
 
 double sqrt(double d)
 {
@@ -991,7 +991,7 @@ double sqrt(double d)
 
 long double nextUpl(long double d);
 
-long double __VERIFIER_nondet_long_double();
+long double __VERIFIER_nondet_long_double(void);
 
 long double sqrtl(long double d)
 {
diff --git a/src/ansi-c/library/mman.c b/src/ansi-c/library/mman.c
@@ -19,7 +19,7 @@
 #    define MAP_UNINITIALIZED 0
 #  endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 void *mmap(
   void *addr,
@@ -72,7 +72,7 @@ void *mmap(
 #    define MAP_UNINITIALIZED 0
 #  endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 void *_mmap(
   void *addr,
@@ -106,7 +106,7 @@ void *_mmap(
 
 /* FUNCTION: munmap */
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 int munmap(void *addr, __CPROVER_size_t length)
 {
@@ -119,7 +119,7 @@ int munmap(void *addr, __CPROVER_size_t length)
 
 /* FUNCTION: _munmap */
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 int _munmap(void *addr, __CPROVER_size_t length)
 {
diff --git a/src/ansi-c/library/netdb.c b/src/ansi-c/library/netdb.c
@@ -6,7 +6,7 @@
 #include <netdb.h>
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 struct hostent *gethostbyname(const char *name)
 {
@@ -35,7 +35,7 @@ struct hostent *gethostbyname(const char *name)
 #include <netdb.h>
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type)
 {
@@ -59,7 +59,7 @@ struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type)
 // There does not appear to be a Windows variant of gethostent
 #include <netdb.h>
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 struct hostent *gethostent(void)
 {
diff --git a/src/ansi-c/library/process.c b/src/ansi-c/library/process.c
@@ -1,6 +1,6 @@
 /* FUNCTION: _beginthread */
 
-__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t();
+__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t(void);
 
 __CPROVER_size_t _beginthread(
   void (*start_address)(void *),
@@ -16,7 +16,7 @@ __CPROVER_size_t _beginthread(
 
 /* FUNCTION: _beginthreadex */
 
-__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t();
+__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t(void);
 
 __CPROVER_size_t _beginthreadex(
    void *security,
diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c
@@ -5,7 +5,7 @@
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
 {
@@ -30,7 +30,7 @@ int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 int pthread_cancel(pthread_t thread)
 {
@@ -839,7 +839,7 @@ int pthread_spin_trylock(pthread_spinlock_t *lock)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 // no pthread_barrier_t on the Mac
 // slightly different declaration on OpenBSD
@@ -893,7 +893,7 @@ __CPROVER_HIDE:;
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 // no pthread_barrier_t on the Mac
 #ifndef __APPLE__
@@ -923,7 +923,7 @@ int pthread_barrier_destroy(pthread_barrier_t *barrier)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-int __VERIFIER_nondet_int();
+int __VERIFIER_nondet_int(void);
 
 // no pthread_barrier_t on the Mac
 #ifndef __APPLE__
diff --git a/src/ansi-c/library/random.c b/src/ansi-c/library/random.c
@@ -17,8 +17,8 @@
 #    define GRND_NONBLOCK 0
 #  endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-size_t __VERIFIER_nondet_size_t();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+size_t __VERIFIER_nondet_size_t(void);
 
 ssize_t getrandom(void *buf, size_t buflen, unsigned int flags)
 {
diff --git a/src/ansi-c/library/signal.c b/src/ansi-c/library/signal.c
@@ -10,7 +10,7 @@
 #define __CPROVER_SIGNAL_H_INCLUDED
 #endif
 
-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
 int kill(pid_t pid, int sig)
 {
diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
diff --git a/src/ansi-c/library/time.c b/src/ansi-c/library/time.c
diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c

Original file line number	Diff line number	Diff line change
`@@ -5,7 +5,7 @@`
`5`	`5`	`#define __CPROVER_FCNTL_H_INCLUDED`
`6`	`6`	`#endif`
`7`	`7`
`8`		`-int __VERIFIER_nondet_int();`
	`8`	`+int __VERIFIER_nondet_int(void);`
`9`	`9`
`10`	`10`	`int fcntl(int fd, int cmd, ...)`
`11`	`11`	`{`
Original file line number	Diff line number	Diff line change
`@@ -8,8 +8,8 @@ extern int optind;`
`8`	`8`	`#define __CPROVER_STRING_H_INCLUDED`
`9`	`9`	`#endif`
`10`	`10`
`11`		`-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();`
`12`		`-size_t __VERIFIER_nondet_size_t();`
	`11`	`+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);`
	`12`	`+size_t __VERIFIER_nondet_size_t(void);`
`13`	`13`
`14`	`14`	`int getopt(int argc, char const argv[], const char optstring)`
`15`	`15`	`{`
Original file line number	Diff line number	Diff line change
`@@ -7,7 +7,7 @@`
`7`	`7`	`#define __CPROVER_INET_H_INCLUDED`
`8`	`8`	`#endif`
`9`	`9`
`10`		`-in_addr_t __VERIFIER_nondet_in_addr_t();`
	`10`	`+in_addr_t __VERIFIER_nondet_in_addr_t(void);`
`11`	`11`
`12`	`12`	`in_addr_t inet_addr(const char *cp)`
`13`	`13`	`{`
`@@ -33,7 +33,7 @@ in_addr_t inet_addr(const char *cp)`
`33`	`33`	`#define __CPROVER_INET_H_INCLUDED`
`34`	`34`	`#endif`
`35`	`35`
`36`		`-int __VERIFIER_nondet_int();`
	`36`	`+int __VERIFIER_nondet_int(void);`
`37`	`37`
`38`	`38`	`int inet_aton(const char cp, struct in_addr pin)`
`39`	`39`	`{`
`@@ -60,7 +60,7 @@ int inet_aton(const char cp, struct in_addr pin)`
`60`	`60`	`#define __CPROVER_INET_H_INCLUDED`
`61`	`61`	`#endif`
`62`	`62`
`63`		`-in_addr_t __VERIFIER_nondet_in_addr_t();`
	`63`	`+in_addr_t __VERIFIER_nondet_in_addr_t(void);`
`64`	`64`
`65`	`65`	`in_addr_t inet_network(const char *cp)`
`66`	`66`	`{`
Original file line number	Diff line number	Diff line change
`@@ -465,7 +465,7 @@ int __fpclassify(double d)`
`465`	`465`
`466`	`466`	`/* FUNCTION: sin */`
`467`	`467`
`468`		`-double __VERIFIER_nondet_double();`
	`468`	`+double __VERIFIER_nondet_double(void);`
`469`	`469`
`470`	`470`	`double sin(double x)`
`471`	`471`	`{`
`@@ -486,7 +486,7 @@ double sin(double x)`
`486`	`486`
`487`	`487`	`/* FUNCTION: sinl */`
`488`	`488`
`489`		`-long double __VERIFIER_nondet_long_double();`
	`489`	`+long double __VERIFIER_nondet_long_double(void);`
`490`	`490`
`491`	`491`	`long double sinl(long double x)`
`492`	`492`	`{`
`@@ -507,7 +507,7 @@ long double sinl(long double x)`
`507`	`507`
`508`	`508`	`/* FUNCTION: sinf */`
`509`	`509`
`510`		`-float __VERIFIER_nondet_float();`
	`510`	`+float __VERIFIER_nondet_float(void);`
`511`	`511`
`512`	`512`	`float sinf(float x)`
`513`	`513`	`{`
`@@ -528,7 +528,7 @@ float sinf(float x)`
`528`	`528`
`529`	`529`	`/* FUNCTION: cos */`
`530`	`530`
`531`		`-double __VERIFIER_nondet_double();`
	`531`	`+double __VERIFIER_nondet_double(void);`
`532`	`532`
`533`	`533`	`double cos(double x)`
`534`	`534`	`{`
`@@ -549,7 +549,7 @@ double cos(double x)`
`549`	`549`
`550`	`550`	`/* FUNCTION: cosl */`
`551`	`551`
`552`		`-long double __VERIFIER_nondet_long_double();`
	`552`	`+long double __VERIFIER_nondet_long_double(void);`
`553`	`553`
`554`	`554`	`long double cosl(long double x)`
`555`	`555`	`{`
`@@ -570,7 +570,7 @@ long double cosl(long double x)`
`570`	`570`
`571`	`571`	`/* FUNCTION: cosf */`
`572`	`572`
`573`		`-float __VERIFIER_nondet_float();`
	`573`	`+float __VERIFIER_nondet_float(void);`
`574`	`574`
`575`	`575`	`float cosf(float x)`
`576`	`576`	`{`
`@@ -833,7 +833,7 @@ __CPROVER_hide:;`
`833`	`833`
`834`	`834`	`float nextUpf(float f);`
`835`	`835`
`836`		`-float __VERIFIER_nondet_float();`
	`836`	`+float __VERIFIER_nondet_float(void);`
`837`	`837`
`838`	`838`	`float sqrtf(float f)`
`839`	`839`	`{`
`@@ -920,7 +920,7 @@ float sqrtf(float f)`
`920`	`920`
`921`	`921`	`double nextUp(double d);`
`922`	`922`
`923`		`-double __VERIFIER_nondet_double();`
	`923`	`+double __VERIFIER_nondet_double(void);`
`924`	`924`
`925`	`925`	`double sqrt(double d)`
`926`	`926`	`{`
`@@ -991,7 +991,7 @@ double sqrt(double d)`
`991`	`991`
`992`	`992`	`long double nextUpl(long double d);`
`993`	`993`
`994`		`-long double __VERIFIER_nondet_long_double();`
	`994`	`+long double __VERIFIER_nondet_long_double(void);`
`995`	`995`
`996`	`996`	`long double sqrtl(long double d)`
`997`	`997`	`{`
Original file line number	Diff line number	Diff line change
`@@ -6,7 +6,7 @@`
`6`	`6`	`#include <netdb.h>`
`7`	`7`	`#endif`
`8`	`8`
`9`		`-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();`
	`9`	`+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);`
`10`	`10`
`11`	`11`	`struct hostent gethostbyname(const char name)`
`12`	`12`	`{`
`@@ -35,7 +35,7 @@ struct hostent gethostbyname(const char name)`
`35`	`35`	`#include <netdb.h>`
`36`	`36`	`#endif`
`37`	`37`
`38`		`-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();`
	`38`	`+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);`
`39`	`39`
`40`	`40`	`struct hostent gethostbyaddr(const void addr, socklen_t len, int type)`
`41`	`41`	`{`
`@@ -59,7 +59,7 @@ struct hostent gethostbyaddr(const void addr, socklen_t len, int type)`
`59`	`59`	`// There does not appear to be a Windows variant of gethostent`
`60`	`60`	`#include <netdb.h>`
`61`	`61`
`62`		`-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();`
	`62`	`+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);`
`63`	`63`
`64`	`64`	`struct hostent *gethostent(void)`
`65`	`65`	`{`
Original file line number	Diff line number	Diff line change
`@@ -17,8 +17,8 @@`
`17`	`17`	`# define GRND_NONBLOCK 0`
`18`	`18`	`# endif`
`19`	`19`
`20`		`-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();`
`21`		`-size_t __VERIFIER_nondet_size_t();`
	`20`	`+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);`
	`21`	`+size_t __VERIFIER_nondet_size_t(void);`
`22`	`22`
`23`	`23`	`ssize_t getrandom(void *buf, size_t buflen, unsigned int flags)`
`24`	`24`	`{`
Original file line number	Diff line number	Diff line change
`@@ -10,7 +10,7 @@`
`10`	`10`	`#define __CPROVER_SIGNAL_H_INCLUDED`
`11`	`11`	`#endif`
`12`	`12`
`13`		`-__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();`
	`13`	`+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);`
`14`	`14`
`15`	`15`	`int kill(pid_t pid, int sig)`
`16`	`16`	`{`