1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7typedef long unsigned int size_t;
8typedef int wchar_t;
9
10union wait
11 {
12 int w_status;
13 struct
14 {
15 unsigned int __w_termsig:7;
16 unsigned int __w_coredump:1;
17 unsigned int __w_retcode:8;
18 unsigned int:16;
19 } __wait_terminated;
20 struct
21 {
22 unsigned int __w_stopval:8;
23 unsigned int __w_stopsig:8;
24 unsigned int:16;
25 } __wait_stopped;
26 };
27typedef union
28 {
29 union wait *__uptr;
30 int *__iptr;
31 } __WAIT_STATUS __attribute__ ((__transparent_union__));
32
33typedef struct
34 {
35 int quot;
36 int rem;
37 } div_t;
38typedef struct
39 {
40 long int quot;
41 long int rem;
42 } ldiv_t;
43
44
45__extension__ typedef struct
46 {
47 long long int quot;
48 long long int rem;
49 } lldiv_t;
50
51extern size_t __ctype_get_mb_cur_max (void) __attribute__ ((__nothrow__ , __leaf__)) ;
52
53extern double atof (__const char *__nptr)
54 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
55extern int atoi (__const char *__nptr)
56 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
57extern long int atol (__const char *__nptr)
58 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
59
60
61__extension__ extern long long int atoll (__const char *__nptr)
62 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
63
64
65extern double strtod (__const char *__restrict __nptr,
66 char **__restrict __endptr)
67 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
68
69
70extern float strtof (__const char *__restrict __nptr,
71 char **__restrict __endptr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
72extern long double strtold (__const char *__restrict __nptr,
73 char **__restrict __endptr)
74 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
75
76
77extern long int strtol (__const char *__restrict __nptr,
78 char **__restrict __endptr, int __base)
79 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
80extern unsigned long int strtoul (__const char *__restrict __nptr,
81 char **__restrict __endptr, int __base)
82 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
83
84__extension__
85extern long long int strtoq (__const char *__restrict __nptr,
86 char **__restrict __endptr, int __base)
87 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
88__extension__
89extern unsigned long long int strtouq (__const char *__restrict __nptr,
90 char **__restrict __endptr, int __base)
91 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
92
93__extension__
94extern long long int strtoll (__const char *__restrict __nptr,
95 char **__restrict __endptr, int __base)
96 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
97__extension__
98extern unsigned long long int strtoull (__const char *__restrict __nptr,
99 char **__restrict __endptr, int __base)
100 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
101
102extern char *l64a (long int __n) __attribute__ ((__nothrow__ , __leaf__)) ;
103extern long int a64l (__const char *__s)
104 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
105
106typedef unsigned char __u_char;
107typedef unsigned short int __u_short;
108typedef unsigned int __u_int;
109typedef unsigned long int __u_long;
110typedef signed char __int8_t;
111typedef unsigned char __uint8_t;
112typedef signed short int __int16_t;
113typedef unsigned short int __uint16_t;
114typedef signed int __int32_t;
115typedef unsigned int __uint32_t;
116typedef signed long int __int64_t;
117typedef unsigned long int __uint64_t;
118typedef long int __quad_t;
119typedef unsigned long int __u_quad_t;
120typedef unsigned long int __dev_t;
121typedef unsigned int __uid_t;
122typedef unsigned int __gid_t;
123typedef unsigned long int __ino_t;
124typedef unsigned long int __ino64_t;
125typedef unsigned int __mode_t;
126typedef unsigned long int __nlink_t;
127typedef long int __off_t;
128typedef long int __off64_t;
129typedef int __pid_t;
130typedef struct { int __val[2]; } __fsid_t;
131typedef long int __clock_t;
132typedef unsigned long int __rlim_t;
133typedef unsigned long int __rlim64_t;
134typedef unsigned int __id_t;
135typedef long int __time_t;
136typedef unsigned int __useconds_t;
137typedef long int __suseconds_t;
138typedef int __daddr_t;
139typedef long int __swblk_t;
140typedef int __key_t;
141typedef int __clockid_t;
142typedef void * __timer_t;
143typedef long int __blksize_t;
144typedef long int __blkcnt_t;
145typedef long int __blkcnt64_t;
146typedef unsigned long int __fsblkcnt_t;
147typedef unsigned long int __fsblkcnt64_t;
148typedef unsigned long int __fsfilcnt_t;
149typedef unsigned long int __fsfilcnt64_t;
150typedef long int __ssize_t;
151typedef __off64_t __loff_t;
152typedef __quad_t *__qaddr_t;
153typedef char *__caddr_t;
154typedef long int __intptr_t;
155typedef unsigned int __socklen_t;
156typedef __u_char u_char;
157typedef __u_short u_short;
158typedef __u_int u_int;
159typedef __u_long u_long;
160typedef __quad_t quad_t;
161typedef __u_quad_t u_quad_t;
162typedef __fsid_t fsid_t;
163typedef __loff_t loff_t;
164typedef __ino_t ino_t;
165typedef __dev_t dev_t;
166typedef __gid_t gid_t;
167typedef __mode_t mode_t;
168typedef __nlink_t nlink_t;
169typedef __uid_t uid_t;
170typedef __off_t off_t;
171typedef __pid_t pid_t;
172typedef __id_t id_t;
173typedef __ssize_t ssize_t;
174typedef __daddr_t daddr_t;
175typedef __caddr_t caddr_t;
176typedef __key_t key_t;
177
178typedef __clock_t clock_t;
179
180
181
182typedef __time_t time_t;
183
184
185typedef __clockid_t clockid_t;
186typedef __timer_t timer_t;
187typedef unsigned long int ulong;
188typedef unsigned short int ushort;
189typedef unsigned int uint;
190
191
192
193
194
195typedef int int8_t __attribute__ ((__mode__ (__QI__)));
196typedef int int16_t __attribute__ ((__mode__ (__HI__)));
197typedef int int32_t __attribute__ ((__mode__ (__SI__)));
198typedef int int64_t __attribute__ ((__mode__ (__DI__)));
199
200
201typedef unsigned int u_int8_t __attribute__ ((__mode__ (__QI__)));
202typedef unsigned int u_int16_t __attribute__ ((__mode__ (__HI__)));
203typedef unsigned int u_int32_t __attribute__ ((__mode__ (__SI__)));
204typedef unsigned int u_int64_t __attribute__ ((__mode__ (__DI__)));
205
206typedef int register_t __attribute__ ((__mode__ (__word__)));
207typedef int __sig_atomic_t;
208typedef struct
209 {
210 unsigned long int __val[(1024 / (8 * sizeof (unsigned long int)))];
211 } __sigset_t;
212typedef __sigset_t sigset_t;
213struct timespec
214 {
215 __time_t tv_sec;
216 long int tv_nsec;
217 };
218struct timeval
219 {
220 __time_t tv_sec;
221 __suseconds_t tv_usec;
222 };
223typedef __suseconds_t suseconds_t;
224typedef long int __fd_mask;
225typedef struct
226 {
227 __fd_mask __fds_bits[1024 / (8 * (int) sizeof (__fd_mask))];
228 } fd_set;
229typedef __fd_mask fd_mask;
230
231extern int select (int __nfds, fd_set *__restrict __readfds,
232 fd_set *__restrict __writefds,
233 fd_set *__restrict __exceptfds,
234 struct timeval *__restrict __timeout);
235extern int pselect (int __nfds, fd_set *__restrict __readfds,
236 fd_set *__restrict __writefds,
237 fd_set *__restrict __exceptfds,
238 const struct timespec *__restrict __timeout,
239 const __sigset_t *__restrict __sigmask);
240
241
242__extension__
243extern unsigned int gnu_dev_major (unsigned long long int __dev)
244 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
245__extension__
246extern unsigned int gnu_dev_minor (unsigned long long int __dev)
247 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
248__extension__
249extern unsigned long long int gnu_dev_makedev (unsigned int __major,
250 unsigned int __minor)
251 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
252
253typedef __blksize_t blksize_t;
254typedef __blkcnt_t blkcnt_t;
255typedef __fsblkcnt_t fsblkcnt_t;
256typedef __fsfilcnt_t fsfilcnt_t;
257typedef unsigned long int pthread_t;
258typedef union
259{
260 char __size[56];
261 long int __align;
262} pthread_attr_t;
263typedef struct __pthread_internal_list
264{
265 struct __pthread_internal_list *__prev;
266 struct __pthread_internal_list *__next;
267} __pthread_list_t;
268typedef union
269{
270 struct __pthread_mutex_s
271 {
272 int __lock;
273 unsigned int __count;
274 int __owner;
275 unsigned int __nusers;
276 int __kind;
277 int __spins;
278 __pthread_list_t __list;
279 } __data;
280 char __size[40];
281 long int __align;
282} pthread_mutex_t;
283typedef union
284{
285 char __size[4];
286 int __align;
287} pthread_mutexattr_t;
288typedef union
289{
290 struct
291 {
292 int __lock;
293 unsigned int __futex;
294 __extension__ unsigned long long int __total_seq;
295 __extension__ unsigned long long int __wakeup_seq;
296 __extension__ unsigned long long int __woken_seq;
297 void *__mutex;
298 unsigned int __nwaiters;
299 unsigned int __broadcast_seq;
300 } __data;
301 char __size[48];
302 __extension__ long long int __align;
303} pthread_cond_t;
304typedef union
305{
306 char __size[4];
307 int __align;
308} pthread_condattr_t;
309typedef unsigned int pthread_key_t;
310typedef int pthread_once_t;
311typedef union
312{
313 struct
314 {
315 int __lock;
316 unsigned int __nr_readers;
317 unsigned int __readers_wakeup;
318 unsigned int __writer_wakeup;
319 unsigned int __nr_readers_queued;
320 unsigned int __nr_writers_queued;
321 int __writer;
322 int __shared;
323 unsigned long int __pad1;
324 unsigned long int __pad2;
325 unsigned int __flags;
326 } __data;
327 char __size[56];
328 long int __align;
329} pthread_rwlock_t;
330typedef union
331{
332 char __size[8];
333 long int __align;
334} pthread_rwlockattr_t;
335typedef volatile int pthread_spinlock_t;
336typedef union
337{
338 char __size[32];
339 long int __align;
340} pthread_barrier_t;
341typedef union
342{
343 char __size[4];
344 int __align;
345} pthread_barrierattr_t;
346
347extern long int random (void) __attribute__ ((__nothrow__ , __leaf__));
348extern void srandom (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));
349extern char *initstate (unsigned int __seed, char *__statebuf,
350 size_t __statelen) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
351extern char *setstate (char *__statebuf) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
352struct random_data
353 {
354 int32_t *fptr;
355 int32_t *rptr;
356 int32_t *state;
357 int rand_type;
358 int rand_deg;
359 int rand_sep;
360 int32_t *end_ptr;
361 };
362extern int random_r (struct random_data *__restrict __buf,
363 int32_t *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
364extern int srandom_r (unsigned int __seed, struct random_data *__buf)
365 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
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
617typedef struct list {
618 int key;
619 struct list *next;
620} mlist;
621mlist *head;
622mlist* search_list(mlist *l, int k){
623 l = head;
624 while(l!=((void *)0) && l->key!=k) {
625 l = l->next;
626 }
627 return l;
628}
629int insert_list(mlist *l, int k){
630 l = (mlist*)malloc(sizeof(mlist));
631 l->key = k;
632 if (head==((void *)0)) {
633 l->next = ((void *)0);
634 } else {
635 l->key = k;
636 l->next = head;
637 }
638 head = l;
639 return 0;
640}
641int main(void){
642 int i;
643 mlist *mylist, *temp;
644 insert_list(mylist,2);
645 insert_list(mylist,5);
646 insert_list(mylist,1);
647 insert_list(mylist,3);
648 temp = search_list(head,2);
649 __VERIFIER_assert(temp->key==1);
650}