1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7
8typedef long unsigned int size_t;
9typedef unsigned char __u_char;
10typedef unsigned short int __u_short;
11typedef unsigned int __u_int;
12typedef unsigned long int __u_long;
13typedef signed char __int8_t;
14typedef unsigned char __uint8_t;
15typedef signed short int __int16_t;
16typedef unsigned short int __uint16_t;
17typedef signed int __int32_t;
18typedef unsigned int __uint32_t;
19typedef signed long int __int64_t;
20typedef unsigned long int __uint64_t;
21typedef long int __quad_t;
22typedef unsigned long int __u_quad_t;
23typedef unsigned long int __dev_t;
24typedef unsigned int __uid_t;
25typedef unsigned int __gid_t;
26typedef unsigned long int __ino_t;
27typedef unsigned long int __ino64_t;
28typedef unsigned int __mode_t;
29typedef unsigned long int __nlink_t;
30typedef long int __off_t;
31typedef long int __off64_t;
32typedef int __pid_t;
33typedef struct { int __val[2]; } __fsid_t;
34typedef long int __clock_t;
35typedef unsigned long int __rlim_t;
36typedef unsigned long int __rlim64_t;
37typedef unsigned int __id_t;
38typedef long int __time_t;
39typedef unsigned int __useconds_t;
40typedef long int __suseconds_t;
41typedef int __daddr_t;
42typedef long int __swblk_t;
43typedef int __key_t;
44typedef int __clockid_t;
45typedef void * __timer_t;
46typedef long int __blksize_t;
47typedef long int __blkcnt_t;
48typedef long int __blkcnt64_t;
49typedef unsigned long int __fsblkcnt_t;
50typedef unsigned long int __fsblkcnt64_t;
51typedef unsigned long int __fsfilcnt_t;
52typedef unsigned long int __fsfilcnt64_t;
53typedef long int __ssize_t;
54typedef __off64_t __loff_t;
55typedef __quad_t *__qaddr_t;
56typedef char *__caddr_t;
57typedef long int __intptr_t;
58typedef unsigned int __socklen_t;
59struct _IO_FILE;
60
61typedef struct _IO_FILE FILE;
62
63
64
65typedef struct _IO_FILE __FILE;
66typedef struct
67{
68 int __count;
69 union
70 {
71 unsigned int __wch;
72 char __wchb[4];
73 } __value;
74} __mbstate_t;
75typedef struct
76{
77 __off_t __pos;
78 __mbstate_t __state;
79} _G_fpos_t;
80typedef struct
81{
82 __off64_t __pos;
83 __mbstate_t __state;
84} _G_fpos64_t;
85typedef int _G_int16_t __attribute__ ((__mode__ (__HI__)));
86typedef int _G_int32_t __attribute__ ((__mode__ (__SI__)));
87typedef unsigned int _G_uint16_t __attribute__ ((__mode__ (__HI__)));
88typedef unsigned int _G_uint32_t __attribute__ ((__mode__ (__SI__)));
89typedef __builtin_va_list __gnuc_va_list;
90struct _IO_jump_t; struct _IO_FILE;
91typedef void _IO_lock_t;
92struct _IO_marker {
93 struct _IO_marker *_next;
94 struct _IO_FILE *_sbuf;
95 int _pos;
96};
97enum __codecvt_result
98{
99 __codecvt_ok,
100 __codecvt_partial,
101 __codecvt_error,
102 __codecvt_noconv
103};
104struct _IO_FILE {
105 int _flags;
106 char* _IO_read_ptr;
107 char* _IO_read_end;
108 char* _IO_read_base;
109 char* _IO_write_base;
110 char* _IO_write_ptr;
111 char* _IO_write_end;
112 char* _IO_buf_base;
113 char* _IO_buf_end;
114 char *_IO_save_base;
115 char *_IO_backup_base;
116 char *_IO_save_end;
117 struct _IO_marker *_markers;
118 struct _IO_FILE *_chain;
119 int _fileno;
120 int _flags2;
121 __off_t _old_offset;
122 unsigned short _cur_column;
123 signed char _vtable_offset;
124 char _shortbuf[1];
125 _IO_lock_t *_lock;
126 __off64_t _offset;
127 void *__pad1;
128 void *__pad2;
129 void *__pad3;
130 void *__pad4;
131 size_t __pad5;
132 int _mode;
133 char _unused2[15 * sizeof (int) - 4 * sizeof (void *) - sizeof (size_t)];
134};
135typedef struct _IO_FILE _IO_FILE;
136struct _IO_FILE_plus;
137extern struct _IO_FILE_plus _IO_2_1_stdin_;
138extern struct _IO_FILE_plus _IO_2_1_stdout_;
139extern struct _IO_FILE_plus _IO_2_1_stderr_;
140typedef __ssize_t __io_read_fn (void *__cookie, char *__buf, size_t __nbytes);
141typedef __ssize_t __io_write_fn (void *__cookie, __const char *__buf,
142 size_t __n);
143typedef int __io_seek_fn (void *__cookie, __off64_t *__pos, int __w);
144typedef int __io_close_fn (void *__cookie);
145extern int __underflow (_IO_FILE *);
146extern int __uflow (_IO_FILE *);
147extern int __overflow (_IO_FILE *, int);
148extern int _IO_getc (_IO_FILE *__fp);
149extern int _IO_putc (int __c, _IO_FILE *__fp);
150extern int _IO_feof (_IO_FILE *__fp) __attribute__ ((__nothrow__ , __leaf__));
151extern int _IO_ferror (_IO_FILE *__fp) __attribute__ ((__nothrow__ , __leaf__));
152extern int _IO_peekc_locked (_IO_FILE *__fp);
153extern void _IO_flockfile (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
154extern void _IO_funlockfile (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
155extern int _IO_ftrylockfile (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
156extern int _IO_vfscanf (_IO_FILE * __restrict, const char * __restrict,
157 __gnuc_va_list, int *__restrict);
158extern int _IO_vfprintf (_IO_FILE *__restrict, const char *__restrict,
159 __gnuc_va_list);
160extern __ssize_t _IO_padn (_IO_FILE *, int, __ssize_t);
161extern size_t _IO_sgetn (_IO_FILE *, void *, size_t);
162extern __off64_t _IO_seekoff (_IO_FILE *, __off64_t, int, int);
163extern __off64_t _IO_seekpos (_IO_FILE *, __off64_t, int);
164extern void _IO_free_backup_area (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
165typedef __gnuc_va_list va_list;
166typedef __off_t off_t;
167typedef __ssize_t ssize_t;
168
169typedef _G_fpos_t fpos_t;
170
171extern struct _IO_FILE *stdin;
172extern struct _IO_FILE *stdout;
173extern struct _IO_FILE *stderr;
174
175
176
177
178
179extern int remove (__const char *__filename) __attribute__ ((__nothrow__ , __leaf__));
180
181extern int rename (__const char *__old, __const char *__new) __attribute__ ((__nothrow__ , __leaf__));
182
183
184
185
186extern int renameat (int __oldfd, __const char *__old, int __newfd,
187 __const char *__new) __attribute__ ((__nothrow__ , __leaf__));
188
189
190
191
192
193
194
195
196extern FILE *tmpfile (void) ;
197extern char *tmpnam (char *__s) __attribute__ ((__nothrow__ , __leaf__)) ;
198
199extern char *tmpnam_r (char *__s) __attribute__ ((__nothrow__ , __leaf__)) ;
200extern char *tempnam (__const char *__dir, __const char *__pfx)
201 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
202
203extern int fclose (FILE *__stream);
204extern int fflush (FILE *__stream);
205
206extern int fflush_unlocked (FILE *__stream);
207
208extern FILE *fopen (__const char *__restrict __filename,
209 __const char *__restrict __modes) ;
210extern FILE *freopen (__const char *__restrict __filename,
211 __const char *__restrict __modes,
212 FILE *__restrict __stream) ;
213
214extern FILE *fdopen (int __fd, __const char *__modes) __attribute__ ((__nothrow__ , __leaf__)) ;
215extern FILE *fmemopen (void *__s, size_t __len, __const char *__modes)
216 __attribute__ ((__nothrow__ , __leaf__)) ;
217extern FILE *open_memstream (char **__bufloc, size_t *__sizeloc) __attribute__ ((__nothrow__ , __leaf__)) ;
218
219extern void setbuf (FILE *__restrict __stream, char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__));
220extern int setvbuf (FILE *__restrict __stream, char *__restrict __buf,
221 int __modes, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
222
223extern void setbuffer (FILE *__restrict __stream, char *__restrict __buf,
224 size_t __size) __attribute__ ((__nothrow__ , __leaf__));
225extern void setlinebuf (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
226
227extern int fprintf (FILE *__restrict __stream,
228 __const char *__restrict __format, ...);
229extern int printf (__const char *__restrict __format, ...);
230extern int sprintf (char *__restrict __s,
231 __const char *__restrict __format, ...) __attribute__ ((__nothrow__));
232extern int vfprintf (FILE *__restrict __s, __const char *__restrict __format,
233 __gnuc_va_list __arg);
234extern int vprintf (__const char *__restrict __format, __gnuc_va_list __arg);
235extern int vsprintf (char *__restrict __s, __const char *__restrict __format,
236 __gnuc_va_list __arg) __attribute__ ((__nothrow__));
237
238
239extern int snprintf (char *__restrict __s, size_t __maxlen,
240 __const char *__restrict __format, ...)
241 __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 4)));
242extern int vsnprintf (char *__restrict __s, size_t __maxlen,
243 __const char *__restrict __format, __gnuc_va_list __arg)
244 __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 0)));
245
246extern int vdprintf (int __fd, __const char *__restrict __fmt,
247 __gnuc_va_list __arg)
248 __attribute__ ((__format__ (__printf__, 2, 0)));
249extern int dprintf (int __fd, __const char *__restrict __fmt, ...)
250 __attribute__ ((__format__ (__printf__, 2, 3)));
251
252extern int fscanf (FILE *__restrict __stream,
253 __const char *__restrict __format, ...) ;
254extern int scanf (__const char *__restrict __format, ...) ;
255extern int sscanf (__const char *__restrict __s,
256 __const char *__restrict __format, ...) __attribute__ ((__nothrow__ , __leaf__));
257extern int fscanf (FILE *__restrict __stream, __const char *__restrict __format, ...) __asm__ ("" "__isoc99_fscanf") ;
258extern int scanf (__const char *__restrict __format, ...) __asm__ ("" "__isoc99_scanf") ;
259extern int sscanf (__const char *__restrict __s, __const char *__restrict __format, ...) __asm__ ("" "__isoc99_sscanf") __attribute__ ((__nothrow__ , __leaf__));
260
261
262extern int vfscanf (FILE *__restrict __s, __const char *__restrict __format,
263 __gnuc_va_list __arg)
264 __attribute__ ((__format__ (__scanf__, 2, 0))) ;
265extern int vscanf (__const char *__restrict __format, __gnuc_va_list __arg)
266 __attribute__ ((__format__ (__scanf__, 1, 0))) ;
267extern int vsscanf (__const char *__restrict __s,
268 __const char *__restrict __format, __gnuc_va_list __arg)
269 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__format__ (__scanf__, 2, 0)));
270extern int vfscanf (FILE *__restrict __s, __const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vfscanf")
271 __attribute__ ((__format__ (__scanf__, 2, 0))) ;
272extern int vscanf (__const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vscanf")
273 __attribute__ ((__format__ (__scanf__, 1, 0))) ;
274extern int vsscanf (__const char *__restrict __s, __const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vsscanf") __attribute__ ((__nothrow__ , __leaf__))
275 __attribute__ ((__format__ (__scanf__, 2, 0)));
276
277
278extern int fgetc (FILE *__stream);
279extern int getc (FILE *__stream);
280extern int getchar (void);
281
282extern int getc_unlocked (FILE *__stream);
283extern int getchar_unlocked (void);
284extern int fgetc_unlocked (FILE *__stream);
285
286extern int fputc (int __c, FILE *__stream);
287extern int putc (int __c, FILE *__stream);
288extern int putchar (int __c);
289
290extern int fputc_unlocked (int __c, FILE *__stream);
291extern int putc_unlocked (int __c, FILE *__stream);
292extern int putchar_unlocked (int __c);
293extern int getw (FILE *__stream);
294extern int putw (int __w, FILE *__stream);
295
296extern char *fgets (char *__restrict __s, int __n, FILE *__restrict __stream)
297 ;
298extern char *gets (char *__s) ;
299
300extern __ssize_t __getdelim (char **__restrict __lineptr,
301 size_t *__restrict __n, int __delimiter,
302 FILE *__restrict __stream) ;
303extern __ssize_t getdelim (char **__restrict __lineptr,
304 size_t *__restrict __n, int __delimiter,
305 FILE *__restrict __stream) ;
306extern __ssize_t getline (char **__restrict __lineptr,
307 size_t *__restrict __n,
308 FILE *__restrict __stream) ;
309
310extern int fputs (__const char *__restrict __s, FILE *__restrict __stream);
311extern int puts (__const char *__s);
312extern int ungetc (int __c, FILE *__stream);
313extern size_t fread (void *__restrict __ptr, size_t __size,
314 size_t __n, FILE *__restrict __stream) ;
315extern size_t fwrite (__const void *__restrict __ptr, size_t __size,
316 size_t __n, FILE *__restrict __s);
317
318extern size_t fread_unlocked (void *__restrict __ptr, size_t __size,
319 size_t __n, FILE *__restrict __stream) ;
320extern size_t fwrite_unlocked (__const void *__restrict __ptr, size_t __size,
321 size_t __n, FILE *__restrict __stream);
322
323extern int fseek (FILE *__stream, long int __off, int __whence);
324extern long int ftell (FILE *__stream) ;
325extern void rewind (FILE *__stream);
326
327extern int fseeko (FILE *__stream, __off_t __off, int __whence);
328extern __off_t ftello (FILE *__stream) ;
329
330extern int fgetpos (FILE *__restrict __stream, fpos_t *__restrict __pos);
331extern int fsetpos (FILE *__stream, __const fpos_t *__pos);
332
333
334extern void clearerr (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
335extern int feof (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
336extern int ferror (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
337
338extern void clearerr_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
339extern int feof_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
340extern int ferror_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
341
342extern void perror (__const char *__s);
343
344extern int sys_nerr;
345extern __const char *__const sys_errlist[];
346extern int fileno (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
347extern int fileno_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
348extern FILE *popen (__const char *__command, __const char *__modes) ;
349extern int pclose (FILE *__stream);
350extern char *ctermid (char *__s) __attribute__ ((__nothrow__ , __leaf__));
351extern void flockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
352extern int ftrylockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
353extern void funlockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
354
355typedef int wchar_t;
356
357union wait
358 {
359 int w_status;
360 struct
361 {
362 unsigned int __w_termsig:7;
363 unsigned int __w_coredump:1;
364 unsigned int __w_retcode:8;
365 unsigned int:16;
366 } __wait_terminated;
367 struct
368 {
369 unsigned int __w_stopval:8;
370 unsigned int __w_stopsig:8;
371 unsigned int:16;
372 } __wait_stopped;
373 };
374typedef union
375 {
376 union wait *__uptr;
377 int *__iptr;
378 } __WAIT_STATUS __attribute__ ((__transparent_union__));
379
380typedef struct
381 {
382 int quot;
383 int rem;
384 } div_t;
385typedef struct
386 {
387 long int quot;
388 long int rem;
389 } ldiv_t;
390
391
392__extension__ typedef struct
393 {
394 long long int quot;
395 long long int rem;
396 } lldiv_t;
397
398extern size_t __ctype_get_mb_cur_max (void) __attribute__ ((__nothrow__ , __leaf__)) ;
399
400extern double atof (__const char *__nptr)
401 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
402extern int atoi (__const char *__nptr)
403 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
404extern long int atol (__const char *__nptr)
405 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
406
407
408__extension__ extern long long int atoll (__const char *__nptr)
409 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
410
411
412extern double strtod (__const char *__restrict __nptr,
413 char **__restrict __endptr)
414 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
415
416
417extern float strtof (__const char *__restrict __nptr,
418 char **__restrict __endptr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
419extern long double strtold (__const char *__restrict __nptr,
420 char **__restrict __endptr)
421 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
422
423
424extern long int strtol (__const char *__restrict __nptr,
425 char **__restrict __endptr, int __base)
426 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
427extern unsigned long int strtoul (__const char *__restrict __nptr,
428 char **__restrict __endptr, int __base)
429 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
430
431__extension__
432extern long long int strtoq (__const char *__restrict __nptr,
433 char **__restrict __endptr, int __base)
434 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
435__extension__
436extern unsigned long long int strtouq (__const char *__restrict __nptr,
437 char **__restrict __endptr, int __base)
438 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
439
440__extension__
441extern long long int strtoll (__const char *__restrict __nptr,
442 char **__restrict __endptr, int __base)
443 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
444__extension__
445extern unsigned long long int strtoull (__const char *__restrict __nptr,
446 char **__restrict __endptr, int __base)
447 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
448
449extern char *l64a (long int __n) __attribute__ ((__nothrow__ , __leaf__)) ;
450extern long int a64l (__const char *__s)
451 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
452
453typedef __u_char u_char;
454typedef __u_short u_short;
455typedef __u_int u_int;
456typedef __u_long u_long;
457typedef __quad_t quad_t;
458typedef __u_quad_t u_quad_t;
459typedef __fsid_t fsid_t;
460typedef __loff_t loff_t;
461typedef __ino_t ino_t;
462typedef __dev_t dev_t;
463typedef __gid_t gid_t;
464typedef __mode_t mode_t;
465typedef __nlink_t nlink_t;
466typedef __uid_t uid_t;
467typedef __pid_t pid_t;
468typedef __id_t id_t;
469typedef __daddr_t daddr_t;
470typedef __caddr_t caddr_t;
471typedef __key_t key_t;
472
473typedef __clock_t clock_t;
474
475
476
477typedef __time_t time_t;
478
479
480typedef __clockid_t clockid_t;
481typedef __timer_t timer_t;
482typedef unsigned long int ulong;
483typedef unsigned short int ushort;
484typedef unsigned int uint;
485typedef int int8_t __attribute__ ((__mode__ (__QI__)));
486typedef int int16_t __attribute__ ((__mode__ (__HI__)));
487typedef int int32_t __attribute__ ((__mode__ (__SI__)));
488typedef int int64_t __attribute__ ((__mode__ (__DI__)));
489typedef unsigned int u_int8_t __attribute__ ((__mode__ (__QI__)));
490typedef unsigned int u_int16_t __attribute__ ((__mode__ (__HI__)));
491typedef unsigned int u_int32_t __attribute__ ((__mode__ (__SI__)));
492typedef unsigned int u_int64_t __attribute__ ((__mode__ (__DI__)));
493typedef int register_t __attribute__ ((__mode__ (__word__)));
494typedef int __sig_atomic_t;
495typedef struct
496 {
497 unsigned long int __val[(1024 / (8 * sizeof (unsigned long int)))];
498 } __sigset_t;
499typedef __sigset_t sigset_t;
500struct timespec
501 {
502 __time_t tv_sec;
503 long int tv_nsec;
504 };
505struct timeval
506 {
507 __time_t tv_sec;
508 __suseconds_t tv_usec;
509 };
510typedef __suseconds_t suseconds_t;
511typedef long int __fd_mask;
512typedef struct
513 {
514 __fd_mask __fds_bits[1024 / (8 * (int) sizeof (__fd_mask))];
515 } fd_set;
516typedef __fd_mask fd_mask;
517
518extern int select (int __nfds, fd_set *__restrict __readfds,
519 fd_set *__restrict __writefds,
520 fd_set *__restrict __exceptfds,
521 struct timeval *__restrict __timeout);
522extern int pselect (int __nfds, fd_set *__restrict __readfds,
523 fd_set *__restrict __writefds,
524 fd_set *__restrict __exceptfds,
525 const struct timespec *__restrict __timeout,
526 const __sigset_t *__restrict __sigmask);
527
528
529__extension__
530extern unsigned int gnu_dev_major (unsigned long long int __dev)
531 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
532__extension__
533extern unsigned int gnu_dev_minor (unsigned long long int __dev)
534 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
535__extension__
536extern unsigned long long int gnu_dev_makedev (unsigned int __major,
537 unsigned int __minor)
538 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
539
540typedef __blksize_t blksize_t;
541typedef __blkcnt_t blkcnt_t;
542typedef __fsblkcnt_t fsblkcnt_t;
543typedef __fsfilcnt_t fsfilcnt_t;
544typedef unsigned long int pthread_t;
545typedef union
546{
547 char __size[56];
548 long int __align;
549} pthread_attr_t;
550typedef struct __pthread_internal_list
551{
552 struct __pthread_internal_list *__prev;
553 struct __pthread_internal_list *__next;
554} __pthread_list_t;
555typedef union
556{
557 struct __pthread_mutex_s
558 {
559 int __lock;
560 unsigned int __count;
561 int __owner;
562 unsigned int __nusers;
563 int __kind;
564 int __spins;
565 __pthread_list_t __list;
566 } __data;
567 char __size[40];
568 long int __align;
569} pthread_mutex_t;
570typedef union
571{
572 char __size[4];
573 int __align;
574} pthread_mutexattr_t;
575typedef union
576{
577 struct
578 {
579 int __lock;
580 unsigned int __futex;
581 __extension__ unsigned long long int __total_seq;
582 __extension__ unsigned long long int __wakeup_seq;
583 __extension__ unsigned long long int __woken_seq;
584 void *__mutex;
585 unsigned int __nwaiters;
586 unsigned int __broadcast_seq;
587 } __data;
588 char __size[48];
589 __extension__ long long int __align;
590} pthread_cond_t;
591typedef union
592{
593 char __size[4];
594 int __align;
595} pthread_condattr_t;
596typedef unsigned int pthread_key_t;
597typedef int pthread_once_t;
598typedef union
599{
600 struct
601 {
602 int __lock;
603 unsigned int __nr_readers;
604 unsigned int __readers_wakeup;
605 unsigned int __writer_wakeup;
606 unsigned int __nr_readers_queued;
607 unsigned int __nr_writers_queued;
608 int __writer;
609 int __shared;
610 unsigned long int __pad1;
611 unsigned long int __pad2;
612 unsigned int __flags;
613 } __data;
614 char __size[56];
615 long int __align;
616} pthread_rwlock_t;
617typedef union
618{
619 char __size[8];
620 long int __align;
621} pthread_rwlockattr_t;
622typedef volatile int pthread_spinlock_t;
623typedef union
624{
625 char __size[32];
626 long int __align;
627} pthread_barrier_t;
628typedef union
629{
630 char __size[4];
631 int __align;
632} pthread_barrierattr_t;
633
634extern long int random (void) __attribute__ ((__nothrow__ , __leaf__));
635extern void srandom (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));
636extern char *initstate (unsigned int __seed, char *__statebuf,
637 size_t __statelen) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
638extern char *setstate (char *__statebuf) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
639struct random_data
640 {
641 int32_t *fptr;
642 int32_t *rptr;
643 int32_t *state;
644 int rand_type;
645 int rand_deg;
646 int rand_sep;
647 int32_t *end_ptr;
648 };
649extern int random_r (struct random_data *__restrict __buf,
650 int32_t *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
651extern int srandom_r (unsigned int __seed, struct random_data *__buf)
652 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
653extern int initstate_r (unsigned int __seed, char *__restrict __statebuf,
654 size_t __statelen,
655 struct random_data *__restrict __buf)
656 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 4)));
657extern int setstate_r (char *__restrict __statebuf,
658 struct random_data *__restrict __buf)
659 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
660
661extern int rand (void) __attribute__ ((__nothrow__ , __leaf__));
662extern void srand (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));
663
664extern int rand_r (unsigned int *__seed) __attribute__ ((__nothrow__ , __leaf__));
665extern double drand48 (void) __attribute__ ((__nothrow__ , __leaf__));
666extern double erand48 (unsigned short int __xsubi[3]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
667extern long int lrand48 (void) __attribute__ ((__nothrow__ , __leaf__));
668extern long int nrand48 (unsigned short int __xsubi[3])
669 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
670extern long int mrand48 (void) __attribute__ ((__nothrow__ , __leaf__));
671extern long int jrand48 (unsigned short int __xsubi[3])
672 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
673extern void srand48 (long int __seedval) __attribute__ ((__nothrow__ , __leaf__));
674extern unsigned short int *seed48 (unsigned short int __seed16v[3])
675 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
676extern void lcong48 (unsigned short int __param[7]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
677struct drand48_data
678 {
679 unsigned short int __x[3];
680 unsigned short int __old_x[3];
681 unsigned short int __c;
682 unsigned short int __init;
683 unsigned long long int __a;
684 };
685extern int drand48_r (struct drand48_data *__restrict __buffer,
686 double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
687extern int erand48_r (unsigned short int __xsubi[3],
688 struct drand48_data *__restrict __buffer,
689 double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
690extern int lrand48_r (struct drand48_data *__restrict __buffer,
691 long int *__restrict __result)
692 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
693extern int nrand48_r (unsigned short int __xsubi[3],
694 struct drand48_data *__restrict __buffer,
695 long int *__restrict __result)
696 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
697extern int mrand48_r (struct drand48_data *__restrict __buffer,
698 long int *__restrict __result)
699 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
700extern int jrand48_r (unsigned short int __xsubi[3],
701 struct drand48_data *__restrict __buffer,
702 long int *__restrict __result)
703 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
704extern int srand48_r (long int __seedval, struct drand48_data *__buffer)
705 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
706extern int seed48_r (unsigned short int __seed16v[3],
707 struct drand48_data *__buffer) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
708extern int lcong48_r (unsigned short int __param[7],
709 struct drand48_data *__buffer)
710 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
711
712extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
713extern void *calloc (size_t __nmemb, size_t __size)
714 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
715
716
717extern void *realloc (void *__ptr, size_t __size)
718 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__warn_unused_result__));
719extern void free (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));
720
721extern void cfree (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));
722
723extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__));
724
725extern void *valloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
726extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size)
727 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
728
729extern void abort (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
730extern int atexit (void (*__func) (void)) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
731
732extern int on_exit (void (*__func) (int __status, void *__arg), void *__arg)
733 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
734
735extern void exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
736
737
738extern void _Exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
739
740
741extern char *getenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
742
743extern char *__secure_getenv (__const char *__name)
744 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
745extern int putenv (char *__string) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
746extern int setenv (__const char *__name, __const char *__value, int __replace)
747 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
748extern int unsetenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
749extern int clearenv (void) __attribute__ ((__nothrow__ , __leaf__));
750extern char *mktemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
751extern int mkstemp (char *__template) __attribute__ ((__nonnull__ (1))) ;
752extern int mkstemps (char *__template, int __suffixlen) __attribute__ ((__nonnull__ (1))) ;
753extern char *mkdtemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
754
755extern int system (__const char *__command) ;
756
757extern char *realpath (__const char *__restrict __name,
758 char *__restrict __resolved) __attribute__ ((__nothrow__ , __leaf__)) ;
759typedef int (*__compar_fn_t) (__const void *, __const void *);
760
761extern void *bsearch (__const void *__key, __const void *__base,
762 size_t __nmemb, size_t __size, __compar_fn_t __compar)
763 __attribute__ ((__nonnull__ (1, 2, 5))) ;
764extern void qsort (void *__base, size_t __nmemb, size_t __size,
765 __compar_fn_t __compar) __attribute__ ((__nonnull__ (1, 4)));
766
767
768
769
770
771extern int abs (int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
772extern long int labs (long int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
773
774
775
776__extension__ extern long long int llabs (long long int __x)
777 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
778
779
780
781
782
783
784
785extern div_t div (int __numer, int __denom)
786 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
787extern ldiv_t ldiv (long int __numer, long int __denom)
788 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
789
790
791
792
793__extension__ extern lldiv_t lldiv (long long int __numer,
794 long long int __denom)
795 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
796
797extern char *ecvt (double __value, int __ndigit, int *__restrict __decpt,
798 int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
799extern char *fcvt (double __value, int __ndigit, int *__restrict __decpt,
800 int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
801extern char *gcvt (double __value, int __ndigit, char *__buf)
802 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;
803extern char *qecvt (long double __value, int __ndigit,
804 int *__restrict __decpt, int *__restrict __sign)
805 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
806extern char *qfcvt (long double __value, int __ndigit,
807 int *__restrict __decpt, int *__restrict __sign)
808 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
809extern char *qgcvt (long double __value, int __ndigit, char *__buf)
810 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;
811extern int ecvt_r (double __value, int __ndigit, int *__restrict __decpt,
812 int *__restrict __sign, char *__restrict __buf,
813 size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
814extern int fcvt_r (double __value, int __ndigit, int *__restrict __decpt,
815 int *__restrict __sign, char *__restrict __buf,
816 size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
817extern int qecvt_r (long double __value, int __ndigit,
818 int *__restrict __decpt, int *__restrict __sign,
819 char *__restrict __buf, size_t __len)
820 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
821extern int qfcvt_r (long double __value, int __ndigit,
822 int *__restrict __decpt, int *__restrict __sign,
823 char *__restrict __buf, size_t __len)
824 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
825
826extern int mblen (__const char *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ;
827extern int mbtowc (wchar_t *__restrict __pwc,
828 __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ;
829extern int wctomb (char *__s, wchar_t __wchar) __attribute__ ((__nothrow__ , __leaf__)) ;
830extern size_t mbstowcs (wchar_t *__restrict __pwcs,
831 __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
832extern size_t wcstombs (char *__restrict __s,
833 __const wchar_t *__restrict __pwcs, size_t __n)
834 __attribute__ ((__nothrow__ , __leaf__));
835
836extern int rpmatch (__const char *__response) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
837extern int getsubopt (char **__restrict __optionp,
838 char *__const *__restrict __tokens,
839 char **__restrict __valuep)
840 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))) ;
841extern int getloadavg (double __loadavg[], int __nelem)
842 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
843
844typedef struct list {
845 int key;
846 struct list *next;
847} mlist;
848mlist *head;
849mlist* search_list(mlist *l, int k){
850 l = head;
851 while(l!=((void *)0) && l->key!=k) {
852 l = l->next;
853 }
854 return l;
855}
856int delete_list(mlist *l){
857 mlist *tmp;
858 tmp = head;
859 if (head != l) {
860 while(tmp->next!=l) {
861 tmp = tmp->next;
862 }
863 } else {
864 head = l->next;
865 }
866 tmp->next = l->next;
867 free(l);
868 return 0;
869}
870int insert_list(mlist *l, int k){
871 l = (mlist*)malloc(sizeof(mlist));
872 if (head==((void *)0)) {
873 l->key = k;
874 l->next = ((void *)0);
875 } else {
876 l->key = k;
877 l->next = head;
878 }
879 head = l;
880 return 0;
881}
882int main(void){
883 int i;
884 mlist *mylist, *temp;
885 insert_list(mylist,2);
886 insert_list(mylist,5);
887 insert_list(mylist,1);
888 insert_list(mylist,3);
889 mylist = head;
890 while(mylist) {
891 mylist = mylist->next;
892 }
893 temp = search_list(mylist,2);
894 __VERIFIER_assert(temp->key==2);
895 delete_list(temp);
896 mylist = head;
897 while(mylist) {
898 mylist = mylist->next;
899 }
900 return 0;
901}