From f211714f92c89b2fe6491963df00315f301de2c0 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 15 Apr 2021 10:25:47 +0200
Subject: [PATCH] [printer] use __restrict when in MSVC mode
also consider `restrict` as a keyword for pretty-printing purposes.
---
.../ast_printing/cil_printer.ml | 7 +-
tests/libc/oracle/inttypes_h.7.res.oracle | 336 +++++++++---------
2 files changed, 174 insertions(+), 169 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index c08d6b3660c..7034e9cd0ea 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2126,7 +2126,12 @@ class cil_printer () = object (self)
| "thread", [] when not (Cil.msvcMode ()) -> fprintf fmt "__thread"; false
| "volatile", [] -> self#pp_keyword fmt "volatile"; false
| "ghost", [] -> self#pp_keyword fmt "\\ghost"; false
- | "restrict", [] -> fprintf fmt "restrict"; false
+ | "restrict", [] ->
+ if Cil.msvcMode () then
+ fprintf fmt "__restrict"
+ else
+ self#pp_keyword fmt "restrict";
+ false
| "missingproto", [] ->
if self#display_comment () then fprintf fmt "/* missing proto */";
false
diff --git a/tests/libc/oracle/inttypes_h.7.res.oracle b/tests/libc/oracle/inttypes_h.7.res.oracle
index e631fbefe41..9dfd0ff2a95 100644
--- a/tests/libc/oracle/inttypes_h.7.res.oracle
+++ b/tests/libc/oracle/inttypes_h.7.res.oracle
@@ -21,7 +21,7 @@
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_1(char const * restrict format, signed char *param0);
+int scanf_va_1(char const * __restrict format, signed char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -34,7 +34,7 @@ int scanf_va_1(char const * restrict format, signed char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_1(char const * restrict format, int param0);
+int printf_va_1(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -51,7 +51,7 @@ int printf_va_1(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_2(char const * restrict format, signed char *param0);
+int scanf_va_2(char const * __restrict format, signed char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -64,7 +64,7 @@ int scanf_va_2(char const * restrict format, signed char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_2(char const * restrict format, int param0);
+int printf_va_2(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -81,7 +81,7 @@ int printf_va_2(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_3(char const * restrict format, unsigned char *param0);
+int scanf_va_3(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -94,7 +94,7 @@ int scanf_va_3(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_3(char const * restrict format, int param0);
+int printf_va_3(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -111,7 +111,7 @@ int printf_va_3(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_4(char const * restrict format, unsigned char *param0);
+int scanf_va_4(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -124,7 +124,7 @@ int scanf_va_4(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_4(char const * restrict format, int param0);
+int printf_va_4(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -141,7 +141,7 @@ int printf_va_4(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_5(char const * restrict format, unsigned char *param0);
+int scanf_va_5(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -154,7 +154,7 @@ int scanf_va_5(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_5(char const * restrict format, int param0);
+int printf_va_5(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -171,7 +171,7 @@ int printf_va_5(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_6(char const * restrict format, unsigned char *param0);
+int scanf_va_6(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -184,7 +184,7 @@ int scanf_va_6(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_6(char const * restrict format, int param0);
+int printf_va_6(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -201,7 +201,7 @@ int printf_va_6(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_7(char const * restrict format, short *param0);
+int scanf_va_7(char const * __restrict format, short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -214,7 +214,7 @@ int scanf_va_7(char const * restrict format, short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_7(char const * restrict format, int param0);
+int printf_va_7(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -231,7 +231,7 @@ int printf_va_7(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_8(char const * restrict format, short *param0);
+int scanf_va_8(char const * __restrict format, short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -244,7 +244,7 @@ int scanf_va_8(char const * restrict format, short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_8(char const * restrict format, int param0);
+int printf_va_8(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -261,7 +261,7 @@ int printf_va_8(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_9(char const * restrict format, unsigned short *param0);
+int scanf_va_9(char const * __restrict format, unsigned short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -274,7 +274,7 @@ int scanf_va_9(char const * restrict format, unsigned short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_9(char const * restrict format, int param0);
+int printf_va_9(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -291,7 +291,7 @@ int printf_va_9(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_10(char const * restrict format, unsigned short *param0);
+int scanf_va_10(char const * __restrict format, unsigned short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -304,7 +304,7 @@ int scanf_va_10(char const * restrict format, unsigned short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_10(char const * restrict format, int param0);
+int printf_va_10(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -321,7 +321,7 @@ int printf_va_10(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_11(char const * restrict format, unsigned short *param0);
+int scanf_va_11(char const * __restrict format, unsigned short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -334,7 +334,7 @@ int scanf_va_11(char const * restrict format, unsigned short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_11(char const * restrict format, int param0);
+int printf_va_11(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -351,7 +351,7 @@ int printf_va_11(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_12(char const * restrict format, unsigned short *param0);
+int scanf_va_12(char const * __restrict format, unsigned short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -364,7 +364,7 @@ int scanf_va_12(char const * restrict format, unsigned short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_12(char const * restrict format, int param0);
+int printf_va_12(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -381,7 +381,7 @@ int printf_va_12(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_13(char const * restrict format, int *param0);
+int scanf_va_13(char const * __restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -394,7 +394,7 @@ int scanf_va_13(char const * restrict format, int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_13(char const * restrict format, int param0);
+int printf_va_13(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -411,7 +411,7 @@ int printf_va_13(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_14(char const * restrict format, int *param0);
+int scanf_va_14(char const * __restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -424,7 +424,7 @@ int scanf_va_14(char const * restrict format, int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_14(char const * restrict format, int param0);
+int printf_va_14(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -441,7 +441,7 @@ int printf_va_14(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_15(char const * restrict format, unsigned int *param0);
+int scanf_va_15(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -454,7 +454,7 @@ int scanf_va_15(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_15(char const * restrict format, unsigned int param0);
+int printf_va_15(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -471,7 +471,7 @@ int printf_va_15(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_16(char const * restrict format, unsigned int *param0);
+int scanf_va_16(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -484,7 +484,7 @@ int scanf_va_16(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_16(char const * restrict format, unsigned int param0);
+int printf_va_16(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -501,7 +501,7 @@ int printf_va_16(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_17(char const * restrict format, unsigned int *param0);
+int scanf_va_17(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -514,7 +514,7 @@ int scanf_va_17(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_17(char const * restrict format, unsigned int param0);
+int printf_va_17(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -531,7 +531,7 @@ int printf_va_17(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_18(char const * restrict format, unsigned int *param0);
+int scanf_va_18(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -544,7 +544,7 @@ int scanf_va_18(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_18(char const * restrict format, unsigned int param0);
+int printf_va_18(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -561,7 +561,7 @@ int printf_va_18(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_19(char const * restrict format, __int64 *param0);
+int scanf_va_19(char const * __restrict format, __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -574,7 +574,7 @@ int scanf_va_19(char const * restrict format, __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_19(char const * restrict format, __int64 param0);
+int printf_va_19(char const * __restrict format, __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -591,7 +591,7 @@ int printf_va_19(char const * restrict format, __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_20(char const * restrict format, __int64 *param0);
+int scanf_va_20(char const * __restrict format, __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -604,7 +604,7 @@ int scanf_va_20(char const * restrict format, __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_20(char const * restrict format, __int64 param0);
+int printf_va_20(char const * __restrict format, __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -621,7 +621,7 @@ int printf_va_20(char const * restrict format, __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_21(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_21(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -634,7 +634,7 @@ int scanf_va_21(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_21(char const * restrict format, unsigned __int64 param0);
+int printf_va_21(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -651,7 +651,7 @@ int printf_va_21(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_22(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_22(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -664,7 +664,7 @@ int scanf_va_22(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_22(char const * restrict format, unsigned __int64 param0);
+int printf_va_22(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -681,7 +681,7 @@ int printf_va_22(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_23(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_23(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -694,7 +694,7 @@ int scanf_va_23(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_23(char const * restrict format, unsigned __int64 param0);
+int printf_va_23(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -711,7 +711,7 @@ int printf_va_23(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_24(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_24(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -724,7 +724,7 @@ int scanf_va_24(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_24(char const * restrict format, unsigned __int64 param0);
+int printf_va_24(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -741,7 +741,7 @@ int printf_va_24(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_25(char const * restrict format, signed char *param0);
+int scanf_va_25(char const * __restrict format, signed char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -754,7 +754,7 @@ int scanf_va_25(char const * restrict format, signed char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_25(char const * restrict format, int param0);
+int printf_va_25(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -771,7 +771,7 @@ int printf_va_25(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_26(char const * restrict format, signed char *param0);
+int scanf_va_26(char const * __restrict format, signed char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -784,7 +784,7 @@ int scanf_va_26(char const * restrict format, signed char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_26(char const * restrict format, int param0);
+int printf_va_26(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -801,7 +801,7 @@ int printf_va_26(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_27(char const * restrict format, unsigned char *param0);
+int scanf_va_27(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -814,7 +814,7 @@ int scanf_va_27(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_27(char const * restrict format, int param0);
+int printf_va_27(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -831,7 +831,7 @@ int printf_va_27(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_28(char const * restrict format, unsigned char *param0);
+int scanf_va_28(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -844,7 +844,7 @@ int scanf_va_28(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_28(char const * restrict format, int param0);
+int printf_va_28(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -861,7 +861,7 @@ int printf_va_28(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_29(char const * restrict format, unsigned char *param0);
+int scanf_va_29(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -874,7 +874,7 @@ int scanf_va_29(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_29(char const * restrict format, int param0);
+int printf_va_29(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -891,7 +891,7 @@ int printf_va_29(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_30(char const * restrict format, unsigned char *param0);
+int scanf_va_30(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -904,7 +904,7 @@ int scanf_va_30(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_30(char const * restrict format, int param0);
+int printf_va_30(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -921,7 +921,7 @@ int printf_va_30(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_31(char const * restrict format, short *param0);
+int scanf_va_31(char const * __restrict format, short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -934,7 +934,7 @@ int scanf_va_31(char const * restrict format, short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_31(char const * restrict format, int param0);
+int printf_va_31(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -951,7 +951,7 @@ int printf_va_31(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_32(char const * restrict format, short *param0);
+int scanf_va_32(char const * __restrict format, short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -964,7 +964,7 @@ int scanf_va_32(char const * restrict format, short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_32(char const * restrict format, int param0);
+int printf_va_32(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -981,7 +981,7 @@ int printf_va_32(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_33(char const * restrict format, unsigned short *param0);
+int scanf_va_33(char const * __restrict format, unsigned short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -994,7 +994,7 @@ int scanf_va_33(char const * restrict format, unsigned short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_33(char const * restrict format, int param0);
+int printf_va_33(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1011,7 +1011,7 @@ int printf_va_33(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_34(char const * restrict format, unsigned short *param0);
+int scanf_va_34(char const * __restrict format, unsigned short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1024,7 +1024,7 @@ int scanf_va_34(char const * restrict format, unsigned short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_34(char const * restrict format, int param0);
+int printf_va_34(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1041,7 +1041,7 @@ int printf_va_34(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_35(char const * restrict format, unsigned short *param0);
+int scanf_va_35(char const * __restrict format, unsigned short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1054,7 +1054,7 @@ int scanf_va_35(char const * restrict format, unsigned short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_35(char const * restrict format, int param0);
+int printf_va_35(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1071,7 +1071,7 @@ int printf_va_35(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_36(char const * restrict format, unsigned short *param0);
+int scanf_va_36(char const * __restrict format, unsigned short *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1084,7 +1084,7 @@ int scanf_va_36(char const * restrict format, unsigned short *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_36(char const * restrict format, int param0);
+int printf_va_36(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1101,7 +1101,7 @@ int printf_va_36(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_37(char const * restrict format, int *param0);
+int scanf_va_37(char const * __restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1114,7 +1114,7 @@ int scanf_va_37(char const * restrict format, int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_37(char const * restrict format, int param0);
+int printf_va_37(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1131,7 +1131,7 @@ int printf_va_37(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_38(char const * restrict format, int *param0);
+int scanf_va_38(char const * __restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1144,7 +1144,7 @@ int scanf_va_38(char const * restrict format, int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_38(char const * restrict format, int param0);
+int printf_va_38(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1161,7 +1161,7 @@ int printf_va_38(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_39(char const * restrict format, unsigned int *param0);
+int scanf_va_39(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1174,7 +1174,7 @@ int scanf_va_39(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_39(char const * restrict format, unsigned int param0);
+int printf_va_39(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1191,7 +1191,7 @@ int printf_va_39(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_40(char const * restrict format, unsigned int *param0);
+int scanf_va_40(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1204,7 +1204,7 @@ int scanf_va_40(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_40(char const * restrict format, unsigned int param0);
+int printf_va_40(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1221,7 +1221,7 @@ int printf_va_40(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_41(char const * restrict format, unsigned int *param0);
+int scanf_va_41(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1234,7 +1234,7 @@ int scanf_va_41(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_41(char const * restrict format, unsigned int param0);
+int printf_va_41(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1251,7 +1251,7 @@ int printf_va_41(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_42(char const * restrict format, unsigned int *param0);
+int scanf_va_42(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1264,7 +1264,7 @@ int scanf_va_42(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_42(char const * restrict format, unsigned int param0);
+int printf_va_42(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1281,7 +1281,7 @@ int printf_va_42(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_43(char const * restrict format, __int64 *param0);
+int scanf_va_43(char const * __restrict format, __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1294,7 +1294,7 @@ int scanf_va_43(char const * restrict format, __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_43(char const * restrict format, __int64 param0);
+int printf_va_43(char const * __restrict format, __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1311,7 +1311,7 @@ int printf_va_43(char const * restrict format, __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_44(char const * restrict format, __int64 *param0);
+int scanf_va_44(char const * __restrict format, __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1324,7 +1324,7 @@ int scanf_va_44(char const * restrict format, __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_44(char const * restrict format, __int64 param0);
+int printf_va_44(char const * __restrict format, __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1341,7 +1341,7 @@ int printf_va_44(char const * restrict format, __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_45(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_45(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1354,7 +1354,7 @@ int scanf_va_45(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_45(char const * restrict format, unsigned __int64 param0);
+int printf_va_45(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1371,7 +1371,7 @@ int printf_va_45(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_46(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_46(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1384,7 +1384,7 @@ int scanf_va_46(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_46(char const * restrict format, unsigned __int64 param0);
+int printf_va_46(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1401,7 +1401,7 @@ int printf_va_46(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_47(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_47(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1414,7 +1414,7 @@ int scanf_va_47(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_47(char const * restrict format, unsigned __int64 param0);
+int printf_va_47(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1431,7 +1431,7 @@ int printf_va_47(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_48(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_48(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1444,7 +1444,7 @@ int scanf_va_48(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_48(char const * restrict format, unsigned __int64 param0);
+int printf_va_48(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1461,7 +1461,7 @@ int printf_va_48(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_49(char const * restrict format, signed char *param0);
+int scanf_va_49(char const * __restrict format, signed char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1474,7 +1474,7 @@ int scanf_va_49(char const * restrict format, signed char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_49(char const * restrict format, int param0);
+int printf_va_49(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1491,7 +1491,7 @@ int printf_va_49(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_50(char const * restrict format, signed char *param0);
+int scanf_va_50(char const * __restrict format, signed char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1504,7 +1504,7 @@ int scanf_va_50(char const * restrict format, signed char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_50(char const * restrict format, int param0);
+int printf_va_50(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1521,7 +1521,7 @@ int printf_va_50(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_51(char const * restrict format, unsigned char *param0);
+int scanf_va_51(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1534,7 +1534,7 @@ int scanf_va_51(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_51(char const * restrict format, int param0);
+int printf_va_51(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1551,7 +1551,7 @@ int printf_va_51(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_52(char const * restrict format, unsigned char *param0);
+int scanf_va_52(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1564,7 +1564,7 @@ int scanf_va_52(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_52(char const * restrict format, int param0);
+int printf_va_52(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1581,7 +1581,7 @@ int printf_va_52(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_53(char const * restrict format, unsigned char *param0);
+int scanf_va_53(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1594,7 +1594,7 @@ int scanf_va_53(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_53(char const * restrict format, int param0);
+int printf_va_53(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1611,7 +1611,7 @@ int printf_va_53(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_54(char const * restrict format, unsigned char *param0);
+int scanf_va_54(char const * __restrict format, unsigned char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1624,7 +1624,7 @@ int scanf_va_54(char const * restrict format, unsigned char *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_54(char const * restrict format, int param0);
+int printf_va_54(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1641,7 +1641,7 @@ int printf_va_54(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_55(char const * restrict format, int *param0);
+int scanf_va_55(char const * __restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1654,7 +1654,7 @@ int scanf_va_55(char const * restrict format, int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_55(char const * restrict format, int param0);
+int printf_va_55(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1671,7 +1671,7 @@ int printf_va_55(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_56(char const * restrict format, int *param0);
+int scanf_va_56(char const * __restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1684,7 +1684,7 @@ int scanf_va_56(char const * restrict format, int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_56(char const * restrict format, int param0);
+int printf_va_56(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1701,7 +1701,7 @@ int printf_va_56(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_57(char const * restrict format, unsigned int *param0);
+int scanf_va_57(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1714,7 +1714,7 @@ int scanf_va_57(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_57(char const * restrict format, unsigned int param0);
+int printf_va_57(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1731,7 +1731,7 @@ int printf_va_57(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_58(char const * restrict format, unsigned int *param0);
+int scanf_va_58(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1744,7 +1744,7 @@ int scanf_va_58(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_58(char const * restrict format, unsigned int param0);
+int printf_va_58(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1761,7 +1761,7 @@ int printf_va_58(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_59(char const * restrict format, unsigned int *param0);
+int scanf_va_59(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1774,7 +1774,7 @@ int scanf_va_59(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_59(char const * restrict format, unsigned int param0);
+int printf_va_59(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1791,7 +1791,7 @@ int printf_va_59(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_60(char const * restrict format, unsigned int *param0);
+int scanf_va_60(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1804,7 +1804,7 @@ int scanf_va_60(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_60(char const * restrict format, unsigned int param0);
+int printf_va_60(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1821,7 +1821,7 @@ int printf_va_60(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_61(char const * restrict format, int *param0);
+int scanf_va_61(char const * __restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1834,7 +1834,7 @@ int scanf_va_61(char const * restrict format, int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_61(char const * restrict format, int param0);
+int printf_va_61(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1851,7 +1851,7 @@ int printf_va_61(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_62(char const * restrict format, int *param0);
+int scanf_va_62(char const * __restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1864,7 +1864,7 @@ int scanf_va_62(char const * restrict format, int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_62(char const * restrict format, int param0);
+int printf_va_62(char const * __restrict format, int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1881,7 +1881,7 @@ int printf_va_62(char const * restrict format, int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_63(char const * restrict format, unsigned int *param0);
+int scanf_va_63(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1894,7 +1894,7 @@ int scanf_va_63(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_63(char const * restrict format, unsigned int param0);
+int printf_va_63(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1911,7 +1911,7 @@ int printf_va_63(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_64(char const * restrict format, unsigned int *param0);
+int scanf_va_64(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1924,7 +1924,7 @@ int scanf_va_64(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_64(char const * restrict format, unsigned int param0);
+int printf_va_64(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1941,7 +1941,7 @@ int printf_va_64(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_65(char const * restrict format, unsigned int *param0);
+int scanf_va_65(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1954,7 +1954,7 @@ int scanf_va_65(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_65(char const * restrict format, unsigned int param0);
+int printf_va_65(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -1971,7 +1971,7 @@ int printf_va_65(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_66(char const * restrict format, unsigned int *param0);
+int scanf_va_66(char const * __restrict format, unsigned int *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -1984,7 +1984,7 @@ int scanf_va_66(char const * restrict format, unsigned int *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_66(char const * restrict format, unsigned int param0);
+int printf_va_66(char const * __restrict format, unsigned int param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2001,7 +2001,7 @@ int printf_va_66(char const * restrict format, unsigned int param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_67(char const * restrict format, __int64 *param0);
+int scanf_va_67(char const * __restrict format, __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2014,7 +2014,7 @@ int scanf_va_67(char const * restrict format, __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_67(char const * restrict format, __int64 param0);
+int printf_va_67(char const * __restrict format, __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2031,7 +2031,7 @@ int printf_va_67(char const * restrict format, __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_68(char const * restrict format, __int64 *param0);
+int scanf_va_68(char const * __restrict format, __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2044,7 +2044,7 @@ int scanf_va_68(char const * restrict format, __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_68(char const * restrict format, __int64 param0);
+int printf_va_68(char const * __restrict format, __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2061,7 +2061,7 @@ int printf_va_68(char const * restrict format, __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_69(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_69(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2074,7 +2074,7 @@ int scanf_va_69(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_69(char const * restrict format, unsigned __int64 param0);
+int printf_va_69(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2091,7 +2091,7 @@ int printf_va_69(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_70(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_70(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2104,7 +2104,7 @@ int scanf_va_70(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_70(char const * restrict format, unsigned __int64 param0);
+int printf_va_70(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2121,7 +2121,7 @@ int printf_va_70(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_71(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_71(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2134,7 +2134,7 @@ int scanf_va_71(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_71(char const * restrict format, unsigned __int64 param0);
+int printf_va_71(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2151,7 +2151,7 @@ int printf_va_71(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_72(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_72(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2164,7 +2164,7 @@ int scanf_va_72(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_72(char const * restrict format, unsigned __int64 param0);
+int printf_va_72(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2181,7 +2181,7 @@ int printf_va_72(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_73(char const * restrict format, __int64 *param0);
+int scanf_va_73(char const * __restrict format, __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2194,7 +2194,7 @@ int scanf_va_73(char const * restrict format, __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_73(char const * restrict format, __int64 param0);
+int printf_va_73(char const * __restrict format, __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2211,7 +2211,7 @@ int printf_va_73(char const * restrict format, __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_74(char const * restrict format, __int64 *param0);
+int scanf_va_74(char const * __restrict format, __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2224,7 +2224,7 @@ int scanf_va_74(char const * restrict format, __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_74(char const * restrict format, __int64 param0);
+int printf_va_74(char const * __restrict format, __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2241,7 +2241,7 @@ int printf_va_74(char const * restrict format, __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_75(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_75(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2254,7 +2254,7 @@ int scanf_va_75(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_75(char const * restrict format, unsigned __int64 param0);
+int printf_va_75(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2271,7 +2271,7 @@ int printf_va_75(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_76(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_76(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2284,7 +2284,7 @@ int scanf_va_76(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_76(char const * restrict format, unsigned __int64 param0);
+int printf_va_76(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2301,7 +2301,7 @@ int printf_va_76(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_77(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_77(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2314,7 +2314,7 @@ int scanf_va_77(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_77(char const * restrict format, unsigned __int64 param0);
+int printf_va_77(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2331,7 +2331,7 @@ int printf_va_77(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_78(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_78(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2344,7 +2344,7 @@ int scanf_va_78(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_78(char const * restrict format, unsigned __int64 param0);
+int printf_va_78(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2361,7 +2361,7 @@ int printf_va_78(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_79(char const * restrict format, __int64 *param0);
+int scanf_va_79(char const * __restrict format, __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2374,7 +2374,7 @@ int scanf_va_79(char const * restrict format, __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_79(char const * restrict format, __int64 param0);
+int printf_va_79(char const * __restrict format, __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2391,7 +2391,7 @@ int printf_va_79(char const * restrict format, __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_80(char const * restrict format, __int64 *param0);
+int scanf_va_80(char const * __restrict format, __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2404,7 +2404,7 @@ int scanf_va_80(char const * restrict format, __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_80(char const * restrict format, __int64 param0);
+int printf_va_80(char const * __restrict format, __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2421,7 +2421,7 @@ int printf_va_80(char const * restrict format, __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_81(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_81(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2434,7 +2434,7 @@ int scanf_va_81(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_81(char const * restrict format, unsigned __int64 param0);
+int printf_va_81(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2451,7 +2451,7 @@ int printf_va_81(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_82(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_82(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2464,7 +2464,7 @@ int scanf_va_82(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_82(char const * restrict format, unsigned __int64 param0);
+int printf_va_82(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2481,7 +2481,7 @@ int printf_va_82(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_83(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_83(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2494,7 +2494,7 @@ int scanf_va_83(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_83(char const * restrict format, unsigned __int64 param0);
+int printf_va_83(char const * __restrict format, unsigned __int64 param0);
/*@ requires valid_read_string(format);
requires \valid(param0);
@@ -2511,7 +2511,7 @@ int printf_va_83(char const * restrict format, unsigned __int64 param0);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_84(char const * restrict format, unsigned __int64 *param0);
+int scanf_va_84(char const * __restrict format, unsigned __int64 *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -2524,7 +2524,7 @@ int scanf_va_84(char const * restrict format, unsigned __int64 *param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_84(char const * restrict format, unsigned __int64 param0);
+int printf_va_84(char const * __restrict format, unsigned __int64 param0);
int main(void)
{
--
GitLab