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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
[B6 (ENTRY)]
Succs (1): B5
[B1]
1: x2
2: [B1.1] (ImplicitCastExpr, LValueToRValue, int)
3: return [B1.2];
Preds (1): B2
Succs (1): B0
[B2]
1: x1
2: [B2.1] (ImplicitCastExpr, LValueToRValue, int)
3: 8
4: [B2.2] <= [B2.3]
T: while [B2.4]
Preds (2): B3 B5
Succs (2): B4 B1
[B3]
Preds (1): B4
Succs (1): B2
[B4]
1: x1
2: [B4.1] (ImplicitCastExpr, LValueToRValue, int)
3: 2
4: [B4.2] + [B4.3]
5: x1
6: [B4.5] = [B4.4]
7: x2
8: [B4.7] (ImplicitCastExpr, LValueToRValue, int)
9: 2
10: [B4.8] + [B4.9]
11: x2
12: [B4.11] = [B4.10]
Preds (1): B2
Succs (1): B3
[B5]
1: 0
2: int x1 = 0;
3: 1
4: int x2 = 1;
Preds (1): B6
Succs (1): B2
[B0 (EXIT)]
Preds (1): B1
0-6-pre = max(-inf, inf)
1-6-pre = max(-inf, inf)
2-6-pre = max(-inf, inf)
0-5-pre = max(-inf, 0-6-pre)
1-5-pre = max(-inf, 1-6-pre)
2-5-pre = max(-inf, 2-6-pre)
0-5-0 = max(-inf, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre))
1-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre)))
2-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre)))
0-2-pre = max(-inf, 0-5-0, 0-3-pre)
1-2-pre = max(-inf, 1-5-0, 1-3-pre)
2-2-pre = max(-inf, 2-5-0, 2-3-pre)
0-4-pre = max(-inf, min(8, 0-2-pre))
1-4-pre = max(-inf, 1-2-pre)
2-4-pre = max(-inf, 2-2-pre)
0-1-pre = max(-inf, 0-2-pre)
1-1-pre = max(-inf, 1-2-pre)
2-1-pre = max(-inf, 2-2-pre)
0-4-0 = max(-inf, add(2, MCF<[-1,1,0],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre)))
1-4-0 = max(-inf, add(2, MCF<[-1,0,1],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre)))
2-4-0 = max(-inf, MCF<[0,-1,1],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre))
0-3-pre = max(-inf, 0-4-0)
1-3-pre = max(-inf, 1-4-0)
2-3-pre = max(-inf, 2-4-0)
0-0-pre = max(-inf, 0-1-pre)
1-0-pre = max(-inf, 1-1-pre)
2-0-pre = max(-inf, 2-1-pre)
Block 0:
x1 <= 10
x2 <= 11
x2-x1 <= 1
Block 1:
x1 <= 10
x2 <= 11
x2-x1 <= 1
Block 2:
x1 <= 10
x2 <= 11
x2-x1 <= 1
Block 3:
x1 <= 10
x2 <= 11
x2-x1 <= 1
Block 4:
x1 <= 8
x2 <= 11
x2-x1 <= 1
Block 5:
x1 <= inf
x2 <= inf
x2-x1 <= inf
Block 6:
x1 <= inf
x2 <= inf
x2-x1 <= inf
|
