void __builtin___bnd_chk_ptr_bounds(const void*, __CPROVER_size_t);
void __builtin___bnd_chk_ptr_lbounds(const void*);
void __builtin___bnd_chk_ptr_ubounds(const void*);
void* __builtin___bnd_copy_ptr_bounds(const void*, const void*);
const void* __builtin___bnd_get_ptr_lbound(const void*);
const void* __builtin___bnd_get_ptr_ubound(const void*);
void* __builtin___bnd_init_ptr_bounds(const void*);
void* __builtin___bnd_narrow_ptr_bounds(const void*, const void*, __CPROVER_size_t);
void* __builtin___bnd_null_ptr_bounds(const void*);
void* __builtin___bnd_set_ptr_bounds(const void*, __CPROVER_size_t);
void __builtin___bnd_store_ptr_bounds(void**, const void*);
const void* __builtin___chkp_bndldx(const void*, const void*);
void __builtin___clear_cache(void*, void*);
void* __builtin___memcpy_chk(void*, const void*, __CPROVER_size_t, __CPROVER_size_t);
void* __builtin___memmove_chk(void*, const void*, __CPROVER_size_t, __CPROVER_size_t);
void* __builtin___mempcpy_chk(void*, const void*, __CPROVER_size_t, __CPROVER_size_t);
void* __builtin___memset_chk(void*, int, __CPROVER_size_t, __CPROVER_size_t);
char* __builtin___stpcpy(char *s1, const char *s2);
char* __builtin___stpcpy_chk(char*, const char*, __CPROVER_size_t);
char* __builtin___stpncpy_chk(char*, const char*, __CPROVER_size_t, __CPROVER_size_t);
char* __builtin___strcat_chk(char*, const char*, __CPROVER_size_t);
char* __builtin___strcpy_chk(char*, const char*, __CPROVER_size_t);
char* __builtin___strncat_chk(char*, const char*, __CPROVER_size_t, __CPROVER_size_t);
char* __builtin___strncpy_chk(char*, const char*, __CPROVER_size_t, __CPROVER_size_t);
void* __builtin_aggregate_incoming_address();
void* __builtin_aligned_alloc(__CPROVER_size_t, __CPROVER_size_t);
void* __builtin_alloca(__CPROVER_size_t);
void* __builtin_assume_aligned(const void*, __CPROVER_size_t, ...);
int __builtin_bcmp(const void*, const void*, __CPROVER_size_t);
void __builtin_bcopy(const void*, void*, __CPROVER_size_t);
short unsigned int __builtin_bswap16(short unsigned int);
unsigned int __builtin_bswap32(unsigned int);
long long unsigned int __builtin_bswap64(long long unsigned int);
void __builtin_bzero(void*, __CPROVER_size_t);
void* __builtin_calloc(__CPROVER_size_t, __CPROVER_size_t);
void* __builtin_chkp_memcpy_nobnd(void*, const void*, __CPROVER_size_t);
void* __builtin_chkp_memcpy_nobnd_nochk(void*, const void*, __CPROVER_size_t);
void* __builtin_chkp_memcpy_nochk(void*, const void*, __CPROVER_size_t);
void* __builtin_chkp_memmove_nobnd(void*, const void*, __CPROVER_size_t);
void* __builtin_chkp_memmove_nobnd_nochk(void*, const void*, __CPROVER_size_t);
void* __builtin_chkp_memmove_nochk(void*, const void*, __CPROVER_size_t);
void* __builtin_chkp_mempcpy_nobnd(void*, const void*, __CPROVER_size_t);
void* __builtin_chkp_mempcpy_nobnd_nochk(void*, const void*, __CPROVER_size_t);
void* __builtin_chkp_mempcpy_nochk(void*, const void*, __CPROVER_size_t);
void* __builtin_chkp_memset_nobnd(void*, int, __CPROVER_size_t);
void* __builtin_chkp_memset_nobnd_nochk(void*, int, __CPROVER_size_t);
void* __builtin_chkp_memset_nochk(void*, int, __CPROVER_size_t);
int __builtin_clrsb(int);
int __builtin_clrsbl(long);
int __builtin_clrsbll(long long);
int __builtin_clz(unsigned);
int __builtin_clzl(unsigned long);
int __builtin_clzll(unsigned long long);
int __builtin_ctz(unsigned);
int __builtin_ctzl(unsigned long);
int __builtin_ctzll(unsigned long long);
char* __builtin_dcgettext(const char*, const char*, int);
char* __builtin_dgettext(const char*, const char*);
void* __builtin_extract_return_addr(void*);
int __builtin_ffs(int);
int __builtin_ffsl(long);
int __builtin_ffsll(long long);
void* __builtin_frame_address(unsigned);
void __builtin_free(void*);
void* __builtin_frob_return_addr(void*);
char* __builtin_gettext(const char*);
char* __builtin_index(const char*, int);
int __builtin_isalnum(int);
int __builtin_isalpha(int);
int __builtin_isascii(int);
int __builtin_isblank(int);
int __builtin_iscntrl(int);
int __builtin_isdigit(int);
int __builtin_isgraph(int);
int __builtin_islower(int);
int __builtin_isprint(int);
int __builtin_ispunct(int);
int __builtin_isspace(int);
int __builtin_isupper(int);
int __builtin_isxdigit(int);
void* __builtin_malloc(__CPROVER_size_t);
void* __builtin_memchr(const void*, int, __CPROVER_size_t);
int __builtin_memcmp(const void*, const void*, __CPROVER_size_t);
void* __builtin_memcpy(void*, const void*, __CPROVER_size_t);
void* __builtin_memmove(void*, const void*, __CPROVER_size_t);
void* __builtin_mempcpy(void*, const void*, __CPROVER_size_t);
void* __builtin_memset(void*, int, __CPROVER_size_t);
__CPROVER_size_t __builtin_object_size(const void*, int);
int __builtin_popcount(unsigned);
int __builtin_popcountll(unsigned long long int x);
int __builtin_posix_memalign(void**, __CPROVER_size_t, __CPROVER_size_t);
void __builtin_prefetch(const void*, ...);
void* __builtin_realloc(void*, __CPROVER_size_t);
void* __builtin_return_address(unsigned);
char* __builtin_rindex(const char*, int);
char* __builtin_stpcpy(char*, const char*);
char* __builtin_stpncpy(char*, const char*, __CPROVER_size_t);
int __builtin_strcasecmp(const char*, const char*);
char* __builtin_strcat(char*, const char*);
char* __builtin_strchr(const char*, int);
int __builtin_strcmp(const char*, const char*);
char* __builtin_strcpy(char*, const char*);
__CPROVER_size_t __builtin_strcspn(const char*, const char*);
char* __builtin_strdup(const char*);
__CPROVER_size_t __builtin_strftime(char*, __CPROVER_size_t, const char*, const struct tm*);
__CPROVER_size_t __builtin_strlen(const char*);
int __builtin_strncasecmp(const char*, const char*, __CPROVER_size_t);
char* __builtin_strncat(char*, const char*, __CPROVER_size_t);
int __builtin_strncmp(const char*, const char*, __CPROVER_size_t);
char* __builtin_strncpy(char*, const char*, __CPROVER_size_t);
char* __builtin_strndup(const char*, __CPROVER_size_t);
char* __builtin_strpbrk(const char*, const char*);
char* __builtin_strrchr(const char*, int);
__CPROVER_size_t __builtin_strspn(const char*, const char*);
char* __builtin_strstr(const char*, const char*);
int __builtin_toascii(int);
int __builtin_tolower(int);
int __builtin_toupper(int);
