source: CIVL/mods/dev.civl.com/examples/pthread/svcomp/mix000_power.opt_false-unreach-call.i@ cb4d4f4

main test-branch
Last change on this file since cb4d4f4 was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

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