Skip to content

Commit 6064cb6

Browse files
tautschnigtautschnig
committed
Remove "inline" from library models
It nowadays has no effect for we don't do partial inlining by default anymore. It does, however, trip up the library check on Ubuntu 22.04 as fopen, fclose, fdopen are marked with attribute "noinline" in the system library. The only exception is goto-analyzer, which still does partial inlining. Therefore, keep "malloc" marked "inline" to ensure the analyses do not need to track allocations across functions. The full fix, however, is for goto-analyzer to selectively do inlining.
1 parent 4e36973 commit 6064cb6

File tree

18 files changed

+266
-264
lines changed

18 files changed

+266
-264
lines changed

‎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: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ extern int optind;
1111
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
1212
size_t __VERIFIER_nondet_size_t();
1313

14-
inline int getopt(
14+
int getopt(
1515
int argc, char * const argv[], const char *optstring)
1616
{
1717
__CPROVER_HIDE:;
@@ -62,7 +62,7 @@ inline int getopt(
6262
#define __CPROVER_GETOPT_H_INCLUDED
6363
#endif
6464

65-
inline int getopt_long(
65+
int getopt_long(
6666
int argc,
6767
char * const argv[],
6868
const char *optstring,

0 commit comments

Comments
 (0)