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
|
/* run.config
COMMENT: also tests the parsing of cmdline options of type string_set
STDOPT: +"-pdg-verbose 0" +"-main main1 -impact-pragma g1" +"-then -main main2 -impact-pragma='-@all,+g2'" +"-then -main main3 -impact-pragma='-g2,+g3'"
*/
int x1, x2, y2, z2, x3;
volatile int c;
/* First case: Out(x1) in main1 is not impacted. It is equivalent to
Out(x1) in g1, which is part of the initial query */
void f1() {
x1 = 1;
}
void g1() {
if (c) {
//@ impact pragma stmt;
f1();
}
}
void main1() {
while(1) {
g1();
}
}
/* Second case: Out(x2) in main2 IS impacted, due to the circular dependency
x2 <- y2 <- z2; However, this cannot be seen immediately, so the nodes
Out(x2) in in h2 and main2 are first put in the worklist as belonging
to the initial impact. */
void f2() {
x2 = y2;
}
void aux2() {
y2 = z2;
}
void g2() {
if (c) {
//@ impact pragma stmt;
f2();
if (c) aux2();
}
}
void h2() {
g2();
z2 = x2;
}
void main2() {
while(1) {
h2();
}
}
void f3() {
x3 = 1;
}
void g3() {
//@ impact pragma stmt;
f3();
if (c) {
x3 = x3;
}
}
/* Third case: Out(x3) in main3 is impacted, as it represents Out(x3) in
the call to f3(), AND x3=x3. However, Out(x3) in the call to f3() is not
self-impacting */
void main3() {
while(1) {
g3();
}
}
|
