Skip to content

Commit 5087d66

Browse files
tautschnigtautschnig
committed
C library: make functions with zero parameters proper declarations
C uses '(void)' to denote this, not an empty list of parameters.
1 parent 4b05d48 commit 5087d66

File tree

17 files changed

+96
-96
lines changed

17 files changed

+96
-96
lines changed

‎src/ansi-c/library/cprover_contracts.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,8 @@ const void *__CPROVER_new_object = 0;
1414
extern const void *__CPROVER_memory_leak;
1515
__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
1616
int __builtin_clzll(unsigned long long);
17-
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
18-
__CPROVER_size_t __VERIFIER_nondet_size();
17+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
18+
__CPROVER_size_t __VERIFIER_nondet_size(void);
1919

2020
/// \brief A conditionally writable range of bytes.
2121
typedef struct

‎src/ansi-c/library/fcntl.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
#define __CPROVER_FCNTL_H_INCLUDED
66
#endif
77

8-
int __VERIFIER_nondet_int();
8+
int __VERIFIER_nondet_int(void);
99

1010
int fcntl(int fd, int cmd, ...)
1111
{

‎src/ansi-c/library/gcc.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -212,7 +212,7 @@ float __builtin_ia32_vec_ext_v4sf(__gcc_v4sf vec, int offset)
212212
#ifndef LIBRARY_CHECK
213213
typedef short __gcc_v8hi __attribute__((__vector_size__(16)));
214214
#else
215-
__gcc_v8hi __CPROVER_saturating_minus();
215+
__gcc_v8hi __CPROVER_saturating_minus(__gcc_v8hi, __gcc_v8hi);
216216
#endif
217217

218218
__gcc_v8hi __builtin_ia32_psubsw128(__gcc_v8hi a, __gcc_v8hi b)
@@ -237,7 +237,7 @@ __gcc_v8hi __builtin_ia32_psubusw128(__gcc_v8hi a, __gcc_v8hi b)
237237
#ifndef LIBRARY_CHECK
238238
typedef short __gcc_v4hi __attribute__((__vector_size__(8)));
239239
#else
240-
__gcc_v4hi __CPROVER_saturating_plus();
240+
__gcc_v4hi __CPROVER_saturating_plus(__gcc_v4hi, __gcc_v4hi);
241241
#endif
242242

243243
__gcc_v4hi __builtin_ia32_paddsw(__gcc_v4hi a, __gcc_v4hi b)

‎src/ansi-c/library/getopt.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@ extern int optind;
88
#define __CPROVER_STRING_H_INCLUDED
99
#endif
1010

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

1414
int getopt(int argc, char *const argv[], const char *optstring)
1515
{

‎src/ansi-c/library/inet.c‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
#define __CPROVER_INET_H_INCLUDED
88
#endif
99

10-
in_addr_t __VERIFIER_nondet_in_addr_t();
10+
in_addr_t __VERIFIER_nondet_in_addr_t(void);
1111

1212
in_addr_t inet_addr(const char *cp)
1313
{
@@ -33,7 +33,7 @@ in_addr_t inet_addr(const char *cp)
3333
#define __CPROVER_INET_H_INCLUDED
3434
#endif
3535

36-
int __VERIFIER_nondet_int();
36+
int __VERIFIER_nondet_int(void);
3737

3838
int inet_aton(const char *cp, struct in_addr *pin)
3939
{
@@ -60,7 +60,7 @@ int inet_aton(const char *cp, struct in_addr *pin)
6060
#define __CPROVER_INET_H_INCLUDED
6161
#endif
6262

63-
in_addr_t __VERIFIER_nondet_in_addr_t();
63+
in_addr_t __VERIFIER_nondet_in_addr_t(void);
6464

6565
in_addr_t inet_network(const char *cp)
6666
{

‎src/ansi-c/library/math.c‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -465,7 +465,7 @@ int __fpclassify(double d)
465465

466466
/* FUNCTION: sin */
467467

468-
double __VERIFIER_nondet_double();
468+
double __VERIFIER_nondet_double(void);
469469

470470
double sin(double x)
471471
{
@@ -486,7 +486,7 @@ double sin(double x)
486486

487487
/* FUNCTION: sinl */
488488

489-
long double __VERIFIER_nondet_long_double();
489+
long double __VERIFIER_nondet_long_double(void);
490490

491491
long double sinl(long double x)
492492
{
@@ -507,7 +507,7 @@ long double sinl(long double x)
507507

508508
/* FUNCTION: sinf */
509509

510-
float __VERIFIER_nondet_float();
510+
float __VERIFIER_nondet_float(void);
511511

512512
float sinf(float x)
513513
{
@@ -528,7 +528,7 @@ float sinf(float x)
528528

529529
/* FUNCTION: cos */
530530

531-
double __VERIFIER_nondet_double();
531+
double __VERIFIER_nondet_double(void);
532532

533533
double cos(double x)
534534
{
@@ -549,7 +549,7 @@ double cos(double x)
549549

550550
/* FUNCTION: cosl */
551551

552-
long double __VERIFIER_nondet_long_double();
552+
long double __VERIFIER_nondet_long_double(void);
553553

554554
long double cosl(long double x)
555555
{
@@ -570,7 +570,7 @@ long double cosl(long double x)
570570

571571
/* FUNCTION: cosf */
572572

573-
float __VERIFIER_nondet_float();
573+
float __VERIFIER_nondet_float(void);
574574

575575
float cosf(float x)
576576
{
@@ -833,7 +833,7 @@ __CPROVER_hide:;
833833

834834
float nextUpf(float f);
835835

836-
float __VERIFIER_nondet_float();
836+
float __VERIFIER_nondet_float(void);
837837

838838
float sqrtf(float f)
839839
{
@@ -920,7 +920,7 @@ float sqrtf(float f)
920920

921921
double nextUp(double d);
922922

923-
double __VERIFIER_nondet_double();
923+
double __VERIFIER_nondet_double(void);
924924

925925
double sqrt(double d)
926926
{
@@ -991,7 +991,7 @@ double sqrt(double d)
991991

992992
long double nextUpl(long double d);
993993

994-
long double __VERIFIER_nondet_long_double();
994+
long double __VERIFIER_nondet_long_double(void);
995995

996996
long double sqrtl(long double d)
997997
{

‎src/ansi-c/library/mman.c‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919
# define MAP_UNINITIALIZED 0
2020
# endif
2121

22-
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
22+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
2323

2424
void *mmap(
2525
void *addr,
@@ -72,7 +72,7 @@ void *mmap(
7272
# define MAP_UNINITIALIZED 0
7373
# endif
7474

75-
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
75+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
7676

7777
void *_mmap(
7878
void *addr,
@@ -106,7 +106,7 @@ void *_mmap(
106106

107107
/* FUNCTION: munmap */
108108

109-
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
109+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
110110

111111
int munmap(void *addr, __CPROVER_size_t length)
112112
{
@@ -119,7 +119,7 @@ int munmap(void *addr, __CPROVER_size_t length)
119119

120120
/* FUNCTION: _munmap */
121121

122-
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
122+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
123123

124124
int _munmap(void *addr, __CPROVER_size_t length)
125125
{

‎src/ansi-c/library/netdb.c‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
#include <netdb.h>
77
#endif
88

9-
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
9+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
1010

1111
struct hostent *gethostbyname(const char *name)
1212
{
@@ -35,7 +35,7 @@ struct hostent *gethostbyname(const char *name)
3535
#include <netdb.h>
3636
#endif
3737

38-
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
38+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
3939

4040
struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type)
4141
{
@@ -59,7 +59,7 @@ struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type)
5959
// There does not appear to be a Windows variant of gethostent
6060
#include <netdb.h>
6161

62-
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
62+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
6363

6464
struct hostent *gethostent(void)
6565
{

‎src/ansi-c/library/process.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
/* FUNCTION: _beginthread */
22

3-
__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t();
3+
__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t(void);
44

55
__CPROVER_size_t _beginthread(
66
void (*start_address)(void *),
@@ -16,7 +16,7 @@ __CPROVER_size_t _beginthread(
1616

1717
/* FUNCTION: _beginthreadex */
1818

19-
__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t();
19+
__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t(void);
2020

2121
__CPROVER_size_t _beginthreadex(
2222
void *security,

‎src/ansi-c/library/pthread_lib.c‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
#define __CPROVER_PTHREAD_H_INCLUDED
66
#endif
77

8-
int __VERIFIER_nondet_int();
8+
int __VERIFIER_nondet_int(void);
99

1010
int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
1111
{
@@ -30,7 +30,7 @@ int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type)
3030
#define __CPROVER_PTHREAD_H_INCLUDED
3131
#endif
3232

33-
int __VERIFIER_nondet_int();
33+
int __VERIFIER_nondet_int(void);
3434

3535
int pthread_cancel(pthread_t thread)
3636
{
@@ -839,7 +839,7 @@ int pthread_spin_trylock(pthread_spinlock_t *lock)
839839
#define __CPROVER_PTHREAD_H_INCLUDED
840840
#endif
841841

842-
int __VERIFIER_nondet_int();
842+
int __VERIFIER_nondet_int(void);
843843

844844
// no pthread_barrier_t on the Mac
845845
// slightly different declaration on OpenBSD
@@ -893,7 +893,7 @@ __CPROVER_HIDE:;
893893
#define __CPROVER_PTHREAD_H_INCLUDED
894894
#endif
895895

896-
int __VERIFIER_nondet_int();
896+
int __VERIFIER_nondet_int(void);
897897

898898
// no pthread_barrier_t on the Mac
899899
#ifndef __APPLE__
@@ -923,7 +923,7 @@ int pthread_barrier_destroy(pthread_barrier_t *barrier)
923923
#define __CPROVER_PTHREAD_H_INCLUDED
924924
#endif
925925

926-
int __VERIFIER_nondet_int();
926+
int __VERIFIER_nondet_int(void);
927927

928928
// no pthread_barrier_t on the Mac
929929
#ifndef __APPLE__

0 commit comments

Comments
 (0)