Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
open-source-case-studies
Commits
dc85004b
Commit
dc85004b
authored
Jun 15, 2021
by
Andre Maroneze
💬
Browse files
synchronize with frama-c master
parent
6d12e258
Pipeline
#35833
passed with stage
in 84 minutes and 47 seconds
Changes
115
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
2048/.frama-c/2048.eva/alarms.csv
View file @
dc85004b
directory file line function property kind status property
. 2048.c 37 getColor mem_access Unknown \valid_read(foreground)
. 2048.c 51 drawBoard precondition of printf_va_3 Unknown valid_read_string(param0)
. 2048.c 51 printf_va_3 precondition Unknown valid_read_string(param0)
. 2048.c 58 drawBoard precondition of printf_va_7 Unknown valid_read_string(param0)
. 2048.c 58 printf_va_7 precondition Unknown valid_read_string(param0)
. 2048.c 61 drawBoard shift Unknown 0 ≤ (int)(*(board + x))[y] < 32
. 2048.c 62 drawBoard precondition of strlen Unknown valid_string_s: valid_read_string(s)
. 2048.c 63 drawBoard precondition of printf_va_8 Unknown valid_read_string(param2)
. 2048.c 63 printf_va_8 precondition Unknown valid_read_string(param2)
. 2048.c 72 drawBoard precondition of printf_va_12 Unknown valid_read_string(param0)
. 2048.c 72 printf_va_12 precondition Unknown valid_read_string(param0)
. 2048.c 90 findTarget mem_access Unknown \valid_read(array + t)
. 2048.c 123 slideArray shift Unknown 0 ≤ (int)*(array + t) < 32
. 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 stdio.h 211 printf_va_12 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 211 printf_va_3 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 211 printf_va_7 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 211 printf_va_8 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc string.h 128 strlen precondition Unknown valid_string_s: valid_read_string(s)
2048/.frama-c/2048.parse/framac.ast
View file @
dc85004b
...
...
@@ -13,10 +13,10 @@
#include "unistd.h"
uint32_t score = (unsigned int)0;
uint8_t scheme = (unsigned char)0;
/*@ requires
/*@ requires valid_read_string(format);
requires
\valid(s + (0 .. n - 1)) ∨
\valid(s + (0 .. format_length(format) - 1));
requires valid_read_string(format);
assigns \result, *(s + (0 ..));
assigns \result
\from (indirect: n), (indirect: *(format + (0 ..))),
...
...
@@ -173,8 +173,8 @@ int printf_va_1(char const * restrict format);
*/
int printf_va_2(char const * restrict format, int param0);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -199,8 +199,8 @@ int printf_va_3(char const * restrict format, char *param0);
*/
int printf_va_4(char const * restrict format);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -225,8 +225,8 @@ int printf_va_5(char const * restrict format, char *param0);
*/
int printf_va_6(char const * restrict format);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -239,10 +239,10 @@ int printf_va_6(char const * restrict format);
*/
int printf_va_7(char const * restrict format, char *param0);
/*@ requires
/*@ requires valid_read_string(format);
requires
\valid(s + (0 .. n - 1)) ∨
\valid(s + (0 .. format_length(format) - 1));
requires valid_read_string(format);
assigns \result, *(s + (0 ..));
assigns \result
\from (indirect: n), (indirect: *(format + (0 ..))), (indirect: param0);
...
...
@@ -252,10 +252,10 @@ int printf_va_7(char const * restrict format, char *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);
/*@ requires valid_read_string(param1);
requires valid_read_string(param2);
requires valid_read_string(param1);
requires valid_read_string(param4);
requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -284,8 +284,8 @@ int printf_va_8(char const * restrict format, int param0, char *param1,
*/
int printf_va_9(char const * restrict format);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -310,8 +310,8 @@ int printf_va_10(char const * restrict format, char *param0);
*/
int printf_va_11(char const * restrict format);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -336,8 +336,8 @@ int printf_va_12(char const * restrict format, char *param0);
*/
int printf_va_13(char const * restrict format);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
basic-cwe-examples/.frama-c/cwe20-2-precise.parse/framac.ast
View file @
dc85004b
...
...
@@ -19,8 +19,8 @@ int stack_top;
*/
int printf_va_1(char const * restrict format);
/*@ requires valid
_read_string(format
);
requires
\
valid
(param0
);
/*@ requires
\
valid
(param0
);
requires valid
_read_string(format
);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
...
...
basic-cwe-examples/.frama-c/cwe20-2.parse/framac.ast
View file @
dc85004b
...
...
@@ -19,8 +19,8 @@ int stack_top;
*/
int printf_va_1(char const * restrict format);
/*@ requires valid
_read_string(format
);
requires
\
valid
(param0
);
/*@ requires
\
valid
(param0
);
requires valid
_read_string(format
);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
...
...
basic-cwe-examples/.frama-c/cwe20-precise.parse/framac.ast
View file @
dc85004b
...
...
@@ -20,8 +20,8 @@ typedef struct _board_square_t board_square_t;
*/
int printf_va_1(char const * restrict format);
/*@ requires valid
_read_string(format
);
requires
\
valid
(param0
);
/*@ requires
\
valid
(param0
);
requires valid
_read_string(format
);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
...
...
@@ -61,8 +61,8 @@ int fprintf_va_1(FILE * restrict stream, char const * restrict format);
*/
int printf_va_2(char const * restrict format);
/*@ requires valid
_read_string(format
);
requires
\
valid
(param0
);
/*@ requires
\
valid
(param0
);
requires valid
_read_string(format
);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
...
...
basic-cwe-examples/.frama-c/cwe20.parse/framac.ast
View file @
dc85004b
...
...
@@ -20,8 +20,8 @@ typedef struct _board_square_t board_square_t;
*/
int printf_va_1(char const * restrict format);
/*@ requires valid
_read_string(format
);
requires
\
valid
(param0
);
/*@ requires
\
valid
(param0
);
requires valid
_read_string(format
);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
...
...
@@ -61,8 +61,8 @@ int fprintf_va_1(FILE * restrict stream, char const * restrict format);
*/
int printf_va_2(char const * restrict format);
/*@ requires valid
_read_string(format
);
requires
\
valid
(param0
);
/*@ requires
\
valid
(param0
);
requires valid
_read_string(format
);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
...
...
c-testsuite/.frama-c/00132.parse/framac.ast
View file @
dc85004b
...
...
@@ -28,9 +28,9 @@ int printf_va_1(char const * restrict format);
*/
int printf_va_2(char const * restrict format, int param0);
/*@ requires valid_read_string(
format
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(param1);
requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
c-testsuite/.frama-c/00173.parse/framac.ast
View file @
dc85004b
...
...
@@ -3,8 +3,8 @@
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -31,8 +31,8 @@ int printf_va_1(char const * restrict format, char *param0);
*/
int printf_va_2(char const * restrict format, int param0, int param1);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
c-testsuite/.frama-c/00179.parse/framac.ast
View file @
dc85004b
...
...
@@ -8,8 +8,8 @@
#include "string.c"
#include "string.h"
#include "strings.h"
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -22,8 +22,8 @@
*/
int printf_va_1(char const * restrict format, char *param0);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -88,8 +88,8 @@ int printf_va_5(char const * restrict format, int param0);
*/
int printf_va_6(char const * restrict format, size_t param0);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -154,8 +154,8 @@ int printf_va_10(char const * restrict format, int param0);
*/
int printf_va_11(char const * restrict format, int param0);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -168,8 +168,8 @@ int printf_va_11(char const * restrict format, int param0);
*/
int printf_va_12(char const * restrict format, char *param0);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -195,8 +195,8 @@ int printf_va_13(char const * restrict format, char *param0);
*/
int printf_va_14(char const * restrict format, int param0);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -209,8 +209,8 @@ int printf_va_14(char const * restrict format, int param0);
*/
int printf_va_15(char const * restrict format, char *param0);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
c-testsuite/.frama-c/00180.parse/framac.ast
View file @
dc85004b
...
...
@@ -8,8 +8,8 @@
#include "string.c"
#include "string.h"
#include "strings.h"
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
c-testsuite/.frama-c/00182.parse/framac.ast
View file @
dc85004b
...
...
@@ -204,8 +204,8 @@ void print_led(unsigned long x, char *buf)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
c-testsuite/.frama-c/00186.eva/alarms.csv
View file @
dc85004b
directory file line function property kind status property
. 00186.c 11 main precondition of printf_va_1 Unknown valid_read_string(param0)
. 00186.c
11 printf_va_1 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 2
11 printf_va_1 precondition Unknown valid_read_string(param0)
c-testsuite/.frama-c/00186.parse/framac.ast
View file @
dc85004b
...
...
@@ -10,8 +10,8 @@
*/
int sprintf_va_1(char * restrict s, char const * restrict format, int param0);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
c-testsuite/.frama-c/00187.eva/alarms.csv
View file @
dc85004b
...
...
@@ -2,12 +2,12 @@ directory file line function property kind status property
. 00187.c 6 main precondition of fwrite Unknown valid_stream: \valid(stream)
. 00187.c 11 main precondition of fread Unknown valid_stream: \valid(stream)
. 00187.c 17 main precondition of printf_va_2 Unknown valid_read_string(param0)
. 00187.c 17 printf_va_2 precondition Unknown valid_read_string(param0)
. 00187.c 22 main precondition of fgetc Unknown valid_stream: \valid(stream)
. 00187.c 33 main precondition of getc Unknown valid_stream: \valid(stream)
. 00187.c 44 main precondition of fgets Unknown valid_stream: \valid(stream)
. 00187.c 45 main precondition of printf_va_5 Unknown valid_read_string(param0)
. 00187.c 45 printf_va_5 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 211 printf_va_2 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 211 printf_va_5 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 258 fgetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 266 fgets precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 296 getc precondition Unknown valid_stream: \valid(stream)
...
...
c-testsuite/.frama-c/00187.parse/framac.ast
View file @
dc85004b
...
...
@@ -15,8 +15,8 @@
*/
int printf_va_1(char const * restrict format);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -57,8 +57,8 @@ int printf_va_3(char const * restrict format, int param0, int param1);
*/
int printf_va_4(char const * restrict format, int param0, int param1);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
c-testsuite/.frama-c/00200.parse/framac.ast
View file @
dc85004b
...
...
@@ -5,8 +5,8 @@
#include "stdio.h"
static int debug;
static int nfailed = 0;
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -21,8 +21,8 @@ static int nfailed = 0;
int printf_va_1(char const * restrict format, char *param0, int param1,
int param2);
/*@ requires valid_read_string(
format
);
requires valid_read_string(
param0
);
/*@ requires valid_read_string(
param0
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
c-testsuite/.frama-c/00204.parse/framac.ast
View file @
dc85004b
...
...
@@ -278,8 +278,8 @@ struct hfa34 hfa34 =
.b = (long double)34.2,
.c = (long double)34.3,
.d = (long double)34.4};
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 1
);
/*@ requires valid_read_
n
string(
param0, 1
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -298,8 +298,8 @@ void fa_s1(struct s1 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 2
);
/*@ requires valid_read_
n
string(
param0, 2
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -318,8 +318,8 @@ void fa_s2(struct s2 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 3
);
/*@ requires valid_read_
n
string(
param0, 3
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -338,8 +338,8 @@ void fa_s3(struct s3 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 4
);
/*@ requires valid_read_
n
string(
param0, 4
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -358,8 +358,8 @@ void fa_s4(struct s4 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 5
);
/*@ requires valid_read_
n
string(
param0, 5
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -378,8 +378,8 @@ void fa_s5(struct s5 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 6
);
/*@ requires valid_read_
n
string(
param0, 6
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -398,8 +398,8 @@ void fa_s6(struct s6 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 7
);
/*@ requires valid_read_
n
string(
param0, 7
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -418,8 +418,8 @@ void fa_s7(struct s7 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 8
);
/*@ requires valid_read_
n
string(
param0, 8
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -438,8 +438,8 @@ void fa_s8(struct s8 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 9
);
/*@ requires valid_read_
n
string(
param0, 9
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -458,8 +458,8 @@ void fa_s9(struct s9 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 10
);
/*@ requires valid_read_
n
string(
param0, 10
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -478,8 +478,8 @@ void fa_s10(struct s10 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 11
);
/*@ requires valid_read_
n
string(
param0, 11
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -498,8 +498,8 @@ void fa_s11(struct s11 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 12
);
/*@ requires valid_read_
n
string(
param0, 12
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -518,8 +518,8 @@ void fa_s12(struct s12 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 13
);
/*@ requires valid_read_
n
string(
param0, 13
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -538,8 +538,8 @@ void fa_s13(struct s13 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 14
);
/*@ requires valid_read_
n
string(
param0, 14
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -558,8 +558,8 @@ void fa_s14(struct s14 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 15
);
/*@ requires valid_read_
n
string(
param0, 15
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -578,8 +578,8 @@ void fa_s15(struct s15 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 16
);
/*@ requires valid_read_
n
string(
param0, 16
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -598,8 +598,8 @@ void fa_s16(struct s16 a)
return;
}
/*@ requires valid_read_string(
format
);
requires valid_read_
n
string(
param0, 17
);
/*@ requires valid_read_
n
string(
param0, 17
);
requires valid_read_string(
format
);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -863,13 +863,13 @@ void fa_hfa34(struct hfa34 a)
return;
}
/*@ requires valid_read_string(format);
requires valid_read_nstring(param5, 3);
requires valid_read_nstring(param4, 3);
requires valid_read_nstring(param3, 3);
requires valid_read_nstring(param2, 3);
/*@ requires valid_read_nstring(param0, 3);
requires valid_read_nstring(param1, 3);
requires valid_read_nstring(param0, 3);
requires valid_read_nstring(param2, 3);
requires valid_read_nstring(param3, 3);
requires valid_read_nstring(param4, 3);
requires valid_read_nstring(param5, 3);
requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -894,13 +894,13 @@ void fa1(struct s8 a, struct s9 b, struct s10 c, struct s11 d, struct s12 e,
return;
}
/*@ requires valid_read_string(format);
requires valid_read_nstring(param5, 3);
requires valid_read_nstring(param4, 3);
requires valid_read_nstring(param3, 3);
requires valid_read_nstring(param2, 3);
/*@ requires valid_read_nstring(param0, 3);
requires valid_read_nstring(param1, 3);
requires valid_read_nstring(param0, 3);
requires valid_read_nstring(param2, 3);
requires valid_read_nstring(param3, 3);
requires valid_read_nstring(param4, 3);
requires valid_read_nstring(param5, 3);
requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
...
...
@@ -949,10 +949,10 @@ void fa3(struct hfa14 a, struct hfa23 b, struct hfa32 c)
return;
}
/*@ requires valid_read_string(format);
requires valid_read_nstring(param6, 3);
/*@ requires valid_read_nstring(param0, 1);
requires valid_read_nstring(param3, 2);
requires valid_read_nstring(param0, 1);
requires valid_read_nstring(param6, 3);
requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;