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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/copy_visitor_bts_1073.c (with preprocessing)
[test] start compute
[test] exported in new project : filtered
/* Generated by Frama-C */
int f(int x);
int f(int x)
{
return x;
}
int g(int y)
{
int tmp;
tmp = f(2 * y);
return tmp;
}
/*@ assigns \result;
assigns \result \from \nothing; */
extern int printf(char const * , ...);
int main(int argc, char **argv)
{
int __retres;
int i;
printf("Hello !\n");
i = 0;
while (i < argc) {
printf("arg %d : %s\n",i,*(argv + i));
i ++;
}
printf("Found %d arguments\n",i - 1);
__retres = 0;
return __retres;
}
|
