Showing error 52

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/bubble_sort_linux_unsafe.i
Line in file: 898
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
 617
 618struct _IO_FILE;
 619
 620typedef struct _IO_FILE FILE;
 621
 622
 623typedef struct _IO_FILE __FILE;
 624typedef struct
 625{
 626  int __count;
 627  union
 628  {
 629    unsigned int __wch;
 630    char __wchb[4];
 631  } __value;
 632} __mbstate_t;
 633typedef struct
 634{
 635  __off_t __pos;
 636  __mbstate_t __state;
 637} _G_fpos_t;
 638typedef struct
 639{
 640  __off64_t __pos;
 641  __mbstate_t __state;
 642} _G_fpos64_t;
 643typedef int _G_int16_t __attribute__ ((__mode__ (__HI__)));
 644typedef int _G_int32_t __attribute__ ((__mode__ (__SI__)));
 645typedef unsigned int _G_uint16_t __attribute__ ((__mode__ (__HI__)));
 646typedef unsigned int _G_uint32_t __attribute__ ((__mode__ (__SI__)));
 647typedef __builtin_va_list __gnuc_va_list;
 648struct _IO_jump_t; struct _IO_FILE;
 649typedef void _IO_lock_t;
 650struct _IO_marker {
 651  struct _IO_marker *_next;
 652  struct _IO_FILE *_sbuf;
 653  int _pos;
 654};
 655enum __codecvt_result
 656{
 657  __codecvt_ok,
 658  __codecvt_partial,
 659  __codecvt_error,
 660  __codecvt_noconv
 661};
 662struct _IO_FILE {
 663  int _flags;
 664  char* _IO_read_ptr;
 665  char* _IO_read_end;
 666  char* _IO_read_base;
 667  char* _IO_write_base;
 668  char* _IO_write_ptr;
 669  char* _IO_write_end;
 670  char* _IO_buf_base;
 671  char* _IO_buf_end;
 672  char *_IO_save_base;
 673  char *_IO_backup_base;
 674  char *_IO_save_end;
 675  struct _IO_marker *_markers;
 676  struct _IO_FILE *_chain;
 677  int _fileno;
 678  int _flags2;
 679  __off_t _old_offset;
 680  unsigned short _cur_column;
 681  signed char _vtable_offset;
 682  char _shortbuf[1];
 683  _IO_lock_t *_lock;
 684  __off64_t _offset;
 685  void *__pad1;
 686  void *__pad2;
 687  void *__pad3;
 688  void *__pad4;
 689  size_t __pad5;
 690  int _mode;
 691  char _unused2[15 * sizeof (int) - 4 * sizeof (void *) - sizeof (size_t)];
 692};
 693typedef struct _IO_FILE _IO_FILE;
 694struct _IO_FILE_plus;
 695extern struct _IO_FILE_plus _IO_2_1_stdin_;
 696extern struct _IO_FILE_plus _IO_2_1_stdout_;
 697extern struct _IO_FILE_plus _IO_2_1_stderr_;
 698typedef __ssize_t __io_read_fn (void *__cookie, char *__buf, size_t __nbytes);
 699typedef __ssize_t __io_write_fn (void *__cookie, __const char *__buf,
 700     size_t __n);
 701typedef int __io_seek_fn (void *__cookie, __off64_t *__pos, int __w);
 702typedef int __io_close_fn (void *__cookie);
 703extern int __underflow (_IO_FILE *);
 704extern int __uflow (_IO_FILE *);
 705extern int __overflow (_IO_FILE *, int);
 706extern int _IO_getc (_IO_FILE *__fp);
 707extern int _IO_putc (int __c, _IO_FILE *__fp);
 708extern int _IO_feof (_IO_FILE *__fp) __attribute__ ((__nothrow__ , __leaf__));
 709extern int _IO_ferror (_IO_FILE *__fp) __attribute__ ((__nothrow__ , __leaf__));
 710extern int _IO_peekc_locked (_IO_FILE *__fp);
 711extern void _IO_flockfile (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
 712extern void _IO_funlockfile (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
 713extern int _IO_ftrylockfile (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
 714extern int _IO_vfscanf (_IO_FILE * __restrict, const char * __restrict,
 715   __gnuc_va_list, int *__restrict);
 716extern int _IO_vfprintf (_IO_FILE *__restrict, const char *__restrict,
 717    __gnuc_va_list);
 718extern __ssize_t _IO_padn (_IO_FILE *, int, __ssize_t);
 719extern size_t _IO_sgetn (_IO_FILE *, void *, size_t);
 720extern __off64_t _IO_seekoff (_IO_FILE *, __off64_t, int, int);
 721extern __off64_t _IO_seekpos (_IO_FILE *, __off64_t, int);
 722extern void _IO_free_backup_area (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
 723typedef __gnuc_va_list va_list;
 724
 725typedef _G_fpos_t fpos_t;
 726
 727extern struct _IO_FILE *stdin;
 728extern struct _IO_FILE *stdout;
 729extern struct _IO_FILE *stderr;
 730
 731extern int remove (__const char *__filename) __attribute__ ((__nothrow__ , __leaf__));
 732extern int rename (__const char *__old, __const char *__new) __attribute__ ((__nothrow__ , __leaf__));
 733
 734extern int renameat (int __oldfd, __const char *__old, int __newfd,
 735       __const char *__new) __attribute__ ((__nothrow__ , __leaf__));
 736
 737extern FILE *tmpfile (void) ;
 738extern char *tmpnam (char *__s) __attribute__ ((__nothrow__ , __leaf__)) ;
 739
 740extern char *tmpnam_r (char *__s) __attribute__ ((__nothrow__ , __leaf__)) ;
 741extern char *tempnam (__const char *__dir, __const char *__pfx)
 742     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
 743
 744extern int fclose (FILE *__stream);
 745extern int fflush (FILE *__stream);
 746
 747extern int fflush_unlocked (FILE *__stream);
 748
 749extern FILE *fopen (__const char *__restrict __filename,
 750      __const char *__restrict __modes) ;
 751extern FILE *freopen (__const char *__restrict __filename,
 752        __const char *__restrict __modes,
 753        FILE *__restrict __stream) ;
 754
 755extern FILE *fdopen (int __fd, __const char *__modes) __attribute__ ((__nothrow__ , __leaf__)) ;
 756extern FILE *fmemopen (void *__s, size_t __len, __const char *__modes)
 757  __attribute__ ((__nothrow__ , __leaf__)) ;
 758extern FILE *open_memstream (char **__bufloc, size_t *__sizeloc) __attribute__ ((__nothrow__ , __leaf__)) ;
 759
 760extern void setbuf (FILE *__restrict __stream, char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__));
 761extern int setvbuf (FILE *__restrict __stream, char *__restrict __buf,
 762      int __modes, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
 763
 764extern void setbuffer (FILE *__restrict __stream, char *__restrict __buf,
 765         size_t __size) __attribute__ ((__nothrow__ , __leaf__));
 766extern void setlinebuf (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
 767
 768extern int fprintf (FILE *__restrict __stream,
 769      __const char *__restrict __format, ...);
 770extern int printf (__const char *__restrict __format, ...);
 771extern int sprintf (char *__restrict __s,
 772      __const char *__restrict __format, ...) __attribute__ ((__nothrow__));
 773extern int vfprintf (FILE *__restrict __s, __const char *__restrict __format,
 774       __gnuc_va_list __arg);
 775extern int vprintf (__const char *__restrict __format, __gnuc_va_list __arg);
 776extern int vsprintf (char *__restrict __s, __const char *__restrict __format,
 777       __gnuc_va_list __arg) __attribute__ ((__nothrow__));
 778
 779
 780extern int snprintf (char *__restrict __s, size_t __maxlen,
 781       __const char *__restrict __format, ...)
 782     __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 4)));
 783extern int vsnprintf (char *__restrict __s, size_t __maxlen,
 784        __const char *__restrict __format, __gnuc_va_list __arg)
 785     __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 0)));
 786
 787extern int vdprintf (int __fd, __const char *__restrict __fmt,
 788       __gnuc_va_list __arg)
 789     __attribute__ ((__format__ (__printf__, 2, 0)));
 790extern int dprintf (int __fd, __const char *__restrict __fmt, ...)
 791     __attribute__ ((__format__ (__printf__, 2, 3)));
 792
 793extern int fscanf (FILE *__restrict __stream,
 794     __const char *__restrict __format, ...) ;
 795extern int scanf (__const char *__restrict __format, ...) ;
 796extern int sscanf (__const char *__restrict __s,
 797     __const char *__restrict __format, ...) __attribute__ ((__nothrow__ , __leaf__));
 798extern int fscanf (FILE *__restrict __stream, __const char *__restrict __format, ...) __asm__ ("" "__isoc99_fscanf") ;
 799extern int scanf (__const char *__restrict __format, ...) __asm__ ("" "__isoc99_scanf") ;
 800extern int sscanf (__const char *__restrict __s, __const char *__restrict __format, ...) __asm__ ("" "__isoc99_sscanf") __attribute__ ((__nothrow__ , __leaf__));
 801
 802
 803extern int vfscanf (FILE *__restrict __s, __const char *__restrict __format,
 804      __gnuc_va_list __arg)
 805     __attribute__ ((__format__ (__scanf__, 2, 0))) ;
 806extern int vscanf (__const char *__restrict __format, __gnuc_va_list __arg)
 807     __attribute__ ((__format__ (__scanf__, 1, 0))) ;
 808extern int vsscanf (__const char *__restrict __s,
 809      __const char *__restrict __format, __gnuc_va_list __arg)
 810     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__format__ (__scanf__, 2, 0)));
 811extern int vfscanf (FILE *__restrict __s, __const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vfscanf")
 812     __attribute__ ((__format__ (__scanf__, 2, 0))) ;
 813extern int vscanf (__const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vscanf")
 814     __attribute__ ((__format__ (__scanf__, 1, 0))) ;
 815extern int vsscanf (__const char *__restrict __s, __const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vsscanf") __attribute__ ((__nothrow__ , __leaf__))
 816     __attribute__ ((__format__ (__scanf__, 2, 0)));
 817
 818
 819extern int fgetc (FILE *__stream);
 820extern int getc (FILE *__stream);
 821extern int getchar (void);
 822
 823extern int getc_unlocked (FILE *__stream);
 824extern int getchar_unlocked (void);
 825extern int fgetc_unlocked (FILE *__stream);
 826
 827extern int fputc (int __c, FILE *__stream);
 828extern int putc (int __c, FILE *__stream);
 829extern int putchar (int __c);
 830
 831extern int fputc_unlocked (int __c, FILE *__stream);
 832extern int putc_unlocked (int __c, FILE *__stream);
 833extern int putchar_unlocked (int __c);
 834extern int getw (FILE *__stream);
 835extern int putw (int __w, FILE *__stream);
 836
 837extern char *fgets (char *__restrict __s, int __n, FILE *__restrict __stream)
 838     ;
 839extern char *gets (char *__s) ;
 840
 841extern __ssize_t __getdelim (char **__restrict __lineptr,
 842          size_t *__restrict __n, int __delimiter,
 843          FILE *__restrict __stream) ;
 844extern __ssize_t getdelim (char **__restrict __lineptr,
 845        size_t *__restrict __n, int __delimiter,
 846        FILE *__restrict __stream) ;
 847extern __ssize_t getline (char **__restrict __lineptr,
 848       size_t *__restrict __n,
 849       FILE *__restrict __stream) ;
 850
 851extern int fputs (__const char *__restrict __s, FILE *__restrict __stream);
 852extern int puts (__const char *__s);
 853extern int ungetc (int __c, FILE *__stream);
 854extern size_t fread (void *__restrict __ptr, size_t __size,
 855       size_t __n, FILE *__restrict __stream) ;
 856extern size_t fwrite (__const void *__restrict __ptr, size_t __size,
 857        size_t __n, FILE *__restrict __s);
 858
 859extern size_t fread_unlocked (void *__restrict __ptr, size_t __size,
 860         size_t __n, FILE *__restrict __stream) ;
 861extern size_t fwrite_unlocked (__const void *__restrict __ptr, size_t __size,
 862          size_t __n, FILE *__restrict __stream);
 863
 864extern int fseek (FILE *__stream, long int __off, int __whence);
 865extern long int ftell (FILE *__stream) ;
 866extern void rewind (FILE *__stream);
 867
 868extern int fseeko (FILE *__stream, __off_t __off, int __whence);
 869extern __off_t ftello (FILE *__stream) ;
 870
 871extern int fgetpos (FILE *__restrict __stream, fpos_t *__restrict __pos);
 872extern int fsetpos (FILE *__stream, __const fpos_t *__pos);
 873
 874
 875extern void clearerr (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
 876extern int feof (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
 877extern int ferror (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
 878
 879extern void clearerr_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
 880extern int feof_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
 881extern int ferror_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
 882
 883extern void perror (__const char *__s);
 884
 885extern int sys_nerr;
 886extern __const char *__const sys_errlist[];
 887extern int fileno (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
 888extern int fileno_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
 889extern FILE *popen (__const char *__command, __const char *__modes) ;
 890extern int pclose (FILE *__stream);
 891extern char *ctermid (char *__s) __attribute__ ((__nothrow__ , __leaf__));
 892extern void flockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
 893extern int ftrylockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
 894extern void funlockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
 895
 896extern int __VERIFIER_nondet_int(void);
 897static void fail(void) {
 898ERROR:
 899    goto ERROR;
 900}
 901struct list_head {
 902 struct list_head *next, *prev;
 903};
 904struct node {
 905    int value;
 906    struct list_head linkage;
 907    struct list_head nested;
 908};
 909struct list_head gl_list = { &(gl_list), &(gl_list) };
 910static void inspect(const struct list_head *head)
 911{
 912    do { if (!(head)) fail(); } while (0);
 913    do { if (!(head->next != head)) fail(); } while (0);
 914    do { if (!(head->prev != head)) fail(); } while (0);
 915    head = head->prev;
 916    do { if (!(head)) fail(); } while (0);
 917    do { if (!(head->next != head)) fail(); } while (0);
 918    do { if (!(head->prev != head)) fail(); } while (0);
 919    const struct node *node = ((struct node *)((char *)(head)-(unsigned long)(&((struct node *)0)->linkage)));
 920    do { if (!(node)) fail(); } while (0);
 921    do { if (!(node->nested.next == &node->nested)) fail(); } while (0);
 922    do { if (!(node->nested.prev == &node->nested)) fail(); } while (0);
 923    do { if (!(node->nested.next != &node->linkage)) fail(); } while (0);
 924    do { if (!(node->nested.prev != &node->linkage)) fail(); } while (0);
 925    do { if (!(node != (const struct node *)head)) fail(); } while (0);
 926    do { if (!(node != (const struct node *)&node->linkage)) fail(); } while (0);
 927    do { if (!(node == (const struct node *)&node->value)) fail(); } while (0);
 928    do { if (!(head == node->linkage.next->prev)) fail(); } while (0);
 929    do { if (!(head == node->linkage.prev->next)) fail(); } while (0);
 930    for (head = head->next; &node->linkage != head; head = head->next);
 931    do { if (!(((struct node *)((char *)(head)-(unsigned long)(&((struct node *)0)->linkage))) == node)) fail(); } while (0);
 932}
 933static inline void __list_add(struct list_head *new,
 934         struct list_head *prev,
 935         struct list_head *next)
 936{
 937 next->prev = new;
 938 new->next = next;
 939 new->prev = prev;
 940 prev->next = new;
 941}
 942static inline void __list_del(struct list_head *prev, struct list_head *next)
 943{
 944 next->prev = prev;
 945 prev->next = next;
 946}
 947static inline void list_add(struct list_head *new, struct list_head *head)
 948{
 949 __list_add(new, head, head->next);
 950}
 951static inline void list_move(struct list_head *list, struct list_head *head)
 952{
 953        __list_del(list->prev, list->next);
 954        list_add(list, head);
 955}
 956static void gl_insert(int value)
 957{
 958    struct node *node = malloc(sizeof *node);
 959    if (!node)
 960        abort();
 961    node->value = value;
 962    list_add(&node->linkage, &gl_list);
 963    do { (&node->nested)->next = (&node->nested); (&node->nested)->next = (&node->nested); } while (0);
 964}
 965static void gl_read()
 966{
 967    do {
 968        gl_insert(__VERIFIER_nondet_int());
 969    }
 970    while (__VERIFIER_nondet_int());
 971}
 972static void gl_destroy()
 973{
 974    struct list_head *next;
 975    while (&gl_list != (next = gl_list.next)) {
 976        gl_list.next = next->next;
 977        free(((struct node *)((char *)(next)-(unsigned long)(&((struct node *)0)->linkage))));
 978 }
 979}
 980static int val_from_node(struct list_head *head) {
 981    struct node *entry = ((struct node *)((char *)(head)-(unsigned long)(&((struct node *)0)->linkage)));
 982    return entry->value;
 983}
 984static _Bool gl_sort_pass()
 985{
 986    _Bool any_change = 0;
 987    struct list_head *pos0 = gl_list.next;
 988    struct list_head *pos1;
 989    while (&gl_list != (pos1 = pos0->next)) {
 990        const int val0 = val_from_node(pos0);
 991        const int val1 = val_from_node(pos1);
 992        if (val0 <= val1) {
 993            pos0 = pos1;
 994            continue;
 995        }
 996        any_change = 1;
 997        list_move(pos0, pos1);
 998    }
 999    return any_change;
1000}
1001static void gl_sort()
1002{
1003    while (gl_sort_pass())
1004        ;
1005}
1006int main()
1007{
1008    gl_read();
1009    inspect(&gl_list);
1010    gl_sort();
1011    inspect(&gl_list);
1012    gl_destroy();
1013    return 0;
1014}