From 4d0164f9d2d879793b435a4bdacb414167543d49 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 4 Feb 2023 19:59:37 +0000 Subject: [PATCH] C model library: Support ARM64 va_list types GCC/ARM appears to uses a struct to represent variadic arguments (where the first component is a pointer to the stack of arguments). Taking the pointer offset requires looking at the first element of this struct, which we do by taking the address, casting to a pointer, and dereferencing. Fixes: #7423 --- src/ansi-c/library/stdio.c | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index ab6ade0db88..fb8dfa09c82 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -997,7 +997,7 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg) } (void)*format; - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) < + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) < __CPROVER_OBJECT_SIZE(arg)) { void *a = va_arg(arg, void *); @@ -1046,7 +1046,7 @@ __CPROVER_HIDE:; } (void)*format; - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) < + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) < __CPROVER_OBJECT_SIZE(arg)) { void *a = va_arg(arg, void *); @@ -1095,7 +1095,7 @@ int __stdio_common_vfscanf( } (void)*format; - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) < + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) < __CPROVER_OBJECT_SIZE(args)) { void *a = va_arg(args, void *); @@ -1174,7 +1174,7 @@ __CPROVER_HIDE:; int result = __VERIFIER_nondet_int(); (void)*s; (void)*format; - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) < + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) < __CPROVER_OBJECT_SIZE(arg)) { void *a = va_arg(arg, void *); @@ -1209,7 +1209,7 @@ __CPROVER_HIDE:; int result = __VERIFIER_nondet_int(); (void)*s; (void)*format; - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) < + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) < __CPROVER_OBJECT_SIZE(arg)) { void *a = va_arg(arg, void *); @@ -1250,7 +1250,7 @@ int __stdio_common_vsscanf( (void)*s; (void)*format; - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) < + while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) < __CPROVER_OBJECT_SIZE(args)) { void *a = va_arg(args, void *);