Skip to content

Commit d927b47

Browse files
authored
Merge pull request #7863 from adpaco-aws/issue-7862
Fix `va_list` types for `__CPROVER_OBJECT_SIZE` in ARM64 Linux
2 parents d61bffc + 9a0c662 commit d927b47

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/ansi-c/library/stdio.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1047,7 +1047,7 @@ __CPROVER_HIDE:;
10471047

10481048
(void)*format;
10491049
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
1050-
__CPROVER_OBJECT_SIZE(arg))
1050+
__CPROVER_OBJECT_SIZE(*(void **)&arg))
10511051
{
10521052
void *a = va_arg(arg, void *);
10531053
__CPROVER_havoc_object(a);
@@ -1210,7 +1210,7 @@ __CPROVER_HIDE:;
12101210
(void)*s;
12111211
(void)*format;
12121212
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
1213-
__CPROVER_OBJECT_SIZE(arg))
1213+
__CPROVER_OBJECT_SIZE(*(void **)&arg))
12141214
{
12151215
void *a = va_arg(arg, void *);
12161216
__CPROVER_havoc_object(a);

0 commit comments

Comments
 (0)