|
1
|
#include <assert.h>
|
|
2
|
#include "oversampling0.h"
|
|
3
|
typedef enum _bool { false = 0, true = 1 } bool ;
|
|
4
|
|
|
5
|
/* C code generated by lustrec
|
|
6
|
SVN version number 0.1-382M
|
|
7
|
Code is C99 compliant */
|
|
8
|
|
|
9
|
/* Import dependencies */
|
|
10
|
|
|
11
|
/* Global constants (definitions) */
|
|
12
|
|
|
13
|
/* Struct definitions */
|
|
14
|
struct f_mem {struct f_reg {int __f_2; } _reg; struct _arrow_mem *ni_2; };
|
|
15
|
|
|
16
|
//@ ghost struct _arrow_mem_pack { struct _arrow_reg _reg; };
|
|
17
|
|
|
18
|
/*@ predicate init_arrow (struct _arrow_mem_pack mem_in) =
|
|
19
|
(mem_in._reg._first == true);
|
|
20
|
*/
|
|
21
|
/*@ predicate trans_arrow(struct _arrow_mem_pack mem_in,struct _arrow_mem_pack mem_out, _Bool out) =
|
|
22
|
(out == mem_in._reg._first)
|
|
23
|
&& (mem_in._reg._first)?(mem_out._reg._first == false):(mem_out._reg._first == mem_in._reg._first);
|
|
24
|
*/
|
|
25
|
|
|
26
|
/*@ predicate _arrow_pack (struct _arrow_mem_pack memp, struct _arrow_mem *mem) =
|
|
27
|
(memp._reg._first == mem->_reg._first);
|
|
28
|
*/
|
|
29
|
|
|
30
|
//@ ghost struct f_mem_pack {struct f_reg _reg; struct _arrow_mem_pack ni_2; };
|
|
31
|
|
|
32
|
|
|
33
|
/*@ predicate f_pack0 (struct f_mem_pack memp, struct f_mem *mem) =
|
|
34
|
\true;
|
|
35
|
*/
|
|
36
|
|
|
37
|
/*@ predicate f_pack1 (struct f_mem_pack memp, struct f_mem *mem) =
|
|
38
|
f_pack0(memp, mem)
|
|
39
|
&& _arrow_pack(memp.ni_2, mem->ni_2);
|
|
40
|
*/
|
|
41
|
|
|
42
|
/*@ predicate f_pack2 (struct f_mem_pack memp, struct f_mem *mem) =
|
|
43
|
f_pack1(memp, mem)
|
|
44
|
&& (memp._reg.__f_2 == mem->_reg.__f_2);
|
|
45
|
*/
|
|
46
|
|
|
47
|
|
|
48
|
/* Scheduling: y ; __f_1 ; __f_3 ; cpt ; __f_2
|
|
49
|
Steps: A B C D E F
|
|
50
|
Mem steps: 0 1 2
|
|
51
|
Death table: __f_3 |-> __f_1, cpt |-> __f_3
|
|
52
|
Reuse table: {}
|
|
53
|
*/
|
|
54
|
|
|
55
|
|
|
56
|
/*@ predicate init_f(struct f_mem_pack mem_in) =
|
|
57
|
init_arrow(mem_in.ni_2);
|
|
58
|
*/
|
|
59
|
|
|
60
|
/*@ predicate trans_fA(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out) =
|
|
61
|
\true;
|
|
62
|
*/
|
|
63
|
|
|
64
|
/*@ predicate trans_fy(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out) =
|
|
65
|
(y_out == x_in + 1);
|
|
66
|
*/
|
|
67
|
|
|
68
|
/*@ predicate clock_fy(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out) =
|
|
69
|
\true;
|
|
70
|
*/
|
|
71
|
|
|
72
|
/*@ predicate trans_fB(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out) =
|
|
73
|
trans_fA(x_in, mem_in, mem_out, y_out)
|
|
74
|
&& (clock_fy(x_in, mem_in, mem_out) ==> trans_fy(x_in, mem_in, mem_out, y_out));
|
|
75
|
*/
|
|
76
|
|
|
77
|
/*@ predicate trans_f__f_1(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, _Bool __f_1) =
|
|
78
|
trans_arrow(mem_in.ni_2, mem_out.ni_2, __f_1);
|
|
79
|
*/
|
|
80
|
|
|
81
|
/*@ predicate clock_f__f_1(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out) =
|
|
82
|
\true;
|
|
83
|
*/
|
|
84
|
|
|
85
|
/*@ predicate trans_fC(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, _Bool __f_1) =
|
|
86
|
trans_fB(x_in, mem_in, mem_out, y_out)
|
|
87
|
&& (clock_f__f_1(x_in, mem_in, mem_out, y_out) ==> trans_f__f_1(x_in, mem_in, mem_out, y_out, __f_1));
|
|
88
|
*/
|
|
89
|
|
|
90
|
/*@ predicate trans_f__f_3(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, _Bool __f_1, int __f_3) =
|
|
91
|
(__f_1)?(__f_3 == 0):(__f_3 == mem_in._reg.__f_2);
|
|
92
|
*/
|
|
93
|
|
|
94
|
/*@ predicate clock_f__f_3(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, _Bool __f_1) =
|
|
95
|
\true;
|
|
96
|
*/
|
|
97
|
|
|
98
|
/*@ predicate trans_fD(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, int __f_3) =
|
|
99
|
\exists _Bool __f_1;
|
|
100
|
trans_fC(x_in, mem_in, mem_out, y_out, __f_1)
|
|
101
|
&& (clock_f__f_3(x_in, mem_in, mem_out, y_out, __f_1) ==> trans_f__f_3(x_in, mem_in, mem_out, y_out, __f_1, __f_3));
|
|
102
|
*/
|
|
103
|
|
|
104
|
/*@ predicate trans_fcpt(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, int __f_3, int cpt_out) =
|
|
105
|
(cpt_out == __f_3 + 1);
|
|
106
|
*/
|
|
107
|
|
|
108
|
/*@ predicate clock_fcpt(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, int __f_3) =
|
|
109
|
\true;
|
|
110
|
*/
|
|
111
|
|
|
112
|
/*@ predicate trans_fE(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, int cpt_out) =
|
|
113
|
\exists int __f_3;
|
|
114
|
trans_fD(x_in, mem_in, mem_out, y_out, __f_3)
|
|
115
|
&& (clock_fcpt(x_in, mem_in, mem_out, y_out, __f_3) ==> trans_fcpt(x_in, mem_in, mem_out, y_out, __f_3, cpt_out));
|
|
116
|
*/
|
|
117
|
|
|
118
|
/*@ predicate trans_f__f_2(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, int cpt_out) =
|
|
119
|
(mem_out._reg.__f_2 == cpt_out);
|
|
120
|
*/
|
|
121
|
|
|
122
|
/*@ predicate clock_f__f_2(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, int cpt_out) =
|
|
123
|
\true;
|
|
124
|
*/
|
|
125
|
|
|
126
|
/*@ predicate trans_fF(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, int cpt_out) =
|
|
127
|
trans_fE(x_in, mem_in, mem_out, y_out, cpt_out)
|
|
128
|
&& (clock_f__f_2(x_in, mem_in, mem_out, y_out, cpt_out) ==> trans_f__f_2(x_in, mem_in, mem_out, y_out, cpt_out));
|
|
129
|
*/
|
|
130
|
|
|
131
|
/*@ predicate valid_f(struct f_mem *self) =
|
|
132
|
\valid(self)
|
|
133
|
&& \valid(self->ni_2);
|
|
134
|
|
|
135
|
*/
|
|
136
|
|
|
137
|
/*@
|
|
138
|
requires valid_f(self);
|
|
139
|
requires \separated(self, (self->ni_2));
|
|
140
|
ensures \forall struct f_mem_pack mem; f_pack2(mem, self) ==> init_f(mem);
|
|
141
|
assigns (self->ni_2)->_reg._first;
|
|
142
|
*/
|
|
143
|
void f_reset (struct f_mem *self) {
|
|
144
|
_arrow_reset(self->ni_2);
|
|
145
|
return;
|
|
146
|
}
|
|
147
|
|
|
148
|
/*@
|
|
149
|
requires valid_f(self);
|
|
150
|
requires \valid(cpt);
|
|
151
|
requires \valid(y);
|
|
152
|
requires \separated(self, cpt, y, (self->ni_2));
|
|
153
|
ensures \forall struct f_mem_pack mem1; \forall struct f_mem_pack mem2; \at(f_pack2(mem1, self), Pre) ==> f_pack2(mem2, self) ==> trans_fF(x, mem1, mem2, *y, *cpt);
|
|
154
|
assigns *cpt, *y, self->_reg.__f_2, (self->ni_2)->_reg._first;
|
|
155
|
*/
|
|
156
|
void f_step (int x,
|
|
157
|
int (*cpt), int (*y),
|
|
158
|
struct f_mem *self) {
|
|
159
|
_Bool __f_1;
|
|
160
|
int __f_3;
|
|
161
|
//@ assert \forall struct f_mem_pack mem1; \forall struct f_mem_pack mem2; \at(f_pack2(mem1, self), Pre) ==> f_pack0(mem2, self) ==> trans_fA(x, mem1, mem2, *y);
|
|
162
|
*y = (x + 1);
|
|
163
|
//@ assert \forall struct f_mem_pack mem1; \forall struct f_mem_pack mem2; \at(f_pack2(mem1, self), Pre) ==> f_pack0(mem2, self) ==> trans_fB(x, mem1, mem2, *y);
|
|
164
|
_once_step (&__f_1, self->ni_2);
|
|
165
|
//@ assert \forall struct f_mem_pack mem1; \forall struct f_mem_pack mem2; \at(f_pack2(mem1, self), Pre) ==> f_pack1(mem2, self) ==> trans_fC(x, mem1, mem2, *y, __f_1);
|
|
166
|
if (__f_1) {
|
|
167
|
__f_3 = 0;
|
|
168
|
} else {
|
|
169
|
__f_3 = self->_reg.__f_2;
|
|
170
|
}
|
|
171
|
//@ assert \forall struct f_mem_pack mem1; \forall struct f_mem_pack mem2; \at(f_pack2(mem1, self), Pre) ==> f_pack1(mem2, self) ==> trans_fD(x, mem1, mem2, *y, __f_3);
|
|
172
|
*cpt = (__f_3 + 1);
|
|
173
|
//@ assert \forall struct f_mem_pack mem1; \forall struct f_mem_pack mem2; \at(f_pack2(mem1, self), Pre) ==> f_pack1(mem2, self) ==> trans_fE(x, mem1, mem2, *y, *cpt);
|
|
174
|
self->_reg.__f_2 = *cpt;
|
|
175
|
//@ assert \forall struct f_mem_pack mem1; \forall struct f_mem_pack mem2; \at(f_pack2(mem1, self), Pre) ==> f_pack2(mem2, self) ==> trans_fF(x, mem1, mem2, *y, *cpt);
|
|
176
|
return;
|
|
177
|
}
|
|
178
|
|
|
179
|
|
|
180
|
/* ***************************************************************************** */
|
|
181
|
|
|
182
|
struct g_mem {struct g_reg {int __g_2; } _reg; struct _arrow_mem *ni_1; struct f_mem *ni_0; };
|
|
183
|
|
|
184
|
//@ ghost struct g_mem_pack {struct g_reg _reg; struct _arrow_mem_pack ni_1; struct f_mem_pack ni_0; };
|
|
185
|
|
|
186
|
|
|
187
|
/*@ predicate g_pack0 (struct g_mem_pack memp, struct g_mem *mem) =
|
|
188
|
\true;
|
|
189
|
*/
|
|
190
|
|
|
191
|
/*@ predicate g_pack1 (struct g_mem_pack memp, struct g_mem *mem) =
|
|
192
|
g_pack0(memp, mem)
|
|
193
|
&& _arrow_pack(memp.ni_1, mem->ni_1);
|
|
194
|
*/
|
|
195
|
|
|
196
|
/*@ predicate g_pack2 (struct g_mem_pack memp, struct g_mem *mem) =
|
|
197
|
g_pack1(memp, mem)
|
|
198
|
&& f_pack2(memp.ni_0, mem->ni_0);
|
|
199
|
*/
|
|
200
|
|
|
201
|
/*@ predicate g_pack3 (struct g_mem_pack memp, struct g_mem *mem) =
|
|
202
|
g_pack2(memp, mem)
|
|
203
|
&& (memp._reg.__g_2 == mem->_reg.__g_2);
|
|
204
|
*/
|
|
205
|
|
|
206
|
/* Scheduling: __g_1 ; last_y ; t ; y ; out ; cpt ; __g_2
|
|
207
|
Real sched: __g_1 ; last_y ; t ; (y, cpt) ; out ; __g_2
|
|
208
|
Steps: A B C D E F G
|
|
209
|
Mem steps: 0 1 2 3
|
|
210
|
Death table: last_y |-> __g_1, t |-> last_y, (y, cpt) |-> {t, cpt}, __g_2 |-> y
|
|
211
|
Reuse table: t |-> last_y, y |-> last_y
|
|
212
|
*/
|
|
213
|
|
|
214
|
|
|
215
|
/*@ predicate init_g(struct g_mem_pack mem_in) =
|
|
216
|
init_f(mem_in.ni_0)
|
|
217
|
&& init_arrow(mem_in.ni_1);
|
|
218
|
*/
|
|
219
|
|
|
220
|
/*@ predicate trans_gA(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out) =
|
|
221
|
\true;
|
|
222
|
*/
|
|
223
|
|
|
224
|
/*@ predicate clock_g__g_1(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out) =
|
|
225
|
\true;
|
|
226
|
*/
|
|
227
|
|
|
228
|
/*@ predicate trans_g__g_1(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, _Bool __g_1) =
|
|
229
|
trans_arrow(mem_in.ni_1, mem_out.ni_1, __g_1);
|
|
230
|
*/
|
|
231
|
|
|
232
|
/*@ predicate trans_gB(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, _Bool __g_1) =
|
|
233
|
trans_gA(c_in, x_in, mem_in, mem_out, out_out)
|
|
234
|
&& (clock_g__g_1(c_in, x_in, mem_in, mem_out, out_out) ==> trans_g__g_1(c_in, x_in, mem_in, mem_out, out_out, __g_1));
|
|
235
|
*/
|
|
236
|
|
|
237
|
/*@ predicate clock_glast_y(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, _Bool __g_1) =
|
|
238
|
\true;
|
|
239
|
*/
|
|
240
|
|
|
241
|
/*@ predicate trans_glast_y(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, _Bool __g_1, int last_y) =
|
|
242
|
(__g_1)?(last_y == 0):(last_y == mem_in._reg.__g_2);
|
|
243
|
*/
|
|
244
|
|
|
245
|
/*@ predicate trans_gC(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int last_y) =
|
|
246
|
\exists _Bool __g_1;
|
|
247
|
trans_gB(c_in, x_in, mem_in, mem_out, out_out, __g_1)
|
|
248
|
&& (clock_glast_y(c_in, x_in, mem_in, mem_out, out_out, __g_1) ==> trans_glast_y(c_in, x_in, mem_in, mem_out, out_out, __g_1, last_y));
|
|
249
|
*/
|
|
250
|
|
|
251
|
/*@ predicate clock_gt(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int last_y) =
|
|
252
|
\true;
|
|
253
|
*/
|
|
254
|
|
|
255
|
/*@ predicate trans_gt(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int last_y, int t) =
|
|
256
|
(c_in)?(t == x_in):(t == last_y);
|
|
257
|
*/
|
|
258
|
|
|
259
|
/*@ predicate trans_gD(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int t) =
|
|
260
|
\exists int last_y;
|
|
261
|
trans_gC(c_in, x_in, mem_in, mem_out, out_out, last_y)
|
|
262
|
&& (clock_gt(c_in, x_in, mem_in, mem_out, out_out, last_y) ==> trans_gt(c_in, x_in, mem_in, mem_out, out_out, last_y, t));
|
|
263
|
*/
|
|
264
|
|
|
265
|
/*@ predicate clock_gy(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int t) =
|
|
266
|
\true;
|
|
267
|
*/
|
|
268
|
|
|
269
|
/*@ predicate trans_gy(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int t, int y, int cpt) =
|
|
270
|
trans_fF(t, mem_in.ni_0, mem_out.ni_0, y, cpt);
|
|
271
|
*/
|
|
272
|
|
|
273
|
/*@ predicate trans_gE(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int y) =
|
|
274
|
\exists int t, int cpt;
|
|
275
|
trans_gD(c_in, x_in, mem_in, mem_out, out_out, t)
|
|
276
|
&& (clock_gy(c_in, x_in, mem_in, mem_out, out_out, t) ==> trans_gy(c_in, x_in, mem_in, mem_out, out_out, t, y, cpt));
|
|
277
|
*/
|
|
278
|
|
|
279
|
/*@ predicate clock_gout(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int y) =
|
|
280
|
(c_in == false);
|
|
281
|
*/
|
|
282
|
|
|
283
|
/*@ predicate trans_gout(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int y) =
|
|
284
|
(out_out == y);
|
|
285
|
*/
|
|
286
|
|
|
287
|
/*@ predicate trans_gF(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int y) =
|
|
288
|
trans_gE(c_in, x_in, mem_in, mem_out, out_out, y)
|
|
289
|
&& (clock_gout(c_in, x_in, mem_in, mem_out, out_out, y) ==> trans_gout(c_in, x_in, mem_in, mem_out, out_out, y));
|
|
290
|
*/
|
|
291
|
|
|
292
|
/*@ predicate clock_g__g_2(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int y) =
|
|
293
|
\true;
|
|
294
|
*/
|
|
295
|
|
|
296
|
/*@ predicate trans_g__g_2(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out, int y) =
|
|
297
|
(mem_out._reg.__g_2 == y);
|
|
298
|
*/
|
|
299
|
|
|
300
|
/*@ predicate trans_gG(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out) =
|
|
301
|
\exists int y;
|
|
302
|
trans_gF(c_in, x_in, mem_in, mem_out, out_out, y)
|
|
303
|
&& (clock_g__g_2(c_in, x_in, mem_in, mem_out, out_out, y) ==> trans_g__g_2(c_in, x_in, mem_in, mem_out, out_out, y));
|
|
304
|
*/
|
|
305
|
|
|
306
|
/*@ predicate valid_g(struct g_mem *self) =
|
|
307
|
\valid(self)
|
|
308
|
&& \valid(self->ni_0)
|
|
309
|
&& \valid(self->ni_1)
|
|
310
|
&& valid_f(self->ni_0);
|
|
311
|
*/
|
|
312
|
|
|
313
|
/*@
|
|
314
|
requires valid_g(self);
|
|
315
|
requires \separated(self, (self->ni_0), (self->ni_1), (self->ni_0)->ni_2);
|
|
316
|
ensures \forall struct g_mem_pack mem; g_pack3(mem, self) ==> init_g(mem);
|
|
317
|
assigns (self->ni_1)->_reg._first, (self-> ni_0)->_reg.__f_2, ((self->ni_0)->ni_2)->_reg._first;
|
|
318
|
*/
|
|
319
|
void g_reset (struct g_mem *self) {
|
|
320
|
_arrow_reset(self->ni_1);
|
|
321
|
f_reset(self->ni_0);
|
|
322
|
return;
|
|
323
|
}
|
|
324
|
|
|
325
|
/*@
|
|
326
|
requires \valid(out);
|
|
327
|
requires valid_g(self);
|
|
328
|
requires \separated(self, out, (self->ni_0), (self->ni_1), (self->ni_0)->ni_2);
|
|
329
|
ensures \forall struct g_mem_pack mem_in; \forall struct g_mem_pack mem_out; \at(g_pack3(mem_in, self), Pre) ==> g_pack3(mem_out, self) ==> trans_gG(c, x, mem_in, mem_out, *out);
|
|
330
|
assigns *out, self->_reg.__g_2, (self->ni_1)->_reg._first, (self-> ni_0)->_reg.__f_2, ((self->ni_0)->ni_2)->_reg._first;
|
|
331
|
*/
|
|
332
|
void g_step (_Bool c, int x,
|
|
333
|
int (*out),
|
|
334
|
struct g_mem *self) {
|
|
335
|
_Bool __g_1;
|
|
336
|
int cpt;
|
|
337
|
int last_y;
|
|
338
|
//int t;
|
|
339
|
//int y;
|
|
340
|
//@ assert \forall struct g_mem_pack mem_in; \forall struct g_mem_pack mem_out; \at(g_pack3(mem_in, self), Pre) ==> g_pack0(mem_out, self) ==> trans_gA(c, x, mem_in, mem_out, *out);
|
|
341
|
_once_step (&__g_1, self->ni_1);
|
|
342
|
//@ assert \forall struct g_mem_pack mem_in; \forall struct g_mem_pack mem_out; \at(g_pack3(mem_in, self), Pre) ==> g_pack1(mem_out, self) ==> trans_gB(c, x, mem_in, mem_out, *out, __g_1);
|
|
343
|
if (__g_1) {
|
|
344
|
last_y = 0;
|
|
345
|
} else {
|
|
346
|
last_y = self->_reg.__g_2;
|
|
347
|
}
|
|
348
|
//@ assert \forall struct g_mem_pack mem_in; \forall struct g_mem_pack mem_out; \at(g_pack3(mem_in, self), Pre) ==> g_pack1(mem_out, self) ==> trans_gC(c, x, mem_in, mem_out, *out, last_y);
|
|
349
|
// t |-> last_y
|
|
350
|
if (c) {
|
|
351
|
last_y = x;
|
|
352
|
} else {
|
|
353
|
//last_y = last_y;
|
|
354
|
}
|
|
355
|
//@ assert \forall struct g_mem_pack mem_in; \forall struct g_mem_pack mem_out; \at(g_pack3(mem_in, self), Pre) ==> g_pack1(mem_out, self) ==> trans_gD(c, x, mem_in, mem_out, *out, last_y);
|
|
356
|
// y |-> last_y
|
|
357
|
f_step (last_y, &cpt, &last_y, self->ni_0);
|
|
358
|
//@ assert \forall struct g_mem_pack mem_in; \forall struct g_mem_pack mem_out; \at(g_pack3(mem_in, self), Pre) ==> g_pack2(mem_out, self) ==> trans_gE(c, x, mem_in, mem_out, *out, last_y);
|
|
359
|
if (c) {
|
|
360
|
} else {
|
|
361
|
*out = last_y;
|
|
362
|
}
|
|
363
|
//@ assert \forall struct g_mem_pack mem_in; \forall struct g_mem_pack mem_out; \at(g_pack3(mem_in, self), Pre) ==> g_pack2(mem_out, self) ==> trans_gF(c, x, mem_in, mem_out, *out, last_y);
|
|
364
|
self->_reg.__g_2 = last_y;
|
|
365
|
//@ assert \forall struct g_mem_pack mem_in; \forall struct g_mem_pack mem_out; \at(g_pack3(mem_in, self), Pre) ==> g_pack3(mem_out, self) ==> trans_gG(c, x, mem_in, mem_out, *out);
|
|
366
|
return;
|
|
367
|
}
|
|
368
|
|