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
|
/* run.config*
PLUGIN: @EVA_MAIN_PLUGINS@ report
OPT: @EVA_CONFIG@ -eva-slevel-function main2:20 -pp-annot -eva -then -report
*/
/*@ requires valid: \valid(&t[0..s-1]);
requires c: 1 <= c < s; */
void init (int *t, int c, int s) {
int* p = t;
/*@ loop invariant \valid(p) && p < &t[s-1]; */
while(1) {
*(++p) = 1;
if(p >= t+c) break;
}
}
void main1 (int c) {
int t1[72];
int t2[11];
if (c >= 1 && c < 72) {
init(t1, c, 72);
if (c < 8)
init(t2, c, 11);
}
}
void main2() {
int i = 0;
int j = 0;
/*@ loop invariant i < 10;
loop invariant i == j; */
while (1) {
i++;
j++;
}
}
void main3() { // Widening is completely inactivated on this example
int j = 0;
//@ loop invariant i == 2*j || i == 2*j+1;
for (int i=0; i<100; i++) {
if (i%2==1)
j++;
Frama_C_show_each(i,j);
}
}
/* The result of the widening should be reduced by the loop invariant,
but the loop invariant must have an unknown status if it still does not hold
in the reduced state —here due to the missing backward propagation on the
multiplication. Change the invariant for a more complicated one when this
propagator is implemented. */
void main4 () {
int a = 9;
int x = 0;
/*@ loop invariant x<10 && x*x<10; */
while(x < a) x++;
}
extern int n;
/* The reduction by the loop invariant after the widening must not jeopardize
the convergence of the analysis. */
int main5(void) {
int i = 1;
int sn = 0;
/*@ loop invariant i <= sn+100; */
while (i <= n) {
Frama_C_show_each(sn, i);
sn += 2;
i ++;
}
return 0;
}
void main(int c) {
main1(c);
if (c) main2();
main3();
main4();
main5();
}
|
