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
|
[kernel] Parsing ghost_parameters_side_effect_arg.i (no preprocessing)
/* Generated by Frama-C */
void function(int x) /*@ ghost (int y) */;
int other(int x) /*@ ghost (int y) */;
void caller(void)
{
/*@ ghost int g_tmp; */
int tmp;
/*@ ghost int g_tmp_0; */
int tmp_0;
/*@ ghost int g_tmp_1; */
int tmp_1;
/*@ ghost int g_tmp_2; */
int tmp_2;
/*@ ghost int g_tmp_3; */
/*@ ghost int g_tmp_4; */
int x = 0;
/*@ ghost int g = 0; */
int t[3] = {0, 0, 0};
/*@ ghost g_tmp = g; */
/*@ ghost g ++; */
/*@ ghost ; */
tmp = x;
x ++;
;
function(tmp) /*@ ghost (g_tmp) */;
/*@ ghost g = 42; */
x = 2;
function(x) /*@ ghost (g) */;
/*@ ghost g += 42; */
x += 2;
function(x) /*@ ghost (g) */;
function(- x) /*@ ghost (- g) */;
/*@ ghost if (g == 0) g_tmp_0 = g; else g_tmp_0 = 42; */
if (x == 0) tmp_0 = x; else tmp_0 = 42;
function(tmp_0) /*@ ghost (g_tmp_0) */;
/*@ ghost g_tmp_1 = g; */
/*@ ghost g ++; */
/*@ ghost ; */
tmp_1 = x;
x ++;
;
function(t[tmp_1]) /*@ ghost (t[g_tmp_1]) */;
/*@ ghost g_tmp_2 = other(x,g); */
tmp_2 = other(x) /*@ ghost (g) */;
function(tmp_2) /*@ ghost (g_tmp_2) */;
/*@ ghost int i = 1; */
/*@ ghost g_tmp_3 = i;
i ++;
;
g_tmp_4 = g;
g ++;
; */
/*@ ghost function(g_tmp_4,g_tmp_3); */
return;
}
|
