Skip to content

Commit

Permalink
C library: Apple does not adhere to aarch64 ABI
Browse files Browse the repository at this point in the history
The fix from #8366 must not be used on macOS as that platform still uses
`__builtin_va_list` instead of the ARM-mandated struct.
  • Loading branch information
tautschnig committed Sep 19, 2024
1 parent 5bd494a commit 02322ae
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions src/ansi-c/library/stdio.c
Original file line number Diff line number Diff line change
Expand Up @@ -1134,7 +1134,7 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
}

(void)*format;
# if defined(__aarch64__) || defined(_M_ARM64)
# if (defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
__CPROVER_OBJECT_SIZE(arg.__stack))
{
Expand Down Expand Up @@ -1192,7 +1192,7 @@ __CPROVER_HIDE:;
}

(void)*format;
#if defined(__aarch64__) || defined(_M_ARM64)
#if (defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
__CPROVER_OBJECT_SIZE(arg.__stack))
{
Expand Down Expand Up @@ -1250,7 +1250,7 @@ int __stdio_common_vfscanf(
}

(void)*format;
# if defined(__aarch64__) || defined(_M_ARM64)
# if (defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args.__stack) <
__CPROVER_OBJECT_SIZE(args.__stack))
{
Expand Down Expand Up @@ -1338,7 +1338,7 @@ __CPROVER_HIDE:;
int result = __VERIFIER_nondet_int();
(void)*s;
(void)*format;
# if defined(__aarch64__) || defined(_M_ARM64)
# if (defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
__CPROVER_OBJECT_SIZE(arg.__stack))
{
Expand Down Expand Up @@ -1382,7 +1382,7 @@ __CPROVER_HIDE:;
int result = __VERIFIER_nondet_int();
(void)*s;
(void)*format;
#if defined(__aarch64__) || defined(_M_ARM64)
#if (defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
__CPROVER_OBJECT_SIZE(arg.__stack))
{
Expand Down Expand Up @@ -1432,7 +1432,7 @@ int __stdio_common_vsscanf(

(void)*s;
(void)*format;
# if defined(__aarch64__) || defined(_M_ARM64)
# if (defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args.__stack) <
__CPROVER_OBJECT_SIZE(args.__stack))
{
Expand Down Expand Up @@ -1827,7 +1827,7 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
{
(void)*fmt;

#if defined(__aarch64__) || defined(_M_ARM64)
#if (defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
__CPROVER_OBJECT_SIZE(ap.__stack))

Expand Down Expand Up @@ -1887,7 +1887,7 @@ int __builtin___vsnprintf_chk(
(void)bufsize;
(void)*fmt;

#if defined(__aarch64__) || defined(_M_ARM64)
#if (defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
__CPROVER_OBJECT_SIZE(ap.__stack))

Expand Down

0 comments on commit 02322ae

Please sign in to comment.