1
2
3
4#line 211 "/usr/lib/x86_64-linux-gnu/gcc/x86_64-linux-gnu/4.5.2/include/stddef.h"
5typedef unsigned long size_t;
6#line 141 "/usr/include/bits/types.h"
7typedef long __off_t;
8#line 142 "/usr/include/bits/types.h"
9typedef long __off64_t;
10#line 45 "/usr/include/stdio.h"
11struct _IO_FILE;
12#line 45
13struct _IO_FILE;
14#line 49 "/usr/include/stdio.h"
15typedef struct _IO_FILE FILE;
16#line 170 "/usr/include/libio.h"
17struct _IO_FILE;
18#line 180 "/usr/include/libio.h"
19typedef void _IO_lock_t;
20#line 186 "/usr/include/libio.h"
21struct _IO_marker {
22 struct _IO_marker *_next ;
23 struct _IO_FILE *_sbuf ;
24 int _pos ;
25};
26#line 271 "/usr/include/libio.h"
27struct _IO_FILE {
28 int _flags ;
29 char *_IO_read_ptr ;
30 char *_IO_read_end ;
31 char *_IO_read_base ;
32 char *_IO_write_base ;
33 char *_IO_write_ptr ;
34 char *_IO_write_end ;
35 char *_IO_buf_base ;
36 char *_IO_buf_end ;
37 char *_IO_save_base ;
38 char *_IO_backup_base ;
39 char *_IO_save_end ;
40 struct _IO_marker *_markers ;
41 struct _IO_FILE *_chain ;
42 int _fileno ;
43 int _flags2 ;
44 __off_t _old_offset ;
45 unsigned short _cur_column ;
46 signed char _vtable_offset ;
47 char _shortbuf[1] ;
48 _IO_lock_t *_lock ;
49 __off64_t _offset ;
50 void *__pad1 ;
51 void *__pad2 ;
52 void *__pad3 ;
53 void *__pad4 ;
54 size_t __pad5 ;
55 int _mode ;
56 char _unused2[(15U * sizeof(int ) - 4U * sizeof(void *)) - sizeof(size_t )] ;
57};
58#line 50 "/usr/include/bits/pthreadtypes.h"
59typedef unsigned long pthread_t;
60#line 53 "/usr/include/bits/pthreadtypes.h"
61union __anonunion_pthread_attr_t_14 {
62 char __size[56] ;
63 long __align ;
64};
65#line 53 "/usr/include/bits/pthreadtypes.h"
66typedef union __anonunion_pthread_attr_t_14 pthread_attr_t;
67#line 61 "/usr/include/bits/pthreadtypes.h"
68struct __pthread_internal_list {
69 struct __pthread_internal_list *__prev ;
70 struct __pthread_internal_list *__next ;
71};
72#line 61 "/usr/include/bits/pthreadtypes.h"
73typedef struct __pthread_internal_list __pthread_list_t;
74#line 76 "/usr/include/bits/pthreadtypes.h"
75struct __pthread_mutex_s {
76 int __lock ;
77 unsigned int __count ;
78 int __owner ;
79 unsigned int __nusers ;
80 int __kind ;
81 int __spins ;
82 __pthread_list_t __list ;
83};
84#line 76 "/usr/include/bits/pthreadtypes.h"
85union __anonunion_pthread_mutex_t_15 {
86 struct __pthread_mutex_s __data ;
87 char __size[40] ;
88 long __align ;
89};
90#line 76 "/usr/include/bits/pthreadtypes.h"
91typedef union __anonunion_pthread_mutex_t_15 pthread_mutex_t;
92#line 106 "/usr/include/bits/pthreadtypes.h"
93union __anonunion_pthread_mutexattr_t_16 {
94 char __size[4] ;
95 int __align ;
96};
97#line 106 "/usr/include/bits/pthreadtypes.h"
98typedef union __anonunion_pthread_mutexattr_t_16 pthread_mutexattr_t;
99#line 1 "<compiler builtins>"
100void *__builtin_alloca(unsigned int ) ;
101#line 167 "/usr/include/stdio.h"
102extern struct _IO_FILE *stderr ;
103#line 353
104extern int fprintf(FILE * __restrict __stream , char const * __restrict __format
105 , ...) ;
106#line 435
107extern __attribute__((__nothrow__)) int sscanf(char const * __restrict __s , char const * __restrict __format
108 , ...) __asm__("__isoc99_sscanf") ;
109#line 471 "/usr/include/stdlib.h"
110extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
111#line 544
112extern __attribute__((__nothrow__, __noreturn__)) void exit(int __status ) ;
113#line 225 "/usr/include/pthread.h"
114extern __attribute__((__nothrow__)) int pthread_create(pthread_t * __restrict __newthread ,
115 pthread_attr_t const * __restrict __attr ,
116 void *(*__start_routine)(void * ) ,
117 void * __restrict __arg ) __attribute__((__nonnull__(1,3))) ;
118#line 242
119extern int pthread_join(pthread_t __th , void **__thread_return ) ;
120#line 733
121extern __attribute__((__nothrow__)) int pthread_mutex_init(pthread_mutex_t *__mutex ,
122 pthread_mutexattr_t const *__mutexattr ) __attribute__((__nonnull__(1))) ;
123#line 746
124extern __attribute__((__nothrow__)) int pthread_mutex_lock(pthread_mutex_t *__mutex ) __attribute__((__nonnull__(1))) ;
125#line 757
126extern __attribute__((__nothrow__)) int pthread_mutex_unlock(pthread_mutex_t *__mutex ) __attribute__((__nonnull__(1))) ;
127#line 8 "twostage_3_bad.c"
128static int iTThreads = 2;
129#line 9 "twostage_3_bad.c"
130static int iRThreads = 1;
131#line 10 "twostage_3_bad.c"
132static int data1Value = 0;
133#line 11 "twostage_3_bad.c"
134static int data2Value = 0;
135#line 12 "twostage_3_bad.c"
136pthread_mutex_t *data1Lock ;
137#line 13 "twostage_3_bad.c"
138pthread_mutex_t *data2Lock ;
139#line 15
140void lock(pthread_mutex_t *lock___0 ) ;
141#line 16
142void unlock(pthread_mutex_t *lock___0 ) ;
143#line 18 "twostage_3_bad.c"
144void *funcA(void *param )
145{
146
147 {
148 {
149#line 19
150 pthread_mutex_lock(data1Lock);
151#line 20
152 data1Value = 1;
153#line 21
154 pthread_mutex_unlock(data1Lock);
155#line 23
156 pthread_mutex_lock(data2Lock);
157#line 24
158 data2Value = data1Value + 1;
159#line 25
160 pthread_mutex_unlock(data2Lock);
161 }
162#line 27
163 return ((void *)0);
164}
165}
166#line 30 "twostage_3_bad.c"
167void *funcB(void *param )
168{ int t1 ;
169 int t2 ;
170 int __cil_tmp4 ;
171 FILE * __restrict __cil_tmp5 ;
172 char const * __restrict __cil_tmp6 ;
173
174 {
175 {
176#line 31
177 t1 = -1;
178#line 32
179 t2 = -1;
180#line 34
181 pthread_mutex_lock(data1Lock);
182 }
183#line 35
184 if (data1Value == 0) {
185 {
186#line 36
187 pthread_mutex_unlock(data1Lock);
188 }
189#line 37
190 return ((void *)0);
191 } else {
192
193 }
194 {
195#line 39
196 t1 = data1Value;
197#line 40
198 pthread_mutex_unlock(data1Lock);
199#line 42
200 pthread_mutex_lock(data2Lock);
201#line 43
202 t2 = data2Value;
203#line 44
204 pthread_mutex_unlock(data2Lock);
205 }
206 {
207#line 46
208 __cil_tmp4 = t1 + 1;
209#line 46
210 if (t2 != __cil_tmp4) {
211 {
212#line 47
213 __cil_tmp5 = (FILE * __restrict )stderr;
214#line 47
215 __cil_tmp6 = (char const * __restrict )"Bug found!\n";
216#line 47
217 fprintf(__cil_tmp5, __cil_tmp6);
218 ERROR: goto ERROR;
219 }
220
221 } else {
222
223 }
224 }
225#line 52
226 return ((void *)0);
227}
228}
229#line 55 "twostage_3_bad.c"
230int main(int argc , char **argv )
231{ int i ;
232 int err ;
233 void *tmp ;
234 void *tmp___0 ;
235 pthread_t *tPool ;
236 unsigned int __lengthoftPool ;
237 void *tmp___1 ;
238 pthread_t *rPool ;
239 unsigned int __lengthofrPool ;
240 void *tmp___2 ;
241 FILE * __restrict __cil_tmp13 ;
242 char const * __restrict __cil_tmp14 ;
243 char **__cil_tmp15 ;
244 char *__cil_tmp16 ;
245 char const * __restrict __cil_tmp17 ;
246 char const * __restrict __cil_tmp18 ;
247 char **__cil_tmp19 ;
248 char *__cil_tmp20 ;
249 char const * __restrict __cil_tmp21 ;
250 char const * __restrict __cil_tmp22 ;
251 unsigned long __cil_tmp23 ;
252 unsigned long __cil_tmp24 ;
253 void *__cil_tmp25 ;
254 pthread_mutexattr_t const *__cil_tmp26 ;
255 FILE * __restrict __cil_tmp27 ;
256 char const * __restrict __cil_tmp28 ;
257 void *__cil_tmp29 ;
258 pthread_mutexattr_t const *__cil_tmp30 ;
259 FILE * __restrict __cil_tmp31 ;
260 char const * __restrict __cil_tmp32 ;
261 int *__cil_tmp33 ;
262 int __cil_tmp34 ;
263 unsigned int __cil_tmp35 ;
264 int *__cil_tmp36 ;
265 int __cil_tmp37 ;
266 unsigned int __cil_tmp38 ;
267 int *__cil_tmp39 ;
268 int __cil_tmp40 ;
269 pthread_t *__cil_tmp41 ;
270 pthread_t * __restrict __cil_tmp42 ;
271 void *__cil_tmp43 ;
272 pthread_attr_t const * __restrict __cil_tmp44 ;
273 void *__cil_tmp45 ;
274 void * __restrict __cil_tmp46 ;
275 FILE * __restrict __cil_tmp47 ;
276 char const * __restrict __cil_tmp48 ;
277 int *__cil_tmp49 ;
278 int __cil_tmp50 ;
279 pthread_t *__cil_tmp51 ;
280 pthread_t * __restrict __cil_tmp52 ;
281 void *__cil_tmp53 ;
282 pthread_attr_t const * __restrict __cil_tmp54 ;
283 void *__cil_tmp55 ;
284 void * __restrict __cil_tmp56 ;
285 FILE * __restrict __cil_tmp57 ;
286 char const * __restrict __cil_tmp58 ;
287 int *__cil_tmp59 ;
288 int __cil_tmp60 ;
289 pthread_t *__cil_tmp61 ;
290 pthread_t __cil_tmp62 ;
291 void *__cil_tmp63 ;
292 void **__cil_tmp64 ;
293 FILE * __restrict __cil_tmp65 ;
294 char const * __restrict __cil_tmp66 ;
295 int *__cil_tmp67 ;
296 int __cil_tmp68 ;
297 pthread_t *__cil_tmp69 ;
298 pthread_t __cil_tmp70 ;
299 void *__cil_tmp71 ;
300 void **__cil_tmp72 ;
301 FILE * __restrict __cil_tmp73 ;
302 char const * __restrict __cil_tmp74 ;
303
304 {
305#line 58
306 if (argc != 1) {
307#line 59
308 if (argc != 3) {
309 {
310#line 60
311 __cil_tmp13 = (FILE * __restrict )stderr;
312#line 60
313 __cil_tmp14 = (char const * __restrict )"./twostage <param1> <param2>\n";
314#line 60
315 fprintf(__cil_tmp13, __cil_tmp14);
316#line 61
317 exit(-1);
318 }
319 } else {
320 {
321#line 63
322 __cil_tmp15 = argv + 1;
323#line 63
324 __cil_tmp16 = *__cil_tmp15;
325#line 63
326 __cil_tmp17 = (char const * __restrict )__cil_tmp16;
327#line 63
328 __cil_tmp18 = (char const * __restrict )"%d";
329#line 63
330 sscanf(__cil_tmp17, __cil_tmp18, & iTThreads);
331#line 64
332 __cil_tmp19 = argv + 2;
333#line 64
334 __cil_tmp20 = *__cil_tmp19;
335#line 64
336 __cil_tmp21 = (char const * __restrict )__cil_tmp20;
337#line 64
338 __cil_tmp22 = (char const * __restrict )"%d";
339#line 64
340 sscanf(__cil_tmp21, __cil_tmp22, & iRThreads);
341 }
342 }
343 } else {
344
345 }
346 {
347#line 68
348 __cil_tmp23 = (unsigned long )40U;
349#line 68
350 tmp = malloc(__cil_tmp23);
351#line 68
352 data1Lock = (pthread_mutex_t *)tmp;
353#line 69
354 __cil_tmp24 = (unsigned long )40U;
355#line 69
356 tmp___0 = malloc(__cil_tmp24);
357#line 69
358 data2Lock = (pthread_mutex_t *)tmp___0;
359#line 70
360 __cil_tmp25 = (void *)0;
361#line 70
362 __cil_tmp26 = (pthread_mutexattr_t const *)__cil_tmp25;
363#line 70
364 err = pthread_mutex_init(data1Lock, __cil_tmp26);
365 }
366#line 70
367 if (0 != err) {
368 {
369#line 71
370 __cil_tmp27 = (FILE * __restrict )stderr;
371#line 71
372 __cil_tmp28 = (char const * __restrict )"pthread_mutex_init error: %d\n";
373#line 71
374 fprintf(__cil_tmp27, __cil_tmp28, err);
375#line 72
376 exit(-1);
377 }
378 } else {
379
380 }
381 {
382#line 74
383 __cil_tmp29 = (void *)0;
384#line 74
385 __cil_tmp30 = (pthread_mutexattr_t const *)__cil_tmp29;
386#line 74
387 err = pthread_mutex_init(data2Lock, __cil_tmp30);
388 }
389#line 74
390 if (0 != err) {
391 {
392#line 75
393 __cil_tmp31 = (FILE * __restrict )stderr;
394#line 75
395 __cil_tmp32 = (char const * __restrict )"pthread_mutex_init error: %d\n";
396#line 75
397 fprintf(__cil_tmp31, __cil_tmp32, err);
398#line 76
399 exit(-1);
400 }
401 } else {
402
403 }
404 {
405#line 79
406 __cil_tmp33 = & iTThreads;
407#line 79
408 __cil_tmp34 = *__cil_tmp33;
409#line 79
410 __lengthoftPool = (unsigned int )__cil_tmp34;
411#line 79
412 __cil_tmp35 = 4U * __lengthoftPool;
413#line 79
414 tmp___1 = __builtin_alloca(__cil_tmp35);
415#line 79
416 tPool = (pthread_t *)tmp___1;
417#line 80
418 __cil_tmp36 = & iRThreads;
419#line 80
420 __cil_tmp37 = *__cil_tmp36;
421#line 80
422 __lengthofrPool = (unsigned int )__cil_tmp37;
423#line 80
424 __cil_tmp38 = 4U * __lengthofrPool;
425#line 80
426 tmp___2 = __builtin_alloca(__cil_tmp38);
427#line 80
428 rPool = (pthread_t *)tmp___2;
429#line 82
430 i = 0;
431 }
432 {
433#line 82
434 while (1) {
435 while_0_continue: ;
436 {
437#line 82
438 __cil_tmp39 = & iTThreads;
439#line 82
440 __cil_tmp40 = *__cil_tmp39;
441#line 82
442 if (i < __cil_tmp40) {
443
444 } else {
445 goto while_0_break;
446 }
447 }
448 {
449#line 83
450 __cil_tmp41 = tPool + i;
451#line 83
452 __cil_tmp42 = (pthread_t * __restrict )__cil_tmp41;
453#line 83
454 __cil_tmp43 = (void *)0;
455#line 83
456 __cil_tmp44 = (pthread_attr_t const * __restrict )__cil_tmp43;
457#line 83
458 __cil_tmp45 = (void *)0;
459#line 83
460 __cil_tmp46 = (void * __restrict )__cil_tmp45;
461#line 83
462 err = pthread_create(__cil_tmp42, __cil_tmp44, & funcA, __cil_tmp46);
463 }
464#line 83
465 if (0 != err) {
466 {
467#line 84
468 __cil_tmp47 = (FILE * __restrict )stderr;
469#line 84
470 __cil_tmp48 = (char const * __restrict )"Error [%d] found creating 2stage thread.\n";
471#line 84
472 fprintf(__cil_tmp47, __cil_tmp48, err);
473#line 85
474 exit(-1);
475 }
476 } else {
477
478 }
479#line 82
480 i = i + 1;
481 }
482 while_0_break: ;
483 }
484#line 89
485 i = 0;
486 {
487#line 89
488 while (1) {
489 while_1_continue: ;
490 {
491#line 89
492 __cil_tmp49 = & iRThreads;
493#line 89
494 __cil_tmp50 = *__cil_tmp49;
495#line 89
496 if (i < __cil_tmp50) {
497
498 } else {
499 goto while_1_break;
500 }
501 }
502 {
503#line 90
504 __cil_tmp51 = rPool + i;
505#line 90
506 __cil_tmp52 = (pthread_t * __restrict )__cil_tmp51;
507#line 90
508 __cil_tmp53 = (void *)0;
509#line 90
510 __cil_tmp54 = (pthread_attr_t const * __restrict )__cil_tmp53;
511#line 90
512 __cil_tmp55 = (void *)0;
513#line 90
514 __cil_tmp56 = (void * __restrict )__cil_tmp55;
515#line 90
516 err = pthread_create(__cil_tmp52, __cil_tmp54, & funcB, __cil_tmp56);
517 }
518#line 90
519 if (0 != err) {
520 {
521#line 91
522 __cil_tmp57 = (FILE * __restrict )stderr;
523#line 91
524 __cil_tmp58 = (char const * __restrict )"Error [%d] found creating read thread.\n";
525#line 91
526 fprintf(__cil_tmp57, __cil_tmp58, err);
527#line 92
528 exit(-1);
529 }
530 } else {
531
532 }
533#line 89
534 i = i + 1;
535 }
536 while_1_break: ;
537 }
538#line 96
539 i = 0;
540 {
541#line 96
542 while (1) {
543 while_2_continue: ;
544 {
545#line 96
546 __cil_tmp59 = & iTThreads;
547#line 96
548 __cil_tmp60 = *__cil_tmp59;
549#line 96
550 if (i < __cil_tmp60) {
551
552 } else {
553 goto while_2_break;
554 }
555 }
556 {
557#line 97
558 __cil_tmp61 = tPool + i;
559#line 97
560 __cil_tmp62 = *__cil_tmp61;
561#line 97
562 __cil_tmp63 = (void *)0;
563#line 97
564 __cil_tmp64 = (void **)__cil_tmp63;
565#line 97
566 err = pthread_join(__cil_tmp62, __cil_tmp64);
567 }
568#line 97
569 if (0 != err) {
570 {
571#line 98
572 __cil_tmp65 = (FILE * __restrict )stderr;
573#line 98
574 __cil_tmp66 = (char const * __restrict )"pthread join error: %d\n";
575#line 98
576 fprintf(__cil_tmp65, __cil_tmp66, err);
577#line 99
578 exit(-1);
579 }
580 } else {
581
582 }
583#line 96
584 i = i + 1;
585 }
586 while_2_break: ;
587 }
588#line 103
589 i = 0;
590 {
591#line 103
592 while (1) {
593 while_3_continue: ;
594 {
595#line 103
596 __cil_tmp67 = & iRThreads;
597#line 103
598 __cil_tmp68 = *__cil_tmp67;
599#line 103
600 if (i < __cil_tmp68) {
601
602 } else {
603 goto while_3_break;
604 }
605 }
606 {
607#line 104
608 __cil_tmp69 = rPool + i;
609#line 104
610 __cil_tmp70 = *__cil_tmp69;
611#line 104
612 __cil_tmp71 = (void *)0;
613#line 104
614 __cil_tmp72 = (void **)__cil_tmp71;
615#line 104
616 err = pthread_join(__cil_tmp70, __cil_tmp72);
617 }
618#line 104
619 if (0 != err) {
620 {
621#line 105
622 __cil_tmp73 = (FILE * __restrict )stderr;
623#line 105
624 __cil_tmp74 = (char const * __restrict )"pthread join error: %d\n";
625#line 105
626 fprintf(__cil_tmp73, __cil_tmp74, err);
627#line 106
628 exit(-1);
629 }
630 } else {
631
632 }
633#line 103
634 i = i + 1;
635 }
636 while_3_break: ;
637 }
638#line 110
639 return (0);
640}
641}
642#line 113 "twostage_3_bad.c"
643void lock(pthread_mutex_t *lock___0 )
644{ int err ;
645 FILE * __restrict __cil_tmp3 ;
646 char const * __restrict __cil_tmp4 ;
647
648 {
649 {
650#line 115
651 err = pthread_mutex_lock(lock___0);
652 }
653#line 115
654 if (0 != err) {
655 {
656#line 116
657 __cil_tmp3 = (FILE * __restrict )stderr;
658#line 116
659 __cil_tmp4 = (char const * __restrict )"Got error %d from pthread_mutex_lock.\n";
660#line 116
661 fprintf(__cil_tmp3, __cil_tmp4, err);
662#line 117
663 exit(-1);
664 }
665 } else {
666
667 }
668#line 119
669 return;
670}
671}
672#line 121 "twostage_3_bad.c"
673void unlock(pthread_mutex_t *lock___0 )
674{ int err ;
675 FILE * __restrict __cil_tmp3 ;
676 char const * __restrict __cil_tmp4 ;
677
678 {
679 {
680#line 123
681 err = pthread_mutex_unlock(lock___0);
682 }
683#line 123
684 if (0 != err) {
685 {
686#line 124
687 __cil_tmp3 = (FILE * __restrict )stderr;
688#line 124
689 __cil_tmp4 = (char const * __restrict )"Got error %d from pthread_mutex_unlock.\n";
690#line 124
691 fprintf(__cil_tmp3, __cil_tmp4, err);
692#line 125
693 exit(-1);
694 }
695 } else {
696
697 }
698#line 127
699 return;
700}
701}