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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/unspecified_access_ptr_bts1519.i (no preprocessing)
/* Generated by Frama-C */
int t[10];
int u[10];
int v[10];
int i = 4;
int j = 0;
void main(void)
{
int *p1;
int *p2;
int tmp;
int tmp_0;
p1 = & v[i];
p2 = & v[j];
{ /* sequence */
tmp = *p1;
/*effects: (t[i]) <- */
(*p1) ++;
/*effects: (t[i]) *p1 <- p1*/
t[i] += tmp + *p2;
/*effects: (t[i]) t[i] <- i, tmp, *p2, p2*/
}
{ /* sequence */
tmp_0 = v[i];
/*effects: (t[i]) <- */
(v[i]) ++;
/*effects: (t[i]) v[i] <- i*/
t[i] += tmp_0 + v[j];
/*effects: (t[i]) t[i] <- i, tmp_0, v[j], j*/
}
return;
}
|
