source: CIVL/examples/pthread/svcomp/stack_longest_true-unreach-call.i@ bb03188

main test-branch
Last change on this file since bb03188 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: 37.9 KB
Line 
1extern void __VERIFIER_error() __attribute__ ((__noreturn__));
2typedef unsigned char __u_char;
3typedef unsigned short int __u_short;
4typedef unsigned int __u_int;
5typedef unsigned long int __u_long;
6typedef signed char __int8_t;
7typedef unsigned char __uint8_t;
8typedef signed short int __int16_t;
9typedef unsigned short int __uint16_t;
10typedef signed int __int32_t;
11typedef unsigned int __uint32_t;
12typedef signed long int __int64_t;
13typedef unsigned long int __uint64_t;
14typedef long int __quad_t;
15typedef unsigned long int __u_quad_t;
16typedef unsigned long int __dev_t;
17typedef unsigned int __uid_t;
18typedef unsigned int __gid_t;
19typedef unsigned long int __ino_t;
20typedef unsigned long int __ino64_t;
21typedef unsigned int __mode_t;
22typedef unsigned long int __nlink_t;
23typedef long int __off_t;
24typedef long int __off64_t;
25typedef int __pid_t;
26typedef struct { int __val[2]; } __fsid_t;
27typedef long int __clock_t;
28typedef unsigned long int __rlim_t;
29typedef unsigned long int __rlim64_t;
30typedef unsigned int __id_t;
31typedef long int __time_t;
32typedef unsigned int __useconds_t;
33typedef long int __suseconds_t;
34typedef int __daddr_t;
35typedef long int __swblk_t;
36typedef int __key_t;
37typedef int __clockid_t;
38typedef void * __timer_t;
39typedef long int __blksize_t;
40typedef long int __blkcnt_t;
41typedef long int __blkcnt64_t;
42typedef unsigned long int __fsblkcnt_t;
43typedef unsigned long int __fsblkcnt64_t;
44typedef unsigned long int __fsfilcnt_t;
45typedef unsigned long int __fsfilcnt64_t;
46typedef long int __ssize_t;
47typedef __off64_t __loff_t;
48typedef __quad_t *__qaddr_t;
49typedef char *__caddr_t;
50typedef long int __intptr_t;
51typedef unsigned int __socklen_t;
52typedef long unsigned int size_t;
53
54typedef __time_t time_t;
55
56
57struct timespec
58 {
59 __time_t tv_sec;
60 long int tv_nsec;
61 };
62typedef __pid_t pid_t;
63struct sched_param
64 {
65 int __sched_priority;
66 };
67
68
69struct __sched_param
70 {
71 int __sched_priority;
72 };
73typedef unsigned long int __cpu_mask;
74typedef struct
75{
76 __cpu_mask __bits[1024 / (8 * sizeof (__cpu_mask))];
77} cpu_set_t;
78
79extern int __sched_cpucount (size_t __setsize, const cpu_set_t *__setp)
80 __attribute__ ((__nothrow__));
81extern cpu_set_t *__sched_cpualloc (size_t __count) __attribute__ ((__nothrow__)) ;
82extern void __sched_cpufree (cpu_set_t *__set) __attribute__ ((__nothrow__));
83
84
85extern int sched_setparam (__pid_t __pid, __const struct sched_param *__param)
86 __attribute__ ((__nothrow__));
87extern int sched_getparam (__pid_t __pid, struct sched_param *__param) __attribute__ ((__nothrow__));
88extern int sched_setscheduler (__pid_t __pid, int __policy,
89 __const struct sched_param *__param) __attribute__ ((__nothrow__));
90extern int sched_getscheduler (__pid_t __pid) __attribute__ ((__nothrow__));
91extern int sched_yield (void) __attribute__ ((__nothrow__));
92extern int sched_get_priority_max (int __algorithm) __attribute__ ((__nothrow__));
93extern int sched_get_priority_min (int __algorithm) __attribute__ ((__nothrow__));
94extern int sched_rr_get_interval (__pid_t __pid, struct timespec *__t) __attribute__ ((__nothrow__));
95
96
97
98typedef __clock_t clock_t;
99
100
101typedef __clockid_t clockid_t;
102typedef __timer_t timer_t;
103
104struct tm
105{
106 int tm_sec;
107 int tm_min;
108 int tm_hour;
109 int tm_mday;
110 int tm_mon;
111 int tm_year;
112 int tm_wday;
113 int tm_yday;
114 int tm_isdst;
115 long int tm_gmtoff;
116 __const char *tm_zone;
117};
118
119
120struct itimerspec
121 {
122 struct timespec it_interval;
123 struct timespec it_value;
124 };
125struct sigevent;
126
127extern clock_t clock (void) __attribute__ ((__nothrow__));
128extern time_t time (time_t *__timer) __attribute__ ((__nothrow__));
129extern double difftime (time_t __time1, time_t __time0)
130 __attribute__ ((__nothrow__)) __attribute__ ((__const__));
131extern time_t mktime (struct tm *__tp) __attribute__ ((__nothrow__));
132extern size_t strftime (char *__restrict __s, size_t __maxsize,
133 __const char *__restrict __format,
134 __const struct tm *__restrict __tp) __attribute__ ((__nothrow__));
135
136typedef struct __locale_struct
137{
138 struct __locale_data *__locales[13];
139 const unsigned short int *__ctype_b;
140 const int *__ctype_tolower;
141 const int *__ctype_toupper;
142 const char *__names[13];
143} *__locale_t;
144typedef __locale_t locale_t;
145extern size_t strftime_l (char *__restrict __s, size_t __maxsize,
146 __const char *__restrict __format,
147 __const struct tm *__restrict __tp,
148 __locale_t __loc) __attribute__ ((__nothrow__));
149
150extern struct tm *gmtime (__const time_t *__timer) __attribute__ ((__nothrow__));
151extern struct tm *localtime (__const time_t *__timer) __attribute__ ((__nothrow__));
152
153extern struct tm *gmtime_r (__const time_t *__restrict __timer,
154 struct tm *__restrict __tp) __attribute__ ((__nothrow__));
155extern struct tm *localtime_r (__const time_t *__restrict __timer,
156 struct tm *__restrict __tp) __attribute__ ((__nothrow__));
157
158extern char *asctime (__const struct tm *__tp) __attribute__ ((__nothrow__));
159extern char *ctime (__const time_t *__timer) __attribute__ ((__nothrow__));
160
161extern char *asctime_r (__const struct tm *__restrict __tp,
162 char *__restrict __buf) __attribute__ ((__nothrow__));
163extern char *ctime_r (__const time_t *__restrict __timer,
164 char *__restrict __buf) __attribute__ ((__nothrow__));
165extern char *__tzname[2];
166extern int __daylight;
167extern long int __timezone;
168extern char *tzname[2];
169extern void tzset (void) __attribute__ ((__nothrow__));
170extern int daylight;
171extern long int timezone;
172extern int stime (__const time_t *__when) __attribute__ ((__nothrow__));
173extern time_t timegm (struct tm *__tp) __attribute__ ((__nothrow__));
174extern time_t timelocal (struct tm *__tp) __attribute__ ((__nothrow__));
175extern int dysize (int __year) __attribute__ ((__nothrow__)) __attribute__ ((__const__));
176extern int nanosleep (__const struct timespec *__requested_time,
177 struct timespec *__remaining);
178extern int clock_getres (clockid_t __clock_id, struct timespec *__res) __attribute__ ((__nothrow__));
179extern int clock_gettime (clockid_t __clock_id, struct timespec *__tp) __attribute__ ((__nothrow__));
180extern int clock_settime (clockid_t __clock_id, __const struct timespec *__tp)
181 __attribute__ ((__nothrow__));
182extern int clock_nanosleep (clockid_t __clock_id, int __flags,
183 __const struct timespec *__req,
184 struct timespec *__rem);
185extern int clock_getcpuclockid (pid_t __pid, clockid_t *__clock_id) __attribute__ ((__nothrow__));
186extern int timer_create (clockid_t __clock_id,
187 struct sigevent *__restrict __evp,
188 timer_t *__restrict __timerid) __attribute__ ((__nothrow__));
189extern int timer_delete (timer_t __timerid) __attribute__ ((__nothrow__));
190extern int timer_settime (timer_t __timerid, int __flags,
191 __const struct itimerspec *__restrict __value,
192 struct itimerspec *__restrict __ovalue) __attribute__ ((__nothrow__));
193extern int timer_gettime (timer_t __timerid, struct itimerspec *__value)
194 __attribute__ ((__nothrow__));
195extern int timer_getoverrun (timer_t __timerid) __attribute__ ((__nothrow__));
196
197typedef unsigned long int pthread_t;
198typedef union
199{
200 char __size[56];
201 long int __align;
202} pthread_attr_t;
203typedef struct __pthread_internal_list
204{
205 struct __pthread_internal_list *__prev;
206 struct __pthread_internal_list *__next;
207} __pthread_list_t;
208typedef union
209{
210 struct __pthread_mutex_s
211 {
212 int __lock;
213 unsigned int __count;
214 int __owner;
215 unsigned int __nusers;
216 int __kind;
217 int __spins;
218 __pthread_list_t __list;
219 } __data;
220 char __size[40];
221 long int __align;
222} pthread_mutex_t;
223typedef union
224{
225 char __size[4];
226 int __align;
227} pthread_mutexattr_t;
228typedef union
229{
230 struct
231 {
232 int __lock;
233 unsigned int __futex;
234 __extension__ unsigned long long int __total_seq;
235 __extension__ unsigned long long int __wakeup_seq;
236 __extension__ unsigned long long int __woken_seq;
237 void *__mutex;
238 unsigned int __nwaiters;
239 unsigned int __broadcast_seq;
240 } __data;
241 char __size[48];
242 __extension__ long long int __align;
243} pthread_cond_t;
244typedef union
245{
246 char __size[4];
247 int __align;
248} pthread_condattr_t;
249typedef unsigned int pthread_key_t;
250typedef int pthread_once_t;
251typedef union
252{
253 struct
254 {
255 int __lock;
256 unsigned int __nr_readers;
257 unsigned int __readers_wakeup;
258 unsigned int __writer_wakeup;
259 unsigned int __nr_readers_queued;
260 unsigned int __nr_writers_queued;
261 int __writer;
262 int __shared;
263 unsigned long int __pad1;
264 unsigned long int __pad2;
265 unsigned int __flags;
266 } __data;
267 char __size[56];
268 long int __align;
269} pthread_rwlock_t;
270typedef union
271{
272 char __size[8];
273 long int __align;
274} pthread_rwlockattr_t;
275typedef volatile int pthread_spinlock_t;
276typedef union
277{
278 char __size[32];
279 long int __align;
280} pthread_barrier_t;
281typedef union
282{
283 char __size[4];
284 int __align;
285} pthread_barrierattr_t;
286typedef long int __jmp_buf[8];
287enum
288{
289 PTHREAD_CREATE_JOINABLE,
290 PTHREAD_CREATE_DETACHED
291};
292enum
293{
294 PTHREAD_MUTEX_TIMED_NP,
295 PTHREAD_MUTEX_RECURSIVE_NP,
296 PTHREAD_MUTEX_ERRORCHECK_NP,
297 PTHREAD_MUTEX_ADAPTIVE_NP
298 ,
299 PTHREAD_MUTEX_NORMAL = PTHREAD_MUTEX_TIMED_NP,
300 PTHREAD_MUTEX_RECURSIVE = PTHREAD_MUTEX_RECURSIVE_NP,
301 PTHREAD_MUTEX_ERRORCHECK = PTHREAD_MUTEX_ERRORCHECK_NP,
302 PTHREAD_MUTEX_DEFAULT = PTHREAD_MUTEX_NORMAL
303};
304enum
305{
306 PTHREAD_MUTEX_STALLED,
307 PTHREAD_MUTEX_STALLED_NP = PTHREAD_MUTEX_STALLED,
308 PTHREAD_MUTEX_ROBUST,
309 PTHREAD_MUTEX_ROBUST_NP = PTHREAD_MUTEX_ROBUST
310};
311enum
312{
313 PTHREAD_RWLOCK_PREFER_READER_NP,
314 PTHREAD_RWLOCK_PREFER_WRITER_NP,
315 PTHREAD_RWLOCK_PREFER_WRITER_NONRECURSIVE_NP,
316 PTHREAD_RWLOCK_DEFAULT_NP = PTHREAD_RWLOCK_PREFER_READER_NP
317};
318enum
319{
320 PTHREAD_INHERIT_SCHED,
321 PTHREAD_EXPLICIT_SCHED
322};
323enum
324{
325 PTHREAD_SCOPE_SYSTEM,
326 PTHREAD_SCOPE_PROCESS
327};
328enum
329{
330 PTHREAD_PROCESS_PRIVATE,
331 PTHREAD_PROCESS_SHARED
332};
333struct _pthread_cleanup_buffer
334{
335 void (*__routine) (void *);
336 void *__arg;
337 int __canceltype;
338 struct _pthread_cleanup_buffer *__prev;
339};
340enum
341{
342 PTHREAD_CANCEL_ENABLE,
343 PTHREAD_CANCEL_DISABLE
344};
345enum
346{
347 PTHREAD_CANCEL_DEFERRED,
348 PTHREAD_CANCEL_ASYNCHRONOUS
349};
350
351extern int pthread_create (pthread_t *__restrict __newthread,
352 __const pthread_attr_t *__restrict __attr,
353 void *(*__start_routine) (void *),
354 void *__restrict __arg) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 3)));
355extern void pthread_exit (void *__retval) __attribute__ ((__noreturn__));
356extern int pthread_join (pthread_t __th, void **__thread_return);
357extern int pthread_detach (pthread_t __th) __attribute__ ((__nothrow__));
358extern pthread_t pthread_self (void) __attribute__ ((__nothrow__)) __attribute__ ((__const__));
359extern int pthread_equal (pthread_t __thread1, pthread_t __thread2) __attribute__ ((__nothrow__));
360extern int pthread_attr_init (pthread_attr_t *__attr) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
361extern int pthread_attr_destroy (pthread_attr_t *__attr)
362 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
363extern int pthread_attr_getdetachstate (__const pthread_attr_t *__attr,
364 int *__detachstate)
365 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
366extern int pthread_attr_setdetachstate (pthread_attr_t *__attr,
367 int __detachstate)
368 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
369extern int pthread_attr_getguardsize (__const pthread_attr_t *__attr,
370 size_t *__guardsize)
371 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
372extern int pthread_attr_setguardsize (pthread_attr_t *__attr,
373 size_t __guardsize)
374 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
375extern int pthread_attr_getschedparam (__const pthread_attr_t *__restrict
376 __attr,
377 struct sched_param *__restrict __param)
378 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
379extern int pthread_attr_setschedparam (pthread_attr_t *__restrict __attr,
380 __const struct sched_param *__restrict
381 __param) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
382extern int pthread_attr_getschedpolicy (__const pthread_attr_t *__restrict
383 __attr, int *__restrict __policy)
384 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
385extern int pthread_attr_setschedpolicy (pthread_attr_t *__attr, int __policy)
386 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
387extern int pthread_attr_getinheritsched (__const pthread_attr_t *__restrict
388 __attr, int *__restrict __inherit)
389 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
390extern int pthread_attr_setinheritsched (pthread_attr_t *__attr,
391 int __inherit)
392 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
393extern int pthread_attr_getscope (__const pthread_attr_t *__restrict __attr,
394 int *__restrict __scope)
395 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
396extern int pthread_attr_setscope (pthread_attr_t *__attr, int __scope)
397 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
398extern int pthread_attr_getstackaddr (__const pthread_attr_t *__restrict
399 __attr, void **__restrict __stackaddr)
400 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2))) __attribute__ ((__deprecated__));
401extern int pthread_attr_setstackaddr (pthread_attr_t *__attr,
402 void *__stackaddr)
403 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) __attribute__ ((__deprecated__));
404extern int pthread_attr_getstacksize (__const pthread_attr_t *__restrict
405 __attr, size_t *__restrict __stacksize)
406 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
407extern int pthread_attr_setstacksize (pthread_attr_t *__attr,
408 size_t __stacksize)
409 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
410extern int pthread_attr_getstack (__const pthread_attr_t *__restrict __attr,
411 void **__restrict __stackaddr,
412 size_t *__restrict __stacksize)
413 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2, 3)));
414extern int pthread_attr_setstack (pthread_attr_t *__attr, void *__stackaddr,
415 size_t __stacksize) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
416extern int pthread_setschedparam (pthread_t __target_thread, int __policy,
417 __const struct sched_param *__param)
418 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3)));
419extern int pthread_getschedparam (pthread_t __target_thread,
420 int *__restrict __policy,
421 struct sched_param *__restrict __param)
422 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2, 3)));
423extern int pthread_setschedprio (pthread_t __target_thread, int __prio)
424 __attribute__ ((__nothrow__));
425extern int pthread_once (pthread_once_t *__once_control,
426 void (*__init_routine) (void)) __attribute__ ((__nonnull__ (1, 2)));
427extern int pthread_setcancelstate (int __state, int *__oldstate);
428extern int pthread_setcanceltype (int __type, int *__oldtype);
429extern int pthread_cancel (pthread_t __th);
430extern void pthread_testcancel (void);
431typedef struct
432{
433 struct
434 {
435 __jmp_buf __cancel_jmp_buf;
436 int __mask_was_saved;
437 } __cancel_jmp_buf[1];
438 void *__pad[4];
439} __pthread_unwind_buf_t __attribute__ ((__aligned__));
440struct __pthread_cleanup_frame
441{
442 void (*__cancel_routine) (void *);
443 void *__cancel_arg;
444 int __do_it;
445 int __cancel_type;
446};
447extern void __pthread_register_cancel (__pthread_unwind_buf_t *__buf)
448 ;
449extern void __pthread_unregister_cancel (__pthread_unwind_buf_t *__buf)
450 ;
451extern void __pthread_unwind_next (__pthread_unwind_buf_t *__buf)
452 __attribute__ ((__noreturn__))
453 __attribute__ ((__weak__))
454 ;
455struct __jmp_buf_tag;
456extern int __sigsetjmp (struct __jmp_buf_tag *__env, int __savemask) __attribute__ ((__nothrow__));
457extern int pthread_mutex_init (pthread_mutex_t *__mutex,
458 __const pthread_mutexattr_t *__mutexattr)
459 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
460extern int pthread_mutex_destroy (pthread_mutex_t *__mutex)
461 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
462extern int pthread_mutex_trylock (pthread_mutex_t *__mutex)
463 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
464extern int pthread_mutex_lock (pthread_mutex_t *__mutex)
465 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
466extern int pthread_mutex_timedlock (pthread_mutex_t *__restrict __mutex,
467 __const struct timespec *__restrict
468 __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
469extern int pthread_mutex_unlock (pthread_mutex_t *__mutex)
470 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
471extern int pthread_mutex_getprioceiling (__const pthread_mutex_t *
472 __restrict __mutex,
473 int *__restrict __prioceiling)
474 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
475extern int pthread_mutex_setprioceiling (pthread_mutex_t *__restrict __mutex,
476 int __prioceiling,
477 int *__restrict __old_ceiling)
478 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 3)));
479extern int pthread_mutex_consistent (pthread_mutex_t *__mutex)
480 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
481extern int pthread_mutexattr_init (pthread_mutexattr_t *__attr)
482 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
483extern int pthread_mutexattr_destroy (pthread_mutexattr_t *__attr)
484 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
485extern int pthread_mutexattr_getpshared (__const pthread_mutexattr_t *
486 __restrict __attr,
487 int *__restrict __pshared)
488 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
489extern int pthread_mutexattr_setpshared (pthread_mutexattr_t *__attr,
490 int __pshared)
491 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
492extern int pthread_mutexattr_gettype (__const pthread_mutexattr_t *__restrict
493 __attr, int *__restrict __kind)
494 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
495extern int pthread_mutexattr_settype (pthread_mutexattr_t *__attr, int __kind)
496 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
497extern int pthread_mutexattr_getprotocol (__const pthread_mutexattr_t *
498 __restrict __attr,
499 int *__restrict __protocol)
500 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
501extern int pthread_mutexattr_setprotocol (pthread_mutexattr_t *__attr,
502 int __protocol)
503 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
504extern int pthread_mutexattr_getprioceiling (__const pthread_mutexattr_t *
505 __restrict __attr,
506 int *__restrict __prioceiling)
507 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
508extern int pthread_mutexattr_setprioceiling (pthread_mutexattr_t *__attr,
509 int __prioceiling)
510 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
511extern int pthread_mutexattr_getrobust (__const pthread_mutexattr_t *__attr,
512 int *__robustness)
513 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
514extern int pthread_mutexattr_setrobust (pthread_mutexattr_t *__attr,
515 int __robustness)
516 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
517extern int pthread_rwlock_init (pthread_rwlock_t *__restrict __rwlock,
518 __const pthread_rwlockattr_t *__restrict
519 __attr) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
520extern int pthread_rwlock_destroy (pthread_rwlock_t *__rwlock)
521 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
522extern int pthread_rwlock_rdlock (pthread_rwlock_t *__rwlock)
523 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
524extern int pthread_rwlock_tryrdlock (pthread_rwlock_t *__rwlock)
525 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
526extern int pthread_rwlock_timedrdlock (pthread_rwlock_t *__restrict __rwlock,
527 __const struct timespec *__restrict
528 __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
529extern int pthread_rwlock_wrlock (pthread_rwlock_t *__rwlock)
530 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
531extern int pthread_rwlock_trywrlock (pthread_rwlock_t *__rwlock)
532 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
533extern int pthread_rwlock_timedwrlock (pthread_rwlock_t *__restrict __rwlock,
534 __const struct timespec *__restrict
535 __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
536extern int pthread_rwlock_unlock (pthread_rwlock_t *__rwlock)
537 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
538extern int pthread_rwlockattr_init (pthread_rwlockattr_t *__attr)
539 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
540extern int pthread_rwlockattr_destroy (pthread_rwlockattr_t *__attr)
541 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
542extern int pthread_rwlockattr_getpshared (__const pthread_rwlockattr_t *
543 __restrict __attr,
544 int *__restrict __pshared)
545 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
546extern int pthread_rwlockattr_setpshared (pthread_rwlockattr_t *__attr,
547 int __pshared)
548 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
549extern int pthread_rwlockattr_getkind_np (__const pthread_rwlockattr_t *
550 __restrict __attr,
551 int *__restrict __pref)
552 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
553extern int pthread_rwlockattr_setkind_np (pthread_rwlockattr_t *__attr,
554 int __pref) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
555extern int pthread_cond_init (pthread_cond_t *__restrict __cond,
556 __const pthread_condattr_t *__restrict
557 __cond_attr) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
558extern int pthread_cond_destroy (pthread_cond_t *__cond)
559 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
560extern int pthread_cond_signal (pthread_cond_t *__cond)
561 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
562extern int pthread_cond_broadcast (pthread_cond_t *__cond)
563 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
564extern int pthread_cond_wait (pthread_cond_t *__restrict __cond,
565 pthread_mutex_t *__restrict __mutex)
566 __attribute__ ((__nonnull__ (1, 2)));
567extern int pthread_cond_timedwait (pthread_cond_t *__restrict __cond,
568 pthread_mutex_t *__restrict __mutex,
569 __const struct timespec *__restrict
570 __abstime) __attribute__ ((__nonnull__ (1, 2, 3)));
571extern int pthread_condattr_init (pthread_condattr_t *__attr)
572 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
573extern int pthread_condattr_destroy (pthread_condattr_t *__attr)
574 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
575extern int pthread_condattr_getpshared (__const pthread_condattr_t *
576 __restrict __attr,
577 int *__restrict __pshared)
578 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
579extern int pthread_condattr_setpshared (pthread_condattr_t *__attr,
580 int __pshared) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
581extern int pthread_condattr_getclock (__const pthread_condattr_t *
582 __restrict __attr,
583 __clockid_t *__restrict __clock_id)
584 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
585extern int pthread_condattr_setclock (pthread_condattr_t *__attr,
586 __clockid_t __clock_id)
587 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
588extern int pthread_spin_init (pthread_spinlock_t *__lock, int __pshared)
589 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
590extern int pthread_spin_destroy (pthread_spinlock_t *__lock)
591 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
592extern int pthread_spin_lock (pthread_spinlock_t *__lock)
593 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
594extern int pthread_spin_trylock (pthread_spinlock_t *__lock)
595 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
596extern int pthread_spin_unlock (pthread_spinlock_t *__lock)
597 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
598extern int pthread_barrier_init (pthread_barrier_t *__restrict __barrier,
599 __const pthread_barrierattr_t *__restrict
600 __attr, unsigned int __count)
601 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
602extern int pthread_barrier_destroy (pthread_barrier_t *__barrier)
603 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
604extern int pthread_barrier_wait (pthread_barrier_t *__barrier)
605 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
606extern int pthread_barrierattr_init (pthread_barrierattr_t *__attr)
607 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
608extern int pthread_barrierattr_destroy (pthread_barrierattr_t *__attr)
609 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
610extern int pthread_barrierattr_getpshared (__const pthread_barrierattr_t *
611 __restrict __attr,
612 int *__restrict __pshared)
613 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
614extern int pthread_barrierattr_setpshared (pthread_barrierattr_t *__attr,
615 int __pshared)
616 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
617extern int pthread_key_create (pthread_key_t *__key,
618 void (*__destr_function) (void *))
619 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
620extern int pthread_key_delete (pthread_key_t __key) __attribute__ ((__nothrow__));
621extern void *pthread_getspecific (pthread_key_t __key) __attribute__ ((__nothrow__));
622extern int pthread_setspecific (pthread_key_t __key,
623 __const void *__pointer) __attribute__ ((__nothrow__)) ;
624extern int pthread_getcpuclockid (pthread_t __thread_id,
625 __clockid_t *__clock_id)
626 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2)));
627extern int pthread_atfork (void (*__prepare) (void),
628 void (*__parent) (void),
629 void (*__child) (void)) __attribute__ ((__nothrow__));
630
631
632struct _IO_FILE;
633
634typedef struct _IO_FILE FILE;
635
636
637typedef struct _IO_FILE __FILE;
638typedef struct
639{
640 int __count;
641 union
642 {
643 unsigned int __wch;
644 char __wchb[4];
645 } __value;
646} __mbstate_t;
647typedef struct
648{
649 __off_t __pos;
650 __mbstate_t __state;
651} _G_fpos_t;
652typedef struct
653{
654 __off64_t __pos;
655 __mbstate_t __state;
656} _G_fpos64_t;
657typedef int _G_int16_t __attribute__ ((__mode__ (__HI__)));
658typedef int _G_int32_t __attribute__ ((__mode__ (__SI__)));
659typedef unsigned int _G_uint16_t __attribute__ ((__mode__ (__HI__)));
660typedef unsigned int _G_uint32_t __attribute__ ((__mode__ (__SI__)));
661typedef __builtin_va_list __gnuc_va_list;
662struct _IO_jump_t; struct _IO_FILE;
663typedef void _IO_lock_t;
664struct _IO_marker {
665 struct _IO_marker *_next;
666 struct _IO_FILE *_sbuf;
667 int _pos;
668};
669enum __codecvt_result
670{
671 __codecvt_ok,
672 __codecvt_partial,
673 __codecvt_error,
674 __codecvt_noconv
675};
676struct _IO_FILE {
677 int _flags;
678 char* _IO_read_ptr;
679 char* _IO_read_end;
680 char* _IO_read_base;
681 char* _IO_write_base;
682 char* _IO_write_ptr;
683 char* _IO_write_end;
684 char* _IO_buf_base;
685 char* _IO_buf_end;
686 char *_IO_save_base;
687 char *_IO_backup_base;
688 char *_IO_save_end;
689 struct _IO_marker *_markers;
690 struct _IO_FILE *_chain;
691 int _fileno;
692 int _flags2;
693 __off_t _old_offset;
694 unsigned short _cur_column;
695 signed char _vtable_offset;
696 char _shortbuf[1];
697 _IO_lock_t *_lock;
698 __off64_t _offset;
699 void *__pad1;
700 void *__pad2;
701 void *__pad3;
702 void *__pad4;
703 size_t __pad5;
704 int _mode;
705 char _unused2[15 * sizeof (int) - 4 * sizeof (void *) - sizeof (size_t)];
706};
707typedef struct _IO_FILE _IO_FILE;
708struct _IO_FILE_plus;
709extern struct _IO_FILE_plus _IO_2_1_stdin_;
710extern struct _IO_FILE_plus _IO_2_1_stdout_;
711extern struct _IO_FILE_plus _IO_2_1_stderr_;
712typedef __ssize_t __io_read_fn (void *__cookie, char *__buf, size_t __nbytes);
713typedef __ssize_t __io_write_fn (void *__cookie, __const char *__buf,
714 size_t __n);
715typedef int __io_seek_fn (void *__cookie, __off64_t *__pos, int __w);
716typedef int __io_close_fn (void *__cookie);
717extern int __underflow (_IO_FILE *);
718extern int __uflow (_IO_FILE *);
719extern int __overflow (_IO_FILE *, int);
720extern int _IO_getc (_IO_FILE *__fp);
721extern int _IO_putc (int __c, _IO_FILE *__fp);
722extern int _IO_feof (_IO_FILE *__fp) __attribute__ ((__nothrow__));
723extern int _IO_ferror (_IO_FILE *__fp) __attribute__ ((__nothrow__));
724extern int _IO_peekc_locked (_IO_FILE *__fp);
725extern void _IO_flockfile (_IO_FILE *) __attribute__ ((__nothrow__));
726extern void _IO_funlockfile (_IO_FILE *) __attribute__ ((__nothrow__));
727extern int _IO_ftrylockfile (_IO_FILE *) __attribute__ ((__nothrow__));
728extern int _IO_vfscanf (_IO_FILE * __restrict, const char * __restrict,
729 __gnuc_va_list, int *__restrict);
730extern int _IO_vfprintf (_IO_FILE *__restrict, const char *__restrict,
731 __gnuc_va_list);
732extern __ssize_t _IO_padn (_IO_FILE *, int, __ssize_t);
733extern size_t _IO_sgetn (_IO_FILE *, void *, size_t);
734extern __off64_t _IO_seekoff (_IO_FILE *, __off64_t, int, int);
735extern __off64_t _IO_seekpos (_IO_FILE *, __off64_t, int);
736extern void _IO_free_backup_area (_IO_FILE *) __attribute__ ((__nothrow__));
737typedef __gnuc_va_list va_list;
738typedef __off_t off_t;
739typedef __ssize_t ssize_t;
740
741typedef _G_fpos_t fpos_t;
742
743extern struct _IO_FILE *stdin;
744extern struct _IO_FILE *stdout;
745extern struct _IO_FILE *stderr;
746
747extern int remove (__const char *__filename) __attribute__ ((__nothrow__));
748extern int rename (__const char *__old, __const char *__new) __attribute__ ((__nothrow__));
749
750extern int renameat (int __oldfd, __const char *__old, int __newfd,
751 __const char *__new) __attribute__ ((__nothrow__));
752
753extern FILE *tmpfile (void) ;
754extern char *tmpnam (char *__s) __attribute__ ((__nothrow__)) ;
755
756extern char *tmpnam_r (char *__s) __attribute__ ((__nothrow__)) ;
757extern char *tempnam (__const char *__dir, __const char *__pfx)
758 __attribute__ ((__nothrow__)) __attribute__ ((__malloc__)) ;
759
760extern int fclose (FILE *__stream);
761extern int fflush (FILE *__stream);
762
763extern int fflush_unlocked (FILE *__stream);
764
765extern FILE *fopen (__const char *__restrict __filename,
766 __const char *__restrict __modes) ;
767extern FILE *freopen (__const char *__restrict __filename,
768 __const char *__restrict __modes,
769 FILE *__restrict __stream) ;
770
771extern FILE *fdopen (int __fd, __const char *__modes) __attribute__ ((__nothrow__)) ;
772extern FILE *fmemopen (void *__s, size_t __len, __const char *__modes)
773 __attribute__ ((__nothrow__)) ;
774extern FILE *open_memstream (char **__bufloc, size_t *__sizeloc) __attribute__ ((__nothrow__)) ;
775
776extern void setbuf (FILE *__restrict __stream, char *__restrict __buf) __attribute__ ((__nothrow__));
777extern int setvbuf (FILE *__restrict __stream, char *__restrict __buf,
778 int __modes, size_t __n) __attribute__ ((__nothrow__));
779
780extern void setbuffer (FILE *__restrict __stream, char *__restrict __buf,
781 size_t __size) __attribute__ ((__nothrow__));
782extern void setlinebuf (FILE *__stream) __attribute__ ((__nothrow__));
783
784extern int fprintf (FILE *__restrict __stream,
785 __const char *__restrict __format, ...);
786extern int printf (__const char *__restrict __format, ...);
787extern int sprintf (char *__restrict __s,
788 __const char *__restrict __format, ...) __attribute__ ((__nothrow__));
789extern int vfprintf (FILE *__restrict __s, __const char *__restrict __format,
790 __gnuc_va_list __arg);
791extern int vprintf (__const char *__restrict __format, __gnuc_va_list __arg);
792extern int vsprintf (char *__restrict __s, __const char *__restrict __format,
793 __gnuc_va_list __arg) __attribute__ ((__nothrow__));
794
795
796extern int snprintf (char *__restrict __s, size_t __maxlen,
797 __const char *__restrict __format, ...)
798 __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 4)));
799extern int vsnprintf (char *__restrict __s, size_t __maxlen,
800 __const char *__restrict __format, __gnuc_va_list __arg)
801 __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 0)));
802
803extern int vdprintf (int __fd, __const char *__restrict __fmt,
804 __gnuc_va_list __arg)
805 __attribute__ ((__format__ (__printf__, 2, 0)));
806extern int dprintf (int __fd, __const char *__restrict __fmt, ...)
807 __attribute__ ((__format__ (__printf__, 2, 3)));
808
809extern int fscanf (FILE *__restrict __stream,
810 __const char *__restrict __format, ...) ;
811extern int scanf (__const char *__restrict __format, ...) ;
812extern int sscanf (__const char *__restrict __s,
813 __const char *__restrict __format, ...) __attribute__ ((__nothrow__));
814extern int fscanf (FILE *__restrict __stream, __const char *__restrict __format, ...) __asm__ ("" "__isoc99_fscanf") ;
815extern int scanf (__const char *__restrict __format, ...) __asm__ ("" "__isoc99_scanf") ;
816extern int sscanf (__const char *__restrict __s, __const char *__restrict __format, ...) __asm__ ("" "__isoc99_sscanf") __attribute__ ((__nothrow__));
817
818
819extern int vfscanf (FILE *__restrict __s, __const char *__restrict __format,
820 __gnuc_va_list __arg)
821 __attribute__ ((__format__ (__scanf__, 2, 0))) ;
822extern int vscanf (__const char *__restrict __format, __gnuc_va_list __arg)
823 __attribute__ ((__format__ (__scanf__, 1, 0))) ;
824extern int vsscanf (__const char *__restrict __s,
825 __const char *__restrict __format, __gnuc_va_list __arg)
826 __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__scanf__, 2, 0)));
827extern int vfscanf (FILE *__restrict __s, __const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vfscanf")
828 __attribute__ ((__format__ (__scanf__, 2, 0))) ;
829extern int vscanf (__const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vscanf")
830 __attribute__ ((__format__ (__scanf__, 1, 0))) ;
831extern int vsscanf (__const char *__restrict __s, __const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vsscanf") __attribute__ ((__nothrow__))
832 __attribute__ ((__format__ (__scanf__, 2, 0)));
833
834
835extern int fgetc (FILE *__stream);
836extern int getc (FILE *__stream);
837extern int getchar (void);
838
839extern int getc_unlocked (FILE *__stream);
840extern int getchar_unlocked (void);
841extern int fgetc_unlocked (FILE *__stream);
842
843extern int fputc (int __c, FILE *__stream);
844extern int putc (int __c, FILE *__stream);
845extern int putchar (int __c);
846
847extern int fputc_unlocked (int __c, FILE *__stream);
848extern int putc_unlocked (int __c, FILE *__stream);
849extern int putchar_unlocked (int __c);
850extern int getw (FILE *__stream);
851extern int putw (int __w, FILE *__stream);
852
853extern char *fgets (char *__restrict __s, int __n, FILE *__restrict __stream)
854 ;
855extern char *gets (char *__s) ;
856
857extern __ssize_t __getdelim (char **__restrict __lineptr,
858 size_t *__restrict __n, int __delimiter,
859 FILE *__restrict __stream) ;
860extern __ssize_t getdelim (char **__restrict __lineptr,
861 size_t *__restrict __n, int __delimiter,
862 FILE *__restrict __stream) ;
863extern __ssize_t getline (char **__restrict __lineptr,
864 size_t *__restrict __n,
865 FILE *__restrict __stream) ;
866
867extern int fputs (__const char *__restrict __s, FILE *__restrict __stream);
868extern int puts (__const char *__s);
869extern int ungetc (int __c, FILE *__stream);
870extern size_t fread (void *__restrict __ptr, size_t __size,
871 size_t __n, FILE *__restrict __stream) ;
872extern size_t fwrite (__const void *__restrict __ptr, size_t __size,
873 size_t __n, FILE *__restrict __s) ;
874
875extern size_t fread_unlocked (void *__restrict __ptr, size_t __size,
876 size_t __n, FILE *__restrict __stream) ;
877extern size_t fwrite_unlocked (__const void *__restrict __ptr, size_t __size,
878 size_t __n, FILE *__restrict __stream) ;
879
880extern int fseek (FILE *__stream, long int __off, int __whence);
881extern long int ftell (FILE *__stream) ;
882extern void rewind (FILE *__stream);
883
884extern int fseeko (FILE *__stream, __off_t __off, int __whence);
885extern __off_t ftello (FILE *__stream) ;
886
887extern int fgetpos (FILE *__restrict __stream, fpos_t *__restrict __pos);
888extern int fsetpos (FILE *__stream, __const fpos_t *__pos);
889
890
891extern void clearerr (FILE *__stream) __attribute__ ((__nothrow__));
892extern int feof (FILE *__stream) __attribute__ ((__nothrow__)) ;
893extern int ferror (FILE *__stream) __attribute__ ((__nothrow__)) ;
894
895extern void clearerr_unlocked (FILE *__stream) __attribute__ ((__nothrow__));
896extern int feof_unlocked (FILE *__stream) __attribute__ ((__nothrow__)) ;
897extern int ferror_unlocked (FILE *__stream) __attribute__ ((__nothrow__)) ;
898
899extern void perror (__const char *__s);
900
901extern int sys_nerr;
902extern __const char *__const sys_errlist[];
903extern int fileno (FILE *__stream) __attribute__ ((__nothrow__)) ;
904extern int fileno_unlocked (FILE *__stream) __attribute__ ((__nothrow__)) ;
905extern FILE *popen (__const char *__command, __const char *__modes) ;
906extern int pclose (FILE *__stream);
907extern char *ctermid (char *__s) __attribute__ ((__nothrow__));
908extern void flockfile (FILE *__stream) __attribute__ ((__nothrow__));
909extern int ftrylockfile (FILE *__stream) __attribute__ ((__nothrow__)) ;
910extern void funlockfile (FILE *__stream) __attribute__ ((__nothrow__));
911
912unsigned int __VERIFIER_nondet_uint();
913int top=0;
914unsigned int arr[(800)];
915pthread_mutex_t m;
916_Bool flag=(0);
917void error(void)
918{
919 ERROR: __VERIFIER_error(); return;
920}
921void inc_top(void)
922{
923 top++;
924}
925void dec_top(void)
926{
927 top--;
928}
929int get_top(void)
930{
931 return top;
932}
933int stack_empty(void)
934{
935 (top==0) ? (1) : (0);
936}
937int push(unsigned int *stack, int x)
938{
939 if (top==(800))
940 {
941 printf("stack overflow\n");
942 return (-1);
943 }
944 else
945 {
946 stack[get_top()] = x;
947 inc_top();
948 }
949 return 0;
950}
951int pop(unsigned int *stack)
952{
953 if (top==0)
954 {
955 printf("stack underflow\n");
956 return (-2);
957 }
958 else
959 {
960 dec_top();
961 return stack[get_top()];
962 }
963 return 0;
964}
965void *t1(void *arg)
966{
967 int i;
968 unsigned int tmp;
969 for(i=0; i<(800); i++)
970 {
971 pthread_mutex_lock(&m);
972 tmp = __VERIFIER_nondet_uint()%(800);
973 if ((push(arr,tmp)==(-1)))
974 error();
975 pthread_mutex_unlock(&m);
976 }
977}
978void *t2(void *arg)
979{
980 int i;
981 for(i=0; i<(800); i++)
982 {
983 pthread_mutex_lock(&m);
984 if (top>0)
985 {
986 if ((pop(arr)==(-2)))
987 error();
988 }
989 pthread_mutex_unlock(&m);
990 }
991}
992int main(void)
993{
994 pthread_t id1, id2;
995 pthread_mutex_init(&m, 0);
996 pthread_create(&id1, ((void *)0), t1, ((void *)0));
997 pthread_create(&id2, ((void *)0), t2, ((void *)0));
998 pthread_join(id1, ((void *)0));
999 pthread_join(id2, ((void *)0));
1000 return 0;
1001}
Note: See TracBrowser for help on using the repository browser.