Skip to content

Commit 65d3c00

Browse files
tautschnigtautschnig
authored
Merge pull request #6901 from tautschnig/bugfixes/library-no-inline
Remove "inline" from library models [blocks: #6863]
2 parents 9975cd1 + 4057726 commit 65d3c00

File tree

27 files changed

+461
-312
lines changed

27 files changed

+461
-312
lines changed

‎regression/goto-analyzer/heap-allocation-nondet-1/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <stdlib.h>
12

23
int main()
34
{

‎regression/goto-analyzer/heap-allocation-nondet-2/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <stdlib.h>
12

23
int main()
34
{

‎regression/goto-analyzer/heap-allocation-nondet-3/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <stdlib.h>
12

23
int main()
34
{

‎regression/goto-analyzer/heap-allocation-nondet-4/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <stdlib.h>
12

23
int main()
34
{

‎regression/goto-analyzer/heap-allocation-nondet-5/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <stdlib.h>
12

23
int main()
34
{

‎regression/goto-analyzer/heap-allocation-nondet-6/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <stdlib.h>
12

23
int main()
34
{

‎regression/goto-analyzer/heap-allocation-write-2/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <stdlib.h>
12

23
int main()
34
{

‎regression/goto-analyzer/heap-allocation-write/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <stdlib.h>
12

23
int main()
34
{

‎regression/goto-analyzer/heap-allocation/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <stdlib.h>
12

23
int main()
34
{

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

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,47 +1,47 @@
11

22
/* FUNCTION: isalnum */
33

4-
inline int isalnum(int c)
4+
int isalnum(int c)
55
{ return (c>='a' && c<='z') || (c>='A' && c<='Z') || (c>='0' && c<='9'); }
66

77
/* FUNCTION: isalpha */
88

9-
inline int isalpha(int c)
9+
int isalpha(int c)
1010
{ return (c>='a' && c<='z') || (c>='A' && c<='Z'); }
1111

1212
/* FUNCTION: isblank */
1313

14-
inline int isblank(int c)
14+
int isblank(int c)
1515
{ return c==' ' || c=='\t'; }
1616

1717
/* FUNCTION: iscntrl */
1818

19-
inline int iscntrl(int c)
19+
int iscntrl(int c)
2020
{ return (c>=0 && c<='\037') || c=='\177'; }
2121

2222
/* FUNCTION: isdigit */
2323

24-
inline int isdigit(int c)
24+
int isdigit(int c)
2525
{ return c>='0' && c<='9'; }
2626

2727
/* FUNCTION: isgraph */
2828

29-
inline int isgraph(int c)
29+
int isgraph(int c)
3030
{ return c>='!' && c<='~'; }
3131

3232
/* FUNCTION: islower */
3333

34-
inline int islower(int c)
34+
int islower(int c)
3535
{ return c>='a' && c<='z'; }
3636

3737
/* FUNCTION: isprint */
3838

39-
inline int isprint(int c)
39+
int isprint(int c)
4040
{ return c>=' ' && c<='~'; }
4141

4242
/* FUNCTION: ispunct */
4343

44-
inline int ispunct(int c)
44+
int ispunct(int c)
4545
{ return c=='!' ||
4646
c=='"' ||
4747
c=='#' ||
@@ -77,7 +77,7 @@ inline int ispunct(int c)
7777

7878
/* FUNCTION: isspace */
7979

80-
inline int isspace(int c)
80+
int isspace(int c)
8181
{ return c=='\t' ||
8282
c=='\n' ||
8383
c=='\v' ||
@@ -87,20 +87,20 @@ inline int isspace(int c)
8787

8888
/* FUNCTION: isupper */
8989

90-
inline int isupper(int c)
90+
int isupper(int c)
9191
{ return c>='A' && c<='Z'; }
9292

9393
/* FUNCTION: isxdigit */
9494

95-
inline int isxdigit(int c)
95+
int isxdigit(int c)
9696
{ return (c>='A' && c<='F') || (c>='a' && c<='f') || (c>='0' && c<='9'); }
9797

9898
/* FUNCTION: tolower */
9999

100-
inline int tolower(int c)
100+
int tolower(int c)
101101
{ return (c>='A' && c<='Z')?c+('a'-'A'):c; }
102102

103103
/* FUNCTION: toupper */
104104

105-
inline int toupper(int c)
105+
int toupper(int c)
106106
{ return (c>='a' && c<='z')?c-('a'-'A'):c; }

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55

66
__CPROVER_thread_local int __CPROVER_errno;
77

8-
inline int * __error(void)
8+
int *__error(void)
99
{
1010
return &__CPROVER_errno;
1111
}
@@ -17,7 +17,7 @@ inline int * __error(void)
1717

1818
__CPROVER_thread_local int __CPROVER_errno;
1919

20-
inline int *__errno_location(void)
20+
int *__errno_location(void)
2121
{
2222
return &__CPROVER_errno;
2323
}
@@ -29,7 +29,7 @@ inline int *__errno_location(void)
2929

3030
__CPROVER_thread_local int __CPROVER_errno;
3131

32-
inline int *_errno(void)
32+
int *_errno(void)
3333
{
3434
return &__CPROVER_errno;
3535
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44

55
extern int __CPROVER_rounding_mode;
66

7-
inline int fegetround(void)
7+
int fegetround(void)
88
{
99
__CPROVER_HIDE:;
1010
// CPROVER uses the x86 numbering of the rounding modes
@@ -24,7 +24,7 @@ __CPROVER_HIDE:;
2424

2525
#include <fenv.h>
2626

27-
inline int fesetround(int rounding_mode)
27+
int fesetround(int rounding_mode)
2828
{
2929
__CPROVER_HIDE:;
3030
// CPROVER uses the x86 numbering of the rounding modes

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ unsigned int _controlfp(
2626

2727
__CPROVER_thread_local unsigned __CPROVER_fpu_control_word;
2828

29-
inline unsigned int _status87(void)
29+
unsigned int _status87(void)
3030
{
3131
return __CPROVER_fpu_control_word;
3232
}
@@ -39,7 +39,7 @@ inline unsigned int _status87(void)
3939

4040
__CPROVER_thread_local unsigned __CPROVER_fpu_control_word;
4141

42-
inline unsigned int _statusfp(void)
42+
unsigned int _statusfp(void)
4343
{
4444
return __CPROVER_fpu_control_word;
4545
}
@@ -52,7 +52,7 @@ inline unsigned int _statusfp(void)
5252

5353
__CPROVER_thread_local unsigned __CPROVER_fpu_control_word;
5454

55-
inline void _statusfp2(unsigned int *px86, unsigned int *pSSE2)
55+
void _statusfp2(unsigned int *px86, unsigned int *pSSE2)
5656
{
5757
unsigned SSE2_status;
5858
*px86=__CPROVER_fpu_control_word;
@@ -63,7 +63,7 @@ inline void _statusfp2(unsigned int *px86, unsigned int *pSSE2)
6363

6464
/* FUNCTION: _isnan */
6565

66-
inline int _isnan(double x)
66+
int _isnan(double x)
6767
{
6868
return __CPROVER_isnand(x);
6969
}
@@ -72,7 +72,7 @@ inline int _isnan(double x)
7272

7373
extern int __CPROVER_rounding_mode;
7474

75-
inline int __builtin_flt_rounds(void)
75+
int __builtin_flt_rounds(void)
7676
{
7777
// This is a clang builtin for FLT_ROUNDS
7878
// The magic numbers are C99 and different from the
@@ -88,7 +88,7 @@ inline int __builtin_flt_rounds(void)
8888

8989
int __builtin_flt_rounds(void);
9090

91-
inline int __flt_rounds(void)
91+
int __flt_rounds(void)
9292
{
9393
// Spotted on FreeBSD
9494
return __builtin_flt_rounds();

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

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,27 @@
11
/* FUNCTION: __builtin_ia32_sfence */
22

3-
inline void __builtin_ia32_sfence(void)
3+
void __builtin_ia32_sfence(void)
44
{
55
__asm("sfence");
66
}
77

88
/* FUNCTION: __builtin_ia32_lfence */
99

10-
inline void __builtin_ia32_lfence(void)
10+
void __builtin_ia32_lfence(void)
1111
{
1212
__asm("lfence");
1313
}
1414

1515
/* FUNCTION: __builtin_ia32_mfence */
1616

17-
inline void __builtin_ia32_mfence(void)
17+
void __builtin_ia32_mfence(void)
1818
{
1919
__asm("mfence");
2020
}
2121

2222
/* FUNCTION: __sync_synchronize */
2323

24-
inline void __sync_synchronize(void)
24+
void __sync_synchronize(void)
2525
{
2626
// WARNING: this was a NOP before gcc 4.3.1,
2727
// but is now believed to be the strongest possible barrier.
@@ -37,7 +37,7 @@ inline void __sync_synchronize(void)
3737

3838
int __builtin_clz(unsigned int x);
3939

40-
inline int __builtin_ffs(int x)
40+
int __builtin_ffs(int x)
4141
{
4242
if(x == 0)
4343
return 0;
@@ -54,7 +54,7 @@ inline int __builtin_ffs(int x)
5454

5555
int __builtin_clzl(unsigned long x);
5656

57-
inline int __builtin_ffsl(long x)
57+
int __builtin_ffsl(long x)
5858
{
5959
if(x == 0)
6060
return 0;
@@ -71,7 +71,7 @@ inline int __builtin_ffsl(long x)
7171

7272
int __builtin_clzll(unsigned long long x);
7373

74-
inline int __builtin_ffsll(long long x)
74+
int __builtin_ffsll(long long x)
7575
{
7676
if(x == 0)
7777
return 0;
@@ -88,7 +88,7 @@ inline int __builtin_ffsll(long long x)
8888

8989
void __atomic_thread_fence(int memorder);
9090

91-
inline _Bool __atomic_test_and_set(void *ptr, int memorder)
91+
_Bool __atomic_test_and_set(void *ptr, int memorder)
9292
{
9393
__CPROVER_HIDE:;
9494
__CPROVER_atomic_begin();
@@ -103,7 +103,7 @@ __CPROVER_HIDE:;
103103

104104
void __atomic_thread_fence(int memorder);
105105

106-
inline void __atomic_clear(_Bool *ptr, int memorder)
106+
void __atomic_clear(_Bool *ptr, int memorder)
107107
{
108108
__CPROVER_HIDE:;
109109
__CPROVER_atomic_begin();
@@ -145,7 +145,7 @@ __CPROVER_HIDE:;
145145
# define __ATOMIC_SEQ_CST 5
146146
#endif
147147

148-
inline void __atomic_thread_fence(int memorder)
148+
void __atomic_thread_fence(int memorder)
149149
{
150150
__CPROVER_HIDE:;
151151
if(memorder == __ATOMIC_CONSUME || memorder == __ATOMIC_ACQUIRE)
@@ -168,15 +168,15 @@ __CPROVER_HIDE:;
168168

169169
void __atomic_thread_fence(int memorder);
170170

171-
inline void __atomic_signal_fence(int memorder)
171+
void __atomic_signal_fence(int memorder)
172172
{
173173
__CPROVER_HIDE:;
174174
__atomic_thread_fence(memorder);
175175
}
176176

177177
/* FUNCTION: __atomic_always_lock_free */
178178

179-
inline _Bool __atomic_always_lock_free(__CPROVER_size_t size, void *ptr)
179+
_Bool __atomic_always_lock_free(__CPROVER_size_t size, void *ptr)
180180
{
181181
__CPROVER_HIDE:;
182182
(void)ptr;
@@ -185,7 +185,7 @@ __CPROVER_HIDE:;
185185

186186
/* FUNCTION: __atomic_is_lock_free */
187187

188-
inline _Bool __atomic_is_lock_free(__CPROVER_size_t size, void *ptr)
188+
_Bool __atomic_is_lock_free(__CPROVER_size_t size, void *ptr)
189189
{
190190
__CPROVER_HIDE:;
191191
(void)ptr;

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,7 @@ extern int optind;
1111
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
1212
size_t __VERIFIER_nondet_size_t();
1313

14-
inline int getopt(
15-
int argc, char * const argv[], const char *optstring)
14+
int getopt(int argc, char *const argv[], const char *optstring)
1615
{
1716
__CPROVER_HIDE:;
1817
int result=-1;
@@ -62,9 +61,9 @@ inline int getopt(
6261
#define __CPROVER_GETOPT_H_INCLUDED
6362
#endif
6463

65-
inline int getopt_long(
64+
int getopt_long(
6665
int argc,
67-
char * const argv[],
66+
char *const argv[],
6867
const char *optstring,
6968
const struct option *longopts,
7069
int *longindex)

0 commit comments

Comments
 (0)