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
87
88
89
|
/* run.config
OPT: -val -cpp-extra-args=-DSYNTAX_ERRORS -continue-annot-error
OPT: -val -cpp-extra-args=-DNONCONST
OPT: -val -slevel 1 -kernel-msg-key widen-hints
OPT: -val -cpp-extra-args=-DALLGLOBAL -kernel-msg-key widen-hints
*/
#define N 2
const int x = 9;
int not_const = 42; // cannot be used as widen hint
#ifdef SYNTAX_ERRORS
int main1() {
/*@ widen_hints x; */ // error: no hints
return 0;
}
int main2() {
/*@ widen_hints 1; */ // error: no variable
return 0;
}
int main3() {
/*@ widen_hints x, b, 1; */ // error: b must be a constant value
return 0;
}
int main() {
/*@ widen_hints x, not_const; */ // error: not_const not a global constant
return 0;
}
#else
#ifdef ALLGLOBAL
int f() {
int m = 10;
int n = 33+m;
int t[100];
// global:"all" hints should apply here
for (int a = 0; a < n*2+1; a++) {
for (int b = 0; b < a; b++) {
t[b] = 1;
}
}
return 0;
}
#endif
#ifdef EXTGLOBAL
// ext_i and external_f are defined in widen_hints_external.c
void external_f();
#endif
int main() {
#ifdef NONCONST
const int local_const = 17; // cannot be used as widen hint
/*@ widen_hints x, local_const; */ // error: local_const not a global constant
#endif
int y;
int m = 10;
int n = 33+m;
// without hints for a, there is a signed overflow
//@ loop widen_hints a, (N+(6*x)+118)/2;
for (int a = 0; a < n*2+1; a++) {
for (int b = 0; b < a; b++) {
}
}
#ifdef ALLGLOBAL
/*@ widen_hints global:"all", 88; */
f();
#endif
struct st {
int i;
double d;
} ss;
//@ widen_hints ss.i, 87;
for (ss.i = 0; ss.i < n*2+1; ss.i++) {
for (int b = 0; b < ss.i; b++) {
}
}
return 0;
}
#endif
|
