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
|
/* run.config*
OPT: -no-annot -val @VALUECONFIG@ -then -continue-annot-error -annot -val -journal-disable
OPT: -continue-annot-error -val @VALUECONFIG@ -main main3 -journal-disable
OPT: -continue-annot-error -val @VALUECONFIG@ -main main_err1 -journal-disable
OPT: -continue-annot-error -val @VALUECONFIG@ -main main_err2 -journal-disable
*/
void main(void)
{ int n = 13;
int i,j;
// ceci tait une annotation, mais on ne fait pas moins bien sans
// maintenant:
// loop pragma WIDEN_VARIABLES i;
/*@ loop widen_hints i, 12, 13; */
for (i=0; i<n; i++)
{
j = 4 * i + 7;
}
}
void main_err1(void)
{ int n = 13;
int i,j;
/*@ loop widen_hints "all", 12 ; */
for (i=0; i<n; i++)
{
j = 4 * i + 7;
}
}
void main_err2(void)
{ int n = 13;
int i,j;
/*@ loop pragma WIDEN_VARIABLES 12; */
for (i=0; i<n; i++)
{
j = 4 * i + 7;
}
}
void main_unhelpful () {
int max = 25;
int next = 0;
int i;
/*@ loop widen_hints next, 24; */ // This pragma is unhelpful, but used to interfere with the bound for i.
for (i=0;i<30;i++) {
int vsize = max;
int vnext = next;
if(vsize > vnext)
next++;
}
}
void main_multiple_hints () {
int maxj = 17;
int maxk = 11;
int j = 0;
int k = 0;
//@ loop widen_hints j, 17; loop widen_hints k, 11;
// 18 and 12 are actually better bounds in this case (one less iteration)
for (int i=0; i<10; i++) {
Frama_C_show_each(i, j, k);
if (j <= maxj) {
j++;
}
if (k <= maxk) {
k++;
}
}
}
void main3() {
main_unhelpful ();
main_multiple_hints ();
}
|
