gen_functions2.c 14.6 KB
Newer Older
1
2
3
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
Julien Signoles's avatar
Julien Signoles committed
4
5
extern int __e_acsl_sound_verdict;

6
7
8
9
10
11
12
struct mystruct {
   int k ;
   int l ;
};
typedef struct mystruct mystruct;
/*@ predicate p1(int x, int y) = x + y > 0;
 */
13
int __gen_e_acsl_p1(int x, int y);
14
15
16
17

/*@ predicate p2(ℤ x, ℤ y) = x + y > 0;

*/
18
int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
Julien Signoles's avatar
Julien Signoles committed
19

20
int __gen_e_acsl_p2(int x, int y);
21
22
23
24

/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;

*/
25
26
void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
                       __e_acsl_mpz_struct * y);
27

28
29
void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
                       __e_acsl_mpz_struct * y);
30

31
void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y);
32

33
34
/*@ logic char h_char(char c) = c;
 */
35
char __gen_e_acsl_h_char(int c);
36
37
38

/*@ logic short h_short(short s) = s;
 */
39
short __gen_e_acsl_h_short(int s);
40
41
42

/*@ logic int g_hidden(int x) = x;
 */
43
int __gen_e_acsl_g_hidden(int x);
44
45
46

/*@ logic int g(int x) = g_hidden(x);
 */
47
int __gen_e_acsl_g(int x);
48
49
50

/*@ logic mystruct t1(mystruct m) = m;
 */
51
mystruct __gen_e_acsl_t1(mystruct m);
52
53

/*@ logic ℤ t2(mystruct m) = m.k + m.l;
54
55
 */
void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m);
56
57
58
59

/*@ predicate k_pred(ℤ x) = x > 0;

*/
60
int __gen_e_acsl_k_pred(int x);
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88

/*@ requires k_pred(x); */
void __gen_e_acsl_k(int x);

void k(int x)
{
  return;
}

int glob = 5;
/*@ predicate never_called(int x) = x ≡ x;
 */
/*@ logic double f2(double x) = (double)(1 / x);
 */
/*@ predicate p_notyet{L}(ℤ x) = x > 0;
 */
/*@ logic ℤ f_notyet{L}(ℤ x) = x;

*/
int main(void)
{
  int __retres;
  mystruct m;
  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
  int x = 1;
  int y = 2;
  /*@ assert p1(x, y); */
  {
89
90
91
    int __gen_e_acsl_p1_2;
    __gen_e_acsl_p1_2 = __gen_e_acsl_p1(x,y);
    __e_acsl_assert(__gen_e_acsl_p1_2,(char *)"Assertion",(char *)"main",
92
93
94
95
                    (char *)"p1(x, y)",42);
  }
  /*@ assert p2(3, 4); */
  {
96
97
98
    int __gen_e_acsl_p2_2;
    __gen_e_acsl_p2_2 = __gen_e_acsl_p2(3,4);
    __e_acsl_assert(__gen_e_acsl_p2_2,(char *)"Assertion",(char *)"main",
99
100
101
102
103
                    (char *)"p2(3, 4)",43);
  }
  /*@ assert p2(5, 99999999999999999999999999999); */
  {
    __e_acsl_mpz_t __gen_e_acsl__3;
104
    int __gen_e_acsl_p2_4;
105
    __gmpz_init_set_str(__gen_e_acsl__3,"99999999999999999999999999999",10);
106
107
108
    __gen_e_acsl_p2_4 = __gen_e_acsl_p2_3(5,
                                          (__e_acsl_mpz_struct *)__gen_e_acsl__3);
    __e_acsl_assert(__gen_e_acsl_p2_4,(char *)"Assertion",(char *)"main",
109
110
111
112
113
                    (char *)"p2(5, 99999999999999999999999999999)",44);
    __gmpz_clear(__gen_e_acsl__3);
  }
  /*@ assert f1(x, y) ≡ 3; */
  {
114
    __e_acsl_mpz_t __gen_e_acsl_f1_2;
115
116
    __e_acsl_mpz_t __gen_e_acsl__5;
    int __gen_e_acsl_eq;
117
    __gen_e_acsl_f1(& __gen_e_acsl_f1_2,x,y);
118
    __gmpz_init_set_si(__gen_e_acsl__5,3L);
119
    __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_2),
120
121
122
                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
    __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
                    (char *)"f1(x, y) == 3",46);
