Commit f939f27c authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

sync with frama-c master; add specs for recursive calls in ioccc

parent 32a85dbb
Pipeline #34583 failed with stage
in 19 minutes and 47 seconds
......@@ -15,4 +15,4 @@ directory file line function property kind status property
. 2048.c 249 addRandom initialization Unknown \initialized(&list[r][0])
. 2048.c 250 addRandom initialization Unknown \initialized(&list[r][1])
. 2048.c 287 setBufferedInput initialization Unknown \initialized(&new.c_lflag)
FRAMAC_SHARE/libc string.h 125 strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 128 strlen precondition Unknown valid_string_s: valid_read_string(s)
......@@ -24,8 +24,8 @@ uint8_t scheme = (unsigned char)0;
assigns *(s + (0 ..))
\from (indirect: n), (indirect: *(format + (0 ..))), param1, param0;
*/
int snprintf_va_1(char * __restrict s, size_t n,
char const * __restrict format, int param0, int param1);
int snprintf_va_1(char * restrict s, size_t n, char const * restrict format,
int param0, int param1);
void getColor(uint8_t value, char *color, size_t length)
{
......@@ -158,7 +158,7 @@ void getColor(uint8_t value, char *color, size_t length)
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_1(char const * __restrict format);
int printf_va_1(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -171,7 +171,7 @@ int printf_va_1(char const * __restrict format);
__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_read_string(param0);
......@@ -185,7 +185,7 @@ int printf_va_2(char const * __restrict format, int param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
*(param0 + (0 ..));
*/
int printf_va_3(char const * __restrict format, char *param0);
int printf_va_3(char const * restrict format, char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -197,7 +197,7 @@ int printf_va_3(char const * __restrict format, char *param0);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_4(char const * __restrict format);
int printf_va_4(char const * restrict format);
/*@ requires valid_read_string(format);
requires valid_read_string(param0);
......@@ -211,7 +211,7 @@ int printf_va_4(char const * __restrict format);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
*(param0 + (0 ..));
*/
int printf_va_5(char const * __restrict format, char *param0);
int printf_va_5(char const * restrict format, char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -223,7 +223,7 @@ int printf_va_5(char const * __restrict format, char *param0);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_6(char const * __restrict format);
int printf_va_6(char const * restrict format);
/*@ requires valid_read_string(format);
requires valid_read_string(param0);
......@@ -237,7 +237,7 @@ int printf_va_6(char const * __restrict format);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
*(param0 + (0 ..));
*/
int printf_va_7(char const * __restrict format, char *param0);
int printf_va_7(char const * restrict format, char *param0);
/*@ requires
\valid(s + (0 .. n - 1)) ∨
......@@ -249,8 +249,8 @@ int printf_va_7(char const * __restrict format, char *param0);
assigns *(s + (0 ..))
\from (indirect: n), (indirect: *(format + (0 ..))), param0;
*/
int snprintf_va_2(char * __restrict s, size_t n,
char const * __restrict format, unsigned int param0);
int snprintf_va_2(char * restrict s, size_t n, char const * restrict format,
unsigned int param0);
/*@ requires valid_read_string(format);
requires valid_read_string(param4);
......@@ -269,7 +269,7 @@ int snprintf_va_2(char * __restrict s, size_t n,
*(param4 + (0 ..)), param3, *(param2 + (0 ..)),
*(param1 + (0 ..)), param0;
*/
int printf_va_8(char const * __restrict format, int param0, char *param1,
int printf_va_8(char const * restrict format, int param0, char *param1,
char *param2, int param3, char *param4);
/*@ requires valid_read_string(format);
......@@ -282,7 +282,7 @@ int printf_va_8(char const * __restrict format, int param0, char *param1,
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_9(char const * __restrict format);
int printf_va_9(char const * restrict format);
/*@ requires valid_read_string(format);
requires valid_read_string(param0);
......@@ -296,7 +296,7 @@ int printf_va_9(char const * __restrict format);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
*(param0 + (0 ..));
*/
int printf_va_10(char const * __restrict format, char *param0);
int printf_va_10(char const * restrict format, char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -308,7 +308,7 @@ int printf_va_10(char const * __restrict format, char *param0);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_11(char const * __restrict format);
int printf_va_11(char const * restrict format);
/*@ requires valid_read_string(format);
requires valid_read_string(param0);
......@@ -322,7 +322,7 @@ int printf_va_11(char const * __restrict format);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
*(param0 + (0 ..));
*/
int printf_va_12(char const * __restrict format, char *param0);
int printf_va_12(char const * restrict format, char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -334,7 +334,7 @@ int printf_va_12(char const * __restrict format, char *param0);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_13(char const * __restrict format);
int printf_va_13(char const * restrict format);
/*@ requires valid_read_string(format);
requires valid_read_string(param0);
......@@ -348,7 +348,7 @@ int printf_va_13(char const * __restrict format);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
*(param0 + (0 ..));
*/
int printf_va_14(char const * __restrict format, char *param0);
int printf_va_14(char const * restrict format, char *param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -360,7 +360,7 @@ int printf_va_14(char const * __restrict format, char *param0);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_15(char const * __restrict format);
int printf_va_15(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -372,7 +372,7 @@ int printf_va_15(char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_16(char const * __restrict format);
int printf_va_16(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -384,7 +384,7 @@ int printf_va_16(char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_17(char const * __restrict format);
int printf_va_17(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -396,9 +396,9 @@ int printf_va_17(char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_18(char const * __restrict format);
int printf_va_18(char const * restrict format);
void drawBoard(uint8_t (* /*[4]*/ board)[4])
void drawBoard(uint8_t board[4][4])
{
uint8_t x;
uint8_t y;
......@@ -454,7 +454,7 @@ void drawBoard(uint8_t (* /*[4]*/ board)[4])
return;
}
uint8_t findTarget(uint8_t * /*[4]*/ array, uint8_t x, uint8_t stop)
uint8_t findTarget(uint8_t array[4], uint8_t x, uint8_t stop)
{
uint8_t __retres;
uint8_t t;
......@@ -483,7 +483,7 @@ uint8_t findTarget(uint8_t * /*[4]*/ array, uint8_t x, uint8_t stop)
return_label: return __retres;
}
_Bool slideArray(uint8_t * /*[4]*/ array)
_Bool slideArray(uint8_t array[4])
{
uint8_t x;
uint8_t t;
......@@ -510,7 +510,7 @@ _Bool slideArray(uint8_t * /*[4]*/ array)
return success;
}
void rotateBoard(uint8_t (* /*[4]*/ board)[4])
void rotateBoard(uint8_t board[4][4])
{
uint8_t i;
uint8_t j;
......@@ -534,7 +534,7 @@ void rotateBoard(uint8_t (* /*[4]*/ board)[4])
return;
}
_Bool moveUp(uint8_t (* /*[4]*/ board)[4])
_Bool moveUp(uint8_t board[4][4])
{
uint8_t x;
_Bool success = (_Bool)0;
......@@ -550,7 +550,7 @@ _Bool moveUp(uint8_t (* /*[4]*/ board)[4])
return success;
}
_Bool moveLeft(uint8_t (* /*[4]*/ board)[4])
_Bool moveLeft(uint8_t board[4][4])
{
_Bool success;
rotateBoard(board);
......@@ -561,7 +561,7 @@ _Bool moveLeft(uint8_t (* /*[4]*/ board)[4])
return success;
}
_Bool moveDown(uint8_t (* /*[4]*/ board)[4])
_Bool moveDown(uint8_t board[4][4])
{
_Bool success;
rotateBoard(board);
......@@ -572,7 +572,7 @@ _Bool moveDown(uint8_t (* /*[4]*/ board)[4])
return success;
}
_Bool moveRight(uint8_t (* /*[4]*/ board)[4])
_Bool moveRight(uint8_t board[4][4])
{
_Bool success;
rotateBoard(board);
......@@ -583,7 +583,7 @@ _Bool moveRight(uint8_t (* /*[4]*/ board)[4])
return success;
}
_Bool findPairDown(uint8_t (* /*[4]*/ board)[4])
_Bool findPairDown(uint8_t board[4][4])
{
_Bool __retres;
uint8_t x;
......@@ -605,7 +605,7 @@ _Bool findPairDown(uint8_t (* /*[4]*/ board)[4])
return_label: return __retres;
}
uint8_t countEmpty(uint8_t (* /*[4]*/ board)[4])
uint8_t countEmpty(uint8_t board[4][4])
{
uint8_t x;
uint8_t y;
......@@ -622,7 +622,7 @@ uint8_t countEmpty(uint8_t (* /*[4]*/ board)[4])
return count;
}
_Bool gameEnded(uint8_t (* /*[4]*/ board)[4])
_Bool gameEnded(uint8_t board[4][4])
{
_Bool __retres;
uint8_t tmp;
......@@ -649,10 +649,10 @@ _Bool gameEnded(uint8_t (* /*[4]*/ board)[4])
return_label: return __retres;
}
void addRandom(uint8_t (* /*[4]*/ board)[4]);
void addRandom(uint8_t board[4][4]);
static _Bool addRandom_initialized = (_Bool)0;
void addRandom(uint8_t (* /*[4]*/ board)[4])
void addRandom(uint8_t board[4][4])
{
uint8_t x;
uint8_t y;
......@@ -695,7 +695,7 @@ void addRandom(uint8_t (* /*[4]*/ board)[4])
return;
}
void initBoard(uint8_t (* /*[4]*/ board)[4])
void initBoard(uint8_t board[4][4])
{
uint8_t x;
uint8_t y;
......@@ -755,7 +755,7 @@ void setBufferedInput(_Bool enable)
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
int printf_va_19(char const * __restrict format, int param0);
int printf_va_19(char const * restrict format, int param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -767,7 +767,7 @@ int printf_va_19(char const * __restrict format, int param0);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_20(char const * __restrict format);
int printf_va_20(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -780,7 +780,7 @@ int printf_va_20(char const * __restrict format);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
int printf_va_21(char const * __restrict format, int param0);
int printf_va_21(char const * restrict format, int param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -792,7 +792,7 @@ int printf_va_21(char const * __restrict format, int param0);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_22(char const * __restrict format);
int printf_va_22(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -805,7 +805,7 @@ int printf_va_22(char const * __restrict format);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
int printf_va_23(char const * __restrict format, int param0);
int printf_va_23(char const * restrict format, int param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -817,7 +817,7 @@ int printf_va_23(char const * __restrict format, int param0);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_24(char const * __restrict format);
int printf_va_24(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -830,7 +830,7 @@ int printf_va_24(char const * __restrict format);
__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);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -842,7 +842,7 @@ int printf_va_25(char const * __restrict format, int param0);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_26(char const * __restrict format);
int printf_va_26(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -855,7 +855,7 @@ int printf_va_26(char const * __restrict format);
__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);
int test(void)
{
......@@ -1034,7 +1034,7 @@ int test(void)
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_28(char const * __restrict format);
int printf_va_28(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -1046,7 +1046,7 @@ int printf_va_28(char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_29(char const * __restrict format);
int printf_va_29(char const * restrict format);
void signal_callback_handler(int signum)
{
......@@ -1067,7 +1067,7 @@ void signal_callback_handler(int signum)
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_30(char const * __restrict format);
int printf_va_30(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -1079,7 +1079,7 @@ int printf_va_30(char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_31(char const * __restrict format);
int printf_va_31(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -1091,7 +1091,7 @@ int printf_va_31(char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_32(char const * __restrict format);
int printf_va_32(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -1103,7 +1103,7 @@ int printf_va_32(char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_33(char const * __restrict format);
int printf_va_33(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -1115,7 +1115,7 @@ int printf_va_33(char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_34(char const * __restrict format);
int printf_va_34(char const * restrict format);
int main(int argc, char **argv)
{
......
......@@ -2,4 +2,4 @@ directory file line function property kind status property
. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s1 + i)
. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s2 + i)
. cwe119.c 65 host_lookup precondition of strcpy Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 352 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 355 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
......@@ -39,7 +39,7 @@ uint32_t nonzero_uint32_t(void)
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
static void validate_addr_form(char *v)
{
......
......@@ -2,4 +2,4 @@ directory file line function property kind status property
. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s1 + i)
. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s2 + i)
. cwe119.c 65 host_lookup precondition of strcpy Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 352 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 355 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
......@@ -39,7 +39,7 @@ uint32_t nonzero_uint32_t(void)
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
static void validate_addr_form(char *v)
{
......
......@@ -17,7 +17,7 @@ int stack_top;
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_1(char const * __restrict format);
int printf_va_1(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
......@@ -34,7 +34,7 @@ int printf_va_1(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_1(char const * __restrict format, int *param0);
int scanf_va_1(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -46,7 +46,7 @@ int scanf_va_1(char const * __restrict format, int *param0);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -58,7 +58,7 @@ int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_2(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -72,7 +72,7 @@ int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param1, param0;
*/
int printf_va_2(char const * __restrict format, int param0, int param1);
int printf_va_2(char const * restrict format, int param0, int param1);
int main(void)
{
......
......@@ -17,7 +17,7 @@ int stack_top;
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_1(char const * __restrict format);
int printf_va_1(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
......@@ -34,7 +34,7 @@ int printf_va_1(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_1(char const * __restrict format, int *param0);
int scanf_va_1(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -46,7 +46,7 @@ int scanf_va_1(char const * __restrict format, int *param0);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -58,7 +58,7 @@ int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_2(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -72,7 +72,7 @@ int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param1, param0;
*/
int printf_va_2(char const * __restrict format, int param0, int param1);
int printf_va_2(char const * restrict format, int param0, int param1);
int main(void)
{
......
......@@ -18,7 +18,7 @@ typedef struct _board_square_t board_square_t;
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_1(char const * __restrict format);
int printf_va_1(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
......@@ -35,7 +35,7 @@ int printf_va_1(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_1(char const * __restrict format, int *param0);
int scanf_va_1(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -47,7 +47,7 @@ int scanf_va_1(char const * __restrict format, int *param0);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -59,7 +59,7 @@ int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_2(char const * __restrict format);
int printf_va_2(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
......@@ -76,7 +76,7 @@ int printf_va_2(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_2(char const * __restrict format, int *param0);
int scanf_va_2(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -88,7 +88,7 @@ int scanf_va_2(char const * __restrict format, int *param0);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_2(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -100,7 +100,7 @@ int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_3(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_3(FILE * restrict stream, char const * restrict format);
int main(void)
{
......
......@@ -18,7 +18,7 @@ typedef struct _board_square_t board_square_t;
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_1(char const * __restrict format);
int printf_va_1(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
......@@ -35,7 +35,7 @@ int printf_va_1(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_1(char const * __restrict format, int *param0);
int scanf_va_1(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -47,7 +47,7 @@ int scanf_va_1(char const * __restrict format, int *param0);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -59,7 +59,7 @@ int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_2(char const * __restrict format);
int printf_va_2(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
......@@ -76,7 +76,7 @@ int printf_va_2(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_2(char const * __restrict format, int *param0);
int scanf_va_2(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -88,7 +88,7 @@ int scanf_va_2(char const * __restrict format, int *param0);
\from