Skip to content

Commit 1ab4d2a

Browse files
tautschnigtautschnig
committed
Built-in C library: only include headers that provide macro- or enum values
1 parent 36a70db commit 1ab4d2a

File tree

19 files changed

+176
-1249
lines changed

19 files changed

+176
-1249
lines changed

‎src/ansi-c/library/cprover.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ void __CPROVER_cover(__CPROVER_bool condition);
3838

3939
void __CPROVER_input(const char *id, ...);
4040
void __CPROVER_output(const char *id, ...);
41+
int __CPROVER_printf(const char *fmt, ...);
4142

4243
// concurrency-related
4344
void __CPROVER_atomic_begin();

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

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

3-
#ifndef __CPROVER_ERR_H_INCLUDED
4-
#include <err.h>
5-
#define __CPROVER_ERR_H_INCLUDED
6-
#endif
7-
8-
#ifndef __CPROVER_STDLIB_H_INCLUDED
9-
#include <stdlib.h>
10-
#define __CPROVER_STDLIB_H_INCLUDED
11-
#endif
3+
void abort(void);
124

135
void err(int eval, const char *fmt, ...)
146
{
@@ -19,15 +11,7 @@ void err(int eval, const char *fmt, ...)
1911

2012
/* FUNCTION: err */
2113

22-
#ifndef __CPROVER_ERR_H_INCLUDED
23-
#include <err.h>
24-
#define __CPROVER_ERR_H_INCLUDED
25-
#endif
26-
27-
#ifndef __CPROVER_STDLIB_H_INCLUDED
28-
#include <stdlib.h>
29-
#define __CPROVER_STDLIB_H_INCLUDED
30-
#endif
14+
void abort(void);
3115

3216
void errx(int eval, const char *fmt, ...)
3317
{
@@ -38,23 +22,13 @@ void errx(int eval, const char *fmt, ...)
3822

3923
/* FUNCTION: warn */
4024

41-
#ifndef __CPROVER_ERR_H_INCLUDED
42-
#include <err.h>
43-
#define __CPROVER_ERR_H_INCLUDED
44-
#endif
45-
4625
void warn(const char *fmt, ...)
4726
{
4827
(void)*fmt;
4928
}
5029

5130
/* FUNCTION: warnx */
5231

53-
#ifndef __CPROVER_ERR_H_INCLUDED
54-
#include <err.h>
55-
#define __CPROVER_ERR_H_INCLUDED
56-
#endif
57-
5832
void warnx(const char *fmt, ...)
5933
{
6034
(void)*fmt;

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

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,5 @@
11
/* FUNCTION: fcntl */
22

3-
#ifndef __CPROVER_FCNTL_H_INCLUDED
4-
#include <fcntl.h>
5-
#define __CPROVER_FCNTL_H_INCLUDED
6-
#endif
7-
83
int __VERIFIER_nondet_int();
94

105
int fcntl(int fd, int cmd, ...)

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

Lines changed: 9 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,16 @@
1+
#ifdef LIBRARY_CHECK
2+
#include <getopt.h>
3+
#endif
4+
15
/* FUNCTION: getopt */
26

37
extern char *optarg;
48
extern int optind;
59

6-
#ifndef __CPROVER_STRING_H_INCLUDED
7-
#include <string.h>
8-
#define __CPROVER_STRING_H_INCLUDED
9-
#endif
10+
__CPROVER_size_t strlen(const char *s);
1011

1112
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
12-
size_t __VERIFIER_nondet_size_t();
13+
__CPROVER_size_t __VERIFIER_nondet_size_t();
1314

1415
inline int getopt(
1516
int argc, char * const argv[], const char *optstring)
@@ -23,7 +24,7 @@ inline int getopt(
2324
if(optind>=argc || argv[optind][0]!='-')
2425
return -1;
2526

26-
size_t result_index=__VERIFIER_nondet_size_t();
27+
__CPROVER_size_t result_index = __VERIFIER_nondet_size_t();
2728
__CPROVER_assume(
2829
result_index<strlen(optstring) && optstring[result_index]!=':');
2930
#ifdef __CPROVER_STRING_ABSTRACTION
@@ -49,18 +50,15 @@ inline int getopt(
4950
++optind;
5051
}
5152
else
52-
optarg=NULL;
53+
optarg = 0;
5354
}
5455

5556
return result;
5657
}
5758

5859
/* FUNCTION: getopt_long */
5960

60-
#ifndef __CPROVER_GETOPT_H_INCLUDED
61-
#include <getopt.h>
62-
#define __CPROVER_GETOPT_H_INCLUDED
63-
#endif
61+
int getopt(int argc, char *const argv[], const char *optstring);
6462

6563
inline int getopt_long(
6664
int argc,

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

Lines changed: 18 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,17 @@
1-
/* FUNCTION: inet_addr */
2-
31
#ifndef _WIN32
4-
5-
#ifndef __CPROVER_INET_H_INCLUDED
2+
#ifdef LIBRARY_CHECK
63
#include <arpa/inet.h>
7-
#define __CPROVER_INET_H_INCLUDED
4+
#undef htonl
5+
#undef htons
6+
#undef ntohl
7+
#undef ntohs
8+
#endif
89
#endif
910

11+
/* FUNCTION: inet_addr */
12+
13+
#ifndef _WIN32
14+
1015
in_addr_t __VERIFIER_nondet_in_addr_t();
1116

1217
in_addr_t inet_addr(const char *cp)
@@ -28,11 +33,6 @@ in_addr_t inet_addr(const char *cp)
2833

2934
#ifndef _WIN32
3035

31-
#ifndef __CPROVER_INET_H_INCLUDED
32-
#include <arpa/inet.h>
33-
#define __CPROVER_INET_H_INCLUDED
34-
#endif
35-
3636
int __VERIFIER_nondet_int();
3737

3838
int inet_aton(const char *cp, struct in_addr *pin)
@@ -55,11 +55,6 @@ int inet_aton(const char *cp, struct in_addr *pin)
5555

5656
#ifndef _WIN32
5757

58-
#ifndef __CPROVER_INET_H_INCLUDED
59-
#include <arpa/inet.h>
60-
#define __CPROVER_INET_H_INCLUDED
61-
#endif
62-
6358
in_addr_t __VERIFIER_nondet_in_addr_t();
6459

6560
in_addr_t inet_network(const char *cp)
@@ -79,16 +74,9 @@ in_addr_t inet_network(const char *cp)
7974

8075
/* FUNCTION: htonl */
8176

82-
#ifndef __CPROVER_STDINT_H_INCLUDED
83-
#include <stdint.h>
84-
#define __CPROVER_STDINT_H_INCLUDED
85-
#endif
86-
87-
#undef htonl
88-
89-
uint32_t __builtin_bswap32(uint32_t);
77+
unsigned int __builtin_bswap32(unsigned int);
9078

91-
uint32_t htonl(uint32_t hostlong)
79+
unsigned int htonl(unsigned int hostlong)
9280
{
9381
#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
9482
return __builtin_bswap32(hostlong);
@@ -99,16 +87,9 @@ uint32_t htonl(uint32_t hostlong)
9987

10088
/* FUNCTION: htons */
10189

102-
#ifndef __CPROVER_STDINT_H_INCLUDED
103-
#include <stdint.h>
104-
#define __CPROVER_STDINT_H_INCLUDED
105-
#endif
106-
107-
#undef htons
108-
109-
uint16_t __builtin_bswap16(uint16_t);
90+
unsigned short __builtin_bswap16(unsigned short);
11091

111-
uint16_t htons(uint16_t hostshort)
92+
unsigned short htons(unsigned short hostshort)
11293
{
11394
#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
11495
return __builtin_bswap16(hostshort);
@@ -120,16 +101,9 @@ uint16_t htons(uint16_t hostshort)
120101

121102
/* FUNCTION: ntohl */
122103

123-
#ifndef __CPROVER_STDINT_H_INCLUDED
124-
#include <stdint.h>
125-
#define __CPROVER_STDINT_H_INCLUDED
126-
#endif
127-
128-
#undef ntohl
129-
130-
uint32_t __builtin_bswap32(uint32_t);
104+
unsigned int __builtin_bswap32(unsigned int);
131105

132-
uint32_t ntohl(uint32_t netlong)
106+
unsigned int ntohl(unsigned int netlong)
133107
{
134108
#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
135109
return __builtin_bswap32(netlong);
@@ -141,16 +115,9 @@ uint32_t ntohl(uint32_t netlong)
141115

142116
/* FUNCTION: ntohs */
143117

144-
#ifndef __CPROVER_STDINT_H_INCLUDED
145-
#include <stdint.h>
146-
#define __CPROVER_STDINT_H_INCLUDED
147-
#endif
148-
149-
#undef ntohs
150-
151-
uint16_t __builtin_bswap16(uint16_t);
118+
unsigned short __builtin_bswap16(unsigned short);
152119

153-
uint16_t ntohs(uint16_t netshort)
120+
unsigned short ntohs(unsigned short netshort)
154121
{
155122
#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
156123
return __builtin_bswap16(netshort);

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

Lines changed: 3 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,9 @@
1-
2-
/* FUNCTION: setlocale */
3-
4-
#ifndef __CPROVER_LOCALE_H_INCLUDED
1+
#ifdef LIBRARY_CHECK
52
#include <locale.h>
6-
#define __CPROVER_LOCALE_H_INCLUDED
73
#endif
84

5+
/* FUNCTION: setlocale */
6+
97
inline char *setlocale(int category, const char *locale)
108
{
119
__CPROVER_HIDE:;
@@ -24,11 +22,6 @@ inline char *setlocale(int category, const char *locale)
2422

2523
/* FUNCTION: localeconv */
2624

27-
#ifndef __CPROVER_LOCALE_H_INCLUDED
28-
#include <locale.h>
29-
#define __CPROVER_LOCALE_H_INCLUDED
30-
#endif
31-
3225
inline struct lconv *localeconv(void)
3326
{
3427
__CPROVER_HIDE:;

0 commit comments

Comments
 (0)