1
2
3
4#line 211 "/usr/lib/gcc/x86_64-pc-linux-gnu/4.5.3/include/stddef.h"
5typedef unsigned int size_t;
6#line 15 "dll_of_dll_BUG.c"
7struct slave_item {
8 struct slave_item *next ;
9 struct slave_item *prev ;
10};
11#line 31 "dll_of_dll_BUG.c"
12struct master_item {
13 struct master_item *next ;
14 struct master_item *prev ;
15 struct slave_item *slave ;
16};
17#line 471 "/usr/include/stdlib.h"
18extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
19#line 488
20extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
21#line 514
22extern __attribute__((__nothrow__, __noreturn__)) void abort(void) ;
23#line 3 "dll_of_dll_BUG.c"
24extern int __VERIFIER_nondet_int(void) ;
25#line 5 "dll_of_dll_BUG.c"
26static void fail(void)
27{
28
29 {
30 ERROR:
31 goto ERROR;
32}
33}
34#line 20 "dll_of_dll_BUG.c"
35struct slave_item *alloc_or_die_slave(void)
36{ struct slave_item *ptr ;
37 void *tmp ;
38 unsigned int __cil_tmp3 ;
39 void *__cil_tmp4 ;
40 void *__cil_tmp5 ;