Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / oversampling0_4.c @ 6a93d814

History | View | Annotate | Download (14.4 KB)

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