Skip to content

Commit 20e7cef

Browse files
committed
fixup! C model library: Support ARM64 va_list types
This extends 4d0164f to uses within `__CPROVER_OBJECT_SIZE`. Fixes: #8357
1 parent 54c20cd commit 20e7cef

File tree

1 file changed

+6
-6
lines changed

1 file changed

+6
-6
lines changed

src/ansi-c/library/stdio.c

+6-6
Original file line numberDiff line numberDiff line change
@@ -1135,7 +1135,7 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
11351135

11361136
(void)*format;
11371137
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
1138-
__CPROVER_OBJECT_SIZE(arg))
1138+
__CPROVER_OBJECT_SIZE(*(void **)&arg))
11391139
{
11401140
void *a = va_arg(arg, void *);
11411141
__CPROVER_havoc_object(a);
@@ -1233,7 +1233,7 @@ int __stdio_common_vfscanf(
12331233

12341234
(void)*format;
12351235
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
1236-
__CPROVER_OBJECT_SIZE(args))
1236+
__CPROVER_OBJECT_SIZE(*(void **)&args))
12371237
{
12381238
void *a = va_arg(args, void *);
12391239
__CPROVER_havoc_object(a);
@@ -1312,7 +1312,7 @@ __CPROVER_HIDE:;
13121312
(void)*s;
13131313
(void)*format;
13141314
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
1315-
__CPROVER_OBJECT_SIZE(arg))
1315+
__CPROVER_OBJECT_SIZE(*(void **)&arg))
13161316
{
13171317
void *a = va_arg(arg, void *);
13181318
__CPROVER_havoc_object(a);
@@ -1388,7 +1388,7 @@ int __stdio_common_vsscanf(
13881388
(void)*s;
13891389
(void)*format;
13901390
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
1391-
__CPROVER_OBJECT_SIZE(args))
1391+
__CPROVER_OBJECT_SIZE(*(void **)&args))
13921392
{
13931393
void *a = va_arg(args, void *);
13941394
__CPROVER_havoc_object(a);
@@ -1774,7 +1774,7 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
17741774
(void)*fmt;
17751775

17761776
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
1777-
__CPROVER_OBJECT_SIZE(ap))
1777+
__CPROVER_OBJECT_SIZE(*(void **)&ap))
17781778

17791779
{
17801780
(void)va_arg(ap, int);
@@ -1822,7 +1822,7 @@ int __builtin___vsnprintf_chk(
18221822
(void)*fmt;
18231823

18241824
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
1825-
__CPROVER_OBJECT_SIZE(ap))
1825+
__CPROVER_OBJECT_SIZE(*(void **)&ap))
18261826

18271827
{
18281828
(void)va_arg(ap, int);

0 commit comments

Comments
 (0)