1
2
3
4#line 19 "include/asm-generic/int-ll64.h"
5typedef signed char __s8;
6#line 22 "include/asm-generic/int-ll64.h"
7typedef short __s16;
8#line 23 "include/asm-generic/int-ll64.h"
9typedef unsigned short __u16;
10#line 25 "include/asm-generic/int-ll64.h"
11typedef int __s32;
12#line 26 "include/asm-generic/int-ll64.h"
13typedef unsigned int __u32;
14#line 29 "include/asm-generic/int-ll64.h"
15typedef long long __s64;
16#line 30 "include/asm-generic/int-ll64.h"
17typedef unsigned long long __u64;
18#line 43 "include/asm-generic/int-ll64.h"
19typedef unsigned char u8;
20#line 46 "include/asm-generic/int-ll64.h"
21typedef unsigned short u16;
22#line 49 "include/asm-generic/int-ll64.h"
23typedef unsigned int u32;
24#line 51 "include/asm-generic/int-ll64.h"
25typedef long long s64;
26#line 52 "include/asm-generic/int-ll64.h"
27typedef unsigned long long u64;
28#line 11 "include/asm-generic/types.h"
29typedef unsigned short umode_t;
30#line 11 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
31typedef unsigned int __kernel_mode_t;
32#line 14 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
33typedef int __kernel_pid_t;
34#line 16 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
35typedef unsigned int __kernel_uid_t;
36#line 17 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
37typedef unsigned int __kernel_gid_t;
38#line 18 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
39typedef unsigned long __kernel_size_t;
40#line 19 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
41typedef long __kernel_ssize_t;
42#line 21 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
43typedef long __kernel_time_t;
44#line 23 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
45typedef long __kernel_clock_t;
46#line 24 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
47typedef int __kernel_timer_t;
48#line 25 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
49typedef int __kernel_clockid_t;
50#line 32 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
51typedef long long __kernel_loff_t;
52#line 41 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
53typedef __kernel_uid_t __kernel_uid32_t;
54#line 42 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/posix_types_64.h"
55typedef __kernel_gid_t __kernel_gid32_t;
56#line 21 "include/linux/types.h"
57typedef __u32 __kernel_dev_t;
58#line 24 "include/linux/types.h"
59typedef __kernel_dev_t dev_t;
60#line 26 "include/linux/types.h"
61typedef __kernel_mode_t mode_t;
62#line 29 "include/linux/types.h"
63typedef __kernel_pid_t pid_t;
64#line 34 "include/linux/types.h"
65typedef __kernel_clockid_t clockid_t;
66#line 37 "include/linux/types.h"
67typedef _Bool bool;
68#line 39 "include/linux/types.h"
69typedef __kernel_uid32_t uid_t;
70#line 40 "include/linux/types.h"
71typedef __kernel_gid32_t gid_t;
72#line 53 "include/linux/types.h"
73typedef __kernel_loff_t loff_t;
74#line 62 "include/linux/types.h"
75typedef __kernel_size_t size_t;
76#line 67 "include/linux/types.h"
77typedef __kernel_ssize_t ssize_t;
78#line 77 "include/linux/types.h"
79typedef __kernel_time_t time_t;
80#line 110 "include/linux/types.h"
81typedef __s32 int32_t;
82#line 116 "include/linux/types.h"
83typedef __u32 uint32_t;
84#line 141 "include/linux/types.h"
85typedef unsigned long sector_t;
86#line 142 "include/linux/types.h"
87typedef unsigned long blkcnt_t;
88#line 201 "include/linux/types.h"
89typedef unsigned int gfp_t;
90#line 202 "include/linux/types.h"
91typedef unsigned int fmode_t;
92#line 214 "include/linux/types.h"
93struct __anonstruct_atomic_t_6 {
94 int counter ;
95};
96#line 214 "include/linux/types.h"
97typedef struct __anonstruct_atomic_t_6 atomic_t;
98#line 219 "include/linux/types.h"
99struct __anonstruct_atomic64_t_7 {
100 long counter ;
101};
102#line 219 "include/linux/types.h"
103typedef struct __anonstruct_atomic64_t_7 atomic64_t;
104#line 220 "include/linux/types.h"
105struct list_head {
106 struct list_head *next ;
107 struct list_head *prev ;
108};
109#line 225
110struct hlist_node;
111#line 225
112struct hlist_node;
113#line 225
114struct hlist_node;
115#line 225 "include/linux/types.h"
116struct hlist_head {
117 struct hlist_node *first ;
118};
119#line 229 "include/linux/types.h"
120struct hlist_node {
121 struct hlist_node *next ;
122 struct hlist_node **pprev ;
123};
124#line 58 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/alternative.h"
125struct module;
126#line 58
127struct module;
128#line 58
129struct module;
130#line 58
131struct module;
132#line 145 "include/linux/init.h"
133typedef void (*ctor_fn_t)(void);
134#line 48 "include/linux/dynamic_debug.h"
135struct bug_entry {
136 int bug_addr_disp ;
137 int file_disp ;
138 unsigned short line ;
139 unsigned short flags ;
140};
141#line 70 "include/asm-generic/bug.h"
142struct completion;
143#line 70
144struct completion;
145#line 70
146struct completion;
147#line 70
148struct completion;
149#line 71
150struct pt_regs;
151#line 71
152struct pt_regs;
153#line 71
154struct pt_regs;
155#line 71
156struct pt_regs;
157#line 321 "include/linux/kernel.h"
158struct pid;
159#line 321
160struct pid;
161#line 321
162struct pid;
163#line 321
164struct pid;
165#line 671
166struct timespec;
167#line 671
168struct timespec;
169#line 671
170struct timespec;
171#line 671
172struct timespec;
173#line 59 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/page_types.h"
174struct page;
175#line 59
176struct page;
177#line 59
178struct page;
179#line 59
180struct page;
181#line 21 "include/asm-generic/getorder.h"
182struct task_struct;
183#line 21
184struct task_struct;
185#line 21
186struct task_struct;
187#line 21
188struct task_struct;
189#line 23
190struct mm_struct;
191#line 23
192struct mm_struct;
193#line 23
194struct mm_struct;
195#line 23
196struct mm_struct;
197#line 215 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/segment.h"
198struct pt_regs {
199 unsigned long r15 ;
200 unsigned long r14 ;
201 unsigned long r13 ;
202 unsigned long r12 ;
203 unsigned long bp ;
204 unsigned long bx ;
205 unsigned long r11 ;
206 unsigned long r10 ;
207 unsigned long r9 ;
208 unsigned long r8 ;
209 unsigned long ax ;
210 unsigned long cx ;
211 unsigned long dx ;
212 unsigned long si ;
213 unsigned long di ;
214 unsigned long orig_ax ;
215 unsigned long ip ;
216 unsigned long cs ;
217 unsigned long flags ;
218 unsigned long sp ;
219 unsigned long ss ;
220};
221#line 282 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/ptrace.h"
222struct kernel_vm86_regs {
223 struct pt_regs pt ;
224 unsigned short es ;
225 unsigned short __esh ;
226 unsigned short ds ;
227 unsigned short __dsh ;
228 unsigned short fs ;
229 unsigned short __fsh ;
230 unsigned short gs ;
231 unsigned short __gsh ;
232};
233#line 203 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/vm86.h"
234union __anonunion_ldv_2292_12 {
235 struct pt_regs *regs ;
236 struct kernel_vm86_regs *vm86 ;
237};
238#line 203 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/vm86.h"
239struct math_emu_info {
240 long ___orig_eip ;
241 union __anonunion_ldv_2292_12 ldv_2292 ;
242};
243#line 13 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_64_types.h"
244typedef unsigned long pgdval_t;
245#line 14 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_64_types.h"
246typedef unsigned long pgprotval_t;
247#line 18 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_64_types.h"
248struct pgprot {
249 pgprotval_t pgprot ;
250};
251#line 190 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
252typedef struct pgprot pgprot_t;
253#line 192 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
254struct __anonstruct_pgd_t_15 {
255 pgdval_t pgd ;
256};
257#line 192 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
258typedef struct __anonstruct_pgd_t_15 pgd_t;
259#line 280 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
260typedef struct page *pgtable_t;
261#line 288
262struct file;
263#line 288
264struct file;
265#line 288
266struct file;
267#line 288
268struct file;
269#line 303
270struct seq_file;
271#line 303
272struct seq_file;
273#line 303
274struct seq_file;
275#line 303
276struct seq_file;
277#line 335 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
278struct __anonstruct_ldv_2526_19 {
279 unsigned int a ;
280 unsigned int b ;
281};
282#line 335 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
283struct __anonstruct_ldv_2541_20 {
284 u16 limit0 ;
285 u16 base0 ;
286 unsigned char base1 ;
287 unsigned char type : 4 ;
288 unsigned char s : 1 ;
289 unsigned char dpl : 2 ;
290 unsigned char p : 1 ;
291 unsigned char limit : 4 ;
292 unsigned char avl : 1 ;
293 unsigned char l : 1 ;
294 unsigned char d : 1 ;
295 unsigned char g : 1 ;
296 unsigned char base2 ;
297};
298#line 335 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
299union __anonunion_ldv_2542_18 {
300 struct __anonstruct_ldv_2526_19 ldv_2526 ;
301 struct __anonstruct_ldv_2541_20 ldv_2541 ;
302};
303#line 335 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
304struct desc_struct {
305 union __anonunion_ldv_2542_18 ldv_2542 ;
306};
307#line 122 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/desc_defs.h"
308struct thread_struct;
309#line 122
310struct thread_struct;
311#line 122
312struct thread_struct;
313#line 122
314struct thread_struct;
315#line 124
316struct cpumask;
317#line 124
318struct cpumask;
319#line 124
320struct cpumask;
321#line 124
322struct cpumask;
323#line 320 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/paravirt_types.h"
324struct arch_spinlock;
325#line 320
326struct arch_spinlock;
327#line 320
328struct arch_spinlock;
329#line 320
330struct arch_spinlock;
331#line 304 "include/linux/bitmap.h"
332struct cpumask {
333 unsigned long bits[64U] ;
334};
335#line 13 "include/linux/cpumask.h"
336typedef struct cpumask cpumask_t;
337#line 622 "include/linux/cpumask.h"
338typedef struct cpumask *cpumask_var_t;
339#line 277 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
340struct i387_fsave_struct {
341 u32 cwd ;
342 u32 swd ;
343 u32 twd ;
344 u32 fip ;
345 u32 fcs ;
346 u32 foo ;
347 u32 fos ;
348 u32 st_space[20U] ;
349 u32 status ;
350};
351#line 295 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
352struct __anonstruct_ldv_5171_24 {
353 u64 rip ;
354 u64 rdp ;
355};
356#line 295 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
357struct __anonstruct_ldv_5177_25 {
358 u32 fip ;
359 u32 fcs ;
360 u32 foo ;
361 u32 fos ;
362};
363#line 295 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
364union __anonunion_ldv_5178_23 {
365 struct __anonstruct_ldv_5171_24 ldv_5171 ;
366 struct __anonstruct_ldv_5177_25 ldv_5177 ;
367};
368#line 295 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
369union __anonunion_ldv_5187_26 {
370 u32 padding1[12U] ;
371 u32 sw_reserved[12U] ;
372};
373#line 295 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
374struct i387_fxsave_struct {
375 u16 cwd ;
376 u16 swd ;
377 u16 twd ;
378 u16 fop ;
379 union __anonunion_ldv_5178_23 ldv_5178 ;
380 u32 mxcsr ;
381 u32 mxcsr_mask ;
382 u32 st_space[32U] ;
383 u32 xmm_space[64U] ;
384 u32 padding[12U] ;
385 union __anonunion_ldv_5187_26 ldv_5187 ;
386};
387#line 329 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
388struct i387_soft_struct {
389 u32 cwd ;
390 u32 swd ;
391 u32 twd ;
392 u32 fip ;
393 u32 fcs ;
394 u32 foo ;
395 u32 fos ;
396 u32 st_space[20U] ;
397 u8 ftop ;
398 u8 changed ;
399 u8 lookahead ;
400 u8 no_update ;
401 u8 rm ;
402 u8 alimit ;
403 struct math_emu_info *info ;
404 u32 entry_eip ;
405};
406#line 350 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
407struct ymmh_struct {
408 u32 ymmh_space[64U] ;
409};
410#line 355 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
411struct xsave_hdr_struct {
412 u64 xstate_bv ;
413 u64 reserved1[2U] ;
414 u64 reserved2[5U] ;
415};
416#line 361 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
417struct xsave_struct {
418 struct i387_fxsave_struct i387 ;
419 struct xsave_hdr_struct xsave_hdr ;
420 struct ymmh_struct ymmh ;
421};
422#line 367 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
423union thread_xstate {
424 struct i387_fsave_struct fsave ;
425 struct i387_fxsave_struct fxsave ;
426 struct i387_soft_struct soft ;
427 struct xsave_struct xsave ;
428};
429#line 375 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
430struct fpu {
431 union thread_xstate *state ;
432};
433#line 421
434struct kmem_cache;
435#line 421
436struct kmem_cache;
437#line 421
438struct kmem_cache;
439#line 422
440struct perf_event;
441#line 422
442struct perf_event;
443#line 422
444struct perf_event;
445#line 422
446struct perf_event;
447#line 423 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
448struct thread_struct {
449 struct desc_struct tls_array[3U] ;
450 unsigned long sp0 ;
451 unsigned long sp ;
452 unsigned long usersp ;
453 unsigned short es ;
454 unsigned short ds ;
455 unsigned short fsindex ;
456 unsigned short gsindex ;
457 unsigned long fs ;
458 unsigned long gs ;
459 struct perf_event *ptrace_bps[4U] ;
460 unsigned long debugreg6 ;
461 unsigned long ptrace_dr7 ;
462 unsigned long cr2 ;
463 unsigned long trap_no ;
464 unsigned long error_code ;
465 struct fpu fpu ;
466 unsigned long *io_bitmap_ptr ;
467 unsigned long iopl ;
468 unsigned int io_bitmap_max ;
469};
470#line 23 "include/asm-generic/atomic-long.h"
471typedef atomic64_t atomic_long_t;
472#line 8 "include/linux/bottom_half.h"
473struct arch_spinlock {
474 unsigned int slock ;
475};
476#line 10 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/spinlock_types.h"
477typedef struct arch_spinlock arch_spinlock_t;
478#line 16 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/spinlock_types.h"
479struct __anonstruct_arch_rwlock_t_29 {
480 unsigned int lock ;
481};
482#line 16 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/spinlock_types.h"
483typedef struct __anonstruct_arch_rwlock_t_29 arch_rwlock_t;
484#line 17
485struct lockdep_map;
486#line 17
487struct lockdep_map;
488#line 17
489struct lockdep_map;
490#line 17
491struct lockdep_map;
492#line 55 "include/linux/debug_locks.h"
493struct stack_trace {
494 unsigned int nr_entries ;
495 unsigned int max_entries ;
496 unsigned long *entries ;
497 int skip ;
498};
499#line 26 "include/linux/stacktrace.h"
500struct lockdep_subclass_key {
501 char __one_byte ;
502};
503#line 53 "include/linux/lockdep.h"
504struct lock_class_key {
505 struct lockdep_subclass_key subkeys[8U] ;
506};
507#line 59 "include/linux/lockdep.h"
508struct lock_class {
509 struct list_head hash_entry ;
510 struct list_head lock_entry ;
511 struct lockdep_subclass_key *key ;
512 unsigned int subclass ;
513 unsigned int dep_gen_id ;
514 unsigned long usage_mask ;
515 struct stack_trace usage_traces[13U] ;
516 struct list_head locks_after ;
517 struct list_head locks_before ;
518 unsigned int version ;
519 unsigned long ops ;
520 char const *name ;
521 int name_version ;
522 unsigned long contention_point[4U] ;
523 unsigned long contending_point[4U] ;
524};
525#line 144 "include/linux/lockdep.h"
526struct lockdep_map {
527 struct lock_class_key *key ;
528 struct lock_class *class_cache[2U] ;
529 char const *name ;
530 int cpu ;
531 unsigned long ip ;
532};
533#line 187 "include/linux/lockdep.h"
534struct held_lock {
535 u64 prev_chain_key ;
536 unsigned long acquire_ip ;
537 struct lockdep_map *instance ;
538 struct lockdep_map *nest_lock ;
539 u64 waittime_stamp ;
540 u64 holdtime_stamp ;
541 unsigned short class_idx : 13 ;
542 unsigned char irq_context : 2 ;
543 unsigned char trylock : 1 ;
544 unsigned char read : 2 ;
545 unsigned char check : 2 ;
546 unsigned char hardirqs_off : 1 ;
547 unsigned short references : 11 ;
548};
549#line 552 "include/linux/lockdep.h"
550struct raw_spinlock {
551 arch_spinlock_t raw_lock ;
552 unsigned int magic ;
553 unsigned int owner_cpu ;
554 void *owner ;
555 struct lockdep_map dep_map ;
556};
557#line 32 "include/linux/spinlock_types.h"
558typedef struct raw_spinlock raw_spinlock_t;
559#line 33 "include/linux/spinlock_types.h"
560struct __anonstruct_ldv_6059_31 {
561 u8 __padding[24U] ;
562 struct lockdep_map dep_map ;
563};
564#line 33 "include/linux/spinlock_types.h"
565union __anonunion_ldv_6060_30 {
566 struct raw_spinlock rlock ;
567 struct __anonstruct_ldv_6059_31 ldv_6059 ;
568};
569#line 33 "include/linux/spinlock_types.h"
570struct spinlock {
571 union __anonunion_ldv_6060_30 ldv_6060 ;
572};
573#line 76 "include/linux/spinlock_types.h"
574typedef struct spinlock spinlock_t;
575#line 23 "include/linux/rwlock_types.h"
576struct __anonstruct_rwlock_t_32 {
577 arch_rwlock_t raw_lock ;
578 unsigned int magic ;
579 unsigned int owner_cpu ;
580 void *owner ;
581 struct lockdep_map dep_map ;
582};
583#line 23 "include/linux/rwlock_types.h"
584typedef struct __anonstruct_rwlock_t_32 rwlock_t;
585#line 110 "include/linux/seqlock.h"
586struct seqcount {
587 unsigned int sequence ;
588};
589#line 121 "include/linux/seqlock.h"
590typedef struct seqcount seqcount_t;
591#line 233 "include/linux/seqlock.h"
592struct timespec {
593 __kernel_time_t tv_sec ;
594 long tv_nsec ;
595};
596#line 286 "include/linux/time.h"
597struct kstat {
598 u64 ino ;
599 dev_t dev ;
600 umode_t mode ;
601 unsigned int nlink ;
602 uid_t uid ;
603 gid_t gid ;
604 dev_t rdev ;
605 loff_t size ;
606 struct timespec atime ;
607 struct timespec mtime ;
608 struct timespec ctime ;
609 unsigned long blksize ;
610 unsigned long long blocks ;
611};
612#line 49 "include/linux/wait.h"
613struct __wait_queue_head {
614 spinlock_t lock ;
615 struct list_head task_list ;
616};
617#line 54 "include/linux/wait.h"
618typedef struct __wait_queue_head wait_queue_head_t;
619#line 96 "include/linux/nodemask.h"
620struct __anonstruct_nodemask_t_34 {
621 unsigned long bits[16U] ;
622};
623#line 96 "include/linux/nodemask.h"
624typedef struct __anonstruct_nodemask_t_34 nodemask_t;
625#line 640 "include/linux/mmzone.h"
626struct mutex {
627 atomic_t count ;
628 spinlock_t wait_lock ;
629 struct list_head wait_list ;
630 struct task_struct *owner ;
631 char const *name ;
632 void *magic ;
633 struct lockdep_map dep_map ;
634};
635#line 63 "include/linux/mutex.h"
636struct mutex_waiter {
637 struct list_head list ;
638 struct task_struct *task ;
639 void *magic ;
640};
641#line 171
642struct rw_semaphore;
643#line 171
644struct rw_semaphore;
645#line 171
646struct rw_semaphore;
647#line 171
648struct rw_semaphore;
649#line 172 "include/linux/mutex.h"
650struct rw_semaphore {
651 long count ;
652 spinlock_t wait_lock ;
653 struct list_head wait_list ;
654 struct lockdep_map dep_map ;
655};
656#line 175 "include/linux/ioport.h"
657struct device;
658#line 175
659struct device;
660#line 175
661struct device;
662#line 175
663struct device;
664#line 312 "include/linux/jiffies.h"
665union ktime {
666 s64 tv64 ;
667};
668#line 59 "include/linux/ktime.h"
669typedef union ktime ktime_t;
670#line 99 "include/linux/debugobjects.h"
671struct tvec_base;
672#line 99
673struct tvec_base;
674#line 99
675struct tvec_base;
676#line 99
677struct tvec_base;
678#line 100 "include/linux/debugobjects.h"
679struct timer_list {
680 struct list_head entry ;
681 unsigned long expires ;
682 struct tvec_base *base ;
683 void (*function)(unsigned long ) ;
684 unsigned long data ;
685 int slack ;
686 int start_pid ;
687 void *start_site ;
688 char start_comm[16U] ;
689 struct lockdep_map lockdep_map ;
690};
691#line 289 "include/linux/timer.h"
692struct hrtimer;
693#line 289
694struct hrtimer;
695#line 289
696struct hrtimer;
697#line 289
698struct hrtimer;
699#line 290
700enum hrtimer_restart;
701#line 290
702enum hrtimer_restart;
703#line 290
704enum hrtimer_restart;
705#line 302
706struct work_struct;
707#line 302
708struct work_struct;
709#line 302
710struct work_struct;
711#line 302
712struct work_struct;
713#line 45 "include/linux/workqueue.h"
714struct work_struct {
715 atomic_long_t data ;
716 struct list_head entry ;
717 void (*func)(struct work_struct * ) ;
718 struct lockdep_map lockdep_map ;
719};
720#line 86 "include/linux/workqueue.h"
721struct delayed_work {
722 struct work_struct work ;
723 struct timer_list timer ;
724};
725#line 443 "include/linux/workqueue.h"
726struct completion {
727 unsigned int done ;
728 wait_queue_head_t wait ;
729};
730#line 46 "include/linux/pm.h"
731struct pm_message {
732 int event ;
733};
734#line 52 "include/linux/pm.h"
735typedef struct pm_message pm_message_t;
736#line 53 "include/linux/pm.h"
737struct dev_pm_ops {
738 int (*prepare)(struct device * ) ;
739 void (*complete)(struct device * ) ;
740 int (*suspend)(struct device * ) ;
741 int (*resume)(struct device * ) ;
742 int (*freeze)(struct device * ) ;
743 int (*thaw)(struct device * ) ;
744 int (*poweroff)(struct device * ) ;
745 int (*restore)(struct device * ) ;
746 int (*suspend_noirq)(struct device * ) ;
747 int (*resume_noirq)(struct device * ) ;
748 int (*freeze_noirq)(struct device * ) ;
749 int (*thaw_noirq)(struct device * ) ;
750 int (*poweroff_noirq)(struct device * ) ;
751 int (*restore_noirq)(struct device * ) ;
752 int (*runtime_suspend)(struct device * ) ;
753 int (*runtime_resume)(struct device * ) ;
754 int (*runtime_idle)(struct device * ) ;
755};
756#line 272
757enum rpm_status {
758 RPM_ACTIVE = 0,
759 RPM_RESUMING = 1,
760 RPM_SUSPENDED = 2,
761 RPM_SUSPENDING = 3
762} ;
763#line 279
764enum rpm_request {
765 RPM_REQ_NONE = 0,
766 RPM_REQ_IDLE = 1,
767 RPM_REQ_SUSPEND = 2,
768 RPM_REQ_AUTOSUSPEND = 3,
769 RPM_REQ_RESUME = 4
770} ;
771#line 287
772struct wakeup_source;
773#line 287
774struct wakeup_source;
775#line 287
776struct wakeup_source;
777#line 287
778struct wakeup_source;
779#line 288 "include/linux/pm.h"
780struct dev_pm_info {
781 pm_message_t power_state ;
782 unsigned char can_wakeup : 1 ;
783 unsigned char async_suspend : 1 ;
784 bool is_prepared ;
785 bool is_suspended ;
786 spinlock_t lock ;
787 struct list_head entry ;
788 struct completion completion ;
789 struct wakeup_source *wakeup ;
790 struct timer_list suspend_timer ;
791 unsigned long timer_expires ;
792 struct work_struct work ;
793 wait_queue_head_t wait_queue ;
794 atomic_t usage_count ;
795 atomic_t child_count ;
796 unsigned char disable_depth : 3 ;
797 unsigned char ignore_children : 1 ;
798 unsigned char idle_notification : 1 ;
799 unsigned char request_pending : 1 ;
800 unsigned char deferred_resume : 1 ;
801 unsigned char run_wake : 1 ;
802 unsigned char runtime_auto : 1 ;
803 unsigned char no_callbacks : 1 ;
804 unsigned char irq_safe : 1 ;
805 unsigned char use_autosuspend : 1 ;
806 unsigned char timer_autosuspends : 1 ;
807 enum rpm_request request ;
808 enum rpm_status runtime_status ;
809 int runtime_error ;
810 int autosuspend_delay ;
811 unsigned long last_busy ;
812 unsigned long active_jiffies ;
813 unsigned long suspended_jiffies ;
814 unsigned long accounting_timestamp ;
815 void *subsys_data ;
816};
817#line 469 "include/linux/pm.h"
818struct dev_power_domain {
819 struct dev_pm_ops ops ;
820};
821#line 22 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/mmu.h"
822struct __anonstruct_mm_context_t_99 {
823 void *ldt ;
824 int size ;
825 unsigned short ia32_compat ;
826 struct mutex lock ;
827 void *vdso ;
828};
829#line 22 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/mmu.h"
830typedef struct __anonstruct_mm_context_t_99 mm_context_t;
831#line 71 "include/asm-generic/iomap.h"
832struct vm_area_struct;
833#line 71
834struct vm_area_struct;
835#line 71
836struct vm_area_struct;
837#line 71
838struct vm_area_struct;
839#line 53 "include/linux/rcupdate.h"
840struct rcu_head {
841 struct rcu_head *next ;
842 void (*func)(struct rcu_head * ) ;
843};
844#line 841
845struct nsproxy;
846#line 841
847struct nsproxy;
848#line 841
849struct nsproxy;
850#line 841
851struct nsproxy;
852#line 36 "include/linux/kmod.h"
853struct cred;
854#line 36
855struct cred;
856#line 36
857struct cred;
858#line 36
859struct cred;
860#line 27 "include/linux/elf.h"
861typedef __u64 Elf64_Addr;
862#line 28 "include/linux/elf.h"
863typedef __u16 Elf64_Half;
864#line 32 "include/linux/elf.h"
865typedef __u32 Elf64_Word;
866#line 33 "include/linux/elf.h"
867typedef __u64 Elf64_Xword;
868#line 202 "include/linux/elf.h"
869struct elf64_sym {
870 Elf64_Word st_name ;
871 unsigned char st_info ;
872 unsigned char st_other ;
873 Elf64_Half st_shndx ;
874 Elf64_Addr st_value ;
875 Elf64_Xword st_size ;
876};
877#line 210 "include/linux/elf.h"
878typedef struct elf64_sym Elf64_Sym;
879#line 444
880struct sock;
881#line 444
882struct sock;
883#line 444
884struct sock;
885#line 444
886struct sock;
887#line 445
888struct kobject;
889#line 445
890struct kobject;
891#line 445
892struct kobject;
893#line 445
894struct kobject;
895#line 446
896enum kobj_ns_type {
897 KOBJ_NS_TYPE_NONE = 0,
898 KOBJ_NS_TYPE_NET = 1,
899 KOBJ_NS_TYPES = 2
900} ;
901#line 452 "include/linux/elf.h"
902struct kobj_ns_type_operations {
903 enum kobj_ns_type type ;
904 void *(*grab_current_ns)(void) ;
905 void const *(*netlink_ns)(struct sock * ) ;
906 void const *(*initial_ns)(void) ;
907 void (*drop_ns)(void * ) ;
908};
909#line 57 "include/linux/kobject_ns.h"
910struct attribute {
911 char const *name ;
912 mode_t mode ;
913 struct lock_class_key *key ;
914 struct lock_class_key skey ;
915};
916#line 33 "include/linux/sysfs.h"
917struct attribute_group {
918 char const *name ;
919 mode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
920 struct attribute **attrs ;
921};
922#line 62 "include/linux/sysfs.h"
923struct bin_attribute {
924 struct attribute attr ;
925 size_t size ;
926 void *private ;
927 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
928 loff_t , size_t ) ;
929 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
930 loff_t , size_t ) ;
931 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
932};
933#line 98 "include/linux/sysfs.h"
934struct sysfs_ops {
935 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
936 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
937};
938#line 116
939struct sysfs_dirent;
940#line 116
941struct sysfs_dirent;
942#line 116
943struct sysfs_dirent;
944#line 116
945struct sysfs_dirent;
946#line 181 "include/linux/sysfs.h"
947struct kref {
948 atomic_t refcount ;
949};
950#line 49 "include/linux/kobject.h"
951struct kset;
952#line 49
953struct kset;
954#line 49
955struct kset;
956#line 49
957struct kobj_type;
958#line 49
959struct kobj_type;
960#line 49
961struct kobj_type;
962#line 49 "include/linux/kobject.h"
963struct kobject {
964 char const *name ;
965 struct list_head entry ;
966 struct kobject *parent ;
967 struct kset *kset ;
968 struct kobj_type *ktype ;
969 struct sysfs_dirent *sd ;
970 struct kref kref ;
971 unsigned char state_initialized : 1 ;
972 unsigned char state_in_sysfs : 1 ;
973 unsigned char state_add_uevent_sent : 1 ;
974 unsigned char state_remove_uevent_sent : 1 ;
975 unsigned char uevent_suppress : 1 ;
976};
977#line 109 "include/linux/kobject.h"
978struct kobj_type {
979 void (*release)(struct kobject * ) ;
980 struct sysfs_ops const *sysfs_ops ;
981 struct attribute **default_attrs ;
982 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
983 void const *(*namespace)(struct kobject * ) ;
984};
985#line 117 "include/linux/kobject.h"
986struct kobj_uevent_env {
987 char *envp[32U] ;
988 int envp_idx ;
989 char buf[2048U] ;
990 int buflen ;
991};
992#line 124 "include/linux/kobject.h"
993struct kset_uevent_ops {
994 int (* const filter)(struct kset * , struct kobject * ) ;
995 char const *(* const name)(struct kset * , struct kobject * ) ;
996 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
997};
998#line 141 "include/linux/kobject.h"
999struct kset {
1000 struct list_head list ;
1001 spinlock_t list_lock ;
1002 struct kobject kobj ;
1003 struct kset_uevent_ops const *uevent_ops ;
1004};
1005#line 219
1006struct kernel_param;
1007#line 219
1008struct kernel_param;
1009#line 219
1010struct kernel_param;
1011#line 219
1012struct kernel_param;
1013#line 220 "include/linux/kobject.h"
1014struct kernel_param_ops {
1015 int (*set)(char const * , struct kernel_param const * ) ;
1016 int (*get)(char * , struct kernel_param const * ) ;
1017 void (*free)(void * ) ;
1018};
1019#line 44 "include/linux/moduleparam.h"
1020struct kparam_string;
1021#line 44
1022struct kparam_string;
1023#line 44
1024struct kparam_string;
1025#line 44
1026struct kparam_array;
1027#line 44
1028struct kparam_array;
1029#line 44
1030struct kparam_array;
1031#line 44 "include/linux/moduleparam.h"
1032union __anonunion_ldv_12924_129 {
1033 void *arg ;
1034 struct kparam_string const *str ;
1035 struct kparam_array const *arr ;
1036};
1037#line 44 "include/linux/moduleparam.h"
1038struct kernel_param {
1039 char const *name ;
1040 struct kernel_param_ops const *ops ;
1041 u16 perm ;
1042 u16 flags ;
1043 union __anonunion_ldv_12924_129 ldv_12924 ;
1044};
1045#line 59 "include/linux/moduleparam.h"
1046struct kparam_string {
1047 unsigned int maxlen ;
1048 char *string ;
1049};
1050#line 65 "include/linux/moduleparam.h"
1051struct kparam_array {
1052 unsigned int max ;
1053 unsigned int elemsize ;
1054 unsigned int *num ;
1055 struct kernel_param_ops const *ops ;
1056 void *elem ;
1057};
1058#line 404 "include/linux/moduleparam.h"
1059struct jump_label_key {
1060 atomic_t enabled ;
1061};
1062#line 99 "include/linux/jump_label.h"
1063struct tracepoint;
1064#line 99
1065struct tracepoint;
1066#line 99
1067struct tracepoint;
1068#line 99
1069struct tracepoint;
1070#line 100 "include/linux/jump_label.h"
1071struct tracepoint_func {
1072 void *func ;
1073 void *data ;
1074};
1075#line 29 "include/linux/tracepoint.h"
1076struct tracepoint {
1077 char const *name ;
1078 struct jump_label_key key ;
1079 void (*regfunc)(void) ;
1080 void (*unregfunc)(void) ;
1081 struct tracepoint_func *funcs ;
1082};
1083#line 84 "include/linux/tracepoint.h"
1084struct mod_arch_specific {
1085
1086};
1087#line 127 "include/trace/events/module.h"
1088struct kernel_symbol {
1089 unsigned long value ;
1090 char const *name ;
1091};
1092#line 48 "include/linux/module.h"
1093struct module_attribute {
1094 struct attribute attr ;
1095 ssize_t (*show)(struct module_attribute * , struct module * , char * ) ;
1096 ssize_t (*store)(struct module_attribute * , struct module * , char const * ,
1097 size_t ) ;
1098 void (*setup)(struct module * , char const * ) ;
1099 int (*test)(struct module * ) ;
1100 void (*free)(struct module * ) ;
1101};
1102#line 68
1103struct module_param_attrs;
1104#line 68
1105struct module_param_attrs;
1106#line 68
1107struct module_param_attrs;
1108#line 68 "include/linux/module.h"
1109struct module_kobject {
1110 struct kobject kobj ;
1111 struct module *mod ;
1112 struct kobject *drivers_dir ;
1113 struct module_param_attrs *mp ;
1114};
1115#line 81
1116struct exception_table_entry;
1117#line 81
1118struct exception_table_entry;
1119#line 81
1120struct exception_table_entry;
1121#line 81
1122struct exception_table_entry;
1123#line 218
1124enum module_state {
1125 MODULE_STATE_LIVE = 0,
1126 MODULE_STATE_COMING = 1,
1127 MODULE_STATE_GOING = 2
1128} ;
1129#line 224 "include/linux/module.h"
1130struct module_ref {
1131 unsigned int incs ;
1132 unsigned int decs ;
1133};
1134#line 418
1135struct module_sect_attrs;
1136#line 418
1137struct module_sect_attrs;
1138#line 418
1139struct module_sect_attrs;
1140#line 418
1141struct module_notes_attrs;
1142#line 418
1143struct module_notes_attrs;
1144#line 418
1145struct module_notes_attrs;
1146#line 418
1147struct ftrace_event_call;
1148#line 418
1149struct ftrace_event_call;
1150#line 418
1151struct ftrace_event_call;
1152#line 418 "include/linux/module.h"
1153struct module {
1154 enum module_state state ;
1155 struct list_head list ;
1156 char name[56U] ;
1157 struct module_kobject mkobj ;
1158 struct module_attribute *modinfo_attrs ;
1159 char const *version ;
1160 char const *srcversion ;
1161 struct kobject *holders_dir ;
1162 struct kernel_symbol const *syms ;
1163 unsigned long const *crcs ;
1164 unsigned int num_syms ;
1165 struct kernel_param *kp ;
1166 unsigned int num_kp ;
1167 unsigned int num_gpl_syms ;
1168 struct kernel_symbol const *gpl_syms ;
1169 unsigned long const *gpl_crcs ;
1170 struct kernel_symbol const *unused_syms ;
1171 unsigned long const *unused_crcs ;
1172 unsigned int num_unused_syms ;
1173 unsigned int num_unused_gpl_syms ;
1174 struct kernel_symbol const *unused_gpl_syms ;
1175 unsigned long const *unused_gpl_crcs ;
1176 struct kernel_symbol const *gpl_future_syms ;
1177 unsigned long const *gpl_future_crcs ;
1178 unsigned int num_gpl_future_syms ;
1179 unsigned int num_exentries ;
1180 struct exception_table_entry *extable ;
1181 int (*init)(void) ;
1182 void *module_init ;
1183 void *module_core ;
1184 unsigned int init_size ;
1185 unsigned int core_size ;
1186 unsigned int init_text_size ;
1187 unsigned int core_text_size ;
1188 unsigned int init_ro_size ;
1189 unsigned int core_ro_size ;
1190 struct mod_arch_specific arch ;
1191 unsigned int taints ;
1192 unsigned int num_bugs ;
1193 struct list_head bug_list ;
1194 struct bug_entry *bug_table ;
1195 Elf64_Sym *symtab ;
1196 Elf64_Sym *core_symtab ;
1197 unsigned int num_symtab ;
1198 unsigned int core_num_syms ;
1199 char *strtab ;
1200 char *core_strtab ;
1201 struct module_sect_attrs *sect_attrs ;
1202 struct module_notes_attrs *notes_attrs ;
1203 char *args ;
1204 void *percpu ;
1205 unsigned int percpu_size ;
1206 unsigned int num_tracepoints ;
1207 struct tracepoint * const *tracepoints_ptrs ;
1208 unsigned int num_trace_bprintk_fmt ;
1209 char const **trace_bprintk_fmt_start ;
1210 struct ftrace_event_call **trace_events ;
1211 unsigned int num_trace_events ;
1212 unsigned int num_ftrace_callsites ;
1213 unsigned long *ftrace_callsites ;
1214 struct list_head source_list ;
1215 struct list_head target_list ;
1216 struct task_struct *waiter ;
1217 void (*exit)(void) ;
1218 struct module_ref *refptr ;
1219 ctor_fn_t (**ctors)(void) ;
1220 unsigned int num_ctors ;
1221};
1222#line 140 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
1223struct block_device;
1224#line 140
1225struct block_device;
1226#line 140
1227struct block_device;
1228#line 140
1229struct block_device;
1230#line 92 "include/linux/bit_spinlock.h"
1231struct hlist_bl_node;
1232#line 92
1233struct hlist_bl_node;
1234#line 92
1235struct hlist_bl_node;
1236#line 92 "include/linux/bit_spinlock.h"
1237struct hlist_bl_head {
1238 struct hlist_bl_node *first ;
1239};
1240#line 36 "include/linux/list_bl.h"
1241struct hlist_bl_node {
1242 struct hlist_bl_node *next ;
1243 struct hlist_bl_node **pprev ;
1244};
1245#line 114 "include/linux/rculist_bl.h"
1246struct nameidata;
1247#line 114
1248struct nameidata;
1249#line 114
1250struct nameidata;
1251#line 114
1252struct nameidata;
1253#line 115
1254struct path;
1255#line 115
1256struct path;
1257#line 115
1258struct path;
1259#line 115
1260struct path;
1261#line 116
1262struct vfsmount;
1263#line 116
1264struct vfsmount;
1265#line 116
1266struct vfsmount;
1267#line 116
1268struct vfsmount;
1269#line 117 "include/linux/rculist_bl.h"
1270struct qstr {
1271 unsigned int hash ;
1272 unsigned int len ;
1273 unsigned char const *name ;
1274};
1275#line 100 "include/linux/dcache.h"
1276struct inode;
1277#line 100
1278struct inode;
1279#line 100
1280struct inode;
1281#line 100
1282struct dentry_operations;
1283#line 100
1284struct dentry_operations;
1285#line 100
1286struct dentry_operations;
1287#line 100
1288struct super_block;
1289#line 100
1290struct super_block;
1291#line 100
1292struct super_block;
1293#line 100 "include/linux/dcache.h"
1294union __anonunion_d_u_130 {
1295 struct list_head d_child ;
1296 struct rcu_head d_rcu ;
1297};
1298#line 100 "include/linux/dcache.h"
1299struct dentry {
1300 unsigned int d_flags ;
1301 seqcount_t d_seq ;
1302 struct hlist_bl_node d_hash ;
1303 struct dentry *d_parent ;
1304 struct qstr d_name ;
1305 struct inode *d_inode ;
1306 unsigned char d_iname[32U] ;
1307 unsigned int d_count ;
1308 spinlock_t d_lock ;
1309 struct dentry_operations const *d_op ;
1310 struct super_block *d_sb ;
1311 unsigned long d_time ;
1312 void *d_fsdata ;
1313 struct list_head d_lru ;
1314 union __anonunion_d_u_130 d_u ;
1315 struct list_head d_subdirs ;
1316 struct list_head d_alias ;
1317};
1318#line 151 "include/linux/dcache.h"
1319struct dentry_operations {
1320 int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1321 int (*d_hash)(struct dentry const * , struct inode const * , struct qstr * ) ;
1322 int (*d_compare)(struct dentry const * , struct inode const * , struct dentry const * ,
1323 struct inode const * , unsigned int , char const * , struct qstr const * ) ;
1324 int (*d_delete)(struct dentry const * ) ;
1325 void (*d_release)(struct dentry * ) ;
1326 void (*d_iput)(struct dentry * , struct inode * ) ;
1327 char *(*d_dname)(struct dentry * , char * , int ) ;
1328 struct vfsmount *(*d_automount)(struct path * ) ;
1329 int (*d_manage)(struct dentry * , bool ) ;
1330};
1331#line 422 "include/linux/dcache.h"
1332struct path {
1333 struct vfsmount *mnt ;
1334 struct dentry *dentry ;
1335};
1336#line 51 "include/linux/radix-tree.h"
1337struct radix_tree_node;
1338#line 51
1339struct radix_tree_node;
1340#line 51
1341struct radix_tree_node;
1342#line 51 "include/linux/radix-tree.h"
1343struct radix_tree_root {
1344 unsigned int height ;
1345 gfp_t gfp_mask ;
1346 struct radix_tree_node *rnode ;
1347};
1348#line 229
1349struct prio_tree_node;
1350#line 229
1351struct prio_tree_node;
1352#line 229
1353struct prio_tree_node;
1354#line 229 "include/linux/radix-tree.h"
1355struct raw_prio_tree_node {
1356 struct prio_tree_node *left ;
1357 struct prio_tree_node *right ;
1358 struct prio_tree_node *parent ;
1359};
1360#line 19 "include/linux/prio_tree.h"
1361struct prio_tree_node {
1362 struct prio_tree_node *left ;
1363 struct prio_tree_node *right ;
1364 struct prio_tree_node *parent ;
1365 unsigned long start ;
1366 unsigned long last ;
1367};
1368#line 27 "include/linux/prio_tree.h"
1369struct prio_tree_root {
1370 struct prio_tree_node *prio_tree_node ;
1371 unsigned short index_bits ;
1372 unsigned short raw ;
1373};
1374#line 111
1375enum pid_type {
1376 PIDTYPE_PID = 0,
1377 PIDTYPE_PGID = 1,
1378 PIDTYPE_SID = 2,
1379 PIDTYPE_MAX = 3
1380} ;
1381#line 118
1382struct pid_namespace;
1383#line 118
1384struct pid_namespace;
1385#line 118
1386struct pid_namespace;
1387#line 118 "include/linux/prio_tree.h"
1388struct upid {
1389 int nr ;
1390 struct pid_namespace *ns ;
1391 struct hlist_node pid_chain ;
1392};
1393#line 56 "include/linux/pid.h"
1394struct pid {
1395 atomic_t count ;
1396 unsigned int level ;
1397 struct hlist_head tasks[3U] ;
1398 struct rcu_head rcu ;
1399 struct upid numbers[1U] ;
1400};
1401#line 68 "include/linux/pid.h"
1402struct pid_link {
1403 struct hlist_node node ;
1404 struct pid *pid ;
1405};
1406#line 93 "include/linux/capability.h"
1407struct kernel_cap_struct {
1408 __u32 cap[2U] ;
1409};
1410#line 96 "include/linux/capability.h"
1411typedef struct kernel_cap_struct kernel_cap_t;
1412#line 104
1413struct user_namespace;
1414#line 104
1415struct user_namespace;
1416#line 104
1417struct user_namespace;
1418#line 104
1419struct user_namespace;
1420#line 45 "include/linux/semaphore.h"
1421struct fiemap_extent {
1422 __u64 fe_logical ;
1423 __u64 fe_physical ;
1424 __u64 fe_length ;
1425 __u64 fe_reserved64[2U] ;
1426 __u32 fe_flags ;
1427 __u32 fe_reserved[3U] ;
1428};
1429#line 38 "include/linux/fiemap.h"
1430struct export_operations;
1431#line 38
1432struct export_operations;
1433#line 38
1434struct export_operations;
1435#line 38
1436struct export_operations;
1437#line 40
1438struct iovec;
1439#line 40
1440struct iovec;
1441#line 40
1442struct iovec;
1443#line 40
1444struct iovec;
1445#line 41
1446struct kiocb;
1447#line 41
1448struct kiocb;
1449#line 41
1450struct kiocb;
1451#line 41
1452struct kiocb;
1453#line 42
1454struct pipe_inode_info;
1455#line 42
1456struct pipe_inode_info;
1457#line 42
1458struct pipe_inode_info;
1459#line 42
1460struct pipe_inode_info;
1461#line 43
1462struct poll_table_struct;
1463#line 43
1464struct poll_table_struct;
1465#line 43
1466struct poll_table_struct;
1467#line 43
1468struct poll_table_struct;
1469#line 44
1470struct kstatfs;
1471#line 44
1472struct kstatfs;
1473#line 44
1474struct kstatfs;
1475#line 44
1476struct kstatfs;
1477#line 426 "include/linux/fs.h"
1478struct iattr {
1479 unsigned int ia_valid ;
1480 umode_t ia_mode ;
1481 uid_t ia_uid ;
1482 gid_t ia_gid ;
1483 loff_t ia_size ;
1484 struct timespec ia_atime ;
1485 struct timespec ia_mtime ;
1486 struct timespec ia_ctime ;
1487 struct file *ia_file ;
1488};
1489#line 119 "include/linux/quota.h"
1490struct if_dqinfo {
1491 __u64 dqi_bgrace ;
1492 __u64 dqi_igrace ;
1493 __u32 dqi_flags ;
1494 __u32 dqi_valid ;
1495};
1496#line 176 "include/linux/percpu_counter.h"
1497struct fs_disk_quota {
1498 __s8 d_version ;
1499 __s8 d_flags ;
1500 __u16 d_fieldmask ;
1501 __u32 d_id ;
1502 __u64 d_blk_hardlimit ;
1503 __u64 d_blk_softlimit ;
1504 __u64 d_ino_hardlimit ;
1505 __u64 d_ino_softlimit ;
1506 __u64 d_bcount ;
1507 __u64 d_icount ;
1508 __s32 d_itimer ;
1509 __s32 d_btimer ;
1510 __u16 d_iwarns ;
1511 __u16 d_bwarns ;
1512 __s32 d_padding2 ;
1513 __u64 d_rtb_hardlimit ;
1514 __u64 d_rtb_softlimit ;
1515 __u64 d_rtbcount ;
1516 __s32 d_rtbtimer ;
1517 __u16 d_rtbwarns ;
1518 __s16 d_padding3 ;
1519 char d_padding4[8U] ;
1520};
1521#line 75 "include/linux/dqblk_xfs.h"
1522struct fs_qfilestat {
1523 __u64 qfs_ino ;
1524 __u64 qfs_nblks ;
1525 __u32 qfs_nextents ;
1526};
1527#line 150 "include/linux/dqblk_xfs.h"
1528typedef struct fs_qfilestat fs_qfilestat_t;
1529#line 151 "include/linux/dqblk_xfs.h"
1530struct fs_quota_stat {
1531 __s8 qs_version ;
1532 __u16 qs_flags ;
1533 __s8 qs_pad ;
1534 fs_qfilestat_t qs_uquota ;
1535 fs_qfilestat_t qs_gquota ;
1536 __u32 qs_incoredqs ;
1537 __s32 qs_btimelimit ;
1538 __s32 qs_itimelimit ;
1539 __s32 qs_rtbtimelimit ;
1540 __u16 qs_bwarnlimit ;
1541 __u16 qs_iwarnlimit ;
1542};
1543#line 165
1544struct dquot;
1545#line 165
1546struct dquot;
1547#line 165
1548struct dquot;
1549#line 165
1550struct dquot;
1551#line 185 "include/linux/quota.h"
1552typedef __kernel_uid32_t qid_t;
1553#line 186 "include/linux/quota.h"
1554typedef long long qsize_t;
1555#line 189 "include/linux/quota.h"
1556struct mem_dqblk {
1557 qsize_t dqb_bhardlimit ;
1558 qsize_t dqb_bsoftlimit ;
1559 qsize_t dqb_curspace ;
1560 qsize_t dqb_rsvspace ;
1561 qsize_t dqb_ihardlimit ;
1562 qsize_t dqb_isoftlimit ;
1563 qsize_t dqb_curinodes ;
1564 time_t dqb_btime ;
1565 time_t dqb_itime ;
1566};
1567#line 211
1568struct quota_format_type;
1569#line 211
1570struct quota_format_type;
1571#line 211
1572struct quota_format_type;
1573#line 211
1574struct quota_format_type;
1575#line 212 "include/linux/quota.h"
1576struct mem_dqinfo {
1577 struct quota_format_type *dqi_format ;
1578 int dqi_fmt_id ;
1579 struct list_head dqi_dirty_list ;
1580 unsigned long dqi_flags ;
1581 unsigned int dqi_bgrace ;
1582 unsigned int dqi_igrace ;
1583 qsize_t dqi_maxblimit ;
1584 qsize_t dqi_maxilimit ;
1585 void *dqi_priv ;
1586};
1587#line 271 "include/linux/quota.h"
1588struct dquot {
1589 struct hlist_node dq_hash ;
1590 struct list_head dq_inuse ;
1591 struct list_head dq_free ;
1592 struct list_head dq_dirty ;
1593 struct mutex dq_lock ;
1594 atomic_t dq_count ;
1595 wait_queue_head_t dq_wait_unused ;
1596 struct super_block *dq_sb ;
1597 unsigned int dq_id ;
1598 loff_t dq_off ;
1599 unsigned long dq_flags ;
1600 short dq_type ;
1601 struct mem_dqblk dq_dqb ;
1602};
1603#line 299 "include/linux/quota.h"
1604struct quota_format_ops {
1605 int (*check_quota_file)(struct super_block * , int ) ;
1606 int (*read_file_info)(struct super_block * , int ) ;
1607 int (*write_file_info)(struct super_block * , int ) ;
1608 int (*free_file_info)(struct super_block * , int ) ;
1609 int (*read_dqblk)(struct dquot * ) ;
1610 int (*commit_dqblk)(struct dquot * ) ;
1611 int (*release_dqblk)(struct dquot * ) ;
1612};
1613#line 310 "include/linux/quota.h"
1614struct dquot_operations {
1615 int (*write_dquot)(struct dquot * ) ;
1616 struct dquot *(*alloc_dquot)(struct super_block * , int ) ;
1617 void (*destroy_dquot)(struct dquot * ) ;
1618 int (*acquire_dquot)(struct dquot * ) ;
1619 int (*release_dquot)(struct dquot * ) ;
1620 int (*mark_dirty)(struct dquot * ) ;
1621 int (*write_info)(struct super_block * , int ) ;
1622 qsize_t *(*get_reserved_space)(struct inode * ) ;
1623};
1624#line 324 "include/linux/quota.h"
1625struct quotactl_ops {
1626 int (*quota_on)(struct super_block * , int , int , struct path * ) ;
1627 int (*quota_on_meta)(struct super_block * , int , int ) ;
1628 int (*quota_off)(struct super_block * , int ) ;
1629 int (*quota_sync)(struct super_block * , int , int ) ;
1630 int (*get_info)(struct super_block * , int , struct if_dqinfo * ) ;
1631 int (*set_info)(struct super_block * , int , struct if_dqinfo * ) ;
1632 int (*get_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1633 int (*set_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1634 int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1635 int (*set_xstate)(struct super_block * , unsigned int , int ) ;
1636};
1637#line 340 "include/linux/quota.h"
1638struct quota_format_type {
1639 int qf_fmt_id ;
1640 struct quota_format_ops const *qf_ops ;
1641 struct module *qf_owner ;
1642 struct quota_format_type *qf_next ;
1643};
1644#line 386 "include/linux/quota.h"
1645struct quota_info {
1646 unsigned int flags ;
1647 struct mutex dqio_mutex ;
1648 struct mutex dqonoff_mutex ;
1649 struct rw_semaphore dqptr_sem ;
1650 struct inode *files[2U] ;
1651 struct mem_dqinfo info[2U] ;
1652 struct quota_format_ops const *ops[2U] ;
1653};
1654#line 417
1655struct address_space;
1656#line 417
1657struct address_space;
1658#line 417
1659struct address_space;
1660#line 417
1661struct address_space;
1662#line 418
1663struct writeback_control;
1664#line 418
1665struct writeback_control;
1666#line 418
1667struct writeback_control;
1668#line 418
1669struct writeback_control;
1670#line 576 "include/linux/fs.h"
1671union __anonunion_arg_133 {
1672 char *buf ;
1673 void *data ;
1674};
1675#line 576 "include/linux/fs.h"
1676struct __anonstruct_read_descriptor_t_132 {
1677 size_t written ;
1678 size_t count ;
1679 union __anonunion_arg_133 arg ;
1680 int error ;
1681};
1682#line 576 "include/linux/fs.h"
1683typedef struct __anonstruct_read_descriptor_t_132 read_descriptor_t;
1684#line 579 "include/linux/fs.h"
1685struct address_space_operations {
1686 int (*writepage)(struct page * , struct writeback_control * ) ;
1687 int (*readpage)(struct file * , struct page * ) ;
1688 int (*writepages)(struct address_space * , struct writeback_control * ) ;
1689 int (*set_page_dirty)(struct page * ) ;
1690 int (*readpages)(struct file * , struct address_space * , struct list_head * ,
1691 unsigned int ) ;
1692 int (*write_begin)(struct file * , struct address_space * , loff_t , unsigned int ,
1693 unsigned int , struct page ** , void ** ) ;
1694 int (*write_end)(struct file * , struct address_space * , loff_t , unsigned int ,
1695 unsigned int , struct page * , void * ) ;
1696 sector_t (*bmap)(struct address_space * , sector_t ) ;
1697 void (*invalidatepage)(struct page * , unsigned long ) ;
1698 int (*releasepage)(struct page * , gfp_t ) ;
1699 void (*freepage)(struct page * ) ;
1700 ssize_t (*direct_IO)(int , struct kiocb * , struct iovec const * , loff_t ,
1701 unsigned long ) ;
1702 int (*get_xip_mem)(struct address_space * , unsigned long , int , void ** , unsigned long * ) ;
1703 int (*migratepage)(struct address_space * , struct page * , struct page * ) ;
1704 int (*launder_page)(struct page * ) ;
1705 int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long ) ;
1706 int (*error_remove_page)(struct address_space * , struct page * ) ;
1707};
1708#line 630
1709struct backing_dev_info;
1710#line 630
1711struct backing_dev_info;
1712#line 630
1713struct backing_dev_info;
1714#line 630
1715struct backing_dev_info;
1716#line 631 "include/linux/fs.h"
1717struct address_space {
1718 struct inode *host ;
1719 struct radix_tree_root page_tree ;
1720 spinlock_t tree_lock ;
1721 unsigned int i_mmap_writable ;
1722 struct prio_tree_root i_mmap ;
1723 struct list_head i_mmap_nonlinear ;
1724 struct mutex i_mmap_mutex ;
1725 unsigned long nrpages ;
1726 unsigned long writeback_index ;
1727 struct address_space_operations const *a_ops ;
1728 unsigned long flags ;
1729 struct backing_dev_info *backing_dev_info ;
1730 spinlock_t private_lock ;
1731 struct list_head private_list ;
1732 struct address_space *assoc_mapping ;
1733};
1734#line 652
1735struct hd_struct;
1736#line 652
1737struct hd_struct;
1738#line 652
1739struct hd_struct;
1740#line 652
1741struct gendisk;
1742#line 652
1743struct gendisk;
1744#line 652
1745struct gendisk;
1746#line 652 "include/linux/fs.h"
1747struct block_device {
1748 dev_t bd_dev ;
1749 int bd_openers ;
1750 struct inode *bd_inode ;
1751 struct super_block *bd_super ;
1752 struct mutex bd_mutex ;
1753 struct list_head bd_inodes ;
1754 void *bd_claiming ;
1755 void *bd_holder ;
1756 int bd_holders ;
1757 bool bd_write_holder ;
1758 struct list_head bd_holder_disks ;
1759 struct block_device *bd_contains ;
1760 unsigned int bd_block_size ;
1761 struct hd_struct *bd_part ;
1762 unsigned int bd_part_count ;
1763 int bd_invalidated ;
1764 struct gendisk *bd_disk ;
1765 struct list_head bd_list ;
1766 unsigned long bd_private ;
1767 int bd_fsfreeze_count ;
1768 struct mutex bd_fsfreeze_mutex ;
1769};
1770#line 723
1771struct posix_acl;
1772#line 723
1773struct posix_acl;
1774#line 723
1775struct posix_acl;
1776#line 723
1777struct posix_acl;
1778#line 724
1779struct inode_operations;
1780#line 724
1781struct inode_operations;
1782#line 724
1783struct inode_operations;
1784#line 724 "include/linux/fs.h"
1785union __anonunion_ldv_15212_134 {
1786 struct list_head i_dentry ;
1787 struct rcu_head i_rcu ;
1788};
1789#line 724
1790struct file_operations;
1791#line 724
1792struct file_operations;
1793#line 724
1794struct file_operations;
1795#line 724
1796struct file_lock;
1797#line 724
1798struct file_lock;
1799#line 724
1800struct file_lock;
1801#line 724
1802struct cdev;
1803#line 724
1804struct cdev;
1805#line 724
1806struct cdev;
1807#line 724 "include/linux/fs.h"
1808union __anonunion_ldv_15239_135 {
1809 struct pipe_inode_info *i_pipe ;
1810 struct block_device *i_bdev ;
1811 struct cdev *i_cdev ;
1812};
1813#line 724 "include/linux/fs.h"
1814struct inode {
1815 umode_t i_mode ;
1816 uid_t i_uid ;
1817 gid_t i_gid ;
1818 struct inode_operations const *i_op ;
1819 struct super_block *i_sb ;
1820 spinlock_t i_lock ;
1821 unsigned int i_flags ;
1822 unsigned long i_state ;
1823 void *i_security ;
1824 struct mutex i_mutex ;
1825 unsigned long dirtied_when ;
1826 struct hlist_node i_hash ;
1827 struct list_head i_wb_list ;
1828 struct list_head i_lru ;
1829 struct list_head i_sb_list ;
1830 union __anonunion_ldv_15212_134 ldv_15212 ;
1831 unsigned long i_ino ;
1832 atomic_t i_count ;
1833 unsigned int i_nlink ;
1834 dev_t i_rdev ;
1835 unsigned int i_blkbits ;
1836 u64 i_version ;
1837 loff_t i_size ;
1838 struct timespec i_atime ;
1839 struct timespec i_mtime ;
1840 struct timespec i_ctime ;
1841 blkcnt_t i_blocks ;
1842 unsigned short i_bytes ;
1843 struct rw_semaphore i_alloc_sem ;
1844 struct file_operations const *i_fop ;
1845 struct file_lock *i_flock ;
1846 struct address_space *i_mapping ;
1847 struct address_space i_data ;
1848 struct dquot *i_dquot[2U] ;
1849 struct list_head i_devices ;
1850 union __anonunion_ldv_15239_135 ldv_15239 ;
1851 __u32 i_generation ;
1852 __u32 i_fsnotify_mask ;
1853 struct hlist_head i_fsnotify_marks ;
1854 atomic_t i_readcount ;
1855 atomic_t i_writecount ;
1856 struct posix_acl *i_acl ;
1857 struct posix_acl *i_default_acl ;
1858 void *i_private ;
1859};
1860#line 902 "include/linux/fs.h"
1861struct fown_struct {
1862 rwlock_t lock ;
1863 struct pid *pid ;
1864 enum pid_type pid_type ;
1865 uid_t uid ;
1866 uid_t euid ;
1867 int signum ;
1868};
1869#line 910 "include/linux/fs.h"
1870struct file_ra_state {
1871 unsigned long start ;
1872 unsigned int size ;
1873 unsigned int async_size ;
1874 unsigned int ra_pages ;
1875 unsigned int mmap_miss ;
1876 loff_t prev_pos ;
1877};
1878#line 933 "include/linux/fs.h"
1879union __anonunion_f_u_136 {
1880 struct list_head fu_list ;
1881 struct rcu_head fu_rcuhead ;
1882};
1883#line 933 "include/linux/fs.h"
1884struct file {
1885 union __anonunion_f_u_136 f_u ;
1886 struct path f_path ;
1887 struct file_operations const *f_op ;
1888 spinlock_t f_lock ;
1889 int f_sb_list_cpu ;
1890 atomic_long_t f_count ;
1891 unsigned int f_flags ;
1892 fmode_t f_mode ;
1893 loff_t f_pos ;
1894 struct fown_struct f_owner ;
1895 struct cred const *f_cred ;
1896 struct file_ra_state f_ra ;
1897 u64 f_version ;
1898 void *f_security ;
1899 void *private_data ;
1900 struct list_head f_ep_links ;
1901 struct address_space *f_mapping ;
1902 unsigned long f_mnt_write_state ;
1903};
1904#line 1064
1905struct files_struct;
1906#line 1064
1907struct files_struct;
1908#line 1064
1909struct files_struct;
1910#line 1064 "include/linux/fs.h"
1911typedef struct files_struct *fl_owner_t;
1912#line 1065 "include/linux/fs.h"
1913struct file_lock_operations {
1914 void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1915 void (*fl_release_private)(struct file_lock * ) ;
1916};
1917#line 1070 "include/linux/fs.h"
1918struct lock_manager_operations {
1919 int (*fl_compare_owner)(struct file_lock * , struct file_lock * ) ;
1920 void (*fl_notify)(struct file_lock * ) ;
1921 int (*fl_grant)(struct file_lock * , struct file_lock * , int ) ;
1922 void (*fl_release_private)(struct file_lock * ) ;
1923 void (*fl_break)(struct file_lock * ) ;
1924 int (*fl_change)(struct file_lock ** , int ) ;
1925};
1926#line 163 "include/linux/nfs.h"
1927struct nlm_lockowner;
1928#line 163
1929struct nlm_lockowner;
1930#line 163
1931struct nlm_lockowner;
1932#line 163
1933struct nlm_lockowner;
1934#line 164 "include/linux/nfs.h"
1935struct nfs_lock_info {
1936 u32 state ;
1937 struct nlm_lockowner *owner ;
1938 struct list_head list ;
1939};
1940#line 18 "include/linux/nfs_fs_i.h"
1941struct nfs4_lock_state;
1942#line 18
1943struct nfs4_lock_state;
1944#line 18
1945struct nfs4_lock_state;
1946#line 18
1947struct nfs4_lock_state;
1948#line 19 "include/linux/nfs_fs_i.h"
1949struct nfs4_lock_info {
1950 struct nfs4_lock_state *owner ;
1951};
1952#line 23
1953struct fasync_struct;
1954#line 23
1955struct fasync_struct;
1956#line 23
1957struct fasync_struct;
1958#line 23 "include/linux/nfs_fs_i.h"
1959struct __anonstruct_afs_138 {
1960 struct list_head link ;
1961 int state ;
1962};
1963#line 23 "include/linux/nfs_fs_i.h"
1964union __anonunion_fl_u_137 {
1965 struct nfs_lock_info nfs_fl ;
1966 struct nfs4_lock_info nfs4_fl ;
1967 struct __anonstruct_afs_138 afs ;
1968};
1969#line 23 "include/linux/nfs_fs_i.h"
1970struct file_lock {
1971 struct file_lock *fl_next ;
1972 struct list_head fl_link ;
1973 struct list_head fl_block ;
1974 fl_owner_t fl_owner ;
1975 unsigned char fl_flags ;
1976 unsigned char fl_type ;
1977 unsigned int fl_pid ;
1978 struct pid *fl_nspid ;
1979 wait_queue_head_t fl_wait ;
1980 struct file *fl_file ;
1981 loff_t fl_start ;
1982 loff_t fl_end ;
1983 struct fasync_struct *fl_fasync ;
1984 unsigned long fl_break_time ;
1985 struct file_lock_operations const *fl_ops ;
1986 struct lock_manager_operations const *fl_lmops ;
1987 union __anonunion_fl_u_137 fl_u ;
1988};
1989#line 1171 "include/linux/fs.h"
1990struct fasync_struct {
1991 spinlock_t fa_lock ;
1992 int magic ;
1993 int fa_fd ;
1994 struct fasync_struct *fa_next ;
1995 struct file *fa_file ;
1996 struct rcu_head fa_rcu ;
1997};
1998#line 1363
1999struct file_system_type;
2000#line 1363
2001struct file_system_type;
2002#line 1363
2003struct file_system_type;
2004#line 1363
2005struct super_operations;
2006#line 1363
2007struct super_operations;
2008#line 1363
2009struct super_operations;
2010#line 1363
2011struct xattr_handler;
2012#line 1363
2013struct xattr_handler;
2014#line 1363
2015struct xattr_handler;
2016#line 1363
2017struct mtd_info;
2018#line 1363
2019struct mtd_info;
2020#line 1363
2021struct mtd_info;
2022#line 1363 "include/linux/fs.h"
2023struct super_block {
2024 struct list_head s_list ;
2025 dev_t s_dev ;
2026 unsigned char s_dirt ;
2027 unsigned char s_blocksize_bits ;
2028 unsigned long s_blocksize ;
2029 loff_t s_maxbytes ;
2030 struct file_system_type *s_type ;
2031 struct super_operations const *s_op ;
2032 struct dquot_operations const *dq_op ;
2033 struct quotactl_ops const *s_qcop ;
2034 struct export_operations const *s_export_op ;
2035 unsigned long s_flags ;
2036 unsigned long s_magic ;
2037 struct dentry *s_root ;
2038 struct rw_semaphore s_umount ;
2039 struct mutex s_lock ;
2040 int s_count ;
2041 atomic_t s_active ;
2042 void *s_security ;
2043 struct xattr_handler const **s_xattr ;
2044 struct list_head s_inodes ;
2045 struct hlist_bl_head s_anon ;
2046 struct list_head *s_files ;
2047 struct list_head s_dentry_lru ;
2048 int s_nr_dentry_unused ;
2049 struct block_device *s_bdev ;
2050 struct backing_dev_info *s_bdi ;
2051 struct mtd_info *s_mtd ;
2052 struct list_head s_instances ;
2053 struct quota_info s_dquot ;
2054 int s_frozen ;
2055 wait_queue_head_t s_wait_unfrozen ;
2056 char s_id[32U] ;
2057 u8 s_uuid[16U] ;
2058 void *s_fs_info ;
2059 fmode_t s_mode ;
2060 u32 s_time_gran ;
2061 struct mutex s_vfs_rename_mutex ;
2062 char *s_subtype ;
2063 char *s_options ;
2064 struct dentry_operations const *s_d_op ;
2065 int cleancache_poolid ;
2066};
2067#line 1495 "include/linux/fs.h"
2068struct fiemap_extent_info {
2069 unsigned int fi_flags ;
2070 unsigned int fi_extents_mapped ;
2071 unsigned int fi_extents_max ;
2072 struct fiemap_extent *fi_extents_start ;
2073};
2074#line 1534 "include/linux/fs.h"
2075struct file_operations {
2076 struct module *owner ;
2077 loff_t (*llseek)(struct file * , loff_t , int ) ;
2078 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ;
2079 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ;
2080 ssize_t (*aio_read)(struct kiocb * , struct iovec const * , unsigned long ,
2081 loff_t ) ;
2082 ssize_t (*aio_write)(struct kiocb * , struct iovec const * , unsigned long ,
2083 loff_t ) ;
2084 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int ,
2085 loff_t , u64 , unsigned int ) ) ;
2086 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
2087 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
2088 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
2089 int (*mmap)(struct file * , struct vm_area_struct * ) ;
2090 int (*open)(struct inode * , struct file * ) ;
2091 int (*flush)(struct file * , fl_owner_t ) ;
2092 int (*release)(struct inode * , struct file * ) ;
2093 int (*fsync)(struct file * , int ) ;
2094 int (*aio_fsync)(struct kiocb * , int ) ;
2095 int (*fasync)(int , struct file * , int ) ;
2096 int (*lock)(struct file * , int , struct file_lock * ) ;
2097 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * ,
2098 int ) ;
2099 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
2100 unsigned long , unsigned long ) ;
2101 int (*check_flags)(int ) ;
2102 int (*flock)(struct file * , int , struct file_lock * ) ;
2103 ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t ,
2104 unsigned int ) ;
2105 ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t ,
2106 unsigned int ) ;
2107 int (*setlease)(struct file * , long , struct file_lock ** ) ;
2108 long (*fallocate)(struct file * , int , loff_t , loff_t ) ;
2109};
2110#line 1574 "include/linux/fs.h"
2111struct inode_operations {
2112 struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
2113 void *(*follow_link)(struct dentry * , struct nameidata * ) ;
2114 int (*permission)(struct inode * , int , unsigned int ) ;
2115 int (*check_acl)(struct inode * , int , unsigned int ) ;
2116 int (*readlink)(struct dentry * , char * , int ) ;
2117 void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
2118 int (*create)(struct inode * , struct dentry * , int , struct nameidata * ) ;
2119 int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
2120 int (*unlink)(struct inode * , struct dentry * ) ;
2121 int (*symlink)(struct inode * , struct dentry * , char const * ) ;
2122 int (*mkdir)(struct inode * , struct dentry * , int ) ;
2123 int (*rmdir)(struct inode * , struct dentry * ) ;
2124 int (*mknod)(struct inode * , struct dentry * , int , dev_t ) ;
2125 int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
2126 void (*truncate)(struct inode * ) ;
2127 int (*setattr)(struct dentry * , struct iattr * ) ;
2128 int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
2129 int (*setxattr)(struct dentry * , char const * , void const * , size_t , int ) ;
2130 ssize_t (*getxattr)(struct dentry * , char const * , void * , size_t ) ;
2131 ssize_t (*listxattr)(struct dentry * , char * , size_t ) ;
2132 int (*removexattr)(struct dentry * , char const * ) ;
2133 void (*truncate_range)(struct inode * , loff_t , loff_t ) ;
2134 int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 , u64 ) ;
2135};
2136#line 1620 "include/linux/fs.h"
2137struct super_operations {
2138 struct inode *(*alloc_inode)(struct super_block * ) ;
2139 void (*destroy_inode)(struct inode * ) ;
2140 void (*dirty_inode)(struct inode * , int ) ;
2141 int (*write_inode)(struct inode * , struct writeback_control * ) ;
2142 int (*drop_inode)(struct inode * ) ;
2143 void (*evict_inode)(struct inode * ) ;
2144 void (*put_super)(struct super_block * ) ;
2145 void (*write_super)(struct super_block * ) ;
2146 int (*sync_fs)(struct super_block * , int ) ;
2147 int (*freeze_fs)(struct super_block * ) ;
2148 int (*unfreeze_fs)(struct super_block * ) ;
2149 int (*statfs)(struct dentry * , struct kstatfs * ) ;
2150 int (*remount_fs)(struct super_block * , int * , char * ) ;
2151 void (*umount_begin)(struct super_block * ) ;
2152 int (*show_options)(struct seq_file * , struct vfsmount * ) ;
2153 int (*show_devname)(struct seq_file * , struct vfsmount * ) ;
2154 int (*show_path)(struct seq_file * , struct vfsmount * ) ;
2155 int (*show_stats)(struct seq_file * , struct vfsmount * ) ;
2156 ssize_t (*quota_read)(struct super_block * , int , char * , size_t , loff_t ) ;
2157 ssize_t (*quota_write)(struct super_block * , int , char const * , size_t ,
2158 loff_t ) ;
2159 int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t ) ;
2160};
2161#line 1801 "include/linux/fs.h"
2162struct file_system_type {
2163 char const *name ;
2164 int fs_flags ;
2165 struct dentry *(*mount)(struct file_system_type * , int , char const * , void * ) ;
2166 void (*kill_sb)(struct super_block * ) ;
2167 struct module *owner ;
2168 struct file_system_type *next ;
2169 struct list_head fs_supers ;
2170 struct lock_class_key s_lock_key ;
2171 struct lock_class_key s_umount_key ;
2172 struct lock_class_key s_vfs_rename_key ;
2173 struct lock_class_key i_lock_key ;
2174 struct lock_class_key i_mutex_key ;
2175 struct lock_class_key i_mutex_dir_key ;
2176 struct lock_class_key i_alloc_sem_key ;
2177};
2178#line 118 "include/linux/kmemleak.h"
2179struct kmem_cache_cpu {
2180 void **freelist ;
2181 unsigned long tid ;
2182 struct page *page ;
2183 int node ;
2184 unsigned int stat[19U] ;
2185};
2186#line 46 "include/linux/slub_def.h"
2187struct kmem_cache_node {
2188 spinlock_t list_lock ;
2189 unsigned long nr_partial ;
2190 struct list_head partial ;
2191 atomic_long_t nr_slabs ;
2192 atomic_long_t total_objects ;
2193 struct list_head full ;
2194};
2195#line 57 "include/linux/slub_def.h"
2196struct kmem_cache_order_objects {
2197 unsigned long x ;
2198};
2199#line 67 "include/linux/slub_def.h"
2200struct kmem_cache {
2201 struct kmem_cache_cpu *cpu_slab ;
2202 unsigned long flags ;
2203 unsigned long min_partial ;
2204 int size ;
2205 int objsize ;
2206 int offset ;
2207 struct kmem_cache_order_objects oo ;
2208 struct kmem_cache_order_objects max ;
2209 struct kmem_cache_order_objects min ;
2210 gfp_t allocflags ;
2211 int refcount ;
2212 void (*ctor)(void * ) ;
2213 int inuse ;
2214 int align ;
2215 int reserved ;
2216 char const *name ;
2217 struct list_head list ;
2218 struct kobject kobj ;
2219 int remote_node_defrag_ratio ;
2220 struct kmem_cache_node *node[1024U] ;
2221};
2222#line 335 "include/linux/slab.h"
2223struct mtop {
2224 short mt_op ;
2225 int mt_count ;
2226};
2227#line 125 "include/linux/mtio.h"
2228struct klist_node;
2229#line 125
2230struct klist_node;
2231#line 125
2232struct klist_node;
2233#line 125
2234struct klist_node;
2235#line 37 "include/linux/klist.h"
2236struct klist_node {
2237 void *n_klist ;
2238 struct list_head n_node ;
2239 struct kref n_ref ;
2240};
2241#line 67
2242struct dma_map_ops;
2243#line 67
2244struct dma_map_ops;
2245#line 67
2246struct dma_map_ops;
2247#line 67 "include/linux/klist.h"
2248struct dev_archdata {
2249 void *acpi_handle ;
2250 struct dma_map_ops *dma_ops ;
2251 void *iommu ;
2252};
2253#line 17 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/device.h"
2254struct device_private;
2255#line 17
2256struct device_private;
2257#line 17
2258struct device_private;
2259#line 17
2260struct device_private;
2261#line 18
2262struct device_driver;
2263#line 18
2264struct device_driver;
2265#line 18
2266struct device_driver;
2267#line 18
2268struct device_driver;
2269#line 19
2270struct driver_private;
2271#line 19
2272struct driver_private;
2273#line 19
2274struct driver_private;
2275#line 19
2276struct driver_private;
2277#line 20
2278struct class;
2279#line 20
2280struct class;
2281#line 20
2282struct class;
2283#line 20
2284struct class;
2285#line 21
2286struct subsys_private;
2287#line 21
2288struct subsys_private;
2289#line 21
2290struct subsys_private;
2291#line 21
2292struct subsys_private;
2293#line 22
2294struct bus_type;
2295#line 22
2296struct bus_type;
2297#line 22
2298struct bus_type;
2299#line 22
2300struct bus_type;
2301#line 23
2302struct device_node;
2303#line 23
2304struct device_node;
2305#line 23
2306struct device_node;
2307#line 23
2308struct device_node;
2309#line 24 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/device.h"
2310struct bus_attribute {
2311 struct attribute attr ;
2312 ssize_t (*show)(struct bus_type * , char * ) ;
2313 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
2314};
2315#line 49 "include/linux/device.h"
2316struct device_attribute;
2317#line 49
2318struct device_attribute;
2319#line 49
2320struct device_attribute;
2321#line 49
2322struct driver_attribute;
2323#line 49
2324struct driver_attribute;
2325#line 49
2326struct driver_attribute;
2327#line 49 "include/linux/device.h"
2328struct bus_type {
2329 char const *name ;
2330 struct bus_attribute *bus_attrs ;
2331 struct device_attribute *dev_attrs ;
2332 struct driver_attribute *drv_attrs ;
2333 int (*match)(struct device * , struct device_driver * ) ;
2334 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
2335 int (*probe)(struct device * ) ;
2336 int (*remove)(struct device * ) ;
2337 void (*shutdown)(struct device * ) ;
2338 int (*suspend)(struct device * , pm_message_t ) ;
2339 int (*resume)(struct device * ) ;
2340 struct dev_pm_ops const *pm ;
2341 struct subsys_private *p ;
2342};
2343#line 153
2344struct of_device_id;
2345#line 153
2346struct of_device_id;
2347#line 153
2348struct of_device_id;
2349#line 153 "include/linux/device.h"
2350struct device_driver {
2351 char const *name ;
2352 struct bus_type *bus ;
2353 struct module *owner ;
2354 char const *mod_name ;
2355 bool suppress_bind_attrs ;
2356 struct of_device_id const *of_match_table ;
2357 int (*probe)(struct device * ) ;
2358 int (*remove)(struct device * ) ;
2359 void (*shutdown)(struct device * ) ;
2360 int (*suspend)(struct device * , pm_message_t ) ;
2361 int (*resume)(struct device * ) ;
2362 struct attribute_group const **groups ;
2363 struct dev_pm_ops const *pm ;
2364 struct driver_private *p ;
2365};
2366#line 218 "include/linux/device.h"
2367struct driver_attribute {
2368 struct attribute attr ;
2369 ssize_t (*show)(struct device_driver * , char * ) ;
2370 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
2371};
2372#line 248
2373struct class_attribute;
2374#line 248
2375struct class_attribute;
2376#line 248
2377struct class_attribute;
2378#line 248 "include/linux/device.h"
2379struct class {
2380 char const *name ;
2381 struct module *owner ;
2382 struct class_attribute *class_attrs ;
2383 struct device_attribute *dev_attrs ;
2384 struct bin_attribute *dev_bin_attrs ;
2385 struct kobject *dev_kobj ;
2386 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
2387 char *(*devnode)(struct device * , mode_t * ) ;
2388 void (*class_release)(struct class * ) ;
2389 void (*dev_release)(struct device * ) ;
2390 int (*suspend)(struct device * , pm_message_t ) ;
2391 int (*resume)(struct device * ) ;
2392 struct kobj_ns_type_operations const *ns_type ;
2393 void const *(*namespace)(struct device * ) ;
2394 struct dev_pm_ops const *pm ;
2395 struct subsys_private *p ;
2396};
2397#line 305
2398struct device_type;
2399#line 305
2400struct device_type;
2401#line 305
2402struct device_type;
2403#line 344 "include/linux/device.h"
2404struct class_attribute {
2405 struct attribute attr ;
2406 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
2407 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
2408};
2409#line 395 "include/linux/device.h"
2410struct device_type {
2411 char const *name ;
2412 struct attribute_group const **groups ;
2413 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
2414 char *(*devnode)(struct device * , mode_t * ) ;
2415 void (*release)(struct device * ) ;
2416 struct dev_pm_ops const *pm ;
2417};
2418#line 422 "include/linux/device.h"
2419struct device_attribute {
2420 struct attribute attr ;
2421 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
2422 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
2423 size_t ) ;
2424};
2425#line 483 "include/linux/device.h"
2426struct device_dma_parameters {
2427 unsigned int max_segment_size ;
2428 unsigned long segment_boundary_mask ;
2429};
2430#line 492
2431struct dma_coherent_mem;
2432#line 492
2433struct dma_coherent_mem;
2434#line 492
2435struct dma_coherent_mem;
2436#line 492 "include/linux/device.h"
2437struct device {
2438 struct device *parent ;
2439 struct device_private *p ;
2440 struct kobject kobj ;
2441 char const *init_name ;
2442 struct device_type const *type ;
2443 struct mutex mutex ;
2444 struct bus_type *bus ;
2445 struct device_driver *driver ;
2446 void *platform_data ;
2447 struct dev_pm_info power ;
2448 struct dev_power_domain *pwr_domain ;
2449 int numa_node ;
2450 u64 *dma_mask ;
2451 u64 coherent_dma_mask ;
2452 struct device_dma_parameters *dma_parms ;
2453 struct list_head dma_pools ;
2454 struct dma_coherent_mem *dma_mem ;
2455 struct dev_archdata archdata ;
2456 struct device_node *of_node ;
2457 dev_t devt ;
2458 spinlock_t devres_lock ;
2459 struct list_head devres_head ;
2460 struct klist_node knode_class ;
2461 struct class *class ;
2462 struct attribute_group const **groups ;
2463 void (*release)(struct device * ) ;
2464};
2465#line 604 "include/linux/device.h"
2466struct wakeup_source {
2467 char *name ;
2468 struct list_head entry ;
2469 spinlock_t lock ;
2470 struct timer_list timer ;
2471 unsigned long timer_expires ;
2472 ktime_t total_time ;
2473 ktime_t max_time ;
2474 ktime_t last_time ;
2475 unsigned long event_count ;
2476 unsigned long active_count ;
2477 unsigned long relax_count ;
2478 unsigned long hit_count ;
2479 unsigned char active : 1 ;
2480};
2481#line 50 "include/linux/sched.h"
2482struct rb_node {
2483 unsigned long rb_parent_color ;
2484 struct rb_node *rb_right ;
2485 struct rb_node *rb_left ;
2486};
2487#line 108 "include/linux/rbtree.h"
2488struct rb_root {
2489 struct rb_node *rb_node ;
2490};
2491#line 180 "include/linux/rbtree.h"
2492struct __anonstruct_ldv_18247_140 {
2493 u16 inuse ;
2494 u16 objects ;
2495};
2496#line 180 "include/linux/rbtree.h"
2497union __anonunion_ldv_18248_139 {
2498 atomic_t _mapcount ;
2499 struct __anonstruct_ldv_18247_140 ldv_18247 ;
2500};
2501#line 180 "include/linux/rbtree.h"
2502struct __anonstruct_ldv_18253_142 {
2503 unsigned long private ;
2504 struct address_space *mapping ;
2505};
2506#line 180 "include/linux/rbtree.h"
2507union __anonunion_ldv_18256_141 {
2508 struct __anonstruct_ldv_18253_142 ldv_18253 ;
2509 struct kmem_cache *slab ;
2510 struct page *first_page ;
2511};
2512#line 180 "include/linux/rbtree.h"
2513union __anonunion_ldv_18260_143 {
2514 unsigned long index ;
2515 void *freelist ;
2516};
2517#line 180 "include/linux/rbtree.h"
2518struct page {
2519 unsigned long flags ;
2520 atomic_t _count ;
2521 union __anonunion_ldv_18248_139 ldv_18248 ;
2522 union __anonunion_ldv_18256_141 ldv_18256 ;
2523 union __anonunion_ldv_18260_143 ldv_18260 ;
2524 struct list_head lru ;
2525};
2526#line 124 "include/linux/mm_types.h"
2527struct __anonstruct_vm_set_145 {
2528 struct list_head list ;
2529 void *parent ;
2530 struct vm_area_struct *head ;
2531};
2532#line 124 "include/linux/mm_types.h"
2533union __anonunion_shared_144 {
2534 struct __anonstruct_vm_set_145 vm_set ;
2535 struct raw_prio_tree_node prio_tree_node ;
2536};
2537#line 124
2538struct anon_vma;
2539#line 124
2540struct anon_vma;
2541#line 124
2542struct anon_vma;
2543#line 124
2544struct vm_operations_struct;
2545#line 124
2546struct vm_operations_struct;
2547#line 124
2548struct vm_operations_struct;
2549#line 124
2550struct mempolicy;
2551#line 124
2552struct mempolicy;
2553#line 124
2554struct mempolicy;
2555#line 124 "include/linux/mm_types.h"
2556struct vm_area_struct {
2557 struct mm_struct *vm_mm ;
2558 unsigned long vm_start ;
2559 unsigned long vm_end ;
2560 struct vm_area_struct *vm_next ;
2561 struct vm_area_struct *vm_prev ;
2562 pgprot_t vm_page_prot ;
2563 unsigned long vm_flags ;
2564 struct rb_node vm_rb ;
2565 union __anonunion_shared_144 shared ;
2566 struct list_head anon_vma_chain ;
2567 struct anon_vma *anon_vma ;
2568 struct vm_operations_struct const *vm_ops ;
2569 unsigned long vm_pgoff ;
2570 struct file *vm_file ;
2571 void *vm_private_data ;
2572 struct mempolicy *vm_policy ;
2573};
2574#line 187 "include/linux/mm_types.h"
2575struct core_thread {
2576 struct task_struct *task ;
2577 struct core_thread *next ;
2578};
2579#line 193 "include/linux/mm_types.h"
2580struct core_state {
2581 atomic_t nr_threads ;
2582 struct core_thread dumper ;
2583 struct completion startup ;
2584};
2585#line 206 "include/linux/mm_types.h"
2586struct mm_rss_stat {
2587 atomic_long_t count[3U] ;
2588};
2589#line 219
2590struct linux_binfmt;
2591#line 219
2592struct linux_binfmt;
2593#line 219
2594struct linux_binfmt;
2595#line 219
2596struct mmu_notifier_mm;
2597#line 219
2598struct mmu_notifier_mm;
2599#line 219
2600struct mmu_notifier_mm;
2601#line 219 "include/linux/mm_types.h"
2602struct mm_struct {
2603 struct vm_area_struct *mmap ;
2604 struct rb_root mm_rb ;
2605 struct vm_area_struct *mmap_cache ;
2606 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
2607 unsigned long , unsigned long ) ;
2608 void (*unmap_area)(struct mm_struct * , unsigned long ) ;
2609 unsigned long mmap_base ;
2610 unsigned long task_size ;
2611 unsigned long cached_hole_size ;
2612 unsigned long free_area_cache ;
2613 pgd_t *pgd ;
2614 atomic_t mm_users ;
2615 atomic_t mm_count ;
2616 int map_count ;
2617 spinlock_t page_table_lock ;
2618 struct rw_semaphore mmap_sem ;
2619 struct list_head mmlist ;
2620 unsigned long hiwater_rss ;
2621 unsigned long hiwater_vm ;
2622 unsigned long total_vm ;
2623 unsigned long locked_vm ;
2624 unsigned long shared_vm ;
2625 unsigned long exec_vm ;
2626 unsigned long stack_vm ;
2627 unsigned long reserved_vm ;
2628 unsigned long def_flags ;
2629 unsigned long nr_ptes ;
2630 unsigned long start_code ;
2631 unsigned long end_code ;
2632 unsigned long start_data ;
2633 unsigned long end_data ;
2634 unsigned long start_brk ;
2635 unsigned long brk ;
2636 unsigned long start_stack ;
2637 unsigned long arg_start ;
2638 unsigned long arg_end ;
2639 unsigned long env_start ;
2640 unsigned long env_end ;
2641 unsigned long saved_auxv[44U] ;
2642 struct mm_rss_stat rss_stat ;
2643 struct linux_binfmt *binfmt ;
2644 cpumask_var_t cpu_vm_mask_var ;
2645 mm_context_t context ;
2646 unsigned int faultstamp ;
2647 unsigned int token_priority ;
2648 unsigned int last_interval ;
2649 atomic_t oom_disable_count ;
2650 unsigned long flags ;
2651 struct core_state *core_state ;
2652 spinlock_t ioctx_lock ;
2653 struct hlist_head ioctx_list ;
2654 struct task_struct *owner ;
2655 struct file *exe_file ;
2656 unsigned long num_exe_file_vmas ;
2657 struct mmu_notifier_mm *mmu_notifier_mm ;
2658 pgtable_t pmd_huge_pte ;
2659 struct cpumask cpumask_allocation ;
2660};
2661#line 7 "include/asm-generic/cputime.h"
2662typedef unsigned long cputime_t;
2663#line 118 "include/linux/sem.h"
2664struct sem_undo_list;
2665#line 118
2666struct sem_undo_list;
2667#line 118
2668struct sem_undo_list;
2669#line 131 "include/linux/sem.h"
2670struct sem_undo_list {
2671 atomic_t refcnt ;
2672 spinlock_t lock ;
2673 struct list_head list_proc ;
2674};
2675#line 140 "include/linux/sem.h"
2676struct sysv_sem {
2677 struct sem_undo_list *undo_list ;
2678};
2679#line 149
2680struct siginfo;
2681#line 149
2682struct siginfo;
2683#line 149
2684struct siginfo;
2685#line 149
2686struct siginfo;
2687#line 32 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h"
2688struct __anonstruct_sigset_t_146 {
2689 unsigned long sig[1U] ;
2690};
2691#line 32 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h"
2692typedef struct __anonstruct_sigset_t_146 sigset_t;
2693#line 17 "include/asm-generic/signal-defs.h"
2694typedef void __signalfn_t(int );
2695#line 18 "include/asm-generic/signal-defs.h"
2696typedef __signalfn_t *__sighandler_t;
2697#line 20 "include/asm-generic/signal-defs.h"
2698typedef void __restorefn_t(void);
2699#line 21 "include/asm-generic/signal-defs.h"
2700typedef __restorefn_t *__sigrestore_t;
2701#line 126 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h"
2702struct sigaction {
2703 __sighandler_t sa_handler ;
2704 unsigned long sa_flags ;
2705 __sigrestore_t sa_restorer ;
2706 sigset_t sa_mask ;
2707};
2708#line 173 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h"
2709struct k_sigaction {
2710 struct sigaction sa ;
2711};
2712#line 185 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h"
2713union sigval {
2714 int sival_int ;
2715 void *sival_ptr ;
2716};
2717#line 10 "include/asm-generic/siginfo.h"
2718typedef union sigval sigval_t;
2719#line 11 "include/asm-generic/siginfo.h"
2720struct __anonstruct__kill_148 {
2721 __kernel_pid_t _pid ;
2722 __kernel_uid32_t _uid ;
2723};
2724#line 11 "include/asm-generic/siginfo.h"
2725struct __anonstruct__timer_149 {
2726 __kernel_timer_t _tid ;
2727 int _overrun ;
2728 char _pad[0U] ;
2729 sigval_t _sigval ;
2730 int _sys_private ;
2731};
2732#line 11 "include/asm-generic/siginfo.h"
2733struct __anonstruct__rt_150 {
2734 __kernel_pid_t _pid ;
2735 __kernel_uid32_t _uid ;
2736 sigval_t _sigval ;
2737};
2738#line 11 "include/asm-generic/siginfo.h"
2739struct __anonstruct__sigchld_151 {
2740 __kernel_pid_t _pid ;
2741 __kernel_uid32_t _uid ;
2742 int _status ;
2743 __kernel_clock_t _utime ;
2744 __kernel_clock_t _stime ;
2745};
2746#line 11 "include/asm-generic/siginfo.h"
2747struct __anonstruct__sigfault_152 {
2748 void *_addr ;
2749 short _addr_lsb ;
2750};
2751#line 11 "include/asm-generic/siginfo.h"
2752struct __anonstruct__sigpoll_153 {
2753 long _band ;
2754 int _fd ;
2755};
2756#line 11 "include/asm-generic/siginfo.h"
2757union __anonunion__sifields_147 {
2758 int _pad[28U] ;
2759 struct __anonstruct__kill_148 _kill ;
2760 struct __anonstruct__timer_149 _timer ;
2761 struct __anonstruct__rt_150 _rt ;
2762 struct __anonstruct__sigchld_151 _sigchld ;
2763 struct __anonstruct__sigfault_152 _sigfault ;
2764 struct __anonstruct__sigpoll_153 _sigpoll ;
2765};
2766#line 11 "include/asm-generic/siginfo.h"
2767struct siginfo {
2768 int si_signo ;
2769 int si_errno ;
2770 int si_code ;
2771 union __anonunion__sifields_147 _sifields ;
2772};
2773#line 94 "include/asm-generic/siginfo.h"
2774typedef struct siginfo siginfo_t;
2775#line 14 "include/linux/signal.h"
2776struct user_struct;
2777#line 14
2778struct user_struct;
2779#line 14
2780struct user_struct;
2781#line 24 "include/linux/signal.h"
2782struct sigpending {
2783 struct list_head list ;
2784 sigset_t signal ;
2785};
2786#line 90 "include/linux/proportions.h"
2787struct prop_local_single {
2788 unsigned long events ;
2789 unsigned long period ;
2790 int shift ;
2791 spinlock_t lock ;
2792};
2793#line 10 "include/linux/seccomp.h"
2794struct __anonstruct_seccomp_t_156 {
2795 int mode ;
2796};
2797#line 10 "include/linux/seccomp.h"
2798typedef struct __anonstruct_seccomp_t_156 seccomp_t;
2799#line 21 "include/linux/seccomp.h"
2800struct plist_head {
2801 struct list_head node_list ;
2802 raw_spinlock_t *rawlock ;
2803 spinlock_t *spinlock ;
2804};
2805#line 88 "include/linux/plist.h"
2806struct plist_node {
2807 int prio ;
2808 struct list_head prio_list ;
2809 struct list_head node_list ;
2810};
2811#line 38 "include/linux/rtmutex.h"
2812struct rt_mutex_waiter;
2813#line 38
2814struct rt_mutex_waiter;
2815#line 38
2816struct rt_mutex_waiter;
2817#line 38
2818struct rt_mutex_waiter;
2819#line 41 "include/linux/resource.h"
2820struct rlimit {
2821 unsigned long rlim_cur ;
2822 unsigned long rlim_max ;
2823};
2824#line 85 "include/linux/resource.h"
2825struct timerqueue_node {
2826 struct rb_node node ;
2827 ktime_t expires ;
2828};
2829#line 12 "include/linux/timerqueue.h"
2830struct timerqueue_head {
2831 struct rb_root head ;
2832 struct timerqueue_node *next ;
2833};
2834#line 50
2835struct hrtimer_clock_base;
2836#line 50
2837struct hrtimer_clock_base;
2838#line 50
2839struct hrtimer_clock_base;
2840#line 50
2841struct hrtimer_clock_base;
2842#line 51
2843struct hrtimer_cpu_base;
2844#line 51
2845struct hrtimer_cpu_base;
2846#line 51
2847struct hrtimer_cpu_base;
2848#line 51
2849struct hrtimer_cpu_base;
2850#line 60
2851enum hrtimer_restart {
2852 HRTIMER_NORESTART = 0,
2853 HRTIMER_RESTART = 1
2854} ;
2855#line 65 "include/linux/timerqueue.h"
2856struct hrtimer {
2857 struct timerqueue_node node ;
2858 ktime_t _softexpires ;
2859 enum hrtimer_restart (*function)(struct hrtimer * ) ;
2860 struct hrtimer_clock_base *base ;
2861 unsigned long state ;
2862 int start_pid ;
2863 void *start_site ;
2864 char start_comm[16U] ;
2865};
2866#line 132 "include/linux/hrtimer.h"
2867struct hrtimer_clock_base {
2868 struct hrtimer_cpu_base *cpu_base ;
2869 int index ;
2870 clockid_t clockid ;
2871 struct timerqueue_head active ;
2872 ktime_t resolution ;
2873 ktime_t (*get_time)(void) ;
2874 ktime_t softirq_time ;
2875 ktime_t offset ;
2876};
2877#line 162 "include/linux/hrtimer.h"
2878struct hrtimer_cpu_base {
2879 raw_spinlock_t lock ;
2880 unsigned long active_bases ;
2881 ktime_t expires_next ;
2882 int hres_active ;
2883 int hang_detected ;
2884 unsigned long nr_events ;
2885 unsigned long nr_retries ;
2886 unsigned long nr_hangs ;
2887 ktime_t max_hang_time ;
2888 struct hrtimer_clock_base clock_base[3U] ;
2889};
2890#line 452 "include/linux/hrtimer.h"
2891struct task_io_accounting {
2892 u64 rchar ;
2893 u64 wchar ;
2894 u64 syscr ;
2895 u64 syscw ;
2896 u64 read_bytes ;
2897 u64 write_bytes ;
2898 u64 cancelled_write_bytes ;
2899};
2900#line 45 "include/linux/task_io_accounting.h"
2901struct latency_record {
2902 unsigned long backtrace[12U] ;
2903 unsigned int count ;
2904 unsigned long time ;
2905 unsigned long max ;
2906};
2907#line 29 "include/linux/key.h"
2908typedef int32_t key_serial_t;
2909#line 32 "include/linux/key.h"
2910typedef uint32_t key_perm_t;
2911#line 33
2912struct key;
2913#line 33
2914struct key;
2915#line 33
2916struct key;
2917#line 33
2918struct key;
2919#line 34
2920struct signal_struct;
2921#line 34
2922struct signal_struct;
2923#line 34
2924struct signal_struct;
2925#line 34
2926struct signal_struct;
2927#line 35
2928struct key_type;
2929#line 35
2930struct key_type;
2931#line 35
2932struct key_type;
2933#line 35
2934struct key_type;
2935#line 37
2936struct keyring_list;
2937#line 37
2938struct keyring_list;
2939#line 37
2940struct keyring_list;
2941#line 37
2942struct keyring_list;
2943#line 115
2944struct key_user;
2945#line 115
2946struct key_user;
2947#line 115
2948struct key_user;
2949#line 115 "include/linux/key.h"
2950union __anonunion_ldv_19317_157 {
2951 time_t expiry ;
2952 time_t revoked_at ;
2953};
2954#line 115 "include/linux/key.h"
2955union __anonunion_type_data_158 {
2956 struct list_head link ;
2957 unsigned long x[2U] ;
2958 void *p[2U] ;
2959 int reject_error ;
2960};
2961#line 115 "include/linux/key.h"
2962union __anonunion_payload_159 {
2963 unsigned long value ;
2964 void *rcudata ;
2965 void *data ;
2966 struct keyring_list *subscriptions ;
2967};
2968#line 115 "include/linux/key.h"
2969struct key {
2970 atomic_t usage ;
2971 key_serial_t serial ;
2972 struct rb_node serial_node ;
2973 struct key_type *type ;
2974 struct rw_semaphore sem ;
2975 struct key_user *user ;
2976 void *security ;
2977 union __anonunion_ldv_19317_157 ldv_19317 ;
2978 uid_t uid ;
2979 gid_t gid ;
2980 key_perm_t perm ;
2981 unsigned short quotalen ;
2982 unsigned short datalen ;
2983 unsigned long flags ;
2984 char *description ;
2985 union __anonunion_type_data_158 type_data ;
2986 union __anonunion_payload_159 payload ;
2987};
2988#line 310
2989struct audit_context;
2990#line 310
2991struct audit_context;
2992#line 310
2993struct audit_context;
2994#line 310
2995struct audit_context;
2996#line 27 "include/linux/selinux.h"
2997struct group_info {
2998 atomic_t usage ;
2999 int ngroups ;
3000 int nblocks ;
3001 gid_t small_block[32U] ;
3002 gid_t *blocks[0U] ;
3003};
3004#line 77 "include/linux/cred.h"
3005struct thread_group_cred {
3006 atomic_t usage ;
3007 pid_t tgid ;
3008 spinlock_t lock ;
3009 struct key *session_keyring ;
3010 struct key *process_keyring ;
3011 struct rcu_head rcu ;
3012};
3013#line 91 "include/linux/cred.h"
3014struct cred {
3015 atomic_t usage ;
3016 atomic_t subscribers ;
3017 void *put_addr ;
3018 unsigned int magic ;
3019 uid_t uid ;
3020 gid_t gid ;
3021 uid_t suid ;
3022 gid_t sgid ;
3023 uid_t euid ;
3024 gid_t egid ;
3025 uid_t fsuid ;
3026 gid_t fsgid ;
3027 unsigned int securebits ;
3028 kernel_cap_t cap_inheritable ;
3029 kernel_cap_t cap_permitted ;
3030 kernel_cap_t cap_effective ;
3031 kernel_cap_t cap_bset ;
3032 unsigned char jit_keyring ;
3033 struct key *thread_keyring ;
3034 struct key *request_key_auth ;
3035 struct thread_group_cred *tgcred ;
3036 void *security ;
3037 struct user_struct *user ;
3038 struct user_namespace *user_ns ;
3039 struct group_info *group_info ;
3040 struct rcu_head rcu ;
3041};
3042#line 264
3043struct futex_pi_state;
3044#line 264
3045struct futex_pi_state;
3046#line 264
3047struct futex_pi_state;
3048#line 264
3049struct futex_pi_state;
3050#line 265
3051struct robust_list_head;
3052#line 265
3053struct robust_list_head;
3054#line 265
3055struct robust_list_head;
3056#line 265
3057struct robust_list_head;
3058#line 266
3059struct bio_list;
3060#line 266
3061struct bio_list;
3062#line 266
3063struct bio_list;
3064#line 266
3065struct bio_list;
3066#line 267
3067struct fs_struct;
3068#line 267
3069struct fs_struct;
3070#line 267
3071struct fs_struct;
3072#line 267
3073struct fs_struct;
3074#line 268
3075struct perf_event_context;
3076#line 268
3077struct perf_event_context;
3078#line 268
3079struct perf_event_context;
3080#line 268
3081struct perf_event_context;
3082#line 269
3083struct blk_plug;
3084#line 269
3085struct blk_plug;
3086#line 269
3087struct blk_plug;
3088#line 269
3089struct blk_plug;
3090#line 149 "include/linux/sched.h"
3091struct cfs_rq;
3092#line 149
3093struct cfs_rq;
3094#line 149
3095struct cfs_rq;
3096#line 149
3097struct cfs_rq;
3098#line 44 "include/linux/aio_abi.h"
3099struct io_event {
3100 __u64 data ;
3101 __u64 obj ;
3102 __s64 res ;
3103 __s64 res2 ;
3104};
3105#line 106 "include/linux/aio_abi.h"
3106struct iovec {
3107 void *iov_base ;
3108 __kernel_size_t iov_len ;
3109};
3110#line 54 "include/linux/uio.h"
3111struct kioctx;
3112#line 54
3113struct kioctx;
3114#line 54
3115struct kioctx;
3116#line 54
3117struct kioctx;
3118#line 55 "include/linux/uio.h"
3119union __anonunion_ki_obj_160 {
3120 void *user ;
3121 struct task_struct *tsk ;
3122};
3123#line 55
3124struct eventfd_ctx;
3125#line 55
3126struct eventfd_ctx;
3127#line 55
3128struct eventfd_ctx;
3129#line 55 "include/linux/uio.h"
3130struct kiocb {
3131 struct list_head ki_run_list ;
3132 unsigned long ki_flags ;
3133 int ki_users ;
3134 unsigned int ki_key ;
3135 struct file *ki_filp ;
3136 struct kioctx *ki_ctx ;
3137 int (*ki_cancel)(struct kiocb * , struct io_event * ) ;
3138 ssize_t (*ki_retry)(struct kiocb * ) ;
3139 void (*ki_dtor)(struct kiocb * ) ;
3140 union __anonunion_ki_obj_160 ki_obj ;
3141 __u64 ki_user_data ;
3142 loff_t ki_pos ;
3143 void *private ;
3144 unsigned short ki_opcode ;
3145 size_t ki_nbytes ;
3146 char *ki_buf ;
3147 size_t ki_left ;
3148 struct iovec ki_inline_vec ;
3149 struct iovec *ki_iovec ;
3150 unsigned long ki_nr_segs ;
3151 unsigned long ki_cur_seg ;
3152 struct list_head ki_list ;
3153 struct eventfd_ctx *ki_eventfd ;
3154};
3155#line 161 "include/linux/aio.h"
3156struct aio_ring_info {
3157 unsigned long mmap_base ;
3158 unsigned long mmap_size ;
3159 struct page **ring_pages ;
3160 spinlock_t ring_lock ;
3161 long nr_pages ;
3162 unsigned int nr ;
3163 unsigned int tail ;
3164 struct page *internal_pages[8U] ;
3165};
3166#line 177 "include/linux/aio.h"
3167struct kioctx {
3168 atomic_t users ;
3169 int dead ;
3170 struct mm_struct *mm ;
3171 unsigned long user_id ;
3172 struct hlist_node list ;
3173 wait_queue_head_t wait ;
3174 spinlock_t ctx_lock ;
3175 int reqs_active ;
3176 struct list_head active_reqs ;
3177 struct list_head run_list ;
3178 unsigned int max_reqs ;
3179 struct aio_ring_info ring_info ;
3180 struct delayed_work wq ;
3181 struct rcu_head rcu_head ;
3182};
3183#line 404 "include/linux/sched.h"
3184struct sighand_struct {
3185 atomic_t count ;
3186 struct k_sigaction action[64U] ;
3187 spinlock_t siglock ;
3188 wait_queue_head_t signalfd_wqh ;
3189};
3190#line 447 "include/linux/sched.h"
3191struct pacct_struct {
3192 int ac_flag ;
3193 long ac_exitcode ;
3194 unsigned long ac_mem ;
3195 cputime_t ac_utime ;
3196 cputime_t ac_stime ;
3197 unsigned long ac_minflt ;
3198 unsigned long ac_majflt ;
3199};
3200#line 455 "include/linux/sched.h"
3201struct cpu_itimer {
3202 cputime_t expires ;
3203 cputime_t incr ;
3204 u32 error ;
3205 u32 incr_error ;
3206};
3207#line 462 "include/linux/sched.h"
3208struct task_cputime {
3209 cputime_t utime ;
3210 cputime_t stime ;
3211 unsigned long long sum_exec_runtime ;
3212};
3213#line 479 "include/linux/sched.h"
3214struct thread_group_cputimer {
3215 struct task_cputime cputime ;
3216 int running ;
3217 spinlock_t lock ;
3218};
3219#line 515
3220struct autogroup;
3221#line 515
3222struct autogroup;
3223#line 515
3224struct autogroup;
3225#line 515
3226struct autogroup;
3227#line 516
3228struct tty_struct;
3229#line 516
3230struct tty_struct;
3231#line 516
3232struct tty_struct;
3233#line 516
3234struct taskstats;
3235#line 516
3236struct taskstats;
3237#line 516
3238struct taskstats;
3239#line 516
3240struct tty_audit_buf;
3241#line 516
3242struct tty_audit_buf;
3243#line 516
3244struct tty_audit_buf;
3245#line 516 "include/linux/sched.h"
3246struct signal_struct {
3247 atomic_t sigcnt ;
3248 atomic_t live ;
3249 int nr_threads ;
3250 wait_queue_head_t wait_chldexit ;
3251 struct task_struct *curr_target ;
3252 struct sigpending shared_pending ;
3253 int group_exit_code ;
3254 int notify_count ;
3255 struct task_struct *group_exit_task ;
3256 int group_stop_count ;
3257 unsigned int flags ;
3258 struct list_head posix_timers ;
3259 struct hrtimer real_timer ;
3260 struct pid *leader_pid ;
3261 ktime_t it_real_incr ;
3262 struct cpu_itimer it[2U] ;
3263 struct thread_group_cputimer cputimer ;
3264 struct task_cputime cputime_expires ;
3265 struct list_head cpu_timers[3U] ;
3266 struct pid *tty_old_pgrp ;
3267 int leader ;
3268 struct tty_struct *tty ;
3269 struct autogroup *autogroup ;
3270 cputime_t utime ;
3271 cputime_t stime ;
3272 cputime_t cutime ;
3273 cputime_t cstime ;
3274 cputime_t gtime ;
3275 cputime_t cgtime ;
3276 cputime_t prev_utime ;
3277 cputime_t prev_stime ;
3278 unsigned long nvcsw ;
3279 unsigned long nivcsw ;
3280 unsigned long cnvcsw ;
3281 unsigned long cnivcsw ;
3282 unsigned long min_flt ;
3283 unsigned long maj_flt ;
3284 unsigned long cmin_flt ;
3285 unsigned long cmaj_flt ;
3286 unsigned long inblock ;
3287 unsigned long oublock ;
3288 unsigned long cinblock ;
3289 unsigned long coublock ;
3290 unsigned long maxrss ;
3291 unsigned long cmaxrss ;
3292 struct task_io_accounting ioac ;
3293 unsigned long long sum_sched_runtime ;
3294 struct rlimit rlim[16U] ;
3295 struct pacct_struct pacct ;
3296 struct taskstats *stats ;
3297 unsigned int audit_tty ;
3298 struct tty_audit_buf *tty_audit_buf ;
3299 struct rw_semaphore threadgroup_fork_lock ;
3300 int oom_adj ;
3301 int oom_score_adj ;
3302 int oom_score_adj_min ;
3303 struct mutex cred_guard_mutex ;
3304};
3305#line 683 "include/linux/sched.h"
3306struct user_struct {
3307 atomic_t __count ;
3308 atomic_t processes ;
3309 atomic_t files ;
3310 atomic_t sigpending ;
3311 atomic_t inotify_watches ;
3312 atomic_t inotify_devs ;
3313 atomic_t fanotify_listeners ;
3314 atomic_long_t epoll_watches ;
3315 unsigned long mq_bytes ;
3316 unsigned long locked_shm ;
3317 struct key *uid_keyring ;
3318 struct key *session_keyring ;
3319 struct hlist_node uidhash_node ;
3320 uid_t uid ;
3321 struct user_namespace *user_ns ;
3322 atomic_long_t locked_vm ;
3323};
3324#line 728
3325struct reclaim_state;
3326#line 728
3327struct reclaim_state;
3328#line 728
3329struct reclaim_state;
3330#line 728
3331struct reclaim_state;
3332#line 729 "include/linux/sched.h"
3333struct sched_info {
3334 unsigned long pcount ;
3335 unsigned long long run_delay ;
3336 unsigned long long last_arrival ;
3337 unsigned long long last_queued ;
3338};
3339#line 744 "include/linux/sched.h"
3340struct task_delay_info {
3341 spinlock_t lock ;
3342 unsigned int flags ;
3343 struct timespec blkio_start ;
3344 struct timespec blkio_end ;
3345 u64 blkio_delay ;
3346 u64 swapin_delay ;
3347 u32 blkio_count ;
3348 u32 swapin_count ;
3349 struct timespec freepages_start ;
3350 struct timespec freepages_end ;
3351 u64 freepages_delay ;
3352 u32 freepages_count ;
3353};
3354#line 1037
3355struct io_context;
3356#line 1037
3357struct io_context;
3358#line 1037
3359struct io_context;
3360#line 1037
3361struct io_context;
3362#line 1060
3363struct rq;
3364#line 1060
3365struct rq;
3366#line 1060
3367struct rq;
3368#line 1060
3369struct rq;
3370#line 1061 "include/linux/sched.h"
3371struct sched_class {
3372 struct sched_class const *next ;
3373 void (*enqueue_task)(struct rq * , struct task_struct * , int ) ;
3374 void (*dequeue_task)(struct rq * , struct task_struct * , int ) ;
3375 void (*yield_task)(struct rq * ) ;
3376 bool (*yield_to_task)(struct rq * , struct task_struct * , bool ) ;
3377 void (*check_preempt_curr)(struct rq * , struct task_struct * , int ) ;
3378 struct task_struct *(*pick_next_task)(struct rq * ) ;
3379 void (*put_prev_task)(struct rq * , struct task_struct * ) ;
3380 int (*select_task_rq)(struct task_struct * , int , int ) ;
3381 void (*pre_schedule)(struct rq * , struct task_struct * ) ;
3382 void (*post_schedule)(struct rq * ) ;
3383 void (*task_waking)(struct task_struct * ) ;
3384 void (*task_woken)(struct rq * , struct task_struct * ) ;
3385 void (*set_cpus_allowed)(struct task_struct * , struct cpumask const * ) ;
3386 void (*rq_online)(struct rq * ) ;
3387 void (*rq_offline)(struct rq * ) ;
3388 void (*set_curr_task)(struct rq * ) ;
3389 void (*task_tick)(struct rq * , struct task_struct * , int ) ;
3390 void (*task_fork)(struct task_struct * ) ;
3391 void (*switched_from)(struct rq * , struct task_struct * ) ;
3392 void (*switched_to)(struct rq * , struct task_struct * ) ;
3393 void (*prio_changed)(struct rq * , struct task_struct * , int ) ;
3394 unsigned int (*get_rr_interval)(struct rq * , struct task_struct * ) ;
3395 void (*task_move_group)(struct task_struct * , int ) ;
3396};
3397#line 1127 "include/linux/sched.h"
3398struct load_weight {
3399 unsigned long weight ;
3400 unsigned long inv_weight ;
3401};
3402#line 1132 "include/linux/sched.h"
3403struct sched_statistics {
3404 u64 wait_start ;
3405 u64 wait_max ;
3406 u64 wait_count ;
3407 u64 wait_sum ;
3408 u64 iowait_count ;
3409 u64 iowait_sum ;
3410 u64 sleep_start ;
3411 u64 sleep_max ;
3412 s64 sum_sleep_runtime ;
3413 u64 block_start ;
3414 u64 block_max ;
3415 u64 exec_max ;
3416 u64 slice_max ;
3417 u64 nr_migrations_cold ;
3418 u64 nr_failed_migrations_affine ;
3419 u64 nr_failed_migrations_running ;
3420 u64 nr_failed_migrations_hot ;
3421 u64 nr_forced_migrations ;
3422 u64 nr_wakeups ;
3423 u64 nr_wakeups_sync ;
3424 u64 nr_wakeups_migrate ;
3425 u64 nr_wakeups_local ;
3426 u64 nr_wakeups_remote ;
3427 u64 nr_wakeups_affine ;
3428 u64 nr_wakeups_affine_attempts ;
3429 u64 nr_wakeups_passive ;
3430 u64 nr_wakeups_idle ;
3431};
3432#line 1167 "include/linux/sched.h"
3433struct sched_entity {
3434 struct load_weight load ;
3435 struct rb_node run_node ;
3436 struct list_head group_node ;
3437 unsigned int on_rq ;
3438 u64 exec_start ;
3439 u64 sum_exec_runtime ;
3440 u64 vruntime ;
3441 u64 prev_sum_exec_runtime ;
3442 u64 nr_migrations ;
3443 struct sched_statistics statistics ;
3444 struct sched_entity *parent ;
3445 struct cfs_rq *cfs_rq ;
3446 struct cfs_rq *my_q ;
3447};
3448#line 1193
3449struct rt_rq;
3450#line 1193
3451struct rt_rq;
3452#line 1193
3453struct rt_rq;
3454#line 1193 "include/linux/sched.h"
3455struct sched_rt_entity {
3456 struct list_head run_list ;
3457 unsigned long timeout ;
3458 unsigned int time_slice ;
3459 int nr_cpus_allowed ;
3460 struct sched_rt_entity *back ;
3461 struct sched_rt_entity *parent ;
3462 struct rt_rq *rt_rq ;
3463 struct rt_rq *my_q ;
3464};
3465#line 1217
3466struct mem_cgroup;
3467#line 1217
3468struct mem_cgroup;
3469#line 1217
3470struct mem_cgroup;
3471#line 1217 "include/linux/sched.h"
3472struct memcg_batch_info {
3473 int do_batch ;
3474 struct mem_cgroup *memcg ;
3475 unsigned long nr_pages ;
3476 unsigned long memsw_nr_pages ;
3477};
3478#line 1569
3479struct irqaction;
3480#line 1569
3481struct irqaction;
3482#line 1569
3483struct irqaction;
3484#line 1569
3485struct css_set;
3486#line 1569
3487struct css_set;
3488#line 1569
3489struct css_set;
3490#line 1569
3491struct compat_robust_list_head;
3492#line 1569
3493struct compat_robust_list_head;
3494#line 1569
3495struct compat_robust_list_head;
3496#line 1569
3497struct ftrace_ret_stack;
3498#line 1569
3499struct ftrace_ret_stack;
3500#line 1569
3501struct ftrace_ret_stack;
3502#line 1569 "include/linux/sched.h"
3503struct task_struct {
3504 long volatile state ;
3505 void *stack ;
3506 atomic_t usage ;
3507 unsigned int flags ;
3508 unsigned int ptrace ;
3509 struct task_struct *wake_entry ;
3510 int on_cpu ;
3511 int on_rq ;
3512 int prio ;
3513 int static_prio ;
3514 int normal_prio ;
3515 unsigned int rt_priority ;
3516 struct sched_class const *sched_class ;
3517 struct sched_entity se ;
3518 struct sched_rt_entity rt ;
3519 struct hlist_head preempt_notifiers ;
3520 unsigned char fpu_counter ;
3521 unsigned int btrace_seq ;
3522 unsigned int policy ;
3523 cpumask_t cpus_allowed ;
3524 struct sched_info sched_info ;
3525 struct list_head tasks ;
3526 struct plist_node pushable_tasks ;
3527 struct mm_struct *mm ;
3528 struct mm_struct *active_mm ;
3529 unsigned char brk_randomized : 1 ;
3530 int exit_state ;
3531 int exit_code ;
3532 int exit_signal ;
3533 int pdeath_signal ;
3534 unsigned int group_stop ;
3535 unsigned int personality ;
3536 unsigned char did_exec : 1 ;
3537 unsigned char in_execve : 1 ;
3538 unsigned char in_iowait : 1 ;
3539 unsigned char sched_reset_on_fork : 1 ;
3540 unsigned char sched_contributes_to_load : 1 ;
3541 pid_t pid ;
3542 pid_t tgid ;
3543 unsigned long stack_canary ;
3544 struct task_struct *real_parent ;
3545 struct task_struct *parent ;
3546 struct list_head children ;
3547 struct list_head sibling ;
3548 struct task_struct *group_leader ;
3549 struct list_head ptraced ;
3550 struct list_head ptrace_entry ;
3551 struct pid_link pids[3U] ;
3552 struct list_head thread_group ;
3553 struct completion *vfork_done ;
3554 int *set_child_tid ;
3555 int *clear_child_tid ;
3556 cputime_t utime ;
3557 cputime_t stime ;
3558 cputime_t utimescaled ;
3559 cputime_t stimescaled ;
3560 cputime_t gtime ;
3561 cputime_t prev_utime ;
3562 cputime_t prev_stime ;
3563 unsigned long nvcsw ;
3564 unsigned long nivcsw ;
3565 struct timespec start_time ;
3566 struct timespec real_start_time ;
3567 unsigned long min_flt ;
3568 unsigned long maj_flt ;
3569 struct task_cputime cputime_expires ;
3570 struct list_head cpu_timers[3U] ;
3571 struct cred const *real_cred ;
3572 struct cred const *cred ;
3573 struct cred *replacement_session_keyring ;
3574 char comm[16U] ;
3575 int link_count ;
3576 int total_link_count ;
3577 struct sysv_sem sysvsem ;
3578 unsigned long last_switch_count ;
3579 struct thread_struct thread ;
3580 struct fs_struct *fs ;
3581 struct files_struct *files ;
3582 struct nsproxy *nsproxy ;
3583 struct signal_struct *signal ;
3584 struct sighand_struct *sighand ;
3585 sigset_t blocked ;
3586 sigset_t real_blocked ;
3587 sigset_t saved_sigmask ;
3588 struct sigpending pending ;
3589 unsigned long sas_ss_sp ;
3590 size_t sas_ss_size ;
3591 int (*notifier)(void * ) ;
3592 void *notifier_data ;
3593 sigset_t *notifier_mask ;
3594 struct audit_context *audit_context ;
3595 uid_t loginuid ;
3596 unsigned int sessionid ;
3597 seccomp_t seccomp ;
3598 u32 parent_exec_id ;
3599 u32 self_exec_id ;
3600 spinlock_t alloc_lock ;
3601 struct irqaction *irqaction ;
3602 raw_spinlock_t pi_lock ;
3603 struct plist_head pi_waiters ;
3604 struct rt_mutex_waiter *pi_blocked_on ;
3605 struct mutex_waiter *blocked_on ;
3606 unsigned int irq_events ;
3607 unsigned long hardirq_enable_ip ;
3608 unsigned long hardirq_disable_ip ;
3609 unsigned int hardirq_enable_event ;
3610 unsigned int hardirq_disable_event ;
3611 int hardirqs_enabled ;
3612 int hardirq_context ;
3613 unsigned long softirq_disable_ip ;
3614 unsigned long softirq_enable_ip ;
3615 unsigned int softirq_disable_event ;
3616 unsigned int softirq_enable_event ;
3617 int softirqs_enabled ;
3618 int softirq_context ;
3619 u64 curr_chain_key ;
3620 int lockdep_depth ;
3621 unsigned int lockdep_recursion ;
3622 struct held_lock held_locks[48U] ;
3623 gfp_t lockdep_reclaim_gfp ;
3624 void *journal_info ;
3625 struct bio_list *bio_list ;
3626 struct blk_plug *plug ;
3627 struct reclaim_state *reclaim_state ;
3628 struct backing_dev_info *backing_dev_info ;
3629 struct io_context *io_context ;
3630 unsigned long ptrace_message ;
3631 siginfo_t *last_siginfo ;
3632 struct task_io_accounting ioac ;
3633 u64 acct_rss_mem1 ;
3634 u64 acct_vm_mem1 ;
3635 cputime_t acct_timexpd ;
3636 nodemask_t mems_allowed ;
3637 int mems_allowed_change_disable ;
3638 int cpuset_mem_spread_rotor ;
3639 int cpuset_slab_spread_rotor ;
3640 struct css_set *cgroups ;
3641 struct list_head cg_list ;
3642 struct robust_list_head *robust_list ;
3643 struct compat_robust_list_head *compat_robust_list ;
3644 struct list_head pi_state_list ;
3645 struct futex_pi_state *pi_state_cache ;
3646 struct perf_event_context *perf_event_ctxp[2U] ;
3647 struct mutex perf_event_mutex ;
3648 struct list_head perf_event_list ;
3649 struct mempolicy *mempolicy ;
3650 short il_next ;
3651 short pref_node_fork ;
3652 atomic_t fs_excl ;
3653 struct rcu_head rcu ;
3654 struct pipe_inode_info *splice_pipe ;
3655 struct task_delay_info *delays ;
3656 int make_it_fail ;
3657 struct prop_local_single dirties ;
3658 int latency_record_count ;
3659 struct latency_record latency_record[32U] ;
3660 unsigned long timer_slack_ns ;
3661 unsigned long default_timer_slack_ns ;
3662 struct list_head *scm_work_list ;
3663 int curr_ret_stack ;
3664 struct ftrace_ret_stack *ret_stack ;
3665 unsigned long long ftrace_timestamp ;
3666 atomic_t trace_overrun ;
3667 atomic_t tracing_graph_pause ;
3668 unsigned long trace ;
3669 unsigned long trace_recursion ;
3670 struct memcg_batch_info memcg_batch ;
3671 atomic_t ptrace_bp_refcnt ;
3672};
3673#line 2698 "include/linux/sched.h"
3674struct exception_table_entry {
3675 unsigned long insn ;
3676 unsigned long fixup ;
3677};
3678#line 168 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3679struct pi_protocol;
3680#line 168
3681struct pi_protocol;
3682#line 168
3683struct pi_protocol;
3684#line 168 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3685struct pi_adapter {
3686 struct pi_protocol *proto ;
3687 int port ;
3688 int mode ;
3689 int delay ;
3690 int devtype ;
3691 char *device ;
3692 int unit ;
3693 int saved_r0 ;
3694 int saved_r2 ;
3695 int reserved ;
3696 unsigned long private ;
3697 wait_queue_head_t parq ;
3698 void *pardev ;
3699 char *parname ;
3700 int claimed ;
3701 void (*claim_cont)(void) ;
3702};
3703#line 57 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/drivers/block/paride/paride.h"
3704typedef struct pi_adapter PIA;
3705#line 134 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/drivers/block/paride/paride.h"
3706struct pi_protocol {
3707 char name[8U] ;
3708 int index ;
3709 int max_mode ;
3710 int epp_first ;
3711 int default_delay ;
3712 int max_units ;
3713 void (*write_regr)(PIA * , int , int , int ) ;
3714 int (*read_regr)(PIA * , int , int ) ;
3715 void (*write_block)(PIA * , char * , int ) ;
3716 void (*read_block)(PIA * , char * , int ) ;
3717 void (*connect)(PIA * ) ;
3718 void (*disconnect)(PIA * ) ;
3719 int (*test_port)(PIA * ) ;
3720 int (*probe_unit)(PIA * ) ;
3721 int (*test_proto)(PIA * , char * , int ) ;
3722 void (*log_adapter)(PIA * , char * , int ) ;
3723 int (*init_proto)(PIA * ) ;
3724 void (*release_proto)(PIA * ) ;
3725 struct module *owner ;
3726};
3727#line 209 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3728struct pt_unit {
3729 struct pi_adapter pia ;
3730 struct pi_adapter *pi ;
3731 int flags ;
3732 int last_sense ;
3733 int drive ;
3734 atomic_t available ;
3735 int bs ;
3736 int capacity ;
3737 int present ;
3738 char *bufptr ;
3739 char name[8U] ;
3740};
3741#line 1 "<compiler builtins>"
3742unsigned long __builtin_object_size(void * , int ) ;
3743#line 1
3744long __builtin_expect(long , long ) ;
3745#line 101 "include/linux/printk.h"
3746extern int printk(char const * , ...) ;
3747#line 64 "include/asm-generic/bug.h"
3748extern void warn_slowpath_fmt(char const * , int , char const * , ...) ;
3749#line 170 "include/linux/kernel.h"
3750extern void might_fault(void) ;
3751#line 295
3752extern int snprintf(char * , size_t , char const * , ...) ;
3753#line 27 "include/linux/err.h"
3754__inline static long PTR_ERR(void const *ptr )
3755{
3756
3757 {
3758#line 29
3759 return ((long )ptr);
3760}
3761}
3762#line 32 "include/linux/err.h"
3763__inline static long IS_ERR(void const *ptr )
3764{ long tmp ;
3765 unsigned long __cil_tmp3 ;
3766 int __cil_tmp4 ;
3767 long __cil_tmp5 ;
3768
3769 {
3770 {
3771#line 34
3772 __cil_tmp3 = (unsigned long )ptr;
3773#line 34
3774 __cil_tmp4 = __cil_tmp3 > 1152921504606842880UL;
3775#line 34
3776 __cil_tmp5 = (long )__cil_tmp4;
3777#line 34
3778 tmp = __builtin_expect(__cil_tmp5, 0L);
3779 }
3780#line 34
3781 return (tmp);
3782}
3783}
3784#line 23 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/atomic.h"
3785__inline static int atomic_read(atomic_t const *v )
3786{ int const *__cil_tmp2 ;
3787 int volatile *__cil_tmp3 ;
3788 int volatile __cil_tmp4 ;
3789
3790 {
3791 {
3792#line 25
3793 __cil_tmp2 = & v->counter;
3794#line 25
3795 __cil_tmp3 = (int volatile *)__cil_tmp2;
3796#line 25
3797 __cil_tmp4 = *__cil_tmp3;
3798#line 25
3799 return ((int )__cil_tmp4);
3800 }
3801}
3802}
3803#line 35 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/atomic.h"
3804__inline static void atomic_set(atomic_t *v , int i )
3805{
3806
3807 {
3808#line 37
3809 v->counter = i;
3810#line 38
3811 return;
3812}
3813}
3814#line 93 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/atomic.h"
3815__inline static void atomic_inc(atomic_t *v )
3816{
3817
3818 {
3819#line 95
3820 __asm__ volatile (".section .smp_locks,\"a\"\n.balign 4\n.long 671f - .\n.previous\n671:\n\tlock; incl %0": "+m" (v->counter));
3821#line 97
3822 return;
3823}
3824}
3825#line 119 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/atomic.h"
3826__inline static int atomic_dec_and_test(atomic_t *v )
3827{ unsigned char c ;
3828 unsigned int __cil_tmp3 ;
3829
3830 {
3831#line 123
3832 __asm__ volatile (".section .smp_locks,\"a\"\n.balign 4\n.long 671f - .\n.previous\n671:\n\tlock; decl %0; sete %1": "+m" (v->counter),
3833 "=qm" (c): : "memory");
3834 {
3835#line 126
3836 __cil_tmp3 = (unsigned int )c;
3837#line 126
3838 return (__cil_tmp3 != 0U);
3839 }
3840}
3841}
3842#line 134 "include/linux/mutex.h"
3843extern void mutex_lock_nested(struct mutex * , unsigned int ) ;
3844#line 169
3845extern void mutex_unlock(struct mutex * ) ;
3846#line 830 "include/linux/rcupdate.h"
3847extern void kfree(void const * ) ;
3848#line 99 "include/linux/module.h"
3849extern struct module __this_module ;
3850#line 3 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3851int ldv_try_module_get(struct module *module ) ;
3852#line 4
3853void ldv_module_get(struct module *module ) ;
3854#line 5
3855void ldv_module_put(struct module *module ) ;
3856#line 6
3857unsigned int ldv_module_refcount(void) ;
3858#line 7
3859void ldv_module_put_and_exit(void) ;
3860#line 126 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3861static int verbose = 0;
3862#line 127 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3863static int major = 96;
3864#line 128 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3865static char *name = (char *)"pt";
3866#line 129 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3867static int disable = 0;
3868#line 131 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3869static int drive0[6U] = { 0, 0, 0, -1,
3870 -1, -1};
3871#line 132 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3872static int drive1[6U] = { 0, 0, 0, -1,
3873 -1, -1};
3874#line 133 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3875static int drive2[6U] = { 0, 0, 0, -1,
3876 -1, -1};
3877#line 134 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3878static int drive3[6U] = { 0, 0, 0, -1,
3879 -1, -1};
3880#line 136 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
3881static int (*drives[4U])[6U] = { & drive0, & drive1, & drive2, & drive3};
3882#line 891 "include/linux/fs.h"
3883__inline static unsigned int iminor(struct inode const *inode )
3884{ dev_t __cil_tmp2 ;
3885 unsigned int __cil_tmp3 ;
3886
3887 {
3888 {
3889#line 893
3890 __cil_tmp2 = inode->i_rdev;
3891#line 893
3892 __cil_tmp3 = (unsigned int )__cil_tmp2;
3893#line 893
3894 return (__cil_tmp3 & 1048575U);
3895 }
3896}
3897}
3898#line 2089
3899extern int __register_chrdev(unsigned int , unsigned int , unsigned int , char const * ,
3900 struct file_operations const * ) ;
3901#line 2092
3902extern void __unregister_chrdev(unsigned int , unsigned int , unsigned int , char const * ) ;
3903#line 2097 "include/linux/fs.h"
3904__inline static int register_chrdev(unsigned int major___0 , char const *name___0 ,
3905 struct file_operations const *fops )
3906{ int tmp ;
3907
3908 {
3909 {
3910#line 2100
3911 tmp = __register_chrdev(major___0, 0U, 256U, name___0, fops);
3912 }
3913#line 2100
3914 return (tmp);
3915}
3916}
3917#line 2103 "include/linux/fs.h"
3918__inline static void unregister_chrdev(unsigned int major___0 , char const *name___0 )
3919{
3920
3921 {
3922 {
3923#line 2105
3924 __unregister_chrdev(major___0, 0U, 256U, name___0);
3925 }
3926#line 2106
3927 return;
3928}
3929}
3930#line 2336
3931extern loff_t noop_llseek(struct file * , loff_t , int ) ;
3932#line 16 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/delay.h"
3933extern void __const_udelay(unsigned long ) ;
3934#line 221 "include/linux/slub_def.h"
3935extern void *__kmalloc(size_t , gfp_t ) ;
3936#line 255 "include/linux/slub_def.h"
3937__inline static void *kmalloc(size_t size , gfp_t flags )
3938{ void *tmp___2 ;
3939
3940 {
3941 {
3942#line 270
3943 tmp___2 = __kmalloc(size, flags);
3944 }
3945#line 270
3946 return (tmp___2);
3947}
3948}
3949#line 391 "include/linux/device.h"
3950extern struct class *__class_create(struct module * , char const * , struct lock_class_key * ) ;
3951#line 394
3952extern void class_destroy(struct class * ) ;
3953#line 743
3954extern struct device *device_create(struct class * , struct device * , dev_t , void * ,
3955 char const * , ...) ;
3956#line 747
3957extern void device_destroy(struct class * , dev_t ) ;
3958#line 358 "include/linux/sched.h"
3959extern long schedule_timeout_interruptible(long ) ;
3960#line 40 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/uaccess_64.h"
3961extern unsigned long _copy_to_user(void * , void const * , unsigned int ) ;
3962#line 42
3963extern unsigned long _copy_from_user(void * , void const * , unsigned int ) ;
3964#line 46 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/uaccess_64.h"
3965__inline static unsigned long copy_from_user(void *to , void const *from , unsigned long n )
3966{ int sz ;
3967 unsigned long tmp ;
3968 int __ret_warn_on ;
3969 long tmp___0 ;
3970 long tmp___1 ;
3971 long tmp___2 ;
3972 void const *__cil_tmp10 ;
3973 void *__cil_tmp11 ;
3974 int __cil_tmp12 ;
3975 long __cil_tmp13 ;
3976 unsigned int __cil_tmp14 ;
3977 unsigned long __cil_tmp15 ;
3978 int __cil_tmp16 ;
3979 long __cil_tmp17 ;
3980 unsigned int __cil_tmp18 ;
3981 int __cil_tmp19 ;
3982 long __cil_tmp20 ;
3983 int __cil_tmp21 ;
3984 int __cil_tmp22 ;
3985 int __cil_tmp23 ;
3986 long __cil_tmp24 ;
3987
3988 {
3989 {
3990#line 50
3991 __cil_tmp10 = (void const *)to;
3992#line 50
3993 __cil_tmp11 = (void *)__cil_tmp10;
3994#line 50
3995 tmp = __builtin_object_size(__cil_tmp11, 0);
3996#line 50
3997 sz = (int )tmp;
3998#line 52
3999 might_fault();
4000#line 53
4001 __cil_tmp12 = sz == -1;
4002#line 53
4003 __cil_tmp13 = (long )__cil_tmp12;
4004#line 53
4005 tmp___1 = __builtin_expect(__cil_tmp13, 1L);
4006 }
4007#line 53
4008 if (tmp___1 != 0L) {
4009 {
4010#line 54
4011 __cil_tmp14 = (unsigned int )n;
4012#line 54
4013 n = _copy_from_user(to, from, __cil_tmp14);
4014 }
4015 } else {
4016 {
4017#line 53
4018 __cil_tmp15 = (unsigned long )sz;
4019#line 53
4020 __cil_tmp16 = __cil_tmp15 >= n;
4021#line 53
4022 __cil_tmp17 = (long )__cil_tmp16;
4023#line 53
4024 tmp___2 = __builtin_expect(__cil_tmp17, 1L);
4025 }
4026#line 53
4027 if (tmp___2 != 0L) {
4028 {
4029#line 54
4030 __cil_tmp18 = (unsigned int )n;
4031#line 54
4032 n = _copy_from_user(to, from, __cil_tmp18);
4033 }
4034 } else {
4035 {
4036#line 57
4037 __ret_warn_on = 1;
4038#line 57
4039 __cil_tmp19 = __ret_warn_on != 0;
4040#line 57
4041 __cil_tmp20 = (long )__cil_tmp19;
4042#line 57
4043 tmp___0 = __builtin_expect(__cil_tmp20, 0L);
4044 }
4045#line 57
4046 if (tmp___0 != 0L) {
4047 {
4048#line 57
4049 __cil_tmp21 = (int const )57;
4050#line 57
4051 __cil_tmp22 = (int )__cil_tmp21;
4052#line 57
4053 warn_slowpath_fmt("/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/uaccess_64.h",
4054 __cil_tmp22, "Buffer overflow detected!\n");
4055 }
4056 } else {
4057
4058 }
4059 {
4060#line 57
4061 __cil_tmp23 = __ret_warn_on != 0;
4062#line 57
4063 __cil_tmp24 = (long )__cil_tmp23;
4064#line 57
4065 __builtin_expect(__cil_tmp24, 0L);
4066 }
4067 }
4068 }
4069#line 59
4070 return (n);
4071}
4072}
4073#line 63 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/uaccess_64.h"
4074__inline static int copy_to_user(void *dst , void const *src , unsigned int size )
4075{ unsigned long tmp ;
4076
4077 {
4078 {
4079#line 65
4080 might_fault();
4081#line 67
4082 tmp = _copy_to_user(dst, src, size);
4083 }
4084#line 67
4085 return ((int )tmp);
4086}
4087}
4088#line 61 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/drivers/block/paride/paride.h"
4089extern int pi_init(PIA * , int , int , int , int , int , int , char * , int ,
4090 int , char * ) ;
4091#line 74
4092extern void pi_release(PIA * ) ;
4093#line 83
4094extern void pi_write_regr(PIA * , int , int , int ) ;
4095#line 85
4096extern int pi_read_regr(PIA * , int , int ) ;
4097#line 87
4098extern void pi_write_block(PIA * , char * , int ) ;
4099#line 89
4100extern void pi_read_block(PIA * , char * , int ) ;
4101#line 91
4102extern void pi_connect(PIA * ) ;
4103#line 93
4104extern void pi_disconnect(PIA * ) ;
4105#line 200 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4106static struct mutex pt_mutex = {{1}, {{{{0U}, 3735899821U, 4294967295U, (void *)1152921504606846975UL, {(struct lock_class_key *)0,
4107 {(struct lock_class *)0,
4108 (struct lock_class *)0},
4109 "pt_mutex.wait_lock",
4110 0, 0UL}}}},
4111 {& pt_mutex.wait_list, & pt_mutex.wait_list}, (struct task_struct *)0, (char const *)0,
4112 (void *)(& pt_mutex), {(struct lock_class_key *)0, {(struct lock_class *)0, (struct lock_class *)0},
4113 "pt_mutex", 0, 0UL}};
4114#line 201
4115static int pt_open(struct inode *inode , struct file *file ) ;
4116#line 202
4117static long pt_ioctl(struct file *file , unsigned int cmd , unsigned long arg ) ;
4118#line 203
4119static int pt_release(struct inode *inode , struct file *file ) ;
4120#line 204
4121static ssize_t pt_read(struct file *filp , char *buf , size_t count , loff_t *ppos ) ;
4122#line 206
4123static ssize_t pt_write(struct file *filp , char const *buf , size_t count , loff_t *ppos ) ;
4124#line 208
4125static int pt_detect(void) ;
4126#line 236
4127static int pt_identify(struct pt_unit *tape ) ;
4128#line 238 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4129static struct pt_unit pt[4U] ;
4130#line 240 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4131static char pt_scratch[512U] ;
4132#line 244 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4133static struct file_operations const pt_fops =
4134#line 244
4135 {& __this_module, & noop_llseek, & pt_read, & pt_write, (ssize_t (*)(struct kiocb * ,
4136 struct iovec const * ,
4137 unsigned long ,
4138 loff_t ))0,
4139 (ssize_t (*)(struct kiocb * , struct iovec const * , unsigned long , loff_t ))0,
4140 (int (*)(struct file * , void * , int (*)(void * , char const * , int , loff_t ,
4141 u64 , unsigned int ) ))0, (unsigned int (*)(struct file * ,
4142 struct poll_table_struct * ))0,
4143 & pt_ioctl, (long (*)(struct file * , unsigned int , unsigned long ))0, (int (*)(struct file * ,
4144 struct vm_area_struct * ))0,
4145 & pt_open, (int (*)(struct file * , fl_owner_t ))0, & pt_release, (int (*)(struct file * ,
4146 int ))0,
4147 (int (*)(struct kiocb * , int ))0, (int (*)(int , struct file * , int ))0,
4148 (int (*)(struct file * , int , struct file_lock * ))0, (ssize_t (*)(struct file * ,
4149 struct page * ,
4150 int , size_t ,
4151 loff_t * ,
4152 int ))0,
4153 (unsigned long (*)(struct file * , unsigned long , unsigned long , unsigned long ,
4154 unsigned long ))0, (int (*)(int ))0, (int (*)(struct file * ,
4155 int , struct file_lock * ))0,
4156 (ssize_t (*)(struct pipe_inode_info * , struct file * , loff_t * , size_t , unsigned int ))0,
4157 (ssize_t (*)(struct file * , loff_t * , struct pipe_inode_info * , size_t , unsigned int ))0,
4158 (int (*)(struct file * , long , struct file_lock ** ))0, (long (*)(struct file * ,
4159 int , loff_t ,
4160 loff_t ))0};
4161#line 255 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4162static struct class *pt_class ;
4163#line 257 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4164__inline static int status_reg(struct pi_adapter *pi )
4165{ int tmp ;
4166
4167 {
4168 {
4169#line 259
4170 tmp = pi_read_regr(pi, 1, 6);
4171 }
4172#line 259
4173 return (tmp);
4174}
4175}
4176#line 262 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4177__inline static int read_reg(struct pi_adapter *pi , int reg )
4178{ int tmp ;
4179
4180 {
4181 {
4182#line 264
4183 tmp = pi_read_regr(pi, 0, reg);
4184 }
4185#line 264
4186 return (tmp);
4187}
4188}
4189#line 267 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4190__inline static void write_reg(struct pi_adapter *pi , int reg , int val )
4191{
4192
4193 {
4194 {
4195#line 269
4196 pi_write_regr(pi, 0, reg, val);
4197 }
4198#line 270
4199 return;
4200}
4201}
4202#line 272 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4203__inline static u8 DRIVE(struct pt_unit *tape )
4204{ int __cil_tmp2 ;
4205 int __cil_tmp3 ;
4206 u8 __cil_tmp4 ;
4207 unsigned int __cil_tmp5 ;
4208 unsigned int __cil_tmp6 ;
4209
4210 {
4211 {
4212#line 274
4213 __cil_tmp2 = tape->drive;
4214#line 274
4215 __cil_tmp3 = __cil_tmp2 + 10;
4216#line 274
4217 __cil_tmp4 = (u8 )__cil_tmp3;
4218#line 274
4219 __cil_tmp5 = (unsigned int )__cil_tmp4;
4220#line 274
4221 __cil_tmp6 = __cil_tmp5 * 16U;
4222#line 274
4223 return ((u8 )__cil_tmp6);
4224 }
4225}
4226}
4227#line 277 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4228static int pt_wait(struct pt_unit *tape , int go , int stop , char *fun , char *msg )
4229{ int j ;
4230 int r ;
4231 int e ;
4232 int s ;
4233 int p ;
4234 struct pi_adapter *pi ;
4235 int tmp ;
4236 int __cil_tmp13 ;
4237 int __cil_tmp14 ;
4238 int __cil_tmp15 ;
4239 int __cil_tmp16 ;
4240 char *__cil_tmp17 ;
4241 unsigned long __cil_tmp18 ;
4242 unsigned long __cil_tmp19 ;
4243 char (*__cil_tmp20)[8U] ;
4244 char *__cil_tmp21 ;
4245 int __cil_tmp22 ;
4246
4247 {
4248#line 280
4249 pi = tape->pi;
4250#line 282
4251 j = 0;
4252#line 283
4253 goto ldv_21508;
4254 ldv_21507:
4255 {
4256#line 285
4257 __const_udelay(214750UL);
4258 }
4259 ldv_21508:
4260 {
4261#line 283
4262 r = status_reg(pi);
4263 }
4264 {
4265#line 283
4266 __cil_tmp13 = r & go;
4267#line 283
4268 if (__cil_tmp13 != 0) {
4269#line 283
4270 goto _L;
4271 } else
4272#line 283
4273 if (stop != 0) {
4274 {
4275#line 283
4276 __cil_tmp14 = r & stop;
4277#line 283
4278 if (__cil_tmp14 == 0) {
4279 _L:
4280#line 283
4281 tmp = j;
4282#line 283
4283 j = j + 1;
4284#line 283
4285 if (tmp <= 239999) {
4286#line 285
4287 goto ldv_21507;
4288 } else {
4289#line 287
4290 goto ldv_21509;
4291 }
4292 } else {
4293#line 287
4294 goto ldv_21509;
4295 }
4296 }
4297 } else {
4298#line 287
4299 goto ldv_21509;
4300 }
4301 }
4302 ldv_21509: ;
4303 {
4304#line 287
4305 __cil_tmp15 = stop & 1;
4306#line 287
4307 __cil_tmp16 = __cil_tmp15 & r;
4308#line 287
4309 if (__cil_tmp16 != 0) {
4310#line 287
4311 goto _L___0;
4312 } else
4313#line 287
4314 if (j > 240000) {
4315 _L___0:
4316 {
4317#line 288
4318 s = read_reg(pi, 7);
4319#line 289
4320 e = read_reg(pi, 1);
4321#line 290
4322 p = read_reg(pi, 2);
4323 }
4324#line 291
4325 if (j > 240000) {
4326#line 292
4327 e = e | 256;
4328 } else {
4329
4330 }
4331 {
4332#line 293
4333 __cil_tmp17 = (char *)0;
4334#line 293
4335 __cil_tmp18 = (unsigned long )__cil_tmp17;
4336#line 293
4337 __cil_tmp19 = (unsigned long )fun;
4338#line 293
4339 if (__cil_tmp19 != __cil_tmp18) {
4340 {
4341#line 294
4342 __cil_tmp20 = & tape->name;
4343#line 294
4344 __cil_tmp21 = (char *)__cil_tmp20;
4345#line 294
4346 printk("%s: %s %s: alt=0x%x stat=0x%x err=0x%x loop=%d phase=%d\n", __cil_tmp21,
4347 fun, msg, r, s, e, j, p);
4348 }
4349 } else {
4350
4351 }
4352 }
4353 {
4354#line 297
4355 __cil_tmp22 = e << 8;
4356#line 297
4357 return (__cil_tmp22 + s);
4358 }
4359 } else {
4360
4361 }
4362 }
4363#line 299
4364 return (0);
4365}
4366}
4367#line 302 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4368static int pt_command(struct pt_unit *tape , char *cmd , int dlen , char *fun )
4369{ struct pi_adapter *pi ;
4370 u8 tmp ;
4371 int tmp___0 ;
4372 int tmp___1 ;
4373 int tmp___2 ;
4374 int __cil_tmp10 ;
4375 char *__cil_tmp11 ;
4376 int __cil_tmp12 ;
4377 int __cil_tmp13 ;
4378 char *__cil_tmp14 ;
4379 char (*__cil_tmp15)[8U] ;
4380 char *__cil_tmp16 ;
4381
4382 {
4383 {
4384#line 304
4385 pi = tape->pi;
4386#line 305
4387 pi_connect(pi);
4388#line 307
4389 tmp = DRIVE(tape);
4390#line 307
4391 __cil_tmp10 = (int )tmp;
4392#line 307
4393 write_reg(pi, 6, __cil_tmp10);
4394#line 309
4395 __cil_tmp11 = (char *)"before command";
4396#line 309
4397 tmp___0 = pt_wait(tape, 136, 0, fun, __cil_tmp11);
4398 }
4399#line 309
4400 if (tmp___0 != 0) {
4401 {
4402#line 310
4403 pi_disconnect(pi);
4404 }
4405#line 311
4406 return (-1);
4407 } else {
4408
4409 }
4410 {
4411#line 314
4412 __cil_tmp12 = dlen % 256;
4413#line 314
4414 write_reg(pi, 4, __cil_tmp12);
4415#line 315
4416 __cil_tmp13 = dlen / 256;
4417#line 315
4418 write_reg(pi, 5, __cil_tmp13);
4419#line 316
4420 write_reg(pi, 7, 160);
4421#line 318
4422 __cil_tmp14 = (char *)"command DRQ";
4423#line 318
4424 tmp___1 = pt_wait(tape, 128, 8, fun, __cil_tmp14);
4425 }
4426#line 318
4427 if (tmp___1 != 0) {
4428 {
4429#line 319
4430 pi_disconnect(pi);
4431 }
4432#line 320
4433 return (-1);
4434 } else {
4435
4436 }
4437 {
4438#line 323
4439 tmp___2 = read_reg(pi, 2);
4440 }
4441#line 323
4442 if (tmp___2 != 1) {
4443 {
4444#line 324
4445 __cil_tmp15 = & tape->name;
4446#line 324
4447 __cil_tmp16 = (char *)__cil_tmp15;
4448#line 324
4449 printk("%s: %s: command phase error\n", __cil_tmp16, fun);
4450#line 325
4451 pi_disconnect(pi);
4452 }
4453#line 326
4454 return (-1);
4455 } else {
4456
4457 }
4458 {
4459#line 329
4460 pi_write_block(pi, cmd, 12);
4461 }
4462#line 331
4463 return (0);
4464}
4465}
4466#line 334 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4467static int pt_completion(struct pt_unit *tape , char *buf , char *fun )
4468{ struct pi_adapter *pi ;
4469 int r ;
4470 int s ;
4471 int n ;
4472 int p ;
4473 int tmp ;
4474 int tmp___0 ;
4475 int tmp___1 ;
4476 int tmp___2 ;
4477 int tmp___3 ;
4478 char *__cil_tmp14 ;
4479 int __cil_tmp15 ;
4480 int __cil_tmp16 ;
4481 int __cil_tmp17 ;
4482 int __cil_tmp18 ;
4483 char *__cil_tmp19 ;
4484
4485 {
4486 {
4487#line 336
4488 pi = tape->pi;
4489#line 339
4490 __cil_tmp14 = (char *)"completion";
4491#line 339
4492 r = pt_wait(tape, 128, 73, fun, __cil_tmp14);
4493#line 342
4494 tmp___2 = read_reg(pi, 7);
4495 }
4496 {
4497#line 342
4498 __cil_tmp15 = tmp___2 & 8;
4499#line 342
4500 if (__cil_tmp15 != 0) {
4501 {
4502#line 343
4503 tmp = read_reg(pi, 4);
4504#line 343
4505 tmp___0 = read_reg(pi, 5);
4506#line 343
4507 __cil_tmp16 = tmp___0 * 256;
4508#line 343
4509 __cil_tmp17 = tmp + __cil_tmp16;
4510#line 343
4511 __cil_tmp18 = __cil_tmp17 + 3;
4512#line 343
4513 n = __cil_tmp18 & 65532;
4514#line 345
4515 tmp___1 = read_reg(pi, 2);
4516#line 345
4517 p = tmp___1 & 3;
4518 }
4519#line 346
4520 if (p == 0) {
4521 {
4522#line 347
4523 pi_write_block(pi, buf, n);
4524 }
4525 } else {
4526
4527 }
4528#line 348
4529 if (p == 2) {
4530 {
4531#line 349
4532 pi_read_block(pi, buf, n);
4533 }
4534 } else {
4535
4536 }
4537 } else {
4538
4539 }
4540 }
4541 {
4542#line 352
4543 __cil_tmp19 = (char *)"data done";
4544#line 352
4545 s = pt_wait(tape, 128, 65, fun, __cil_tmp19);
4546#line 354
4547 pi_disconnect(pi);
4548 }
4549#line 356
4550 if (r != 0) {
4551#line 356
4552 tmp___3 = r;
4553 } else {
4554#line 356
4555 tmp___3 = s;
4556 }
4557#line 356
4558 return (tmp___3);
4559}
4560}
4561#line 359 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4562static void pt_req_sense(struct pt_unit *tape , int quiet )
4563{ char rs_cmd[12U] ;
4564 char buf[16U] ;
4565 int r ;
4566 unsigned long __ms ;
4567 unsigned long tmp ;
4568 char *__cil_tmp8 ;
4569 char *__cil_tmp9 ;
4570 char *__cil_tmp10 ;
4571 char *__cil_tmp11 ;
4572 char (*__cil_tmp12)[8U] ;
4573 char *__cil_tmp13 ;
4574 int __cil_tmp14 ;
4575 int __cil_tmp15 ;
4576 int __cil_tmp16 ;
4577 int __cil_tmp17 ;
4578 int __cil_tmp18 ;
4579 int __cil_tmp19 ;
4580 int __cil_tmp20 ;
4581 int __cil_tmp21 ;
4582 int __cil_tmp22 ;
4583 int __cil_tmp23 ;
4584 int __cil_tmp24 ;
4585 int __cil_tmp25 ;
4586 int __cil_tmp26 ;
4587
4588 {
4589 {
4590#line 361
4591 rs_cmd[0] = (char)3;
4592#line 361
4593 rs_cmd[1] = (char)0;
4594#line 361
4595 rs_cmd[2] = (char)0;
4596#line 361
4597 rs_cmd[3] = (char)0;
4598#line 361
4599 rs_cmd[4] = (char)16;
4600#line 361
4601 rs_cmd[5] = (char)0;
4602#line 361
4603 rs_cmd[6] = (char)0;
4604#line 361
4605 rs_cmd[7] = (char)0;
4606#line 361
4607 rs_cmd[8] = (char)0;
4608#line 361
4609 rs_cmd[9] = (char)0;
4610#line 361
4611 rs_cmd[10] = (char)0;
4612#line 361
4613 rs_cmd[11] = (char)0;
4614#line 365
4615 __cil_tmp8 = (char *)(& rs_cmd);
4616#line 365
4617 __cil_tmp9 = (char *)"Request sense";
4618#line 365
4619 r = pt_command(tape, __cil_tmp8, 16, __cil_tmp9);
4620 }
4621#line 366
4622 if (1) {
4623 {
4624#line 366
4625 __const_udelay(4295000UL);
4626 }
4627 } else {
4628#line 366
4629 __ms = 1UL;
4630#line 366
4631 goto ldv_21536;
4632 ldv_21535:
4633 {
4634#line 366
4635 __const_udelay(4295000UL);
4636 }
4637 ldv_21536:
4638#line 366
4639 tmp = __ms;
4640#line 366
4641 __ms = __ms - 1UL;
4642#line 366
4643 if (tmp != 0UL) {
4644#line 367
4645 goto ldv_21535;
4646 } else {
4647#line 369
4648 goto ldv_21537;
4649 }
4650 ldv_21537: ;
4651 }
4652#line 367
4653 if (r == 0) {
4654 {
4655#line 368
4656 __cil_tmp10 = (char *)(& buf);
4657#line 368
4658 __cil_tmp11 = (char *)"Request sense";
4659#line 368
4660 pt_completion(tape, __cil_tmp10, __cil_tmp11);
4661 }
4662 } else {
4663
4664 }
4665#line 370
4666 tape->last_sense = -1;
4667#line 371
4668 if (r == 0) {
4669#line 372
4670 if (quiet == 0) {
4671 {
4672#line 373
4673 __cil_tmp12 = & tape->name;
4674#line 373
4675 __cil_tmp13 = (char *)__cil_tmp12;
4676#line 373
4677 __cil_tmp14 = (int )buf[2];
4678#line 373
4679 __cil_tmp15 = __cil_tmp14 & 15;
4680#line 373
4681 __cil_tmp16 = (int )buf[12];
4682#line 373
4683 __cil_tmp17 = (int )buf[13];
4684#line 373
4685 printk("%s: Sense key: %x, ASC: %x, ASQ: %x\n", __cil_tmp13, __cil_tmp15, __cil_tmp16,
4686 __cil_tmp17);
4687 }
4688 } else {
4689
4690 }
4691#line 375
4692 __cil_tmp18 = (int )buf[13];
4693#line 375
4694 __cil_tmp19 = __cil_tmp18 & 255;
4695#line 375
4696 __cil_tmp20 = __cil_tmp19 << 16;
4697#line 375
4698 __cil_tmp21 = (int )buf[12];
4699#line 375
4700 __cil_tmp22 = __cil_tmp21 << 8;
4701#line 375
4702 __cil_tmp23 = __cil_tmp22 & 65535;
4703#line 375
4704 __cil_tmp24 = (int )buf[2];
4705#line 375
4706 __cil_tmp25 = __cil_tmp24 & 15;
4707#line 375
4708 __cil_tmp26 = __cil_tmp25 | __cil_tmp23;
4709#line 375
4710 tape->last_sense = __cil_tmp26 | __cil_tmp20;
4711 } else {
4712
4713 }
4714#line 378
4715 return;
4716}
4717}
4718#line 380 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4719static int pt_atapi(struct pt_unit *tape , char *cmd , int dlen , char *buf , char *fun )
4720{ int r ;
4721 unsigned long __ms ;
4722 unsigned long tmp ;
4723 char *__cil_tmp9 ;
4724 unsigned long __cil_tmp10 ;
4725 unsigned long __cil_tmp11 ;
4726 int __cil_tmp12 ;
4727
4728 {
4729 {
4730#line 384
4731 r = pt_command(tape, cmd, dlen, fun);
4732 }
4733#line 385
4734 if (1) {
4735 {
4736#line 385
4737 __const_udelay(4295000UL);
4738 }
4739 } else {
4740#line 385
4741 __ms = 1UL;
4742#line 385
4743 goto ldv_21548;
4744 ldv_21547:
4745 {
4746#line 385
4747 __const_udelay(4295000UL);
4748 }
4749 ldv_21548:
4750#line 385
4751 tmp = __ms;
4752#line 385
4753 __ms = __ms - 1UL;
4754#line 385
4755 if (tmp != 0UL) {
4756#line 386
4757 goto ldv_21547;
4758 } else {
4759#line 388
4760 goto ldv_21549;
4761 }
4762 ldv_21549: ;
4763 }
4764#line 386
4765 if (r == 0) {
4766 {
4767#line 387
4768 r = pt_completion(tape, buf, fun);
4769 }
4770 } else {
4771
4772 }
4773#line 388
4774 if (r != 0) {
4775 {
4776#line 389
4777 __cil_tmp9 = (char *)0;
4778#line 389
4779 __cil_tmp10 = (unsigned long )__cil_tmp9;
4780#line 389
4781 __cil_tmp11 = (unsigned long )fun;
4782#line 389
4783 __cil_tmp12 = __cil_tmp11 == __cil_tmp10;
4784#line 389
4785 pt_req_sense(tape, __cil_tmp12);
4786 }
4787 } else {
4788
4789 }
4790#line 391
4791 return (r);
4792}
4793}
4794#line 394 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4795static void pt_sleep(int cs )
4796{ long __cil_tmp2 ;
4797
4798 {
4799 {
4800#line 396
4801 __cil_tmp2 = (long )cs;
4802#line 396
4803 schedule_timeout_interruptible(__cil_tmp2);
4804 }
4805#line 397
4806 return;
4807}
4808}
4809#line 399 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4810static int pt_poll_dsc(struct pt_unit *tape , int pause , int tmo , char *msg )
4811{ struct pi_adapter *pi ;
4812 int k ;
4813 int e ;
4814 int s ;
4815 u8 tmp ;
4816 int __cil_tmp10 ;
4817 int __cil_tmp11 ;
4818 char (*__cil_tmp12)[8U] ;
4819 char *__cil_tmp13 ;
4820 char (*__cil_tmp14)[8U] ;
4821 char *__cil_tmp15 ;
4822
4823 {
4824#line 401
4825 pi = tape->pi;
4826#line 404
4827 k = 0;
4828#line 405
4829 e = 0;
4830#line 406
4831 s = 0;
4832#line 407
4833 goto ldv_21565;
4834 ldv_21564:
4835 {
4836#line 408
4837 pt_sleep(pause);
4838#line 409
4839 k = k + 1;
4840#line 410
4841 pi_connect(pi);
4842#line 411
4843 tmp = DRIVE(tape);
4844#line 411
4845 __cil_tmp10 = (int )tmp;
4846#line 411
4847 write_reg(pi, 6, __cil_tmp10);
4848#line 412
4849 s = read_reg(pi, 7);
4850#line 413
4851 e = read_reg(pi, 1);
4852#line 414
4853 pi_disconnect(pi);
4854 }
4855 {
4856#line 415
4857 __cil_tmp11 = s & 17;
4858#line 415
4859 if (__cil_tmp11 != 0) {
4860#line 416
4861 goto ldv_21563;
4862 } else {
4863
4864 }
4865 }
4866 ldv_21565: ;
4867#line 407
4868 if (k < tmo) {
4869#line 408
4870 goto ldv_21564;
4871 } else {
4872#line 410
4873 goto ldv_21563;
4874 }
4875 ldv_21563: ;
4876#line 418
4877 if (k >= tmo) {
4878#line 418
4879 goto _L;
4880 } else
4881#line 418
4882 if (s & 1) {
4883 _L:
4884#line 419
4885 if (k >= tmo) {
4886 {
4887#line 420
4888 __cil_tmp12 = & tape->name;
4889#line 420
4890 __cil_tmp13 = (char *)__cil_tmp12;
4891#line 420
4892 printk("%s: %s DSC timeout\n", __cil_tmp13, msg);
4893 }
4894 } else {
4895 {
4896#line 422
4897 __cil_tmp14 = & tape->name;
4898#line 422
4899 __cil_tmp15 = (char *)__cil_tmp14;
4900#line 422
4901 printk("%s: %s stat=0x%x err=0x%x\n", __cil_tmp15, msg, s, e);
4902 }
4903 }
4904 {
4905#line 424
4906 pt_req_sense(tape, 0);
4907 }
4908#line 425
4909 return (0);
4910 } else {
4911
4912 }
4913#line 427
4914 return (1);
4915}
4916}
4917#line 430 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4918static void pt_media_access_cmd(struct pt_unit *tape , int tmo , char *cmd , char *fun )
4919{ int tmp ;
4920 struct pi_adapter *__cil_tmp6 ;
4921
4922 {
4923 {
4924#line 432
4925 tmp = pt_command(tape, cmd, 0, fun);
4926 }
4927#line 432
4928 if (tmp != 0) {
4929 {
4930#line 433
4931 pt_req_sense(tape, 0);
4932 }
4933#line 434
4934 return;
4935 } else {
4936
4937 }
4938 {
4939#line 436
4940 __cil_tmp6 = tape->pi;
4941#line 436
4942 pi_disconnect(__cil_tmp6);
4943#line 437
4944 pt_poll_dsc(tape, 250, tmo, fun);
4945 }
4946#line 438
4947 return;
4948}
4949}
4950#line 440 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4951static void pt_rewind(struct pt_unit *tape )
4952{ char rw_cmd[12U] ;
4953 char *__cil_tmp3 ;
4954 char *__cil_tmp4 ;
4955
4956 {
4957 {
4958#line 442
4959 rw_cmd[0] = (char)1;
4960#line 442
4961 rw_cmd[1] = (char)0;
4962#line 442
4963 rw_cmd[2] = (char)0;
4964#line 442
4965 rw_cmd[3] = (char)0;
4966#line 442
4967 rw_cmd[4] = (char)0;
4968#line 442
4969 rw_cmd[5] = (char)0;
4970#line 442
4971 rw_cmd[6] = (char)0;
4972#line 442
4973 rw_cmd[7] = (char)0;
4974#line 442
4975 rw_cmd[8] = (char)0;
4976#line 442
4977 rw_cmd[9] = (char)0;
4978#line 442
4979 rw_cmd[10] = (char)0;
4980#line 442
4981 rw_cmd[11] = (char)0;
4982#line 444
4983 __cil_tmp3 = (char *)(& rw_cmd);
4984#line 444
4985 __cil_tmp4 = (char *)"rewind";
4986#line 444
4987 pt_media_access_cmd(tape, 1200, __cil_tmp3, __cil_tmp4);
4988 }
4989#line 445
4990 return;
4991}
4992}
4993#line 447 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
4994static void pt_write_fm(struct pt_unit *tape )
4995{ char wm_cmd[12U] ;
4996 char *__cil_tmp3 ;
4997 char *__cil_tmp4 ;
4998
4999 {
5000 {
5001#line 449
5002 wm_cmd[0] = (char)16;
5003#line 449
5004 wm_cmd[1] = (char)0;
5005#line 449
5006 wm_cmd[2] = (char)0;
5007#line 449
5008 wm_cmd[3] = (char)0;
5009#line 449
5010 wm_cmd[4] = (char)1;
5011#line 449
5012 wm_cmd[5] = (char)0;
5013#line 449
5014 wm_cmd[6] = (char)0;
5015#line 449
5016 wm_cmd[7] = (char)0;
5017#line 449
5018 wm_cmd[8] = (char)0;
5019#line 449
5020 wm_cmd[9] = (char)0;
5021#line 449
5022 wm_cmd[10] = (char)0;
5023#line 449
5024 wm_cmd[11] = (char)0;
5025#line 451
5026 __cil_tmp3 = (char *)(& wm_cmd);
5027#line 451
5028 __cil_tmp4 = (char *)"write filemark";
5029#line 451
5030 pt_media_access_cmd(tape, 3000, __cil_tmp3, __cil_tmp4);
5031 }
5032#line 452
5033 return;
5034}
5035}
5036#line 456 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
5037static int pt_reset(struct pt_unit *tape )
5038{ struct pi_adapter *pi ;
5039 int i ;
5040 int k ;
5041 int flg ;
5042 int expect[5U] ;
5043 u8 tmp ;
5044 int tmp___0 ;
5045 int tmp___1 ;
5046 int tmp___2 ;
5047 int tmp___3 ;
5048 int __cil_tmp12 ;
5049 int __cil_tmp13 ;
5050 int __cil_tmp14 ;
5051 int __cil_tmp15 ;
5052 char (*__cil_tmp16)[8U] ;
5053 char *__cil_tmp17 ;
5054 int __cil_tmp18 ;
5055
5056 {
5057 {
5058#line 458
5059 pi = tape->pi;
5060#line 460
5061 expect[0] = 1;
5062#line 460
5063 expect[1] = 1;
5064#line 460
5065 expect[2] = 1;
5066#line 460
5067 expect[3] = 20;
5068#line 460
5069 expect[4] = 235;
5070#line 462
5071 pi_connect(pi);
5072#line 463
5073 tmp = DRIVE(tape);
5074#line 463
5075 __cil_tmp12 = (int )tmp;
5076#line 463
5077 write_reg(pi, 6, __cil_tmp12);
5078#line 464
5079 write_reg(pi, 7, 8);
5080#line 466
5081 pt_sleep(5);
5082#line 468
5083 k = 0;
5084 }
5085#line 469
5086 goto ldv_21589;
5087 ldv_21588:
5088 {
5089#line 470
5090 pt_sleep(25);
5091 }
5092 ldv_21589:
5093#line 469
5094 tmp___0 = k;
5095#line 469
5096 k = k + 1;
5097#line 469
5098 if (tmp___0 <= 29) {
5099 {
5100#line 469
5101 tmp___1 = status_reg(pi);
5102 }
5103 {
5104#line 469
5105 __cil_tmp13 = tmp___1 & 128;
5106#line 469
5107 if (__cil_tmp13 != 0) {
5108#line 470
5109 goto ldv_21588;
5110 } else {
5111#line 472
5112 goto ldv_21590;
5113 }
5114 }
5115 } else {
5116#line 472
5117 goto ldv_21590;
5118 }
5119 ldv_21590:
5120#line 472
5121 flg = 1;
5122#line 473
5123 i = 0;
5124#line 473
5125 goto ldv_21592;
5126 ldv_21591:
5127 {
5128#line 474
5129 __cil_tmp14 = i + 1;
5130#line 474
5131 tmp___2 = read_reg(pi, __cil_tmp14);
5132#line 474
5133 __cil_tmp15 = tmp___2 == expect[i];
5134#line 474
5135 flg = __cil_tmp15 & flg;
5136#line 473
5137 i = i + 1;
5138 }
5139 ldv_21592: ;
5140#line 473
5141 if (i <= 4) {
5142#line 474
5143 goto ldv_21591;
5144 } else {
5145#line 476
5146 goto ldv_21593;
5147 }
5148 ldv_21593: ;
5149#line 476
5150 if (verbose != 0) {
5151 {
5152#line 477
5153 __cil_tmp16 = & tape->name;
5154#line 477
5155 __cil_tmp17 = (char *)__cil_tmp16;
5156#line 477
5157 printk("%s: Reset (%d) signature = ", __cil_tmp17, k);
5158#line 478
5159 i = 0;
5160 }
5161#line 478
5162 goto ldv_21595;
5163 ldv_21594:
5164 {
5165#line 479
5166 __cil_tmp18 = i + 1;
5167#line 479
5168 tmp___3 = read_reg(pi, __cil_tmp18);
5169#line 479
5170 printk("%3x", tmp___3);
5171#line 478
5172 i = i + 1;
5173 }
5174 ldv_21595: ;
5175#line 478
5176 if (i <= 4) {
5177#line 479
5178 goto ldv_21594;
5179 } else {
5180#line 481
5181 goto ldv_21596;
5182 }
5183 ldv_21596: ;
5184#line 480
5185 if (flg == 0) {
5186 {
5187#line 481
5188 printk(" (incorrect)");
5189 }
5190 } else {
5191
5192 }
5193 {
5194#line 482
5195 printk("\n");
5196 }
5197 } else {
5198
5199 }
5200 {
5201#line 485
5202 pi_disconnect(pi);
5203 }
5204#line 486
5205 return (flg + -1);
5206}
5207}
5208#line 489 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
5209static int pt_ready_wait(struct pt_unit *tape , int tmo )
5210{ char tr_cmd[12U] ;
5211 int k ;
5212 int p ;
5213 char *tmp ;
5214 char *__cil_tmp7 ;
5215 char *__cil_tmp8 ;
5216 int __cil_tmp9 ;
5217 int __cil_tmp10 ;
5218
5219 {
5220#line 491
5221 tr_cmd[0] = (char)0;
5222#line 491
5223 tr_cmd[1] = (char)0;
5224#line 491
5225 tr_cmd[2] = (char)0;
5226#line 491
5227 tr_cmd[3] = (char)0;
5228#line 491
5229 tr_cmd[4] = (char)0;
5230#line 491
5231 tr_cmd[5] = (char)0;
5232#line 491
5233 tr_cmd[6] = (char)0;
5234#line 491
5235 tr_cmd[7] = (char)0;
5236#line 491
5237 tr_cmd[8] = (char)0;
5238#line 491
5239 tr_cmd[9] = (char)0;
5240#line 491
5241 tr_cmd[10] = (char)0;
5242#line 491
5243 tr_cmd[11] = (char)0;
5244#line 494
5245 k = 0;
5246#line 495
5247 goto ldv_21605;
5248 ldv_21604:
5249#line 496
5250 tape->last_sense = 0;
5251#line 497
5252 if (verbose > 1) {
5253#line 497
5254 tmp = (char *)"test unit ready";
5255 } else {
5256#line 497
5257 tmp = (char *)0;
5258 }
5259 {
5260#line 497
5261 __cil_tmp7 = (char *)(& tr_cmd);
5262#line 497
5263 __cil_tmp8 = (char *)0;
5264#line 497
5265 pt_atapi(tape, __cil_tmp7, 0, __cil_tmp8, tmp);
5266#line 498
5267 p = tape->last_sense;
5268 }
5269#line 499
5270 if (p == 0) {
5271#line 500
5272 return (0);
5273 } else {
5274
5275 }
5276 {
5277#line 501
5278 __cil_tmp9 = p & 65535;
5279#line 501
5280 if (__cil_tmp9 != 1026) {
5281 {
5282#line 501
5283 __cil_tmp10 = p & 255;
5284#line 501
5285 if (__cil_tmp10 != 6) {
5286#line 502
5287 return (p);
5288 } else {
5289
5290 }
5291 }
5292 } else {
5293
5294 }
5295 }
5296 {
5297#line 503
5298 k = k + 1;
5299#line 504
5300 pt_sleep(250);
5301 }
5302 ldv_21605: ;
5303#line 495
5304 if (k < tmo) {
5305#line 496
5306 goto ldv_21604;
5307 } else {
5308#line 498
5309 goto ldv_21606;
5310 }
5311 ldv_21606: ;
5312#line 506
5313 return (32);
5314}
5315}
5316#line 509 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
5317static void xs(char *buf , char *targ , int offs , int len )
5318{ int j ;
5319 int k ;
5320 int l ;
5321 int tmp ;
5322 char tmp___0 ;
5323 int __cil_tmp10 ;
5324 unsigned long __cil_tmp11 ;
5325 char *__cil_tmp12 ;
5326 char __cil_tmp13 ;
5327 signed char __cil_tmp14 ;
5328 int __cil_tmp15 ;
5329 int __cil_tmp16 ;
5330 unsigned long __cil_tmp17 ;
5331 char *__cil_tmp18 ;
5332 unsigned long __cil_tmp19 ;
5333 char *__cil_tmp20 ;
5334 int __cil_tmp21 ;
5335 unsigned long __cil_tmp22 ;
5336 char *__cil_tmp23 ;
5337 char __cil_tmp24 ;
5338 int __cil_tmp25 ;
5339 int __cil_tmp26 ;
5340 unsigned long __cil_tmp27 ;
5341 char *__cil_tmp28 ;
5342 unsigned long __cil_tmp29 ;
5343 char *__cil_tmp30 ;
5344 unsigned long __cil_tmp31 ;
5345 char *__cil_tmp32 ;
5346
5347 {
5348#line 513
5349 j = 0;
5350#line 514
5351 l = 0;
5352#line 515
5353 k = 0;
5354#line 515
5355 goto ldv_21617;
5356 ldv_21616: ;
5357 {
5358#line 516
5359 __cil_tmp10 = k + offs;
5360#line 516
5361 __cil_tmp11 = (unsigned long )__cil_tmp10;
5362#line 516
5363 __cil_tmp12 = buf + __cil_tmp11;
5364#line 516
5365 __cil_tmp13 = *__cil_tmp12;
5366#line 516
5367 __cil_tmp14 = (signed char )__cil_tmp13;
5368#line 516
5369 __cil_tmp15 = (int )__cil_tmp14;
5370#line 516
5371 if (__cil_tmp15 != 32) {
5372#line 517
5373 tmp = j;
5374#line 517
5375 j = j + 1;
5376#line 517
5377 __cil_tmp16 = k + offs;
5378#line 517
5379 __cil_tmp17 = (unsigned long )__cil_tmp16;
5380#line 517
5381 __cil_tmp18 = buf + __cil_tmp17;
5382#line 517
5383 tmp___0 = *__cil_tmp18;
5384#line 517
5385 __cil_tmp19 = (unsigned long )tmp;
5386#line 517
5387 __cil_tmp20 = targ + __cil_tmp19;
5388#line 517
5389 *__cil_tmp20 = tmp___0;
5390#line 517
5391 l = (int )tmp___0;
5392 } else {
5393 {
5394#line 516
5395 __cil_tmp21 = k + offs;
5396#line 516
5397 __cil_tmp22 = (unsigned long )__cil_tmp21;
5398#line 516
5399 __cil_tmp23 = buf + __cil_tmp22;
5400#line 516
5401 __cil_tmp24 = *__cil_tmp23;
5402#line 516
5403 __cil_tmp25 = (int )__cil_tmp24;
5404#line 516
5405 if (__cil_tmp25 != l) {
5406#line 517
5407 tmp = j;
5408#line 517
5409 j = j + 1;
5410#line 517
5411 __cil_tmp26 = k + offs;
5412#line 517
5413 __cil_tmp27 = (unsigned long )__cil_tmp26;
5414#line 517
5415 __cil_tmp28 = buf + __cil_tmp27;
5416#line 517
5417 tmp___0 = *__cil_tmp28;
5418#line 517
5419 __cil_tmp29 = (unsigned long )tmp;
5420#line 517
5421 __cil_tmp30 = targ + __cil_tmp29;
5422#line 517
5423 *__cil_tmp30 = tmp___0;
5424#line 517
5425 l = (int )tmp___0;
5426 } else {
5427
5428 }
5429 }
5430 }
5431 }
5432#line 515
5433 k = k + 1;
5434 ldv_21617: ;
5435#line 515
5436 if (k < len) {
5437#line 516
5438 goto ldv_21616;
5439 } else {
5440#line 518
5441 goto ldv_21618;
5442 }
5443 ldv_21618: ;
5444#line 518
5445 if (l == 32) {
5446#line 519
5447 j = j - 1;
5448 } else {
5449
5450 }
5451#line 520
5452 __cil_tmp31 = (unsigned long )j;
5453#line 520
5454 __cil_tmp32 = targ + __cil_tmp31;
5455#line 520
5456 *__cil_tmp32 = (char)0;
5457#line 521
5458 return;
5459}
5460}
5461#line 523 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
5462static int xn(char *buf , int offs , int size )
5463{ int v ;
5464 int k ;
5465 int __cil_tmp6 ;
5466 unsigned long __cil_tmp7 ;
5467 char *__cil_tmp8 ;
5468 char __cil_tmp9 ;
5469 int __cil_tmp10 ;
5470 int __cil_tmp11 ;
5471 int __cil_tmp12 ;
5472
5473 {
5474#line 527
5475 v = 0;
5476#line 528
5477 k = 0;
5478#line 528
5479 goto ldv_21627;
5480 ldv_21626:
5481#line 529
5482 __cil_tmp6 = k + offs;
5483#line 529
5484 __cil_tmp7 = (unsigned long )__cil_tmp6;
5485#line 529
5486 __cil_tmp8 = buf + __cil_tmp7;
5487#line 529
5488 __cil_tmp9 = *__cil_tmp8;
5489#line 529
5490 __cil_tmp10 = (int )__cil_tmp9;
5491#line 529
5492 __cil_tmp11 = __cil_tmp10 & 255;
5493#line 529
5494 __cil_tmp12 = v * 256;
5495#line 529
5496 v = __cil_tmp12 + __cil_tmp11;
5497#line 528
5498 k = k + 1;
5499 ldv_21627: ;
5500#line 528
5501 if (k < size) {
5502#line 529
5503 goto ldv_21626;
5504 } else {
5505#line 531
5506 goto ldv_21628;
5507 }
5508 ldv_21628: ;
5509#line 530
5510 return (v);
5511}
5512}
5513#line 533 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
5514static int pt_identify(struct pt_unit *tape )
5515{ int dt ;
5516 int s ;
5517 char *ms[2U] ;
5518 char mf[10U] ;
5519 char id[18U] ;
5520 char id_cmd[12U] ;
5521 char ms_cmd[12U] ;
5522 char ls_cmd[12U] ;
5523 char buf[36U] ;
5524 int tmp ;
5525 int tmp___0 ;
5526 int tmp___1 ;
5527 char *__cil_tmp14 ;
5528 char *__cil_tmp15 ;
5529 char *__cil_tmp16 ;
5530 int __cil_tmp17 ;
5531 char (*__cil_tmp18)[8U] ;
5532 char *__cil_tmp19 ;
5533 int __cil_tmp20 ;
5534 char *__cil_tmp21 ;
5535 char *__cil_tmp22 ;
5536 char *__cil_tmp23 ;
5537 char *__cil_tmp24 ;
5538 int __cil_tmp25 ;
5539 char *__cil_tmp26 ;
5540 char *__cil_tmp27 ;
5541 char *__cil_tmp28 ;
5542 int __cil_tmp29 ;
5543 int __cil_tmp30 ;
5544 char *__cil_tmp31 ;
5545 char *__cil_tmp32 ;
5546 char *__cil_tmp33 ;
5547 char *__cil_tmp34 ;
5548 char *__cil_tmp35 ;
5549 char (*__cil_tmp36)[8U] ;
5550 char *__cil_tmp37 ;
5551 char *__cil_tmp38 ;
5552 char *__cil_tmp39 ;
5553 int __cil_tmp40 ;
5554 int __cil_tmp41 ;
5555 int __cil_tmp42 ;
5556 int __cil_tmp43 ;
5557 int __cil_tmp44 ;
5558 int __cil_tmp45 ;
5559 int __cil_tmp46 ;
5560
5561 {
5562 {
5563#line 536
5564 ms[0] = (char *)"master";
5565#line 536
5566 ms[1] = (char *)"slave";
5567#line 538
5568 id_cmd[0] = (char)18;
5569#line 538
5570 id_cmd[1] = (char)0;
5571#line 538
5572 id_cmd[2] = (char)0;
5573#line 538
5574 id_cmd[3] = (char)0;
5575#line 538
5576 id_cmd[4] = (char)36;
5577#line 538
5578 id_cmd[5] = (char)0;
5579#line 538
5580 id_cmd[6] = (char)0;
5581#line 538
5582 id_cmd[7] = (char)0;
5583#line 538
5584 id_cmd[8] = (char)0;
5585#line 538
5586 id_cmd[9] = (char)0;
5587#line 538
5588 id_cmd[10] = (char)0;
5589#line 538
5590 id_cmd[11] = (char)0;
5591#line 539
5592 ms_cmd[0] = (char)26;
5593#line 539
5594 ms_cmd[1] = (char)0;
5595#line 539
5596 ms_cmd[2] = (char)42;
5597#line 539
5598 ms_cmd[3] = (char)0;
5599#line 539
5600 ms_cmd[4] = (char)36;
5601#line 539
5602 ms_cmd[5] = (char)0;
5603#line 539
5604 ms_cmd[6] = (char)0;
5605#line 539
5606 ms_cmd[7] = (char)0;
5607#line 539
5608 ms_cmd[8] = (char)0;
5609#line 539
5610 ms_cmd[9] = (char)0;
5611#line 539
5612 ms_cmd[10] = (char)0;
5613#line 539
5614 ms_cmd[11] = (char)0;
5615#line 541
5616 ls_cmd[0] = (char)77;
5617#line 541
5618 ls_cmd[1] = (char)0;
5619#line 541
5620 ls_cmd[2] = (char)113;
5621#line 541
5622 ls_cmd[3] = (char)0;
5623#line 541
5624 ls_cmd[4] = (char)0;
5625#line 541
5626 ls_cmd[5] = (char)0;
5627#line 541
5628 ls_cmd[6] = (char)0;
5629#line 541
5630 ls_cmd[7] = (char)0;
5631#line 541
5632 ls_cmd[8] = (char)36;
5633#line 541
5634 ls_cmd[9] = (char)0;
5635#line 541
5636 ls_cmd[10] = (char)0;
5637#line 541
5638 ls_cmd[11] = (char)0;
5639#line 545
5640 __cil_tmp14 = (char *)(& id_cmd);
5641#line 545
5642 __cil_tmp15 = (char *)(& buf);
5643#line 545
5644 __cil_tmp16 = (char *)"identify";
5645#line 545
5646 s = pt_atapi(tape, __cil_tmp14, 36, __cil_tmp15, __cil_tmp16);
5647 }
5648#line 546
5649 if (s != 0) {
5650#line 547
5651 return (-1);
5652 } else {
5653
5654 }
5655#line 549
5656 __cil_tmp17 = (int )buf[0];
5657#line 549
5658 dt = __cil_tmp17 & 31;
5659#line 550
5660 if (dt != 1) {
5661#line 551
5662 if (verbose != 0) {
5663 {
5664#line 552
5665 __cil_tmp18 = & tape->name;
5666#line 552
5667 __cil_tmp19 = (char *)__cil_tmp18;
5668#line 552
5669 __cil_tmp20 = tape->drive;
5670#line 552
5671 printk("%s: Drive %d, unsupported type %d\n", __cil_tmp19, __cil_tmp20, dt);
5672 }
5673 } else {
5674
5675 }
5676#line 554
5677 return (-1);
5678 } else {
5679
5680 }
5681 {
5682#line 557
5683 __cil_tmp21 = (char *)(& buf);
5684#line 557
5685 __cil_tmp22 = (char *)(& mf);
5686#line 557
5687 xs(__cil_tmp21, __cil_tmp22, 8, 8);
5688#line 558
5689 __cil_tmp23 = (char *)(& buf);
5690#line 558
5691 __cil_tmp24 = (char *)(& id);
5692#line 558
5693 xs(__cil_tmp23, __cil_tmp24, 16, 16);
5694#line 560
5695 tape->flags = 0;
5696#line 561
5697 tape->capacity = 0;
5698#line 562
5699 tape->bs = 0;
5700#line 564
5701 tmp = pt_ready_wait(tape, 60);
5702 }
5703#line 564
5704 if (tmp == 0) {
5705#line 565
5706 __cil_tmp25 = tape->flags;
5707#line 565
5708 tape->flags = __cil_tmp25 | 1;
5709 } else {
5710
5711 }
5712 {
5713#line 567
5714 __cil_tmp26 = (char *)(& ms_cmd);
5715#line 567
5716 __cil_tmp27 = (char *)(& buf);
5717#line 567
5718 __cil_tmp28 = (char *)"mode sense";
5719#line 567
5720 tmp___0 = pt_atapi(tape, __cil_tmp26, 36, __cil_tmp27, __cil_tmp28);
5721 }
5722#line 567
5723 if (tmp___0 == 0) {
5724 {
5725#line 568
5726 __cil_tmp29 = (int )buf[2];
5727#line 568
5728 if (__cil_tmp29 >= 0) {
5729#line 569
5730 __cil_tmp30 = tape->flags;
5731#line 569
5732 tape->flags = __cil_tmp30 | 2;
5733 } else {
5734
5735 }
5736 }
5737 {
5738#line 570
5739 __cil_tmp31 = (char *)(& buf);
5740#line 570
5741 tape->bs = xn(__cil_tmp31, 10, 2);
5742 }
5743 } else {
5744
5745 }
5746 {
5747#line 573
5748 __cil_tmp32 = (char *)(& ls_cmd);
5749#line 573
5750 __cil_tmp33 = (char *)(& buf);
5751#line 573
5752 __cil_tmp34 = (char *)"log sense";
5753#line 573
5754 tmp___1 = pt_atapi(tape, __cil_tmp32, 36, __cil_tmp33, __cil_tmp34);
5755 }
5756#line 573
5757 if (tmp___1 == 0) {
5758 {
5759#line 574
5760 __cil_tmp35 = (char *)(& buf);
5761#line 574
5762 tape->capacity = xn(__cil_tmp35, 24, 4);
5763 }
5764 } else {
5765
5766 }
5767 {
5768#line 576
5769 __cil_tmp36 = & tape->name;
5770#line 576
5771 __cil_tmp37 = (char *)__cil_tmp36;
5772#line 576
5773 __cil_tmp38 = (char *)(& mf);
5774#line 576
5775 __cil_tmp39 = (char *)(& id);
5776#line 576
5777 printk("%s: %s %s, %s", __cil_tmp37, __cil_tmp38, __cil_tmp39, ms[tape->drive]);
5778 }
5779 {
5780#line 577
5781 __cil_tmp40 = tape->flags;
5782#line 577
5783 __cil_tmp41 = __cil_tmp40 & 1;
5784#line 577
5785 if (__cil_tmp41 == 0) {
5786 {
5787#line 578
5788 printk(", no media\n");
5789 }
5790 } else {
5791 {
5792#line 580
5793 __cil_tmp42 = tape->flags;
5794#line 580
5795 __cil_tmp43 = __cil_tmp42 & 2;
5796#line 580
5797 if (__cil_tmp43 == 0) {
5798 {
5799#line 581
5800 printk(", RO");
5801 }
5802 } else {
5803
5804 }
5805 }
5806 {
5807#line 582
5808 __cil_tmp44 = tape->bs;
5809#line 582
5810 __cil_tmp45 = tape->capacity;
5811#line 582
5812 __cil_tmp46 = __cil_tmp45 / 1024;
5813#line 582
5814 printk(", blocksize %d, %d MB\n", __cil_tmp44, __cil_tmp46);
5815 }
5816 }
5817 }
5818#line 585
5819 return (0);
5820}
5821}
5822#line 593 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
5823static int pt_probe(struct pt_unit *tape )
5824{ int tmp ;
5825 int tmp___0 ;
5826 int tmp___1 ;
5827 int tmp___2 ;
5828 int __cil_tmp6 ;
5829 int __cil_tmp7 ;
5830 int __cil_tmp8 ;
5831
5832 {
5833 {
5834#line 595
5835 __cil_tmp6 = tape->drive;
5836#line 595
5837 if (__cil_tmp6 == -1) {
5838#line 596
5839 tape->drive = 0;
5840#line 596
5841 goto ldv_21645;
5842 ldv_21644:
5843 {
5844#line 597
5845 tmp___0 = pt_reset(tape);
5846 }
5847#line 597
5848 if (tmp___0 == 0) {
5849 {
5850#line 598
5851 tmp = pt_identify(tape);
5852 }
5853#line 598
5854 return (tmp);
5855 } else {
5856
5857 }
5858#line 596
5859 __cil_tmp7 = tape->drive;
5860#line 596
5861 tape->drive = __cil_tmp7 + 1;
5862 ldv_21645: ;
5863 {
5864#line 596
5865 __cil_tmp8 = tape->drive;
5866#line 596
5867 if (__cil_tmp8 <= 1) {
5868#line 597
5869 goto ldv_21644;
5870 } else {
5871#line 599
5872 goto ldv_21646;
5873 }
5874 }
5875 ldv_21646: ;
5876 } else {
5877 {
5878#line 600
5879 tmp___2 = pt_reset(tape);
5880 }
5881#line 600
5882 if (tmp___2 == 0) {
5883 {
5884#line 601
5885 tmp___1 = pt_identify(tape);
5886 }
5887#line 601
5888 return (tmp___1);
5889 } else {
5890
5891 }
5892 }
5893 }
5894#line 603
5895 return (-1);
5896}
5897}
5898#line 606 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
5899static int pt_detect(void)
5900{ struct pt_unit *tape ;
5901 int specified ;
5902 int found ;
5903 int unit ;
5904 struct pt_unit *tape___0 ;
5905 int tmp ;
5906 int tmp___0 ;
5907 int tmp___1 ;
5908 int tmp___2 ;
5909 char *__cil_tmp10 ;
5910 unsigned long __cil_tmp11 ;
5911 struct pt_unit *__cil_tmp12 ;
5912 atomic_t *__cil_tmp13 ;
5913 char (*__cil_tmp14)[8U] ;
5914 char *__cil_tmp15 ;
5915 int __cil_tmp16 ;
5916 struct pi_adapter *__cil_tmp17 ;
5917 int __cil_tmp18 ;
5918 int __cil_tmp19 ;
5919 int __cil_tmp20 ;
5920 int __cil_tmp21 ;
5921 int __cil_tmp22 ;
5922 char *__cil_tmp23 ;
5923 char (*__cil_tmp24)[8U] ;
5924 char *__cil_tmp25 ;
5925 struct pi_adapter *__cil_tmp26 ;
5926 struct pi_adapter *__cil_tmp27 ;
5927 char *__cil_tmp28 ;
5928 char (*__cil_tmp29)[8U] ;
5929 char *__cil_tmp30 ;
5930 struct pi_adapter *__cil_tmp31 ;
5931
5932 {
5933 {
5934#line 609
5935 specified = 0;
5936#line 609
5937 found = 0;
5938#line 612
5939 __cil_tmp10 = (char *)"1.04";
5940#line 612
5941 printk("%s: %s version %s, major %d\n", name, name, __cil_tmp10, major);
5942#line 614
5943 specified = 0;
5944#line 615
5945 unit = 0;
5946 }
5947#line 615
5948 goto ldv_21657;
5949 ldv_21656:
5950 {
5951#line 616
5952 __cil_tmp11 = (unsigned long )unit;
5953#line 616
5954 __cil_tmp12 = (struct pt_unit *)(& pt);
5955#line 616
5956 tape___0 = __cil_tmp12 + __cil_tmp11;
5957#line 617
5958 tape___0->pi = & tape___0->pia;
5959#line 618
5960 __cil_tmp13 = & tape___0->available;
5961#line 618
5962 atomic_set(__cil_tmp13, 1);
5963#line 619
5964 tape___0->flags = 0;
5965#line 620
5966 tape___0->last_sense = 0;
5967#line 621
5968 tape___0->present = 0;
5969#line 622
5970 tape___0->bufptr = (char *)0;
5971#line 623
5972 tape___0->drive = (*(drives[unit]))[4];
5973#line 624
5974 __cil_tmp14 = & tape___0->name;
5975#line 624
5976 __cil_tmp15 = (char *)__cil_tmp14;
5977#line 624
5978 snprintf(__cil_tmp15, 8UL, "%s%d", name, unit);
5979 }
5980 {
5981#line 625
5982 __cil_tmp16 = (*(drives[unit]))[0];
5983#line 625
5984 if (__cil_tmp16 == 0) {
5985#line 626
5986 goto ldv_21655;
5987 } else {
5988
5989 }
5990 }
5991 {
5992#line 627
5993 specified = specified + 1;
5994#line 628
5995 __cil_tmp17 = tape___0->pi;
5996#line 628
5997 __cil_tmp18 = (*(drives[unit]))[0];
5998#line 628
5999 __cil_tmp19 = (*(drives[unit]))[3];
6000#line 628
6001 __cil_tmp20 = (*(drives[unit]))[2];
6002#line 628
6003 __cil_tmp21 = (*(drives[unit]))[1];
6004#line 628
6005 __cil_tmp22 = (*(drives[unit]))[5];
6006#line 628
6007 __cil_tmp23 = (char *)(& pt_scratch);
6008#line 628
6009 __cil_tmp24 = & tape___0->name;
6010#line 628
6011 __cil_tmp25 = (char *)__cil_tmp24;
6012#line 628
6013 tmp___0 = pi_init(__cil_tmp17, 0, __cil_tmp18, __cil_tmp19, __cil_tmp20, __cil_tmp21,
6014 __cil_tmp22, __cil_tmp23, 3, verbose, __cil_tmp25);
6015 }
6016#line 628
6017 if (tmp___0 != 0) {
6018 {
6019#line 631
6020 tmp = pt_probe(tape___0);
6021 }
6022#line 631
6023 if (tmp == 0) {
6024#line 632
6025 tape___0->present = 1;
6026#line 633
6027 found = found + 1;
6028 } else {
6029 {
6030#line 635
6031 __cil_tmp26 = tape___0->pi;
6032#line 635
6033 pi_release(__cil_tmp26);
6034 }
6035 }
6036 } else {
6037
6038 }
6039 ldv_21655:
6040#line 615
6041 unit = unit + 1;
6042 ldv_21657: ;
6043#line 615
6044 if (unit <= 3) {
6045#line 616
6046 goto ldv_21656;
6047 } else {
6048#line 618
6049 goto ldv_21658;
6050 }
6051 ldv_21658: ;
6052#line 638
6053 if (specified == 0) {
6054 {
6055#line 639
6056 tape = (struct pt_unit *)(& pt);
6057#line 640
6058 __cil_tmp27 = tape->pi;
6059#line 640
6060 __cil_tmp28 = (char *)(& pt_scratch);
6061#line 640
6062 __cil_tmp29 = & tape->name;
6063#line 640
6064 __cil_tmp30 = (char *)__cil_tmp29;
6065#line 640
6066 tmp___2 = pi_init(__cil_tmp27, 1, -1, -1, -1, -1, -1, __cil_tmp28, 3, verbose,
6067 __cil_tmp30);
6068 }
6069#line 640
6070 if (tmp___2 != 0) {
6071 {
6072#line 642
6073 tmp___1 = pt_probe(tape);
6074 }
6075#line 642
6076 if (tmp___1 == 0) {
6077#line 643
6078 tape->present = 1;
6079#line 644
6080 found = found + 1;
6081 } else {
6082 {
6083#line 646
6084 __cil_tmp31 = tape->pi;
6085#line 646
6086 pi_release(__cil_tmp31);
6087 }
6088 }
6089 } else {
6090
6091 }
6092 } else {
6093
6094 }
6095#line 650
6096 if (found != 0) {
6097#line 651
6098 return (0);
6099 } else {
6100
6101 }
6102 {
6103#line 653
6104 printk("%s: No ATAPI tape drive detected\n", name);
6105 }
6106#line 654
6107 return (-1);
6108}
6109}
6110#line 657 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
6111static int pt_open(struct inode *inode , struct file *file )
6112{ int unit ;
6113 unsigned int tmp ;
6114 struct pt_unit *tape ;
6115 int err ;
6116 int tmp___0 ;
6117 unsigned int tmp___1 ;
6118 void *tmp___2 ;
6119 struct inode const *__cil_tmp10 ;
6120 int __cil_tmp11 ;
6121 unsigned long __cil_tmp12 ;
6122 struct pt_unit *__cil_tmp13 ;
6123 int __cil_tmp14 ;
6124 atomic_t *__cil_tmp15 ;
6125 int __cil_tmp16 ;
6126 int __cil_tmp17 ;
6127 int __cil_tmp18 ;
6128 int __cil_tmp19 ;
6129 fmode_t __cil_tmp20 ;
6130 unsigned int __cil_tmp21 ;
6131 struct inode const *__cil_tmp22 ;
6132 unsigned int __cil_tmp23 ;
6133 int __cil_tmp24 ;
6134 char *__cil_tmp25 ;
6135 unsigned long __cil_tmp26 ;
6136 char *__cil_tmp27 ;
6137 unsigned long __cil_tmp28 ;
6138 char (*__cil_tmp29)[8U] ;
6139 char *__cil_tmp30 ;
6140 atomic_t *__cil_tmp31 ;
6141
6142 {
6143 {
6144#line 659
6145 __cil_tmp10 = (struct inode const *)inode;
6146#line 659
6147 tmp = iminor(__cil_tmp10);
6148#line 659
6149 __cil_tmp11 = (int )tmp;
6150#line 659
6151 unit = __cil_tmp11 & 127;
6152#line 660
6153 __cil_tmp12 = (unsigned long )unit;
6154#line 660
6155 __cil_tmp13 = (struct pt_unit *)(& pt);
6156#line 660
6157 tape = __cil_tmp13 + __cil_tmp12;
6158#line 663
6159 mutex_lock_nested(& pt_mutex, 0U);
6160 }
6161#line 664
6162 if (unit > 3) {
6163 {
6164#line 665
6165 mutex_unlock(& pt_mutex);
6166 }
6167#line 666
6168 return (-19);
6169 } else {
6170 {
6171#line 664
6172 __cil_tmp14 = tape->present;
6173#line 664
6174 if (__cil_tmp14 == 0) {
6175 {
6176#line 665
6177 mutex_unlock(& pt_mutex);
6178 }
6179#line 666
6180 return (-19);
6181 } else {
6182
6183 }
6184 }
6185 }
6186 {
6187#line 669
6188 err = -16;
6189#line 670
6190 __cil_tmp15 = & tape->available;
6191#line 670
6192 tmp___0 = atomic_dec_and_test(__cil_tmp15);
6193 }
6194#line 670
6195 if (tmp___0 == 0) {
6196#line 671
6197 goto out;
6198 } else {
6199
6200 }
6201 {
6202#line 673
6203 pt_identify(tape);
6204#line 675
6205 err = -19;
6206 }
6207 {
6208#line 676
6209 __cil_tmp16 = tape->flags;
6210#line 676
6211 __cil_tmp17 = __cil_tmp16 & 1;
6212#line 676
6213 if (__cil_tmp17 == 0) {
6214#line 677
6215 goto out;
6216 } else {
6217
6218 }
6219 }
6220#line 679
6221 err = -30;
6222 {
6223#line 680
6224 __cil_tmp18 = tape->flags;
6225#line 680
6226 __cil_tmp19 = __cil_tmp18 & 2;
6227#line 680
6228 if (__cil_tmp19 == 0) {
6229 {
6230#line 680
6231 __cil_tmp20 = file->f_mode;
6232#line 680
6233 __cil_tmp21 = __cil_tmp20 & 2U;
6234#line 680
6235 if (__cil_tmp21 != 0U) {
6236#line 681
6237 goto out;
6238 } else {
6239
6240 }
6241 }
6242 } else {
6243
6244 }
6245 }
6246 {
6247#line 683
6248 __cil_tmp22 = (struct inode const *)inode;
6249#line 683
6250 tmp___1 = iminor(__cil_tmp22);
6251 }
6252 {
6253#line 683
6254 __cil_tmp23 = tmp___1 & 128U;
6255#line 683
6256 if (__cil_tmp23 == 0U) {
6257#line 684
6258 __cil_tmp24 = tape->flags;
6259#line 684
6260 tape->flags = __cil_tmp24 | 4;
6261 } else {
6262
6263 }
6264 }
6265 {
6266#line 686
6267 err = -12;
6268#line 687
6269 tmp___2 = kmalloc(16384UL, 208U);
6270#line 687
6271 tape->bufptr = (char *)tmp___2;
6272 }
6273 {
6274#line 688
6275 __cil_tmp25 = (char *)0;
6276#line 688
6277 __cil_tmp26 = (unsigned long )__cil_tmp25;
6278#line 688
6279 __cil_tmp27 = tape->bufptr;
6280#line 688
6281 __cil_tmp28 = (unsigned long )__cil_tmp27;
6282#line 688
6283 if (__cil_tmp28 == __cil_tmp26) {
6284 {
6285#line 689
6286 __cil_tmp29 = & tape->name;
6287#line 689
6288 __cil_tmp30 = (char *)__cil_tmp29;
6289#line 689
6290 printk("%s: buffer allocation failed\n", __cil_tmp30);
6291 }
6292#line 690
6293 goto out;
6294 } else {
6295
6296 }
6297 }
6298 {
6299#line 693
6300 file->private_data = (void *)tape;
6301#line 694
6302 mutex_unlock(& pt_mutex);
6303 }
6304#line 695
6305 return (0);
6306 out:
6307 {
6308#line 698
6309 __cil_tmp31 = & tape->available;
6310#line 698
6311 atomic_inc(__cil_tmp31);
6312#line 699
6313 mutex_unlock(& pt_mutex);
6314 }
6315#line 700
6316 return (err);
6317}
6318}
6319#line 703 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
6320static long pt_ioctl(struct file *file , unsigned int cmd , unsigned long arg )
6321{ struct pt_unit *tape ;
6322 struct mtop *p ;
6323 struct mtop mtop ;
6324 unsigned long tmp ;
6325 void *__cil_tmp8 ;
6326 int __cil_tmp9 ;
6327 void *__cil_tmp10 ;
6328 void const *__cil_tmp11 ;
6329 int __cil_tmp12 ;
6330 int __cil_tmp13 ;
6331 char (*__cil_tmp14)[8U] ;
6332 char *__cil_tmp15 ;
6333 int __cil_tmp16 ;
6334
6335 {
6336#line 705
6337 __cil_tmp8 = file->private_data;
6338#line 705
6339 tape = (struct pt_unit *)__cil_tmp8;
6340#line 706
6341 p = (struct mtop *)arg;
6342 {
6343#line 710
6344 __cil_tmp9 = (int )cmd;
6345#line 710
6346 if (__cil_tmp9 == 1074294017) {
6347#line 710
6348 goto case_1074294017;
6349 } else {
6350#line 735
6351 goto switch_default___0;
6352#line 709
6353 if (0) {
6354 case_1074294017:
6355 {
6356#line 711
6357 __cil_tmp10 = (void *)(& mtop);
6358#line 711
6359 __cil_tmp11 = (void const *)p;
6360#line 711
6361 tmp = copy_from_user(__cil_tmp10, __cil_tmp11, 8UL);
6362 }
6363#line 711
6364 if (tmp != 0UL) {
6365#line 712
6366 return (-14L);
6367 } else {
6368
6369 }
6370 {
6371#line 716
6372 __cil_tmp12 = (int )mtop.mt_op;
6373#line 716
6374 if (__cil_tmp12 == 6) {
6375#line 716
6376 goto case_6;
6377 } else {
6378 {
6379#line 722
6380 __cil_tmp13 = (int )mtop.mt_op;
6381#line 722
6382 if (__cil_tmp13 == 5) {
6383#line 722
6384 goto case_5;
6385 } else {
6386#line 728
6387 goto switch_default;
6388#line 714
6389 if (0) {
6390 case_6:
6391 {
6392#line 717
6393 mutex_lock_nested(& pt_mutex, 0U);
6394#line 718
6395 pt_rewind(tape);
6396#line 719
6397 mutex_unlock(& pt_mutex);
6398 }
6399#line 720
6400 return (0L);
6401 case_5:
6402 {
6403#line 723
6404 mutex_lock_nested(& pt_mutex, 0U);
6405#line 724
6406 pt_write_fm(tape);
6407#line 725
6408 mutex_unlock(& pt_mutex);
6409 }
6410#line 726
6411 return (0L);
6412 switch_default:
6413 {
6414#line 730
6415 __cil_tmp14 = & tape->name;
6416#line 730
6417 __cil_tmp15 = (char *)__cil_tmp14;
6418#line 730
6419 __cil_tmp16 = (int )mtop.mt_op;
6420#line 730
6421 printk("<7>%s: Unimplemented mt_op %d\n", __cil_tmp15, __cil_tmp16);
6422 }
6423#line 732
6424 return (-22L);
6425 } else {
6426
6427 }
6428 }
6429 }
6430 }
6431 }
6432 switch_default___0: ;
6433#line 736
6434 return (-25L);
6435 } else {
6436
6437 }
6438 }
6439 }
6440}
6441}
6442#line 741 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
6443static int pt_release(struct inode *inode , struct file *file )
6444{ struct pt_unit *tape ;
6445 int tmp ;
6446 void *__cil_tmp5 ;
6447 atomic_t *__cil_tmp6 ;
6448 atomic_t const *__cil_tmp7 ;
6449 int __cil_tmp8 ;
6450 int __cil_tmp9 ;
6451 int __cil_tmp10 ;
6452 int __cil_tmp11 ;
6453 char *__cil_tmp12 ;
6454 void const *__cil_tmp13 ;
6455 atomic_t *__cil_tmp14 ;
6456
6457 {
6458 {
6459#line 743
6460 __cil_tmp5 = file->private_data;
6461#line 743
6462 tape = (struct pt_unit *)__cil_tmp5;
6463#line 745
6464 __cil_tmp6 = & tape->available;
6465#line 745
6466 __cil_tmp7 = (atomic_t const *)__cil_tmp6;
6467#line 745
6468 tmp = atomic_read(__cil_tmp7);
6469 }
6470#line 745
6471 if (tmp > 1) {
6472#line 746
6473 return (-22);
6474 } else {
6475
6476 }
6477 {
6478#line 748
6479 __cil_tmp8 = tape->flags;
6480#line 748
6481 __cil_tmp9 = __cil_tmp8 & 8;
6482#line 748
6483 if (__cil_tmp9 != 0) {
6484 {
6485#line 749
6486 pt_write_fm(tape);
6487 }
6488 } else {
6489
6490 }
6491 }
6492 {
6493#line 751
6494 __cil_tmp10 = tape->flags;
6495#line 751
6496 __cil_tmp11 = __cil_tmp10 & 4;
6497#line 751
6498 if (__cil_tmp11 != 0) {
6499 {
6500#line 752
6501 pt_rewind(tape);
6502 }
6503 } else {
6504
6505 }
6506 }
6507 {
6508#line 754
6509 __cil_tmp12 = tape->bufptr;
6510#line 754
6511 __cil_tmp13 = (void const *)__cil_tmp12;
6512#line 754
6513 kfree(__cil_tmp13);
6514#line 755
6515 tape->bufptr = (char *)0;
6516#line 757
6517 __cil_tmp14 = & tape->available;
6518#line 757
6519 atomic_inc(__cil_tmp14);
6520 }
6521#line 759
6522 return (0);
6523}
6524}
6525#line 763 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
6526static ssize_t pt_read(struct file *filp , char *buf , size_t count , loff_t *ppos )
6527{ struct pt_unit *tape ;
6528 struct pi_adapter *pi ;
6529 char rd_cmd[12U] ;
6530 int k ;
6531 int n ;
6532 int r ;
6533 int p ;
6534 int s ;
6535 int t ;
6536 int b ;
6537 int tmp ;
6538 int tmp___0 ;
6539 unsigned long __ms ;
6540 unsigned long tmp___1 ;
6541 char *tmp___2 ;
6542 int tmp___3 ;
6543 int tmp___4 ;
6544 int tmp___5 ;
6545 int tmp___6 ;
6546 void *__cil_tmp24 ;
6547 int __cil_tmp25 ;
6548 int __cil_tmp26 ;
6549 int __cil_tmp27 ;
6550 char *__cil_tmp28 ;
6551 char *__cil_tmp29 ;
6552 char *__cil_tmp30 ;
6553 int __cil_tmp31 ;
6554 int __cil_tmp32 ;
6555 int __cil_tmp33 ;
6556 int __cil_tmp34 ;
6557 char *__cil_tmp35 ;
6558 int __cil_tmp36 ;
6559 int __cil_tmp37 ;
6560 int __cil_tmp38 ;
6561 int __cil_tmp39 ;
6562 int __cil_tmp40 ;
6563 char *__cil_tmp41 ;
6564 char *__cil_tmp42 ;
6565 char *__cil_tmp43 ;
6566 int __cil_tmp44 ;
6567 int __cil_tmp45 ;
6568 int __cil_tmp46 ;
6569 int __cil_tmp47 ;
6570 char (*__cil_tmp48)[8U] ;
6571 char *__cil_tmp49 ;
6572 char *__cil_tmp50 ;
6573 size_t __cil_tmp51 ;
6574 unsigned long __cil_tmp52 ;
6575 void *__cil_tmp53 ;
6576 void *__cil_tmp54 ;
6577 char *__cil_tmp55 ;
6578 void const *__cil_tmp56 ;
6579 unsigned int __cil_tmp57 ;
6580 size_t __cil_tmp58 ;
6581 int __cil_tmp59 ;
6582 int __cil_tmp60 ;
6583
6584 {
6585#line 765
6586 __cil_tmp24 = filp->private_data;
6587#line 765
6588 tape = (struct pt_unit *)__cil_tmp24;
6589#line 766
6590 pi = tape->pi;
6591#line 767
6592 rd_cmd[0] = (char)8;
6593#line 767
6594 rd_cmd[1] = (char)1;
6595#line 767
6596 rd_cmd[2] = (char)0;
6597#line 767
6598 rd_cmd[3] = (char)0;
6599#line 767
6600 rd_cmd[4] = (char)0;
6601#line 767
6602 rd_cmd[5] = (char)0;
6603#line 767
6604 rd_cmd[6] = (char)0;
6605#line 767
6606 rd_cmd[7] = (char)0;
6607#line 767
6608 rd_cmd[8] = (char)0;
6609#line 767
6610 rd_cmd[9] = (char)0;
6611#line 767
6612 rd_cmd[10] = (char)0;
6613#line 767
6614 rd_cmd[11] = (char)0;
6615 {
6616#line 770
6617 __cil_tmp25 = tape->flags;
6618#line 770
6619 __cil_tmp26 = __cil_tmp25 & 24;
6620#line 770
6621 if (__cil_tmp26 == 0) {
6622 {
6623#line 771
6624 __cil_tmp27 = tape->flags;
6625#line 771
6626 tape->flags = __cil_tmp27 | 16;
6627#line 772
6628 __cil_tmp28 = (char *)(& rd_cmd);
6629#line 772
6630 __cil_tmp29 = (char *)0;
6631#line 772
6632 __cil_tmp30 = (char *)"start read-ahead";
6633#line 772
6634 tmp = pt_atapi(tape, __cil_tmp28, 0, __cil_tmp29, __cil_tmp30);
6635 }
6636#line 772
6637 if (tmp != 0) {
6638#line 773
6639 return (-5L);
6640 } else {
6641
6642 }
6643 } else {
6644 {
6645#line 774
6646 __cil_tmp31 = tape->flags;
6647#line 774
6648 __cil_tmp32 = __cil_tmp31 & 8;
6649#line 774
6650 if (__cil_tmp32 != 0) {
6651#line 775
6652 return (-5L);
6653 } else {
6654
6655 }
6656 }
6657 }
6658 }
6659 {
6660#line 777
6661 __cil_tmp33 = tape->flags;
6662#line 777
6663 __cil_tmp34 = __cil_tmp33 & 32;
6664#line 777
6665 if (__cil_tmp34 != 0) {
6666#line 778
6667 return (0L);
6668 } else {
6669
6670 }
6671 }
6672#line 780
6673 t = 0;
6674#line 782
6675 goto ldv_21712;
6676 ldv_21711:
6677 {
6678#line 784
6679 __cil_tmp35 = (char *)"read";
6680#line 784
6681 tmp___0 = pt_poll_dsc(tape, 2, 3000, __cil_tmp35);
6682 }
6683#line 784
6684 if (tmp___0 == 0) {
6685#line 785
6686 return (-5L);
6687 } else {
6688
6689 }
6690#line 787
6691 n = (int )count;
6692#line 788
6693 if (n > 32768) {
6694#line 789
6695 n = 32768;
6696 } else {
6697
6698 }
6699 {
6700#line 790
6701 __cil_tmp36 = tape->bs;
6702#line 790
6703 __cil_tmp37 = tape->bs;
6704#line 790
6705 __cil_tmp38 = n + -1;
6706#line 790
6707 __cil_tmp39 = __cil_tmp38 + __cil_tmp37;
6708#line 790
6709 b = __cil_tmp39 / __cil_tmp36;
6710#line 791
6711 __cil_tmp40 = tape->bs;
6712#line 791
6713 n = __cil_tmp40 * b;
6714#line 793
6715 rd_cmd[4] = (char )b;
6716#line 795
6717 __cil_tmp41 = (char *)(& rd_cmd);
6718#line 795
6719 __cil_tmp42 = (char *)"read";
6720#line 795
6721 r = pt_command(tape, __cil_tmp41, n, __cil_tmp42);
6722 }
6723#line 797
6724 if (1) {
6725 {
6726#line 797
6727 __const_udelay(4295000UL);
6728 }
6729 } else {
6730#line 797
6731 __ms = 1UL;
6732#line 797
6733 goto ldv_21703;
6734 ldv_21702:
6735 {
6736#line 797
6737 __const_udelay(4295000UL);
6738 }
6739 ldv_21703:
6740#line 797
6741 tmp___1 = __ms;
6742#line 797
6743 __ms = __ms - 1UL;
6744#line 797
6745 if (tmp___1 != 0UL) {
6746#line 798
6747 goto ldv_21702;
6748 } else {
6749#line 800
6750 goto ldv_21704;
6751 }
6752 ldv_21704: ;
6753 }
6754#line 799
6755 if (r != 0) {
6756 {
6757#line 800
6758 pt_req_sense(tape, 0);
6759 }
6760#line 801
6761 return (-5L);
6762 } else {
6763
6764 }
6765 ldv_21709: ;
6766#line 806
6767 if (verbose > 1) {
6768#line 806
6769 tmp___2 = (char *)"read DRQ";
6770 } else {
6771#line 806
6772 tmp___2 = (char *)0;
6773 }
6774 {
6775#line 806
6776 __cil_tmp43 = (char *)"";
6777#line 806
6778 r = pt_wait(tape, 128, 73, tmp___2, __cil_tmp43);
6779 }
6780 {
6781#line 810
6782 __cil_tmp44 = r & 126976;
6783#line 810
6784 if (__cil_tmp44 != 0) {
6785 {
6786#line 811
6787 pi_disconnect(pi);
6788#line 812
6789 pt_req_sense(tape, 0);
6790 }
6791#line 813
6792 return (-5L);
6793 } else {
6794
6795 }
6796 }
6797#line 816
6798 if (r != 0) {
6799#line 817
6800 __cil_tmp45 = tape->flags;
6801#line 817
6802 tape->flags = __cil_tmp45 | 32;
6803 } else {
6804
6805 }
6806 {
6807#line 819
6808 s = read_reg(pi, 7);
6809 }
6810 {
6811#line 821
6812 __cil_tmp46 = s & 8;
6813#line 821
6814 if (__cil_tmp46 == 0) {
6815#line 822
6816 goto ldv_21705;
6817 } else {
6818
6819 }
6820 }
6821 {
6822#line 824
6823 tmp___3 = read_reg(pi, 4);
6824#line 824
6825 tmp___4 = read_reg(pi, 5);
6826#line 824
6827 __cil_tmp47 = tmp___4 * 256;
6828#line 824
6829 n = tmp___3 + __cil_tmp47;
6830#line 825
6831 tmp___5 = read_reg(pi, 2);
6832#line 825
6833 p = tmp___5 & 3;
6834 }
6835#line 826
6836 if (p != 2) {
6837 {
6838#line 827
6839 pi_disconnect(pi);
6840#line 828
6841 __cil_tmp48 = & tape->name;
6842#line 828
6843 __cil_tmp49 = (char *)__cil_tmp48;
6844#line 828
6845 printk("%s: Phase error on read: %d\n", __cil_tmp49, p);
6846 }
6847#line 830
6848 return (-5L);
6849 } else {
6850
6851 }
6852#line 833
6853 goto ldv_21707;
6854 ldv_21706:
6855#line 834
6856 k = n;
6857#line 835
6858 if (k > 16384) {
6859#line 836
6860 k = 16384;
6861 } else {
6862
6863 }
6864 {
6865#line 837
6866 __cil_tmp50 = tape->bufptr;
6867#line 837
6868 pi_read_block(pi, __cil_tmp50, k);
6869#line 838
6870 n = n - k;
6871#line 839
6872 b = k;
6873 }
6874 {
6875#line 840
6876 __cil_tmp51 = (size_t )b;
6877#line 840
6878 if (__cil_tmp51 > count) {
6879#line 841
6880 b = (int )count;
6881 } else {
6882
6883 }
6884 }
6885 {
6886#line 842
6887 __cil_tmp52 = (unsigned long )t;
6888#line 842
6889 __cil_tmp53 = (void *)buf;
6890#line 842
6891 __cil_tmp54 = __cil_tmp53 + __cil_tmp52;
6892#line 842
6893 __cil_tmp55 = tape->bufptr;
6894#line 842
6895 __cil_tmp56 = (void const *)__cil_tmp55;
6896#line 842
6897 __cil_tmp57 = (unsigned int )b;
6898#line 842
6899 tmp___6 = copy_to_user(__cil_tmp54, __cil_tmp56, __cil_tmp57);
6900 }
6901#line 842
6902 if (tmp___6 != 0) {
6903 {
6904#line 843
6905 pi_disconnect(pi);
6906 }
6907#line 844
6908 return (-14L);
6909 } else {
6910
6911 }
6912#line 846
6913 t = t + b;
6914#line 847
6915 __cil_tmp58 = (size_t )b;
6916#line 847
6917 count = count - __cil_tmp58;
6918 ldv_21707: ;
6919#line 833
6920 if (n > 0) {
6921#line 834
6922 goto ldv_21706;
6923 } else {
6924#line 836
6925 goto ldv_21708;
6926 }
6927 ldv_21708: ;
6928#line 850
6929 goto ldv_21709;
6930 ldv_21705:
6931 {
6932#line 851
6933 pi_disconnect(pi);
6934 }
6935 {
6936#line 852
6937 __cil_tmp59 = tape->flags;
6938#line 852
6939 __cil_tmp60 = __cil_tmp59 & 32;
6940#line 852
6941 if (__cil_tmp60 != 0) {
6942#line 853
6943 goto ldv_21710;
6944 } else {
6945
6946 }
6947 }
6948 ldv_21712: ;
6949#line 782
6950 if (count != 0UL) {
6951#line 783
6952 goto ldv_21711;
6953 } else {
6954#line 785
6955 goto ldv_21710;
6956 }
6957 ldv_21710: ;
6958#line 856
6959 return ((ssize_t )t);
6960}
6961}
6962#line 860 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
6963static ssize_t pt_write(struct file *filp , char const *buf , size_t count , loff_t *ppos )
6964{ struct pt_unit *tape ;
6965 struct pi_adapter *pi ;
6966 char wr_cmd[12U] ;
6967 int k ;
6968 int n ;
6969 int r ;
6970 int p ;
6971 int s ;
6972 int t ;
6973 int b ;
6974 int tmp ;
6975 int tmp___0 ;
6976 unsigned long __ms ;
6977 unsigned long tmp___1 ;
6978 char *tmp___2 ;
6979 int tmp___3 ;
6980 int tmp___4 ;
6981 int tmp___5 ;
6982 unsigned long tmp___6 ;
6983 void *__cil_tmp24 ;
6984 int __cil_tmp25 ;
6985 int __cil_tmp26 ;
6986 int __cil_tmp27 ;
6987 int __cil_tmp28 ;
6988 int __cil_tmp29 ;
6989 char *__cil_tmp30 ;
6990 char *__cil_tmp31 ;
6991 char *__cil_tmp32 ;
6992 int __cil_tmp33 ;
6993 int __cil_tmp34 ;
6994 int __cil_tmp35 ;
6995 int __cil_tmp36 ;
6996 char *__cil_tmp37 ;
6997 int __cil_tmp38 ;
6998 int __cil_tmp39 ;
6999 int __cil_tmp40 ;
7000 int __cil_tmp41 ;
7001 int __cil_tmp42 ;
7002 char *__cil_tmp43 ;
7003 char *__cil_tmp44 ;
7004 char *__cil_tmp45 ;
7005 int __cil_tmp46 ;
7006 int __cil_tmp47 ;
7007 int __cil_tmp48 ;
7008 int __cil_tmp49 ;
7009 char (*__cil_tmp50)[8U] ;
7010 char *__cil_tmp51 ;
7011 size_t __cil_tmp52 ;
7012 char *__cil_tmp53 ;
7013 void *__cil_tmp54 ;
7014 unsigned long __cil_tmp55 ;
7015 void const *__cil_tmp56 ;
7016 void const *__cil_tmp57 ;
7017 unsigned long __cil_tmp58 ;
7018 char *__cil_tmp59 ;
7019 size_t __cil_tmp60 ;
7020 int __cil_tmp61 ;
7021 int __cil_tmp62 ;
7022
7023 {
7024#line 862
7025 __cil_tmp24 = filp->private_data;
7026#line 862
7027 tape = (struct pt_unit *)__cil_tmp24;
7028#line 863
7029 pi = tape->pi;
7030#line 864
7031 wr_cmd[0] = (char)10;
7032#line 864
7033 wr_cmd[1] = (char)1;
7034#line 864
7035 wr_cmd[2] = (char)0;
7036#line 864
7037 wr_cmd[3] = (char)0;
7038#line 864
7039 wr_cmd[4] = (char)0;
7040#line 864
7041 wr_cmd[5] = (char)0;
7042#line 864
7043 wr_cmd[6] = (char)0;
7044#line 864
7045 wr_cmd[7] = (char)0;
7046#line 864
7047 wr_cmd[8] = (char)0;
7048#line 864
7049 wr_cmd[9] = (char)0;
7050#line 864
7051 wr_cmd[10] = (char)0;
7052#line 864
7053 wr_cmd[11] = (char)0;
7054 {
7055#line 867
7056 __cil_tmp25 = tape->flags;
7057#line 867
7058 __cil_tmp26 = __cil_tmp25 & 2;
7059#line 867
7060 if (__cil_tmp26 == 0) {
7061#line 868
7062 return (-30L);
7063 } else {
7064
7065 }
7066 }
7067 {
7068#line 870
7069 __cil_tmp27 = tape->flags;
7070#line 870
7071 __cil_tmp28 = __cil_tmp27 & 24;
7072#line 870
7073 if (__cil_tmp28 == 0) {
7074 {
7075#line 871
7076 __cil_tmp29 = tape->flags;
7077#line 871
7078 tape->flags = __cil_tmp29 | 8;
7079#line 872
7080 __cil_tmp30 = (char *)(& wr_cmd);
7081#line 872
7082 __cil_tmp31 = (char *)0;
7083#line 872
7084 __cil_tmp32 = (char *)"start buffer-available mode";
7085#line 872
7086 tmp = pt_atapi(tape, __cil_tmp30, 0, __cil_tmp31, __cil_tmp32);
7087 }
7088#line 872
7089 if (tmp != 0) {
7090#line 874
7091 return (-5L);
7092 } else {
7093
7094 }
7095 } else {
7096 {
7097#line 875
7098 __cil_tmp33 = tape->flags;
7099#line 875
7100 __cil_tmp34 = __cil_tmp33 & 16;
7101#line 875
7102 if (__cil_tmp34 != 0) {
7103#line 876
7104 return (-5L);
7105 } else {
7106
7107 }
7108 }
7109 }
7110 }
7111 {
7112#line 878
7113 __cil_tmp35 = tape->flags;
7114#line 878
7115 __cil_tmp36 = __cil_tmp35 & 32;
7116#line 878
7117 if (__cil_tmp36 != 0) {
7118#line 879
7119 return (-28L);
7120 } else {
7121
7122 }
7123 }
7124#line 881
7125 t = 0;
7126#line 883
7127 goto ldv_21740;
7128 ldv_21739:
7129 {
7130#line 885
7131 __cil_tmp37 = (char *)"write";
7132#line 885
7133 tmp___0 = pt_poll_dsc(tape, 2, 3000, __cil_tmp37);
7134 }
7135#line 885
7136 if (tmp___0 == 0) {
7137#line 886
7138 return (-5L);
7139 } else {
7140
7141 }
7142#line 888
7143 n = (int )count;
7144#line 889
7145 if (n > 32768) {
7146#line 890
7147 n = 32768;
7148 } else {
7149
7150 }
7151 {
7152#line 891
7153 __cil_tmp38 = tape->bs;
7154#line 891
7155 __cil_tmp39 = tape->bs;
7156#line 891
7157 __cil_tmp40 = n + -1;
7158#line 891
7159 __cil_tmp41 = __cil_tmp40 + __cil_tmp39;
7160#line 891
7161 b = __cil_tmp41 / __cil_tmp38;
7162#line 892
7163 __cil_tmp42 = tape->bs;
7164#line 892
7165 n = __cil_tmp42 * b;
7166#line 894
7167 wr_cmd[4] = (char )b;
7168#line 896
7169 __cil_tmp43 = (char *)(& wr_cmd);
7170#line 896
7171 __cil_tmp44 = (char *)"write";
7172#line 896
7173 r = pt_command(tape, __cil_tmp43, n, __cil_tmp44);
7174 }
7175#line 898
7176 if (1) {
7177 {
7178#line 898
7179 __const_udelay(4295000UL);
7180 }
7181 } else {
7182#line 898
7183 __ms = 1UL;
7184#line 898
7185 goto ldv_21731;
7186 ldv_21730:
7187 {
7188#line 898
7189 __const_udelay(4295000UL);
7190 }
7191 ldv_21731:
7192#line 898
7193 tmp___1 = __ms;
7194#line 898
7195 __ms = __ms - 1UL;
7196#line 898
7197 if (tmp___1 != 0UL) {
7198#line 899
7199 goto ldv_21730;
7200 } else {
7201#line 901
7202 goto ldv_21732;
7203 }
7204 ldv_21732: ;
7205 }
7206#line 900
7207 if (r != 0) {
7208 {
7209#line 901
7210 pt_req_sense(tape, 0);
7211 }
7212#line 902
7213 return (-5L);
7214 } else {
7215
7216 }
7217 ldv_21737: ;
7218#line 907
7219 if (verbose > 1) {
7220#line 907
7221 tmp___2 = (char *)"write DRQ";
7222 } else {
7223#line 907
7224 tmp___2 = (char *)0;
7225 }
7226 {
7227#line 907
7228 __cil_tmp45 = (char *)0;
7229#line 907
7230 r = pt_wait(tape, 128, 73, tmp___2, __cil_tmp45);
7231 }
7232 {
7233#line 911
7234 __cil_tmp46 = r & 126976;
7235#line 911
7236 if (__cil_tmp46 != 0) {
7237 {
7238#line 912
7239 pi_disconnect(pi);
7240#line 913
7241 pt_req_sense(tape, 0);
7242 }
7243#line 914
7244 return (-5L);
7245 } else {
7246
7247 }
7248 }
7249#line 917
7250 if (r != 0) {
7251#line 918
7252 __cil_tmp47 = tape->flags;
7253#line 918
7254 tape->flags = __cil_tmp47 | 32;
7255 } else {
7256
7257 }
7258 {
7259#line 920
7260 s = read_reg(pi, 7);
7261 }
7262 {
7263#line 922
7264 __cil_tmp48 = s & 8;
7265#line 922
7266 if (__cil_tmp48 == 0) {
7267#line 923
7268 goto ldv_21733;
7269 } else {
7270
7271 }
7272 }
7273 {
7274#line 925
7275 tmp___3 = read_reg(pi, 4);
7276#line 925
7277 tmp___4 = read_reg(pi, 5);
7278#line 925
7279 __cil_tmp49 = tmp___4 * 256;
7280#line 925
7281 n = tmp___3 + __cil_tmp49;
7282#line 926
7283 tmp___5 = read_reg(pi, 2);
7284#line 926
7285 p = tmp___5 & 3;
7286 }
7287#line 927
7288 if (p != 0) {
7289 {
7290#line 928
7291 pi_disconnect(pi);
7292#line 929
7293 __cil_tmp50 = & tape->name;
7294#line 929
7295 __cil_tmp51 = (char *)__cil_tmp50;
7296#line 929
7297 printk("%s: Phase error on write: %d \n", __cil_tmp51, p);
7298 }
7299#line 931
7300 return (-5L);
7301 } else {
7302
7303 }
7304#line 934
7305 goto ldv_21735;
7306 ldv_21734:
7307#line 935
7308 k = n;
7309#line 936
7310 if (k > 16384) {
7311#line 937
7312 k = 16384;
7313 } else {
7314
7315 }
7316#line 938
7317 b = k;
7318 {
7319#line 939
7320 __cil_tmp52 = (size_t )b;
7321#line 939
7322 if (__cil_tmp52 > count) {
7323#line 940
7324 b = (int )count;
7325 } else {
7326
7327 }
7328 }
7329 {
7330#line 941
7331 __cil_tmp53 = tape->bufptr;
7332#line 941
7333 __cil_tmp54 = (void *)__cil_tmp53;
7334#line 941
7335 __cil_tmp55 = (unsigned long )t;
7336#line 941
7337 __cil_tmp56 = (void const *)buf;
7338#line 941
7339 __cil_tmp57 = __cil_tmp56 + __cil_tmp55;
7340#line 941
7341 __cil_tmp58 = (unsigned long )b;
7342#line 941
7343 tmp___6 = copy_from_user(__cil_tmp54, __cil_tmp57, __cil_tmp58);
7344 }
7345#line 941
7346 if (tmp___6 != 0UL) {
7347 {
7348#line 942
7349 pi_disconnect(pi);
7350 }
7351#line 943
7352 return (-14L);
7353 } else {
7354
7355 }
7356 {
7357#line 945
7358 __cil_tmp59 = tape->bufptr;
7359#line 945
7360 pi_write_block(pi, __cil_tmp59, k);
7361#line 946
7362 t = t + b;
7363#line 947
7364 __cil_tmp60 = (size_t )b;
7365#line 947
7366 count = count - __cil_tmp60;
7367#line 948
7368 n = n - k;
7369 }
7370 ldv_21735: ;
7371#line 934
7372 if (n > 0) {
7373#line 935
7374 goto ldv_21734;
7375 } else {
7376#line 937
7377 goto ldv_21736;
7378 }
7379 ldv_21736: ;
7380#line 951
7381 goto ldv_21737;
7382 ldv_21733:
7383 {
7384#line 952
7385 pi_disconnect(pi);
7386 }
7387 {
7388#line 953
7389 __cil_tmp61 = tape->flags;
7390#line 953
7391 __cil_tmp62 = __cil_tmp61 & 32;
7392#line 953
7393 if (__cil_tmp62 != 0) {
7394#line 954
7395 goto ldv_21738;
7396 } else {
7397
7398 }
7399 }
7400 ldv_21740: ;
7401#line 883
7402 if (count != 0UL) {
7403#line 884
7404 goto ldv_21739;
7405 } else {
7406#line 886
7407 goto ldv_21738;
7408 }
7409 ldv_21738: ;
7410#line 957
7411 return ((ssize_t )t);
7412}
7413}
7414#line 960 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
7415static int pt_init(void)
7416{ int unit ;
7417 int err ;
7418 int tmp ;
7419 struct lock_class_key __key ;
7420 struct class *tmp___0 ;
7421 long tmp___1 ;
7422 long tmp___2 ;
7423 unsigned int __cil_tmp8 ;
7424 char const *__cil_tmp9 ;
7425 void const *__cil_tmp10 ;
7426 void const *__cil_tmp11 ;
7427 struct device *__cil_tmp12 ;
7428 int __cil_tmp13 ;
7429 int __cil_tmp14 ;
7430 dev_t __cil_tmp15 ;
7431 void *__cil_tmp16 ;
7432 struct device *__cil_tmp17 ;
7433 int __cil_tmp18 ;
7434 int __cil_tmp19 ;
7435 int __cil_tmp20 ;
7436 dev_t __cil_tmp21 ;
7437 void *__cil_tmp22 ;
7438 unsigned int __cil_tmp23 ;
7439
7440 {
7441#line 965
7442 if (disable != 0) {
7443#line 966
7444 err = -22;
7445#line 967
7446 goto out;
7447 } else {
7448
7449 }
7450 {
7451#line 970
7452 tmp = pt_detect();
7453 }
7454#line 970
7455 if (tmp != 0) {
7456#line 971
7457 err = -19;
7458#line 972
7459 goto out;
7460 } else {
7461
7462 }
7463 {
7464#line 975
7465 __cil_tmp8 = (unsigned int )major;
7466#line 975
7467 __cil_tmp9 = (char const *)name;
7468#line 975
7469 err = register_chrdev(__cil_tmp8, __cil_tmp9, & pt_fops);
7470 }
7471#line 976
7472 if (err < 0) {
7473 {
7474#line 977
7475 printk("pt_init: unable to get major number %d\n", major);
7476#line 978
7477 unit = 0;
7478 }
7479#line 978
7480 goto ldv_21748;
7481 ldv_21747: ;
7482#line 979
7483 if (pt[unit].present != 0) {
7484 {
7485#line 980
7486 pi_release(pt[unit].pi);
7487 }
7488 } else {
7489
7490 }
7491#line 978
7492 unit = unit + 1;
7493 ldv_21748: ;
7494#line 978
7495 if (unit <= 3) {
7496#line 979
7497 goto ldv_21747;
7498 } else {
7499#line 981
7500 goto ldv_21749;
7501 }
7502 ldv_21749: ;
7503#line 981
7504 goto out;
7505 } else {
7506
7507 }
7508 {
7509#line 983
7510 major = err;
7511#line 984
7512 tmp___0 = __class_create(& __this_module, "pt", & __key);
7513#line 984
7514 pt_class = tmp___0;
7515#line 985
7516 __cil_tmp10 = (void const *)pt_class;
7517#line 985
7518 tmp___2 = IS_ERR(__cil_tmp10);
7519 }
7520#line 985
7521 if (tmp___2 != 0L) {
7522 {
7523#line 986
7524 __cil_tmp11 = (void const *)pt_class;
7525#line 986
7526 tmp___1 = PTR_ERR(__cil_tmp11);
7527#line 986
7528 err = (int )tmp___1;
7529 }
7530#line 987
7531 goto out_chrdev;
7532 } else {
7533
7534 }
7535#line 990
7536 unit = 0;
7537#line 990
7538 goto ldv_21754;
7539 ldv_21753: ;
7540#line 991
7541 if (pt[unit].present != 0) {
7542 {
7543#line 992
7544 __cil_tmp12 = (struct device *)0;
7545#line 992
7546 __cil_tmp13 = major << 20;
7547#line 992
7548 __cil_tmp14 = __cil_tmp13 | unit;
7549#line 992
7550 __cil_tmp15 = (dev_t )__cil_tmp14;
7551#line 992
7552 __cil_tmp16 = (void *)0;
7553#line 992
7554 device_create(pt_class, __cil_tmp12, __cil_tmp15, __cil_tmp16, "pt%d", unit);
7555#line 994
7556 __cil_tmp17 = (struct device *)0;
7557#line 994
7558 __cil_tmp18 = unit + 128;
7559#line 994
7560 __cil_tmp19 = major << 20;
7561#line 994
7562 __cil_tmp20 = __cil_tmp19 | __cil_tmp18;
7563#line 994
7564 __cil_tmp21 = (dev_t )__cil_tmp20;
7565#line 994
7566 __cil_tmp22 = (void *)0;
7567#line 994
7568 device_create(pt_class, __cil_tmp17, __cil_tmp21, __cil_tmp22, "pt%dn", unit);
7569 }
7570 } else {
7571
7572 }
7573#line 990
7574 unit = unit + 1;
7575 ldv_21754: ;
7576#line 990
7577 if (unit <= 3) {
7578#line 991
7579 goto ldv_21753;
7580 } else {
7581#line 993
7582 goto ldv_21755;
7583 }
7584 ldv_21755: ;
7585#line 997
7586 goto out;
7587 out_chrdev:
7588 {
7589#line 1000
7590 __cil_tmp23 = (unsigned int )major;
7591#line 1000
7592 unregister_chrdev(__cil_tmp23, "pt");
7593 }
7594 out: ;
7595#line 1002
7596 return (err);
7597}
7598}
7599#line 1005 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
7600static void pt_exit(void)
7601{ int unit ;
7602 int __cil_tmp2 ;
7603 int __cil_tmp3 ;
7604 dev_t __cil_tmp4 ;
7605 int __cil_tmp5 ;
7606 int __cil_tmp6 ;
7607 int __cil_tmp7 ;
7608 dev_t __cil_tmp8 ;
7609 unsigned int __cil_tmp9 ;
7610 char const *__cil_tmp10 ;
7611
7612 {
7613#line 1008
7614 unit = 0;
7615#line 1008
7616 goto ldv_21761;
7617 ldv_21760: ;
7618#line 1009
7619 if (pt[unit].present != 0) {
7620 {
7621#line 1010
7622 __cil_tmp2 = major << 20;
7623#line 1010
7624 __cil_tmp3 = __cil_tmp2 | unit;
7625#line 1010
7626 __cil_tmp4 = (dev_t )__cil_tmp3;
7627#line 1010
7628 device_destroy(pt_class, __cil_tmp4);
7629#line 1011
7630 __cil_tmp5 = unit + 128;
7631#line 1011
7632 __cil_tmp6 = major << 20;
7633#line 1011
7634 __cil_tmp7 = __cil_tmp6 | __cil_tmp5;
7635#line 1011
7636 __cil_tmp8 = (dev_t )__cil_tmp7;
7637#line 1011
7638 device_destroy(pt_class, __cil_tmp8);
7639 }
7640 } else {
7641
7642 }
7643#line 1008
7644 unit = unit + 1;
7645 ldv_21761: ;
7646#line 1008
7647 if (unit <= 3) {
7648#line 1009
7649 goto ldv_21760;
7650 } else {
7651#line 1011
7652 goto ldv_21762;
7653 }
7654 ldv_21762:
7655 {
7656#line 1013
7657 class_destroy(pt_class);
7658#line 1014
7659 __cil_tmp9 = (unsigned int )major;
7660#line 1014
7661 __cil_tmp10 = (char const *)name;
7662#line 1014
7663 unregister_chrdev(__cil_tmp9, __cil_tmp10);
7664#line 1015
7665 unit = 0;
7666 }
7667#line 1015
7668 goto ldv_21764;
7669 ldv_21763: ;
7670#line 1016
7671 if (pt[unit].present != 0) {
7672 {
7673#line 1017
7674 pi_release(pt[unit].pi);
7675 }
7676 } else {
7677
7678 }
7679#line 1015
7680 unit = unit + 1;
7681 ldv_21764: ;
7682#line 1015
7683 if (unit <= 3) {
7684#line 1016
7685 goto ldv_21763;
7686 } else {
7687#line 1018
7688 goto ldv_21765;
7689 }
7690 ldv_21765: ;
7691#line 1020
7692 return;
7693}
7694}
7695#line 1040
7696void ldv_check_final_state(void) ;
7697#line 1043
7698extern void ldv_check_return_value(int ) ;
7699#line 1046
7700extern void ldv_initialize(void) ;
7701#line 1049
7702extern int nondet_int(void) ;
7703#line 1052 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
7704int LDV_IN_INTERRUPT ;
7705#line 1055 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
7706void main(void)
7707{ struct file *var_group1 ;
7708 char *var_pt_read_24_p1 ;
7709 size_t var_pt_read_24_p2 ;
7710 loff_t *var_pt_read_24_p3 ;
7711 ssize_t res_pt_read_24 ;
7712 char const *var_pt_write_25_p1 ;
7713 size_t var_pt_write_25_p2 ;
7714 loff_t *var_pt_write_25_p3 ;
7715 ssize_t res_pt_write_25 ;
7716 unsigned int var_pt_ioctl_22_p1 ;
7717 unsigned long var_pt_ioctl_22_p2 ;
7718 struct inode *var_group2 ;
7719 int res_pt_open_21 ;
7720 int ldv_s_pt_fops_file_operations ;
7721 int tmp ;
7722 int tmp___0 ;
7723 int tmp___1 ;
7724 int __cil_tmp18 ;
7725 int __cil_tmp19 ;
7726
7727 {
7728 {
7729#line 1398
7730 ldv_s_pt_fops_file_operations = 0;
7731#line 1335
7732 LDV_IN_INTERRUPT = 1;
7733#line 1344
7734 ldv_initialize();
7735#line 1396
7736 tmp = pt_init();
7737 }
7738#line 1396
7739 if (tmp != 0) {
7740#line 1397
7741 goto ldv_final;
7742 } else {
7743
7744 }
7745#line 1402
7746 goto ldv_21813;
7747 ldv_21812:
7748 {
7749#line 1406
7750 tmp___0 = nondet_int();
7751 }
7752#line 1408
7753 if (tmp___0 == 0) {
7754#line 1408
7755 goto case_0;
7756 } else
7757#line 1473
7758 if (tmp___0 == 1) {
7759#line 1473
7760 goto case_1;
7761 } else
7762#line 1538
7763 if (tmp___0 == 2) {
7764#line 1538
7765 goto case_2;
7766 } else
7767#line 1603
7768 if (tmp___0 == 3) {
7769#line 1603
7770 goto case_3;
7771 } else
7772#line 1665
7773 if (tmp___0 == 4) {
7774#line 1665
7775 goto case_4;
7776 } else {
7777#line 1727
7778 goto switch_default;
7779#line 1406
7780 if (0) {
7781 case_0: ;
7782#line 1411
7783 if (ldv_s_pt_fops_file_operations == 0) {
7784 {
7785#line 1462
7786 res_pt_open_21 = pt_open(var_group2, var_group1);
7787#line 1463
7788 ldv_check_return_value(res_pt_open_21);
7789 }
7790#line 1464
7791 if (res_pt_open_21 != 0) {
7792#line 1465
7793 goto ldv_module_exit;
7794 } else {
7795
7796 }
7797#line 1466
7798 ldv_s_pt_fops_file_operations = ldv_s_pt_fops_file_operations + 1;
7799 } else {
7800
7801 }
7802#line 1472
7803 goto ldv_21806;
7804 case_1: ;
7805#line 1476
7806 if (ldv_s_pt_fops_file_operations == 1) {
7807 {
7808#line 1527
7809 res_pt_read_24 = pt_read(var_group1, var_pt_read_24_p1, var_pt_read_24_p2,
7810 var_pt_read_24_p3);
7811#line 1528
7812 __cil_tmp18 = (int )res_pt_read_24;
7813#line 1528
7814 ldv_check_return_value(__cil_tmp18);
7815 }
7816#line 1529
7817 if (res_pt_read_24 < 0L) {
7818#line 1530
7819 goto ldv_module_exit;
7820 } else {
7821
7822 }
7823#line 1531
7824 ldv_s_pt_fops_file_operations = ldv_s_pt_fops_file_operations + 1;
7825 } else {
7826
7827 }
7828#line 1537
7829 goto ldv_21806;
7830 case_2: ;
7831#line 1541
7832 if (ldv_s_pt_fops_file_operations == 2) {
7833 {
7834#line 1592
7835 res_pt_write_25 = pt_write(var_group1, var_pt_write_25_p1, var_pt_write_25_p2,
7836 var_pt_write_25_p3);
7837#line 1593
7838 __cil_tmp19 = (int )res_pt_write_25;
7839#line 1593
7840 ldv_check_return_value(__cil_tmp19);
7841 }
7842#line 1594
7843 if (res_pt_write_25 < 0L) {
7844#line 1595
7845 goto ldv_module_exit;
7846 } else {
7847
7848 }
7849#line 1596
7850 ldv_s_pt_fops_file_operations = ldv_s_pt_fops_file_operations + 1;
7851 } else {
7852
7853 }
7854#line 1602
7855 goto ldv_21806;
7856 case_3: ;
7857#line 1606
7858 if (ldv_s_pt_fops_file_operations == 3) {
7859 {
7860#line 1657
7861 pt_release(var_group2, var_group1);
7862#line 1658
7863 ldv_s_pt_fops_file_operations = 0;
7864 }
7865 } else {
7866
7867 }
7868#line 1664
7869 goto ldv_21806;
7870 case_4:
7871 {
7872#line 1719
7873 pt_ioctl(var_group1, var_pt_ioctl_22_p1, var_pt_ioctl_22_p2);
7874 }
7875#line 1726
7876 goto ldv_21806;
7877 switch_default: ;
7878#line 1727
7879 goto ldv_21806;
7880 } else {
7881
7882 }
7883 }
7884 ldv_21806: ;
7885 ldv_21813:
7886 {
7887#line 1402
7888 tmp___1 = nondet_int();
7889 }
7890#line 1402
7891 if (tmp___1 != 0) {
7892#line 1404
7893 goto ldv_21812;
7894 } else
7895#line 1402
7896 if (ldv_s_pt_fops_file_operations != 0) {
7897#line 1404
7898 goto ldv_21812;
7899 } else {
7900#line 1406
7901 goto ldv_21814;
7902 }
7903 ldv_21814: ;
7904 ldv_module_exit:
7905 {
7906#line 1785
7907 pt_exit();
7908 }
7909 ldv_final:
7910 {
7911#line 1788
7912 ldv_check_final_state();
7913 }
7914#line 1791
7915 return;
7916}
7917}
7918#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
7919void ldv_blast_assert(void)
7920{
7921
7922 {
7923 ERROR: ;
7924#line 6
7925 goto ERROR;
7926}
7927}
7928#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
7929extern int ldv_undefined_int(void) ;
7930#line 1808 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
7931int ldv_module_refcounter = 1;
7932#line 1811 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
7933void ldv_module_get(struct module *module )
7934{ struct module *__cil_tmp2 ;
7935 unsigned long __cil_tmp3 ;
7936 unsigned long __cil_tmp4 ;
7937
7938 {
7939 {
7940#line 1814
7941 __cil_tmp2 = (struct module *)0;
7942#line 1814
7943 __cil_tmp3 = (unsigned long )__cil_tmp2;
7944#line 1814
7945 __cil_tmp4 = (unsigned long )module;
7946#line 1814
7947 if (__cil_tmp4 != __cil_tmp3) {
7948#line 1816
7949 ldv_module_refcounter = ldv_module_refcounter + 1;
7950 } else {
7951
7952 }
7953 }
7954#line 1817
7955 return;
7956}
7957}
7958#line 1821 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
7959int ldv_try_module_get(struct module *module )
7960{ int module_get_succeeded ;
7961 struct module *__cil_tmp3 ;
7962 unsigned long __cil_tmp4 ;
7963 unsigned long __cil_tmp5 ;
7964
7965 {
7966 {
7967#line 1826
7968 __cil_tmp3 = (struct module *)0;
7969#line 1826
7970 __cil_tmp4 = (unsigned long )__cil_tmp3;
7971#line 1826
7972 __cil_tmp5 = (unsigned long )module;
7973#line 1826
7974 if (__cil_tmp5 != __cil_tmp4) {
7975 {
7976#line 1829
7977 module_get_succeeded = ldv_undefined_int();
7978 }
7979#line 1831
7980 if (module_get_succeeded == 1) {
7981#line 1833
7982 ldv_module_refcounter = ldv_module_refcounter + 1;
7983#line 1835
7984 return (1);
7985 } else {
7986#line 1840
7987 return (0);
7988 }
7989 } else {
7990
7991 }
7992 }
7993#line 1842
7994 return (0);
7995}
7996}
7997#line 1846 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
7998void ldv_module_put(struct module *module )
7999{ struct module *__cil_tmp2 ;
8000 unsigned long __cil_tmp3 ;
8001 unsigned long __cil_tmp4 ;
8002
8003 {
8004 {
8005#line 1849
8006 __cil_tmp2 = (struct module *)0;
8007#line 1849
8008 __cil_tmp3 = (unsigned long )__cil_tmp2;
8009#line 1849
8010 __cil_tmp4 = (unsigned long )module;
8011#line 1849
8012 if (__cil_tmp4 != __cil_tmp3) {
8013#line 1851
8014 if (ldv_module_refcounter <= 1) {
8015 {
8016#line 1851
8017 ldv_blast_assert();
8018 }
8019 } else {
8020
8021 }
8022#line 1853
8023 ldv_module_refcounter = ldv_module_refcounter - 1;
8024 } else {
8025
8026 }
8027 }
8028#line 1855
8029 return;
8030}
8031}
8032#line 1858 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
8033void ldv_module_put_and_exit(void)
8034{ struct module *__cil_tmp1 ;
8035
8036 {
8037 {
8038#line 1860
8039 __cil_tmp1 = (struct module *)1;
8040#line 1860
8041 ldv_module_put(__cil_tmp1);
8042 }
8043 LDV_STOP: ;
8044#line 1862
8045 goto LDV_STOP;
8046}
8047}
8048#line 1866 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
8049unsigned int ldv_module_refcount(void)
8050{ int __cil_tmp1 ;
8051
8052 {
8053 {
8054#line 1869
8055 __cil_tmp1 = ldv_module_refcounter + -1;
8056#line 1869
8057 return ((unsigned int )__cil_tmp1);
8058 }
8059}
8060}
8061#line 1873 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
8062void ldv_check_final_state(void)
8063{
8064
8065 {
8066#line 1876
8067 if (ldv_module_refcounter != 1) {
8068 {
8069#line 1876
8070 ldv_blast_assert();
8071 }
8072 } else {
8073
8074 }
8075#line 1879
8076 return;
8077}
8078}