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_ok.c"
46struct __anonstruct_QType_29 {
47 int element[20] ;
48 int head ;
49 int tail ;
50 int amount ;
51};
52#line 11 "queue_ok.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_ok.c"
71pthread_mutex_t m ;
72#line 19
73extern int nondet_int() ;
74#line 20 "queue_ok.c"
75int stored_elements[20] ;
76#line 21 "queue_ok.c"
77_Bool enqueue_flag ;
78#line 21 "queue_ok.c"
79_Bool dequeue_flag ;
80#line 22 "queue_ok.c"
81QType queue ;
82#line 24 "queue_ok.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_ok.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_ok.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_ok.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_ok.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_ok.c"
365void *t1(void *arg )
366{ int value ;
367 int i ;
368 unsigned int __cil_tmp4 ;
369 unsigned int __cil_tmp5 ;
370
371 {
372 {
373#line 89
374 pthread_mutex_lock(& m);
375 }
376#line 90
377 if (enqueue_flag) {
378#line 92
379 i = 0;
380 {
381#line 92
382 while (1) {
383 while_0_continue: ;
384#line 92
385 if (i < 20) {
386
387 } else {
388 goto while_0_break;
389 }
390 {
391#line 94
392 value = nondet_int();
393#line 95
394 enqueue(& queue, value);
395#line 96
396 __cil_tmp4 = i * 4U;
397#line 96
398 __cil_tmp5 = (unsigned int )(stored_elements) + __cil_tmp4;
399#line 96
400 *((int *)__cil_tmp5) = value;
401#line 92
402 i = i + 1;
403 }
404 }
405 while_0_break: ;
406 }
407#line 98
408 enqueue_flag = (_Bool)0;
409#line 99
410 dequeue_flag = (_Bool)1;
411 } else {
412
413 }
414 {
415#line 101
416 pthread_mutex_unlock(& m);
417 }
418#line 103
419 return ((void *)0);
420}
421}
422#line 106 "queue_ok.c"
423void *t2(void *arg )
424{ int i ;
425 int tmp ;
426 int tmp___0 ;
427 int tmp___1 ;
428 unsigned int __cil_tmp6 ;
429 unsigned int __cil_tmp7 ;
430 int __cil_tmp8 ;
431
432 {
433 {
434#line 110
435 pthread_mutex_lock(& m);
436 }
437#line 111
438 if (dequeue_flag) {
439#line 113
440 i = 0;
441 {
442#line 113
443 while (1) {
444 while_1_continue: ;
445#line 113
446 if (i < 20) {
447
448 } else {
449 goto while_1_break;
450 }
451 {
452#line 115
453 tmp___1 = empty(& queue);
454 }
455#line 115
456 if (tmp___1 != -1) {
457 {
458#line 116
459 tmp = dequeue(& queue);
460 }
461#line 116
462 if (tmp) {
463#line 116
464 tmp___0 = 0;
465 } else {
466#line 116
467 tmp___0 = 1;
468 }
469 {
470#line 116
471 __cil_tmp6 = i * 4U;
472#line 116
473 __cil_tmp7 = (unsigned int )(stored_elements) + __cil_tmp6;
474#line 116
475 __cil_tmp8 = *((int *)__cil_tmp7);
476#line 116
477 if (tmp___0 == __cil_tmp8) {
478 goto ERROR;
479 ERROR: ;
480 } else {
481
482 }
483 }
484 } else {
485
486 }
487#line 113
488 i = i + 1;
489 }
490 while_1_break: ;
491 }
492#line 122
493 dequeue_flag = (_Bool)0;
494#line 123
495 enqueue_flag = (_Bool)1;
496 } else {
497
498 }
499 {
500#line 125
501 pthread_mutex_unlock(& m);
502 }
503#line 127
504 return ((void *)0);
505}
506}
507#line 130 "queue_ok.c"
508int main(void)
509{ pthread_t id1 ;
510 pthread_t id2 ;
511 int tmp ;
512 int tmp___0 ;
513 pthread_mutexattr_t const *__cil_tmp5 ;
514 pthread_t * __restrict __cil_tmp6 ;
515 void *__cil_tmp7 ;
516 pthread_attr_t const * __restrict __cil_tmp8 ;
517 void * __restrict __cil_tmp9 ;
518 pthread_t * __restrict __cil_tmp10 ;
519 void *__cil_tmp11 ;
520 pthread_attr_t const * __restrict __cil_tmp12 ;
521 void * __restrict __cil_tmp13 ;
522 pthread_t *__cil_tmp14 ;
523 pthread_t __cil_tmp15 ;
524 void *__cil_tmp16 ;
525 void **__cil_tmp17 ;
526 pthread_t *__cil_tmp18 ;
527 pthread_t __cil_tmp19 ;
528 void *__cil_tmp20 ;
529 void **__cil_tmp21 ;
530
531 {
532 {
533#line 134
534 enqueue_flag = (_Bool)1;
535#line 135
536 dequeue_flag = (_Bool)0;
537#line 137
538 init(& queue);
539#line 139
540 tmp = empty(& queue);
541 }
542#line 139
543 if (tmp) {
544#line 139
545 tmp___0 = 0;
546 } else {
547#line 139
548 tmp___0 = 1;
549 }
550#line 139
551 if (tmp___0 == -1) {
552 goto ERROR;
553 ERROR: ;
554 } else {
555
556 }
557 {
558#line 145
559 __cil_tmp5 = (pthread_mutexattr_t const *)0;
560#line 145
561 pthread_mutex_init(& m, __cil_tmp5);
562#line 147
563 __cil_tmp6 = (pthread_t * __restrict )(& id1);
564#line 147
565 __cil_tmp7 = (void *)0;
566#line 147
567 __cil_tmp8 = (pthread_attr_t const * __restrict )__cil_tmp7;
568#line 147
569 __cil_tmp9 = (void * __restrict )(& queue);
570#line 147
571 pthread_create(__cil_tmp6, __cil_tmp8, & t1, __cil_tmp9);
572#line 148
573 __cil_tmp10 = (pthread_t * __restrict )(& id2);
574#line 148
575 __cil_tmp11 = (void *)0;
576#line 148
577 __cil_tmp12 = (pthread_attr_t const * __restrict )__cil_tmp11;
578#line 148
579 __cil_tmp13 = (void * __restrict )(& queue);
580#line 148
581 pthread_create(__cil_tmp10, __cil_tmp12, & t2, __cil_tmp13);
582#line 150
583 __cil_tmp14 = & id1;
584#line 150
585 __cil_tmp15 = *__cil_tmp14;
586#line 150
587 __cil_tmp16 = (void *)0;
588#line 150
589 __cil_tmp17 = (void **)__cil_tmp16;
590#line 150
591 pthread_join(__cil_tmp15, __cil_tmp17);
592#line 151
593 __cil_tmp18 = & id2;
594#line 151
595 __cil_tmp19 = *__cil_tmp18;
596#line 151
597 __cil_tmp20 = (void *)0;
598#line 151
599 __cil_tmp21 = (void **)__cil_tmp20;
600#line 151
601 pthread_join(__cil_tmp19, __cil_tmp21);
602 }
603#line 153
604 return (0);
605}
606}