explicitly mark kill accesses
[pet.git] / tests / for_while_inc2.scop
blobbbc8b9d6d07d02c2506dde1f2df47d9f34a71291
1 start: 83
2 end: 234
3 indent: "\t"
4 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
5 arrays:
6 - context: '{  :  }'
7   extent: '[n] -> { __pet_test_0[x1, t] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
8   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
9   element_type: int
10   element_size: 4
11   uniquely_defined: 1
12 - context: '{  :  }'
13   extent: '[n] -> { x2[] }'
14   element_type: int
15   element_size: 4
16   declared: 1
17 - context: '{  :  }'
18   extent: '[n] -> { s[] }'
19   element_type: int
20   element_size: 4
21 statements:
22 - line: 12
23   domain: '[n] -> { S1[x1] : x1 <= -1 + n and x1 >= 0 }'
24   schedule: '[n] -> { S1[x1] -> [0, x1, 0] }'
25   body:
26     type: expression
27     expr:
28       type: op
29       operation: =
30       arguments:
31       - type: access
32         index: '[n] -> { S1[x1] -> s[] }'
33         reference: __pet_ref_0
34         read: 0
35         write: 1
36       - type: call
37         name: f
38 - line: 13
39   domain: '[n] -> { S_5[x1] : x1 <= -1 + n and x1 >= 0 }'
40   schedule: '[n] -> { S_5[x1] -> [0, x1, 1, 0] }'
41   body:
42     type: expression
43     expr:
44       type: op
45       operation: kill
46       arguments:
47       - type: access
48         relation: '[n] -> { S_5[x1] -> x2[] }'
49         index: '[n] -> { S_5[x1] -> x2[] }'
50         reference: __pet_ref_1
51         kill: 1
52 - line: 13
53   domain: '[n] -> { S_1[x1] : x1 <= -1 + n and x1 >= 0 }'
54   schedule: '[n] -> { S_1[x1] -> [0, x1, 1, 1] }'
55   body:
56     type: expression
57     expr:
58       type: op
59       operation: =
60       arguments:
61       - type: access
62         index: '[n] -> { S_1[x1] -> x2[] }'
63         reference: __pet_ref_2
64         read: 0
65         write: 1
66       - type: int
67         value: 0
68 - line: 13
69   domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
70   schedule: '[n] -> { S_2[x1, t] -> [0, x1, 1, 2, t, 0] }'
71   body:
72     type: expression
73     expr:
74       type: op
75       operation: =
76       arguments:
77       - type: access
78         index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }'
79         reference: __pet_ref_4
80         read: 0
81         write: 1
82       - type: call
83         name: P
84         arguments:
85         - type: access
86           index: '[n] -> { S_2[x1, t] -> [(x1)] }'
87           reference: __pet_ref_5
88           read: 1
89           write: 0
90         - type: access
91           index: '[n] -> { S_2[x1, t] -> x2[] }'
92           reference: __pet_ref_6
93           read: 1
94           write: 0
95   arguments:
96   - type: access
97     index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }'
98     reference: __pet_ref_3
99     read: 1
100     write: 0
101 - line: 14
102   domain: '[n] -> { [S2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
103   schedule: '[n] -> { S2[x1, t] -> [0, x1, 1, 2, t, 1, 0] }'
104   body:
105     type: expression
106     expr:
107       type: op
108       operation: =
109       arguments:
110       - type: access
111         index: '[n] -> { S2[x1, t] -> s[] }'
112         reference: __pet_ref_8
113         read: 0
114         write: 1
115       - type: call
116         name: g
117         arguments:
118         - type: access
119           index: '[n] -> { S2[x1, t] -> s[] }'
120           reference: __pet_ref_9
121           read: 1
122           write: 0
123   arguments:
124   - type: access
125     index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }'
126     reference: __pet_ref_7
127     read: 1
128     write: 0
129 - line: 13
130   domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
131   schedule: '[n] -> { S_4[x1, t] -> [0, x1, 1, 2, t, 2] }'
132   body:
133     type: expression
134     expr:
135       type: op
136       operation: +=
137       arguments:
138       - type: access
139         index: '[n] -> { S_4[x1, t] -> x2[] }'
140         reference: __pet_ref_11
141         read: 0
142         write: 1
143       - type: access
144         index: '[n] -> { S_4[x1, t] -> s[] }'
145         reference: __pet_ref_12
146         read: 1
147         write: 0
148   arguments:
149   - type: access
150     index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }'
151     reference: __pet_ref_10
152     read: 1
153     write: 0
154 - line: 13
155   domain: '[n] -> { S_6[x1] : x1 <= -1 + n and x1 >= 0 }'
156   schedule: '[n] -> { S_6[x1] -> [0, x1, 1, 3] }'
157   body:
158     type: expression
159     expr:
160       type: op
161       operation: kill
162       arguments:
163       - type: access
164         relation: '[n] -> { S_6[x1] -> x2[] }'
165         index: '[n] -> { S_6[x1] -> x2[] }'
166         reference: __pet_ref_13
167         kill: 1
168 - line: 16
169   domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }'
170   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
171   body:
172     type: expression
173     expr:
174       type: call
175       name: h
176       arguments:
177       - type: access
178         index: '[n] -> { R[x1] -> s[] }'
179         reference: __pet_ref_14
180         read: 1
181         write: 0
182 implications:
183 - satisfied: 1
184   extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : t'' <= t and
185     x1 >= 0 and x1 <= -1 + n and t'' >= 0 }'