1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
[kernel] Parsing copy_visitor_bts_1073.c (with preprocessing)
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
int f(int x);
int f(int x)
{
return x;
}
int f1(int x)
{
return x;
}
int g(int y)
{
int tmp;
tmp = f1(2 * y);
return tmp;
}
int g1(int y)
{
int tmp;
tmp = f1(2 * y);
return tmp;
}
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
(indirect: __fc_stdout->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns __fc_stdout->__fc_FILE_data
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_1(char const * restrict format);
/*@ requires valid_read_string(param1);
requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
(indirect: __fc_stdout->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: *(param1 + (0 ..))),
(indirect: param0);
assigns __fc_stdout->__fc_FILE_data
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
*(param1 + (0 ..)), param0;
*/
int printf_va_2(char const * restrict format, int param0, char *param1);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
(indirect: __fc_stdout->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: param0);
assigns __fc_stdout->__fc_FILE_data
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
int printf_va_3(char const * restrict format, int param0);
int main(int argc, char **argv)
{
int __retres;
int i;
printf_va_1("Hello !\n");
i = 0;
while (i < argc) {
printf_va_2("arg %d : %s\n",i,*(argv + i));
i ++;
}
printf_va_3("Found %d arguments\n",i - 1);
__retres = 0;
return __retres;
}
int main1(int argc, char **argv)
{
int __retres;
int i;
printf_va_1("Hello !\n");
i = 0;
while (i < argc) {
printf_va_2("arg %d : %s\n",i,*(argv + i));
i ++;
}
printf_va_3("Found %d arguments\n",i - 1);
__retres = 0;
return __retres;
}
|