123
    __gmpz_clear(__gen_e_acsl_f1_2);
124
125
126
127
    __gmpz_clear(__gen_e_acsl__5);
  }
  /*@ assert p2(x, f1(3, 4)); */
  {
128
129
130
131
132
133
134
135
136
137
138
139
    __e_acsl_mpz_t __gen_e_acsl_f1_4;
    int __gen_e_acsl_p2_6;
    __gen_e_acsl_f1(& __gen_e_acsl_f1_4,3,4);
    /*@ assert
        Eva: initialization:
          \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_4);
    */
    __gen_e_acsl_p2_6 = __gen_e_acsl_p2_3(x,
                                          (__e_acsl_mpz_struct *)__gen_e_acsl_f1_4);
    __e_acsl_assert(__gen_e_acsl_p2_6,(char *)"Assertion",(char *)"main",
                    (char *)"p2(x, f1(3, 4))",47);
    __gmpz_clear(__gen_e_acsl_f1_4);
140
141
142
143
  }
  /*@ assert f1(9, 99999999999999999999999999999) > 0; */
  {
    __e_acsl_mpz_t __gen_e_acsl__6;
144
    __e_acsl_mpz_t __gen_e_acsl_f1_6;
145
146
147
    __e_acsl_mpz_t __gen_e_acsl__7;
    int __gen_e_acsl_gt_4;
    __gmpz_init_set_str(__gen_e_acsl__6,"99999999999999999999999999999",10);
148
    __gen_e_acsl_f1_5(& __gen_e_acsl_f1_6,9,
149
150
                      (__e_acsl_mpz_struct *)__gen_e_acsl__6);
    __gmpz_init_set_si(__gen_e_acsl__7,0L);
151
    __gen_e_acsl_gt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
152
153
154
155
                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
    __e_acsl_assert(__gen_e_acsl_gt_4 > 0,(char *)"Assertion",(char *)"main",
                    (char *)"f1(9, 99999999999999999999999999999) > 0",48);
    __gmpz_clear(__gen_e_acsl__6);
156
    __gmpz_clear(__gen_e_acsl_f1_6);
157
158
159
160
161
162
163
164
    __gmpz_clear(__gen_e_acsl__7);
  }
  /*@ assert
      f1(99999999999999999999999999999, 99999999999999999999999999999) ≡
      199999999999999999999999999998;
  */
  {
    __e_acsl_mpz_t __gen_e_acsl__8;
165
    __e_acsl_mpz_t __gen_e_acsl_f1_8;
166
167
168
    __e_acsl_mpz_t __gen_e_acsl__9;
    int __gen_e_acsl_eq_2;
    __gmpz_init_set_str(__gen_e_acsl__8,"99999999999999999999999999999",10);
169
    __gen_e_acsl_f1_7(& __gen_e_acsl_f1_8,
170
171
172
                      (__e_acsl_mpz_struct *)__gen_e_acsl__8,
                      (__e_acsl_mpz_struct *)__gen_e_acsl__8);
    __gmpz_init_set_str(__gen_e_acsl__9,"199999999999999999999999999998",10);
173
    __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8),
174
175
176
177
178
179
                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
    __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
                    (char *)"main",
                    (char *)"f1(99999999999999999999999999999, 99999999999999999999999999999) ==\n199999999999999999999999999998",
                    49);
    __gmpz_clear(__gen_e_acsl__8);
