Merge pull request #7521 from tautschnig/bugfixes/7423-va_list

tautschnig · web-flow · commit 669baae97ef1 · 2023-02-07T14:43:08.000+01:00
C model library: Support ARM64 va_list types
diff --git 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 *);

Original file line number	Diff line number	Diff line change
`@@ -997,7 +997,7 @@ int vfscanf(FILE restrict stream, const char restrict format, va_list arg)`
`997`	`997`	`}`
`998`	`998`
`999`	`999`	`(void)*format;`
`1000`		`- while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <`
	`1000`	`+ while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET((void *)&arg) <`
`1001`	`1001`	`__CPROVER_OBJECT_SIZE(arg))`
`1002`	`1002`	`{`
`1003`	`1003`	`void a = va_arg(arg, void );`
`@@ -1046,7 +1046,7 @@ __CPROVER_HIDE:;`
`1046`	`1046`	`}`
`1047`	`1047`
`1048`	`1048`	`(void)*format;`
`1049`		`- while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <`
	`1049`	`+ while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET((void *)&arg) <`
`1050`	`1050`	`__CPROVER_OBJECT_SIZE(arg))`
`1051`	`1051`	`{`
`1052`	`1052`	`void a = va_arg(arg, void );`
`@@ -1095,7 +1095,7 @@ int __stdio_common_vfscanf(`
`1095`	`1095`	`}`
`1096`	`1096`
`1097`	`1097`	`(void)*format;`
`1098`		`- while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <`
	`1098`	`+ while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET((void *)&args) <`
`1099`	`1099`	`__CPROVER_OBJECT_SIZE(args))`
`1100`	`1100`	`{`
`1101`	`1101`	`void a = va_arg(args, void );`
`@@ -1174,7 +1174,7 @@ __CPROVER_HIDE:;`
`1174`	`1174`	`int result = __VERIFIER_nondet_int();`
`1175`	`1175`	`(void)*s;`
`1176`	`1176`	`(void)*format;`
`1177`		`- while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <`
	`1177`	`+ while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET((void *)&arg) <`
`1178`	`1178`	`__CPROVER_OBJECT_SIZE(arg))`
`1179`	`1179`	`{`
`1180`	`1180`	`void a = va_arg(arg, void );`
`@@ -1209,7 +1209,7 @@ __CPROVER_HIDE:;`
`1209`	`1209`	`int result = __VERIFIER_nondet_int();`
`1210`	`1210`	`(void)*s;`
`1211`	`1211`	`(void)*format;`
`1212`		`- while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <`
	`1212`	`+ while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET((void *)&arg) <`
`1213`	`1213`	`__CPROVER_OBJECT_SIZE(arg))`
`1214`	`1214`	`{`
`1215`	`1215`	`void a = va_arg(arg, void );`
`@@ -1250,7 +1250,7 @@ int __stdio_common_vsscanf(`
`1250`	`1250`
`1251`	`1251`	`(void)*s;`
`1252`	`1252`	`(void)*format;`
`1253`		`- while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <`
	`1253`	`+ while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET((void *)&args) <`
`1254`	`1254`	`__CPROVER_OBJECT_SIZE(args))`
`1255`	`1255`	`{`
`1256`	`1256`	`void a = va_arg(args, void );`