From 3b3d8c4144d9679ec8ac29430210a60f6846476b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 2 Jun 2022 09:07:46 +0000 Subject: [PATCH 1/4] goto-analyzer regression tests: declare malloc Avoid unnecessary warnings about malloc not being declared. The resulting type conflict may also trip up the analysis, and is only worked around by inlining calls to malloc. --- regression/goto-analyzer/heap-allocation-nondet-1/main.c | 1 + regression/goto-analyzer/heap-allocation-nondet-2/main.c | 1 + regression/goto-analyzer/heap-allocation-nondet-3/main.c | 1 + regression/goto-analyzer/heap-allocation-nondet-4/main.c | 1 + regression/goto-analyzer/heap-allocation-nondet-5/main.c | 1 + regression/goto-analyzer/heap-allocation-nondet-6/main.c | 1 + regression/goto-analyzer/heap-allocation-write-2/main.c | 1 + regression/goto-analyzer/heap-allocation-write/main.c | 1 + regression/goto-analyzer/heap-allocation/main.c | 1 + 9 files changed, 9 insertions(+) diff --git a/regression/goto-analyzer/heap-allocation-nondet-1/main.c b/regression/goto-analyzer/heap-allocation-nondet-1/main.c index e022d770c6e..39c49fd3e5f 100644 --- a/regression/goto-analyzer/heap-allocation-nondet-1/main.c +++ b/regression/goto-analyzer/heap-allocation-nondet-1/main.c @@ -1,3 +1,4 @@ +#include int main() { diff --git a/regression/goto-analyzer/heap-allocation-nondet-2/main.c b/regression/goto-analyzer/heap-allocation-nondet-2/main.c index 84ef19235fe..7fc257fc51e 100644 --- a/regression/goto-analyzer/heap-allocation-nondet-2/main.c +++ b/regression/goto-analyzer/heap-allocation-nondet-2/main.c @@ -1,3 +1,4 @@ +#include int main() { diff --git a/regression/goto-analyzer/heap-allocation-nondet-3/main.c b/regression/goto-analyzer/heap-allocation-nondet-3/main.c index d49b7ec72b7..77bd433bb93 100644 --- a/regression/goto-analyzer/heap-allocation-nondet-3/main.c +++ b/regression/goto-analyzer/heap-allocation-nondet-3/main.c @@ -1,3 +1,4 @@ +#include int main() { diff --git a/regression/goto-analyzer/heap-allocation-nondet-4/main.c b/regression/goto-analyzer/heap-allocation-nondet-4/main.c index 7870ce77aa5..92297746fed 100644 --- a/regression/goto-analyzer/heap-allocation-nondet-4/main.c +++ b/regression/goto-analyzer/heap-allocation-nondet-4/main.c @@ -1,3 +1,4 @@ +#include int main() { diff --git a/regression/goto-analyzer/heap-allocation-nondet-5/main.c b/regression/goto-analyzer/heap-allocation-nondet-5/main.c index faa8283feff..fb3bd9c97e2 100644 --- a/regression/goto-analyzer/heap-allocation-nondet-5/main.c +++ b/regression/goto-analyzer/heap-allocation-nondet-5/main.c @@ -1,3 +1,4 @@ +#include int main() { diff --git a/regression/goto-analyzer/heap-allocation-nondet-6/main.c b/regression/goto-analyzer/heap-allocation-nondet-6/main.c index 8dabb4a1132..9f7dda347ef 100644 --- a/regression/goto-analyzer/heap-allocation-nondet-6/main.c +++ b/regression/goto-analyzer/heap-allocation-nondet-6/main.c @@ -1,3 +1,4 @@ +#include int main() { diff --git a/regression/goto-analyzer/heap-allocation-write-2/main.c b/regression/goto-analyzer/heap-allocation-write-2/main.c index 020067294d8..2d63500ffd5 100644 --- a/regression/goto-analyzer/heap-allocation-write-2/main.c +++ b/regression/goto-analyzer/heap-allocation-write-2/main.c @@ -1,3 +1,4 @@ +#include int main() { diff --git a/regression/goto-analyzer/heap-allocation-write/main.c b/regression/goto-analyzer/heap-allocation-write/main.c index 6019ab2f1d7..1e666f099e2 100644 --- a/regression/goto-analyzer/heap-allocation-write/main.c +++ b/regression/goto-analyzer/heap-allocation-write/main.c @@ -1,3 +1,4 @@ +#include int main() { diff --git a/regression/goto-analyzer/heap-allocation/main.c b/regression/goto-analyzer/heap-allocation/main.c index c09abc337b8..6c50b5d00f9 100644 --- a/regression/goto-analyzer/heap-allocation/main.c +++ b/regression/goto-analyzer/heap-allocation/main.c @@ -1,3 +1,4 @@ +#include int main() { From 4e3697334990fca60cf8f56fd366b691d9f61991 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 3 Jun 2022 21:35:01 +0000 Subject: [PATCH 2/4] Fix duplicate _mm_subs_epi16 Instead, add the missing _mm_adds_epu16. --- src/ansi-c/library/intrin.c | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/ansi-c/library/intrin.c b/src/ansi-c/library/intrin.c index fed5b57ed2c..96ddabebaa6 100644 --- a/src/ansi-c/library/intrin.c +++ b/src/ansi-c/library/intrin.c @@ -533,7 +533,7 @@ inline __m128i _mm_subs_epi16(__m128i a, __m128i b) } #endif -/* FUNCTION: _mm_subs_epi16 */ +/* FUNCTION: _mm_adds_epu16 */ #ifdef _MSC_VER # ifndef __CPROVER_INTRIN_H_INCLUDED @@ -541,18 +541,18 @@ inline __m128i _mm_subs_epi16(__m128i a, __m128i b) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline __m128i _mm_subs_epi16(__m128i a, __m128i b) +inline __m128i _mm_adds_epu16(__m128i a, __m128i b) { return (__m128i){ .m128i_i16 = { - __CPROVER_saturating_minus(a.m128i_i16[0], b.m128i_i16[0]), - __CPROVER_saturating_minus(a.m128i_i16[1], b.m128i_i16[1]), - __CPROVER_saturating_minus(a.m128i_i16[2], b.m128i_i16[2]), - __CPROVER_saturating_minus(a.m128i_i16[3], b.m128i_i16[3]), - __CPROVER_saturating_minus(a.m128i_i16[4], b.m128i_i16[4]), - __CPROVER_saturating_minus(a.m128i_i16[5], b.m128i_i16[5]), - __CPROVER_saturating_minus(a.m128i_i16[6], b.m128i_i16[6]), - __CPROVER_saturating_minus(a.m128i_i16[7], b.m128i_i16[7]), + __CPROVER_saturating_plus(a.m128i_u16[0], b.m128i_u16[0]), + __CPROVER_saturating_plus(a.m128i_u16[1], b.m128i_u16[1]), + __CPROVER_saturating_plus(a.m128i_u16[2], b.m128i_u16[2]), + __CPROVER_saturating_plus(a.m128i_u16[3], b.m128i_u16[3]), + __CPROVER_saturating_plus(a.m128i_u16[4], b.m128i_u16[4]), + __CPROVER_saturating_plus(a.m128i_u16[5], b.m128i_u16[5]), + __CPROVER_saturating_plus(a.m128i_u16[6], b.m128i_u16[6]), + __CPROVER_saturating_plus(a.m128i_u16[7], b.m128i_u16[7]), }}; } #endif From 6064cb60a212da70e6d5e88b5bbfc39c80f2d0af Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 1 Jun 2022 09:20:17 +0000 Subject: [PATCH 3/4] 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. --- src/ansi-c/library/ctype.c | 28 ++++----- src/ansi-c/library/errno.c | 6 +- src/ansi-c/library/fenv.c | 4 +- src/ansi-c/library/float.c | 12 ++-- src/ansi-c/library/gcc.c | 26 ++++----- src/ansi-c/library/getopt.c | 4 +- src/ansi-c/library/intrin.c | 86 ++++++++++++++-------------- src/ansi-c/library/locale.c | 4 +- src/ansi-c/library/math.c | 92 +++++++++++++++--------------- src/ansi-c/library/pthread_lib.c | 66 ++++++++++----------- src/ansi-c/library/semaphore.c | 16 +++--- src/ansi-c/library/setjmp.c | 14 ++--- src/ansi-c/library/stdio.c | 68 +++++++++++----------- src/ansi-c/library/stdlib.c | 50 ++++++++-------- src/ansi-c/library/string.c | 30 +++++----- src/ansi-c/library/unistd.c | 8 +-- src/ansi-c/library/windows.c | 4 +- src/ansi-c/library/x86_assembler.c | 12 ++-- 18 files changed, 266 insertions(+), 264 deletions(-) diff --git a/src/ansi-c/library/ctype.c b/src/ansi-c/library/ctype.c index ac13bd9c07a..e7bfb4461ad 100644 --- a/src/ansi-c/library/ctype.c +++ b/src/ansi-c/library/ctype.c @@ -1,47 +1,47 @@ /* FUNCTION: isalnum */ -inline int isalnum(int c) +int isalnum(int c) { return (c>='a' && c<='z') || (c>='A' && c<='Z') || (c>='0' && c<='9'); } /* FUNCTION: isalpha */ -inline int isalpha(int c) +int isalpha(int c) { return (c>='a' && c<='z') || (c>='A' && c<='Z'); } /* FUNCTION: isblank */ -inline int isblank(int c) +int isblank(int c) { return c==' ' || c=='\t'; } /* FUNCTION: iscntrl */ -inline int iscntrl(int c) +int iscntrl(int c) { return (c>=0 && c<='\037') || c=='\177'; } /* FUNCTION: isdigit */ -inline int isdigit(int c) +int isdigit(int c) { return c>='0' && c<='9'; } /* FUNCTION: isgraph */ -inline int isgraph(int c) +int isgraph(int c) { return c>='!' && c<='~'; } /* FUNCTION: islower */ -inline int islower(int c) +int islower(int c) { return c>='a' && c<='z'; } /* FUNCTION: isprint */ -inline int isprint(int c) +int isprint(int c) { return c>=' ' && c<='~'; } /* FUNCTION: ispunct */ -inline int ispunct(int c) +int ispunct(int c) { return c=='!' || c=='"' || c=='#' || @@ -77,7 +77,7 @@ inline int ispunct(int c) /* FUNCTION: isspace */ -inline int isspace(int c) +int isspace(int c) { return c=='\t' || c=='\n' || c=='\v' || @@ -87,20 +87,20 @@ inline int isspace(int c) /* FUNCTION: isupper */ -inline int isupper(int c) +int isupper(int c) { return c>='A' && c<='Z'; } /* FUNCTION: isxdigit */ -inline int isxdigit(int c) +int isxdigit(int c) { return (c>='A' && c<='F') || (c>='a' && c<='f') || (c>='0' && c<='9'); } /* FUNCTION: tolower */ -inline int tolower(int c) +int tolower(int c) { return (c>='A' && c<='Z')?c+('a'-'A'):c; } /* FUNCTION: toupper */ -inline int toupper(int c) +int toupper(int c) { return (c>='a' && c<='z')?c-('a'-'A'):c; } diff --git a/src/ansi-c/library/errno.c b/src/ansi-c/library/errno.c index e19ac3a6d1b..341465129b7 100644 --- a/src/ansi-c/library/errno.c +++ b/src/ansi-c/library/errno.c @@ -5,7 +5,7 @@ __CPROVER_thread_local int __CPROVER_errno; -inline int * __error(void) +int * __error(void) { return &__CPROVER_errno; } @@ -17,7 +17,7 @@ inline int * __error(void) __CPROVER_thread_local int __CPROVER_errno; -inline int *__errno_location(void) +int *__errno_location(void) { return &__CPROVER_errno; } @@ -29,7 +29,7 @@ inline int *__errno_location(void) __CPROVER_thread_local int __CPROVER_errno; -inline int *_errno(void) +int *_errno(void) { return &__CPROVER_errno; } diff --git a/src/ansi-c/library/fenv.c b/src/ansi-c/library/fenv.c index 6c9eb388653..31e17d615d2 100644 --- a/src/ansi-c/library/fenv.c +++ b/src/ansi-c/library/fenv.c @@ -4,7 +4,7 @@ extern int __CPROVER_rounding_mode; -inline int fegetround(void) +int fegetround(void) { __CPROVER_HIDE:; // CPROVER uses the x86 numbering of the rounding modes @@ -24,7 +24,7 @@ __CPROVER_HIDE:; #include -inline int fesetround(int rounding_mode) +int fesetround(int rounding_mode) { __CPROVER_HIDE:; // CPROVER uses the x86 numbering of the rounding modes diff --git a/src/ansi-c/library/float.c b/src/ansi-c/library/float.c index a2ba36e4daa..a3b14577159 100644 --- a/src/ansi-c/library/float.c +++ b/src/ansi-c/library/float.c @@ -26,7 +26,7 @@ unsigned int _controlfp( __CPROVER_thread_local unsigned __CPROVER_fpu_control_word; -inline unsigned int _status87(void) +unsigned int _status87(void) { return __CPROVER_fpu_control_word; } @@ -39,7 +39,7 @@ inline unsigned int _status87(void) __CPROVER_thread_local unsigned __CPROVER_fpu_control_word; -inline unsigned int _statusfp(void) +unsigned int _statusfp(void) { return __CPROVER_fpu_control_word; } @@ -52,7 +52,7 @@ inline unsigned int _statusfp(void) __CPROVER_thread_local unsigned __CPROVER_fpu_control_word; -inline void _statusfp2(unsigned int *px86, unsigned int *pSSE2) +void _statusfp2(unsigned int *px86, unsigned int *pSSE2) { unsigned SSE2_status; *px86=__CPROVER_fpu_control_word; @@ -63,7 +63,7 @@ inline void _statusfp2(unsigned int *px86, unsigned int *pSSE2) /* FUNCTION: _isnan */ -inline int _isnan(double x) +int _isnan(double x) { return __CPROVER_isnand(x); } @@ -72,7 +72,7 @@ inline int _isnan(double x) extern int __CPROVER_rounding_mode; -inline int __builtin_flt_rounds(void) +int __builtin_flt_rounds(void) { // This is a clang builtin for FLT_ROUNDS // The magic numbers are C99 and different from the @@ -88,7 +88,7 @@ inline int __builtin_flt_rounds(void) int __builtin_flt_rounds(void); -inline int __flt_rounds(void) +int __flt_rounds(void) { // Spotted on FreeBSD return __builtin_flt_rounds(); diff --git a/src/ansi-c/library/gcc.c b/src/ansi-c/library/gcc.c index ee5f8b17d93..79ac7fda79e 100644 --- a/src/ansi-c/library/gcc.c +++ b/src/ansi-c/library/gcc.c @@ -1,27 +1,27 @@ /* FUNCTION: __builtin_ia32_sfence */ -inline void __builtin_ia32_sfence(void) +void __builtin_ia32_sfence(void) { __asm("sfence"); } /* FUNCTION: __builtin_ia32_lfence */ -inline void __builtin_ia32_lfence(void) +void __builtin_ia32_lfence(void) { __asm("lfence"); } /* FUNCTION: __builtin_ia32_mfence */ -inline void __builtin_ia32_mfence(void) +void __builtin_ia32_mfence(void) { __asm("mfence"); } /* FUNCTION: __sync_synchronize */ -inline void __sync_synchronize(void) +void __sync_synchronize(void) { // WARNING: this was a NOP before gcc 4.3.1, // but is now believed to be the strongest possible barrier. @@ -37,7 +37,7 @@ inline void __sync_synchronize(void) int __builtin_clz(unsigned int x); -inline int __builtin_ffs(int x) +int __builtin_ffs(int x) { if(x == 0) return 0; @@ -54,7 +54,7 @@ inline int __builtin_ffs(int x) int __builtin_clzl(unsigned long x); -inline int __builtin_ffsl(long x) +int __builtin_ffsl(long x) { if(x == 0) return 0; @@ -71,7 +71,7 @@ inline int __builtin_ffsl(long x) int __builtin_clzll(unsigned long long x); -inline int __builtin_ffsll(long long x) +int __builtin_ffsll(long long x) { if(x == 0) return 0; @@ -88,7 +88,7 @@ inline int __builtin_ffsll(long long x) void __atomic_thread_fence(int memorder); -inline _Bool __atomic_test_and_set(void *ptr, int memorder) +_Bool __atomic_test_and_set(void *ptr, int memorder) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -103,7 +103,7 @@ __CPROVER_HIDE:; void __atomic_thread_fence(int memorder); -inline void __atomic_clear(_Bool *ptr, int memorder) +void __atomic_clear(_Bool *ptr, int memorder) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -145,7 +145,7 @@ __CPROVER_HIDE:; # define __ATOMIC_SEQ_CST 5 #endif -inline void __atomic_thread_fence(int memorder) +void __atomic_thread_fence(int memorder) { __CPROVER_HIDE:; if(memorder == __ATOMIC_CONSUME || memorder == __ATOMIC_ACQUIRE) @@ -168,7 +168,7 @@ __CPROVER_HIDE:; void __atomic_thread_fence(int memorder); -inline void __atomic_signal_fence(int memorder) +void __atomic_signal_fence(int memorder) { __CPROVER_HIDE:; __atomic_thread_fence(memorder); @@ -176,7 +176,7 @@ __CPROVER_HIDE:; /* FUNCTION: __atomic_always_lock_free */ -inline _Bool __atomic_always_lock_free(__CPROVER_size_t size, void *ptr) +_Bool __atomic_always_lock_free(__CPROVER_size_t size, void *ptr) { __CPROVER_HIDE:; (void)ptr; @@ -185,7 +185,7 @@ __CPROVER_HIDE:; /* FUNCTION: __atomic_is_lock_free */ -inline _Bool __atomic_is_lock_free(__CPROVER_size_t size, void *ptr) +_Bool __atomic_is_lock_free(__CPROVER_size_t size, void *ptr) { __CPROVER_HIDE:; (void)ptr; diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c index 0045cbd105d..45ceeae9e7b 100644 --- a/src/ansi-c/library/getopt.c +++ b/src/ansi-c/library/getopt.c @@ -11,7 +11,7 @@ extern int optind; __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); size_t __VERIFIER_nondet_size_t(); -inline int getopt( +int getopt( int argc, char * const argv[], const char *optstring) { __CPROVER_HIDE:; @@ -62,7 +62,7 @@ inline int getopt( #define __CPROVER_GETOPT_H_INCLUDED #endif -inline int getopt_long( +int getopt_long( int argc, char * const argv[], const char *optstring, diff --git a/src/ansi-c/library/intrin.c b/src/ansi-c/library/intrin.c index 96ddabebaa6..5665dce4084 100644 --- a/src/ansi-c/library/intrin.c +++ b/src/ansi-c/library/intrin.c @@ -2,7 +2,7 @@ /* FUNCTION: _InterlockedDecrement */ -inline long _InterlockedDecrement(long volatile *p) +long _InterlockedDecrement(long volatile *p) { __CPROVER_HIDE:; // This function generates a full memory barrier (or fence) to ensure that @@ -16,7 +16,7 @@ inline long _InterlockedDecrement(long volatile *p) /* FUNCTION: _InterlockedExchange */ -inline long _InterlockedExchange(long volatile *p, long v) +long _InterlockedExchange(long volatile *p, long v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -28,7 +28,7 @@ inline long _InterlockedExchange(long volatile *p, long v) /* FUNCTION: _InterlockedExchange16 */ -inline short _InterlockedExchange16(short volatile *p, short v) +short _InterlockedExchange16(short volatile *p, short v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -40,7 +40,7 @@ inline short _InterlockedExchange16(short volatile *p, short v) /* FUNCTION: _InterlockedExchange8 */ -inline char _InterlockedExchange8(char volatile *p, char v) +char _InterlockedExchange8(char volatile *p, char v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -52,7 +52,7 @@ inline char _InterlockedExchange8(char volatile *p, char v) /* FUNCTION: _InterlockedExchangeAdd */ -inline long _InterlockedExchangeAdd(long volatile *p, long v) +long _InterlockedExchangeAdd(long volatile *p, long v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -64,7 +64,7 @@ inline long _InterlockedExchangeAdd(long volatile *p, long v) /* FUNCTION: _InterlockedExchangeAdd16 */ -inline short _InterlockedExchangeAdd16(short volatile *p, short v) +short _InterlockedExchangeAdd16(short volatile *p, short v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -76,7 +76,7 @@ inline short _InterlockedExchangeAdd16(short volatile *p, short v) /* FUNCTION: _InterlockedExchangeAdd8 */ -inline char _InterlockedExchangeAdd8(char volatile *p, char v) +char _InterlockedExchangeAdd8(char volatile *p, char v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -88,7 +88,7 @@ inline char _InterlockedExchangeAdd8(char volatile *p, char v) /* FUNCTION: _InterlockedCompareExchange */ -inline long _InterlockedCompareExchange(long volatile *p, long v1, long v2) +long _InterlockedCompareExchange(long volatile *p, long v1, long v2) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -101,7 +101,7 @@ inline long _InterlockedCompareExchange(long volatile *p, long v1, long v2) /* FUNCTION: _InterlockedCompareExchange64 */ -inline long long _InterlockedCompareExchange64(long long volatile *p, long long v1, long long v2) +long long _InterlockedCompareExchange64(long long volatile *p, long long v1, long long v2) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -114,7 +114,7 @@ inline long long _InterlockedCompareExchange64(long long volatile *p, long long /* FUNCTION: __InterlockedIncrement */ -inline long _InterlockedIncrement(long volatile *p) +long _InterlockedIncrement(long volatile *p) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -126,7 +126,7 @@ inline long _InterlockedIncrement(long volatile *p) /* FUNCTION: _InterlockedOr */ -inline long _InterlockedOr(long volatile *p, long v) +long _InterlockedOr(long volatile *p, long v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -138,7 +138,7 @@ inline long _InterlockedOr(long volatile *p, long v) /* FUNCTION: _InterlockedOr8 */ -inline char _InterlockedOr8(char volatile *p, char v) +char _InterlockedOr8(char volatile *p, char v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -150,7 +150,7 @@ inline char _InterlockedOr8(char volatile *p, char v) /* FUNCTION: _InterlockedOr16 */ -inline short _InterlockedOr16(short volatile *p, short v) +short _InterlockedOr16(short volatile *p, short v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -162,7 +162,7 @@ inline short _InterlockedOr16(short volatile *p, short v) /* FUNCTION: _InterlockedXor */ -inline long _InterlockedXor(long volatile *p, long v) +long _InterlockedXor(long volatile *p, long v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -174,7 +174,7 @@ inline long _InterlockedXor(long volatile *p, long v) /* FUNCTION: _InterlockedXor8 */ -inline char _InterlockedXor8(char volatile *p, char v) +char _InterlockedXor8(char volatile *p, char v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -186,7 +186,7 @@ inline char _InterlockedXor8(char volatile *p, char v) /* FUNCTION: _InterlockedXor16 */ -inline short _InterlockedXor16(short volatile *p, short v) +short _InterlockedXor16(short volatile *p, short v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -198,7 +198,7 @@ inline short _InterlockedXor16(short volatile *p, short v) /* FUNCTION: _InterlockedAnd */ -inline long _InterlockedAnd(long volatile *p, long v) +long _InterlockedAnd(long volatile *p, long v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -210,7 +210,7 @@ inline long _InterlockedAnd(long volatile *p, long v) /* FUNCTION: _InterlockedAnd8 */ -inline char _InterlockedAnd8(char volatile *p, char v) +char _InterlockedAnd8(char volatile *p, char v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -222,7 +222,7 @@ inline char _InterlockedAnd8(char volatile *p, char v) /* FUNCTION: _InterlockedAnd16 */ -inline short _InterlockedAnd16(short volatile *p, short v) +short _InterlockedAnd16(short volatile *p, short v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -234,7 +234,7 @@ inline short _InterlockedAnd16(short volatile *p, short v) /* FUNCTION: _InterlockedAdd */ -inline long _InterlockedAdd(long volatile *p, long v) +long _InterlockedAdd(long volatile *p, long v) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -246,7 +246,7 @@ inline long _InterlockedAdd(long volatile *p, long v) /* FUNCTION: _InterlockedAddLargeStatistic */ -inline long _InterlockedAddLargeStatistic(long long volatile *p, long v) +long _InterlockedAddLargeStatistic(long long volatile *p, long v) { __CPROVER_HIDE:; // not atomic: @@ -258,14 +258,14 @@ inline long _InterlockedAddLargeStatistic(long long volatile *p, long v) /* FUNCTION: _mm_lfence */ -inline void _mm_lfence(void) +void _mm_lfence(void) { __CPROVER_HIDE:; } /* FUNCTION: _mm_mfence */ -inline void _mm_mfence(void) +void _mm_mfence(void) { __CPROVER_HIDE:; __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence"); @@ -273,14 +273,14 @@ inline void _mm_mfence(void) /* FUNCTION: _WriteBarrier */ -inline void _WriteBarrier(void) +void _WriteBarrier(void) { __CPROVER_HIDE:; } /* FUNCTION: _ReadWriteBarrier */ -inline void _ReadWriteBarrier(void) +void _ReadWriteBarrier(void) { __CPROVER_HIDE:; __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence"); @@ -288,14 +288,14 @@ inline void _ReadWriteBarrier(void) /* FUNCTION: _ReadBarrier */ -inline void _ReadBarrier(void) +void _ReadBarrier(void) { __CPROVER_HIDE:; } /* FUNCTION: _InterlockedIncrement16 */ -inline short _InterlockedIncrement16(short volatile *p) +short _InterlockedIncrement16(short volatile *p) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -307,7 +307,7 @@ inline short _InterlockedIncrement16(short volatile *p) /* FUNCTION: _InterlockedDecrement16 */ -inline short _InterlockedDecrement16(short volatile *p) +short _InterlockedDecrement16(short volatile *p) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -319,7 +319,7 @@ inline short _InterlockedDecrement16(short volatile *p) /* FUNCTION: _InterlockedCompareExchange16 */ -inline short _InterlockedCompareExchange16(short volatile *p, short v1, short v2) +short _InterlockedCompareExchange16(short volatile *p, short v1, short v2) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -332,7 +332,7 @@ inline short _InterlockedCompareExchange16(short volatile *p, short v1, short v2 /* FUNCTION: _InterlockedCompareExchange8 */ -inline char _InterlockedCompareExchange8(char volatile *p, char v1, char v2) +char _InterlockedCompareExchange8(char volatile *p, char v1, char v2) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -351,7 +351,7 @@ inline char _InterlockedCompareExchange8(char volatile *p, char v1, char v2) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline __m128i _mm_set_epi32(int e3, int e2, int e1, int e0) +__m128i _mm_set_epi32(int e3, int e2, int e1, int e0) { return (__m128i){.m128i_i32 = {e0, e1, e2, e3}}; } @@ -365,7 +365,7 @@ inline __m128i _mm_set_epi32(int e3, int e2, int e1, int e0) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline __m128i _mm_setr_epi32(int e3, int e2, int e1, int e0) +__m128i _mm_setr_epi32(int e3, int e2, int e1, int e0) { return (__m128i){.m128i_i32 = {e3, e2, e1, e0}}; } @@ -379,7 +379,7 @@ inline __m128i _mm_setr_epi32(int e3, int e2, int e1, int e0) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline __m128i _mm_set_epi16( +__m128i _mm_set_epi16( short e7, short e6, short e5, @@ -401,7 +401,7 @@ inline __m128i _mm_set_epi16( # define __CPROVER_INTRIN_H_INCLUDED # endif -inline __m128i _mm_setr_epi16( +__m128i _mm_setr_epi16( short e7, short e6, short e5, @@ -423,7 +423,7 @@ inline __m128i _mm_setr_epi16( # define __CPROVER_INTRIN_H_INCLUDED # endif -inline __m64 _mm_set_pi16(short e3, short e2, short e1, short e0) +__m64 _mm_set_pi16(short e3, short e2, short e1, short e0) { return (__m64){.m64_i16 = {e0, e1, e2, e3}}; } @@ -437,7 +437,7 @@ inline __m64 _mm_set_pi16(short e3, short e2, short e1, short e0) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline __m64 _mm_setr_pi16(short e3, short e2, short e1, short e0) +__m64 _mm_setr_pi16(short e3, short e2, short e1, short e0) { return (__m64){.m64_i16 = {e3, e2, e1, e0}}; } @@ -451,7 +451,7 @@ inline __m64 _mm_setr_pi16(short e3, short e2, short e1, short e0) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline int _mm_extract_epi32(__m128i a, const int imm8) +int _mm_extract_epi32(__m128i a, const int imm8) { return a.m128i_i32[imm8]; } @@ -465,7 +465,7 @@ inline int _mm_extract_epi32(__m128i a, const int imm8) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline int _mm_extract_epi16(__m128i a, const int imm8) +int _mm_extract_epi16(__m128i a, const int imm8) { return a.m128i_i16[imm8]; } @@ -479,7 +479,7 @@ inline int _mm_extract_epi16(__m128i a, const int imm8) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline int _mm_extract_pi16(__m64 a, const int imm8) +int _mm_extract_pi16(__m64 a, const int imm8) { return a.m64_i16[imm8]; } @@ -493,7 +493,7 @@ inline int _mm_extract_pi16(__m64 a, const int imm8) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline __m128i _mm_adds_epi16(__m128i a, __m128i b) +__m128i _mm_adds_epi16(__m128i a, __m128i b) { return (__m128i){ .m128i_i16 = { @@ -517,7 +517,7 @@ inline __m128i _mm_adds_epi16(__m128i a, __m128i b) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline __m128i _mm_subs_epi16(__m128i a, __m128i b) +__m128i _mm_subs_epi16(__m128i a, __m128i b) { return (__m128i){ .m128i_i16 = { @@ -541,7 +541,7 @@ inline __m128i _mm_subs_epi16(__m128i a, __m128i b) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline __m128i _mm_adds_epu16(__m128i a, __m128i b) +__m128i _mm_adds_epu16(__m128i a, __m128i b) { return (__m128i){ .m128i_i16 = { @@ -565,7 +565,7 @@ inline __m128i _mm_adds_epu16(__m128i a, __m128i b) # define __CPROVER_INTRIN_H_INCLUDED # endif -inline __m128i _mm_subs_epu16(__m128i a, __m128i b) +__m128i _mm_subs_epu16(__m128i a, __m128i b) { return (__m128i){ .m128i_u16 = { diff --git a/src/ansi-c/library/locale.c b/src/ansi-c/library/locale.c index 61d5353457e..1250fd93d0c 100644 --- a/src/ansi-c/library/locale.c +++ b/src/ansi-c/library/locale.c @@ -6,7 +6,7 @@ #define __CPROVER_LOCALE_H_INCLUDED #endif -inline char *setlocale(int category, const char *locale) +char *setlocale(int category, const char *locale) { __CPROVER_HIDE:; (void)category; @@ -29,7 +29,7 @@ inline char *setlocale(int category, const char *locale) #define __CPROVER_LOCALE_H_INCLUDED #endif -inline struct lconv *localeconv(void) +struct lconv *localeconv(void) { __CPROVER_HIDE:; #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index 34da9f51cb1..c0946cda903 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -1,26 +1,26 @@ /* FUNCTION: fabs */ -inline double fabs(double d) { return __CPROVER_fabs(d); } +double fabs(double d) { return __CPROVER_fabs(d); } /* FUNCTION: fabsl */ -inline long double fabsl(long double d) { return __CPROVER_fabsl(d); } +long double fabsl(long double d) { return __CPROVER_fabsl(d); } /* FUNCTION: fabsf */ -inline float fabsf(float f) { return __CPROVER_fabsf(f); } +float fabsf(float f) { return __CPROVER_fabsf(f); } /* FUNCTION: __builtin_fabs */ -inline double __builtin_fabs(double d) { return __CPROVER_fabs(d); } +double __builtin_fabs(double d) { return __CPROVER_fabs(d); } /* FUNCTION: __builtin_fabsl */ -inline long double __builtin_fabsl(long double d) { return __CPROVER_fabsl(d); } +long double __builtin_fabsl(long double d) { return __CPROVER_fabsl(d); } /* FUNCTION: __builtin_fabsf */ -inline float __builtin_fabsf(float f) { return __CPROVER_fabsf(f); } +float __builtin_fabsf(float f) { return __CPROVER_fabsf(f); } /* FUNCTION: __CPROVER_isgreaterf */ @@ -98,137 +98,137 @@ int __finitel(long double ld) { return __CPROVER_isfiniteld(ld); } #undef isinf -inline int isinf(double d) { return __CPROVER_isinfd(d); } +int isinf(double d) { return __CPROVER_isinfd(d); } /* FUNCTION: __isinf */ -inline int __isinf(double d) { return __CPROVER_isinfd(d); } +int __isinf(double d) { return __CPROVER_isinfd(d); } /* FUNCTION: isinff */ -inline int isinff(float f) { return __CPROVER_isinff(f); } +int isinff(float f) { return __CPROVER_isinff(f); } /* FUNCTION: __isinff */ -inline int __isinff(float f) { return __CPROVER_isinff(f); } +int __isinff(float f) { return __CPROVER_isinff(f); } /* FUNCTION: isinfl */ -inline int isinfl(long double ld) { return __CPROVER_isinfld(ld); } +int isinfl(long double ld) { return __CPROVER_isinfld(ld); } /* FUNCTION: __isinfl */ -inline int __isinfl(long double ld) { return __CPROVER_isinfld(ld); } +int __isinfl(long double ld) { return __CPROVER_isinfld(ld); } /* FUNCTION: isnan */ #undef isnan -inline int isnan(double d) { return __CPROVER_isnand(d); } +int isnan(double d) { return __CPROVER_isnand(d); } /* FUNCTION: __isnan */ -inline int __isnan(double d) { return __CPROVER_isnand(d); } +int __isnan(double d) { return __CPROVER_isnand(d); } /* FUNCTION: __isnanf */ -inline int __isnanf(float f) { return __CPROVER_isnanf(f); } +int __isnanf(float f) { return __CPROVER_isnanf(f); } /* FUNCTION: isnanf */ -inline int isnanf(float f) { return __CPROVER_isnanf(f); } +int isnanf(float f) { return __CPROVER_isnanf(f); } /* FUNCTION: isnanl */ -inline int isnanl(long double ld) { return __CPROVER_isnanld(ld); } +int isnanl(long double ld) { return __CPROVER_isnanld(ld); } /* FUNCTION: __isnanl */ -inline int __isnanl(long double ld) { return __CPROVER_isnanld(ld); } +int __isnanl(long double ld) { return __CPROVER_isnanld(ld); } /* FUNCTION: isnormal */ #undef isnormal -inline int isnormal(double d) { return __CPROVER_isnormald(d); } +int isnormal(double d) { return __CPROVER_isnormald(d); } /* FUNCTION: __isnormalf */ -inline int __isnormalf(float f) { return __CPROVER_isnormalf(f); } +int __isnormalf(float f) { return __CPROVER_isnormalf(f); } /* FUNCTION: __builtin_inff */ -inline float __builtin_inff(void) { return 1.0f/0.0f; } +float __builtin_inff(void) { return 1.0f/0.0f; } /* FUNCTION: __builtin_inf */ -inline double __builtin_inf(void) { return 1.0/0.0; } +double __builtin_inf(void) { return 1.0/0.0; } /* FUNCTION: __builtin_infl */ -inline long double __builtin_infl(void) { return 1.0l/0.0l; } +long double __builtin_infl(void) { return 1.0l/0.0l; } /* FUNCTION: __builtin_isinf */ -inline int __builtin_isinf(double d) { return __CPROVER_isinfd(d); } +int __builtin_isinf(double d) { return __CPROVER_isinfd(d); } /* FUNCTION: __builtin_isinff */ -inline int __builtin_isinff(float f) { return __CPROVER_isinff(f); } +int __builtin_isinff(float f) { return __CPROVER_isinff(f); } /* FUNCTION: __builtin_isinf */ -inline int __builtin_isinfl(long double ld) { return __CPROVER_isinfld(ld); } +int __builtin_isinfl(long double ld) { return __CPROVER_isinfld(ld); } /* FUNCTION: __builtin_isnan */ -inline int __builtin_isnan(double d) { return __CPROVER_isnand(d); } +int __builtin_isnan(double d) { return __CPROVER_isnand(d); } /* FUNCTION: __builtin_isnanf */ -inline int __builtin_isnanf(float f) { return __CPROVER_isnanf(f); } +int __builtin_isnanf(float f) { return __CPROVER_isnanf(f); } /* FUNCTION: __builtin_huge_valf */ -inline float __builtin_huge_valf(void) { return 1.0f/0.0f; } +float __builtin_huge_valf(void) { return 1.0f/0.0f; } /* FUNCTION: __builtin_huge_val */ -inline double __builtin_huge_val(void) { return 1.0/0.0; } +double __builtin_huge_val(void) { return 1.0/0.0; } /* FUNCTION: __builtin_huge_vall */ -inline long double __builtin_huge_vall(void) { return 1.0l/0.0l; } +long double __builtin_huge_vall(void) { return 1.0l/0.0l; } /* FUNCTION: _dsign */ -inline int _dsign(double d) { return __CPROVER_signd(d); } +int _dsign(double d) { return __CPROVER_signd(d); } /* FUNCTION: _ldsign */ -inline int _ldsign(long double ld) { return __CPROVER_signld(ld); } +int _ldsign(long double ld) { return __CPROVER_signld(ld); } /* FUNCTION: _fdsign */ -inline int _fdsign(float f) { return __CPROVER_signf(f); } +int _fdsign(float f) { return __CPROVER_signf(f); } /* FUNCTION: signbit */ #undef signbit -inline int signbit(double d) { return __CPROVER_signd(d); } +int signbit(double d) { return __CPROVER_signd(d); } /* FUNCTION: __signbitd */ -inline int __signbitd(double d) { return __CPROVER_signd(d); } +int __signbitd(double d) { return __CPROVER_signd(d); } /* FUNCTION: __signbitf */ -inline int __signbitf(float f) { return __CPROVER_signf(f); } +int __signbitf(float f) { return __CPROVER_signf(f); } /* FUNCTION: __signbit */ -inline int __signbit(double ld) { return __CPROVER_signld(ld); } +int __signbit(double ld) { return __CPROVER_signld(ld); } /* FUNCTION: _dclass */ @@ -237,7 +237,7 @@ inline int __signbit(double ld) { return __CPROVER_signld(ld); } #define __CPROVER_MATH_H_INCLUDED #endif -inline short _dclass(double d) { +short _dclass(double d) { __CPROVER_HIDE: return __CPROVER_isnand(d)?FP_NAN: __CPROVER_isinfd(d)?FP_INFINITE: @@ -253,7 +253,7 @@ inline short _dclass(double d) { #define __CPROVER_MATH_H_INCLUDED #endif -inline short _ldclass(long double ld) { +short _ldclass(long double ld) { __CPROVER_HIDE: return __CPROVER_isnanld(ld)?FP_NAN: __CPROVER_isinfld(ld)?FP_INFINITE: @@ -269,7 +269,7 @@ inline short _ldclass(long double ld) { #define __CPROVER_MATH_H_INCLUDED #endif -inline short _fdclass(float f) { +short _fdclass(float f) { __CPROVER_HIDE: return __CPROVER_isnanf(f)?FP_NAN: __CPROVER_isinff(f)?FP_INFINITE: @@ -285,7 +285,7 @@ inline short _fdclass(float f) { #define __CPROVER_MATH_H_INCLUDED #endif -inline int __fpclassifyd(double d) { +int __fpclassifyd(double d) { __CPROVER_HIDE: return __CPROVER_fpclassify( FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); @@ -298,7 +298,7 @@ inline int __fpclassifyd(double d) { #define __CPROVER_MATH_H_INCLUDED #endif -inline int __fpclassifyf(float f) { +int __fpclassifyf(float f) { __CPROVER_HIDE: return __CPROVER_fpclassify( FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f); @@ -311,7 +311,7 @@ inline int __fpclassifyf(float f) { #define __CPROVER_MATH_H_INCLUDED #endif -inline int __fpclassifyl(long double f) { +int __fpclassifyl(long double f) { __CPROVER_HIDE: return __CPROVER_fpclassify( FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f); @@ -328,13 +328,13 @@ inline int __fpclassifyl(long double f) { // only; newer ones use __fpclassifyd. #ifdef __APPLE__ -inline int __fpclassify(long double d) { +int __fpclassify(long double d) { __CPROVER_HIDE: return __CPROVER_fpclassify( FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); } #else -inline int __fpclassify(double d) { +int __fpclassify(double d) { __CPROVER_HIDE: return __CPROVER_fpclassify( FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index 849f217472f..d93bf2e5f05 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -7,7 +7,7 @@ int __VERIFIER_nondet_int(); -inline int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type) +int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type) { __CPROVER_HIDE:; @@ -32,7 +32,7 @@ inline int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type) int __VERIFIER_nondet_int(); -inline int pthread_cancel(pthread_t thread) +int pthread_cancel(pthread_t thread) { __CPROVER_HIDE:; @@ -64,7 +64,7 @@ typedef signed char __CPROVER_mutex_t; #endif #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS -inline void pthread_mutex_cleanup(void *p) +void pthread_mutex_cleanup(void *p) { __CPROVER_HIDE:; __CPROVER_assert( @@ -73,7 +73,7 @@ inline void pthread_mutex_cleanup(void *p) } #endif -inline int pthread_mutex_init( +int pthread_mutex_init( pthread_mutex_t *mutex, const pthread_mutexattr_t *mutexattr) { __CPROVER_HIDE:; @@ -108,7 +108,7 @@ typedef signed char __CPROVER_mutex_t; #endif #endif -inline int pthread_mutex_lock(pthread_mutex_t *mutex) +int pthread_mutex_lock(pthread_mutex_t *mutex) { __CPROVER_HIDE:; #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS @@ -157,7 +157,7 @@ typedef signed char __CPROVER_mutex_t; #endif #endif -inline int pthread_mutex_trylock(pthread_mutex_t *mutex) +int pthread_mutex_trylock(pthread_mutex_t *mutex) { __CPROVER_HIDE:; int return_value; @@ -208,7 +208,7 @@ typedef signed char __CPROVER_mutex_t; #endif #endif -inline int pthread_mutex_unlock(pthread_mutex_t *mutex) +int pthread_mutex_unlock(pthread_mutex_t *mutex) { __CPROVER_HIDE:; @@ -256,7 +256,7 @@ typedef signed char __CPROVER_mutex_t; #endif #endif -inline int pthread_mutex_destroy(pthread_mutex_t *mutex) +int pthread_mutex_destroy(pthread_mutex_t *mutex) { __CPROVER_HIDE:; @@ -297,7 +297,7 @@ extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; -inline void pthread_exit(void *value_ptr) +void pthread_exit(void *value_ptr) { __CPROVER_HIDE:; if(value_ptr!=0) (void)*(char*)value_ptr; @@ -335,7 +335,7 @@ extern __CPROVER_bool __CPROVER_threads_exited[]; extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; extern unsigned long __CPROVER_next_thread_id; -inline int pthread_join(pthread_t thread, void **value_ptr) +int pthread_join(pthread_t thread, void **value_ptr) { __CPROVER_HIDE:; @@ -372,7 +372,7 @@ extern __CPROVER_bool __CPROVER_threads_exited[]; extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; extern unsigned long __CPROVER_next_thread_id; -inline int _pthread_join(pthread_t thread, void **value_ptr) +int _pthread_join(pthread_t thread, void **value_ptr) { __CPROVER_HIDE:; @@ -398,7 +398,7 @@ __CPROVER_HIDE:; #define __CPROVER_PTHREAD_H_INCLUDED #endif -inline int pthread_rwlock_destroy(pthread_rwlock_t *lock) +int pthread_rwlock_destroy(pthread_rwlock_t *lock) { __CPROVER_HIDE:; __CPROVER_assert(*((signed char *)lock)==0, @@ -420,7 +420,7 @@ inline int pthread_rwlock_destroy(pthread_rwlock_t *lock) #endif #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS -inline void pthread_rwlock_cleanup(void *p) +void pthread_rwlock_cleanup(void *p) { __CPROVER_HIDE:; __CPROVER_assert(__CPROVER_get_must(p, "rwlock_destroyed"), @@ -428,7 +428,7 @@ inline void pthread_rwlock_cleanup(void *p) } #endif -inline int pthread_rwlock_init(pthread_rwlock_t *lock, +int pthread_rwlock_init(pthread_rwlock_t *lock, const pthread_rwlockattr_t *attr) { __CPROVER_HIDE:; @@ -449,7 +449,7 @@ inline int pthread_rwlock_init(pthread_rwlock_t *lock, #define __CPROVER_PTHREAD_H_INCLUDED #endif -inline int pthread_rwlock_rdlock(pthread_rwlock_t *lock) +int pthread_rwlock_rdlock(pthread_rwlock_t *lock) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -468,7 +468,7 @@ inline int pthread_rwlock_rdlock(pthread_rwlock_t *lock) #define __CPROVER_PTHREAD_H_INCLUDED #endif -inline int pthread_rwlock_tryrdlock(pthread_rwlock_t *lock) +int pthread_rwlock_tryrdlock(pthread_rwlock_t *lock) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -485,7 +485,7 @@ inline int pthread_rwlock_tryrdlock(pthread_rwlock_t *lock) #define __CPROVER_PTHREAD_H_INCLUDED #endif -inline int pthread_rwlock_trywrlock(pthread_rwlock_t *lock) +int pthread_rwlock_trywrlock(pthread_rwlock_t *lock) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -502,7 +502,7 @@ inline int pthread_rwlock_trywrlock(pthread_rwlock_t *lock) #define __CPROVER_PTHREAD_H_INCLUDED #endif -inline int pthread_rwlock_unlock(pthread_rwlock_t *lock) +int pthread_rwlock_unlock(pthread_rwlock_t *lock) { __CPROVER_HIDE:; __CPROVER_assert(*((signed char *)lock)==1, @@ -519,7 +519,7 @@ inline int pthread_rwlock_unlock(pthread_rwlock_t *lock) #define __CPROVER_PTHREAD_H_INCLUDED #endif -inline int pthread_rwlock_wrlock(pthread_rwlock_t *lock) +int pthread_rwlock_wrlock(pthread_rwlock_t *lock) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); @@ -540,7 +540,7 @@ extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; -inline void __spawned_thread( +void __spawned_thread( unsigned long this_thread_id, #if 0 // Destructor support is disabled as it is too expensive due to its extensive @@ -609,7 +609,7 @@ void __spawned_thread( void *(*start_routine)(void *), void *arg); -inline int pthread_create( +int pthread_create( pthread_t *thread, // must not be null const pthread_attr_t *attr, // may be null void * (*start_routine)(void *), // must not be null @@ -659,7 +659,7 @@ inline int pthread_create( #define __CPROVER_PTHREAD_H_INCLUDED #endif -inline int pthread_cond_init( +int pthread_cond_init( pthread_cond_t *cond, const pthread_condattr_t *attr) { __CPROVER_HIDE: @@ -675,7 +675,7 @@ inline int pthread_cond_init( #define __CPROVER_PTHREAD_H_INCLUDED #endif -inline int pthread_cond_signal( +int pthread_cond_signal( pthread_cond_t *cond) { __CPROVER_HIDE: __CPROVER_atomic_begin(); @@ -691,7 +691,7 @@ inline int pthread_cond_signal( #define __CPROVER_PTHREAD_H_INCLUDED #endif -inline int pthread_cond_broadcast( +int pthread_cond_broadcast( pthread_cond_t *cond) { __CPROVER_HIDE: __CPROVER_atomic_begin(); @@ -707,7 +707,7 @@ inline int pthread_cond_broadcast( #define __CPROVER_PTHREAD_H_INCLUDED #endif -inline int pthread_cond_wait( +int pthread_cond_wait( pthread_cond_t *cond, pthread_mutex_t *mutex) { __CPROVER_HIDE: @@ -825,7 +825,7 @@ int __VERIFIER_nondet_int(); // no pthread_barrier_t on the Mac // slightly different declaration on OpenBSD #if !defined(__APPLE__) && !defined(__OpenBSD__) -inline int pthread_barrier_init( +int pthread_barrier_init( pthread_barrier_t *restrict barrier, const pthread_barrierattr_t *restrict attr, unsigned count) { @@ -846,7 +846,7 @@ inline int pthread_barrier_init( // pthread_barrier_init has a slightly different decl on OpenBSD #if defined(__OpenBSD__) -inline int pthread_barrier_init( +int pthread_barrier_init( pthread_barrier_t *restrict barrier, pthread_barrierattr_t *restrict attr, unsigned count) @@ -877,7 +877,7 @@ int __VERIFIER_nondet_int(); // no pthread_barrier_t on the Mac #ifndef __APPLE__ -inline int pthread_barrier_destroy(pthread_barrier_t *barrier) +int pthread_barrier_destroy(pthread_barrier_t *barrier) { __CPROVER_HIDE:; @@ -907,7 +907,7 @@ int __VERIFIER_nondet_int(); // no pthread_barrier_t on the Mac #ifndef __APPLE__ -inline int pthread_barrier_wait(pthread_barrier_t *barrier) +int pthread_barrier_wait(pthread_barrier_t *barrier) { __CPROVER_HIDE:; @@ -936,7 +936,7 @@ extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; -inline int pthread_key_create(pthread_key_t *key, void (*destructor)(void *)) +int pthread_key_create(pthread_key_t *key, void (*destructor)(void *)) { __CPROVER_HIDE:; __CPROVER_thread_keys[__CPROVER_next_thread_key] = 0; @@ -960,7 +960,7 @@ __CPROVER_HIDE:; extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; -inline int pthread_key_delete(pthread_key_t key) +int pthread_key_delete(pthread_key_t key) { __CPROVER_HIDE:; __CPROVER_thread_keys[key] = 0; @@ -976,7 +976,7 @@ __CPROVER_HIDE:; extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; -inline void *pthread_getspecific(pthread_key_t key) +void *pthread_getspecific(pthread_key_t key) { __CPROVER_HIDE:; return (void *)__CPROVER_thread_keys[key]; @@ -991,7 +991,7 @@ __CPROVER_HIDE:; extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; -inline int pthread_setspecific(pthread_key_t key, const void *value) +int pthread_setspecific(pthread_key_t key, const void *value) { __CPROVER_HIDE:; __CPROVER_thread_keys[key] = value; diff --git a/src/ansi-c/library/semaphore.c b/src/ansi-c/library/semaphore.c index 5499a8ca72f..c071693cb8a 100644 --- a/src/ansi-c/library/semaphore.c +++ b/src/ansi-c/library/semaphore.c @@ -2,7 +2,7 @@ #include -inline int sem_init(sem_t *sem, int pshared, unsigned int value) +int sem_init(sem_t *sem, int pshared, unsigned int value) { __CPROVER_HIDE:; (void)pshared; @@ -21,7 +21,7 @@ inline int sem_init(sem_t *sem, int pshared, unsigned int value) #include -inline int sem_wait(sem_t *sem) +int sem_wait(sem_t *sem) { __CPROVER_HIDE:; (void)sem; @@ -40,7 +40,7 @@ inline int sem_wait(sem_t *sem) #include -inline int sem_timedwait(sem_t *sem, const struct timespec *abstime) +int sem_timedwait(sem_t *sem, const struct timespec *abstime) { __CPROVER_HIDE:; (void)sem; @@ -60,7 +60,7 @@ inline int sem_timedwait(sem_t *sem, const struct timespec *abstime) #include -inline int sem_trywait(sem_t *sem) +int sem_trywait(sem_t *sem) { __CPROVER_HIDE:; (void)sem; @@ -79,7 +79,7 @@ inline int sem_trywait(sem_t *sem) #include -inline int sem_post(sem_t *sem) +int sem_post(sem_t *sem) { __CPROVER_HIDE:; (void)sem; @@ -98,7 +98,7 @@ inline int sem_post(sem_t *sem) #include -inline int sem_post_multiple(sem_t *sem, int number) +int sem_post_multiple(sem_t *sem, int number) { __CPROVER_HIDE:; (void)sem; @@ -118,7 +118,7 @@ inline int sem_post_multiple(sem_t *sem, int number) #include -inline int sem_getvalue(sem_t *sem, int *sval) +int sem_getvalue(sem_t *sem, int *sval) { __CPROVER_HIDE:; (void)sem; @@ -138,7 +138,7 @@ inline int sem_getvalue(sem_t *sem, int *sval) #include -inline int sem_destroy(sem_t *sem) +int sem_destroy(sem_t *sem) { __CPROVER_HIDE:; (void)sem; diff --git a/src/ansi-c/library/setjmp.c b/src/ansi-c/library/setjmp.c index 7ee26630129..625a25cc393 100644 --- a/src/ansi-c/library/setjmp.c +++ b/src/ansi-c/library/setjmp.c @@ -6,7 +6,7 @@ #define __CPROVER_SETJMP_H_INCLUDED #endif -inline void longjmp(jmp_buf env, int val) +void longjmp(jmp_buf env, int val) { // does not return (void)env; @@ -25,7 +25,7 @@ inline void longjmp(jmp_buf env, int val) #define __CPROVER_SETJMP_H_INCLUDED #endif -inline void _longjmp(jmp_buf env, int val) +void _longjmp(jmp_buf env, int val) { // does not return (void)env; @@ -46,7 +46,7 @@ inline void _longjmp(jmp_buf env, int val) #define __CPROVER_SETJMP_H_INCLUDED #endif -inline void siglongjmp(sigjmp_buf env, int val) +void siglongjmp(sigjmp_buf env, int val) { // does not return (void)env; @@ -69,7 +69,7 @@ inline void siglongjmp(sigjmp_buf env, int val) #undef setjmp -inline int setjmp(jmp_buf env) +int setjmp(jmp_buf env) { (void)env; // returns via longjmp require instrumentation; only such returns would @@ -84,7 +84,7 @@ inline int setjmp(jmp_buf env) #define __CPROVER_SETJMP_H_INCLUDED #endif -inline int _setjmp(jmp_buf env) +int _setjmp(jmp_buf env) { (void)env; // returns via longjmp require instrumentation; only such returns would @@ -103,7 +103,7 @@ inline int _setjmp(jmp_buf env) #undef sigsetjmp -inline int sigsetjmp(sigjmp_buf env, int savesigs) +int sigsetjmp(sigjmp_buf env, int savesigs) { (void)env; (void)savesigs; @@ -123,7 +123,7 @@ inline int sigsetjmp(sigjmp_buf env, int savesigs) # define __CPROVER_SETJMP_H_INCLUDED #endif -inline int __sigsetjmp(sigjmp_buf env, int savesigs) +int __sigsetjmp(sigjmp_buf env, int savesigs) { (void)env; (void)savesigs; diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index 59250dacae2..4afe29a66c6 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -18,7 +18,7 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); -inline int putchar(int c) +int putchar(int c) { __CPROVER_HIDE:; __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); @@ -36,7 +36,7 @@ inline int putchar(int c) __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); int __VERIFIER_nondet_int(); -inline int puts(const char *s) +int puts(const char *s) { __CPROVER_HIDE:; __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); @@ -49,7 +49,7 @@ inline int puts(const char *s) /* FUNCTION: fclose_cleanup */ #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS -inline void fclose_cleanup(void *stream) +void fclose_cleanup(void *stream) { __CPROVER_HIDE:; __CPROVER_assert( @@ -73,7 +73,7 @@ __CPROVER_HIDE:; void fclose_cleanup(void *stream); __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); -inline FILE *fopen(const char *filename, const char *mode) +FILE *fopen(const char *filename, const char *mode) { __CPROVER_HIDE:; (void)*filename; @@ -124,7 +124,7 @@ void fclose_cleanup(void *stream); __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); #ifdef __APPLE__ -inline FILE *_fopen(const char *filename, const char *mode) +FILE *_fopen(const char *filename, const char *mode) { __CPROVER_HIDE:; (void)*filename; @@ -159,7 +159,7 @@ __CPROVER_HIDE:; #define __CPROVER_STDIO_H_INCLUDED #endif -inline FILE* freopen(const char *filename, const char *mode, FILE *f) +FILE* freopen(const char *filename, const char *mode, FILE *f) { __CPROVER_HIDE:; (void)*filename; @@ -187,7 +187,7 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f) int __VERIFIER_nondet_int(); -inline int fclose(FILE *stream) +int fclose(FILE *stream) { __CPROVER_HIDE:; #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS @@ -213,7 +213,7 @@ __CPROVER_HIDE:; #define __CPROVER_STDLIB_H_INCLUDED #endif -inline FILE *fdopen(int handle, const char *mode) +FILE *fdopen(int handle, const char *mode) { __CPROVER_HIDE:; (void)handle; @@ -252,7 +252,7 @@ inline FILE *fdopen(int handle, const char *mode) #endif #ifdef __APPLE__ -inline FILE *_fdopen(int handle, const char *mode) +FILE *_fdopen(int handle, const char *mode) { __CPROVER_HIDE:; (void)handle; @@ -333,7 +333,7 @@ char *fgets(char *str, int size, FILE *stream) char __VERIFIER_nondet_char(); size_t __VERIFIER_nondet_size_t(); -inline size_t fread( +size_t fread( void *ptr, size_t size, size_t nitems, @@ -375,7 +375,7 @@ inline size_t fread( int __VERIFIER_nondet_int(); -inline int feof(FILE *stream) +int feof(FILE *stream) { // just return nondet __CPROVER_HIDE:; @@ -407,7 +407,7 @@ inline int feof(FILE *stream) int __VERIFIER_nondet_int(); -inline int ferror(FILE *stream) +int ferror(FILE *stream) { // just return nondet __CPROVER_HIDE:; @@ -439,7 +439,7 @@ inline int ferror(FILE *stream) int __VERIFIER_nondet_int(); -inline int fileno(FILE *stream) +int fileno(FILE *stream) { __CPROVER_HIDE:; if(stream == stdin) @@ -475,7 +475,7 @@ __CPROVER_HIDE:; int __VERIFIER_nondet_int(); -inline int fputs(const char *s, FILE *stream) +int fputs(const char *s, FILE *stream) { // just return nondet __CPROVER_HIDE:; @@ -511,7 +511,7 @@ inline int fputs(const char *s, FILE *stream) int __VERIFIER_nondet_int(); -inline int fflush(FILE *stream) +int fflush(FILE *stream) { // just return nondet __CPROVER_HIDE:; @@ -536,7 +536,7 @@ inline int fflush(FILE *stream) int __VERIFIER_nondet_int(); -inline int fpurge(FILE *stream) +int fpurge(FILE *stream) { // just return nondet __CPROVER_HIDE:; @@ -568,7 +568,7 @@ inline int fpurge(FILE *stream) int __VERIFIER_nondet_int(); -inline int fgetc(FILE *stream) +int fgetc(FILE *stream) { __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); @@ -604,7 +604,7 @@ inline int fgetc(FILE *stream) int __VERIFIER_nondet_int(); -inline int getc(FILE *stream) +int getc(FILE *stream) { __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); @@ -640,7 +640,7 @@ inline int getc(FILE *stream) int __VERIFIER_nondet_int(); -inline int getchar() +int getchar() { __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); @@ -659,7 +659,7 @@ inline int getchar() int __VERIFIER_nondet_int(); -inline int getw(FILE *stream) +int getw(FILE *stream) { __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); @@ -693,7 +693,7 @@ inline int getw(FILE *stream) int __VERIFIER_nondet_int(); -inline int fseek(FILE *stream, long offset, int whence) +int fseek(FILE *stream, long offset, int whence) { __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); @@ -723,7 +723,7 @@ inline int fseek(FILE *stream, long offset, int whence) long __VERIFIER_nondet_long(); -inline long ftell(FILE *stream) +long ftell(FILE *stream) { __CPROVER_HIDE:; long return_value=__VERIFIER_nondet_long(); @@ -838,7 +838,7 @@ void perror(const char *s) #define __CPROVER_STDARG_H_INCLUDED #endif -inline int fscanf(FILE *restrict stream, const char *restrict format, ...) +int fscanf(FILE *restrict stream, const char *restrict format, ...) { __CPROVER_HIDE:; va_list list; @@ -860,7 +860,7 @@ __CPROVER_HIDE:; #define __CPROVER_STDARG_H_INCLUDED #endif -inline int scanf(const char *restrict format, ...) +int scanf(const char *restrict format, ...) { __CPROVER_HIDE:; va_list list; @@ -882,7 +882,7 @@ __CPROVER_HIDE:; #define __CPROVER_STDARG_H_INCLUDED #endif -inline int sscanf(const char *restrict s, const char *restrict format, ...) +int sscanf(const char *restrict s, const char *restrict format, ...) { __CPROVER_HIDE:; va_list list; @@ -906,7 +906,7 @@ __CPROVER_HIDE:; int __VERIFIER_nondet_int(); -inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg) +int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg) { __CPROVER_HIDE:; int result=__VERIFIER_nondet_int(); @@ -943,7 +943,7 @@ inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list a #define __CPROVER_STDARG_H_INCLUDED #endif -inline int vscanf(const char *restrict format, va_list arg) +int vscanf(const char *restrict format, va_list arg) { __CPROVER_HIDE:; return vfscanf(stdin, format, arg); @@ -963,7 +963,7 @@ inline int vscanf(const char *restrict format, va_list arg) int __VERIFIER_nondet_int(); -inline int vsscanf(const char *restrict s, const char *restrict format, va_list arg) +int vsscanf(const char *restrict s, const char *restrict format, va_list arg) { __CPROVER_HIDE:; int result=__VERIFIER_nondet_int(); @@ -987,7 +987,7 @@ inline int vsscanf(const char *restrict s, const char *restrict format, va_list int __VERIFIER_nondet_int(); -inline int printf(const char *format, ...) +int printf(const char *format, ...) { __CPROVER_HIDE:; int result = __VERIFIER_nondet_int(); @@ -1010,7 +1010,7 @@ __CPROVER_HIDE:; #define __CPROVER_STDARG_H_INCLUDED #endif -inline int fprintf(FILE *stream, const char *restrict format, ...) +int fprintf(FILE *stream, const char *restrict format, ...) { __CPROVER_HIDE:; va_list list; @@ -1034,7 +1034,7 @@ inline int fprintf(FILE *stream, const char *restrict format, ...) int __VERIFIER_nondet_int(); -inline int vfprintf(FILE *stream, const char *restrict format, va_list arg) +int vfprintf(FILE *stream, const char *restrict format, va_list arg) { __CPROVER_HIDE:; @@ -1080,7 +1080,7 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg) char __VERIFIER_nondet_char(); int __VERIFIER_nondet_int(); -inline int vasprintf(char **ptr, const char *fmt, va_list ap) +int vasprintf(char **ptr, const char *fmt, va_list ap) { (void)*fmt; (void)ap; @@ -1113,7 +1113,7 @@ inline int vasprintf(char **ptr, const char *fmt, va_list ap) # define __CPROVER_STDIO_H_INCLUDED # endif -inline FILE *__acrt_iob_func(unsigned fd) +FILE *__acrt_iob_func(unsigned fd) { static FILE stdin_file; static FILE stdout_file; @@ -1148,7 +1148,7 @@ inline FILE *__acrt_iob_func(unsigned fd) # define __CPROVER_STDARG_H_INCLUDED # endif -inline int __stdio_common_vfprintf( +int __stdio_common_vfprintf( unsigned __int64 options, FILE *stream, char const *format, diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index dbe0fb43f75..ccde0e838b4 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -2,37 +2,37 @@ #undef abs -inline int abs(int i) { return __CPROVER_abs(i); } +int abs(int i) { return __CPROVER_abs(i); } /* FUNCTION: labs */ #undef labs -inline long int labs(long int i) { return __CPROVER_labs(i); } +long int labs(long int i) { return __CPROVER_labs(i); } /* FUNCTION: llabs */ #undef llabs -inline long long int llabs(long long int i) { return __CPROVER_llabs(i); } +long long int llabs(long long int i) { return __CPROVER_llabs(i); } /* FUNCTION: __builtin_abs */ -inline int __builtin_abs(int i) { return __CPROVER_abs(i); } +int __builtin_abs(int i) { return __CPROVER_abs(i); } /* FUNCTION: __builtin_labs */ -inline long int __builtin_labs(long int i) { return __CPROVER_labs(i); } +long int __builtin_labs(long int i) { return __CPROVER_labs(i); } /* FUNCTION: __builtin_llabs */ -inline long long int __builtin_llabs(long long int i) { return __CPROVER_llabs(i); } +long long int __builtin_llabs(long long int i) { return __CPROVER_llabs(i); } /* FUNCTION: exit */ #undef exit -inline void exit(int status) +void exit(int status) { (void)status; __CPROVER_assume(0); @@ -45,7 +45,7 @@ inline void exit(int status) #undef _Exit -inline void _Exit(int status) +void _Exit(int status) { (void)status; __CPROVER_assume(0); @@ -58,7 +58,7 @@ inline void _Exit(int status) #undef abort -inline void abort(void) +void abort(void) { __CPROVER_assume(0); #ifdef LIBRARY_CHECK @@ -75,7 +75,7 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); _Bool __builtin_mul_overflow(); #endif -inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size) +void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size) { __CPROVER_HIDE:; __CPROVER_size_t alloc_size; @@ -140,6 +140,8 @@ __CPROVER_HIDE:; __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +// malloc is marked "inline" for the benefit of goto-analyzer. Really, +// goto-analyzer should take care of inlining as needed. inline void *malloc(__CPROVER_size_t malloc_size) { // realistically, malloc may return NULL, @@ -199,7 +201,7 @@ __CPROVER_HIDE:; __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); extern void *__CPROVER_alloca_object; -inline void *__builtin_alloca(__CPROVER_size_t alloca_size) +void *__builtin_alloca(__CPROVER_size_t alloca_size) { __CPROVER_HIDE:; void *res; @@ -229,7 +231,7 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size) void *__builtin_alloca(__CPROVER_size_t alloca_size); -inline void *alloca(__CPROVER_size_t alloca_size) +void *alloca(__CPROVER_size_t alloca_size) { __CPROVER_HIDE:; return __builtin_alloca(alloca_size); @@ -242,7 +244,7 @@ __CPROVER_HIDE:; __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); extern void *__CPROVER_alloca_object; -inline void free(void *ptr) +void free(void *ptr) { __CPROVER_HIDE:; // If ptr is NULL, no operation is performed. @@ -303,7 +305,7 @@ _Bool __builtin_add_overflow(); _Bool __builtin_mul_overflow(); #endif -inline long strtol(const char *nptr, char **endptr, int base) +long strtol(const char *nptr, char **endptr, int base) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -390,7 +392,7 @@ inline long strtol(const char *nptr, char **endptr, int base) long strtol(const char *nptr, char **endptr, int base); -inline int atoi(const char *nptr) +int atoi(const char *nptr) { __CPROVER_HIDE:; return (int)strtol(nptr, (char **)0, 10); @@ -403,7 +405,7 @@ inline int atoi(const char *nptr) long strtol(const char *nptr, char **endptr, int base); -inline long atol(const char *nptr) +long atol(const char *nptr) { __CPROVER_HIDE:; return strtol(nptr, (char **)0, 10); @@ -421,7 +423,7 @@ inline long atol(const char *nptr) __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); ptrdiff_t __VERIFIER_nondet_ptrdiff_t(); -inline char *getenv(const char *name) +char *getenv(const char *name) { __CPROVER_HIDE:; @@ -464,10 +466,10 @@ inline char *getenv(const char *name) /* FUNCTION: realloc */ -inline void *malloc(__CPROVER_size_t malloc_size); -inline void free(void *ptr); +void *malloc(__CPROVER_size_t malloc_size); +void free(void *ptr); -inline void *realloc(void *ptr, __CPROVER_size_t malloc_size) +void *realloc(void *ptr, __CPROVER_size_t malloc_size) { __CPROVER_HIDE:; @@ -500,9 +502,9 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size) /* FUNCTION: valloc */ -inline void *malloc(__CPROVER_size_t malloc_size); +void *malloc(__CPROVER_size_t malloc_size); -inline void *valloc(__CPROVER_size_t malloc_size) +void *valloc(__CPROVER_size_t malloc_size) { // The allocated memory is aligned on a page // boundary, which we don't model. @@ -520,8 +522,8 @@ inline void *valloc(__CPROVER_size_t malloc_size) #undef posix_memalign -inline void *malloc(__CPROVER_size_t malloc_size); -inline int +void *malloc(__CPROVER_size_t malloc_size); +int posix_memalign(void **ptr, __CPROVER_size_t alignment, __CPROVER_size_t size) { __CPROVER_HIDE:; diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c index 757f54d6422..59e31de10b6 100644 --- a/src/ansi-c/library/string.c +++ b/src/ansi-c/library/string.c @@ -1,6 +1,6 @@ /* FUNCTION: __builtin___strcpy_chk */ -inline char *__builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t s) +char *__builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t s) { __CPROVER_HIDE:; @@ -136,7 +136,7 @@ __CPROVER_HIDE:; #undef strcpy -inline char *strcpy(char *dst, const char *src) +char *strcpy(char *dst, const char *src) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -173,7 +173,7 @@ __CPROVER_HIDE:; #undef strncpy -inline char *strncpy(char *dst, const char *src, size_t n) +char *strncpy(char *dst, const char *src, size_t n) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -211,7 +211,7 @@ __CPROVER_HIDE:; #define __CPROVER_STRING_H_INCLUDED #endif -inline char *__builtin___strncpy_chk(char *dst, const char *src, size_t n, size_t object_size) +char *__builtin___strncpy_chk(char *dst, const char *src, size_t n, size_t object_size) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -255,7 +255,7 @@ __CPROVER_HIDE:; #undef strcat -inline char *strcat(char *dst, const char *src) +char *strcat(char *dst, const char *src) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -301,7 +301,7 @@ __CPROVER_HIDE:; #undef strncat -inline char *strncat(char *dst, const char *src, size_t n) +char *strncat(char *dst, const char *src, size_t n) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -356,7 +356,7 @@ __CPROVER_HIDE:; #undef strcmp -inline int strcmp(const char *s1, const char *s2) +int strcmp(const char *s1, const char *s2) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -405,7 +405,7 @@ __CPROVER_HIDE:; #undef strcasecmp -inline int strcasecmp(const char *s1, const char *s2) +int strcasecmp(const char *s1, const char *s2) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -457,7 +457,7 @@ __CPROVER_HIDE:; #undef strncmp -inline int strncmp(const char *s1, const char *s2, size_t n) +int strncmp(const char *s1, const char *s2, size_t n) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -504,7 +504,7 @@ __CPROVER_HIDE:; #undef strncasecmp -inline int strncasecmp(const char *s1, const char *s2, size_t n) +int strncasecmp(const char *s1, const char *s2, size_t n) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -554,7 +554,7 @@ __CPROVER_HIDE:; #undef strlen -inline size_t strlen(const char *s) +size_t strlen(const char *s) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -583,7 +583,7 @@ inline size_t strlen(const char *s) #undef strdup #undef strcpy -inline char *strdup(const char *str) +char *strdup(const char *str) { __CPROVER_HIDE:; __CPROVER_size_t bufsz; @@ -916,7 +916,7 @@ void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_s #undef memcmp -inline int memcmp(const void *s1, const void *s2, size_t n) +int memcmp(const void *s1, const void *s2, size_t n) { __CPROVER_HIDE:; int res=0; @@ -951,7 +951,7 @@ inline int memcmp(const void *s1, const void *s2, size_t n) #undef strchr -inline char *strchr(const char *src, int c) +char *strchr(const char *src, int c) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION @@ -980,7 +980,7 @@ inline char *strchr(const char *src, int c) #undef strchr -inline char *strrchr(const char *src, int c) +char *strrchr(const char *src, int c) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c index 096d8f9837d..d4bc309954f 100644 --- a/src/ansi-c/library/unistd.c +++ b/src/ansi-c/library/unistd.c @@ -16,7 +16,7 @@ unsigned int sleep(unsigned int seconds) unsigned int sleep(unsigned int seconds); -inline unsigned int _sleep(unsigned int seconds) +unsigned int _sleep(unsigned int seconds) { __CPROVER_HIDE:; return sleep(seconds); @@ -125,7 +125,7 @@ int close(int fildes) int close(int fildes); -inline int _close(int fildes) +int _close(int fildes) { __CPROVER_HIDE:; return close(fildes); @@ -199,7 +199,7 @@ ret_type write(int fildes, const void *buf, size_type nbyte) ret_type write(int fildes, const void *buf, size_type nbyte); -inline ret_type _write(int fildes, const void *buf, size_type nbyte) +ret_type _write(int fildes, const void *buf, size_type nbyte) { __CPROVER_HIDE:; return write(fildes, buf, nbyte); @@ -303,7 +303,7 @@ ret_type read(int fildes, void *buf, size_type nbyte) ret_type read(int fildes, void *buf, size_type nbyte); -inline ret_type _read(int fildes, void *buf, size_type nbyte) +ret_type _read(int fildes, void *buf, size_type nbyte) { __CPROVER_HIDE:; return read(fildes, buf, nbyte); diff --git a/src/ansi-c/library/windows.c b/src/ansi-c/library/windows.c index 1c6b5e758bf..d3a94669300 100644 --- a/src/ansi-c/library/windows.c +++ b/src/ansi-c/library/windows.c @@ -20,7 +20,7 @@ BOOL QueryPerformanceFrequency(LARGE_INTEGER *lpFrequency) #ifdef _WIN32 #include -inline VOID ExitThread(DWORD dwExitCode) +VOID ExitThread(DWORD dwExitCode) { // never returns __CPROVER_assume(0); @@ -32,7 +32,7 @@ inline VOID ExitThread(DWORD dwExitCode) #ifdef _WIN32 #include -inline HANDLE CreateThread( +HANDLE CreateThread( LPSECURITY_ATTRIBUTES lpThreadAttributes, SIZE_T dwStackSize, LPTHREAD_START_ROUTINE lpStartAddress, diff --git a/src/ansi-c/library/x86_assembler.c b/src/ansi-c/library/x86_assembler.c index d1e5517ea0d..54f83177cec 100644 --- a/src/ansi-c/library/x86_assembler.c +++ b/src/ansi-c/library/x86_assembler.c @@ -3,7 +3,7 @@ extern int __CPROVER_rounding_mode; -inline void __asm_fnstcw(unsigned short *dest) +void __asm_fnstcw(unsigned short *dest) { // the rounding mode is bits 10 and 11 in the control word *dest=__CPROVER_rounding_mode<<10; @@ -13,7 +13,7 @@ inline void __asm_fnstcw(unsigned short *dest) extern int __CPROVER_rounding_mode; -inline void __asm_fstcw(unsigned short *dest) +void __asm_fstcw(unsigned short *dest) { // the rounding mode is bits 10 and 11 in the control word *dest=__CPROVER_rounding_mode<<10; @@ -23,7 +23,7 @@ inline void __asm_fstcw(unsigned short *dest) extern int __CPROVER_rounding_mode; -inline void __asm_fldcw(const unsigned short *src) +void __asm_fldcw(const unsigned short *src) { // the rounding mode is bits 10 and 11 in the control word __CPROVER_rounding_mode=((*src)>>10)&3; @@ -31,21 +31,21 @@ inline void __asm_fldcw(const unsigned short *src) /* FUNCTION: __asm_mfence */ -inline void __asm_mfence(void) +void __asm_mfence(void) { __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence"); } /* FUNCTION: __asm_sfence */ -inline void __asm_sfence(void) +void __asm_sfence(void) { __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence"); } /* FUNCTION: __asm_lfence */ -inline void __asm_lfence(void) +void __asm_lfence(void) { __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence"); } From 4057726efa91d8153fda446914a074426196c341 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 1 Jun 2022 09:22:10 +0000 Subject: [PATCH 4/4] Clang-format library code after removing "inline" --- src/ansi-c/library/errno.c | 2 +- src/ansi-c/library/getopt.c | 5 +- src/ansi-c/library/intrin.c | 3 +- src/ansi-c/library/math.c | 250 +++++++++++++++++++++++-------- src/ansi-c/library/pthread_lib.c | 31 ++-- src/ansi-c/library/stdio.c | 8 +- src/ansi-c/library/stdlib.c | 36 ++++- src/ansi-c/library/string.c | 6 +- src/ansi-c/library/windows.c | 3 +- 9 files changed, 241 insertions(+), 103 deletions(-) diff --git a/src/ansi-c/library/errno.c b/src/ansi-c/library/errno.c index 341465129b7..edb46ccaabe 100644 --- a/src/ansi-c/library/errno.c +++ b/src/ansi-c/library/errno.c @@ -5,7 +5,7 @@ __CPROVER_thread_local int __CPROVER_errno; -int * __error(void) +int *__error(void) { return &__CPROVER_errno; } diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c index 45ceeae9e7b..9acc33a3f63 100644 --- a/src/ansi-c/library/getopt.c +++ b/src/ansi-c/library/getopt.c @@ -11,8 +11,7 @@ extern int optind; __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); size_t __VERIFIER_nondet_size_t(); -int getopt( - int argc, char * const argv[], const char *optstring) +int getopt(int argc, char *const argv[], const char *optstring) { __CPROVER_HIDE:; int result=-1; @@ -64,7 +63,7 @@ int getopt( int getopt_long( int argc, - char * const argv[], + char *const argv[], const char *optstring, const struct option *longopts, int *longindex) diff --git a/src/ansi-c/library/intrin.c b/src/ansi-c/library/intrin.c index 5665dce4084..1ea076b7f72 100644 --- a/src/ansi-c/library/intrin.c +++ b/src/ansi-c/library/intrin.c @@ -101,7 +101,8 @@ long _InterlockedCompareExchange(long volatile *p, long v1, long v2) /* FUNCTION: _InterlockedCompareExchange64 */ -long long _InterlockedCompareExchange64(long long volatile *p, long long v1, long long v2) +long long +_InterlockedCompareExchange64(long long volatile *p, long long v1, long long v2) { __CPROVER_HIDE:; __CPROVER_atomic_begin(); diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index c0946cda903..9814d428cf5 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -1,26 +1,44 @@ /* FUNCTION: fabs */ -double fabs(double d) { return __CPROVER_fabs(d); } +double fabs(double d) +{ + return __CPROVER_fabs(d); +} /* FUNCTION: fabsl */ -long double fabsl(long double d) { return __CPROVER_fabsl(d); } +long double fabsl(long double d) +{ + return __CPROVER_fabsl(d); +} /* FUNCTION: fabsf */ -float fabsf(float f) { return __CPROVER_fabsf(f); } +float fabsf(float f) +{ + return __CPROVER_fabsf(f); +} /* FUNCTION: __builtin_fabs */ -double __builtin_fabs(double d) { return __CPROVER_fabs(d); } +double __builtin_fabs(double d) +{ + return __CPROVER_fabs(d); +} /* FUNCTION: __builtin_fabsl */ -long double __builtin_fabsl(long double d) { return __CPROVER_fabsl(d); } +long double __builtin_fabsl(long double d) +{ + return __CPROVER_fabsl(d); +} /* FUNCTION: __builtin_fabsf */ -float __builtin_fabsf(float f) { return __CPROVER_fabsf(f); } +float __builtin_fabsf(float f) +{ + return __CPROVER_fabsf(f); +} /* FUNCTION: __CPROVER_isgreaterf */ @@ -98,137 +116,233 @@ int __finitel(long double ld) { return __CPROVER_isfiniteld(ld); } #undef isinf -int isinf(double d) { return __CPROVER_isinfd(d); } +int isinf(double d) +{ + return __CPROVER_isinfd(d); +} /* FUNCTION: __isinf */ -int __isinf(double d) { return __CPROVER_isinfd(d); } +int __isinf(double d) +{ + return __CPROVER_isinfd(d); +} /* FUNCTION: isinff */ -int isinff(float f) { return __CPROVER_isinff(f); } +int isinff(float f) +{ + return __CPROVER_isinff(f); +} /* FUNCTION: __isinff */ -int __isinff(float f) { return __CPROVER_isinff(f); } +int __isinff(float f) +{ + return __CPROVER_isinff(f); +} /* FUNCTION: isinfl */ -int isinfl(long double ld) { return __CPROVER_isinfld(ld); } +int isinfl(long double ld) +{ + return __CPROVER_isinfld(ld); +} /* FUNCTION: __isinfl */ -int __isinfl(long double ld) { return __CPROVER_isinfld(ld); } +int __isinfl(long double ld) +{ + return __CPROVER_isinfld(ld); +} /* FUNCTION: isnan */ #undef isnan -int isnan(double d) { return __CPROVER_isnand(d); } +int isnan(double d) +{ + return __CPROVER_isnand(d); +} /* FUNCTION: __isnan */ -int __isnan(double d) { return __CPROVER_isnand(d); } +int __isnan(double d) +{ + return __CPROVER_isnand(d); +} /* FUNCTION: __isnanf */ -int __isnanf(float f) { return __CPROVER_isnanf(f); } +int __isnanf(float f) +{ + return __CPROVER_isnanf(f); +} /* FUNCTION: isnanf */ -int isnanf(float f) { return __CPROVER_isnanf(f); } +int isnanf(float f) +{ + return __CPROVER_isnanf(f); +} /* FUNCTION: isnanl */ -int isnanl(long double ld) { return __CPROVER_isnanld(ld); } +int isnanl(long double ld) +{ + return __CPROVER_isnanld(ld); +} /* FUNCTION: __isnanl */ -int __isnanl(long double ld) { return __CPROVER_isnanld(ld); } +int __isnanl(long double ld) +{ + return __CPROVER_isnanld(ld); +} /* FUNCTION: isnormal */ #undef isnormal -int isnormal(double d) { return __CPROVER_isnormald(d); } +int isnormal(double d) +{ + return __CPROVER_isnormald(d); +} /* FUNCTION: __isnormalf */ -int __isnormalf(float f) { return __CPROVER_isnormalf(f); } +int __isnormalf(float f) +{ + return __CPROVER_isnormalf(f); +} /* FUNCTION: __builtin_inff */ -float __builtin_inff(void) { return 1.0f/0.0f; } +float __builtin_inff(void) +{ + return 1.0f / 0.0f; +} /* FUNCTION: __builtin_inf */ -double __builtin_inf(void) { return 1.0/0.0; } +double __builtin_inf(void) +{ + return 1.0 / 0.0; +} /* FUNCTION: __builtin_infl */ -long double __builtin_infl(void) { return 1.0l/0.0l; } +long double __builtin_infl(void) +{ + return 1.0l / 0.0l; +} /* FUNCTION: __builtin_isinf */ -int __builtin_isinf(double d) { return __CPROVER_isinfd(d); } +int __builtin_isinf(double d) +{ + return __CPROVER_isinfd(d); +} /* FUNCTION: __builtin_isinff */ -int __builtin_isinff(float f) { return __CPROVER_isinff(f); } +int __builtin_isinff(float f) +{ + return __CPROVER_isinff(f); +} /* FUNCTION: __builtin_isinf */ -int __builtin_isinfl(long double ld) { return __CPROVER_isinfld(ld); } +int __builtin_isinfl(long double ld) +{ + return __CPROVER_isinfld(ld); +} /* FUNCTION: __builtin_isnan */ -int __builtin_isnan(double d) { return __CPROVER_isnand(d); } +int __builtin_isnan(double d) +{ + return __CPROVER_isnand(d); +} /* FUNCTION: __builtin_isnanf */ -int __builtin_isnanf(float f) { return __CPROVER_isnanf(f); } +int __builtin_isnanf(float f) +{ + return __CPROVER_isnanf(f); +} /* FUNCTION: __builtin_huge_valf */ -float __builtin_huge_valf(void) { return 1.0f/0.0f; } +float __builtin_huge_valf(void) +{ + return 1.0f / 0.0f; +} /* FUNCTION: __builtin_huge_val */ -double __builtin_huge_val(void) { return 1.0/0.0; } +double __builtin_huge_val(void) +{ + return 1.0 / 0.0; +} /* FUNCTION: __builtin_huge_vall */ -long double __builtin_huge_vall(void) { return 1.0l/0.0l; } +long double __builtin_huge_vall(void) +{ + return 1.0l / 0.0l; +} /* FUNCTION: _dsign */ -int _dsign(double d) { return __CPROVER_signd(d); } +int _dsign(double d) +{ + return __CPROVER_signd(d); +} /* FUNCTION: _ldsign */ -int _ldsign(long double ld) { return __CPROVER_signld(ld); } +int _ldsign(long double ld) +{ + return __CPROVER_signld(ld); +} /* FUNCTION: _fdsign */ -int _fdsign(float f) { return __CPROVER_signf(f); } +int _fdsign(float f) +{ + return __CPROVER_signf(f); +} /* FUNCTION: signbit */ #undef signbit -int signbit(double d) { return __CPROVER_signd(d); } +int signbit(double d) +{ + return __CPROVER_signd(d); +} /* FUNCTION: __signbitd */ -int __signbitd(double d) { return __CPROVER_signd(d); } +int __signbitd(double d) +{ + return __CPROVER_signd(d); +} /* FUNCTION: __signbitf */ -int __signbitf(float f) { return __CPROVER_signf(f); } +int __signbitf(float f) +{ + return __CPROVER_signf(f); +} /* FUNCTION: __signbit */ -int __signbit(double ld) { return __CPROVER_signld(ld); } +int __signbit(double ld) +{ + return __CPROVER_signld(ld); +} /* FUNCTION: _dclass */ @@ -237,8 +351,9 @@ int __signbit(double ld) { return __CPROVER_signld(ld); } #define __CPROVER_MATH_H_INCLUDED #endif -short _dclass(double d) { - __CPROVER_HIDE: +short _dclass(double d) +{ +__CPROVER_HIDE: return __CPROVER_isnand(d)?FP_NAN: __CPROVER_isinfd(d)?FP_INFINITE: d==0?FP_ZERO: @@ -253,8 +368,9 @@ short _dclass(double d) { #define __CPROVER_MATH_H_INCLUDED #endif -short _ldclass(long double ld) { - __CPROVER_HIDE: +short _ldclass(long double ld) +{ +__CPROVER_HIDE: return __CPROVER_isnanld(ld)?FP_NAN: __CPROVER_isinfld(ld)?FP_INFINITE: ld==0?FP_ZERO: @@ -269,8 +385,9 @@ short _ldclass(long double ld) { #define __CPROVER_MATH_H_INCLUDED #endif -short _fdclass(float f) { - __CPROVER_HIDE: +short _fdclass(float f) +{ +__CPROVER_HIDE: return __CPROVER_isnanf(f)?FP_NAN: __CPROVER_isinff(f)?FP_INFINITE: f==0?FP_ZERO: @@ -285,10 +402,11 @@ short _fdclass(float f) { #define __CPROVER_MATH_H_INCLUDED #endif -int __fpclassifyd(double d) { - __CPROVER_HIDE: - return __CPROVER_fpclassify( - FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); +int __fpclassifyd(double d) +{ +__CPROVER_HIDE: + return __CPROVER_fpclassify( + FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); } /* FUNCTION: __fpclassifyf */ @@ -298,10 +416,11 @@ int __fpclassifyd(double d) { #define __CPROVER_MATH_H_INCLUDED #endif -int __fpclassifyf(float f) { - __CPROVER_HIDE: - return __CPROVER_fpclassify( - FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f); +int __fpclassifyf(float f) +{ +__CPROVER_HIDE: + return __CPROVER_fpclassify( + FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f); } /* FUNCTION: __fpclassifyl */ @@ -311,10 +430,11 @@ int __fpclassifyf(float f) { #define __CPROVER_MATH_H_INCLUDED #endif -int __fpclassifyl(long double f) { - __CPROVER_HIDE: - return __CPROVER_fpclassify( - FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f); +int __fpclassifyl(long double f) +{ +__CPROVER_HIDE: + return __CPROVER_fpclassify( + FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f); } /* FUNCTION: __fpclassify */ @@ -328,16 +448,18 @@ int __fpclassifyl(long double f) { // only; newer ones use __fpclassifyd. #ifdef __APPLE__ -int __fpclassify(long double d) { - __CPROVER_HIDE: - return __CPROVER_fpclassify( - FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); +int __fpclassify(long double d) +{ +__CPROVER_HIDE: + return __CPROVER_fpclassify( + FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); } #else -int __fpclassify(double d) { - __CPROVER_HIDE: - return __CPROVER_fpclassify( - FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); +int __fpclassify(double d) +{ +__CPROVER_HIDE: + return __CPROVER_fpclassify( + FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); } #endif diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index d93bf2e5f05..5155a42e6c3 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -74,7 +74,8 @@ void pthread_mutex_cleanup(void *p) #endif int pthread_mutex_init( - pthread_mutex_t *mutex, const pthread_mutexattr_t *mutexattr) + pthread_mutex_t *mutex, + const pthread_mutexattr_t *mutexattr) { __CPROVER_HIDE:; *((__CPROVER_mutex_t *)mutex)=0; @@ -428,7 +429,8 @@ void pthread_rwlock_cleanup(void *p) } #endif -int pthread_rwlock_init(pthread_rwlock_t *lock, +int pthread_rwlock_init( + pthread_rwlock_t *lock, const pthread_rwlockattr_t *attr) { __CPROVER_HIDE:; @@ -610,10 +612,10 @@ void __spawned_thread( void *arg); int pthread_create( - pthread_t *thread, // must not be null - const pthread_attr_t *attr, // may be null - void * (*start_routine)(void *), // must not be null - void *arg) // may be null + pthread_t *thread, // must not be null + const pthread_attr_t *attr, // may be null + void *(*start_routine)(void *), // must not be null + void *arg) // may be null { __CPROVER_HIDE:; unsigned long this_thread_id; @@ -659,9 +661,7 @@ int pthread_create( #define __CPROVER_PTHREAD_H_INCLUDED #endif -int pthread_cond_init( - pthread_cond_t *cond, - const pthread_condattr_t *attr) +int pthread_cond_init(pthread_cond_t *cond, const pthread_condattr_t *attr) { __CPROVER_HIDE: *((unsigned *)cond)=0; if(attr) (void)*attr; @@ -675,8 +675,7 @@ int pthread_cond_init( #define __CPROVER_PTHREAD_H_INCLUDED #endif -int pthread_cond_signal( - pthread_cond_t *cond) +int pthread_cond_signal(pthread_cond_t *cond) { __CPROVER_HIDE: __CPROVER_atomic_begin(); (*((unsigned *)cond))++; @@ -691,8 +690,7 @@ int pthread_cond_signal( #define __CPROVER_PTHREAD_H_INCLUDED #endif -int pthread_cond_broadcast( - pthread_cond_t *cond) +int pthread_cond_broadcast(pthread_cond_t *cond) { __CPROVER_HIDE: __CPROVER_atomic_begin(); *((unsigned *)cond)=(unsigned)-1; @@ -707,9 +705,7 @@ int pthread_cond_broadcast( #define __CPROVER_PTHREAD_H_INCLUDED #endif -int pthread_cond_wait( - pthread_cond_t *cond, - pthread_mutex_t *mutex) +int pthread_cond_wait(pthread_cond_t *cond, pthread_mutex_t *mutex) { __CPROVER_HIDE: (void)*mutex; @@ -827,7 +823,8 @@ int __VERIFIER_nondet_int(); #if !defined(__APPLE__) && !defined(__OpenBSD__) int pthread_barrier_init( pthread_barrier_t *restrict barrier, - const pthread_barrierattr_t *restrict attr, unsigned count) + const pthread_barrierattr_t *restrict attr, + unsigned count) { __CPROVER_HIDE:; (void)barrier; diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index 4afe29a66c6..0ae97100176 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -159,7 +159,7 @@ __CPROVER_HIDE:; #define __CPROVER_STDIO_H_INCLUDED #endif -FILE* freopen(const char *filename, const char *mode, FILE *f) +FILE *freopen(const char *filename, const char *mode, FILE *f) { __CPROVER_HIDE:; (void)*filename; @@ -333,11 +333,7 @@ char *fgets(char *str, int size, FILE *stream) char __VERIFIER_nondet_char(); size_t __VERIFIER_nondet_size_t(); -size_t fread( - void *ptr, - size_t size, - size_t nitems, - FILE *stream) +size_t fread(void *ptr, size_t size, size_t nitems, FILE *stream) { __CPROVER_HIDE:; size_t nread=__VERIFIER_nondet_size_t(); diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index ccde0e838b4..1d7e36616dd 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -2,31 +2,49 @@ #undef abs -int abs(int i) { return __CPROVER_abs(i); } +int abs(int i) +{ + return __CPROVER_abs(i); +} /* FUNCTION: labs */ #undef labs -long int labs(long int i) { return __CPROVER_labs(i); } +long int labs(long int i) +{ + return __CPROVER_labs(i); +} /* FUNCTION: llabs */ #undef llabs -long long int llabs(long long int i) { return __CPROVER_llabs(i); } +long long int llabs(long long int i) +{ + return __CPROVER_llabs(i); +} /* FUNCTION: __builtin_abs */ -int __builtin_abs(int i) { return __CPROVER_abs(i); } +int __builtin_abs(int i) +{ + return __CPROVER_abs(i); +} /* FUNCTION: __builtin_labs */ -long int __builtin_labs(long int i) { return __CPROVER_labs(i); } +long int __builtin_labs(long int i) +{ + return __CPROVER_labs(i); +} /* FUNCTION: __builtin_llabs */ -long long int __builtin_llabs(long long int i) { return __CPROVER_llabs(i); } +long long int __builtin_llabs(long long int i) +{ + return __CPROVER_llabs(i); +} /* FUNCTION: exit */ @@ -523,8 +541,10 @@ void *valloc(__CPROVER_size_t malloc_size) #undef posix_memalign void *malloc(__CPROVER_size_t malloc_size); -int -posix_memalign(void **ptr, __CPROVER_size_t alignment, __CPROVER_size_t size) +int posix_memalign( + void **ptr, + __CPROVER_size_t alignment, + __CPROVER_size_t size) { __CPROVER_HIDE:; diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c index 59e31de10b6..ce6aa57bff4 100644 --- a/src/ansi-c/library/string.c +++ b/src/ansi-c/library/string.c @@ -211,7 +211,11 @@ __CPROVER_HIDE:; #define __CPROVER_STRING_H_INCLUDED #endif -char *__builtin___strncpy_chk(char *dst, const char *src, size_t n, size_t object_size) +char *__builtin___strncpy_chk( + char *dst, + const char *src, + size_t n, + size_t object_size) { __CPROVER_HIDE:; #ifdef __CPROVER_STRING_ABSTRACTION diff --git a/src/ansi-c/library/windows.c b/src/ansi-c/library/windows.c index d3a94669300..fdb5864b3f3 100644 --- a/src/ansi-c/library/windows.c +++ b/src/ansi-c/library/windows.c @@ -38,8 +38,7 @@ HANDLE CreateThread( LPTHREAD_START_ROUTINE lpStartAddress, LPVOID lpParameter, DWORD dwCreationFlags, - LPDWORD lpThreadId -) + LPDWORD lpThreadId) { __CPROVER_HIDE:; DWORD thread_id;