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 19 "sll_to_dll_rev.c"
7struct node {
8 struct node *next ;
9 struct node *prev ;
10};
11#line 471 "/usr/include/stdlib.h"
12extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
13#line 488
14extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
15#line 514
16extern __attribute__((__nothrow__, __noreturn__)) void abort(void) ;
17#line 3 "sll_to_dll_rev.c"
18extern int __VERIFIER_nondet_int(void) ;
19#line 5 "sll_to_dll_rev.c"
20static void fail(void)
21{
22
23 {
24 ERROR:
25 goto ERROR;
26}
27}
28#line 24 "sll_to_dll_rev.c"
29static struct node *alloc_node(void)
30{ struct node *ptr ;
31 void *tmp ;
32 unsigned int __cil_tmp3 ;
33 void *__cil_tmp4 ;
34 unsigned int __cil_tmp5 ;