180
    __gmpz_clear(__gen_e_acsl_f1_8);
181
182
183
184
    __gmpz_clear(__gen_e_acsl__9);
  }
  /*@ assert g(x) ≡ x; */
  {
185
    int __gen_e_acsl_g_2;
186
    __e_acsl_mpz_t __gen_e_acsl_app;
187
    __e_acsl_mpz_t __gen_e_acsl_x_6;
188
    int __gen_e_acsl_eq_3;
189
190
191
    __gen_e_acsl_g_2 = __gen_e_acsl_g(x);
    __gmpz_init_set_si(__gen_e_acsl_app,(long)__gen_e_acsl_g_2);
    __gmpz_init_set_si(__gen_e_acsl_x_6,(long)x);
192
    __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_app),
193
                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6));
194
195
196
    __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
                    (char *)"main",(char *)"g(x) == x",53);
    __gmpz_clear(__gen_e_acsl_app);
197
    __gmpz_clear(__gen_e_acsl_x_6);
198
199
200
201
  }
  char c = (char)'c';
  /*@ assert h_char(c) ≡ c; */
  {
202
    char __gen_e_acsl_h_char_2;
203
204
205
    __e_acsl_mpz_t __gen_e_acsl_app_2;
    __e_acsl_mpz_t __gen_e_acsl_c;
    int __gen_e_acsl_eq_4;
206
207
    __gen_e_acsl_h_char_2 = __gen_e_acsl_h_char((int)c);
    __gmpz_init_set_si(__gen_e_acsl_app_2,(long)__gen_e_acsl_h_char_2);
208
209
210
211
212
213
214
215
216
217
218
    __gmpz_init_set_si(__gen_e_acsl_c,(long)c);
    __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_app_2),
                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_c));
    __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
                    (char *)"main",(char *)"h_char(c) == c",56);
    __gmpz_clear(__gen_e_acsl_app_2);
    __gmpz_clear(__gen_e_acsl_c);
  }
  short s = (short)1;
  /*@ assert h_short(s) ≡ s; */
  {
219
    short __gen_e_acsl_h_short_2;
220
221
222
    __e_acsl_mpz_t __gen_e_acsl_app_3;
    __e_acsl_mpz_t __gen_e_acsl_s;
    int __gen_e_acsl_eq_5;
223
224
    __gen_e_acsl_h_short_2 = __gen_e_acsl_h_short((int)s);
    __gmpz_init_set_si(__gen_e_acsl_app_3,(long)__gen_e_acsl_h_short_2);
225
226
227
228
229
230
231
232
233
234
235
236
    __gmpz_init_set_si(__gen_e_acsl_s,(long)s);
    __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_app_3),
                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_s));
    __e_acsl_assert(__gen_e_acsl_eq_5 == 0,(char *)"Assertion",
                    (char *)"main",(char *)"h_short(s) == s",58);
    __gmpz_clear(__gen_e_acsl_app_3);
    __gmpz_clear(__gen_e_acsl_s);
  }
  m.k = 8;
  m.l = 9;
  /*@ assert t2(t1(m)) ≡ 17; */
  {
237
238
    mystruct __gen_e_acsl_t1_2;
    __e_acsl_mpz_t __gen_e_acsl_t2_2;
239
240
    __e_acsl_mpz_t __gen_e_acsl__12;
    int __gen_e_acsl_eq_6;
241
242
    __gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
    __gen_e_acsl_t2(& __gen_e_acsl_t2_2,__gen_e_acsl_t1_2);
243
    __gmpz_init_set_si(__gen_e_acsl__12,17L);
244
    __gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_t2_2),
245
246
247
                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
    __e_acsl_assert(__gen_e_acsl_eq_6 == 0,(char *)"Assertion",
                    (char *)"main",(char *)"t2(t1(m)) == 17",63);
248
    __gmpz_clear(__gen_e_acsl_t2_2);
