Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / oversampling0_3.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
/* 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 f_mem {struct f_reg {int __f_2; } _reg; struct _arrow_mem *ni_2; };
14

    
15
//@ ghost struct _arrow_mem_pack { struct _arrow_reg _reg; };
16

    
17
/*@ predicate init_arrow (struct _arrow_mem_pack mem_in) =
18
       (mem_in._reg._first == true);
19
 */
20
/*@ predicate trans_arrow(struct _arrow_mem_pack mem_in,struct _arrow_mem_pack mem_out, _Bool out) = 
21
       (out == mem_in._reg._first)
22
    && (mem_in._reg._first)?(mem_out._reg._first == false):(mem_out._reg._first == mem_in._reg._first);
23
*/
24

    
25
/*@ predicate _arrow_pack (struct _arrow_mem_pack memp, struct _arrow_mem *mem) =
26
       (memp._reg._first == mem->_reg._first);
27
*/
28

    
29
//@ ghost struct f_mem_pack {struct f_reg _reg; struct _arrow_mem_pack ni_2; };
30

    
31

    
32
/*@ predicate f_pack0 (struct f_mem_pack memp, struct f_mem *mem) =
33
    \true;
34
*/
35

    
36
/*@ predicate f_pack1 (struct f_mem_pack memp, struct f_mem *mem) =
37
       f_pack0(memp, mem)
38
    && _arrow_pack(memp.ni_2, mem->ni_2);
39
*/
40

    
41
/*@ predicate f_pack2 (struct f_mem_pack memp, struct f_mem *mem) =
42
       f_pack1(memp, mem)
43
    && (memp._reg.__f_2 == mem->_reg.__f_2);
44
*/
45

    
46

    
47
/* Scheduling:   y ; __f_1 ; __f_3 ; cpt ; __f_2
48
   Steps:      A   B       C       D     E       F
49
   Mem steps:  0           1                     2
50
   Death table: __f_3 |-> __f_1, cpt |-> __f_3
51
   Reuse table: {}
52
*/
53

    
54

    
55
/*@ predicate init_f(struct f_mem_pack mem_in) =
56
       init_arrow(mem_in.ni_2);
57
 */
58

    
59
/*@ predicate trans_fA(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out) =
60
    \true;
61
*/
62

    
63
/*@ predicate trans_fy(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out) =
64
    (y_out == x_in + 1);
65
*/
66

    
67
/*@ predicate clock_fy(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out) =
68
    \true;
69
*/
70

    
71
/*@ predicate trans_fB(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out) =
72
       trans_fA(x_in, mem_in, mem_out, y_out)
73
    && (clock_fy(x_in, mem_in, mem_out) ==> trans_fy(x_in, mem_in, mem_out, y_out));
74
*/
75

    
76
/*@ 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) =
77
       trans_arrow(mem_in.ni_2, mem_out.ni_2, __f_1);
78
*/
79

    
80
/*@ predicate clock_f__f_1(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out) =
81
    \true;
82
*/
83

    
84
/*@ predicate trans_fC(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, _Bool __f_1) =
85
       trans_fB(x_in, mem_in, mem_out, y_out)
86
    && (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));
87
*/
88

    
89
/*@ 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) =
90
    (__f_1)?(__f_3 == 0):(__f_3 == mem_in._reg.__f_2);
91
*/
92

    
93
/*@ 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) =
94
    \true;
95
*/
96

    
97
/*@ predicate trans_fD(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, int __f_3) =
98
    \exists _Bool __f_1;
99
       trans_fC(x_in, mem_in, mem_out, y_out, __f_1)
100
    && (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));
101
*/
102

    
103
/*@ 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) =
104
    (cpt_out == __f_3 + 1);
105
*/
106

    
107
/*@ predicate clock_fcpt(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, int __f_3) =
108
    \true;
109
*/
110

    
111
/*@ predicate trans_fE(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, int cpt_out) =
112
    \exists int __f_3;
113
       trans_fD(x_in, mem_in, mem_out, y_out, __f_3)
114
    && (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));
115
*/
116

    
117
/*@ 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) =
118
    (mem_out._reg.__f_2 == cpt_out);
119
*/
120

    
121
/*@ 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) =
122
    \true;
123
*/
124

    
125
/*@ predicate trans_fF(int x_in, struct f_mem_pack mem_in, struct f_mem_pack mem_out, int y_out, int cpt_out) =
126
       trans_fE(x_in, mem_in, mem_out, y_out, cpt_out)
127
    && (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));
128
*/
129

    
130
/*@ predicate valid_f(struct f_mem *self) =
131
       \valid(self)
132
    && \valid(self->ni_2);
133

134
 */
