Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (13.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 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
}