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