249
250
251
252
253
254
255
256
257
258
259
    __gmpz_clear(__gen_e_acsl__12);
  }
  __gen_e_acsl_k(9);
  __retres = 0;
  return __retres;
}

/*@ requires k_pred(x); */
void __gen_e_acsl_k(int x)
{
  {
260
261
262
263
    int __gen_e_acsl_k_pred_2;
    __gen_e_acsl_k_pred_2 = __gen_e_acsl_k_pred(x);
    __e_acsl_assert(__gen_e_acsl_k_pred_2,(char *)"Precondition",(char *)"k",
                    (char *)"k_pred(x)",25);
264
265
266
267
268
  }
  k(x);
  return;
}

269
270
271
272
273
274
char __gen_e_acsl_h_char(int c)
{
  char __retres = (char)c;
  return __retres;
}

275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
short __gen_e_acsl_h_short(int s)
{
  short __retres = (short)s;
  return __retres;
}

int __gen_e_acsl_g_hidden(int x)
{
  return x;
}

int __gen_e_acsl_g(int x)
{
  int __gen_e_acsl_g_hidden_2;
  __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
  return __gen_e_acsl_g_hidden_2;
}

mystruct __gen_e_acsl_t1(mystruct m)
{
  return m;
}

int __gen_e_acsl_p1(int x, int y)
299
300
{
  __e_acsl_mpz_t __gen_e_acsl_x;
301
302
  __e_acsl_mpz_t __gen_e_acsl_y;
  __e_acsl_mpz_t __gen_e_acsl_add;
303
304
  __e_acsl_mpz_t __gen_e_acsl_;
  int __gen_e_acsl_gt;
305
306
307
308
309
  __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
  __gmpz_init_set_si(__gen_e_acsl_y,(long)y);
  __gmpz_init(__gen_e_acsl_add);
  __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
             (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
310
  __gmpz_init_set_si(__gen_e_acsl_,0L);
311
  __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
312
                               (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
313
  int __retres = __gen_e_acsl_gt > 0;
314
  __gmpz_clear(__gen_e_acsl_x);
315
316
  __gmpz_clear(__gen_e_acsl_y);
  __gmpz_clear(__gen_e_acsl_add);
317
318
319
320
  __gmpz_clear(__gen_e_acsl_);
  return __retres;
}

321
void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
322
323
324
325
{
  __e_acsl_mpz_t __gen_e_acsl__10;
  __e_acsl_mpz_t __gen_e_acsl__11;
  __e_acsl_mpz_t __gen_e_acsl_add_7;
326
327
  __gmpz_init_set_si(__gen_e_acsl__10,(long)m.k);
  __gmpz_init_set_si(__gen_e_acsl__11,(long)m.l);
328
329
330
331
  __gmpz_init(__gen_e_acsl_add_7);
  __gmpz_add(__gen_e_acsl_add_7,
             (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
             (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
332
  __gmpz_init_set(*__retres_arg,
333
334
335
336
337
338
339
                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
  __gmpz_clear(__gen_e_acsl__10);
  __gmpz_clear(__gen_e_acsl__11);
  __gmpz_clear(__gen_e_acsl_add_7);
  return;
}

340
int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
341
342
343
344
345
{
  __e_acsl_mpz_t __gen_e_acsl_x_3;
  __e_acsl_mpz_t __gen_e_acsl_add_3;
  __e_acsl_mpz_t __gen_e_acsl__4;
  int __gen_e_acsl_gt_3;
346
  __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
347
348
349
  __gmpz_init(__gen_e_acsl_add_3);
  __gmpz_add(__gen_e_acsl_add_3,
             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
350
             (__e_acsl_mpz_struct const *)(y));
351
352
353
  __gmpz_init_set_si(__gen_e_acsl__4,0L);
  __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3),
                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
354
  int __retres = __gen_e_acsl_gt_3 > 0;
355
356
357
358
359
360
  __gmpz_clear(__gen_e_acsl_x_3);
  __gmpz_clear(__gen_e_acsl_add_3);
  __gmpz_clear(__gen_e_acsl__4);
  return __retres;
}

361
int __gen_e_acsl_p2(int x, int y)
Julien Signoles's avatar
Julien Signoles committed
362
363
364
365
366
367
{
  __e_acsl_mpz_t __gen_e_acsl_x_2;
  __e_acsl_mpz_t __gen_e_acsl_y_2;
  __e_acsl_mpz_t __gen_e_acsl_add_2;
  __e_acsl_mpz_t __gen_e_acsl__2;
  int __gen_e_acsl_gt_2;
368
369
  __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
  __gmpz_init_set_si(__gen_e_acsl_y_2,(long)y);
Julien Signoles's avatar
Julien Signoles committed
370
371
372
373
374
375
376
  __gmpz_init(__gen_e_acsl_add_2);
  __gmpz_add(__gen_e_acsl_add_2,
             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
             (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
  __gmpz_init_set_si(__gen_e_acsl__2,0L);
  __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
377
  int __retres = __gen_e_acsl_gt_2 > 0;
Julien Signoles's avatar
Julien Signoles committed
378
379
380
381
382
383
384
  __gmpz_clear(__gen_e_acsl_x_2);
  __gmpz_clear(__gen_e_acsl_y_2);
  __gmpz_clear(__gen_e_acsl_add_2);
  __gmpz_clear(__gen_e_acsl__2);
  return __retres;
}

385
int __gen_e_acsl_k_pred(int x)
386
387
388
389
{
  __e_acsl_mpz_t __gen_e_acsl_x;
  __e_acsl_mpz_t __gen_e_acsl_;
  int __gen_e_acsl_gt;
390
  __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
391
  __gmpz_init_set_si(__gen_e_acsl_,0L);
392
  __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
393
                               (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
394
  int __retres = __gen_e_acsl_gt > 0;
395
396
397
398
399
  __gmpz_clear(__gen_e_acsl_x);
  __gmpz_clear(__gen_e_acsl_);
  return __retres;
}

400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
                       __e_acsl_mpz_struct * y)
{
  __e_acsl_mpz_t __gen_e_acsl_add_6;
  __gmpz_init(__gen_e_acsl_add_6);
  __gmpz_add(__gen_e_acsl_add_6,(__e_acsl_mpz_struct const *)(x),
             (__e_acsl_mpz_struct const *)(y));
  __gmpz_init_set(*__retres_arg,
                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
  __gmpz_clear(__gen_e_acsl_add_6);
  return;
}

void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
                       __e_acsl_mpz_struct * y)
{
  __e_acsl_mpz_t __gen_e_acsl_x_5;
  __e_acsl_mpz_t __gen_e_acsl_add_5;
  __gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
  __gmpz_init(__gen_e_acsl_add_5);
  __gmpz_add(__gen_e_acsl_add_5,
             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
             (__e_acsl_mpz_struct const *)(y));
  __gmpz_init_set(*__retres_arg,
                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
  __gmpz_clear(__gen_e_acsl_x_5);
  __gmpz_clear(__gen_e_acsl_add_5);
  return;
}

void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
{
  __e_acsl_mpz_t __gen_e_acsl_x_4;
  __e_acsl_mpz_t __gen_e_acsl_y_3;
  __e_acsl_mpz_t __gen_e_acsl_add_4;
  __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
  __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
  __gmpz_init(__gen_e_acsl_add_4);
  __gmpz_add(__gen_e_acsl_add_4,
             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
             (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
  __gmpz_init_set(*__retres_arg,
                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
  __gmpz_clear(__gen_e_acsl_x_4);
  __gmpz_clear(__gen_e_acsl_y_3);
  __gmpz_clear(__gen_e_acsl_add_4);
  return;
}

449