135

    
136
/*@
137
    requires valid_f(self);
138
    requires \separated(self, (self->ni_2));
139
    ensures \forall struct f_mem_pack mem; f_pack2(mem, self) ==> init_f(mem);
140
    assigns (self->ni_2)->_reg._first;
141
*/
142
void f_reset (struct f_mem *self) {
143
  _arrow_reset(self->ni_2);
144
  return;
145
}
146

    
147
/*@
148
    requires valid_f(self);
149
    requires \valid(cpt);
150
    requires \valid(y);
151
    requires \separated(self, cpt, y, (self->ni_2));
152
    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);
153
    assigns *cpt, *y, self->_reg.__f_2, (self->ni_2)->_reg._first;
154
*/
155
void f_step (int x, 
156
             int (*cpt), int (*y),
157
             struct f_mem *self) {
158
  _Bool __f_1;
159
  int __f_3;
160
  //@ 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);
161
  *y = (x + 1);
162
  //@ 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);
163
  _once_step (&__f_1, self->ni_2);
164
  //@ 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);
165
  if (__f_1) {
166
    __f_3 = 0;
167
  } else {
168
    __f_3 = self->_reg.__f_2;
169
  }
170
  //@ 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);
171
  *cpt = (__f_3 + 1);
172
  //@ 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);
173
  self->_reg.__f_2 = *cpt;
174
  //@ 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);
175
  return;
176
}
177

    
178

    
179
/* ***************************************************************************** */
180

    
181
struct g_mem {struct g_reg {int __g_2; } _reg; struct _arrow_mem *ni_1; struct f_mem *ni_0; };
182

    
183
//@ ghost struct g_mem_pack {struct g_reg _reg; struct _arrow_mem_pack ni_1; struct f_mem_pack ni_0; };
184

    
185

    
186
/*@ predicate g_pack0 (struct g_mem_pack memp, struct g_mem *mem) =
187
    \true;
188
*/
189

    
190
/*@ predicate g_pack1 (struct g_mem_pack memp, struct g_mem *mem) =
191
       g_pack0(memp, mem)
192
    && _arrow_pack(memp.ni_1, mem->ni_1);
193
*/
194

    
195
/*@ predicate g_pack2 (struct g_mem_pack memp, struct g_mem *mem) =
196
       g_pack1(memp, mem)
197
    && f_pack2(memp.ni_0, mem->ni_0);
198
*/
199

    
200
/*@ predicate g_pack3 (struct g_mem_pack memp, struct g_mem *mem) =
201
       g_pack2(memp, mem)
202
    && (memp._reg.__g_2 == mem->_reg.__g_2);
203
*/
204

    
205
/* Scheduling:   __g_1 ; last_y ; t ; y ; out ; cpt ; __g_2
206
   Real sched:   __g_1 ; last_y ; t ; (y, cpt) ; out ; __g_2
207
   Steps:      A       B        C   D          E     F       G
208
   Mem steps:  0       1                       2             3
209
   Death table: last_y |-> __g_1, t |-> last_y, (y, cpt) |-> {t, cpt}, __g_2 |-> y
210
   Reuse table: t |-> last_y, y |-> last_y
211
*/
212

    
213

    
214
/*@ predicate init_g(struct g_mem_pack mem_in) =
215
       init_f(mem_in.ni_0)
216
    && init_arrow(mem_in.ni_1);
217
*/
218

    
219
/*@ predicate trans_gA(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out) =
220
      \true;
221
*/
222

    
223
/*@ 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) =
224
      \true;
225
 */
226

    
227
/*@ 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) =
228
       trans_arrow(mem_in.ni_1, mem_out.ni_1, __g_1);
229
 */
230

    
231
/*@ 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) =
232
       trans_gA(c_in, x_in, mem_in, mem_out, out_out)
233
    && (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));
234
*/
235

    
236
/*@ 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) =
237
      \true;
238
 */
