source: CIVL/examples/pthread/svcomp/10_fmaxsym_cas_true-unreach-call.i@ 4e16aed

1.23 2.0 main test-branch
Last change on this file since 4e16aed 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: 27.7 KB
Line 
1extern void __VERIFIER_error() __attribute__ ((__noreturn__));
2extern int __VERIFIER_nondet_int();
3
4typedef unsigned char __u_char;
5typedef unsigned short int __u_short;
6typedef unsigned int __u_int;
7typedef unsigned long int __u_long;
8typedef signed char __int8_t;
9typedef unsigned char __uint8_t;
10typedef signed short int __int16_t;
11typedef unsigned short int __uint16_t;
12typedef signed int __int32_t;
13typedef unsigned int __uint32_t;
14typedef signed long int __int64_t;
15typedef unsigned long int __uint64_t;
16typedef long int __quad_t;
17typedef unsigned long int __u_quad_t;
18typedef unsigned long int __dev_t;
19typedef unsigned int __uid_t;
20typedef unsigned int __gid_t;
21typedef unsigned long int __ino_t;
22typedef unsigned long int __ino64_t;
23typedef unsigned int __mode_t;
24typedef unsigned long int __nlink_t;
25typedef long int __off_t;
26typedef long int __off64_t;
27typedef int __pid_t;
28typedef struct { int __val[2]; } __fsid_t;
29typedef long int __clock_t;
30typedef unsigned long int __rlim_t;
31typedef unsigned long int __rlim64_t;
32typedef unsigned int __id_t;
33typedef long int __time_t;
34typedef unsigned int __useconds_t;
35typedef long int __suseconds_t;
36typedef int __daddr_t;
37typedef long int __swblk_t;
38typedef int __key_t;
39typedef int __clockid_t;
40typedef void * __timer_t;
41typedef long int __blksize_t;
42typedef long int __blkcnt_t;
43typedef long int __blkcnt64_t;
44typedef unsigned long int __fsblkcnt_t;
45typedef unsigned long int __fsblkcnt64_t;
46typedef unsigned long int __fsfilcnt_t;
47typedef unsigned long int __fsfilcnt64_t;
48typedef long int __ssize_t;
49typedef __off64_t __loff_t;
50typedef __quad_t *__qaddr_t;
51typedef char *__caddr_t;
52typedef long int __intptr_t;
53typedef unsigned int __socklen_t;
54typedef long unsigned int size_t;
55
56typedef __time_t time_t;
57
58
59struct timespec
60 {
61 __time_t tv_sec;
62 long int tv_nsec;
63 };
64typedef __pid_t pid_t;
65struct sched_param
66 {
67 int __sched_priority;
68 };
69
70
71struct __sched_param
72 {
73 int __sched_priority;
74 };
75typedef unsigned long int __cpu_mask;
76typedef struct
77{
78 __cpu_mask __bits[1024 / (8 * sizeof (__cpu_mask))];
79} cpu_set_t;
80
81extern int __sched_cpucount (size_t __setsize, const cpu_set_t *__setp)
82 __attribute__ ((__nothrow__ , __leaf__));
83extern cpu_set_t *__sched_cpualloc (size_t __count) __attribute__ ((__nothrow__ , __leaf__)) ;
84extern void __sched_cpufree (cpu_set_t *__set) __attribute__ ((__nothrow__ , __leaf__));
85
86
87extern int sched_setparam (__pid_t __pid, __const struct sched_param *__param)
88 __attribute__ ((__nothrow__ , __leaf__));
89extern int sched_getparam (__pid_t __pid, struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__));
90extern int sched_setscheduler (__pid_t __pid, int __policy,
91 __const struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__));
92extern int sched_getscheduler (__pid_t __pid) __attribute__ ((__nothrow__ , __leaf__));
93extern int sched_yield (void) __attribute__ ((__nothrow__ , __leaf__));
94extern int sched_get_priority_max (int __algorithm) __attribute__ ((__nothrow__ , __leaf__));
95extern int sched_get_priority_min (int __algorithm) __attribute__ ((__nothrow__ , __leaf__));
96extern int sched_rr_get_interval (__pid_t __pid, struct timespec *__t) __attribute__ ((__nothrow__ , __leaf__));
97
98
99
100typedef __clock_t clock_t;
101
102
103typedef __clockid_t clockid_t;
104
105
106
107typedef __timer_t timer_t;
108
109struct tm
110{
111 int tm_sec;
112 int tm_min;
113 int tm_hour;
114 int tm_mday;
115 int tm_mon;
116 int tm_year;
117 int tm_wday;
118 int tm_yday;
119 int tm_isdst;
120 long int tm_gmtoff;
121 __const char *tm_zone;
122};
123
124
125struct itimerspec
126 {
127 struct timespec it_interval;
128 struct timespec it_value;
129 };
130struct sigevent;
131
132extern clock_t clock (void) __attribute__ ((__nothrow__ , __leaf__));
133extern time_t time (time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
134extern double difftime (time_t __time1, time_t __time0)
135 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
136extern time_t mktime (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
137extern size_t strftime (char *__restrict __s, size_t __maxsize,
138 __const char *__restrict __format,
139 __const struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__));
140
141typedef struct __locale_struct
142{
143 struct __locale_data *__locales[13];
144 const unsigned short int *__ctype_b;
145 const int *__ctype_tolower;
146 const int *__ctype_toupper;
147 const char *__names[13];
148} *__locale_t;
149typedef __locale_t locale_t;
150extern size_t strftime_l (char *__restrict __s, size_t __maxsize,
151 __const char *__restrict __format,
152 __const struct tm *__restrict __tp,
153 __locale_t __loc) __attribute__ ((__nothrow__ , __leaf__));
154
155extern struct tm *gmtime (__const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
156extern struct tm *localtime (__const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
157
158extern struct tm *gmtime_r (__const time_t *__restrict __timer,
159 struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__));
160extern struct tm *localtime_r (__const time_t *__restrict __timer,
161 struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__));
162
163extern char *asctime (__const struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
164extern char *ctime (__const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
165
166extern char *asctime_r (__const struct tm *__restrict __tp,
167 char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__));
168extern char *ctime_r (__const time_t *__restrict __timer,
169 char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__));
170extern char *__tzname[2];
171extern int __daylight;
172extern long int __timezone;
173extern char *tzname[2];
174extern void tzset (void) __attribute__ ((__nothrow__ , __leaf__));
175extern int daylight;
176extern long int timezone;
177extern int stime (__const time_t *__when) __attribute__ ((__nothrow__ , __leaf__));
178extern time_t timegm (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
179extern time_t timelocal (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
180extern int dysize (int __year) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
181extern int nanosleep (__const struct timespec *__requested_time,
182 struct timespec *__remaining);
183extern int clock_getres (clockid_t __clock_id, struct timespec *__res) __attribute__ ((__nothrow__ , __leaf__));
184extern int clock_gettime (clockid_t __clock_id, struct timespec *__tp) __attribute__ ((__nothrow__ , __leaf__));
185extern int clock_settime (clockid_t __clock_id, __const struct timespec *__tp)
186 __attribute__ ((__nothrow__ , __leaf__));
187extern int clock_nanosleep (clockid_t __clock_id, int __flags,
188 __const struct timespec *__req,
189 struct timespec *__rem);
190extern int clock_getcpuclockid (pid_t __pid, clockid_t *__clock_id) __attribute__ ((__nothrow__ , __leaf__));
191extern int timer_create (clockid_t __clock_id,
192 struct sigevent *__restrict __evp,
193 timer_t *__restrict __timerid) __attribute__ ((__nothrow__ , __leaf__));
194extern int timer_delete (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__));
195extern int timer_settime (timer_t __timerid, int __flags,
196 __const struct itimerspec *__restrict __value,
197 struct itimerspec *__restrict __ovalue) __attribute__ ((__nothrow__ , __leaf__));
198extern int timer_gettime (timer_t __timerid, struct itimerspec *__value)
199 __attribute__ ((__nothrow__ , __leaf__));
200extern int timer_getoverrun (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__));
201
202typedef unsigned long int pthread_t;
203typedef union
204{
205 char __size[56];
206 long int __align;
207} pthread_attr_t;
208typedef struct __pthread_internal_list
209{
210 struct __pthread_internal_list *__prev;
211 struct __pthread_internal_list *__next;
212} __pthread_list_t;
213typedef union
214{
215 struct __pthread_mutex_s
216 {
217 int __lock;
218 unsigned int __count;
219 int __owner;
220 unsigned int __nusers;
221 int __kind;
222 int __spins;
223 __pthread_list_t __list;
224 } __data;
225 char __size[40];
226 long int __align;
227} pthread_mutex_t;
228typedef union
229{
230 char __size[4];
231 int __align;
232} pthread_mutexattr_t;
233typedef union
234{
235 struct
236 {
237 int __lock;
238 unsigned int __futex;
239 __extension__ unsigned long long int __total_seq;
240 __extension__ unsigned long long int __wakeup_seq;
241 __extension__ unsigned long long int __woken_seq;
242 void *__mutex;
243 unsigned int __nwaiters;
244 unsigned int __broadcast_seq;
245 } __data;
246 char __size[48];
247 __extension__ long long int __align;
248} pthread_cond_t;
249typedef union
250{
251 char __size[4];
252 int __align;
253} pthread_condattr_t;
254typedef unsigned int pthread_key_t;
255typedef int pthread_once_t;
256typedef union
257{
258 struct
259 {
260 int __lock;
261 unsigned int __nr_readers;
262 unsigned int __readers_wakeup;
263 unsigned int __writer_wakeup;
264 unsigned int __nr_readers_queued;
265 unsigned int __nr_writers_queued;
266 int __writer;
267 int __shared;
268 unsigned long int __pad1;
269 unsigned long int __pad2;
270 unsigned int __flags;
271 } __data;
272 char __size[56];
273 long int __align;
274} pthread_rwlock_t;
275typedef union
276{
277 char __size[8];
278 long int __align;
279} pthread_rwlockattr_t;
280typedef volatile int pthread_spinlock_t;
281typedef union
282{
283 char __size[32];
284 long int __align;
285} pthread_barrier_t;
286typedef union
287{
288 char __size[4];
289 int __align;
290} pthread_barrierattr_t;
291typedef long int __jmp_buf[8];
292enum
293{
294 PTHREAD_CREATE_JOINABLE,
295 PTHREAD_CREATE_DETACHED
296};
297enum
298{
299 PTHREAD_MUTEX_TIMED_NP,
300 PTHREAD_MUTEX_RECURSIVE_NP,
301 PTHREAD_MUTEX_ERRORCHECK_NP,
302 PTHREAD_MUTEX_ADAPTIVE_NP
303 ,
304 PTHREAD_MUTEX_NORMAL = PTHREAD_MUTEX_TIMED_NP,
305 PTHREAD_MUTEX_RECURSIVE = PTHREAD_MUTEX_RECURSIVE_NP,
306 PTHREAD_MUTEX_ERRORCHECK = PTHREAD_MUTEX_ERRORCHECK_NP,
307 PTHREAD_MUTEX_DEFAULT = PTHREAD_MUTEX_NORMAL
308};
309enum
310{
311 PTHREAD_MUTEX_STALLED,
312 PTHREAD_MUTEX_STALLED_NP = PTHREAD_MUTEX_STALLED,
313 PTHREAD_MUTEX_ROBUST,
314 PTHREAD_MUTEX_ROBUST_NP = PTHREAD_MUTEX_ROBUST
315};
316enum
317{
318 PTHREAD_RWLOCK_PREFER_READER_NP,
319 PTHREAD_RWLOCK_PREFER_WRITER_NP,
320 PTHREAD_RWLOCK_PREFER_WRITER_NONRECURSIVE_NP,
321 PTHREAD_RWLOCK_DEFAULT_NP = PTHREAD_RWLOCK_PREFER_READER_NP
322};
323enum
324{
325 PTHREAD_INHERIT_SCHED,
326 PTHREAD_EXPLICIT_SCHED
327};
328enum
329{
330 PTHREAD_SCOPE_SYSTEM,
331 PTHREAD_SCOPE_PROCESS
332};
333enum
334{
335 PTHREAD_PROCESS_PRIVATE,
336 PTHREAD_PROCESS_SHARED
337};
338struct _pthread_cleanup_buffer
339{
340 void (*__routine) (void *);
341 void *__arg;
342 int __canceltype;
343 struct _pthread_cleanup_buffer *__prev;
344};
345enum
346{
347 PTHREAD_CANCEL_ENABLE,
348 PTHREAD_CANCEL_DISABLE
349};
350enum
351{
352 PTHREAD_CANCEL_DEFERRED,
353 PTHREAD_CANCEL_ASYNCHRONOUS
354};
355
356extern int pthread_create (pthread_t *__restrict __newthread,
357 __const pthread_attr_t *__restrict __attr,
358 void *(*__start_routine) (void *),
359 void *__restrict __arg) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 3)));
360extern void pthread_exit (void *__retval) __attribute__ ((__noreturn__));
361extern int pthread_join (pthread_t __th, void **__thread_return);
362extern int pthread_detach (pthread_t __th) __attribute__ ((__nothrow__ , __leaf__));
363extern pthread_t pthread_self (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
364extern int pthread_equal (pthread_t __thread1, pthread_t __thread2) __attribute__ ((__nothrow__ , __leaf__));
365extern int pthread_attr_init (pthread_attr_t *__attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
366extern int pthread_attr_destroy (pthread_attr_t *__attr)
367 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
368extern int pthread_attr_getdetachstate (__const pthread_attr_t *__attr,
369 int *__detachstate)
370 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
371extern int pthread_attr_setdetachstate (pthread_attr_t *__attr,
372 int __detachstate)
373 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
374extern int pthread_attr_getguardsize (__const pthread_attr_t *__attr,
375 size_t *__guardsize)
376 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
377extern int pthread_attr_setguardsize (pthread_attr_t *__attr,
378 size_t __guardsize)
379 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
380extern int pthread_attr_getschedparam (__const pthread_attr_t *__restrict
381 __attr,
382 struct sched_param *__restrict __param)
383 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
384extern int pthread_attr_setschedparam (pthread_attr_t *__restrict __attr,
385 __const struct sched_param *__restrict
386 __param) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
387extern int pthread_attr_getschedpolicy (__const pthread_attr_t *__restrict
388 __attr, int *__restrict __policy)
389 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
390extern int pthread_attr_setschedpolicy (pthread_attr_t *__attr, int __policy)
391 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
392extern int pthread_attr_getinheritsched (__const pthread_attr_t *__restrict
393 __attr, int *__restrict __inherit)
394 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
395extern int pthread_attr_setinheritsched (pthread_attr_t *__attr,
396 int __inherit)
397 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
398extern int pthread_attr_getscope (__const pthread_attr_t *__restrict __attr,
399 int *__restrict __scope)
400 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
401extern int pthread_attr_setscope (pthread_attr_t *__attr, int __scope)
402 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
403extern int pthread_attr_getstackaddr (__const pthread_attr_t *__restrict
404 __attr, void **__restrict __stackaddr)
405 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))) __attribute__ ((__deprecated__));
406extern int pthread_attr_setstackaddr (pthread_attr_t *__attr,
407 void *__stackaddr)
408 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) __attribute__ ((__deprecated__));
409extern int pthread_attr_getstacksize (__const pthread_attr_t *__restrict
410 __attr, size_t *__restrict __stacksize)
411 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
412extern int pthread_attr_setstacksize (pthread_attr_t *__attr,
413 size_t __stacksize)
414 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
415extern int pthread_attr_getstack (__const pthread_attr_t *__restrict __attr,
416 void **__restrict __stackaddr,
417 size_t *__restrict __stacksize)
418 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3)));
419extern int pthread_attr_setstack (pthread_attr_t *__attr, void *__stackaddr,
420 size_t __stacksize) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
421extern int pthread_setschedparam (pthread_t __target_thread, int __policy,
422 __const struct sched_param *__param)
423 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3)));
424extern int pthread_getschedparam (pthread_t __target_thread,
425 int *__restrict __policy,
426 struct sched_param *__restrict __param)
427 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 3)));
428extern int pthread_setschedprio (pthread_t __target_thread, int __prio)
429 __attribute__ ((__nothrow__ , __leaf__));
430extern int pthread_once (pthread_once_t *__once_control,
431 void (*__init_routine) (void)) __attribute__ ((__nonnull__ (1, 2)));
432extern int pthread_setcancelstate (int __state, int *__oldstate);
433extern int pthread_setcanceltype (int __type, int *__oldtype);
434extern int pthread_cancel (pthread_t __th);
435extern void pthread_testcancel (void);
436typedef struct
437{
438 struct
439 {
440 __jmp_buf __cancel_jmp_buf;
441 int __mask_was_saved;
442 } __cancel_jmp_buf[1];
443 void *__pad[4];
444} __pthread_unwind_buf_t __attribute__ ((__aligned__));
445struct __pthread_cleanup_frame
446{
447 void (*__cancel_routine) (void *);
448 void *__cancel_arg;
449 int __do_it;
450 int __cancel_type;
451};
452extern void __pthread_register_cancel (__pthread_unwind_buf_t *__buf)
453 ;
454extern void __pthread_unregister_cancel (__pthread_unwind_buf_t *__buf)
455 ;
456extern void __pthread_unwind_next (__pthread_unwind_buf_t *__buf)
457 __attribute__ ((__noreturn__))
458 __attribute__ ((__weak__))
459 ;
460struct __jmp_buf_tag;
461extern int __sigsetjmp (struct __jmp_buf_tag *__env, int __savemask) __attribute__ ((__nothrow__ , __leaf__));
462extern int pthread_mutex_init (pthread_mutex_t *__mutex,
463 __const pthread_mutexattr_t *__mutexattr)
464 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
465extern int pthread_mutex_destroy (pthread_mutex_t *__mutex)
466 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
467extern int pthread_mutex_trylock (pthread_mutex_t *__mutex)
468 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
469extern int pthread_mutex_lock (pthread_mutex_t *__mutex)
470 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
471extern int pthread_mutex_timedlock (pthread_mutex_t *__restrict __mutex,
472 __const struct timespec *__restrict
473 __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
474extern int pthread_mutex_unlock (pthread_mutex_t *__mutex)
475 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
476extern int pthread_mutex_getprioceiling (__const pthread_mutex_t *
477 __restrict __mutex,
478 int *__restrict __prioceiling)
479 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
480extern int pthread_mutex_setprioceiling (pthread_mutex_t *__restrict __mutex,
481 int __prioceiling,
482 int *__restrict __old_ceiling)
483 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 3)));
484extern int pthread_mutex_consistent (pthread_mutex_t *__mutex)
485 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
486extern int pthread_mutexattr_init (pthread_mutexattr_t *__attr)
487 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
488extern int pthread_mutexattr_destroy (pthread_mutexattr_t *__attr)
489 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
490extern int pthread_mutexattr_getpshared (__const pthread_mutexattr_t *
491 __restrict __attr,
492 int *__restrict __pshared)
493 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
494extern int pthread_mutexattr_setpshared (pthread_mutexattr_t *__attr,
495 int __pshared)
496 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
497extern int pthread_mutexattr_gettype (__const pthread_mutexattr_t *__restrict
498 __attr, int *__restrict __kind)
499 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
500extern int pthread_mutexattr_settype (pthread_mutexattr_t *__attr, int __kind)
501 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
502extern int pthread_mutexattr_getprotocol (__const pthread_mutexattr_t *
503 __restrict __attr,
504 int *__restrict __protocol)
505 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
506extern int pthread_mutexattr_setprotocol (pthread_mutexattr_t *__attr,
507 int __protocol)
508 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
509extern int pthread_mutexattr_getprioceiling (__const pthread_mutexattr_t *
510 __restrict __attr,
511 int *__restrict __prioceiling)
512 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
513extern int pthread_mutexattr_setprioceiling (pthread_mutexattr_t *__attr,
514 int __prioceiling)
515 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
516extern int pthread_mutexattr_getrobust (__const pthread_mutexattr_t *__attr,
517 int *__robustness)
518 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
519extern int pthread_mutexattr_setrobust (pthread_mutexattr_t *__attr,
520 int __robustness)
521 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
522extern int pthread_rwlock_init (pthread_rwlock_t *__restrict __rwlock,
523 __const pthread_rwlockattr_t *__restrict
524 __attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
525extern int pthread_rwlock_destroy (pthread_rwlock_t *__rwlock)
526 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
527extern int pthread_rwlock_rdlock (pthread_rwlock_t *__rwlock)
528 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
529extern int pthread_rwlock_tryrdlock (pthread_rwlock_t *__rwlock)
530 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
531extern int pthread_rwlock_timedrdlock (pthread_rwlock_t *__restrict __rwlock,
532 __const struct timespec *__restrict
533 __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
534extern int pthread_rwlock_wrlock (pthread_rwlock_t *__rwlock)
535 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
536extern int pthread_rwlock_trywrlock (pthread_rwlock_t *__rwlock)
537 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
538extern int pthread_rwlock_timedwrlock (pthread_rwlock_t *__restrict __rwlock,
539 __const struct timespec *__restrict
540 __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
541extern int pthread_rwlock_unlock (pthread_rwlock_t *__rwlock)
542 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
543extern int pthread_rwlockattr_init (pthread_rwlockattr_t *__attr)
544 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
545extern int pthread_rwlockattr_destroy (pthread_rwlockattr_t *__attr)
546 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
547extern int pthread_rwlockattr_getpshared (__const pthread_rwlockattr_t *
548 __restrict __attr,
549 int *__restrict __pshared)
550 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
551extern int pthread_rwlockattr_setpshared (pthread_rwlockattr_t *__attr,
552 int __pshared)
553 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
554extern int pthread_rwlockattr_getkind_np (__const pthread_rwlockattr_t *
555 __restrict __attr,
556 int *__restrict __pref)
557 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
558extern int pthread_rwlockattr_setkind_np (pthread_rwlockattr_t *__attr,
559 int __pref) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
560extern int pthread_cond_init (pthread_cond_t *__restrict __cond,
561 __const pthread_condattr_t *__restrict
562 __cond_attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
563extern int pthread_cond_destroy (pthread_cond_t *__cond)
564 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
565extern int pthread_cond_signal (pthread_cond_t *__cond)
566 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
567extern int pthread_cond_broadcast (pthread_cond_t *__cond)
568 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
569extern int pthread_cond_wait (pthread_cond_t *__restrict __cond,
570 pthread_mutex_t *__restrict __mutex)
571 __attribute__ ((__nonnull__ (1, 2)));
572extern int pthread_cond_timedwait (pthread_cond_t *__restrict __cond,
573 pthread_mutex_t *__restrict __mutex,
574 __const struct timespec *__restrict
575 __abstime) __attribute__ ((__nonnull__ (1, 2, 3)));
576extern int pthread_condattr_init (pthread_condattr_t *__attr)
577 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
578extern int pthread_condattr_destroy (pthread_condattr_t *__attr)
579 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
580extern int pthread_condattr_getpshared (__const pthread_condattr_t *
581 __restrict __attr,
582 int *__restrict __pshared)
583 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
584extern int pthread_condattr_setpshared (pthread_condattr_t *__attr,
585 int __pshared) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
586extern int pthread_condattr_getclock (__const pthread_condattr_t *
587 __restrict __attr,
588 __clockid_t *__restrict __clock_id)
589 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
590extern int pthread_condattr_setclock (pthread_condattr_t *__attr,
591 __clockid_t __clock_id)
592 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
593extern int pthread_spin_init (pthread_spinlock_t *__lock, int __pshared)
594 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
595extern int pthread_spin_destroy (pthread_spinlock_t *__lock)
596 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
597extern int pthread_spin_lock (pthread_spinlock_t *__lock)
598 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
599extern int pthread_spin_trylock (pthread_spinlock_t *__lock)
600 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
601extern int pthread_spin_unlock (pthread_spinlock_t *__lock)
602 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
603extern int pthread_barrier_init (pthread_barrier_t *__restrict __barrier,
604 __const pthread_barrierattr_t *__restrict
605 __attr, unsigned int __count)
606 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
607extern int pthread_barrier_destroy (pthread_barrier_t *__barrier)
608 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
609extern int pthread_barrier_wait (pthread_barrier_t *__barrier)
610 __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
611extern int pthread_barrierattr_init (pthread_barrierattr_t *__attr)
612 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
613extern int pthread_barrierattr_destroy (pthread_barrierattr_t *__attr)
614 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
615extern int pthread_barrierattr_getpshared (__const pthread_barrierattr_t *
616 __restrict __attr,
617 int *__restrict __pshared)
618 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
619extern int pthread_barrierattr_setpshared (pthread_barrierattr_t *__attr,
620 int __pshared)
621 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
622extern int pthread_key_create (pthread_key_t *__key,
623 void (*__destr_function) (void *))
624 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
625extern int pthread_key_delete (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__));
626extern void *pthread_getspecific (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__));
627extern int pthread_setspecific (pthread_key_t __key,
628 __const void *__pointer) __attribute__ ((__nothrow__ , __leaf__)) ;
629extern int pthread_getcpuclockid (pthread_t __thread_id,
630 __clockid_t *__clock_id)
631 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
632extern int pthread_atfork (void (*__prepare) (void),
633 void (*__parent) (void),
634 void (*__child) (void)) __attribute__ ((__nothrow__ , __leaf__));
635
636volatile int max = 0x80000000;
637int storage[2*3];
638void __VERIFIER_atomic_CAS(
639 volatile int *v,
640 int e,
641 int u,
642 int *r)
643{
644 if(*v == e)
645 {
646 *v = u, *r = 1;
647 }
648 else
649 {
650 *r = 0;
651 }
652}
653inline void findMax(int offset){
654 int i;
655 int e;
656 int c;
657 int cret;
658 for(i = offset; i < offset+2; i++) {
659 e = storage[i];
660 while(1){
661 c = max;
662 if(e > c){
663 __VERIFIER_atomic_CAS(&max,c,e,&cret);
664 if(cret){
665 break;
666 }
667 }else{
668 break;
669 }
670 }
671 { if(!(e <= max)) { ERROR: __VERIFIER_error();(void)0; } };
672 }
673}
674void* thr1(void* arg) {
675 int offset=__VERIFIER_nondet_int();
676 __VERIFIER_assume(offset % 2 == 0 && offset >= 0 && offset < 2*3);
677 findMax(offset);
678 return 0;
679}
680int main(){
681 pthread_t t;
682 while(1) { pthread_create(&t, 0, thr1, 0); }
683}
Note: See TracBrowser for help on using the repository browser.