1
2
3
4#line 50 "/usr/include/bits/pthreadtypes.h"
5typedef unsigned long pthread_t;
6#line 53 "/usr/include/bits/pthreadtypes.h"
7union __anonunion_pthread_attr_t_3 {
8 char __size[56] ;
9 long __align ;
10};
11#line 53 "/usr/include/bits/pthreadtypes.h"
12typedef union __anonunion_pthread_attr_t_3 pthread_attr_t;
13#line 61 "/usr/include/bits/pthreadtypes.h"
14struct __pthread_internal_list {
15 struct __pthread_internal_list *__prev ;
16 struct __pthread_internal_list *__next ;
17};
18#line 61 "/usr/include/bits/pthreadtypes.h"
19typedef struct __pthread_internal_list __pthread_list_t;
20#line 76 "/usr/include/bits/pthreadtypes.h"
21struct __pthread_mutex_s {
22 int __lock ;
23 unsigned int __count ;
24 int __owner ;
25 unsigned int __nusers ;
26 int __kind ;
27 int __spins ;
28 __pthread_list_t __list ;
29};
30#line 76 "/usr/include/bits/pthreadtypes.h"
31union __anonunion_pthread_mutex_t_4 {
32 struct __pthread_mutex_s __data ;
33 char __size[40] ;
34 long __align ;
35};
36#line 76 "/usr/include/bits/pthreadtypes.h"
37typedef union __anonunion_pthread_mutex_t_4 pthread_mutex_t;
38#line 106 "/usr/include/bits/pthreadtypes.h"
39union __anonunion_pthread_mutexattr_t_5 {
40 char __size[4] ;
41 int __align ;
42};
43#line 106 "/usr/include/bits/pthreadtypes.h"
44typedef union __anonunion_pthread_mutexattr_t_5 pthread_mutexattr_t;
45#line 11 "queue_bad.c"
46struct __anonstruct_QType_29 {
47 int element[20] ;
48 int head ;
49 int tail ;
50 int amount ;
51};
52#line 11 "queue_bad.c"
53typedef struct __anonstruct_QType_29 QType;
54#line 225 "/usr/include/pthread.h"
55extern __attribute__((__nothrow__)) int pthread_create(pthread_t * __restrict __newthread ,
56 pthread_attr_t const * __restrict __attr ,
57 void *(*__start_routine)(void * ) ,
58 void * __restrict __arg ) __attribute__((__nonnull__(1,3))) ;
59#line 242
60extern int pthread_join(pthread_t __th , void **__thread_return ) ;
61#line 733
62extern __attribute__((__nothrow__)) int pthread_mutex_init(pthread_mutex_t *__mutex ,
63 pthread_mutexattr_t const *__mutexattr ) __attribute__((__nonnull__(1))) ;
64#line 746
65extern __attribute__((__nothrow__)) int pthread_mutex_lock(pthread_mutex_t *__mutex ) __attribute__((__nonnull__(1))) ;
66#line 757
67extern __attribute__((__nothrow__)) int pthread_mutex_unlock(pthread_mutex_t *__mutex ) __attribute__((__nonnull__(1))) ;
68#line 359 "/usr/include/stdio.h"
69extern int printf(char const * __restrict __format , ...) ;
70#line 18 "queue_bad.c"
71pthread_mutex_t m ;
72#line 19
73extern int nondet_int() ;
74#line 20 "queue_bad.c"
75int stored_elements[20] ;
76#line 21 "queue_bad.c"
77_Bool enqueue_flag ;
78#line 21 "queue_bad.c"
79_Bool dequeue_flag ;
80#line 22 "queue_bad.c"
81QType queue ;
82#line 24 "queue_bad.c"
83int init(QType *q )
84{ unsigned int __cil_tmp2 ;
85 unsigned int __cil_tmp3 ;
86 unsigned int __cil_tmp4 ;
87 unsigned int __cil_tmp5 ;
88 unsigned int __cil_tmp6 ;
89 unsigned int __cil_tmp7 ;
90
91 {
92#line 26
93 __cil_tmp2 = (unsigned int )q;
94#line 26
95 __cil_tmp3 = __cil_tmp2 + 80;
96#line 26
97 *((int *)__cil_tmp3) = 0;
98#line 27
99 __cil_tmp4 = (unsigned int )q;
100#line 27
101 __cil_tmp5 = __cil_tmp4 + 84;
102#line 27
103 *((int *)__cil_tmp5) = 0;
104#line 28
105 __cil_tmp6 = (unsigned int )q;
106#line 28
107 __cil_tmp7 = __cil_tmp6 + 88;
108#line 28
109 *((int *)__cil_tmp7) = 0;
110#line 29
111 return (0);
112}
113}
114#line 31 "queue_bad.c"
115int empty(QType *q )
116{ unsigned int __cil_tmp2 ;
117 unsigned int __cil_tmp3 ;
118 int __cil_tmp4 ;
119 unsigned int __cil_tmp5 ;
120 unsigned int __cil_tmp6 ;
121 int __cil_tmp7 ;
122 char const * __restrict __cil_tmp8 ;
123
124 {
125 {
126#line 33
127 __cil_tmp2 = (unsigned int )q;
128#line 33
129 __cil_tmp3 = __cil_tmp2 + 84;
130#line 33
131 __cil_tmp4 = *((int *)__cil_tmp3);
132#line 33
133 __cil_tmp5 = (unsigned int )q;
134#line 33
135 __cil_tmp6 = __cil_tmp5 + 80;
136#line 33
137 __cil_tmp7 = *((int *)__cil_tmp6);
138#line 33
139 if (__cil_tmp7 == __cil_tmp4) {
140 {
141#line 35
142 __cil_tmp8 = (char const * __restrict )"queue is empty\n";
143#line 35
144 printf(__cil_tmp8);
145 }
146#line 36
147 return (-1);
148 } else {
149#line 39
150 return (0);
151 }
152 }
153}
154}
155#line 42 "queue_bad.c"
156int full(QType *q )
157{ unsigned int __cil_tmp2 ;
158 unsigned int __cil_tmp3 ;
159 int __cil_tmp4 ;
160 char const * __restrict __cil_tmp5 ;
161
162 {
163 {
164#line 44
165 __cil_tmp2 = (unsigned int )q;
166#line 44
167 __cil_tmp3 = __cil_tmp2 + 88;
168#line 44
169 __cil_tmp4 = *((int *)__cil_tmp3);
170#line 44
171 if (__cil_tmp4 == 20) {
172 {
173#line 46
174 __cil_tmp5 = (char const * __restrict )"queue is full\n";
175#line 46
176 printf(__cil_tmp5);
177 }
178#line 47
179 return (-2);
180 } else {
181#line 50
182 return (0);
183 }
184 }
185}
186}
187#line 53 "queue_bad.c"
188int enqueue(QType *q , int x )
189{ unsigned int __cil_tmp3 ;
190 unsigned int __cil_tmp4 ;
191 int __cil_tmp5 ;
192 unsigned int __cil_tmp6 ;
193 unsigned int __cil_tmp7 ;
194 unsigned int __cil_tmp8 ;
195 unsigned int __cil_tmp9 ;
196 unsigned int __cil_tmp10 ;
197 unsigned int __cil_tmp11 ;
198 unsigned int __cil_tmp12 ;
199 unsigned int __cil_tmp13 ;
200 int __cil_tmp14 ;
201 unsigned int __cil_tmp15 ;
202 unsigned int __cil_tmp16 ;
203 int __cil_tmp17 ;
204 unsigned int __cil_tmp18 ;
205 unsigned int __cil_tmp19 ;
206 unsigned int __cil_tmp20 ;
207 unsigned int __cil_tmp21 ;
208 unsigned int __cil_tmp22 ;
209 unsigned int __cil_tmp23 ;
210 int __cil_tmp24 ;
211
212 {
213#line 55
214 __cil_tmp3 = (unsigned int )q;
215#line 55
216 __cil_tmp4 = __cil_tmp3 + 84;
217#line 55
218 __cil_tmp5 = *((int *)__cil_tmp4);
219#line 55
220 __cil_tmp6 = __cil_tmp5 * 4U;
221#line 55
222 __cil_tmp7 = 0 + __cil_tmp6;
223#line 55
224 __cil_tmp8 = (unsigned int )q;
225#line 55
226 __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
227#line 55
228 *((int *)__cil_tmp9) = x;
229#line 56
230 __cil_tmp10 = (unsigned int )q;
231#line 56
232 __cil_tmp11 = __cil_tmp10 + 88;
233#line 56
234 __cil_tmp12 = (unsigned int )q;
235#line 56
236 __cil_tmp13 = __cil_tmp12 + 88;
237#line 56
238 __cil_tmp14 = *((int *)__cil_tmp13);
239#line 56
240 *((int *)__cil_tmp11) = __cil_tmp14 + 1;
241 {
242#line 57
243 __cil_tmp15 = (unsigned int )q;
244#line 57
245 __cil_tmp16 = __cil_tmp15 + 84;
246#line 57
247 __cil_tmp17 = *((int *)__cil_tmp16);
248#line 57
249 if (__cil_tmp17 == 20) {
250#line 59
251 __cil_tmp18 = (unsigned int )q;
252#line 59
253 __cil_tmp19 = __cil_tmp18 + 84;
254#line 59
255 *((int *)__cil_tmp19) = 1;
256 } else {
257#line 63
258 __cil_tmp20 = (unsigned int )q;
259#line 63
260 __cil_tmp21 = __cil_tmp20 + 84;
261#line 63
262 __cil_tmp22 = (unsigned int )q;
263#line 63
264 __cil_tmp23 = __cil_tmp22 + 84;
265#line 63
266 __cil_tmp24 = *((int *)__cil_tmp23);
267#line 63
268 *((int *)__cil_tmp21) = __cil_tmp24 + 1;
269 }
270 }
271#line 66
272 return (0);
273}
274}
275#line 69 "queue_bad.c"
276int dequeue(QType *q )
277{ int x ;
278 unsigned int __cil_tmp3 ;
279 unsigned int __cil_tmp4 ;
280 int __cil_tmp5 ;
281 unsigned int __cil_tmp6 ;
282 unsigned int __cil_tmp7 ;
283 unsigned int __cil_tmp8 ;
284 unsigned int __cil_tmp9 ;
285 unsigned int __cil_tmp10 ;
286 unsigned int __cil_tmp11 ;
287 unsigned int __cil_tmp12 ;
288 unsigned int __cil_tmp13 ;
289 int __cil_tmp14 ;
290 unsigned int __cil_tmp15 ;
291 unsigned int __cil_tmp16 ;
292 int __cil_tmp17 ;
293 unsigned int __cil_tmp18 ;
294 unsigned int __cil_tmp19 ;
295 unsigned int __cil_tmp20 ;
296 unsigned int __cil_tmp21 ;
297 unsigned int __cil_tmp22 ;
298 unsigned int __cil_tmp23 ;
299 int __cil_tmp24 ;
300
301 {
302#line 73
303 __cil_tmp3 = (unsigned int )q;
304#line 73
305 __cil_tmp4 = __cil_tmp3 + 80;
306#line 73
307 __cil_tmp5 = *((int *)__cil_tmp4);
308#line 73
309 __cil_tmp6 = __cil_tmp5 * 4U;
310#line 73
311 __cil_tmp7 = 0 + __cil_tmp6;
312#line 73
313 __cil_tmp8 = (unsigned int )q;
314#line 73
315 __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
316#line 73
317 x = *((int *)__cil_tmp9);
318#line 74
319 __cil_tmp10 = (unsigned int )q;
320#line 74
321 __cil_tmp11 = __cil_tmp10 + 88;
322#line 74
323 __cil_tmp12 = (unsigned int )q;
324#line 74
325 __cil_tmp13 = __cil_tmp12 + 88;
326#line 74
327 __cil_tmp14 = *((int *)__cil_tmp13);
328#line 74
329 *((int *)__cil_tmp11) = __cil_tmp14 - 1;
330 {
331#line 75
332 __cil_tmp15 = (unsigned int )q;
333#line 75
334 __cil_tmp16 = __cil_tmp15 + 80;
335#line 75
336 __cil_tmp17 = *((int *)__cil_tmp16);
337#line 75
338 if (__cil_tmp17 == 20) {
339#line 77
340 __cil_tmp18 = (unsigned int )q;
341#line 77
342 __cil_tmp19 = __cil_tmp18 + 80;
343#line 77
344 *((int *)__cil_tmp19) = 1;
345 } else {
346#line 80
347 __cil_tmp20 = (unsigned int )q;
348#line 80
349 __cil_tmp21 = __cil_tmp20 + 80;
350#line 80
351 __cil_tmp22 = (unsigned int )q;
352#line 80
353 __cil_tmp23 = __cil_tmp22 + 80;
354#line 80
355 __cil_tmp24 = *((int *)__cil_tmp23);
356#line 80
357 *((int *)__cil_tmp21) = __cil_tmp24 + 1;
358 }
359 }
360#line 82
361 return (x);
362}
363}
364#line 85 "queue_bad.c"
365void *t1(void *arg )
366{ int value ;
367 int i ;
368 int tmp ;
369 int tmp___0 ;
370 unsigned int __cil_tmp6 ;
371 unsigned int __cil_tmp7 ;
372 int __cil_tmp8 ;
373 unsigned int __cil_tmp9 ;
374 unsigned int __cil_tmp10 ;
375
376 {
377 {
378#line 89
379 pthread_mutex_lock(& m);
380#line 90
381 value = nondet_int();
382#line 91
383 tmp = enqueue(& queue, value);
384 }
385#line 91
386 if (tmp) {
387 goto ERROR;
388 } else {
389
390 }
391 {
392#line 95
393 __cil_tmp6 = 0 * 4U;
394#line 95
395 __cil_tmp7 = (unsigned int )(stored_elements) + __cil_tmp6;
396#line 95
397 *((int *)__cil_tmp7) = value;
398#line 96
399 tmp___0 = empty(& queue);
400 }
401#line 96
402 if (tmp___0) {
403 goto ERROR;
404 } else {
405
406 }
407 {
408#line 100
409 pthread_mutex_unlock(& m);
410#line 102
411 i = 0;
412 }
413 {
414#line 102
415 while (1) {
416 while_0_continue: ;
417#line 102
418 if (i < 19) {
419
420 } else {
421 goto while_0_break;
422 }
423 {
424#line 104
425 pthread_mutex_lock(& m);
426 }
427#line 105
428 if (enqueue_flag) {
429 {
430#line 107
431 value = nondet_int();
432#line 108
433 enqueue(& queue, value);
434#line 109
435 __cil_tmp8 = i + 1;
436#line 109
437 __cil_tmp9 = __cil_tmp8 * 4U;
438#line 109
439 __cil_tmp10 = (unsigned int )(stored_elements) + __cil_tmp9;
440#line 109
441 *((int *)__cil_tmp10) = value;
442#line 110
443 enqueue_flag = (_Bool)0;
444#line 111
445 dequeue_flag = (_Bool)1;
446 }
447 } else {
448
449 }
450 {
451#line 113
452 pthread_mutex_unlock(& m);
453#line 102
454 i = i + 1;
455 }
456 }
457 while_0_break: ;
458 }
459#line 116
460 return ((void *)0);
461 ERROR: ;
462#line 120
463 return ((void *)0);
464}
465}
466#line 122 "queue_bad.c"
467void *t2(void *arg )
468{ int i ;
469 int tmp ;
470 int tmp___0 ;
471 unsigned int __cil_tmp5 ;
472 unsigned int __cil_tmp6 ;
473 int __cil_tmp7 ;
474
475 {
476#line 126
477 i = 0;
478 {
479#line 126
480 while (1) {
481 while_1_continue: ;
482#line 126
483 if (i < 20) {
484
485 } else {
486 goto while_1_break;
487 }
488 {
489#line 128
490 pthread_mutex_lock(& m);
491 }
492#line 129
493 if (dequeue_flag) {
494 {
495#line 131
496 tmp = dequeue(& queue);
497 }
498#line 131
499 if (tmp) {
500#line 131
501 tmp___0 = 0;
502 } else {
503#line 131
504 tmp___0 = 1;
505 }
506 {
507#line 131
508 __cil_tmp5 = i * 4U;
509#line 131
510 __cil_tmp6 = (unsigned int )(stored_elements) + __cil_tmp5;
511#line 131
512 __cil_tmp7 = *((int *)__cil_tmp6);
513#line 131
514 if (tmp___0 == __cil_tmp7) {
515 goto ERROR;
516 ERROR: ;
517 } else {
518
519 }
520 }
521#line 136
522 dequeue_flag = (_Bool)0;
523#line 137
524 enqueue_flag = (_Bool)1;
525 } else {
526
527 }
528 {
529#line 139
530 pthread_mutex_unlock(& m);
531#line 126
532 i = i + 1;
533 }
534 }
535 while_1_break: ;
536 }
537#line 142
538 return ((void *)0);
539}
540}
541#line 145 "queue_bad.c"
542int main(void)
543{ pthread_t id1 ;
544 pthread_t id2 ;
545 int tmp ;
546 int tmp___0 ;
547 pthread_mutexattr_t const *__cil_tmp5 ;
548 pthread_t * __restrict __cil_tmp6 ;
549 void *__cil_tmp7 ;
550 pthread_attr_t const * __restrict __cil_tmp8 ;
551 void * __restrict __cil_tmp9 ;
552 pthread_t * __restrict __cil_tmp10 ;
553 void *__cil_tmp11 ;
554 pthread_attr_t const * __restrict __cil_tmp12 ;
555 void * __restrict __cil_tmp13 ;
556 pthread_t *__cil_tmp14 ;
557 pthread_t __cil_tmp15 ;
558 void *__cil_tmp16 ;
559 void **__cil_tmp17 ;
560 pthread_t *__cil_tmp18 ;
561 pthread_t __cil_tmp19 ;
562 void *__cil_tmp20 ;
563 void **__cil_tmp21 ;
564
565 {
566 {
567#line 149
568 enqueue_flag = (_Bool)1;
569#line 150
570 dequeue_flag = (_Bool)0;
571#line 152
572 init(& queue);
573#line 154
574 tmp = empty(& queue);
575 }
576#line 154
577 if (tmp) {
578#line 154
579 tmp___0 = 0;
580 } else {
581#line 154
582 tmp___0 = 1;
583 }
584#line 154
585 if (tmp___0 == -1) {
586 goto ERROR;
587 ERROR: ;
588 } else {
589
590 }
591 {
592#line 161
593 __cil_tmp5 = (pthread_mutexattr_t const *)0;
594#line 161
595 pthread_mutex_init(& m, __cil_tmp5);
596#line 163
597 __cil_tmp6 = (pthread_t * __restrict )(& id1);
598#line 163
599 __cil_tmp7 = (void *)0;
600#line 163
601 __cil_tmp8 = (pthread_attr_t const * __restrict )__cil_tmp7;
602#line 163
603 __cil_tmp9 = (void * __restrict )(& queue);
604#line 163
605 pthread_create(__cil_tmp6, __cil_tmp8, & t1, __cil_tmp9);
606#line 164
607 __cil_tmp10 = (pthread_t * __restrict )(& id2);
608#line 164
609 __cil_tmp11 = (void *)0;
610#line 164
611 __cil_tmp12 = (pthread_attr_t const * __restrict )__cil_tmp11;
612#line 164
613 __cil_tmp13 = (void * __restrict )(& queue);
614#line 164
615 pthread_create(__cil_tmp10, __cil_tmp12, & t2, __cil_tmp13);
616#line 166
617 __cil_tmp14 = & id1;
618#line 166
619 __cil_tmp15 = *__cil_tmp14;
620#line 166
621 __cil_tmp16 = (void *)0;
622#line 166
623 __cil_tmp17 = (void **)__cil_tmp16;
624#line 166
625 pthread_join(__cil_tmp15, __cil_tmp17);
626#line 167
627 __cil_tmp18 = & id2;
628#line 167
629 __cil_tmp19 = *__cil_tmp18;
630#line 167
631 __cil_tmp20 = (void *)0;
632#line 167
633 __cil_tmp21 = (void **)__cil_tmp20;
634#line 167
635 pthread_join(__cil_tmp19, __cil_tmp21);
636 }
637#line 169
638 return (0);
639}
640}