239

    
240
/*@ 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) =
241
      (__g_1)?(last_y == 0):(last_y == mem_in._reg.__g_2);
242
 */
243

    
244
/*@ 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) =
245
    \exists  _Bool __g_1;
246
       trans_gB(c_in, x_in, mem_in, mem_out, out_out, __g_1)
247
    && (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));
248
*/
249

    
250
/*@ 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) =
251
      \true;
252
 */
253

    
254
/*@ 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) =
255
      (c_in)?(t == x_in):(t == last_y);
256
 */
257

    
258
/*@ 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) =
259
    \exists int last_y;
260
       trans_gC(c_in, x_in, mem_in, mem_out, out_out, last_y)
261
    && (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));
262
*/
263

    
264
/*@ 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) =
265
      \true;
266
 */
267

    
268
/*@ 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) =
269
      trans_fF(t, mem_in.ni_0, mem_out.ni_0, y, cpt);
270
 */
271

    
272
/*@ 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) =
273
    \exists int t, int cpt;
274
       trans_gD(c_in, x_in, mem_in, mem_out, out_out, t)
275
    && (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));
276
*/
277

    
278
/*@ 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) =
279
      (c_in == false);
280
 */
281

    
282
/*@ 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) =
283
      (out_out == y);
284
 */
285

    
286
/*@ 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) =
287
       trans_gE(c_in, x_in, mem_in, mem_out, out_out, y)
288
    && (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));
289
*/
290

    
291
/*@ 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) =
292
      \true;
293
 */
294

    
295
/*@ 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) =
296
      (mem_out._reg.__g_2 == y);
297
 */
298

    
299
/*@ predicate trans_gG(_Bool c_in, int x_in, struct g_mem_pack mem_in, struct g_mem_pack mem_out, int out_out) =
300
    \exists int y;
301
       trans_gF(c_in, x_in, mem_in, mem_out, out_out, y)
302
    && (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));
303
*/
304

    
305
/*@ predicate valid_g(struct g_mem *self) =
306
       \valid(self)
307
    && \valid(self->ni_0)
308
    && \valid(self->ni_1)
309
    && valid_f(self->ni_0);
310
 */
311

    
312
/*@
313
    requires valid_g(self);
314
    requires \separated(self, (self->ni_0), (self->ni_1), (self->ni_0)->ni_2);
315
    ensures \forall struct g_mem_pack mem; g_pack3(mem, self) ==> init_g(mem);
316
    assigns (self->ni_1)->_reg._first, (self-> ni_0)->_reg.__f_2, ((self->ni_0)->ni_2)->_reg._first;
317
*/
318
void g_reset (struct g_mem *self) {
319
  _arrow_reset(self->ni_1);
320
  f_reset(self->ni_0);
321
  return;
322
}
323

    
324
/*@
325
    requires \valid(out);
326
    requires valid_g(self);
327
    requires \separated(self, out, (self->ni_0), (self->ni_1), (self->ni_0)->ni_2);
328
    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);
329
    assigns *out, self->_reg.__g_2, (self->ni_1)->_reg._first, (self-> ni_0)->_reg.__f_2, ((self->ni_0)->ni_2)->_reg._first;
330
*/
331
void g_step (_Bool c, int x, 
332
             int (*out),
333
             struct g_mem *self) {
334
  _Bool __g_1;
335
  int cpt;
336
  int last_y;
337
  //int t;
338
  //int y;
339
  //@ 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);
340
  _once_step (&__g_1, self->ni_1);
341
  //@ 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);
342
  if (__g_1) {
343
    last_y = 0;
344
  } else {
345
    last_y = self->_reg.__g_2;
346
  }
347
  //@ 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);
348
  // t |-> last_y
349
  if (c) {
350
    last_y = x;
351
  } else {
352
    //last_y = last_y;
353
  }
354
  //@ 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);
355
  // y |-> last_y
356
  f_step (last_y, &cpt, &last_y, self->ni_0);
357
  //@ 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);
358
  if (c) {
359
  } else {
360
    *out = last_y;
361
  }
362
  //@ 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);
363
  self->_reg.__g_2 = last_y;
364
  //@ 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);
365
  return;
366
}
367