Remove "inline" from library models [blocks: #6863]

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

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {

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

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {

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

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {

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

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {

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

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {

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

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {

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

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {

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

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {

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

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 
 int main()
 {

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; }

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;
 }

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 <fenv.h>
 
-inline int fesetround(int rounding_mode)
+int fesetround(int rounding_mode)
 {
 __CPROVER_HIDE:;
   // CPROVER uses the x86 numbering of the rounding modes

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

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,15 +168,15 @@ __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);
 }
 
 /* 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;

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();
 
-inline 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;
@@ -62,9 +61,9 @@ inline int getopt(
 #define __CPROVER_GETOPT_H_INCLUDED
 #endif
 
-inline int getopt_long(
+int getopt_long(
   int argc,
-  char * const argv[],
+  char *const argv[],
   const char *optstring,
   const struct option *longopts,
   int *longindex)