source: CIVL/mods/dev.civl.abc/examples/svcomp/sssc12_variant_true-unreach-call.i

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