Showing error 62

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: heap-manipulation/sll_to_dll_rev_safe.i
Line in file: 619
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

  1typedef long unsigned int size_t;
  2typedef int wchar_t;
  3
  4union wait
  5  {
  6    int w_status;
  7    struct
  8      {
  9 unsigned int __w_termsig:7;
 10 unsigned int __w_coredump:1;
 11 unsigned int __w_retcode:8;
 12 unsigned int:16;
 13      } __wait_terminated;
 14    struct
 15      {
 16 unsigned int __w_stopval:8;
 17 unsigned int __w_stopsig:8;
 18 unsigned int:16;
 19      } __wait_stopped;
 20  };
 21typedef union
 22  {
 23    union wait *__uptr;
 24    int *__iptr;
 25  } __WAIT_STATUS __attribute__ ((__transparent_union__));
 26
 27typedef struct
 28  {
 29    int quot;
 30    int rem;
 31  } div_t;
 32typedef struct
 33  {
 34    long int quot;
 35    long int rem;
 36  } ldiv_t;
 37
 38
 39__extension__ typedef struct
 40  {
 41    long long int quot;
 42    long long int rem;
 43  } lldiv_t;
 44
 45extern size_t __ctype_get_mb_cur_max (void) __attribute__ ((__nothrow__ , __leaf__)) ;
 46
 47extern double atof (__const char *__nptr)
 48     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
 49extern int atoi (__const char *__nptr)
 50     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
 51extern long int atol (__const char *__nptr)
 52     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
 53
 54
 55__extension__ extern long long int atoll (__const char *__nptr)
 56     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
 57
 58
 59extern double strtod (__const char *__restrict __nptr,
 60        char **__restrict __endptr)
 61     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
 62
 63
 64extern float strtof (__const char *__restrict __nptr,
 65       char **__restrict __endptr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
 66extern long double strtold (__const char *__restrict __nptr,
 67       char **__restrict __endptr)
 68     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
 69
 70
 71extern long int strtol (__const char *__restrict __nptr,
 72   char **__restrict __endptr, int __base)
 73     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
 74extern unsigned long int strtoul (__const char *__restrict __nptr,
 75      char **__restrict __endptr, int __base)
 76     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
 77
 78__extension__
 79extern long long int strtoq (__const char *__restrict __nptr,
 80        char **__restrict __endptr, int __base)
 81     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
 82__extension__
 83extern unsigned long long int strtouq (__const char *__restrict __nptr,
 84           char **__restrict __endptr, int __base)
 85     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
 86
 87__extension__
 88extern long long int strtoll (__const char *__restrict __nptr,
 89         char **__restrict __endptr, int __base)
 90     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
 91__extension__
 92extern unsigned long long int strtoull (__const char *__restrict __nptr,
 93     char **__restrict __endptr, int __base)
 94     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
 95
 96extern char *l64a (long int __n) __attribute__ ((__nothrow__ , __leaf__)) ;
 97extern long int a64l (__const char *__s)
 98     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
 99
100typedef unsigned char __u_char;
101typedef unsigned short int __u_short;
102typedef unsigned int __u_int;
103typedef unsigned long int __u_long;
104typedef signed char __int8_t;
105typedef unsigned char __uint8_t;
106typedef signed short int __int16_t;
107typedef unsigned short int __uint16_t;
108typedef signed int __int32_t;
109typedef unsigned int __uint32_t;
110typedef signed long int __int64_t;
111typedef unsigned long int __uint64_t;
112typedef long int __quad_t;
113typedef unsigned long int __u_quad_t;
114typedef unsigned long int __dev_t;
115typedef unsigned int __uid_t;
116typedef unsigned int __gid_t;
117typedef unsigned long int __ino_t;
118typedef unsigned long int __ino64_t;
119typedef unsigned int __mode_t;
120typedef unsigned long int __nlink_t;
121typedef long int __off_t;
122typedef long int __off64_t;
123typedef int __pid_t;
124typedef struct { int __val[2]; } __fsid_t;
125typedef long int __clock_t;
126typedef unsigned long int __rlim_t;
127typedef unsigned long int __rlim64_t;
128typedef unsigned int __id_t;
129typedef long int __time_t;
130typedef unsigned int __useconds_t;
131typedef long int __suseconds_t;
132typedef int __daddr_t;
133typedef long int __swblk_t;
134typedef int __key_t;
135typedef int __clockid_t;
136typedef void * __timer_t;
137typedef long int __blksize_t;
138typedef long int __blkcnt_t;
139typedef long int __blkcnt64_t;
140typedef unsigned long int __fsblkcnt_t;
141typedef unsigned long int __fsblkcnt64_t;
142typedef unsigned long int __fsfilcnt_t;
143typedef unsigned long int __fsfilcnt64_t;
144typedef long int __ssize_t;
145typedef __off64_t __loff_t;
146typedef __quad_t *__qaddr_t;
147typedef char *__caddr_t;
148typedef long int __intptr_t;
149typedef unsigned int __socklen_t;
150typedef __u_char u_char;
151typedef __u_short u_short;
152typedef __u_int u_int;
153typedef __u_long u_long;
154typedef __quad_t quad_t;
155typedef __u_quad_t u_quad_t;
156typedef __fsid_t fsid_t;
157typedef __loff_t loff_t;
158typedef __ino_t ino_t;
159typedef __dev_t dev_t;
160typedef __gid_t gid_t;
161typedef __mode_t mode_t;
162typedef __nlink_t nlink_t;
163typedef __uid_t uid_t;
164typedef __off_t off_t;
165typedef __pid_t pid_t;
166typedef __id_t id_t;
167typedef __ssize_t ssize_t;
168typedef __daddr_t daddr_t;
169typedef __caddr_t caddr_t;
170typedef __key_t key_t;
171
172typedef __clock_t clock_t;
173
174
175
176typedef __time_t time_t;
177
178
179typedef __clockid_t clockid_t;
180typedef __timer_t timer_t;
181typedef unsigned long int ulong;
182typedef unsigned short int ushort;
183typedef unsigned int uint;
184typedef int int8_t __attribute__ ((__mode__ (__QI__)));
185typedef int int16_t __attribute__ ((__mode__ (__HI__)));
186typedef int int32_t __attribute__ ((__mode__ (__SI__)));
187typedef int int64_t __attribute__ ((__mode__ (__DI__)));
188typedef unsigned int u_int8_t __attribute__ ((__mode__ (__QI__)));
189typedef unsigned int u_int16_t __attribute__ ((__mode__ (__HI__)));
190typedef unsigned int u_int32_t __attribute__ ((__mode__ (__SI__)));
191typedef unsigned int u_int64_t __attribute__ ((__mode__ (__DI__)));
192typedef int register_t __attribute__ ((__mode__ (__word__)));
193typedef int __sig_atomic_t;
194typedef struct
195  {
196    unsigned long int __val[(1024 / (8 * sizeof (unsigned long int)))];
197  } __sigset_t;
198typedef __sigset_t sigset_t;
199struct timespec
200  {
201    __time_t tv_sec;
202    long int tv_nsec;
203  };
204struct timeval
205  {
206    __time_t tv_sec;
207    __suseconds_t tv_usec;
208  };
209typedef __suseconds_t suseconds_t;
210typedef long int __fd_mask;
211typedef struct
212  {
213    __fd_mask __fds_bits[1024 / (8 * (int) sizeof (__fd_mask))];
214  } fd_set;
215typedef __fd_mask fd_mask;
216
217extern int select (int __nfds, fd_set *__restrict __readfds,
218     fd_set *__restrict __writefds,
219     fd_set *__restrict __exceptfds,
220     struct timeval *__restrict __timeout);
221extern int pselect (int __nfds, fd_set *__restrict __readfds,
222      fd_set *__restrict __writefds,
223      fd_set *__restrict __exceptfds,
224      const struct timespec *__restrict __timeout,
225      const __sigset_t *__restrict __sigmask);
226
227
228__extension__
229extern unsigned int gnu_dev_major (unsigned long long int __dev)
230     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
231__extension__
232extern unsigned int gnu_dev_minor (unsigned long long int __dev)
233     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
234__extension__
235extern unsigned long long int gnu_dev_makedev (unsigned int __major,
236            unsigned int __minor)
237     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
238
239typedef __blksize_t blksize_t;
240typedef __blkcnt_t blkcnt_t;
241typedef __fsblkcnt_t fsblkcnt_t;
242
243
244typedef __fsfilcnt_t fsfilcnt_t;
245typedef unsigned long int pthread_t;
246typedef union
247{
248  char __size[56];
249  long int __align;
250} pthread_attr_t;
251typedef struct __pthread_internal_list
252{
253  struct __pthread_internal_list *__prev;
254  struct __pthread_internal_list *__next;
255} __pthread_list_t;
256typedef union
257{
258  struct __pthread_mutex_s
259  {
260    int __lock;
261    unsigned int __count;
262    int __owner;
263    unsigned int __nusers;
264    int __kind;
265    int __spins;
266    __pthread_list_t __list;
267  } __data;
268  char __size[40];
269  long int __align;
270} pthread_mutex_t;
271typedef union
272{
273  char __size[4];
274  int __align;
275} pthread_mutexattr_t;
276typedef union
277{
278  struct
279  {
280    int __lock;
281    unsigned int __futex;
282    __extension__ unsigned long long int __total_seq;
283    __extension__ unsigned long long int __wakeup_seq;
284    __extension__ unsigned long long int __woken_seq;
285    void *__mutex;
286    unsigned int __nwaiters;
287    unsigned int __broadcast_seq;
288  } __data;
289  char __size[48];
290  __extension__ long long int __align;
291} pthread_cond_t;
292typedef union
293{
294  char __size[4];
295  int __align;
296} pthread_condattr_t;
297typedef unsigned int pthread_key_t;
298typedef int pthread_once_t;
299typedef union
300{
301  struct
302  {
303    int __lock;
304    unsigned int __nr_readers;
305    unsigned int __readers_wakeup;
306    unsigned int __writer_wakeup;
307    unsigned int __nr_readers_queued;
308    unsigned int __nr_writers_queued;
309    int __writer;
310    int __shared;
311    unsigned long int __pad1;
312    unsigned long int __pad2;
313    unsigned int __flags;
314  } __data;
315  char __size[56];
316  long int __align;
317} pthread_rwlock_t;
318typedef union
319{
320  char __size[8];
321  long int __align;
322} pthread_rwlockattr_t;
323typedef volatile int pthread_spinlock_t;
324typedef union
325{
326  char __size[32];
327  long int __align;
328} pthread_barrier_t;
329typedef union
330{
331  char __size[4];
332  int __align;
333} pthread_barrierattr_t;
334
335extern long int random (void) __attribute__ ((__nothrow__ , __leaf__));
336extern void srandom (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));
337extern char *initstate (unsigned int __seed, char *__statebuf,
338   size_t __statelen) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
339
340
341extern char *setstate (char *__statebuf) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
342
343
344
345
346
347
348
349struct random_data
350  {
351    int32_t *fptr;
352    int32_t *rptr;
353    int32_t *state;
354    int rand_type;
355    int rand_deg;
356    int rand_sep;
357    int32_t *end_ptr;
358  };
359
360extern int random_r (struct random_data *__restrict __buf,
361       int32_t *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
362
363extern int srandom_r (unsigned int __seed, struct random_data *__buf)
364     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
365
366extern int initstate_r (unsigned int __seed, char *__restrict __statebuf,
367   size_t __statelen,
368   struct random_data *__restrict __buf)
369     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 4)));
370
371extern int setstate_r (char *__restrict __statebuf,
372         struct random_data *__restrict __buf)
373     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
374
375
376
377
378
379
380extern int rand (void) __attribute__ ((__nothrow__ , __leaf__));
381
382extern void srand (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));
383
384
385
386
387extern int rand_r (unsigned int *__seed) __attribute__ ((__nothrow__ , __leaf__));
388
389
390
391
392
393
394
395extern double drand48 (void) __attribute__ ((__nothrow__ , __leaf__));
396extern double erand48 (unsigned short int __xsubi[3]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
397
398
399extern long int lrand48 (void) __attribute__ ((__nothrow__ , __leaf__));
400extern long int nrand48 (unsigned short int __xsubi[3])
401     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
402
403
404extern long int mrand48 (void) __attribute__ ((__nothrow__ , __leaf__));
405extern long int jrand48 (unsigned short int __xsubi[3])
406     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
407
408
409extern void srand48 (long int __seedval) __attribute__ ((__nothrow__ , __leaf__));
410extern unsigned short int *seed48 (unsigned short int __seed16v[3])
411     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
412extern void lcong48 (unsigned short int __param[7]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
413
414
415
416
417
418struct drand48_data
419  {
420    unsigned short int __x[3];
421    unsigned short int __old_x[3];
422    unsigned short int __c;
423    unsigned short int __init;
424    unsigned long long int __a;
425  };
426
427
428extern int drand48_r (struct drand48_data *__restrict __buffer,
429        double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
430extern int erand48_r (unsigned short int __xsubi[3],
431        struct drand48_data *__restrict __buffer,
432        double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
433
434
435extern int lrand48_r (struct drand48_data *__restrict __buffer,
436        long int *__restrict __result)
437     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
438extern int nrand48_r (unsigned short int __xsubi[3],
439        struct drand48_data *__restrict __buffer,
440        long int *__restrict __result)
441     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
442
443
444extern int mrand48_r (struct drand48_data *__restrict __buffer,
445        long int *__restrict __result)
446     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
447extern int jrand48_r (unsigned short int __xsubi[3],
448        struct drand48_data *__restrict __buffer,
449        long int *__restrict __result)
450     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
451
452
453extern int srand48_r (long int __seedval, struct drand48_data *__buffer)
454     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
455
456extern int seed48_r (unsigned short int __seed16v[3],
457       struct drand48_data *__buffer) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
458
459extern int lcong48_r (unsigned short int __param[7],
460        struct drand48_data *__buffer)
461     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
462
463
464
465
466
467
468
469
470
471extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
472
473extern void *calloc (size_t __nmemb, size_t __size)
474     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
475
476
477
478
479
480
481
482
483
484
485extern void *realloc (void *__ptr, size_t __size)
486     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__warn_unused_result__));
487
488extern void free (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));
489
490
491
492
493extern void cfree (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));
494
495extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__));
496
497
498
499
500
501
502
503extern void *valloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
504
505
506
507
508extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size)
509     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
510
511
512
513
514extern void abort (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
515
516
517
518extern int atexit (void (*__func) (void)) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
519
520extern int on_exit (void (*__func) (int __status, void *__arg), void *__arg)
521     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
522
523extern void exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
524
525
526extern void _Exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
527
528
529extern char *getenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
530
531extern char *__secure_getenv (__const char *__name)
532     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
533extern int putenv (char *__string) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
534extern int setenv (__const char *__name, __const char *__value, int __replace)
535     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
536extern int unsetenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
537extern int clearenv (void) __attribute__ ((__nothrow__ , __leaf__));
538extern char *mktemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
539extern int mkstemp (char *__template) __attribute__ ((__nonnull__ (1))) ;
540extern int mkstemps (char *__template, int __suffixlen) __attribute__ ((__nonnull__ (1))) ;
541extern char *mkdtemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
542
543extern int system (__const char *__command) ;
544
545extern char *realpath (__const char *__restrict __name,
546         char *__restrict __resolved) __attribute__ ((__nothrow__ , __leaf__)) ;
547typedef int (*__compar_fn_t) (__const void *, __const void *);
548
549extern void *bsearch (__const void *__key, __const void *__base,
550        size_t __nmemb, size_t __size, __compar_fn_t __compar)
551     __attribute__ ((__nonnull__ (1, 2, 5))) ;
552extern void qsort (void *__base, size_t __nmemb, size_t __size,
553     __compar_fn_t __compar) __attribute__ ((__nonnull__ (1, 4)));
554extern int abs (int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
555extern long int labs (long int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
556
557__extension__ extern long long int llabs (long long int __x)
558     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
559
560extern div_t div (int __numer, int __denom)
561     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
562extern ldiv_t ldiv (long int __numer, long int __denom)
563     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
564
565
566__extension__ extern lldiv_t lldiv (long long int __numer,
567        long long int __denom)
568     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
569
570extern char *ecvt (double __value, int __ndigit, int *__restrict __decpt,
571     int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
572extern char *fcvt (double __value, int __ndigit, int *__restrict __decpt,
573     int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
574extern char *gcvt (double __value, int __ndigit, char *__buf)
575     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;
576extern char *qecvt (long double __value, int __ndigit,
577      int *__restrict __decpt, int *__restrict __sign)
578     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
579extern char *qfcvt (long double __value, int __ndigit,
580      int *__restrict __decpt, int *__restrict __sign)
581     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
582extern char *qgcvt (long double __value, int __ndigit, char *__buf)
583     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;
584extern int ecvt_r (double __value, int __ndigit, int *__restrict __decpt,
585     int *__restrict __sign, char *__restrict __buf,
586     size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
587extern int fcvt_r (double __value, int __ndigit, int *__restrict __decpt,
588     int *__restrict __sign, char *__restrict __buf,
589     size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
590extern int qecvt_r (long double __value, int __ndigit,
591      int *__restrict __decpt, int *__restrict __sign,
592      char *__restrict __buf, size_t __len)
593     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
594extern int qfcvt_r (long double __value, int __ndigit,
595      int *__restrict __decpt, int *__restrict __sign,
596      char *__restrict __buf, size_t __len)
597     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
598
599extern int mblen (__const char *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ;
600extern int mbtowc (wchar_t *__restrict __pwc,
601     __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ;
602extern int wctomb (char *__s, wchar_t __wchar) __attribute__ ((__nothrow__ , __leaf__)) ;
603extern size_t mbstowcs (wchar_t *__restrict __pwcs,
604   __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
605extern size_t wcstombs (char *__restrict __s,
606   __const wchar_t *__restrict __pwcs, size_t __n)
607     __attribute__ ((__nothrow__ , __leaf__));
608
609extern int rpmatch (__const char *__response) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
610extern int getsubopt (char **__restrict __optionp,
611        char *__const *__restrict __tokens,
612        char **__restrict __valuep)
613     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))) ;
614extern int getloadavg (double __loadavg[], int __nelem)
615     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
616
617extern int __VERIFIER_nondet_int(void);
618static void fail(void) {
619ERROR:
620    goto ERROR;
621}
622struct node {
623    struct node *next;
624    struct node *prev;
625};
626static struct node* alloc_node(void)
627{
628    struct node *ptr = malloc(sizeof *ptr);
629    if (!ptr)
630        abort();
631    ptr->next = ((void *)0);
632    ptr->prev = ((void *)0);
633    return ptr;
634}
635static void chain_node(struct node **ppnode)
636{
637    struct node *node = alloc_node();
638    node->next = *ppnode;
639    *ppnode = node;
640}
641static struct node* create_sll(const struct node **pp1, const struct node **pp2)
642{
643    struct node *list = ((void *)0);
644    do
645        chain_node(&list);
646    while (__VERIFIER_nondet_int());
647    *pp2 = list;
648    do
649        chain_node(&list);
650    while (__VERIFIER_nondet_int());
651    *pp1 = list;
652    do
653        chain_node(&list);
654    while (__VERIFIER_nondet_int());
655    return list;
656}
657void init_back_link(struct node *list) {
658    for (;;) {
659        struct node *next = list->next;
660        if (!next)
661            return;
662        next->prev = list;
663        list = next;
664    }
665}
666void reverse_dll(struct node *list) {
667    while (list) {
668        struct node *next = list->next;
669        list->next = list->prev;
670        list->prev = next;
671        list = next;
672    }
673}
674void remove_fw_link(struct node *list) {
675    while (list) {
676        struct node *next = list->next;
677        list->next = ((void *)0);
678        list = next;
679    }
680}
681void check_seq_next(const struct node *beg, const struct node *const end) {
682    do { if (!(beg)) fail(); } while (0);
683    do { if (!(end)) fail(); } while (0);
684    for (beg = beg->next; end != beg; beg = beg->next)
685        do { if (!(beg)) fail(); } while (0);
686}
687void check_seq_prev(const struct node *beg, const struct node *const end) {
688    do { if (!(beg)) fail(); } while (0);
689    do { if (!(end)) fail(); } while (0);
690    for (beg = beg->prev; end != beg; beg = beg->prev)
691        do { if (!(beg)) fail(); } while (0);
692}
693int main()
694{
695    const struct node *p1, *p2;
696    struct node *list = create_sll(&p1, &p2);
697    do { } while (0);
698    check_seq_next(p1, p2);
699    do { if (!(!p1->prev)) fail(); } while (0);
700    do { if (!(!p2->prev)) fail(); } while (0);
701    init_back_link(list);
702    do { } while (0);
703    check_seq_next(p1, p2);
704    check_seq_prev(p2, p1);
705    reverse_dll(list);
706    do { } while (0);
707    check_seq_prev(p1, p2);
708    check_seq_next(p2, p1);
709    remove_fw_link(list);
710    do { } while (0);
711    check_seq_prev(p1, p2);
712    while (list) {
713        struct node *prev = list->prev;
714        free(list);
715        list = prev;
716    }
717    return 0;
718}