source: CIVL/examples/svcomp17/elimination_backoff_stack_false-unreach-call.i@ beab7f2

main test-branch
Last change on this file since beab7f2 was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 63.2 KB
Line 
1
2typedef unsigned int size_t;
3typedef unsigned char __u_char;
4typedef unsigned short int __u_short;
5typedef unsigned int __u_int;
6typedef unsigned long int __u_long;
7typedef signed char __int8_t;
8typedef unsigned char __uint8_t;
9typedef signed short int __int16_t;
10typedef unsigned short int __uint16_t;
11typedef signed int __int32_t;
12typedef unsigned int __uint32_t;
13__extension__ typedef signed long long int __int64_t;
14__extension__ typedef unsigned long long int __uint64_t;
15__extension__ typedef long long int __quad_t;
16__extension__ typedef unsigned long long int __u_quad_t;
17__extension__ typedef __u_quad_t __dev_t;
18__extension__ typedef unsigned int __uid_t;
19__extension__ typedef unsigned int __gid_t;
20__extension__ typedef unsigned long int __ino_t;
21__extension__ typedef __u_quad_t __ino64_t;
22__extension__ typedef unsigned int __mode_t;
23__extension__ typedef unsigned int __nlink_t;
24__extension__ typedef long int __off_t;
25__extension__ typedef __quad_t __off64_t;
26__extension__ typedef int __pid_t;
27__extension__ typedef struct { int __val[2]; } __fsid_t;
28__extension__ typedef long int __clock_t;
29__extension__ typedef unsigned long int __rlim_t;
30__extension__ typedef __u_quad_t __rlim64_t;
31__extension__ typedef unsigned int __id_t;
32__extension__ typedef long int __time_t;
33__extension__ typedef unsigned int __useconds_t;
34__extension__ typedef long int __suseconds_t;
35__extension__ typedef int __daddr_t;
36__extension__ typedef int __key_t;
37__extension__ typedef int __clockid_t;
38__extension__ typedef void * __timer_t;
39__extension__ typedef long int __blksize_t;
40__extension__ typedef long int __blkcnt_t;
41__extension__ typedef __quad_t __blkcnt64_t;
42__extension__ typedef unsigned long int __fsblkcnt_t;
43__extension__ typedef __u_quad_t __fsblkcnt64_t;
44__extension__ typedef unsigned long int __fsfilcnt_t;
45__extension__ typedef __u_quad_t __fsfilcnt64_t;
46__extension__ typedef int __fsword_t;
47__extension__ typedef int __ssize_t;
48__extension__ typedef long int __syscall_slong_t;
49__extension__ typedef unsigned long int __syscall_ulong_t;
50typedef __off64_t __loff_t;
51typedef __quad_t *__qaddr_t;
52typedef char *__caddr_t;
53__extension__ typedef int __intptr_t;
54__extension__ typedef unsigned int __socklen_t;
55struct _IO_FILE;
56
57typedef struct _IO_FILE FILE;
58
59
60typedef struct _IO_FILE __FILE;
61typedef struct
62{
63 int __count;
64 union
65 {
66 unsigned int __wch;
67 char __wchb[4];
68 } __value;
69} __mbstate_t;
70typedef struct
71{
72 __off_t __pos;
73 __mbstate_t __state;
74} _G_fpos_t;
75typedef struct
76{
77 __off64_t __pos;
78 __mbstate_t __state;
79} _G_fpos64_t;
80typedef __builtin_va_list __gnuc_va_list;
81struct _IO_jump_t; struct _IO_FILE;
82typedef void _IO_lock_t;
83struct _IO_marker {
84 struct _IO_marker *_next;
85 struct _IO_FILE *_sbuf;
86 int _pos;
87};
88enum __codecvt_result
89{
90 __codecvt_ok,
91 __codecvt_partial,
92 __codecvt_error,
93 __codecvt_noconv
94};
95struct _IO_FILE {
96 int _flags;
97 char* _IO_read_ptr;
98 char* _IO_read_end;
99 char* _IO_read_base;
100 char* _IO_write_base;
101 char* _IO_write_ptr;
102 char* _IO_write_end;
103 char* _IO_buf_base;
104 char* _IO_buf_end;
105 char *_IO_save_base;
106 char *_IO_backup_base;
107 char *_IO_save_end;
108 struct _IO_marker *_markers;
109 struct _IO_FILE *_chain;
110 int _fileno;
111 int _flags2;
112 __off_t _old_offset;
113 unsigned short _cur_column;
114 signed char _vtable_offset;
115 char _shortbuf[1];
116 _IO_lock_t *_lock;
117 __off64_t _offset;
118 void *__pad1;
119 void *__pad2;
120 void *__pad3;
121 void *__pad4;
122 size_t __pad5;
123 int _mode;
124 char _unused2[15 * sizeof (int) - 4 * sizeof (void *) - sizeof (size_t)];
125};
126typedef struct _IO_FILE _IO_FILE;
127struct _IO_FILE_plus;
128extern struct _IO_FILE_plus _IO_2_1_stdin_;
129extern struct _IO_FILE_plus _IO_2_1_stdout_;
130extern struct _IO_FILE_plus _IO_2_1_stderr_;
131typedef __ssize_t __io_read_fn (void *__cookie, char *__buf, size_t __nbytes);
132typedef __ssize_t __io_write_fn (void *__cookie, const char *__buf,
133 size_t __n);
134typedef int __io_seek_fn (void *__cookie, __off64_t *__pos, int __w);
135typedef int __io_close_fn (void *__cookie);
136extern int __underflow (_IO_FILE *);
137extern int __uflow (_IO_FILE *);
138extern int __overflow (_IO_FILE *, int);
139extern int _IO_getc (_IO_FILE *__fp);
140extern int _IO_putc (int __c, _IO_FILE *__fp);
141extern int _IO_feof (_IO_FILE *__fp) __attribute__ ((__nothrow__ , __leaf__));
142extern int _IO_ferror (_IO_FILE *__fp) __attribute__ ((__nothrow__ , __leaf__));
143extern int _IO_peekc_locked (_IO_FILE *__fp);
144extern void _IO_flockfile (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
145extern void _IO_funlockfile (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
146extern int _IO_ftrylockfile (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
147extern int _IO_vfscanf (_IO_FILE * __restrict, const char * __restrict,
148 __gnuc_va_list, int *__restrict);
149extern int _IO_vfprintf (_IO_FILE *__restrict, const char *__restrict,
150 __gnuc_va_list);
151extern __ssize_t _IO_padn (_IO_FILE *, int, __ssize_t);
152extern size_t _IO_sgetn (_IO_FILE *, void *, size_t);
153extern __off64_t _IO_seekoff (_IO_FILE *, __off64_t, int, int);
154extern __off64_t _IO_seekpos (_IO_FILE *, __off64_t, int);
155extern void _IO_free_backup_area (_IO_FILE *) __attribute__ ((__nothrow__ , __leaf__));
156typedef __gnuc_va_list va_list;
157typedef __off_t off_t;
158typedef __ssize_t ssize_t;
159
160typedef _G_fpos_t fpos_t;
161
162extern struct _IO_FILE *stdin;
163extern struct _IO_FILE *stdout;
164extern struct _IO_FILE *stderr;
165
166extern int remove (const char *__filename) __attribute__ ((__nothrow__ , __leaf__));
167extern int rename (const char *__old, const char *__new) __attribute__ ((__nothrow__ , __leaf__));
168
169extern int renameat (int __oldfd, const char *__old, int __newfd,
170 const char *__new) __attribute__ ((__nothrow__ , __leaf__));
171
172extern FILE *tmpfile (void) ;
173extern char *tmpnam (char *__s) __attribute__ ((__nothrow__ , __leaf__)) ;
174
175extern char *tmpnam_r (char *__s) __attribute__ ((__nothrow__ , __leaf__)) ;
176extern char *tempnam (const char *__dir, const char *__pfx)
177 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
178
179extern int fclose (FILE *__stream);
180extern int fflush (FILE *__stream);
181
182extern int fflush_unlocked (FILE *__stream);
183
184extern FILE *fopen (const char *__restrict __filename,
185 const char *__restrict __modes) ;
186extern FILE *freopen (const char *__restrict __filename,
187 const char *__restrict __modes,
188 FILE *__restrict __stream) ;
189
190extern FILE *fdopen (int __fd, const char *__modes) __attribute__ ((__nothrow__ , __leaf__)) ;
191extern FILE *fmemopen (void *__s, size_t __len, const char *__modes)
192 __attribute__ ((__nothrow__ , __leaf__)) ;
193extern FILE *open_memstream (char **__bufloc, size_t *__sizeloc) __attribute__ ((__nothrow__ , __leaf__)) ;
194
195extern void setbuf (FILE *__restrict __stream, char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__));
196extern int setvbuf (FILE *__restrict __stream, char *__restrict __buf,
197 int __modes, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
198
199extern void setbuffer (FILE *__restrict __stream, char *__restrict __buf,
200 size_t __size) __attribute__ ((__nothrow__ , __leaf__));
201extern void setlinebuf (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
202
203extern int fprintf (FILE *__restrict __stream,
204 const char *__restrict __format, ...);
205extern int printf (const char *__restrict __format, ...);
206extern int sprintf (char *__restrict __s,
207 const char *__restrict __format, ...) __attribute__ ((__nothrow__));
208extern int vfprintf (FILE *__restrict __s, const char *__restrict __format,
209 __gnuc_va_list __arg);
210extern int vprintf (const char *__restrict __format, __gnuc_va_list __arg);
211extern int vsprintf (char *__restrict __s, const char *__restrict __format,
212 __gnuc_va_list __arg) __attribute__ ((__nothrow__));
213
214
215extern int snprintf (char *__restrict __s, size_t __maxlen,
216 const char *__restrict __format, ...)
217 __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 4)));
218extern int vsnprintf (char *__restrict __s, size_t __maxlen,
219 const char *__restrict __format, __gnuc_va_list __arg)
220 __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 0)));
221
222extern int vdprintf (int __fd, const char *__restrict __fmt,
223 __gnuc_va_list __arg)
224 __attribute__ ((__format__ (__printf__, 2, 0)));
225extern int dprintf (int __fd, const char *__restrict __fmt, ...)
226 __attribute__ ((__format__ (__printf__, 2, 3)));
227
228extern int fscanf (FILE *__restrict __stream,
229 const char *__restrict __format, ...) ;
230extern int scanf (const char *__restrict __format, ...) ;
231extern int sscanf (const char *__restrict __s,
232 const char *__restrict __format, ...) __attribute__ ((__nothrow__ , __leaf__));
233extern int fscanf (FILE *__restrict __stream, const char *__restrict __format, ...) __asm__ ("" "__isoc99_fscanf") ;
234extern int scanf (const char *__restrict __format, ...) __asm__ ("" "__isoc99_scanf") ;
235extern int sscanf (const char *__restrict __s, const char *__restrict __format, ...) __asm__ ("" "__isoc99_sscanf") __attribute__ ((__nothrow__ , __leaf__));
236
237
238extern int vfscanf (FILE *__restrict __s, const char *__restrict __format,
239 __gnuc_va_list __arg)
240 __attribute__ ((__format__ (__scanf__, 2, 0))) ;
241extern int vscanf (const char *__restrict __format, __gnuc_va_list __arg)
242 __attribute__ ((__format__ (__scanf__, 1, 0))) ;
243extern int vsscanf (const char *__restrict __s,
244 const char *__restrict __format, __gnuc_va_list __arg)
245 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__format__ (__scanf__, 2, 0)));
246extern int vfscanf (FILE *__restrict __s, const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vfscanf")
247 __attribute__ ((__format__ (__scanf__, 2, 0))) ;
248extern int vscanf (const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vscanf")
249 __attribute__ ((__format__ (__scanf__, 1, 0))) ;
250extern int vsscanf (const char *__restrict __s, const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vsscanf") __attribute__ ((__nothrow__ , __leaf__))
251 __attribute__ ((__format__ (__scanf__, 2, 0)));
252
253
254extern int fgetc (FILE *__stream);
255extern int getc (FILE *__stream);
256extern int getchar (void);
257
258extern int getc_unlocked (FILE *__stream);
259extern int getchar_unlocked (void);
260extern int fgetc_unlocked (FILE *__stream);
261
262extern int fputc (int __c, FILE *__stream);
263extern int putc (int __c, FILE *__stream);
264extern int putchar (int __c);
265
266extern int fputc_unlocked (int __c, FILE *__stream);
267extern int putc_unlocked (int __c, FILE *__stream);
268extern int putchar_unlocked (int __c);
269extern int getw (FILE *__stream);
270extern int putw (int __w, FILE *__stream);
271
272extern char *fgets (char *__restrict __s, int __n, FILE *__restrict __stream)
273 ;
274
275extern __ssize_t __getdelim (char **__restrict __lineptr,
276 size_t *__restrict __n, int __delimiter,
277 FILE *__restrict __stream) ;
278extern __ssize_t getdelim (char **__restrict __lineptr,
279 size_t *__restrict __n, int __delimiter,
280 FILE *__restrict __stream) ;
281extern __ssize_t getline (char **__restrict __lineptr,
282 size_t *__restrict __n,
283 FILE *__restrict __stream) ;
284
285extern int fputs (const char *__restrict __s, FILE *__restrict __stream);
286extern int puts (const char *__s);
287extern int ungetc (int __c, FILE *__stream);
288extern size_t fread (void *__restrict __ptr, size_t __size,
289 size_t __n, FILE *__restrict __stream) ;
290extern size_t fwrite (const void *__restrict __ptr, size_t __size,
291 size_t __n, FILE *__restrict __s);
292
293extern size_t fread_unlocked (void *__restrict __ptr, size_t __size,
294 size_t __n, FILE *__restrict __stream) ;
295extern size_t fwrite_unlocked (const void *__restrict __ptr, size_t __size,
296 size_t __n, FILE *__restrict __stream);
297
298extern int fseek (FILE *__stream, long int __off, int __whence);
299extern long int ftell (FILE *__stream) ;
300extern void rewind (FILE *__stream);
301
302extern int fseeko (FILE *__stream, __off_t __off, int __whence);
303extern __off_t ftello (FILE *__stream) ;
304
305extern int fgetpos (FILE *__restrict __stream, fpos_t *__restrict __pos);
306extern int fsetpos (FILE *__stream, const fpos_t *__pos);
307
308
309extern void clearerr (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
310extern int feof (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
311extern int ferror (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
312
313extern void clearerr_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
314extern int feof_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
315extern int ferror_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
316
317extern void perror (const char *__s);
318
319extern int sys_nerr;
320extern const char *const sys_errlist[];
321extern int fileno (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
322extern int fileno_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
323extern FILE *popen (const char *__command, const char *__modes) ;
324extern int pclose (FILE *__stream);
325extern char *ctermid (char *__s) __attribute__ ((__nothrow__ , __leaf__));
326extern void flockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
327extern int ftrylockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ;
328extern void funlockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__));
329
330typedef long int wchar_t;
331
332typedef enum
333{
334 P_ALL,
335 P_PID,
336 P_PGID
337} idtype_t;
338static __inline unsigned int
339__bswap_32 (unsigned int __bsx)
340{
341 return __builtin_bswap32 (__bsx);
342}
343static __inline __uint64_t
344__bswap_64 (__uint64_t __bsx)
345{
346 return __builtin_bswap64 (__bsx);
347}
348union wait
349 {
350 int w_status;
351 struct
352 {
353 unsigned int __w_termsig:7;
354 unsigned int __w_coredump:1;
355 unsigned int __w_retcode:8;
356 unsigned int:16;
357 } __wait_terminated;
358 struct
359 {
360 unsigned int __w_stopval:8;
361 unsigned int __w_stopsig:8;
362 unsigned int:16;
363 } __wait_stopped;
364 };
365typedef union
366 {
367 union wait *__uptr;
368 int *__iptr;
369 } __WAIT_STATUS __attribute__ ((__transparent_union__));
370
371typedef struct
372 {
373 int quot;
374 int rem;
375 } div_t;
376typedef struct
377 {
378 long int quot;
379 long int rem;
380 } ldiv_t;
381
382
383__extension__ typedef struct
384 {
385 long long int quot;
386 long long int rem;
387 } lldiv_t;
388
389extern size_t __ctype_get_mb_cur_max (void) __attribute__ ((__nothrow__ , __leaf__)) ;
390
391extern double atof (const char *__nptr)
392 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
393extern int atoi (const char *__nptr)
394 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
395extern long int atol (const char *__nptr)
396 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
397
398
399__extension__ extern long long int atoll (const char *__nptr)
400 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
401
402
403extern double strtod (const char *__restrict __nptr,
404 char **__restrict __endptr)
405 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
406
407
408extern float strtof (const char *__restrict __nptr,
409 char **__restrict __endptr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
410extern long double strtold (const char *__restrict __nptr,
411 char **__restrict __endptr)
412 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
413
414
415extern long int strtol (const char *__restrict __nptr,
416 char **__restrict __endptr, int __base)
417 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
418extern unsigned long int strtoul (const char *__restrict __nptr,
419 char **__restrict __endptr, int __base)
420 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
421
422__extension__
423extern long long int strtoq (const char *__restrict __nptr,
424 char **__restrict __endptr, int __base)
425 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
426__extension__
427extern unsigned long long int strtouq (const char *__restrict __nptr,
428 char **__restrict __endptr, int __base)
429 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
430
431__extension__
432extern long long int strtoll (const char *__restrict __nptr,
433 char **__restrict __endptr, int __base)
434 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
435__extension__
436extern unsigned long long int strtoull (const char *__restrict __nptr,
437 char **__restrict __endptr, int __base)
438 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
439
440extern char *l64a (long int __n) __attribute__ ((__nothrow__ , __leaf__)) ;
441extern long int a64l (const char *__s)
442 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
443
444typedef __u_char u_char;
445typedef __u_short u_short;
446typedef __u_int u_int;
447typedef __u_long u_long;
448typedef __quad_t quad_t;
449typedef __u_quad_t u_quad_t;
450typedef __fsid_t fsid_t;
451typedef __loff_t loff_t;
452typedef __ino_t ino_t;
453typedef __dev_t dev_t;
454typedef __gid_t gid_t;
455typedef __mode_t mode_t;
456typedef __nlink_t nlink_t;
457typedef __uid_t uid_t;
458typedef __pid_t pid_t;
459typedef __id_t id_t;
460typedef __daddr_t daddr_t;
461typedef __caddr_t caddr_t;
462typedef __key_t key_t;
463
464typedef __clock_t clock_t;
465
466
467
468typedef __time_t time_t;
469
470
471typedef __clockid_t clockid_t;
472typedef __timer_t timer_t;
473typedef unsigned long int ulong;
474typedef unsigned short int ushort;
475typedef unsigned int uint;
476typedef int int8_t __attribute__ ((__mode__ (__QI__)));
477typedef int int16_t __attribute__ ((__mode__ (__HI__)));
478typedef int int32_t __attribute__ ((__mode__ (__SI__)));
479typedef int int64_t __attribute__ ((__mode__ (__DI__)));
480typedef unsigned int u_int8_t __attribute__ ((__mode__ (__QI__)));
481typedef unsigned int u_int16_t __attribute__ ((__mode__ (__HI__)));
482typedef unsigned int u_int32_t __attribute__ ((__mode__ (__SI__)));
483typedef unsigned int u_int64_t __attribute__ ((__mode__ (__DI__)));
484typedef int register_t __attribute__ ((__mode__ (__word__)));
485typedef int __sig_atomic_t;
486typedef struct
487 {
488 unsigned long int __val[(1024 / (8 * sizeof (unsigned long int)))];
489 } __sigset_t;
490typedef __sigset_t sigset_t;
491struct timespec
492 {
493 __time_t tv_sec;
494 __syscall_slong_t tv_nsec;
495 };
496struct timeval
497 {
498 __time_t tv_sec;
499 __suseconds_t tv_usec;
500 };
501typedef __suseconds_t suseconds_t;
502typedef long int __fd_mask;
503typedef struct
504 {
505 __fd_mask __fds_bits[1024 / (8 * (int) sizeof (__fd_mask))];
506 } fd_set;
507typedef __fd_mask fd_mask;
508
509extern int select (int __nfds, fd_set *__restrict __readfds,
510 fd_set *__restrict __writefds,
511 fd_set *__restrict __exceptfds,
512 struct timeval *__restrict __timeout);
513extern int pselect (int __nfds, fd_set *__restrict __readfds,
514 fd_set *__restrict __writefds,
515 fd_set *__restrict __exceptfds,
516 const struct timespec *__restrict __timeout,
517 const __sigset_t *__restrict __sigmask);
518
519
520__extension__
521extern unsigned int gnu_dev_major (unsigned long long int __dev)
522 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
523__extension__
524extern unsigned int gnu_dev_minor (unsigned long long int __dev)
525 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
526__extension__
527extern unsigned long long int gnu_dev_makedev (unsigned int __major,
528 unsigned int __minor)
529 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
530
531typedef __blksize_t blksize_t;
532typedef __blkcnt_t blkcnt_t;
533typedef __fsblkcnt_t fsblkcnt_t;
534typedef __fsfilcnt_t fsfilcnt_t;
535typedef unsigned long int pthread_t;
536union pthread_attr_t
537{
538 char __size[36];
539 long int __align;
540};
541typedef union pthread_attr_t pthread_attr_t;
542typedef struct __pthread_internal_slist
543{
544 struct __pthread_internal_slist *__next;
545} __pthread_slist_t;
546typedef union
547{
548 struct __pthread_mutex_s
549 {
550 int __lock;
551 unsigned int __count;
552 int __owner;
553 int __kind;
554 unsigned int __nusers;
555 __extension__ union
556 {
557 struct
558 {
559 short __espins;
560 short __elision;
561 } __elision_data;
562 __pthread_slist_t __list;
563 };
564 } __data;
565 char __size[24];
566 long int __align;
567} pthread_mutex_t;
568typedef union
569{
570 char __size[4];
571 int __align;
572} pthread_mutexattr_t;
573typedef union
574{
575 struct
576 {
577 int __lock;
578 unsigned int __futex;
579 __extension__ unsigned long long int __total_seq;
580 __extension__ unsigned long long int __wakeup_seq;
581 __extension__ unsigned long long int __woken_seq;
582 void *__mutex;
583 unsigned int __nwaiters;
584 unsigned int __broadcast_seq;
585 } __data;
586 char __size[48];
587 __extension__ long long int __align;
588} pthread_cond_t;
589typedef union
590{
591 char __size[4];
592 int __align;
593} pthread_condattr_t;
594typedef unsigned int pthread_key_t;
595typedef int pthread_once_t;
596typedef union
597{
598 struct
599 {
600 int __lock;
601 unsigned int __nr_readers;
602 unsigned int __readers_wakeup;
603 unsigned int __writer_wakeup;
604 unsigned int __nr_readers_queued;
605 unsigned int __nr_writers_queued;
606 unsigned char __flags;
607 unsigned char __shared;
608 signed char __rwelision;
609 unsigned char __pad2;
610 int __writer;
611 } __data;
612 char __size[32];
613 long int __align;
614} pthread_rwlock_t;
615typedef union
616{
617 char __size[8];
618 long int __align;
619} pthread_rwlockattr_t;
620typedef volatile int pthread_spinlock_t;
621typedef union
622{
623 char __size[20];
624 long int __align;
625} pthread_barrier_t;
626typedef union
627{
628 char __size[4];
629 int __align;
630} pthread_barrierattr_t;
631
632extern long int random (void) __attribute__ ((__nothrow__ , __leaf__));
633extern void srandom (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));
634extern char *initstate (unsigned int __seed, char *__statebuf,
635 size_t __statelen) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
636extern char *setstate (char *__statebuf) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
637struct random_data
638 {
639 int32_t *fptr;
640 int32_t *rptr;
641 int32_t *state;
642 int rand_type;
643 int rand_deg;
644 int rand_sep;
645 int32_t *end_ptr;
646 };
647extern int random_r (struct random_data *__restrict __buf,
648 int32_t *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
649extern int srandom_r (unsigned int __seed, struct random_data *__buf)
650 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
651extern int initstate_r (unsigned int __seed, char *__restrict __statebuf,
652 size_t __statelen,
653 struct random_data *__restrict __buf)
654 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 4)));
655extern int setstate_r (char *__restrict __statebuf,
656 struct random_data *__restrict __buf)
657 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
658
659extern int rand (void) __attribute__ ((__nothrow__ , __leaf__));
660extern void srand (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));
661
662extern int rand_r (unsigned int *__seed) __attribute__ ((__nothrow__ , __leaf__));
663extern double drand48 (void) __attribute__ ((__nothrow__ , __leaf__));
664extern double erand48 (unsigned short int __xsubi[3]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
665extern long int lrand48 (void) __attribute__ ((__nothrow__ , __leaf__));
666extern long int nrand48 (unsigned short int __xsubi[3])
667 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
668extern long int mrand48 (void) __attribute__ ((__nothrow__ , __leaf__));
669extern long int jrand48 (unsigned short int __xsubi[3])
670 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
671extern void srand48 (long int __seedval) __attribute__ ((__nothrow__ , __leaf__));
672extern unsigned short int *seed48 (unsigned short int __seed16v[3])
673 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
674extern void lcong48 (unsigned short int __param[7]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
675struct drand48_data
676 {
677 unsigned short int __x[3];
678 unsigned short int __old_x[3];
679 unsigned short int __c;
680 unsigned short int __init;
681 __extension__ unsigned long long int __a;
682 };
683extern int drand48_r (struct drand48_data *__restrict __buffer,
684 double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
685extern int erand48_r (unsigned short int __xsubi[3],
686 struct drand48_data *__restrict __buffer,
687 double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
688extern int lrand48_r (struct drand48_data *__restrict __buffer,
689 long int *__restrict __result)
690 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
691extern int nrand48_r (unsigned short int __xsubi[3],
692 struct drand48_data *__restrict __buffer,
693 long int *__restrict __result)
694 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
695extern int mrand48_r (struct drand48_data *__restrict __buffer,
696 long int *__restrict __result)
697 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
698extern int jrand48_r (unsigned short int __xsubi[3],
699 struct drand48_data *__restrict __buffer,
700 long int *__restrict __result)
701 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
702extern int srand48_r (long int __seedval, struct drand48_data *__buffer)
703 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
704extern int seed48_r (unsigned short int __seed16v[3],
705 struct drand48_data *__buffer) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
706extern int lcong48_r (unsigned short int __param[7],
707 struct drand48_data *__buffer)
708 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
709
710extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
711extern void *calloc (size_t __nmemb, size_t __size)
712 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
713
714
715extern void *realloc (void *__ptr, size_t __size)
716 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__warn_unused_result__));
717extern void free (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));
718
719extern void cfree (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));
720
721extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__));
722
723extern void *valloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
724extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size)
725 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
726extern void *aligned_alloc (size_t __alignment, size_t __size)
727 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) __attribute__ ((__alloc_size__ (2))) ;
728
729extern void abort (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
730extern int atexit (void (*__func) (void)) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
731extern int at_quick_exit (void (*__func) (void)) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
732
733extern int on_exit (void (*__func) (int __status, void *__arg), void *__arg)
734 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
735
736extern void exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
737extern void quick_exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
738
739
740extern void _Exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
741
742
743extern char *getenv (const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
744
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)));
766extern int abs (int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
767extern long int labs (long int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
768
769__extension__ extern long long int llabs (long long int __x)
770 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
771
772extern div_t div (int __numer, int __denom)
773 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
774extern ldiv_t ldiv (long int __numer, long int __denom)
775 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
776
777
778__extension__ extern lldiv_t lldiv (long long int __numer,
779 long long int __denom)
780 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;
781
782extern char *ecvt (double __value, int __ndigit, int *__restrict __decpt,
783 int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
784extern char *fcvt (double __value, int __ndigit, int *__restrict __decpt,
785 int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
786extern char *gcvt (double __value, int __ndigit, char *__buf)
787 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;
788extern char *qecvt (long double __value, int __ndigit,
789 int *__restrict __decpt, int *__restrict __sign)
790 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
791extern char *qfcvt (long double __value, int __ndigit,
792 int *__restrict __decpt, int *__restrict __sign)
793 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;
794extern char *qgcvt (long double __value, int __ndigit, char *__buf)
795 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;
796extern int ecvt_r (double __value, int __ndigit, int *__restrict __decpt,
797 int *__restrict __sign, char *__restrict __buf,
798 size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
799extern int fcvt_r (double __value, int __ndigit, int *__restrict __decpt,
800 int *__restrict __sign, char *__restrict __buf,
801 size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
802extern int qecvt_r (long double __value, int __ndigit,
803 int *__restrict __decpt, int *__restrict __sign,
804 char *__restrict __buf, size_t __len)
805 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
806extern int qfcvt_r (long double __value, int __ndigit,
807 int *__restrict __decpt, int *__restrict __sign,
808 char *__restrict __buf, size_t __len)
809 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));
810
811extern int mblen (const char *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
812extern int mbtowc (wchar_t *__restrict __pwc,
813 const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
814extern int wctomb (char *__s, wchar_t __wchar) __attribute__ ((__nothrow__ , __leaf__));
815extern size_t mbstowcs (wchar_t *__restrict __pwcs,
816 const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__));
817extern size_t wcstombs (char *__restrict __s,
818 const wchar_t *__restrict __pwcs, size_t __n)
819 __attribute__ ((__nothrow__ , __leaf__));
820
821extern int rpmatch (const char *__response) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;
822extern int getsubopt (char **__restrict __optionp,
823 char *const *__restrict __tokens,
824 char **__restrict __valuep)
825 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))) ;
826extern int getloadavg (double __loadavg[], int __nelem)
827 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
828
829struct sched_param
830 {
831 int __sched_priority;
832 };
833
834
835struct __sched_param
836 {
837 int __sched_priority;
838 };
839typedef unsigned long int __cpu_mask;
840typedef struct
841{
842 __cpu_mask __bits[1024 / (8 * sizeof (__cpu_mask))];
843} cpu_set_t;
844
845extern int __sched_cpucount (size_t __setsize, const cpu_set_t *__setp)
846 __attribute__ ((__nothrow__ , __leaf__));
847extern cpu_set_t *__sched_cpualloc (size_t __count) __attribute__ ((__nothrow__ , __leaf__)) ;
848extern void __sched_cpufree (cpu_set_t *__set) __attribute__ ((__nothrow__ , __leaf__));
849
850
851extern int sched_setparam (__pid_t __pid, const struct sched_param *__param)
852 __attribute__ ((__nothrow__ , __leaf__));
853extern int sched_getparam (__pid_t __pid, struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__));
854extern int sched_setscheduler (__pid_t __pid, int __policy,
855 const struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__));
856extern int sched_getscheduler (__pid_t __pid) __attribute__ ((__nothrow__ , __leaf__));
857extern int sched_yield (void) __attribute__ ((__nothrow__ , __leaf__));
858extern int sched_get_priority_max (int __algorithm) __attribute__ ((__nothrow__ , __leaf__));
859extern int sched_get_priority_min (int __algorithm) __attribute__ ((__nothrow__ , __leaf__));
860extern int sched_rr_get_interval (__pid_t __pid, struct timespec *__t) __attribute__ ((__nothrow__ , __leaf__));
861
862
863
864struct tm
865{
866 int tm_sec;
867 int tm_min;
868 int tm_hour;
869 int tm_mday;
870 int tm_mon;
871 int tm_year;
872 int tm_wday;
873 int tm_yday;
874 int tm_isdst;
875 long int tm_gmtoff;
876 const char *tm_zone;
877};
878
879
880struct itimerspec
881 {
882 struct timespec it_interval;
883 struct timespec it_value;
884 };
885struct sigevent;
886
887extern clock_t clock (void) __attribute__ ((__nothrow__ , __leaf__));
888extern time_t time (time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
889extern double difftime (time_t __time1, time_t __time0)
890 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
891extern time_t mktime (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
892extern size_t strftime (char *__restrict __s, size_t __maxsize,
893 const char *__restrict __format,
894 const struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__));
895
896typedef struct __locale_struct
897{
898 struct __locale_data *__locales[13];
899 const unsigned short int *__ctype_b;
900 const int *__ctype_tolower;
901 const int *__ctype_toupper;
902 const char *__names[13];
903} *__locale_t;
904typedef __locale_t locale_t;
905extern size_t strftime_l (char *__restrict __s, size_t __maxsize,
906 const char *__restrict __format,
907 const struct tm *__restrict __tp,
908 __locale_t __loc) __attribute__ ((__nothrow__ , __leaf__));
909
910extern struct tm *gmtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
911extern struct tm *localtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
912
913extern struct tm *gmtime_r (const time_t *__restrict __timer,
914 struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__));
915extern struct tm *localtime_r (const time_t *__restrict __timer,
916 struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__));
917
918extern char *asctime (const struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
919extern char *ctime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
920
921extern char *asctime_r (const struct tm *__restrict __tp,
922 char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__));
923extern char *ctime_r (const time_t *__restrict __timer,
924 char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__));
925extern char *__tzname[2];
926extern int __daylight;
927extern long int __timezone;
928extern char *tzname[2];
929extern void tzset (void) __attribute__ ((__nothrow__ , __leaf__));
930extern int daylight;
931extern long int timezone;
932extern int stime (const time_t *__when) __attribute__ ((__nothrow__ , __leaf__));
933extern time_t timegm (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
934extern time_t timelocal (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
935extern int dysize (int __year) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
936extern int nanosleep (const struct timespec *__requested_time,
937 struct timespec *__remaining);
938extern int clock_getres (clockid_t __clock_id, struct timespec *__res) __attribute__ ((__nothrow__ , __leaf__));
939extern int clock_gettime (clockid_t __clock_id, struct timespec *__tp) __attribute__ ((__nothrow__ , __leaf__));
940extern int clock_settime (clockid_t __clock_id, const struct timespec *__tp)
941 __attribute__ ((__nothrow__ , __leaf__));
942extern int clock_nanosleep (clockid_t __clock_id, int __flags,
943 const struct timespec *__req,
944 struct timespec *__rem);
945extern int clock_getcpuclockid (pid_t __pid, clockid_t *__clock_id) __attribute__ ((__nothrow__ , __leaf__));
946extern int timer_create (clockid_t __clock_id,
947 struct sigevent *__restrict __evp,
948 timer_t *__restrict __timerid) __attribute__ ((__nothrow__ , __leaf__));
949extern int timer_delete (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__));
950extern int timer_settime (timer_t __timerid, int __flags,
951 const struct itimerspec *__restrict __value,
952 struct itimerspec *__restrict __ovalue) __attribute__ ((__nothrow__ , __leaf__));
953extern int timer_gettime (timer_t __timerid, struct itimerspec *__value)
954 __attribute__ ((__nothrow__ , __leaf__));
955extern int timer_getoverrun (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__));
956extern int timespec_get (struct timespec *__ts, int __base)
957 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
958
959typedef int __jmp_buf[6];
960enum
961{
962 PTHREAD_CREATE_JOINABLE,
963 PTHREAD_CREATE_DETACHED
964};
965enum
966{
967 PTHREAD_MUTEX_TIMED_NP,
968 PTHREAD_MUTEX_RECURSIVE_NP,
969 PTHREAD_MUTEX_ERRORCHECK_NP,
970 PTHREAD_MUTEX_ADAPTIVE_NP
971 ,
972 PTHREAD_MUTEX_NORMAL = PTHREAD_MUTEX_TIMED_NP,
973 PTHREAD_MUTEX_RECURSIVE = PTHREAD_MUTEX_RECURSIVE_NP,
974 PTHREAD_MUTEX_ERRORCHECK = PTHREAD_MUTEX_ERRORCHECK_NP,
975 PTHREAD_MUTEX_DEFAULT = PTHREAD_MUTEX_NORMAL
976};
977enum
978{
979 PTHREAD_MUTEX_STALLED,
980 PTHREAD_MUTEX_STALLED_NP = PTHREAD_MUTEX_STALLED,
981 PTHREAD_MUTEX_ROBUST,
982 PTHREAD_MUTEX_ROBUST_NP = PTHREAD_MUTEX_ROBUST
983};
984enum
985{
986 PTHREAD_PRIO_NONE,
987 PTHREAD_PRIO_INHERIT,
988 PTHREAD_PRIO_PROTECT
989};
990enum
991{
992 PTHREAD_RWLOCK_PREFER_READER_NP,
993 PTHREAD_RWLOCK_PREFER_WRITER_NP,
994 PTHREAD_RWLOCK_PREFER_WRITER_NONRECURSIVE_NP,
995 PTHREAD_RWLOCK_DEFAULT_NP = PTHREAD_RWLOCK_PREFER_READER_NP
996};
997enum
998{
999 PTHREAD_INHERIT_SCHED,
1000 PTHREAD_EXPLICIT_SCHED
1001};
1002enum
1003{
1004 PTHREAD_SCOPE_SYSTEM,
1005 PTHREAD_SCOPE_PROCESS
1006};
1007enum
1008{
1009 PTHREAD_PROCESS_PRIVATE,
1010 PTHREAD_PROCESS_SHARED
1011};
1012struct _pthread_cleanup_buffer
1013{
1014 void (*__routine) (void *);
1015 void *__arg;
1016 int __canceltype;
1017 struct _pthread_cleanup_buffer *__prev;
1018};
1019enum
1020{
1021 PTHREAD_CANCEL_ENABLE,
1022 PTHREAD_CANCEL_DISABLE
1023};
1024enum
1025{
1026 PTHREAD_CANCEL_DEFERRED,
1027 PTHREAD_CANCEL_ASYNCHRONOUS
1028};
1029
1030extern int pthread_create (pthread_t *__restrict __newthread,
1031 const pthread_attr_t *__restrict __attr,
1032 void *(*__start_routine) (void *),
1033 void *__restrict __arg) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 3)));
1034extern void pthread_exit (void *__retval) __attribute__ ((__noreturn__));
1035extern int pthread_join (pthread_t __th, void **__thread_return);
1036extern int pthread_detach (pthread_t __th) __attribute__ ((__nothrow__ , __leaf__));
1037extern pthread_t pthread_self (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
1038extern int pthread_equal (pthread_t __thread1, pthread_t __thread2)
1039 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
1040extern int pthread_attr_init (pthread_attr_t *__attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1041extern int pthread_attr_destroy (pthread_attr_t *__attr)
1042 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1043extern int pthread_attr_getdetachstate (const pthread_attr_t *__attr,
1044 int *__detachstate)
1045 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1046extern int pthread_attr_setdetachstate (pthread_attr_t *__attr,
1047 int __detachstate)
1048 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1049extern int pthread_attr_getguardsize (const pthread_attr_t *__attr,
1050 size_t *__guardsize)
1051 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1052extern int pthread_attr_setguardsize (pthread_attr_t *__attr,
1053 size_t __guardsize)
1054 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1055extern int pthread_attr_getschedparam (const pthread_attr_t *__restrict __attr,
1056 struct sched_param *__restrict __param)
1057 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1058extern int pthread_attr_setschedparam (pthread_attr_t *__restrict __attr,
1059 const struct sched_param *__restrict
1060 __param) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1061extern int pthread_attr_getschedpolicy (const pthread_attr_t *__restrict
1062 __attr, int *__restrict __policy)
1063 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1064extern int pthread_attr_setschedpolicy (pthread_attr_t *__attr, int __policy)
1065 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1066extern int pthread_attr_getinheritsched (const pthread_attr_t *__restrict
1067 __attr, int *__restrict __inherit)
1068 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1069extern int pthread_attr_setinheritsched (pthread_attr_t *__attr,
1070 int __inherit)
1071 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1072extern int pthread_attr_getscope (const pthread_attr_t *__restrict __attr,
1073 int *__restrict __scope)
1074 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1075extern int pthread_attr_setscope (pthread_attr_t *__attr, int __scope)
1076 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1077extern int pthread_attr_getstackaddr (const pthread_attr_t *__restrict
1078 __attr, void **__restrict __stackaddr)
1079 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))) __attribute__ ((__deprecated__));
1080extern int pthread_attr_setstackaddr (pthread_attr_t *__attr,
1081 void *__stackaddr)
1082 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) __attribute__ ((__deprecated__));
1083extern int pthread_attr_getstacksize (const pthread_attr_t *__restrict
1084 __attr, size_t *__restrict __stacksize)
1085 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1086extern int pthread_attr_setstacksize (pthread_attr_t *__attr,
1087 size_t __stacksize)
1088 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1089extern int pthread_attr_getstack (const pthread_attr_t *__restrict __attr,
1090 void **__restrict __stackaddr,
1091 size_t *__restrict __stacksize)
1092 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3)));
1093extern int pthread_attr_setstack (pthread_attr_t *__attr, void *__stackaddr,
1094 size_t __stacksize) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1095extern int pthread_setschedparam (pthread_t __target_thread, int __policy,
1096 const struct sched_param *__param)
1097 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3)));
1098extern int pthread_getschedparam (pthread_t __target_thread,
1099 int *__restrict __policy,
1100 struct sched_param *__restrict __param)
1101 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 3)));
1102extern int pthread_setschedprio (pthread_t __target_thread, int __prio)
1103 __attribute__ ((__nothrow__ , __leaf__));
1104extern int pthread_once (pthread_once_t *__once_control,
1105 void (*__init_routine) (void)) __attribute__ ((__nonnull__ (1, 2)));
1106extern int pthread_setcancelstate (int __state, int *__oldstate);
1107extern int pthread_setcanceltype (int __type, int *__oldtype);
1108extern int pthread_cancel (pthread_t __th);
1109extern void pthread_testcancel (void);
1110typedef struct
1111{
1112 struct
1113 {
1114 __jmp_buf __cancel_jmp_buf;
1115 int __mask_was_saved;
1116 } __cancel_jmp_buf[1];
1117 void *__pad[4];
1118} __pthread_unwind_buf_t __attribute__ ((__aligned__));
1119struct __pthread_cleanup_frame
1120{
1121 void (*__cancel_routine) (void *);
1122 void *__cancel_arg;
1123 int __do_it;
1124 int __cancel_type;
1125};
1126extern void __pthread_register_cancel (__pthread_unwind_buf_t *__buf)
1127 __attribute__ ((__regparm__ (1)));
1128extern void __pthread_unregister_cancel (__pthread_unwind_buf_t *__buf)
1129 __attribute__ ((__regparm__ (1)));
1130extern void __pthread_unwind_next (__pthread_unwind_buf_t *__buf)
1131 __attribute__ ((__regparm__ (1))) __attribute__ ((__noreturn__))
1132 __attribute__ ((__weak__))
1133 ;
1134struct __jmp_buf_tag;
1135extern int __sigsetjmp (struct __jmp_buf_tag *__env, int __savemask) __attribute__ ((__nothrow__));
1136extern int pthread_mutex_init (pthread_mutex_t *__mutex,
1137 const pthread_mutexattr_t *__mutexattr)
1138 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1139extern int pthread_mutex_destroy (pthread_mutex_t *__mutex)
1140 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1141extern int pthread_mutex_trylock (pthread_mutex_t *__mutex)
1142 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1143extern int pthread_mutex_lock (pthread_mutex_t *__mutex)
1144 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1145extern int pthread_mutex_timedlock (pthread_mutex_t *__restrict __mutex,
1146 const struct timespec *__restrict
1147 __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
1148extern int pthread_mutex_unlock (pthread_mutex_t *__mutex)
1149 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1150extern int pthread_mutex_getprioceiling (const pthread_mutex_t *
1151 __restrict __mutex,
1152 int *__restrict __prioceiling)
1153 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1154extern int pthread_mutex_setprioceiling (pthread_mutex_t *__restrict __mutex,
1155 int __prioceiling,
1156 int *__restrict __old_ceiling)
1157 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 3)));
1158extern int pthread_mutex_consistent (pthread_mutex_t *__mutex)
1159 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1160extern int pthread_mutexattr_init (pthread_mutexattr_t *__attr)
1161 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1162extern int pthread_mutexattr_destroy (pthread_mutexattr_t *__attr)
1163 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1164extern int pthread_mutexattr_getpshared (const pthread_mutexattr_t *
1165 __restrict __attr,
1166 int *__restrict __pshared)
1167 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1168extern int pthread_mutexattr_setpshared (pthread_mutexattr_t *__attr,
1169 int __pshared)
1170 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1171extern int pthread_mutexattr_gettype (const pthread_mutexattr_t *__restrict
1172 __attr, int *__restrict __kind)
1173 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1174extern int pthread_mutexattr_settype (pthread_mutexattr_t *__attr, int __kind)
1175 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1176extern int pthread_mutexattr_getprotocol (const pthread_mutexattr_t *
1177 __restrict __attr,
1178 int *__restrict __protocol)
1179 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1180extern int pthread_mutexattr_setprotocol (pthread_mutexattr_t *__attr,
1181 int __protocol)
1182 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1183extern int pthread_mutexattr_getprioceiling (const pthread_mutexattr_t *
1184 __restrict __attr,
1185 int *__restrict __prioceiling)
1186 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1187extern int pthread_mutexattr_setprioceiling (pthread_mutexattr_t *__attr,
1188 int __prioceiling)
1189 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1190extern int pthread_mutexattr_getrobust (const pthread_mutexattr_t *__attr,
1191 int *__robustness)
1192 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1193extern int pthread_mutexattr_setrobust (pthread_mutexattr_t *__attr,
1194 int __robustness)
1195 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1196extern int pthread_rwlock_init (pthread_rwlock_t *__restrict __rwlock,
1197 const pthread_rwlockattr_t *__restrict
1198 __attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1199extern int pthread_rwlock_destroy (pthread_rwlock_t *__rwlock)
1200 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1201extern int pthread_rwlock_rdlock (pthread_rwlock_t *__rwlock)
1202 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1203extern int pthread_rwlock_tryrdlock (pthread_rwlock_t *__rwlock)
1204 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1205extern int pthread_rwlock_timedrdlock (pthread_rwlock_t *__restrict __rwlock,
1206 const struct timespec *__restrict
1207 __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
1208extern int pthread_rwlock_wrlock (pthread_rwlock_t *__rwlock)
1209 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1210extern int pthread_rwlock_trywrlock (pthread_rwlock_t *__rwlock)
1211 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1212extern int pthread_rwlock_timedwrlock (pthread_rwlock_t *__restrict __rwlock,
1213 const struct timespec *__restrict
1214 __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
1215extern int pthread_rwlock_unlock (pthread_rwlock_t *__rwlock)
1216 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1217extern int pthread_rwlockattr_init (pthread_rwlockattr_t *__attr)
1218 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1219extern int pthread_rwlockattr_destroy (pthread_rwlockattr_t *__attr)
1220 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1221extern int pthread_rwlockattr_getpshared (const pthread_rwlockattr_t *
1222 __restrict __attr,
1223 int *__restrict __pshared)
1224 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1225extern int pthread_rwlockattr_setpshared (pthread_rwlockattr_t *__attr,
1226 int __pshared)
1227 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1228extern int pthread_rwlockattr_getkind_np (const pthread_rwlockattr_t *
1229 __restrict __attr,
1230 int *__restrict __pref)
1231 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1232extern int pthread_rwlockattr_setkind_np (pthread_rwlockattr_t *__attr,
1233 int __pref) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1234extern int pthread_cond_init (pthread_cond_t *__restrict __cond,
1235 const pthread_condattr_t *__restrict __cond_attr)
1236 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1237extern int pthread_cond_destroy (pthread_cond_t *__cond)
1238 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1239extern int pthread_cond_signal (pthread_cond_t *__cond)
1240 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1241extern int pthread_cond_broadcast (pthread_cond_t *__cond)
1242 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1243extern int pthread_cond_wait (pthread_cond_t *__restrict __cond,
1244 pthread_mutex_t *__restrict __mutex)
1245 __attribute__ ((__nonnull__ (1, 2)));
1246extern int pthread_cond_timedwait (pthread_cond_t *__restrict __cond,
1247 pthread_mutex_t *__restrict __mutex,
1248 const struct timespec *__restrict __abstime)
1249 __attribute__ ((__nonnull__ (1, 2, 3)));
1250extern int pthread_condattr_init (pthread_condattr_t *__attr)
1251 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1252extern int pthread_condattr_destroy (pthread_condattr_t *__attr)
1253 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1254extern int pthread_condattr_getpshared (const pthread_condattr_t *
1255 __restrict __attr,
1256 int *__restrict __pshared)
1257 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1258extern int pthread_condattr_setpshared (pthread_condattr_t *__attr,
1259 int __pshared) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1260extern int pthread_condattr_getclock (const pthread_condattr_t *
1261 __restrict __attr,
1262 __clockid_t *__restrict __clock_id)
1263 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1264extern int pthread_condattr_setclock (pthread_condattr_t *__attr,
1265 __clockid_t __clock_id)
1266 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1267extern int pthread_spin_init (pthread_spinlock_t *__lock, int __pshared)
1268 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1269extern int pthread_spin_destroy (pthread_spinlock_t *__lock)
1270 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1271extern int pthread_spin_lock (pthread_spinlock_t *__lock)
1272 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1273extern int pthread_spin_trylock (pthread_spinlock_t *__lock)
1274 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1275extern int pthread_spin_unlock (pthread_spinlock_t *__lock)
1276 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1277extern int pthread_barrier_init (pthread_barrier_t *__restrict __barrier,
1278 const pthread_barrierattr_t *__restrict
1279 __attr, unsigned int __count)
1280 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1281extern int pthread_barrier_destroy (pthread_barrier_t *__barrier)
1282 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1283extern int pthread_barrier_wait (pthread_barrier_t *__barrier)
1284 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1285extern int pthread_barrierattr_init (pthread_barrierattr_t *__attr)
1286 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1287extern int pthread_barrierattr_destroy (pthread_barrierattr_t *__attr)
1288 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1289extern int pthread_barrierattr_getpshared (const pthread_barrierattr_t *
1290 __restrict __attr,
1291 int *__restrict __pshared)
1292 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
1293extern int pthread_barrierattr_setpshared (pthread_barrierattr_t *__attr,
1294 int __pshared)
1295 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1296extern int pthread_key_create (pthread_key_t *__key,
1297 void (*__destr_function) (void *))
1298 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
1299extern int pthread_key_delete (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__));
1300extern void *pthread_getspecific (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__));
1301extern int pthread_setspecific (pthread_key_t __key,
1302 const void *__pointer) __attribute__ ((__nothrow__ , __leaf__)) ;
1303extern int pthread_getcpuclockid (pthread_t __thread_id,
1304 __clockid_t *__clock_id)
1305 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
1306extern int pthread_atfork (void (*__prepare) (void),
1307 void (*__parent) (void),
1308 void (*__child) (void)) __attribute__ ((__nothrow__ , __leaf__));
1309
1310extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1311extern int __VERIFIER_nondet_int(void);
1312extern void __VERIFIER_assume(int);
1313extern void __VERIFIER_atomic_begin(void);
1314extern void __VERIFIER_atomic_end(void);
1315typedef struct Cell Cell;
1316struct Cell {
1317 Cell *pnext;
1318 int pdata;
1319};
1320typedef struct ThreadInfo ThreadInfo;
1321struct ThreadInfo {
1322 unsigned int id;
1323 int op;
1324 Cell cell;
1325};
1326typedef struct Simple_Stack Simple_Stack;
1327struct Simple_Stack {
1328 Cell *ptop;
1329};
1330Simple_Stack S;
1331ThreadInfo *location[8];
1332int collision;
1333int unique_id = 0;
1334void StackOp(ThreadInfo *p);
1335int TryPerformStackOp(ThreadInfo *p);
1336int TryCollision(ThreadInfo * p, ThreadInfo * q, int him);
1337void FinishCollision(ThreadInfo * p);
1338int atomic_int_cas(int *p, int cmp, int new) {
1339 int ret;
1340 __VERIFIER_atomic_begin();
1341 if (*p == cmp) {
1342 *p = new;
1343 ret = 1;
1344 } else {
1345 ret = 0;
1346 }
1347 __VERIFIER_atomic_end();
1348 return ret;
1349}
1350int atomic_ti_cas(ThreadInfo * *p, ThreadInfo* cmp, ThreadInfo* new) {
1351 int ret;
1352 __VERIFIER_atomic_begin();
1353 if (*p == cmp) {
1354 *p = new;
1355 ret = 1;
1356 } else {
1357 ret = 0;
1358 }
1359 __VERIFIER_atomic_end();
1360 return ret;
1361}
1362int ti_cas(ThreadInfo * *p, ThreadInfo* cmp, ThreadInfo* new) {
1363 if (*p == cmp) {
1364 *p = new;
1365 return 1;
1366 } else {
1367 return 0;
1368 }
1369}
1370int atomic_c_cas(Cell * *p, Cell* cmp, Cell* new) {
1371 int ret;
1372 __VERIFIER_atomic_begin();
1373 if (*p == cmp) {
1374 *p = new;
1375 ret = 1;
1376 } else {
1377 ret = 0;
1378 }
1379 __VERIFIER_atomic_end();
1380 return ret;
1381}
1382ThreadInfo threads[4];
1383int allocated[4];
1384ThreadInfo* malloc_ThreadInfo() {
1385 __VERIFIER_atomic_begin();
1386 int i = __VERIFIER_nondet_int();
1387 __VERIFIER_assume(0 <= i && i < 4);
1388 __VERIFIER_assume(!allocated[i]);
1389 allocated[i] = 1;
1390 __VERIFIER_atomic_end();
1391 return &threads[i];
1392}
1393void free_ThreadInfo(ThreadInfo* ti) {
1394 __VERIFIER_atomic_begin();
1395 int i = __VERIFIER_nondet_int();
1396 __VERIFIER_assume(0 <= i && i < 4);
1397 __VERIFIER_assume(&threads[i] == ti);
1398 allocated[i] = 0;
1399 __VERIFIER_atomic_end();
1400}
1401void LesOP(ThreadInfo *p) {
1402 int mypid = p->id;
1403 location[mypid] = p;
1404 int him = collision;
1405 __VERIFIER_assume (atomic_int_cas(&collision, him, mypid));
1406 if (him > 0) {
1407 ThreadInfo* q = location[him];
1408 if (q != ((void *)0) && q->id == him && q->op != p->op) {
1409 if (atomic_ti_cas(&location[mypid], p, ((void *)0))) {
1410 if (TryCollision(p, q, him) == 1) {
1411 return;
1412 } else {
1413 goto stack;
1414 }
1415 } else {
1416 FinishCollision(p);
1417 return;
1418 }
1419 }
1420 }
1421 if (!atomic_ti_cas(&location[mypid], p, ((void *)0))) {
1422 FinishCollision(p);
1423 return;
1424 }
1425stack:
1426 if (TryPerformStackOp(p) == 1) {
1427 return;
1428 }
1429 __VERIFIER_assume(0);
1430}
1431int TryPerformStackOp(ThreadInfo * p) {
1432 Cell *phead, *pnext;
1433 if (p->op == 1) {
1434 phead = S.ptop;
1435 p->cell.pnext = phead;
1436 if (atomic_c_cas(&S.ptop, phead, &p->cell)) {
1437 return 1;
1438 } else {
1439 return 0;
1440 }
1441 }
1442 if (p->op == 0) {
1443 phead = S.ptop;
1444 if (phead == ((void *)0)) {
1445 p->cell.pnext = 0; p->cell.pdata = 2;
1446 return 1;
1447 }
1448 pnext = phead->pnext;
1449 if (atomic_c_cas(&S.ptop, phead, pnext)) {
1450 p->cell = *phead;
1451 __VERIFIER_atomic_begin();
1452 int i = __VERIFIER_nondet_int();
1453 __VERIFIER_assume(0 <= i && i < 4);
1454 __VERIFIER_assume(&threads[i].cell == phead);
1455 allocated[i] = 0;
1456 __VERIFIER_atomic_end();
1457 return 1;
1458 } else {
1459 p->cell.pnext = 0; p->cell.pdata = 2;
1460 return 0;
1461 }
1462 }
1463}
1464void FinishCollision(ThreadInfo * p) {
1465 __VERIFIER_atomic_begin();
1466 if (p->op == 0) {
1467 int mypid = p->id;
1468 p->cell = location[mypid]->cell;
1469 location[mypid] = ((void *)0);
1470 }
1471 __VERIFIER_atomic_end();
1472}
1473int TryCollision(ThreadInfo * p, ThreadInfo * q, int him) {
1474 int ret = 0;
1475 __VERIFIER_atomic_begin();
1476 int mypid = p->id;
1477 if (p->op == 1) {
1478 if (ti_cas(&location[him], q, p)) {
1479 ret = 1;
1480 } else {
1481 ret = 0;
1482 }
1483 }
1484 if (p->op == 0) {
1485 if (ti_cas(&location[him], q, ((void *)0))) {
1486 p->cell = q->cell;
1487 location[mypid] = ((void *)0);
1488 ret = 1;
1489 } else {
1490 ret = 0;
1491 }
1492 }
1493 __VERIFIER_atomic_end();
1494 return ret;
1495}
1496void Init() {
1497 S.ptop = ((void *)0);
1498}
1499void Push(int x) {
1500 ThreadInfo *ti = malloc_ThreadInfo();
1501 ti->id = ++unique_id;
1502 ti->op = 1;
1503 ti->cell.pdata = x;
1504 if (TryPerformStackOp(ti) == 0) {
1505 LesOP(ti);
1506 }
1507}
1508int Pop() {
1509 ThreadInfo *ti = malloc_ThreadInfo();
1510 ti->id = ++unique_id;
1511 ti->op = 0;
1512 if (TryPerformStackOp(ti) == 0) {
1513 LesOP(ti);
1514 }
1515 int v = ti->cell.pdata;
1516 free_ThreadInfo(ti);
1517 return v;
1518}
1519int PushOpen[2];
1520int PushDone[2];
1521int PopOpen;
1522int PopDone[3];
1523void checkInvariant() {
1524 if (!(PopDone[0] <= PushDone[0] + PushOpen[0] && PopDone[1] <= PushDone[1] + PushOpen[1])) __VERIFIER_error();
1525}
1526void Incr_Push(int localPush1) {
1527 __VERIFIER_atomic_begin();
1528 PushOpen[localPush1]++;
1529 __VERIFIER_atomic_end();
1530}
1531void DecrIncr_Push(int localPush1) {
1532 __VERIFIER_atomic_begin();
1533 PushOpen[localPush1]--;
1534 PushDone[localPush1]++;
1535 checkInvariant();
1536 __VERIFIER_atomic_end();
1537}
1538void Incr_Pop() {
1539 __VERIFIER_atomic_begin();
1540 PopOpen++;
1541 __VERIFIER_atomic_end();
1542}
1543void DecrIncr_Pop(int localPop_ret) {
1544 __VERIFIER_atomic_begin();
1545 PopOpen--;
1546 PopDone[localPop_ret]++;
1547 checkInvariant();
1548 __VERIFIER_atomic_end();
1549}
1550void* instrPush0(void* unused) {
1551 Incr_Push(1);
1552 Push(1);
1553 DecrIncr_Push(1);
1554 return ((void *)0);
1555}
1556void* instrPush1(void* unused) {
1557 Incr_Push(1);
1558 Push(1);
1559 DecrIncr_Push(1);
1560 return ((void *)0);
1561}
1562void* instrPush2(void* unused) {
1563 Incr_Push(1);
1564 Push(1);
1565 DecrIncr_Push(1);
1566 return ((void *)0);
1567}
1568void* instrPop3(void* unused) {
1569 Incr_Pop();
1570 int localPop_ret = Pop();
1571 DecrIncr_Pop(localPop_ret);
1572 return ((void *)0);
1573}
1574void* instrPop4(void* unused) {
1575 Incr_Pop();
1576 int localPop_ret = Pop();
1577 DecrIncr_Pop(localPop_ret);
1578 return ((void *)0);
1579}
1580void* instrPop5(void* unused) {
1581 Incr_Pop();
1582 int localPop_ret = Pop();
1583 DecrIncr_Pop(localPop_ret);
1584 return ((void *)0);
1585}
1586void* instrPop6(void* unused) {
1587 Incr_Pop();
1588 int localPop_ret = Pop();
1589 DecrIncr_Pop(localPop_ret);
1590 return ((void *)0);
1591}
1592int main(void) {
1593 Init();
1594 pthread_t tid1, tid2, tid3, tid4, tid5, tid6, tid7;
1595 pthread_create(&tid1, ((void *)0), &instrPush0, ((void *)0));
1596 pthread_create(&tid2, ((void *)0), &instrPush1, ((void *)0));
1597 pthread_create(&tid3, ((void *)0), &instrPush2, ((void *)0));
1598 pthread_create(&tid4, ((void *)0), &instrPop3, ((void *)0));
1599 pthread_create(&tid5, ((void *)0), &instrPop4, ((void *)0));
1600 pthread_create(&tid6, ((void *)0), &instrPop5, ((void *)0));
1601 pthread_create(&tid7, ((void *)0), &instrPop6, ((void *)0));
1602 return 0;
1603}
Note: See TracBrowser for help on using the repository browser.