1
2
3
4#line 19 "include/asm-generic/int-ll64.h"
5typedef signed char __s8;
6#line 20 "include/asm-generic/int-ll64.h"
7typedef unsigned char __u8;
8#line 22 "include/asm-generic/int-ll64.h"
9typedef short __s16;
10#line 23 "include/asm-generic/int-ll64.h"
11typedef unsigned short __u16;
12#line 25 "include/asm-generic/int-ll64.h"
13typedef int __s32;
14#line 26 "include/asm-generic/int-ll64.h"
15typedef unsigned int __u32;
16#line 29 "include/asm-generic/int-ll64.h"
17typedef long long __s64;
18#line 30 "include/asm-generic/int-ll64.h"
19typedef unsigned long long __u64;
20#line 43 "include/asm-generic/int-ll64.h"
21typedef unsigned char u8;
22#line 46 "include/asm-generic/int-ll64.h"
23typedef unsigned short u16;
24#line 49 "include/asm-generic/int-ll64.h"
25typedef unsigned int u32;
26#line 51 "include/asm-generic/int-ll64.h"
27typedef long long s64;
28#line 52 "include/asm-generic/int-ll64.h"
29typedef unsigned long long u64;
30#line 11 "include/asm-generic/types.h"
31typedef unsigned short umode_t;
32#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"
33typedef unsigned int __kernel_mode_t;
34#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"
35typedef int __kernel_pid_t;
36#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"
37typedef unsigned int __kernel_uid_t;
38#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"
39typedef unsigned int __kernel_gid_t;
40#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"
41typedef unsigned long __kernel_size_t;
42#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"
43typedef long __kernel_ssize_t;
44#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"
45typedef long __kernel_time_t;
46#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"
47typedef long __kernel_clock_t;
48#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"
49typedef int __kernel_timer_t;
50#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"
51typedef int __kernel_clockid_t;
52#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"
53typedef long long __kernel_loff_t;
54#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"
55typedef __kernel_uid_t __kernel_uid32_t;
56#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"
57typedef __kernel_gid_t __kernel_gid32_t;
58#line 21 "include/linux/types.h"
59typedef __u32 __kernel_dev_t;
60#line 24 "include/linux/types.h"
61typedef __kernel_dev_t dev_t;
62#line 26 "include/linux/types.h"
63typedef __kernel_mode_t mode_t;
64#line 29 "include/linux/types.h"
65typedef __kernel_pid_t pid_t;
66#line 34 "include/linux/types.h"
67typedef __kernel_clockid_t clockid_t;
68#line 37 "include/linux/types.h"
69typedef _Bool bool;
70#line 39 "include/linux/types.h"
71typedef __kernel_uid32_t uid_t;
72#line 40 "include/linux/types.h"
73typedef __kernel_gid32_t gid_t;
74#line 53 "include/linux/types.h"
75typedef __kernel_loff_t loff_t;
76#line 62 "include/linux/types.h"
77typedef __kernel_size_t size_t;
78#line 67 "include/linux/types.h"
79typedef __kernel_ssize_t ssize_t;
80#line 77 "include/linux/types.h"
81typedef __kernel_time_t time_t;
82#line 110 "include/linux/types.h"
83typedef __s32 int32_t;
84#line 116 "include/linux/types.h"
85typedef __u32 uint32_t;
86#line 141 "include/linux/types.h"
87typedef unsigned long sector_t;
88#line 142 "include/linux/types.h"
89typedef unsigned long blkcnt_t;
90#line 154 "include/linux/types.h"
91typedef u64 dma_addr_t;
92#line 177 "include/linux/types.h"
93typedef __u16 __le16;
94#line 201 "include/linux/types.h"
95typedef unsigned int gfp_t;
96#line 202 "include/linux/types.h"
97typedef unsigned int fmode_t;
98#line 212 "include/linux/types.h"
99struct __anonstruct_atomic_t_7 {
100 int counter ;
101};
102#line 212 "include/linux/types.h"
103typedef struct __anonstruct_atomic_t_7 atomic_t;
104#line 217 "include/linux/types.h"
105struct __anonstruct_atomic64_t_8 {
106 long counter ;
107};
108#line 217 "include/linux/types.h"
109typedef struct __anonstruct_atomic64_t_8 atomic64_t;
110#line 222 "include/linux/types.h"
111struct list_head {
112 struct list_head *next ;
113 struct list_head *prev ;
114};
115#line 226
116struct hlist_node;
117#line 226
118struct hlist_node;
119#line 226
120struct hlist_node;
121#line 226 "include/linux/types.h"
122struct hlist_head {
123 struct hlist_node *first ;
124};
125#line 230 "include/linux/types.h"
126struct hlist_node {
127 struct hlist_node *next ;
128 struct hlist_node **pprev ;
129};
130#line 59 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/alternative.h"
131struct module;
132#line 59
133struct module;
134#line 59
135struct module;
136#line 59
137struct module;
138#line 145 "include/linux/init.h"
139typedef void (*ctor_fn_t)(void);
140#line 10 "include/asm-generic/bug.h"
141struct bug_entry {
142 int bug_addr_disp ;
143 int file_disp ;
144 unsigned short line ;
145 unsigned short flags ;
146};
147#line 113 "include/linux/kernel.h"
148struct completion;
149#line 113
150struct completion;
151#line 113
152struct completion;
153#line 113
154struct completion;
155#line 114
156struct pt_regs;
157#line 114
158struct pt_regs;
159#line 114
160struct pt_regs;
161#line 114
162struct pt_regs;
163#line 322
164struct pid;
165#line 322
166struct pid;
167#line 322
168struct pid;
169#line 322
170struct pid;
171#line 12 "include/linux/thread_info.h"
172struct timespec;
173#line 12
174struct timespec;
175#line 12
176struct timespec;
177#line 12
178struct timespec;
179#line 18 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/page.h"
180struct page;
181#line 18
182struct page;
183#line 18
184struct page;
185#line 18
186struct page;
187#line 20 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/thread_info.h"
188struct task_struct;
189#line 20
190struct task_struct;
191#line 20
192struct task_struct;
193#line 20
194struct task_struct;
195#line 7 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
196struct task_struct;
197#line 8
198struct mm_struct;
199#line 8
200struct mm_struct;
201#line 8
202struct mm_struct;
203#line 8
204struct mm_struct;
205#line 99 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/ptrace.h"
206struct pt_regs {
207 unsigned long r15 ;
208 unsigned long r14 ;
209 unsigned long r13 ;
210 unsigned long r12 ;
211 unsigned long bp ;
212 unsigned long bx ;
213 unsigned long r11 ;
214 unsigned long r10 ;
215 unsigned long r9 ;
216 unsigned long r8 ;
217 unsigned long ax ;
218 unsigned long cx ;
219 unsigned long dx ;
220 unsigned long si ;
221 unsigned long di ;
222 unsigned long orig_ax ;
223 unsigned long ip ;
224 unsigned long cs ;
225 unsigned long flags ;
226 unsigned long sp ;
227 unsigned long ss ;
228};
229#line 136
230struct task_struct;
231#line 141 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/vm86.h"
232struct kernel_vm86_regs {
233 struct pt_regs pt ;
234 unsigned short es ;
235 unsigned short __esh ;
236 unsigned short ds ;
237 unsigned short __dsh ;
238 unsigned short fs ;
239 unsigned short __fsh ;
240 unsigned short gs ;
241 unsigned short __gsh ;
242};
243#line 11 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/math_emu.h"
244union __anonunion____missing_field_name_14 {
245 struct pt_regs *regs ;
246 struct kernel_vm86_regs *vm86 ;
247};
248#line 11 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/math_emu.h"
249struct math_emu_info {
250 long ___orig_eip ;
251 union __anonunion____missing_field_name_14 __annonCompField5 ;
252};
253#line 8 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/current.h"
254struct task_struct;
255#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"
256typedef unsigned long pgdval_t;
257#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"
258typedef unsigned long pgprotval_t;
259#line 190 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
260struct pgprot {
261 pgprotval_t pgprot ;
262};
263#line 190 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
264typedef struct pgprot pgprot_t;
265#line 192 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
266struct __anonstruct_pgd_t_17 {
267 pgdval_t pgd ;
268};
269#line 192 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
270typedef struct __anonstruct_pgd_t_17 pgd_t;
271#line 280 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_types.h"
272typedef struct page *pgtable_t;
273#line 293
274struct file;
275#line 293
276struct file;
277#line 293
278struct file;
279#line 293
280struct file;
281#line 311
282struct seq_file;
283#line 311
284struct seq_file;
285#line 311
286struct seq_file;
287#line 311
288struct seq_file;
289#line 22 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/desc_defs.h"
290struct __anonstruct____missing_field_name_22 {
291 unsigned int a ;
292 unsigned int b ;
293};
294#line 22 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/desc_defs.h"
295struct __anonstruct____missing_field_name_23 {
296 u16 limit0 ;
297 u16 base0 ;
298 unsigned int base1 : 8 ;
299 unsigned int type : 4 ;
300 unsigned int s : 1 ;
301 unsigned int dpl : 2 ;
302 unsigned int p : 1 ;
303 unsigned int limit : 4 ;
304 unsigned int avl : 1 ;
305 unsigned int l : 1 ;
306 unsigned int d : 1 ;
307 unsigned int g : 1 ;
308 unsigned int base2 : 8 ;
309};
310#line 22 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/desc_defs.h"
311union __anonunion____missing_field_name_21 {
312 struct __anonstruct____missing_field_name_22 __annonCompField7 ;
313 struct __anonstruct____missing_field_name_23 __annonCompField8 ;
314};
315#line 22 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/desc_defs.h"
316struct desc_struct {
317 union __anonunion____missing_field_name_21 __annonCompField9 ;
318} __attribute__((__packed__)) ;
319#line 45 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/paravirt_types.h"
320struct page;
321#line 46
322struct thread_struct;
323#line 46
324struct thread_struct;
325#line 46
326struct thread_struct;
327#line 46
328struct thread_struct;
329#line 49
330struct mm_struct;
331#line 50
332struct desc_struct;
333#line 51
334struct task_struct;
335#line 52
336struct cpumask;
337#line 52
338struct cpumask;
339#line 52
340struct cpumask;
341#line 52
342struct cpumask;
343#line 322
344struct arch_spinlock;
345#line 322
346struct arch_spinlock;
347#line 322
348struct arch_spinlock;
349#line 322
350struct arch_spinlock;
351#line 13 "include/linux/cpumask.h"
352struct cpumask {
353 unsigned long bits[((4096UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
354};
355#line 13 "include/linux/cpumask.h"
356typedef struct cpumask cpumask_t;
357#line 622 "include/linux/cpumask.h"
358typedef struct cpumask *cpumask_var_t;
359#line 20 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/system.h"
360struct task_struct;
361#line 11 "include/linux/personality.h"
362struct pt_regs;
363#line 280 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
364struct i387_fsave_struct {
365 u32 cwd ;
366 u32 swd ;
367 u32 twd ;
368 u32 fip ;
369 u32 fcs ;
370 u32 foo ;
371 u32 fos ;
372 u32 st_space[20] ;
373 u32 status ;
374};
375#line 296 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
376struct __anonstruct____missing_field_name_31 {
377 u64 rip ;
378 u64 rdp ;
379};
380#line 296 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
381struct __anonstruct____missing_field_name_32 {
382 u32 fip ;
383 u32 fcs ;
384 u32 foo ;
385 u32 fos ;
386};
387#line 296 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
388union __anonunion____missing_field_name_30 {
389 struct __anonstruct____missing_field_name_31 __annonCompField12 ;
390 struct __anonstruct____missing_field_name_32 __annonCompField13 ;
391};
392#line 296 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
393union __anonunion____missing_field_name_33 {
394 u32 padding1[12] ;
395 u32 sw_reserved[12] ;
396};
397#line 296 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
398struct i387_fxsave_struct {
399 u16 cwd ;
400 u16 swd ;
401 u16 twd ;
402 u16 fop ;
403 union __anonunion____missing_field_name_30 __annonCompField14 ;
404 u32 mxcsr ;
405 u32 mxcsr_mask ;
406 u32 st_space[32] ;
407 u32 xmm_space[64] ;
408 u32 padding[12] ;
409 union __anonunion____missing_field_name_33 __annonCompField15 ;
410} __attribute__((__aligned__(16))) ;
411#line 331 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
412struct i387_soft_struct {
413 u32 cwd ;
414 u32 swd ;
415 u32 twd ;
416 u32 fip ;
417 u32 fcs ;
418 u32 foo ;
419 u32 fos ;
420 u32 st_space[20] ;
421 u8 ftop ;
422 u8 changed ;
423 u8 lookahead ;
424 u8 no_update ;
425 u8 rm ;
426 u8 alimit ;
427 struct math_emu_info *info ;
428 u32 entry_eip ;
429};
430#line 351 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
431struct ymmh_struct {
432 u32 ymmh_space[64] ;
433};
434#line 356 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
435struct xsave_hdr_struct {
436 u64 xstate_bv ;
437 u64 reserved1[2] ;
438 u64 reserved2[5] ;
439} __attribute__((__packed__)) ;
440#line 362 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
441struct xsave_struct {
442 struct i387_fxsave_struct i387 ;
443 struct xsave_hdr_struct xsave_hdr ;
444 struct ymmh_struct ymmh ;
445} __attribute__((__packed__, __aligned__(64))) ;
446#line 369 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
447union thread_xstate {
448 struct i387_fsave_struct fsave ;
449 struct i387_fxsave_struct fxsave ;
450 struct i387_soft_struct soft ;
451 struct xsave_struct xsave ;
452};
453#line 376 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
454struct fpu {
455 union thread_xstate *state ;
456};
457#line 421
458struct kmem_cache;
459#line 421
460struct kmem_cache;
461#line 421
462struct kmem_cache;
463#line 423
464struct perf_event;
465#line 423
466struct perf_event;
467#line 423
468struct perf_event;
469#line 423
470struct perf_event;
471#line 425 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/processor.h"
472struct thread_struct {
473 struct desc_struct tls_array[3] ;
474 unsigned long sp0 ;
475 unsigned long sp ;
476 unsigned long usersp ;
477 unsigned short es ;
478 unsigned short ds ;
479 unsigned short fsindex ;
480 unsigned short gsindex ;
481 unsigned long fs ;
482 unsigned long gs ;
483 struct perf_event *ptrace_bps[4] ;
484 unsigned long debugreg6 ;
485 unsigned long ptrace_dr7 ;
486 unsigned long cr2 ;
487 unsigned long trap_no ;
488 unsigned long error_code ;
489 struct fpu fpu ;
490 unsigned long *io_bitmap_ptr ;
491 unsigned long iopl ;
492 unsigned int io_bitmap_max ;
493};
494#line 23 "include/asm-generic/atomic-long.h"
495typedef atomic64_t atomic_long_t;
496#line 8 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/spinlock_types.h"
497struct arch_spinlock {
498 unsigned int slock ;
499};
500#line 8 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/spinlock_types.h"
501typedef struct arch_spinlock arch_spinlock_t;
502#line 14 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/spinlock_types.h"
503struct __anonstruct_arch_rwlock_t_36 {
504 unsigned int lock ;
505};
506#line 14 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/spinlock_types.h"
507typedef struct __anonstruct_arch_rwlock_t_36 arch_rwlock_t;
508#line 12 "include/linux/lockdep.h"
509struct task_struct;
510#line 13
511struct lockdep_map;
512#line 13
513struct lockdep_map;
514#line 13
515struct lockdep_map;
516#line 13
517struct lockdep_map;
518#line 8 "include/linux/debug_locks.h"
519struct task_struct;
520#line 48
521struct task_struct;
522#line 4 "include/linux/stacktrace.h"
523struct task_struct;
524#line 5
525struct pt_regs;
526#line 8
527struct task_struct;
528#line 10 "include/linux/stacktrace.h"
529struct stack_trace {
530 unsigned int nr_entries ;
531 unsigned int max_entries ;
532 unsigned long *entries ;
533 int skip ;
534};
535#line 50 "include/linux/lockdep.h"
536struct lockdep_subclass_key {
537 char __one_byte ;
538} __attribute__((__packed__)) ;
539#line 54 "include/linux/lockdep.h"
540struct lock_class_key {
541 struct lockdep_subclass_key subkeys[8UL] ;
542};
543#line 65 "include/linux/lockdep.h"
544struct lock_class {
545 struct list_head hash_entry ;
546 struct list_head lock_entry ;
547 struct lockdep_subclass_key *key ;
548 unsigned int subclass ;
549 unsigned int dep_gen_id ;
550 unsigned long usage_mask ;
551 struct stack_trace usage_traces[13] ;
552 struct list_head locks_after ;
553 struct list_head locks_before ;
554 unsigned int version ;
555 unsigned long ops ;
556 char const *name ;
557 int name_version ;
558 unsigned long contention_point[4] ;
559 unsigned long contending_point[4] ;
560};
561#line 150 "include/linux/lockdep.h"
562struct lockdep_map {
563 struct lock_class_key *key ;
564 struct lock_class *class_cache[2] ;
565 char const *name ;
566 int cpu ;
567 unsigned long ip ;
568};
569#line 196 "include/linux/lockdep.h"
570struct held_lock {
571 u64 prev_chain_key ;
572 unsigned long acquire_ip ;
573 struct lockdep_map *instance ;
574 struct lockdep_map *nest_lock ;
575 u64 waittime_stamp ;
576 u64 holdtime_stamp ;
577 unsigned int class_idx : 13 ;
578 unsigned int irq_context : 2 ;
579 unsigned int trylock : 1 ;
580 unsigned int read : 2 ;
581 unsigned int check : 2 ;
582 unsigned int hardirqs_off : 1 ;
583 unsigned int references : 11 ;
584};
585#line 20 "include/linux/spinlock_types.h"
586struct raw_spinlock {
587 arch_spinlock_t raw_lock ;
588 unsigned int magic ;
589 unsigned int owner_cpu ;
590 void *owner ;
591 struct lockdep_map dep_map ;
592};
593#line 20 "include/linux/spinlock_types.h"
594typedef struct raw_spinlock raw_spinlock_t;
595#line 64 "include/linux/spinlock_types.h"
596struct __anonstruct____missing_field_name_38 {
597 u8 __padding[(unsigned int )(& ((struct raw_spinlock *)0)->dep_map)] ;
598 struct lockdep_map dep_map ;
599};
600#line 64 "include/linux/spinlock_types.h"
601union __anonunion____missing_field_name_37 {
602 struct raw_spinlock rlock ;
603 struct __anonstruct____missing_field_name_38 __annonCompField17 ;
604};
605#line 64 "include/linux/spinlock_types.h"
606struct spinlock {
607 union __anonunion____missing_field_name_37 __annonCompField18 ;
608};
609#line 64 "include/linux/spinlock_types.h"
610typedef struct spinlock spinlock_t;
611#line 11 "include/linux/rwlock_types.h"
612struct __anonstruct_rwlock_t_39 {
613 arch_rwlock_t raw_lock ;
614 unsigned int magic ;
615 unsigned int owner_cpu ;
616 void *owner ;
617 struct lockdep_map dep_map ;
618};
619#line 11 "include/linux/rwlock_types.h"
620typedef struct __anonstruct_rwlock_t_39 rwlock_t;
621#line 50 "include/linux/wait.h"
622struct __wait_queue_head {
623 spinlock_t lock ;
624 struct list_head task_list ;
625};
626#line 54 "include/linux/wait.h"
627typedef struct __wait_queue_head wait_queue_head_t;
628#line 56
629struct task_struct;
630#line 119 "include/linux/seqlock.h"
631struct seqcount {
632 unsigned int sequence ;
633};
634#line 119 "include/linux/seqlock.h"
635typedef struct seqcount seqcount_t;
636#line 96 "include/linux/nodemask.h"
637struct __anonstruct_nodemask_t_41 {
638 unsigned long bits[(((unsigned long )(1 << 10) + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
639};
640#line 96 "include/linux/nodemask.h"
641typedef struct __anonstruct_nodemask_t_41 nodemask_t;
642#line 60 "include/linux/pageblock-flags.h"
643struct page;
644#line 48 "include/linux/mutex.h"
645struct mutex {
646 atomic_t count ;
647 spinlock_t wait_lock ;
648 struct list_head wait_list ;
649 struct task_struct *owner ;
650 char const *name ;
651 void *magic ;
652 struct lockdep_map dep_map ;
653};
654#line 69 "include/linux/mutex.h"
655struct mutex_waiter {
656 struct list_head list ;
657 struct task_struct *task ;
658 void *magic ;
659};
660#line 20 "include/linux/rwsem.h"
661struct rw_semaphore;
662#line 20
663struct rw_semaphore;
664#line 20
665struct rw_semaphore;
666#line 20
667struct rw_semaphore;
668#line 26 "include/linux/rwsem.h"
669struct rw_semaphore {
670 long count ;
671 spinlock_t wait_lock ;
672 struct list_head wait_list ;
673 struct lockdep_map dep_map ;
674};
675#line 8 "include/linux/memory_hotplug.h"
676struct page;
677#line 177 "include/linux/ioport.h"
678struct device;
679#line 177
680struct device;
681#line 177
682struct device;
683#line 177
684struct device;
685#line 103 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/mpspec.h"
686struct device;
687#line 14 "include/linux/time.h"
688struct timespec {
689 __kernel_time_t tv_sec ;
690 long tv_nsec ;
691};
692#line 46 "include/linux/ktime.h"
693union ktime {
694 s64 tv64 ;
695};
696#line 59 "include/linux/ktime.h"
697typedef union ktime ktime_t;
698#line 10 "include/linux/timer.h"
699struct tvec_base;
700#line 10
701struct tvec_base;
702#line 10
703struct tvec_base;
704#line 10
705struct tvec_base;
706#line 12 "include/linux/timer.h"
707struct timer_list {
708 struct list_head entry ;
709 unsigned long expires ;
710 struct tvec_base *base ;
711 void (*function)(unsigned long ) ;
712 unsigned long data ;
713 int slack ;
714 int start_pid ;
715 void *start_site ;
716 char start_comm[16] ;
717 struct lockdep_map lockdep_map ;
718};
719#line 289
720struct hrtimer;
721#line 289
722struct hrtimer;
723#line 289
724struct hrtimer;
725#line 289
726struct hrtimer;
727#line 290
728enum hrtimer_restart;
729#line 290
730enum hrtimer_restart;
731#line 290
732enum hrtimer_restart;
733#line 17 "include/linux/workqueue.h"
734struct work_struct;
735#line 17
736struct work_struct;
737#line 17
738struct work_struct;
739#line 17
740struct work_struct;
741#line 79 "include/linux/workqueue.h"
742struct work_struct {
743 atomic_long_t data ;
744 struct list_head entry ;
745 void (*func)(struct work_struct *work ) ;
746 struct lockdep_map lockdep_map ;
747};
748#line 92 "include/linux/workqueue.h"
749struct delayed_work {
750 struct work_struct work ;
751 struct timer_list timer ;
752};
753#line 25 "include/linux/completion.h"
754struct completion {
755 unsigned int done ;
756 wait_queue_head_t wait ;
757};
758#line 42 "include/linux/pm.h"
759struct device;
760#line 50 "include/linux/pm.h"
761struct pm_message {
762 int event ;
763};
764#line 50 "include/linux/pm.h"
765typedef struct pm_message pm_message_t;
766#line 204 "include/linux/pm.h"
767struct dev_pm_ops {
768 int (*prepare)(struct device *dev ) ;
769 void (*complete)(struct device *dev ) ;
770 int (*suspend)(struct device *dev ) ;
771 int (*resume)(struct device *dev ) ;
772 int (*freeze)(struct device *dev ) ;
773 int (*thaw)(struct device *dev ) ;
774 int (*poweroff)(struct device *dev ) ;
775 int (*restore)(struct device *dev ) ;
776 int (*suspend_noirq)(struct device *dev ) ;
777 int (*resume_noirq)(struct device *dev ) ;
778 int (*freeze_noirq)(struct device *dev ) ;
779 int (*thaw_noirq)(struct device *dev ) ;
780 int (*poweroff_noirq)(struct device *dev ) ;
781 int (*restore_noirq)(struct device *dev ) ;
782 int (*runtime_suspend)(struct device *dev ) ;
783 int (*runtime_resume)(struct device *dev ) ;
784 int (*runtime_idle)(struct device *dev ) ;
785};
786#line 392
787enum rpm_status {
788 RPM_ACTIVE = 0,
789 RPM_RESUMING = 1,
790 RPM_SUSPENDED = 2,
791 RPM_SUSPENDING = 3
792} ;
793#line 414
794enum rpm_request {
795 RPM_REQ_NONE = 0,
796 RPM_REQ_IDLE = 1,
797 RPM_REQ_SUSPEND = 2,
798 RPM_REQ_AUTOSUSPEND = 3,
799 RPM_REQ_RESUME = 4
800} ;
801#line 422
802struct wakeup_source;
803#line 422
804struct wakeup_source;
805#line 422
806struct wakeup_source;
807#line 422
808struct wakeup_source;
809#line 424 "include/linux/pm.h"
810struct dev_pm_info {
811 pm_message_t power_state ;
812 unsigned int can_wakeup : 1 ;
813 unsigned int async_suspend : 1 ;
814 bool is_prepared : 1 ;
815 bool is_suspended : 1 ;
816 spinlock_t lock ;
817 struct list_head entry ;
818 struct completion completion ;
819 struct wakeup_source *wakeup ;
820 struct timer_list suspend_timer ;
821 unsigned long timer_expires ;
822 struct work_struct work ;
823 wait_queue_head_t wait_queue ;
824 atomic_t usage_count ;
825 atomic_t child_count ;
826 unsigned int disable_depth : 3 ;
827 unsigned int ignore_children : 1 ;
828 unsigned int idle_notification : 1 ;
829 unsigned int request_pending : 1 ;
830 unsigned int deferred_resume : 1 ;
831 unsigned int run_wake : 1 ;
832 unsigned int runtime_auto : 1 ;
833 unsigned int no_callbacks : 1 ;
834 unsigned int irq_safe : 1 ;
835 unsigned int use_autosuspend : 1 ;
836 unsigned int timer_autosuspends : 1 ;
837 enum rpm_request request ;
838 enum rpm_status runtime_status ;
839 int runtime_error ;
840 int autosuspend_delay ;
841 unsigned long last_busy ;
842 unsigned long active_jiffies ;
843 unsigned long suspended_jiffies ;
844 unsigned long accounting_timestamp ;
845 void *subsys_data ;
846};
847#line 475 "include/linux/pm.h"
848struct dev_power_domain {
849 struct dev_pm_ops ops ;
850};
851#line 11 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/mmu.h"
852struct __anonstruct_mm_context_t_111 {
853 void *ldt ;
854 int size ;
855 unsigned short ia32_compat ;
856 struct mutex lock ;
857 void *vdso ;
858};
859#line 11 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/mmu.h"
860typedef struct __anonstruct_mm_context_t_111 mm_context_t;
861#line 8 "include/linux/vmalloc.h"
862struct vm_area_struct;
863#line 8
864struct vm_area_struct;
865#line 8
866struct vm_area_struct;
867#line 8
868struct vm_area_struct;
869#line 964 "include/linux/mmzone.h"
870struct page;
871#line 10 "include/linux/gfp.h"
872struct vm_area_struct;
873#line 20 "include/linux/kobject_ns.h"
874struct sock;
875#line 20
876struct sock;
877#line 20
878struct sock;
879#line 20
880struct sock;
881#line 21
882struct kobject;
883#line 21
884struct kobject;
885#line 21
886struct kobject;
887#line 21
888struct kobject;
889#line 27
890enum kobj_ns_type {
891 KOBJ_NS_TYPE_NONE = 0,
892 KOBJ_NS_TYPE_NET = 1,
893 KOBJ_NS_TYPES = 2
894} ;
895#line 40 "include/linux/kobject_ns.h"
896struct kobj_ns_type_operations {
897 enum kobj_ns_type type ;
898 void *(*grab_current_ns)(void) ;
899 void const *(*netlink_ns)(struct sock *sk ) ;
900 void const *(*initial_ns)(void) ;
901 void (*drop_ns)(void * ) ;
902};
903#line 22 "include/linux/sysfs.h"
904struct kobject;
905#line 23
906struct module;
907#line 24
908enum kobj_ns_type;
909#line 26 "include/linux/sysfs.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 56 "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 85
923struct file;
924#line 86
925struct vm_area_struct;
926#line 88 "include/linux/sysfs.h"
927struct bin_attribute {
928 struct attribute attr ;
929 size_t size ;
930 void *private ;
931 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
932 loff_t , size_t ) ;
933 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
934 loff_t , size_t ) ;
935 int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
936};
937#line 112 "include/linux/sysfs.h"
938struct sysfs_ops {
939 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
940 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
941};
942#line 117
943struct sysfs_dirent;
944#line 117
945struct sysfs_dirent;
946#line 117
947struct sysfs_dirent;
948#line 117
949struct sysfs_dirent;
950#line 20 "include/linux/kref.h"
951struct kref {
952 atomic_t refcount ;
953};
954#line 60 "include/linux/kobject.h"
955struct kset;
956#line 60
957struct kset;
958#line 60
959struct kset;
960#line 60
961struct kobj_type;
962#line 60
963struct kobj_type;
964#line 60
965struct kobj_type;
966#line 60 "include/linux/kobject.h"
967struct kobject {
968 char const *name ;
969 struct list_head entry ;
970 struct kobject *parent ;
971 struct kset *kset ;
972 struct kobj_type *ktype ;
973 struct sysfs_dirent *sd ;
974 struct kref kref ;
975 unsigned int state_initialized : 1 ;
976 unsigned int state_in_sysfs : 1 ;
977 unsigned int state_add_uevent_sent : 1 ;
978 unsigned int state_remove_uevent_sent : 1 ;
979 unsigned int uevent_suppress : 1 ;
980};
981#line 110 "include/linux/kobject.h"
982struct kobj_type {
983 void (*release)(struct kobject *kobj ) ;
984 struct sysfs_ops const *sysfs_ops ;
985 struct attribute **default_attrs ;
986 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
987 void const *(*namespace)(struct kobject *kobj ) ;
988};
989#line 118 "include/linux/kobject.h"
990struct kobj_uevent_env {
991 char *envp[32] ;
992 int envp_idx ;
993 char buf[2048] ;
994 int buflen ;
995};
996#line 125 "include/linux/kobject.h"
997struct kset_uevent_ops {
998 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
999 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
1000 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
1001};
1002#line 142
1003struct sock;
1004#line 161 "include/linux/kobject.h"
1005struct kset {
1006 struct list_head list ;
1007 spinlock_t list_lock ;
1008 struct kobject kobj ;
1009 struct kset_uevent_ops const *uevent_ops ;
1010};
1011#line 38 "include/linux/slub_def.h"
1012struct kmem_cache_cpu {
1013 void **freelist ;
1014 unsigned long tid ;
1015 struct page *page ;
1016 int node ;
1017 unsigned int stat[19] ;
1018};
1019#line 48 "include/linux/slub_def.h"
1020struct kmem_cache_node {
1021 spinlock_t list_lock ;
1022 unsigned long nr_partial ;
1023 struct list_head partial ;
1024 atomic_long_t nr_slabs ;
1025 atomic_long_t total_objects ;
1026 struct list_head full ;
1027};
1028#line 64 "include/linux/slub_def.h"
1029struct kmem_cache_order_objects {
1030 unsigned long x ;
1031};
1032#line 71 "include/linux/slub_def.h"
1033struct kmem_cache {
1034 struct kmem_cache_cpu *cpu_slab ;
1035 unsigned long flags ;
1036 unsigned long min_partial ;
1037 int size ;
1038 int objsize ;
1039 int offset ;
1040 struct kmem_cache_order_objects oo ;
1041 struct kmem_cache_order_objects max ;
1042 struct kmem_cache_order_objects min ;
1043 gfp_t allocflags ;
1044 int refcount ;
1045 void (*ctor)(void * ) ;
1046 int inuse ;
1047 int align ;
1048 int reserved ;
1049 char const *name ;
1050 struct list_head list ;
1051 struct kobject kobj ;
1052 int remote_node_defrag_ratio ;
1053 struct kmem_cache_node *node[1 << 10] ;
1054};
1055#line 62 "include/linux/stat.h"
1056struct kstat {
1057 u64 ino ;
1058 dev_t dev ;
1059 umode_t mode ;
1060 unsigned int nlink ;
1061 uid_t uid ;
1062 gid_t gid ;
1063 dev_t rdev ;
1064 loff_t size ;
1065 struct timespec atime ;
1066 struct timespec mtime ;
1067 struct timespec ctime ;
1068 unsigned long blksize ;
1069 unsigned long long blocks ;
1070};
1071#line 29 "include/linux/sysctl.h"
1072struct completion;
1073#line 72 "include/linux/rcupdate.h"
1074struct rcu_head {
1075 struct rcu_head *next ;
1076 void (*func)(struct rcu_head *head ) ;
1077};
1078#line 937 "include/linux/sysctl.h"
1079struct nsproxy;
1080#line 937
1081struct nsproxy;
1082#line 937
1083struct nsproxy;
1084#line 937
1085struct nsproxy;
1086#line 48 "include/linux/kmod.h"
1087struct cred;
1088#line 48
1089struct cred;
1090#line 48
1091struct cred;
1092#line 48
1093struct cred;
1094#line 49
1095struct file;
1096#line 264 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/elf.h"
1097struct task_struct;
1098#line 10 "include/linux/elf.h"
1099struct file;
1100#line 27 "include/linux/elf.h"
1101typedef __u64 Elf64_Addr;
1102#line 28 "include/linux/elf.h"
1103typedef __u16 Elf64_Half;
1104#line 32 "include/linux/elf.h"
1105typedef __u32 Elf64_Word;
1106#line 33 "include/linux/elf.h"
1107typedef __u64 Elf64_Xword;
1108#line 203 "include/linux/elf.h"
1109struct elf64_sym {
1110 Elf64_Word st_name ;
1111 unsigned char st_info ;
1112 unsigned char st_other ;
1113 Elf64_Half st_shndx ;
1114 Elf64_Addr st_value ;
1115 Elf64_Xword st_size ;
1116};
1117#line 203 "include/linux/elf.h"
1118typedef struct elf64_sym Elf64_Sym;
1119#line 34 "include/linux/moduleparam.h"
1120struct kernel_param;
1121#line 34
1122struct kernel_param;
1123#line 34
1124struct kernel_param;
1125#line 34
1126struct kernel_param;
1127#line 36 "include/linux/moduleparam.h"
1128struct kernel_param_ops {
1129 int (*set)(char const *val , struct kernel_param const *kp ) ;
1130 int (*get)(char *buffer , struct kernel_param const *kp ) ;
1131 void (*free)(void *arg ) ;
1132};
1133#line 48
1134struct kparam_string;
1135#line 48
1136struct kparam_string;
1137#line 48
1138struct kparam_string;
1139#line 48
1140struct kparam_array;
1141#line 48
1142struct kparam_array;
1143#line 48
1144struct kparam_array;
1145#line 48 "include/linux/moduleparam.h"
1146union __anonunion____missing_field_name_195 {
1147 void *arg ;
1148 struct kparam_string const *str ;
1149 struct kparam_array const *arr ;
1150};
1151#line 48 "include/linux/moduleparam.h"
1152struct kernel_param {
1153 char const *name ;
1154 struct kernel_param_ops const *ops ;
1155 u16 perm ;
1156 u16 flags ;
1157 union __anonunion____missing_field_name_195 __annonCompField31 ;
1158};
1159#line 61 "include/linux/moduleparam.h"
1160struct kparam_string {
1161 unsigned int maxlen ;
1162 char *string ;
1163};
1164#line 67 "include/linux/moduleparam.h"
1165struct kparam_array {
1166 unsigned int max ;
1167 unsigned int elemsize ;
1168 unsigned int *num ;
1169 struct kernel_param_ops const *ops ;
1170 void *elem ;
1171};
1172#line 391
1173struct module;
1174#line 26 "include/linux/jump_label.h"
1175struct module;
1176#line 61 "include/linux/jump_label.h"
1177struct jump_label_key {
1178 atomic_t enabled ;
1179};
1180#line 22 "include/linux/tracepoint.h"
1181struct module;
1182#line 23
1183struct tracepoint;
1184#line 23
1185struct tracepoint;
1186#line 23
1187struct tracepoint;
1188#line 23
1189struct tracepoint;
1190#line 25 "include/linux/tracepoint.h"
1191struct tracepoint_func {
1192 void *func ;
1193 void *data ;
1194};
1195#line 30 "include/linux/tracepoint.h"
1196struct tracepoint {
1197 char const *name ;
1198 struct jump_label_key key ;
1199 void (*regfunc)(void) ;
1200 void (*unregfunc)(void) ;
1201 struct tracepoint_func *funcs ;
1202};
1203#line 8 "include/asm-generic/module.h"
1204struct mod_arch_specific {
1205
1206};
1207#line 21 "include/trace/events/module.h"
1208struct module;
1209#line 37 "include/linux/module.h"
1210struct kernel_symbol {
1211 unsigned long value ;
1212 char const *name ;
1213};
1214#line 49
1215struct module;
1216#line 51 "include/linux/module.h"
1217struct module_attribute {
1218 struct attribute attr ;
1219 ssize_t (*show)(struct module_attribute * , struct module * , char * ) ;
1220 ssize_t (*store)(struct module_attribute * , struct module * , char const * ,
1221 size_t count ) ;
1222 void (*setup)(struct module * , char const * ) ;
1223 int (*test)(struct module * ) ;
1224 void (*free)(struct module * ) ;
1225};
1226#line 70
1227struct module_param_attrs;
1228#line 70
1229struct module_param_attrs;
1230#line 70
1231struct module_param_attrs;
1232#line 70 "include/linux/module.h"
1233struct module_kobject {
1234 struct kobject kobj ;
1235 struct module *mod ;
1236 struct kobject *drivers_dir ;
1237 struct module_param_attrs *mp ;
1238};
1239#line 83
1240struct exception_table_entry;
1241#line 83
1242struct exception_table_entry;
1243#line 83
1244struct exception_table_entry;
1245#line 83
1246struct exception_table_entry;
1247#line 265
1248enum module_state {
1249 MODULE_STATE_LIVE = 0,
1250 MODULE_STATE_COMING = 1,
1251 MODULE_STATE_GOING = 2
1252} ;
1253#line 272
1254struct module_sect_attrs;
1255#line 272
1256struct module_sect_attrs;
1257#line 272
1258struct module_sect_attrs;
1259#line 272
1260struct module_notes_attrs;
1261#line 272
1262struct module_notes_attrs;
1263#line 272
1264struct module_notes_attrs;
1265#line 272
1266struct ftrace_event_call;
1267#line 272
1268struct ftrace_event_call;
1269#line 272
1270struct ftrace_event_call;
1271#line 272 "include/linux/module.h"
1272struct module_ref {
1273 unsigned int incs ;
1274 unsigned int decs ;
1275};
1276#line 272 "include/linux/module.h"
1277struct module {
1278 enum module_state state ;
1279 struct list_head list ;
1280 char name[64UL - sizeof(unsigned long )] ;
1281 struct module_kobject mkobj ;
1282 struct module_attribute *modinfo_attrs ;
1283 char const *version ;
1284 char const *srcversion ;
1285 struct kobject *holders_dir ;
1286 struct kernel_symbol const *syms ;
1287 unsigned long const *crcs ;
1288 unsigned int num_syms ;
1289 struct kernel_param *kp ;
1290 unsigned int num_kp ;
1291 unsigned int num_gpl_syms ;
1292 struct kernel_symbol const *gpl_syms ;
1293 unsigned long const *gpl_crcs ;
1294 struct kernel_symbol const *unused_syms ;
1295 unsigned long const *unused_crcs ;
1296 unsigned int num_unused_syms ;
1297 unsigned int num_unused_gpl_syms ;
1298 struct kernel_symbol const *unused_gpl_syms ;
1299 unsigned long const *unused_gpl_crcs ;
1300 struct kernel_symbol const *gpl_future_syms ;
1301 unsigned long const *gpl_future_crcs ;
1302 unsigned int num_gpl_future_syms ;
1303 unsigned int num_exentries ;
1304 struct exception_table_entry *extable ;
1305 int (*init)(void) ;
1306 void *module_init ;
1307 void *module_core ;
1308 unsigned int init_size ;
1309 unsigned int core_size ;
1310 unsigned int init_text_size ;
1311 unsigned int core_text_size ;
1312 unsigned int init_ro_size ;
1313 unsigned int core_ro_size ;
1314 struct mod_arch_specific arch ;
1315 unsigned int taints ;
1316 unsigned int num_bugs ;
1317 struct list_head bug_list ;
1318 struct bug_entry *bug_table ;
1319 Elf64_Sym *symtab ;
1320 Elf64_Sym *core_symtab ;
1321 unsigned int num_symtab ;
1322 unsigned int core_num_syms ;
1323 char *strtab ;
1324 char *core_strtab ;
1325 struct module_sect_attrs *sect_attrs ;
1326 struct module_notes_attrs *notes_attrs ;
1327 char *args ;
1328 void *percpu ;
1329 unsigned int percpu_size ;
1330 unsigned int num_tracepoints ;
1331 struct tracepoint * const *tracepoints_ptrs ;
1332 unsigned int num_trace_bprintk_fmt ;
1333 char const **trace_bprintk_fmt_start ;
1334 struct ftrace_event_call **trace_events ;
1335 unsigned int num_trace_events ;
1336 unsigned int num_ftrace_callsites ;
1337 unsigned long *ftrace_callsites ;
1338 struct list_head source_list ;
1339 struct list_head target_list ;
1340 struct task_struct *waiter ;
1341 void (*exit)(void) ;
1342 struct module_ref *refptr ;
1343 ctor_fn_t *ctors ;
1344 unsigned int num_ctors ;
1345};
1346#line 12 "include/linux/mod_devicetable.h"
1347typedef unsigned long kernel_ulong_t;
1348#line 98 "include/linux/mod_devicetable.h"
1349struct usb_device_id {
1350 __u16 match_flags ;
1351 __u16 idVendor ;
1352 __u16 idProduct ;
1353 __u16 bcdDevice_lo ;
1354 __u16 bcdDevice_hi ;
1355 __u8 bDeviceClass ;
1356 __u8 bDeviceSubClass ;
1357 __u8 bDeviceProtocol ;
1358 __u8 bInterfaceClass ;
1359 __u8 bInterfaceSubClass ;
1360 __u8 bInterfaceProtocol ;
1361 kernel_ulong_t driver_info ;
1362};
1363#line 219 "include/linux/mod_devicetable.h"
1364struct of_device_id {
1365 char name[32] ;
1366 char type[32] ;
1367 char compatible[128] ;
1368 void *data ;
1369};
1370#line 312 "include/linux/mod_devicetable.h"
1371struct input_device_id {
1372 kernel_ulong_t flags ;
1373 __u16 bustype ;
1374 __u16 vendor ;
1375 __u16 product ;
1376 __u16 version ;
1377 kernel_ulong_t evbit[1] ;
1378 kernel_ulong_t keybit[12] ;
1379 kernel_ulong_t relbit[1] ;
1380 kernel_ulong_t absbit[1] ;
1381 kernel_ulong_t mscbit[1] ;
1382 kernel_ulong_t ledbit[1] ;
1383 kernel_ulong_t sndbit[1] ;
1384 kernel_ulong_t ffbit[2] ;
1385 kernel_ulong_t swbit[1] ;
1386 kernel_ulong_t driver_info ;
1387};
1388#line 244 "include/linux/usb/ch9.h"
1389struct usb_device_descriptor {
1390 __u8 bLength ;
1391 __u8 bDescriptorType ;
1392 __le16 bcdUSB ;
1393 __u8 bDeviceClass ;
1394 __u8 bDeviceSubClass ;
1395 __u8 bDeviceProtocol ;
1396 __u8 bMaxPacketSize0 ;
1397 __le16 idVendor ;
1398 __le16 idProduct ;
1399 __le16 bcdDevice ;
1400 __u8 iManufacturer ;
1401 __u8 iProduct ;
1402 __u8 iSerialNumber ;
1403 __u8 bNumConfigurations ;
1404} __attribute__((__packed__)) ;
1405#line 300 "include/linux/usb/ch9.h"
1406struct usb_config_descriptor {
1407 __u8 bLength ;
1408 __u8 bDescriptorType ;
1409 __le16 wTotalLength ;
1410 __u8 bNumInterfaces ;
1411 __u8 bConfigurationValue ;
1412 __u8 iConfiguration ;
1413 __u8 bmAttributes ;
1414 __u8 bMaxPower ;
1415} __attribute__((__packed__)) ;
1416#line 337 "include/linux/usb/ch9.h"
1417struct usb_interface_descriptor {
1418 __u8 bLength ;
1419 __u8 bDescriptorType ;
1420 __u8 bInterfaceNumber ;
1421 __u8 bAlternateSetting ;
1422 __u8 bNumEndpoints ;
1423 __u8 bInterfaceClass ;
1424 __u8 bInterfaceSubClass ;
1425 __u8 bInterfaceProtocol ;
1426 __u8 iInterface ;
1427} __attribute__((__packed__)) ;
1428#line 355 "include/linux/usb/ch9.h"
1429struct usb_endpoint_descriptor {
1430 __u8 bLength ;
1431 __u8 bDescriptorType ;
1432 __u8 bEndpointAddress ;
1433 __u8 bmAttributes ;
1434 __le16 wMaxPacketSize ;
1435 __u8 bInterval ;
1436 __u8 bRefresh ;
1437 __u8 bSynchAddress ;
1438} __attribute__((__packed__)) ;
1439#line 576 "include/linux/usb/ch9.h"
1440struct usb_ss_ep_comp_descriptor {
1441 __u8 bLength ;
1442 __u8 bDescriptorType ;
1443 __u8 bMaxBurst ;
1444 __u8 bmAttributes ;
1445 __le16 wBytesPerInterval ;
1446} __attribute__((__packed__)) ;
1447#line 637 "include/linux/usb/ch9.h"
1448struct usb_interface_assoc_descriptor {
1449 __u8 bLength ;
1450 __u8 bDescriptorType ;
1451 __u8 bFirstInterface ;
1452 __u8 bInterfaceCount ;
1453 __u8 bFunctionClass ;
1454 __u8 bFunctionSubClass ;
1455 __u8 bFunctionProtocol ;
1456 __u8 iFunction ;
1457} __attribute__((__packed__)) ;
1458#line 846
1459enum usb_device_speed {
1460 USB_SPEED_UNKNOWN = 0,
1461 USB_SPEED_LOW = 1,
1462 USB_SPEED_FULL = 2,
1463 USB_SPEED_HIGH = 3,
1464 USB_SPEED_WIRELESS = 4,
1465 USB_SPEED_SUPER = 5
1466} ;
1467#line 854
1468enum usb_device_state {
1469 USB_STATE_NOTATTACHED = 0,
1470 USB_STATE_ATTACHED = 1,
1471 USB_STATE_POWERED = 2,
1472 USB_STATE_RECONNECTING = 3,
1473 USB_STATE_UNAUTHENTICATED = 4,
1474 USB_STATE_DEFAULT = 5,
1475 USB_STATE_ADDRESS = 6,
1476 USB_STATE_CONFIGURED = 7,
1477 USB_STATE_SUSPENDED = 8
1478} ;
1479#line 10 "include/linux/irqreturn.h"
1480enum irqreturn {
1481 IRQ_NONE = 0,
1482 IRQ_HANDLED = 1,
1483 IRQ_WAKE_THREAD = 2
1484} ;
1485#line 16 "include/linux/irqreturn.h"
1486typedef enum irqreturn irqreturn_t;
1487#line 31 "include/linux/irq.h"
1488struct seq_file;
1489#line 12 "include/linux/irqdesc.h"
1490struct proc_dir_entry;
1491#line 12
1492struct proc_dir_entry;
1493#line 12
1494struct proc_dir_entry;
1495#line 12
1496struct proc_dir_entry;
1497#line 39
1498struct irqaction;
1499#line 39
1500struct irqaction;
1501#line 39
1502struct irqaction;
1503#line 16 "include/linux/profile.h"
1504struct proc_dir_entry;
1505#line 17
1506struct pt_regs;
1507#line 65
1508struct task_struct;
1509#line 66
1510struct mm_struct;
1511#line 88
1512struct pt_regs;
1513#line 94 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/uaccess.h"
1514struct exception_table_entry {
1515 unsigned long insn ;
1516 unsigned long fixup ;
1517};
1518#line 363 "include/linux/irq.h"
1519struct irqaction;
1520#line 132 "include/linux/hardirq.h"
1521struct task_struct;
1522#line 100 "include/linux/rbtree.h"
1523struct rb_node {
1524 unsigned long rb_parent_color ;
1525 struct rb_node *rb_right ;
1526 struct rb_node *rb_left ;
1527} __attribute__((__aligned__(sizeof(long )))) ;
1528#line 110 "include/linux/rbtree.h"
1529struct rb_root {
1530 struct rb_node *rb_node ;
1531};
1532#line 8 "include/linux/timerqueue.h"
1533struct timerqueue_node {
1534 struct rb_node node ;
1535 ktime_t expires ;
1536};
1537#line 13 "include/linux/timerqueue.h"
1538struct timerqueue_head {
1539 struct rb_root head ;
1540 struct timerqueue_node *next ;
1541};
1542#line 27 "include/linux/hrtimer.h"
1543struct hrtimer_clock_base;
1544#line 27
1545struct hrtimer_clock_base;
1546#line 27
1547struct hrtimer_clock_base;
1548#line 27
1549struct hrtimer_clock_base;
1550#line 28
1551struct hrtimer_cpu_base;
1552#line 28
1553struct hrtimer_cpu_base;
1554#line 28
1555struct hrtimer_cpu_base;
1556#line 28
1557struct hrtimer_cpu_base;
1558#line 44
1559enum hrtimer_restart {
1560 HRTIMER_NORESTART = 0,
1561 HRTIMER_RESTART = 1
1562} ;
1563#line 108 "include/linux/hrtimer.h"
1564struct hrtimer {
1565 struct timerqueue_node node ;
1566 ktime_t _softexpires ;
1567 enum hrtimer_restart (*function)(struct hrtimer * ) ;
1568 struct hrtimer_clock_base *base ;
1569 unsigned long state ;
1570 int start_pid ;
1571 void *start_site ;
1572 char start_comm[16] ;
1573};
1574#line 145 "include/linux/hrtimer.h"
1575struct hrtimer_clock_base {
1576 struct hrtimer_cpu_base *cpu_base ;
1577 int index ;
1578 clockid_t clockid ;
1579 struct timerqueue_head active ;
1580 ktime_t resolution ;
1581 ktime_t (*get_time)(void) ;
1582 ktime_t softirq_time ;
1583 ktime_t offset ;
1584};
1585#line 178 "include/linux/hrtimer.h"
1586struct hrtimer_cpu_base {
1587 raw_spinlock_t lock ;
1588 unsigned long active_bases ;
1589 ktime_t expires_next ;
1590 int hres_active ;
1591 int hang_detected ;
1592 unsigned long nr_events ;
1593 unsigned long nr_retries ;
1594 unsigned long nr_hangs ;
1595 ktime_t max_hang_time ;
1596 struct hrtimer_clock_base clock_base[3] ;
1597};
1598#line 9 "include/trace/events/irq.h"
1599struct irqaction;
1600#line 106 "include/linux/interrupt.h"
1601struct irqaction {
1602 irqreturn_t (*handler)(int , void * ) ;
1603 unsigned long flags ;
1604 void *dev_id ;
1605 struct irqaction *next ;
1606 int irq ;
1607 irqreturn_t (*thread_fn)(int , void * ) ;
1608 struct task_struct *thread ;
1609 unsigned long thread_flags ;
1610 unsigned long thread_mask ;
1611 char const *name ;
1612 struct proc_dir_entry *dir ;
1613} __attribute__((__aligned__((1) << (12) ))) ;
1614#line 172
1615struct device;
1616#line 682
1617struct seq_file;
1618#line 19 "include/linux/klist.h"
1619struct klist_node;
1620#line 19
1621struct klist_node;
1622#line 19
1623struct klist_node;
1624#line 19
1625struct klist_node;
1626#line 39 "include/linux/klist.h"
1627struct klist_node {
1628 void *n_klist ;
1629 struct list_head n_node ;
1630 struct kref n_ref ;
1631};
1632#line 4 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/device.h"
1633struct dma_map_ops;
1634#line 4
1635struct dma_map_ops;
1636#line 4
1637struct dma_map_ops;
1638#line 4 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/device.h"
1639struct dev_archdata {
1640 void *acpi_handle ;
1641 struct dma_map_ops *dma_ops ;
1642 void *iommu ;
1643};
1644#line 28 "include/linux/device.h"
1645struct device;
1646#line 29
1647struct device_private;
1648#line 29
1649struct device_private;
1650#line 29
1651struct device_private;
1652#line 29
1653struct device_private;
1654#line 30
1655struct device_driver;
1656#line 30
1657struct device_driver;
1658#line 30
1659struct device_driver;
1660#line 30
1661struct device_driver;
1662#line 31
1663struct driver_private;
1664#line 31
1665struct driver_private;
1666#line 31
1667struct driver_private;
1668#line 31
1669struct driver_private;
1670#line 32
1671struct class;
1672#line 32
1673struct class;
1674#line 32
1675struct class;
1676#line 32
1677struct class;
1678#line 33
1679struct subsys_private;
1680#line 33
1681struct subsys_private;
1682#line 33
1683struct subsys_private;
1684#line 33
1685struct subsys_private;
1686#line 34
1687struct bus_type;
1688#line 34
1689struct bus_type;
1690#line 34
1691struct bus_type;
1692#line 34
1693struct bus_type;
1694#line 35
1695struct device_node;
1696#line 35
1697struct device_node;
1698#line 35
1699struct device_node;
1700#line 35
1701struct device_node;
1702#line 37 "include/linux/device.h"
1703struct bus_attribute {
1704 struct attribute attr ;
1705 ssize_t (*show)(struct bus_type *bus , char *buf ) ;
1706 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ;
1707};
1708#line 82
1709struct device_attribute;
1710#line 82
1711struct device_attribute;
1712#line 82
1713struct device_attribute;
1714#line 82
1715struct driver_attribute;
1716#line 82
1717struct driver_attribute;
1718#line 82
1719struct driver_attribute;
1720#line 82 "include/linux/device.h"
1721struct bus_type {
1722 char const *name ;
1723 struct bus_attribute *bus_attrs ;
1724 struct device_attribute *dev_attrs ;
1725 struct driver_attribute *drv_attrs ;
1726 int (*match)(struct device *dev , struct device_driver *drv ) ;
1727 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1728 int (*probe)(struct device *dev ) ;
1729 int (*remove)(struct device *dev ) ;
1730 void (*shutdown)(struct device *dev ) ;
1731 int (*suspend)(struct device *dev , pm_message_t state ) ;
1732 int (*resume)(struct device *dev ) ;
1733 struct dev_pm_ops const *pm ;
1734 struct subsys_private *p ;
1735};
1736#line 185 "include/linux/device.h"
1737struct device_driver {
1738 char const *name ;
1739 struct bus_type *bus ;
1740 struct module *owner ;
1741 char const *mod_name ;
1742 bool suppress_bind_attrs ;
1743 struct of_device_id const *of_match_table ;
1744 int (*probe)(struct device *dev ) ;
1745 int (*remove)(struct device *dev ) ;
1746 void (*shutdown)(struct device *dev ) ;
1747 int (*suspend)(struct device *dev , pm_message_t state ) ;
1748 int (*resume)(struct device *dev ) ;
1749 struct attribute_group const **groups ;
1750 struct dev_pm_ops const *pm ;
1751 struct driver_private *p ;
1752};
1753#line 222 "include/linux/device.h"
1754struct driver_attribute {
1755 struct attribute attr ;
1756 ssize_t (*show)(struct device_driver *driver , char *buf ) ;
1757 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ;
1758};
1759#line 280
1760struct class_attribute;
1761#line 280
1762struct class_attribute;
1763#line 280
1764struct class_attribute;
1765#line 280 "include/linux/device.h"
1766struct class {
1767 char const *name ;
1768 struct module *owner ;
1769 struct class_attribute *class_attrs ;
1770 struct device_attribute *dev_attrs ;
1771 struct bin_attribute *dev_bin_attrs ;
1772 struct kobject *dev_kobj ;
1773 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1774 char *(*devnode)(struct device *dev , mode_t *mode ) ;
1775 void (*class_release)(struct class *class ) ;
1776 void (*dev_release)(struct device *dev ) ;
1777 int (*suspend)(struct device *dev , pm_message_t state ) ;
1778 int (*resume)(struct device *dev ) ;
1779 struct kobj_ns_type_operations const *ns_type ;
1780 void const *(*namespace)(struct device *dev ) ;
1781 struct dev_pm_ops const *pm ;
1782 struct subsys_private *p ;
1783};
1784#line 306
1785struct device_type;
1786#line 306
1787struct device_type;
1788#line 306
1789struct device_type;
1790#line 347 "include/linux/device.h"
1791struct class_attribute {
1792 struct attribute attr ;
1793 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
1794 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf ,
1795 size_t count ) ;
1796};
1797#line 413 "include/linux/device.h"
1798struct device_type {
1799 char const *name ;
1800 struct attribute_group const **groups ;
1801 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1802 char *(*devnode)(struct device *dev , mode_t *mode ) ;
1803 void (*release)(struct device *dev ) ;
1804 struct dev_pm_ops const *pm ;
1805};
1806#line 424 "include/linux/device.h"
1807struct device_attribute {
1808 struct attribute attr ;
1809 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
1810 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf ,
1811 size_t count ) ;
1812};
1813#line 484 "include/linux/device.h"
1814struct device_dma_parameters {
1815 unsigned int max_segment_size ;
1816 unsigned long segment_boundary_mask ;
1817};
1818#line 551
1819struct dma_coherent_mem;
1820#line 551
1821struct dma_coherent_mem;
1822#line 551
1823struct dma_coherent_mem;
1824#line 551 "include/linux/device.h"
1825struct device {
1826 struct device *parent ;
1827 struct device_private *p ;
1828 struct kobject kobj ;
1829 char const *init_name ;
1830 struct device_type const *type ;
1831 struct mutex mutex ;
1832 struct bus_type *bus ;
1833 struct device_driver *driver ;
1834 void *platform_data ;
1835 struct dev_pm_info power ;
1836 struct dev_power_domain *pwr_domain ;
1837 int numa_node ;
1838 u64 *dma_mask ;
1839 u64 coherent_dma_mask ;
1840 struct device_dma_parameters *dma_parms ;
1841 struct list_head dma_pools ;
1842 struct dma_coherent_mem *dma_mem ;
1843 struct dev_archdata archdata ;
1844 struct device_node *of_node ;
1845 dev_t devt ;
1846 spinlock_t devres_lock ;
1847 struct list_head devres_head ;
1848 struct klist_node knode_class ;
1849 struct class *class ;
1850 struct attribute_group const **groups ;
1851 void (*release)(struct device *dev ) ;
1852};
1853#line 43 "include/linux/pm_wakeup.h"
1854struct wakeup_source {
1855 char *name ;
1856 struct list_head entry ;
1857 spinlock_t lock ;
1858 struct timer_list timer ;
1859 unsigned long timer_expires ;
1860 ktime_t total_time ;
1861 ktime_t max_time ;
1862 ktime_t last_time ;
1863 unsigned long event_count ;
1864 unsigned long active_count ;
1865 unsigned long relax_count ;
1866 unsigned long hit_count ;
1867 unsigned int active : 1 ;
1868};
1869#line 15 "include/linux/blk_types.h"
1870struct page;
1871#line 16
1872struct block_device;
1873#line 16
1874struct block_device;
1875#line 16
1876struct block_device;
1877#line 16
1878struct block_device;
1879#line 33 "include/linux/list_bl.h"
1880struct hlist_bl_node;
1881#line 33
1882struct hlist_bl_node;
1883#line 33
1884struct hlist_bl_node;
1885#line 33 "include/linux/list_bl.h"
1886struct hlist_bl_head {
1887 struct hlist_bl_node *first ;
1888};
1889#line 37 "include/linux/list_bl.h"
1890struct hlist_bl_node {
1891 struct hlist_bl_node *next ;
1892 struct hlist_bl_node **pprev ;
1893};
1894#line 13 "include/linux/dcache.h"
1895struct nameidata;
1896#line 13
1897struct nameidata;
1898#line 13
1899struct nameidata;
1900#line 13
1901struct nameidata;
1902#line 14
1903struct path;
1904#line 14
1905struct path;
1906#line 14
1907struct path;
1908#line 14
1909struct path;
1910#line 15
1911struct vfsmount;
1912#line 15
1913struct vfsmount;
1914#line 15
1915struct vfsmount;
1916#line 15
1917struct vfsmount;
1918#line 35 "include/linux/dcache.h"
1919struct qstr {
1920 unsigned int hash ;
1921 unsigned int len ;
1922 unsigned char const *name ;
1923};
1924#line 116
1925struct inode;
1926#line 116
1927struct inode;
1928#line 116
1929struct inode;
1930#line 116
1931struct dentry_operations;
1932#line 116
1933struct dentry_operations;
1934#line 116
1935struct dentry_operations;
1936#line 116
1937struct super_block;
1938#line 116
1939struct super_block;
1940#line 116
1941struct super_block;
1942#line 116 "include/linux/dcache.h"
1943union __anonunion_d_u_206 {
1944 struct list_head d_child ;
1945 struct rcu_head d_rcu ;
1946};
1947#line 116 "include/linux/dcache.h"
1948struct dentry {
1949 unsigned int d_flags ;
1950 seqcount_t d_seq ;
1951 struct hlist_bl_node d_hash ;
1952 struct dentry *d_parent ;
1953 struct qstr d_name ;
1954 struct inode *d_inode ;
1955 unsigned char d_iname[32] ;
1956 unsigned int d_count ;
1957 spinlock_t d_lock ;
1958 struct dentry_operations const *d_op ;
1959 struct super_block *d_sb ;
1960 unsigned long d_time ;
1961 void *d_fsdata ;
1962 struct list_head d_lru ;
1963 union __anonunion_d_u_206 d_u ;
1964 struct list_head d_subdirs ;
1965 struct list_head d_alias ;
1966};
1967#line 159 "include/linux/dcache.h"
1968struct dentry_operations {
1969 int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1970 int (*d_hash)(struct dentry const * , struct inode const * , struct qstr * ) ;
1971 int (*d_compare)(struct dentry const * , struct inode const * , struct dentry const * ,
1972 struct inode const * , unsigned int , char const * , struct qstr const * ) ;
1973 int (*d_delete)(struct dentry const * ) ;
1974 void (*d_release)(struct dentry * ) ;
1975 void (*d_iput)(struct dentry * , struct inode * ) ;
1976 char *(*d_dname)(struct dentry * , char * , int ) ;
1977 struct vfsmount *(*d_automount)(struct path * ) ;
1978 int (*d_manage)(struct dentry * , bool ) ;
1979} __attribute__((__aligned__((1) << (6) ))) ;
1980#line 4 "include/linux/path.h"
1981struct dentry;
1982#line 5
1983struct vfsmount;
1984#line 7 "include/linux/path.h"
1985struct path {
1986 struct vfsmount *mnt ;
1987 struct dentry *dentry ;
1988};
1989#line 57 "include/linux/radix-tree.h"
1990struct radix_tree_node;
1991#line 57
1992struct radix_tree_node;
1993#line 57
1994struct radix_tree_node;
1995#line 57 "include/linux/radix-tree.h"
1996struct radix_tree_root {
1997 unsigned int height ;
1998 gfp_t gfp_mask ;
1999 struct radix_tree_node *rnode ;
2000};
2001#line 14 "include/linux/prio_tree.h"
2002struct prio_tree_node;
2003#line 14
2004struct prio_tree_node;
2005#line 14
2006struct prio_tree_node;
2007#line 14 "include/linux/prio_tree.h"
2008struct raw_prio_tree_node {
2009 struct prio_tree_node *left ;
2010 struct prio_tree_node *right ;
2011 struct prio_tree_node *parent ;
2012};
2013#line 20 "include/linux/prio_tree.h"
2014struct prio_tree_node {
2015 struct prio_tree_node *left ;
2016 struct prio_tree_node *right ;
2017 struct prio_tree_node *parent ;
2018 unsigned long start ;
2019 unsigned long last ;
2020};
2021#line 28 "include/linux/prio_tree.h"
2022struct prio_tree_root {
2023 struct prio_tree_node *prio_tree_node ;
2024 unsigned short index_bits ;
2025 unsigned short raw ;
2026};
2027#line 6 "include/linux/pid.h"
2028enum pid_type {
2029 PIDTYPE_PID = 0,
2030 PIDTYPE_PGID = 1,
2031 PIDTYPE_SID = 2,
2032 PIDTYPE_MAX = 3
2033} ;
2034#line 50
2035struct pid_namespace;
2036#line 50
2037struct pid_namespace;
2038#line 50
2039struct pid_namespace;
2040#line 50 "include/linux/pid.h"
2041struct upid {
2042 int nr ;
2043 struct pid_namespace *ns ;
2044 struct hlist_node pid_chain ;
2045};
2046#line 57 "include/linux/pid.h"
2047struct pid {
2048 atomic_t count ;
2049 unsigned int level ;
2050 struct hlist_head tasks[3] ;
2051 struct rcu_head rcu ;
2052 struct upid numbers[1] ;
2053};
2054#line 69 "include/linux/pid.h"
2055struct pid_link {
2056 struct hlist_node node ;
2057 struct pid *pid ;
2058};
2059#line 100
2060struct pid_namespace;
2061#line 18 "include/linux/capability.h"
2062struct task_struct;
2063#line 94 "include/linux/capability.h"
2064struct kernel_cap_struct {
2065 __u32 cap[2] ;
2066};
2067#line 94 "include/linux/capability.h"
2068typedef struct kernel_cap_struct kernel_cap_t;
2069#line 376
2070struct dentry;
2071#line 377
2072struct user_namespace;
2073#line 377
2074struct user_namespace;
2075#line 377
2076struct user_namespace;
2077#line 377
2078struct user_namespace;
2079#line 16 "include/linux/fiemap.h"
2080struct fiemap_extent {
2081 __u64 fe_logical ;
2082 __u64 fe_physical ;
2083 __u64 fe_length ;
2084 __u64 fe_reserved64[2] ;
2085 __u32 fe_flags ;
2086 __u32 fe_reserved[3] ;
2087};
2088#line 399 "include/linux/fs.h"
2089struct export_operations;
2090#line 399
2091struct export_operations;
2092#line 399
2093struct export_operations;
2094#line 399
2095struct export_operations;
2096#line 401
2097struct iovec;
2098#line 401
2099struct iovec;
2100#line 401
2101struct iovec;
2102#line 401
2103struct iovec;
2104#line 402
2105struct nameidata;
2106#line 403
2107struct kiocb;
2108#line 403
2109struct kiocb;
2110#line 403
2111struct kiocb;
2112#line 403
2113struct kiocb;
2114#line 404
2115struct kobject;
2116#line 405
2117struct pipe_inode_info;
2118#line 405
2119struct pipe_inode_info;
2120#line 405
2121struct pipe_inode_info;
2122#line 405
2123struct pipe_inode_info;
2124#line 406
2125struct poll_table_struct;
2126#line 406
2127struct poll_table_struct;
2128#line 406
2129struct poll_table_struct;
2130#line 406
2131struct poll_table_struct;
2132#line 407
2133struct kstatfs;
2134#line 407
2135struct kstatfs;
2136#line 407
2137struct kstatfs;
2138#line 407
2139struct kstatfs;
2140#line 408
2141struct vm_area_struct;
2142#line 409
2143struct vfsmount;
2144#line 410
2145struct cred;
2146#line 460 "include/linux/fs.h"
2147struct iattr {
2148 unsigned int ia_valid ;
2149 umode_t ia_mode ;
2150 uid_t ia_uid ;
2151 gid_t ia_gid ;
2152 loff_t ia_size ;
2153 struct timespec ia_atime ;
2154 struct timespec ia_mtime ;
2155 struct timespec ia_ctime ;
2156 struct file *ia_file ;
2157};
2158#line 129 "include/linux/quota.h"
2159struct if_dqinfo {
2160 __u64 dqi_bgrace ;
2161 __u64 dqi_igrace ;
2162 __u32 dqi_flags ;
2163 __u32 dqi_valid ;
2164};
2165#line 50 "include/linux/dqblk_xfs.h"
2166struct fs_disk_quota {
2167 __s8 d_version ;
2168 __s8 d_flags ;
2169 __u16 d_fieldmask ;
2170 __u32 d_id ;
2171 __u64 d_blk_hardlimit ;
2172 __u64 d_blk_softlimit ;
2173 __u64 d_ino_hardlimit ;
2174 __u64 d_ino_softlimit ;
2175 __u64 d_bcount ;
2176 __u64 d_icount ;
2177 __s32 d_itimer ;
2178 __s32 d_btimer ;
2179 __u16 d_iwarns ;
2180 __u16 d_bwarns ;
2181 __s32 d_padding2 ;
2182 __u64 d_rtb_hardlimit ;
2183 __u64 d_rtb_softlimit ;
2184 __u64 d_rtbcount ;
2185 __s32 d_rtbtimer ;
2186 __u16 d_rtbwarns ;
2187 __s16 d_padding3 ;
2188 char d_padding4[8] ;
2189};
2190#line 146 "include/linux/dqblk_xfs.h"
2191struct fs_qfilestat {
2192 __u64 qfs_ino ;
2193 __u64 qfs_nblks ;
2194 __u32 qfs_nextents ;
2195};
2196#line 146 "include/linux/dqblk_xfs.h"
2197typedef struct fs_qfilestat fs_qfilestat_t;
2198#line 152 "include/linux/dqblk_xfs.h"
2199struct fs_quota_stat {
2200 __s8 qs_version ;
2201 __u16 qs_flags ;
2202 __s8 qs_pad ;
2203 fs_qfilestat_t qs_uquota ;
2204 fs_qfilestat_t qs_gquota ;
2205 __u32 qs_incoredqs ;
2206 __s32 qs_btimelimit ;
2207 __s32 qs_itimelimit ;
2208 __s32 qs_rtbtimelimit ;
2209 __u16 qs_bwarnlimit ;
2210 __u16 qs_iwarnlimit ;
2211};
2212#line 17 "include/linux/dqblk_qtree.h"
2213struct dquot;
2214#line 17
2215struct dquot;
2216#line 17
2217struct dquot;
2218#line 17
2219struct dquot;
2220#line 185 "include/linux/quota.h"
2221typedef __kernel_uid32_t qid_t;
2222#line 186 "include/linux/quota.h"
2223typedef long long qsize_t;
2224#line 200 "include/linux/quota.h"
2225struct mem_dqblk {
2226 qsize_t dqb_bhardlimit ;
2227 qsize_t dqb_bsoftlimit ;
2228 qsize_t dqb_curspace ;
2229 qsize_t dqb_rsvspace ;
2230 qsize_t dqb_ihardlimit ;
2231 qsize_t dqb_isoftlimit ;
2232 qsize_t dqb_curinodes ;
2233 time_t dqb_btime ;
2234 time_t dqb_itime ;
2235};
2236#line 215
2237struct quota_format_type;
2238#line 215
2239struct quota_format_type;
2240#line 215
2241struct quota_format_type;
2242#line 215
2243struct quota_format_type;
2244#line 217 "include/linux/quota.h"
2245struct mem_dqinfo {
2246 struct quota_format_type *dqi_format ;
2247 int dqi_fmt_id ;
2248 struct list_head dqi_dirty_list ;
2249 unsigned long dqi_flags ;
2250 unsigned int dqi_bgrace ;
2251 unsigned int dqi_igrace ;
2252 qsize_t dqi_maxblimit ;
2253 qsize_t dqi_maxilimit ;
2254 void *dqi_priv ;
2255};
2256#line 230
2257struct super_block;
2258#line 284 "include/linux/quota.h"
2259struct dquot {
2260 struct hlist_node dq_hash ;
2261 struct list_head dq_inuse ;
2262 struct list_head dq_free ;
2263 struct list_head dq_dirty ;
2264 struct mutex dq_lock ;
2265 atomic_t dq_count ;
2266 wait_queue_head_t dq_wait_unused ;
2267 struct super_block *dq_sb ;
2268 unsigned int dq_id ;
2269 loff_t dq_off ;
2270 unsigned long dq_flags ;
2271 short dq_type ;
2272 struct mem_dqblk dq_dqb ;
2273};
2274#line 301 "include/linux/quota.h"
2275struct quota_format_ops {
2276 int (*check_quota_file)(struct super_block *sb , int type ) ;
2277 int (*read_file_info)(struct super_block *sb , int type ) ;
2278 int (*write_file_info)(struct super_block *sb , int type ) ;
2279 int (*free_file_info)(struct super_block *sb , int type ) ;
2280 int (*read_dqblk)(struct dquot *dquot ) ;
2281 int (*commit_dqblk)(struct dquot *dquot ) ;
2282 int (*release_dqblk)(struct dquot *dquot ) ;
2283};
2284#line 312 "include/linux/quota.h"
2285struct dquot_operations {
2286 int (*write_dquot)(struct dquot * ) ;
2287 struct dquot *(*alloc_dquot)(struct super_block * , int ) ;
2288 void (*destroy_dquot)(struct dquot * ) ;
2289 int (*acquire_dquot)(struct dquot * ) ;
2290 int (*release_dquot)(struct dquot * ) ;
2291 int (*mark_dirty)(struct dquot * ) ;
2292 int (*write_info)(struct super_block * , int ) ;
2293 qsize_t *(*get_reserved_space)(struct inode * ) ;
2294};
2295#line 325
2296struct path;
2297#line 328 "include/linux/quota.h"
2298struct quotactl_ops {
2299 int (*quota_on)(struct super_block * , int , int , struct path * ) ;
2300 int (*quota_on_meta)(struct super_block * , int , int ) ;
2301 int (*quota_off)(struct super_block * , int ) ;
2302 int (*quota_sync)(struct super_block * , int , int ) ;
2303 int (*get_info)(struct super_block * , int , struct if_dqinfo * ) ;
2304 int (*set_info)(struct super_block * , int , struct if_dqinfo * ) ;
2305 int (*get_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
2306 int (*set_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
2307 int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
2308 int (*set_xstate)(struct super_block * , unsigned int , int ) ;
2309};
2310#line 341 "include/linux/quota.h"
2311struct quota_format_type {
2312 int qf_fmt_id ;
2313 struct quota_format_ops const *qf_ops ;
2314 struct module *qf_owner ;
2315 struct quota_format_type *qf_next ;
2316};
2317#line 395 "include/linux/quota.h"
2318struct quota_info {
2319 unsigned int flags ;
2320 struct mutex dqio_mutex ;
2321 struct mutex dqonoff_mutex ;
2322 struct rw_semaphore dqptr_sem ;
2323 struct inode *files[2] ;
2324 struct mem_dqinfo info[2] ;
2325 struct quota_format_ops const *ops[2] ;
2326};
2327#line 523 "include/linux/fs.h"
2328struct page;
2329#line 524
2330struct address_space;
2331#line 524
2332struct address_space;
2333#line 524
2334struct address_space;
2335#line 524
2336struct address_space;
2337#line 525
2338struct writeback_control;
2339#line 525
2340struct writeback_control;
2341#line 525
2342struct writeback_control;
2343#line 525
2344struct writeback_control;
2345#line 568 "include/linux/fs.h"
2346union __anonunion_arg_214 {
2347 char *buf ;
2348 void *data ;
2349};
2350#line 568 "include/linux/fs.h"
2351struct __anonstruct_read_descriptor_t_213 {
2352 size_t written ;
2353 size_t count ;
2354 union __anonunion_arg_214 arg ;
2355 int error ;
2356};
2357#line 568 "include/linux/fs.h"
2358typedef struct __anonstruct_read_descriptor_t_213 read_descriptor_t;
2359#line 581 "include/linux/fs.h"
2360struct address_space_operations {
2361 int (*writepage)(struct page *page , struct writeback_control *wbc ) ;
2362 int (*readpage)(struct file * , struct page * ) ;
2363 int (*writepages)(struct address_space * , struct writeback_control * ) ;
2364 int (*set_page_dirty)(struct page *page ) ;
2365 int (*readpages)(struct file *filp , struct address_space *mapping , struct list_head *pages ,
2366 unsigned int nr_pages ) ;
2367 int (*write_begin)(struct file * , struct address_space *mapping , loff_t pos ,
2368 unsigned int len , unsigned int flags , struct page **pagep ,
2369 void **fsdata ) ;
2370 int (*write_end)(struct file * , struct address_space *mapping , loff_t pos , unsigned int len ,
2371 unsigned int copied , struct page *page , void *fsdata ) ;
2372 sector_t (*bmap)(struct address_space * , sector_t ) ;
2373 void (*invalidatepage)(struct page * , unsigned long ) ;
2374 int (*releasepage)(struct page * , gfp_t ) ;
2375 void (*freepage)(struct page * ) ;
2376 ssize_t (*direct_IO)(int , struct kiocb * , struct iovec const *iov , loff_t offset ,
2377 unsigned long nr_segs ) ;
2378 int (*get_xip_mem)(struct address_space * , unsigned long , int , void ** , unsigned long * ) ;
2379 int (*migratepage)(struct address_space * , struct page * , struct page * ) ;
2380 int (*launder_page)(struct page * ) ;
2381 int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long ) ;
2382 int (*error_remove_page)(struct address_space * , struct page * ) ;
2383};
2384#line 633
2385struct backing_dev_info;
2386#line 633
2387struct backing_dev_info;
2388#line 633
2389struct backing_dev_info;
2390#line 633
2391struct backing_dev_info;
2392#line 634 "include/linux/fs.h"
2393struct address_space {
2394 struct inode *host ;
2395 struct radix_tree_root page_tree ;
2396 spinlock_t tree_lock ;
2397 unsigned int i_mmap_writable ;
2398 struct prio_tree_root i_mmap ;
2399 struct list_head i_mmap_nonlinear ;
2400 struct mutex i_mmap_mutex ;
2401 unsigned long nrpages ;
2402 unsigned long writeback_index ;
2403 struct address_space_operations const *a_ops ;
2404 unsigned long flags ;
2405 struct backing_dev_info *backing_dev_info ;
2406 spinlock_t private_lock ;
2407 struct list_head private_list ;
2408 struct address_space *assoc_mapping ;
2409} __attribute__((__aligned__(sizeof(long )))) ;
2410#line 658
2411struct hd_struct;
2412#line 658
2413struct hd_struct;
2414#line 658
2415struct hd_struct;
2416#line 658
2417struct gendisk;
2418#line 658
2419struct gendisk;
2420#line 658
2421struct gendisk;
2422#line 658 "include/linux/fs.h"
2423struct block_device {
2424 dev_t bd_dev ;
2425 int bd_openers ;
2426 struct inode *bd_inode ;
2427 struct super_block *bd_super ;
2428 struct mutex bd_mutex ;
2429 struct list_head bd_inodes ;
2430 void *bd_claiming ;
2431 void *bd_holder ;
2432 int bd_holders ;
2433 bool bd_write_holder ;
2434 struct list_head bd_holder_disks ;
2435 struct block_device *bd_contains ;
2436 unsigned int bd_block_size ;
2437 struct hd_struct *bd_part ;
2438 unsigned int bd_part_count ;
2439 int bd_invalidated ;
2440 struct gendisk *bd_disk ;
2441 struct list_head bd_list ;
2442 unsigned long bd_private ;
2443 int bd_fsfreeze_count ;
2444 struct mutex bd_fsfreeze_mutex ;
2445};
2446#line 735
2447struct posix_acl;
2448#line 735
2449struct posix_acl;
2450#line 735
2451struct posix_acl;
2452#line 735
2453struct posix_acl;
2454#line 738
2455struct inode_operations;
2456#line 738
2457struct inode_operations;
2458#line 738
2459struct inode_operations;
2460#line 738 "include/linux/fs.h"
2461union __anonunion____missing_field_name_215 {
2462 struct list_head i_dentry ;
2463 struct rcu_head i_rcu ;
2464};
2465#line 738
2466struct file_operations;
2467#line 738
2468struct file_operations;
2469#line 738
2470struct file_operations;
2471#line 738
2472struct file_lock;
2473#line 738
2474struct file_lock;
2475#line 738
2476struct file_lock;
2477#line 738
2478struct cdev;
2479#line 738
2480struct cdev;
2481#line 738
2482struct cdev;
2483#line 738 "include/linux/fs.h"
2484union __anonunion____missing_field_name_216 {
2485 struct pipe_inode_info *i_pipe ;
2486 struct block_device *i_bdev ;
2487 struct cdev *i_cdev ;
2488};
2489#line 738 "include/linux/fs.h"
2490struct inode {
2491 umode_t i_mode ;
2492 uid_t i_uid ;
2493 gid_t i_gid ;
2494 struct inode_operations const *i_op ;
2495 struct super_block *i_sb ;
2496 spinlock_t i_lock ;
2497 unsigned int i_flags ;
2498 unsigned long i_state ;
2499 void *i_security ;
2500 struct mutex i_mutex ;
2501 unsigned long dirtied_when ;
2502 struct hlist_node i_hash ;
2503 struct list_head i_wb_list ;
2504 struct list_head i_lru ;
2505 struct list_head i_sb_list ;
2506 union __anonunion____missing_field_name_215 __annonCompField32 ;
2507 unsigned long i_ino ;
2508 atomic_t i_count ;
2509 unsigned int i_nlink ;
2510 dev_t i_rdev ;
2511 unsigned int i_blkbits ;
2512 u64 i_version ;
2513 loff_t i_size ;
2514 struct timespec i_atime ;
2515 struct timespec i_mtime ;
2516 struct timespec i_ctime ;
2517 blkcnt_t i_blocks ;
2518 unsigned short i_bytes ;
2519 struct rw_semaphore i_alloc_sem ;
2520 struct file_operations const *i_fop ;
2521 struct file_lock *i_flock ;
2522 struct address_space *i_mapping ;
2523 struct address_space i_data ;
2524 struct dquot *i_dquot[2] ;
2525 struct list_head i_devices ;
2526 union __anonunion____missing_field_name_216 __annonCompField33 ;
2527 __u32 i_generation ;
2528 __u32 i_fsnotify_mask ;
2529 struct hlist_head i_fsnotify_marks ;
2530 atomic_t i_readcount ;
2531 atomic_t i_writecount ;
2532 struct posix_acl *i_acl ;
2533 struct posix_acl *i_default_acl ;
2534 void *i_private ;
2535};
2536#line 903 "include/linux/fs.h"
2537struct fown_struct {
2538 rwlock_t lock ;
2539 struct pid *pid ;
2540 enum pid_type pid_type ;
2541 uid_t uid ;
2542 uid_t euid ;
2543 int signum ;
2544};
2545#line 914 "include/linux/fs.h"
2546struct file_ra_state {
2547 unsigned long start ;
2548 unsigned int size ;
2549 unsigned int async_size ;
2550 unsigned int ra_pages ;
2551 unsigned int mmap_miss ;
2552 loff_t prev_pos ;
2553};
2554#line 937 "include/linux/fs.h"
2555union __anonunion_f_u_217 {
2556 struct list_head fu_list ;
2557 struct rcu_head fu_rcuhead ;
2558};
2559#line 937 "include/linux/fs.h"
2560struct file {
2561 union __anonunion_f_u_217 f_u ;
2562 struct path f_path ;
2563 struct file_operations const *f_op ;
2564 spinlock_t f_lock ;
2565 int f_sb_list_cpu ;
2566 atomic_long_t f_count ;
2567 unsigned int f_flags ;
2568 fmode_t f_mode ;
2569 loff_t f_pos ;
2570 struct fown_struct f_owner ;
2571 struct cred const *f_cred ;
2572 struct file_ra_state f_ra ;
2573 u64 f_version ;
2574 void *f_security ;
2575 void *private_data ;
2576 struct list_head f_ep_links ;
2577 struct address_space *f_mapping ;
2578 unsigned long f_mnt_write_state ;
2579};
2580#line 1064
2581struct files_struct;
2582#line 1064
2583struct files_struct;
2584#line 1064
2585struct files_struct;
2586#line 1064 "include/linux/fs.h"
2587typedef struct files_struct *fl_owner_t;
2588#line 1066 "include/linux/fs.h"
2589struct file_lock_operations {
2590 void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
2591 void (*fl_release_private)(struct file_lock * ) ;
2592};
2593#line 1071 "include/linux/fs.h"
2594struct lock_manager_operations {
2595 int (*fl_compare_owner)(struct file_lock * , struct file_lock * ) ;
2596 void (*fl_notify)(struct file_lock * ) ;
2597 int (*fl_grant)(struct file_lock * , struct file_lock * , int ) ;
2598 void (*fl_release_private)(struct file_lock * ) ;
2599 void (*fl_break)(struct file_lock * ) ;
2600 int (*fl_change)(struct file_lock ** , int ) ;
2601};
2602#line 8 "include/linux/nfs_fs_i.h"
2603struct nlm_lockowner;
2604#line 8
2605struct nlm_lockowner;
2606#line 8
2607struct nlm_lockowner;
2608#line 8
2609struct nlm_lockowner;
2610#line 13 "include/linux/nfs_fs_i.h"
2611struct nfs_lock_info {
2612 u32 state ;
2613 struct nlm_lockowner *owner ;
2614 struct list_head list ;
2615};
2616#line 19
2617struct nfs4_lock_state;
2618#line 19
2619struct nfs4_lock_state;
2620#line 19
2621struct nfs4_lock_state;
2622#line 19
2623struct nfs4_lock_state;
2624#line 20 "include/linux/nfs_fs_i.h"
2625struct nfs4_lock_info {
2626 struct nfs4_lock_state *owner ;
2627};
2628#line 1091 "include/linux/fs.h"
2629struct fasync_struct;
2630#line 1091
2631struct fasync_struct;
2632#line 1091
2633struct fasync_struct;
2634#line 1091 "include/linux/fs.h"
2635struct __anonstruct_afs_219 {
2636 struct list_head link ;
2637 int state ;
2638};
2639#line 1091 "include/linux/fs.h"
2640union __anonunion_fl_u_218 {
2641 struct nfs_lock_info nfs_fl ;
2642 struct nfs4_lock_info nfs4_fl ;
2643 struct __anonstruct_afs_219 afs ;
2644};
2645#line 1091 "include/linux/fs.h"
2646struct file_lock {
2647 struct file_lock *fl_next ;
2648 struct list_head fl_link ;
2649 struct list_head fl_block ;
2650 fl_owner_t fl_owner ;
2651 unsigned char fl_flags ;
2652 unsigned char fl_type ;
2653 unsigned int fl_pid ;
2654 struct pid *fl_nspid ;
2655 wait_queue_head_t fl_wait ;
2656 struct file *fl_file ;
2657 loff_t fl_start ;
2658 loff_t fl_end ;
2659 struct fasync_struct *fl_fasync ;
2660 unsigned long fl_break_time ;
2661 struct file_lock_operations const *fl_ops ;
2662 struct lock_manager_operations const *fl_lmops ;
2663 union __anonunion_fl_u_218 fl_u ;
2664};
2665#line 1324 "include/linux/fs.h"
2666struct fasync_struct {
2667 spinlock_t fa_lock ;
2668 int magic ;
2669 int fa_fd ;
2670 struct fasync_struct *fa_next ;
2671 struct file *fa_file ;
2672 struct rcu_head fa_rcu ;
2673};
2674#line 1364
2675struct file_system_type;
2676#line 1364
2677struct file_system_type;
2678#line 1364
2679struct file_system_type;
2680#line 1364
2681struct super_operations;
2682#line 1364
2683struct super_operations;
2684#line 1364
2685struct super_operations;
2686#line 1364
2687struct xattr_handler;
2688#line 1364
2689struct xattr_handler;
2690#line 1364
2691struct xattr_handler;
2692#line 1364
2693struct mtd_info;
2694#line 1364
2695struct mtd_info;
2696#line 1364
2697struct mtd_info;
2698#line 1364 "include/linux/fs.h"
2699struct super_block {
2700 struct list_head s_list ;
2701 dev_t s_dev ;
2702 unsigned char s_dirt ;
2703 unsigned char s_blocksize_bits ;
2704 unsigned long s_blocksize ;
2705 loff_t s_maxbytes ;
2706 struct file_system_type *s_type ;
2707 struct super_operations const *s_op ;
2708 struct dquot_operations const *dq_op ;
2709 struct quotactl_ops const *s_qcop ;
2710 struct export_operations const *s_export_op ;
2711 unsigned long s_flags ;
2712 unsigned long s_magic ;
2713 struct dentry *s_root ;
2714 struct rw_semaphore s_umount ;
2715 struct mutex s_lock ;
2716 int s_count ;
2717 atomic_t s_active ;
2718 void *s_security ;
2719 struct xattr_handler const **s_xattr ;
2720 struct list_head s_inodes ;
2721 struct hlist_bl_head s_anon ;
2722 struct list_head *s_files ;
2723 struct list_head s_dentry_lru ;
2724 int s_nr_dentry_unused ;
2725 struct block_device *s_bdev ;
2726 struct backing_dev_info *s_bdi ;
2727 struct mtd_info *s_mtd ;
2728 struct list_head s_instances ;
2729 struct quota_info s_dquot ;
2730 int s_frozen ;
2731 wait_queue_head_t s_wait_unfrozen ;
2732 char s_id[32] ;
2733 u8 s_uuid[16] ;
2734 void *s_fs_info ;
2735 fmode_t s_mode ;
2736 u32 s_time_gran ;
2737 struct mutex s_vfs_rename_mutex ;
2738 char *s_subtype ;
2739 char *s_options ;
2740 struct dentry_operations const *s_d_op ;
2741 int cleancache_poolid ;
2742};
2743#line 1499 "include/linux/fs.h"
2744struct fiemap_extent_info {
2745 unsigned int fi_flags ;
2746 unsigned int fi_extents_mapped ;
2747 unsigned int fi_extents_max ;
2748 struct fiemap_extent *fi_extents_start ;
2749};
2750#line 1546 "include/linux/fs.h"
2751struct file_operations {
2752 struct module *owner ;
2753 loff_t (*llseek)(struct file * , loff_t , int ) ;
2754 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ;
2755 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ;
2756 ssize_t (*aio_read)(struct kiocb * , struct iovec const * , unsigned long ,
2757 loff_t ) ;
2758 ssize_t (*aio_write)(struct kiocb * , struct iovec const * , unsigned long ,
2759 loff_t ) ;
2760 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int ,
2761 loff_t , u64 , unsigned int ) ) ;
2762 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
2763 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
2764 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
2765 int (*mmap)(struct file * , struct vm_area_struct * ) ;
2766 int (*open)(struct inode * , struct file * ) ;
2767 int (*flush)(struct file * , fl_owner_t id ) ;
2768 int (*release)(struct inode * , struct file * ) ;
2769 int (*fsync)(struct file * , int datasync ) ;
2770 int (*aio_fsync)(struct kiocb * , int datasync ) ;
2771 int (*fasync)(int , struct file * , int ) ;
2772 int (*lock)(struct file * , int , struct file_lock * ) ;
2773 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * ,
2774 int ) ;
2775 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
2776 unsigned long , unsigned long ) ;
2777 int (*check_flags)(int ) ;
2778 int (*flock)(struct file * , int , struct file_lock * ) ;
2779 ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t ,
2780 unsigned int ) ;
2781 ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t ,
2782 unsigned int ) ;
2783 int (*setlease)(struct file * , long , struct file_lock ** ) ;
2784 long (*fallocate)(struct file *file , int mode , loff_t offset , loff_t len ) ;
2785};
2786#line 1578 "include/linux/fs.h"
2787struct inode_operations {
2788 struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
2789 void *(*follow_link)(struct dentry * , struct nameidata * ) ;
2790 int (*permission)(struct inode * , int , unsigned int ) ;
2791 int (*check_acl)(struct inode * , int , unsigned int ) ;
2792 int (*readlink)(struct dentry * , char * , int ) ;
2793 void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
2794 int (*create)(struct inode * , struct dentry * , int , struct nameidata * ) ;
2795 int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
2796 int (*unlink)(struct inode * , struct dentry * ) ;
2797 int (*symlink)(struct inode * , struct dentry * , char const * ) ;
2798 int (*mkdir)(struct inode * , struct dentry * , int ) ;
2799 int (*rmdir)(struct inode * , struct dentry * ) ;
2800 int (*mknod)(struct inode * , struct dentry * , int , dev_t ) ;
2801 int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
2802 void (*truncate)(struct inode * ) ;
2803 int (*setattr)(struct dentry * , struct iattr * ) ;
2804 int (*getattr)(struct vfsmount *mnt , struct dentry * , struct kstat * ) ;
2805 int (*setxattr)(struct dentry * , char const * , void const * , size_t , int ) ;
2806 ssize_t (*getxattr)(struct dentry * , char const * , void * , size_t ) ;
2807 ssize_t (*listxattr)(struct dentry * , char * , size_t ) ;
2808 int (*removexattr)(struct dentry * , char const * ) ;
2809 void (*truncate_range)(struct inode * , loff_t , loff_t ) ;
2810 int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 start , u64 len ) ;
2811} __attribute__((__aligned__((1) << (6) ))) ;
2812#line 1608
2813struct seq_file;
2814#line 1622 "include/linux/fs.h"
2815struct super_operations {
2816 struct inode *(*alloc_inode)(struct super_block *sb ) ;
2817 void (*destroy_inode)(struct inode * ) ;
2818 void (*dirty_inode)(struct inode * , int flags ) ;
2819 int (*write_inode)(struct inode * , struct writeback_control *wbc ) ;
2820 int (*drop_inode)(struct inode * ) ;
2821 void (*evict_inode)(struct inode * ) ;
2822 void (*put_super)(struct super_block * ) ;
2823 void (*write_super)(struct super_block * ) ;
2824 int (*sync_fs)(struct super_block *sb , int wait ) ;
2825 int (*freeze_fs)(struct super_block * ) ;
2826 int (*unfreeze_fs)(struct super_block * ) ;
2827 int (*statfs)(struct dentry * , struct kstatfs * ) ;
2828 int (*remount_fs)(struct super_block * , int * , char * ) ;
2829 void (*umount_begin)(struct super_block * ) ;
2830 int (*show_options)(struct seq_file * , struct vfsmount * ) ;
2831 int (*show_devname)(struct seq_file * , struct vfsmount * ) ;
2832 int (*show_path)(struct seq_file * , struct vfsmount * ) ;
2833 int (*show_stats)(struct seq_file * , struct vfsmount * ) ;
2834 ssize_t (*quota_read)(struct super_block * , int , char * , size_t , loff_t ) ;
2835 ssize_t (*quota_write)(struct super_block * , int , char const * , size_t ,
2836 loff_t ) ;
2837 int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t ) ;
2838};
2839#line 1802 "include/linux/fs.h"
2840struct file_system_type {
2841 char const *name ;
2842 int fs_flags ;
2843 struct dentry *(*mount)(struct file_system_type * , int , char const * , void * ) ;
2844 void (*kill_sb)(struct super_block * ) ;
2845 struct module *owner ;
2846 struct file_system_type *next ;
2847 struct list_head fs_supers ;
2848 struct lock_class_key s_lock_key ;
2849 struct lock_class_key s_umount_key ;
2850 struct lock_class_key s_vfs_rename_key ;
2851 struct lock_class_key i_lock_key ;
2852 struct lock_class_key i_mutex_key ;
2853 struct lock_class_key i_mutex_dir_key ;
2854 struct lock_class_key i_alloc_sem_key ;
2855};
2856#line 23 "include/linux/mm_types.h"
2857struct address_space;
2858#line 34 "include/linux/mm_types.h"
2859struct __anonstruct____missing_field_name_223 {
2860 u16 inuse ;
2861 u16 objects ;
2862};
2863#line 34 "include/linux/mm_types.h"
2864union __anonunion____missing_field_name_222 {
2865 atomic_t _mapcount ;
2866 struct __anonstruct____missing_field_name_223 __annonCompField34 ;
2867};
2868#line 34 "include/linux/mm_types.h"
2869struct __anonstruct____missing_field_name_225 {
2870 unsigned long private ;
2871 struct address_space *mapping ;
2872};
2873#line 34 "include/linux/mm_types.h"
2874union __anonunion____missing_field_name_224 {
2875 struct __anonstruct____missing_field_name_225 __annonCompField36 ;
2876 struct kmem_cache *slab ;
2877 struct page *first_page ;
2878};
2879#line 34 "include/linux/mm_types.h"
2880union __anonunion____missing_field_name_226 {
2881 unsigned long index ;
2882 void *freelist ;
2883};
2884#line 34 "include/linux/mm_types.h"
2885struct page {
2886 unsigned long flags ;
2887 atomic_t _count ;
2888 union __anonunion____missing_field_name_222 __annonCompField35 ;
2889 union __anonunion____missing_field_name_224 __annonCompField37 ;
2890 union __anonunion____missing_field_name_226 __annonCompField38 ;
2891 struct list_head lru ;
2892};
2893#line 132 "include/linux/mm_types.h"
2894struct __anonstruct_vm_set_228 {
2895 struct list_head list ;
2896 void *parent ;
2897 struct vm_area_struct *head ;
2898};
2899#line 132 "include/linux/mm_types.h"
2900union __anonunion_shared_227 {
2901 struct __anonstruct_vm_set_228 vm_set ;
2902 struct raw_prio_tree_node prio_tree_node ;
2903};
2904#line 132
2905struct anon_vma;
2906#line 132
2907struct anon_vma;
2908#line 132
2909struct anon_vma;
2910#line 132
2911struct vm_operations_struct;
2912#line 132
2913struct vm_operations_struct;
2914#line 132
2915struct vm_operations_struct;
2916#line 132
2917struct mempolicy;
2918#line 132
2919struct mempolicy;
2920#line 132
2921struct mempolicy;
2922#line 132 "include/linux/mm_types.h"
2923struct vm_area_struct {
2924 struct mm_struct *vm_mm ;
2925 unsigned long vm_start ;
2926 unsigned long vm_end ;
2927 struct vm_area_struct *vm_next ;
2928 struct vm_area_struct *vm_prev ;
2929 pgprot_t vm_page_prot ;
2930 unsigned long vm_flags ;
2931 struct rb_node vm_rb ;
2932 union __anonunion_shared_227 shared ;
2933 struct list_head anon_vma_chain ;
2934 struct anon_vma *anon_vma ;
2935 struct vm_operations_struct const *vm_ops ;
2936 unsigned long vm_pgoff ;
2937 struct file *vm_file ;
2938 void *vm_private_data ;
2939 struct mempolicy *vm_policy ;
2940};
2941#line 189 "include/linux/mm_types.h"
2942struct core_thread {
2943 struct task_struct *task ;
2944 struct core_thread *next ;
2945};
2946#line 194 "include/linux/mm_types.h"
2947struct core_state {
2948 atomic_t nr_threads ;
2949 struct core_thread dumper ;
2950 struct completion startup ;
2951};
2952#line 216 "include/linux/mm_types.h"
2953struct mm_rss_stat {
2954 atomic_long_t count[3] ;
2955};
2956#line 220
2957struct linux_binfmt;
2958#line 220
2959struct linux_binfmt;
2960#line 220
2961struct linux_binfmt;
2962#line 220
2963struct mmu_notifier_mm;
2964#line 220
2965struct mmu_notifier_mm;
2966#line 220
2967struct mmu_notifier_mm;
2968#line 220 "include/linux/mm_types.h"
2969struct mm_struct {
2970 struct vm_area_struct *mmap ;
2971 struct rb_root mm_rb ;
2972 struct vm_area_struct *mmap_cache ;
2973 unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
2974 unsigned long pgoff , unsigned long flags ) ;
2975 void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
2976 unsigned long mmap_base ;
2977 unsigned long task_size ;
2978 unsigned long cached_hole_size ;
2979 unsigned long free_area_cache ;
2980 pgd_t *pgd ;
2981 atomic_t mm_users ;
2982 atomic_t mm_count ;
2983 int map_count ;
2984 spinlock_t page_table_lock ;
2985 struct rw_semaphore mmap_sem ;
2986 struct list_head mmlist ;
2987 unsigned long hiwater_rss ;
2988 unsigned long hiwater_vm ;
2989 unsigned long total_vm ;
2990 unsigned long locked_vm ;
2991 unsigned long shared_vm ;
2992 unsigned long exec_vm ;
2993 unsigned long stack_vm ;
2994 unsigned long reserved_vm ;
2995 unsigned long def_flags ;
2996 unsigned long nr_ptes ;
2997 unsigned long start_code ;
2998 unsigned long end_code ;
2999 unsigned long start_data ;
3000 unsigned long end_data ;
3001 unsigned long start_brk ;
3002 unsigned long brk ;
3003 unsigned long start_stack ;
3004 unsigned long arg_start ;
3005 unsigned long arg_end ;
3006 unsigned long env_start ;
3007 unsigned long env_end ;
3008 unsigned long saved_auxv[44] ;
3009 struct mm_rss_stat rss_stat ;
3010 struct linux_binfmt *binfmt ;
3011 cpumask_var_t cpu_vm_mask_var ;
3012 mm_context_t context ;
3013 unsigned int faultstamp ;
3014 unsigned int token_priority ;
3015 unsigned int last_interval ;
3016 atomic_t oom_disable_count ;
3017 unsigned long flags ;
3018 struct core_state *core_state ;
3019 spinlock_t ioctx_lock ;
3020 struct hlist_head ioctx_list ;
3021 struct task_struct *owner ;
3022 struct file *exe_file ;
3023 unsigned long num_exe_file_vmas ;
3024 struct mmu_notifier_mm *mmu_notifier_mm ;
3025 pgtable_t pmd_huge_pte ;
3026 struct cpumask cpumask_allocation ;
3027};
3028#line 7 "include/asm-generic/cputime.h"
3029typedef unsigned long cputime_t;
3030#line 84 "include/linux/sem.h"
3031struct task_struct;
3032#line 122
3033struct sem_undo_list;
3034#line 122
3035struct sem_undo_list;
3036#line 122
3037struct sem_undo_list;
3038#line 135 "include/linux/sem.h"
3039struct sem_undo_list {
3040 atomic_t refcnt ;
3041 spinlock_t lock ;
3042 struct list_head list_proc ;
3043};
3044#line 141 "include/linux/sem.h"
3045struct sysv_sem {
3046 struct sem_undo_list *undo_list ;
3047};
3048#line 10 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h"
3049struct siginfo;
3050#line 10
3051struct siginfo;
3052#line 10
3053struct siginfo;
3054#line 10
3055struct siginfo;
3056#line 30 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h"
3057struct __anonstruct_sigset_t_230 {
3058 unsigned long sig[1] ;
3059};
3060#line 30 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h"
3061typedef struct __anonstruct_sigset_t_230 sigset_t;
3062#line 17 "include/asm-generic/signal-defs.h"
3063typedef void __signalfn_t(int );
3064#line 18 "include/asm-generic/signal-defs.h"
3065typedef __signalfn_t *__sighandler_t;
3066#line 20 "include/asm-generic/signal-defs.h"
3067typedef void __restorefn_t(void);
3068#line 21 "include/asm-generic/signal-defs.h"
3069typedef __restorefn_t *__sigrestore_t;
3070#line 167 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h"
3071struct sigaction {
3072 __sighandler_t sa_handler ;
3073 unsigned long sa_flags ;
3074 __sigrestore_t sa_restorer ;
3075 sigset_t sa_mask ;
3076};
3077#line 174 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h"
3078struct k_sigaction {
3079 struct sigaction sa ;
3080};
3081#line 7 "include/asm-generic/siginfo.h"
3082union sigval {
3083 int sival_int ;
3084 void *sival_ptr ;
3085};
3086#line 7 "include/asm-generic/siginfo.h"
3087typedef union sigval sigval_t;
3088#line 40 "include/asm-generic/siginfo.h"
3089struct __anonstruct__kill_232 {
3090 __kernel_pid_t _pid ;
3091 __kernel_uid32_t _uid ;
3092};
3093#line 40 "include/asm-generic/siginfo.h"
3094struct __anonstruct__timer_233 {
3095 __kernel_timer_t _tid ;
3096 int _overrun ;
3097 char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ;
3098 sigval_t _sigval ;
3099 int _sys_private ;
3100};
3101#line 40 "include/asm-generic/siginfo.h"
3102struct __anonstruct__rt_234 {
3103 __kernel_pid_t _pid ;
3104 __kernel_uid32_t _uid ;
3105 sigval_t _sigval ;
3106};
3107#line 40 "include/asm-generic/siginfo.h"
3108struct __anonstruct__sigchld_235 {
3109 __kernel_pid_t _pid ;
3110 __kernel_uid32_t _uid ;
3111 int _status ;
3112 __kernel_clock_t _utime ;
3113 __kernel_clock_t _stime ;
3114};
3115#line 40 "include/asm-generic/siginfo.h"
3116struct __anonstruct__sigfault_236 {
3117 void *_addr ;
3118 short _addr_lsb ;
3119};
3120#line 40 "include/asm-generic/siginfo.h"
3121struct __anonstruct__sigpoll_237 {
3122 long _band ;
3123 int _fd ;
3124};
3125#line 40 "include/asm-generic/siginfo.h"
3126union __anonunion__sifields_231 {
3127 int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ;
3128 struct __anonstruct__kill_232 _kill ;
3129 struct __anonstruct__timer_233 _timer ;
3130 struct __anonstruct__rt_234 _rt ;
3131 struct __anonstruct__sigchld_235 _sigchld ;
3132 struct __anonstruct__sigfault_236 _sigfault ;
3133 struct __anonstruct__sigpoll_237 _sigpoll ;
3134};
3135#line 40 "include/asm-generic/siginfo.h"
3136struct siginfo {
3137 int si_signo ;
3138 int si_errno ;
3139 int si_code ;
3140 union __anonunion__sifields_231 _sifields ;
3141};
3142#line 40 "include/asm-generic/siginfo.h"
3143typedef struct siginfo siginfo_t;
3144#line 280
3145struct siginfo;
3146#line 10 "include/linux/signal.h"
3147struct task_struct;
3148#line 18
3149struct user_struct;
3150#line 18
3151struct user_struct;
3152#line 18
3153struct user_struct;
3154#line 28 "include/linux/signal.h"
3155struct sigpending {
3156 struct list_head list ;
3157 sigset_t signal ;
3158};
3159#line 239
3160struct timespec;
3161#line 240
3162struct pt_regs;
3163#line 97 "include/linux/proportions.h"
3164struct prop_local_single {
3165 unsigned long events ;
3166 unsigned long period ;
3167 int shift ;
3168 spinlock_t lock ;
3169};
3170#line 10 "include/linux/seccomp.h"
3171struct __anonstruct_seccomp_t_240 {
3172 int mode ;
3173};
3174#line 10 "include/linux/seccomp.h"
3175typedef struct __anonstruct_seccomp_t_240 seccomp_t;
3176#line 82 "include/linux/plist.h"
3177struct plist_head {
3178 struct list_head node_list ;
3179 raw_spinlock_t *rawlock ;
3180 spinlock_t *spinlock ;
3181};
3182#line 90 "include/linux/plist.h"
3183struct plist_node {
3184 int prio ;
3185 struct list_head prio_list ;
3186 struct list_head node_list ;
3187};
3188#line 40 "include/linux/rtmutex.h"
3189struct rt_mutex_waiter;
3190#line 40
3191struct rt_mutex_waiter;
3192#line 40
3193struct rt_mutex_waiter;
3194#line 40
3195struct rt_mutex_waiter;
3196#line 42 "include/linux/resource.h"
3197struct rlimit {
3198 unsigned long rlim_cur ;
3199 unsigned long rlim_max ;
3200};
3201#line 81
3202struct task_struct;
3203#line 11 "include/linux/task_io_accounting.h"
3204struct task_io_accounting {
3205 u64 rchar ;
3206 u64 wchar ;
3207 u64 syscr ;
3208 u64 syscw ;
3209 u64 read_bytes ;
3210 u64 write_bytes ;
3211 u64 cancelled_write_bytes ;
3212};
3213#line 18 "include/linux/latencytop.h"
3214struct latency_record {
3215 unsigned long backtrace[12] ;
3216 unsigned int count ;
3217 unsigned long time ;
3218 unsigned long max ;
3219};
3220#line 26
3221struct task_struct;
3222#line 29 "include/linux/key.h"
3223typedef int32_t key_serial_t;
3224#line 32 "include/linux/key.h"
3225typedef uint32_t key_perm_t;
3226#line 34
3227struct key;
3228#line 34
3229struct key;
3230#line 34
3231struct key;
3232#line 34
3233struct key;
3234#line 74
3235struct seq_file;
3236#line 75
3237struct user_struct;
3238#line 76
3239struct signal_struct;
3240#line 76
3241struct signal_struct;
3242#line 76
3243struct signal_struct;
3244#line 76
3245struct signal_struct;
3246#line 77
3247struct cred;
3248#line 79
3249struct key_type;
3250#line 79
3251struct key_type;
3252#line 79
3253struct key_type;
3254#line 79
3255struct key_type;
3256#line 81
3257struct keyring_list;
3258#line 81
3259struct keyring_list;
3260#line 81
3261struct keyring_list;
3262#line 81
3263struct keyring_list;
3264#line 124
3265struct key_user;
3266#line 124
3267struct key_user;
3268#line 124
3269struct key_user;
3270#line 124 "include/linux/key.h"
3271union __anonunion____missing_field_name_241 {
3272 time_t expiry ;
3273 time_t revoked_at ;
3274};
3275#line 124 "include/linux/key.h"
3276union __anonunion_type_data_242 {
3277 struct list_head link ;
3278 unsigned long x[2] ;
3279 void *p[2] ;
3280 int reject_error ;
3281};
3282#line 124 "include/linux/key.h"
3283union __anonunion_payload_243 {
3284 unsigned long value ;
3285 void *rcudata ;
3286 void *data ;
3287 struct keyring_list *subscriptions ;
3288};
3289#line 124 "include/linux/key.h"
3290struct key {
3291 atomic_t usage ;
3292 key_serial_t serial ;
3293 struct rb_node serial_node ;
3294 struct key_type *type ;
3295 struct rw_semaphore sem ;
3296 struct key_user *user ;
3297 void *security ;
3298 union __anonunion____missing_field_name_241 __annonCompField39 ;
3299 uid_t uid ;
3300 gid_t gid ;
3301 key_perm_t perm ;
3302 unsigned short quotalen ;
3303 unsigned short datalen ;
3304 unsigned long flags ;
3305 char *description ;
3306 union __anonunion_type_data_242 type_data ;
3307 union __anonunion_payload_243 payload ;
3308};
3309#line 18 "include/linux/selinux.h"
3310struct audit_context;
3311#line 18
3312struct audit_context;
3313#line 18
3314struct audit_context;
3315#line 18
3316struct audit_context;
3317#line 21 "include/linux/cred.h"
3318struct user_struct;
3319#line 22
3320struct cred;
3321#line 23
3322struct inode;
3323#line 31 "include/linux/cred.h"
3324struct group_info {
3325 atomic_t usage ;
3326 int ngroups ;
3327 int nblocks ;
3328 gid_t small_block[32] ;
3329 gid_t *blocks[0] ;
3330};
3331#line 83 "include/linux/cred.h"
3332struct thread_group_cred {
3333 atomic_t usage ;
3334 pid_t tgid ;
3335 spinlock_t lock ;
3336 struct key *session_keyring ;
3337 struct key *process_keyring ;
3338 struct rcu_head rcu ;
3339};
3340#line 116 "include/linux/cred.h"
3341struct cred {
3342 atomic_t usage ;
3343 atomic_t subscribers ;
3344 void *put_addr ;
3345 unsigned int magic ;
3346 uid_t uid ;
3347 gid_t gid ;
3348 uid_t suid ;
3349 gid_t sgid ;
3350 uid_t euid ;
3351 gid_t egid ;
3352 uid_t fsuid ;
3353 gid_t fsgid ;
3354 unsigned int securebits ;
3355 kernel_cap_t cap_inheritable ;
3356 kernel_cap_t cap_permitted ;
3357 kernel_cap_t cap_effective ;
3358 kernel_cap_t cap_bset ;
3359 unsigned char jit_keyring ;
3360 struct key *thread_keyring ;
3361 struct key *request_key_auth ;
3362 struct thread_group_cred *tgcred ;
3363 void *security ;
3364 struct user_struct *user ;
3365 struct user_namespace *user_ns ;
3366 struct group_info *group_info ;
3367 struct rcu_head rcu ;
3368};
3369#line 97 "include/linux/sched.h"
3370struct futex_pi_state;
3371#line 97
3372struct futex_pi_state;
3373#line 97
3374struct futex_pi_state;
3375#line 97
3376struct futex_pi_state;
3377#line 98
3378struct robust_list_head;
3379#line 98
3380struct robust_list_head;
3381#line 98
3382struct robust_list_head;
3383#line 98
3384struct robust_list_head;
3385#line 99
3386struct bio_list;
3387#line 99
3388struct bio_list;
3389#line 99
3390struct bio_list;
3391#line 99
3392struct bio_list;
3393#line 100
3394struct fs_struct;
3395#line 100
3396struct fs_struct;
3397#line 100
3398struct fs_struct;
3399#line 100
3400struct fs_struct;
3401#line 101
3402struct perf_event_context;
3403#line 101
3404struct perf_event_context;
3405#line 101
3406struct perf_event_context;
3407#line 101
3408struct perf_event_context;
3409#line 102
3410struct blk_plug;
3411#line 102
3412struct blk_plug;
3413#line 102
3414struct blk_plug;
3415#line 102
3416struct blk_plug;
3417#line 150
3418struct seq_file;
3419#line 151
3420struct cfs_rq;
3421#line 151
3422struct cfs_rq;
3423#line 151
3424struct cfs_rq;
3425#line 151
3426struct cfs_rq;
3427#line 259
3428struct task_struct;
3429#line 364
3430struct nsproxy;
3431#line 365
3432struct user_namespace;
3433#line 58 "include/linux/aio_abi.h"
3434struct io_event {
3435 __u64 data ;
3436 __u64 obj ;
3437 __s64 res ;
3438 __s64 res2 ;
3439};
3440#line 16 "include/linux/uio.h"
3441struct iovec {
3442 void *iov_base ;
3443 __kernel_size_t iov_len ;
3444};
3445#line 15 "include/linux/aio.h"
3446struct kioctx;
3447#line 15
3448struct kioctx;
3449#line 15
3450struct kioctx;
3451#line 15
3452struct kioctx;
3453#line 87 "include/linux/aio.h"
3454union __anonunion_ki_obj_245 {
3455 void *user ;
3456 struct task_struct *tsk ;
3457};
3458#line 87
3459struct eventfd_ctx;
3460#line 87
3461struct eventfd_ctx;
3462#line 87
3463struct eventfd_ctx;
3464#line 87 "include/linux/aio.h"
3465struct kiocb {
3466 struct list_head ki_run_list ;
3467 unsigned long ki_flags ;
3468 int ki_users ;
3469 unsigned int ki_key ;
3470 struct file *ki_filp ;
3471 struct kioctx *ki_ctx ;
3472 int (*ki_cancel)(struct kiocb * , struct io_event * ) ;
3473 ssize_t (*ki_retry)(struct kiocb * ) ;
3474 void (*ki_dtor)(struct kiocb * ) ;
3475 union __anonunion_ki_obj_245 ki_obj ;
3476 __u64 ki_user_data ;
3477 loff_t ki_pos ;
3478 void *private ;
3479 unsigned short ki_opcode ;
3480 size_t ki_nbytes ;
3481 char *ki_buf ;
3482 size_t ki_left ;
3483 struct iovec ki_inline_vec ;
3484 struct iovec *ki_iovec ;
3485 unsigned long ki_nr_segs ;
3486 unsigned long ki_cur_seg ;
3487 struct list_head ki_list ;
3488 struct eventfd_ctx *ki_eventfd ;
3489};
3490#line 165 "include/linux/aio.h"
3491struct aio_ring_info {
3492 unsigned long mmap_base ;
3493 unsigned long mmap_size ;
3494 struct page **ring_pages ;
3495 spinlock_t ring_lock ;
3496 long nr_pages ;
3497 unsigned int nr ;
3498 unsigned int tail ;
3499 struct page *internal_pages[8] ;
3500};
3501#line 178 "include/linux/aio.h"
3502struct kioctx {
3503 atomic_t users ;
3504 int dead ;
3505 struct mm_struct *mm ;
3506 unsigned long user_id ;
3507 struct hlist_node list ;
3508 wait_queue_head_t wait ;
3509 spinlock_t ctx_lock ;
3510 int reqs_active ;
3511 struct list_head active_reqs ;
3512 struct list_head run_list ;
3513 unsigned int max_reqs ;
3514 struct aio_ring_info ring_info ;
3515 struct delayed_work wq ;
3516 struct rcu_head rcu_head ;
3517};
3518#line 213
3519struct mm_struct;
3520#line 441 "include/linux/sched.h"
3521struct sighand_struct {
3522 atomic_t count ;
3523 struct k_sigaction action[64] ;
3524 spinlock_t siglock ;
3525 wait_queue_head_t signalfd_wqh ;
3526};
3527#line 448 "include/linux/sched.h"
3528struct pacct_struct {
3529 int ac_flag ;
3530 long ac_exitcode ;
3531 unsigned long ac_mem ;
3532 cputime_t ac_utime ;
3533 cputime_t ac_stime ;
3534 unsigned long ac_minflt ;
3535 unsigned long ac_majflt ;
3536};
3537#line 456 "include/linux/sched.h"
3538struct cpu_itimer {
3539 cputime_t expires ;
3540 cputime_t incr ;
3541 u32 error ;
3542 u32 incr_error ;
3543};
3544#line 474 "include/linux/sched.h"
3545struct task_cputime {
3546 cputime_t utime ;
3547 cputime_t stime ;
3548 unsigned long long sum_exec_runtime ;
3549};
3550#line 510 "include/linux/sched.h"
3551struct thread_group_cputimer {
3552 struct task_cputime cputime ;
3553 int running ;
3554 spinlock_t lock ;
3555};
3556#line 517
3557struct autogroup;
3558#line 517
3559struct autogroup;
3560#line 517
3561struct autogroup;
3562#line 517
3563struct autogroup;
3564#line 526
3565struct tty_struct;
3566#line 526
3567struct tty_struct;
3568#line 526
3569struct tty_struct;
3570#line 526
3571struct taskstats;
3572#line 526
3573struct taskstats;
3574#line 526
3575struct taskstats;
3576#line 526
3577struct tty_audit_buf;
3578#line 526
3579struct tty_audit_buf;
3580#line 526
3581struct tty_audit_buf;
3582#line 526 "include/linux/sched.h"
3583struct signal_struct {
3584 atomic_t sigcnt ;
3585 atomic_t live ;
3586 int nr_threads ;
3587 wait_queue_head_t wait_chldexit ;
3588 struct task_struct *curr_target ;
3589 struct sigpending shared_pending ;
3590 int group_exit_code ;
3591 int notify_count ;
3592 struct task_struct *group_exit_task ;
3593 int group_stop_count ;
3594 unsigned int flags ;
3595 struct list_head posix_timers ;
3596 struct hrtimer real_timer ;
3597 struct pid *leader_pid ;
3598 ktime_t it_real_incr ;
3599 struct cpu_itimer it[2] ;
3600 struct thread_group_cputimer cputimer ;
3601 struct task_cputime cputime_expires ;
3602 struct list_head cpu_timers[3] ;
3603 struct pid *tty_old_pgrp ;
3604 int leader ;
3605 struct tty_struct *tty ;
3606 struct autogroup *autogroup ;
3607 cputime_t utime ;
3608 cputime_t stime ;
3609 cputime_t cutime ;
3610 cputime_t cstime ;
3611 cputime_t gtime ;
3612 cputime_t cgtime ;
3613 cputime_t prev_utime ;
3614 cputime_t prev_stime ;
3615 unsigned long nvcsw ;
3616 unsigned long nivcsw ;
3617 unsigned long cnvcsw ;
3618 unsigned long cnivcsw ;
3619 unsigned long min_flt ;
3620 unsigned long maj_flt ;
3621 unsigned long cmin_flt ;
3622 unsigned long cmaj_flt ;
3623 unsigned long inblock ;
3624 unsigned long oublock ;
3625 unsigned long cinblock ;
3626 unsigned long coublock ;
3627 unsigned long maxrss ;
3628 unsigned long cmaxrss ;
3629 struct task_io_accounting ioac ;
3630 unsigned long long sum_sched_runtime ;
3631 struct rlimit rlim[16] ;
3632 struct pacct_struct pacct ;
3633 struct taskstats *stats ;
3634 unsigned int audit_tty ;
3635 struct tty_audit_buf *tty_audit_buf ;
3636 struct rw_semaphore threadgroup_fork_lock ;
3637 int oom_adj ;
3638 int oom_score_adj ;
3639 int oom_score_adj_min ;
3640 struct mutex cred_guard_mutex ;
3641};
3642#line 687 "include/linux/sched.h"
3643struct user_struct {
3644 atomic_t __count ;
3645 atomic_t processes ;
3646 atomic_t files ;
3647 atomic_t sigpending ;
3648 atomic_t inotify_watches ;
3649 atomic_t inotify_devs ;
3650 atomic_t fanotify_listeners ;
3651 atomic_long_t epoll_watches ;
3652 unsigned long mq_bytes ;
3653 unsigned long locked_shm ;
3654 struct key *uid_keyring ;
3655 struct key *session_keyring ;
3656 struct hlist_node uidhash_node ;
3657 uid_t uid ;
3658 struct user_namespace *user_ns ;
3659 atomic_long_t locked_vm ;
3660};
3661#line 731
3662struct backing_dev_info;
3663#line 732
3664struct reclaim_state;
3665#line 732
3666struct reclaim_state;
3667#line 732
3668struct reclaim_state;
3669#line 732
3670struct reclaim_state;
3671#line 735 "include/linux/sched.h"
3672struct sched_info {
3673 unsigned long pcount ;
3674 unsigned long long run_delay ;
3675 unsigned long long last_arrival ;
3676 unsigned long long last_queued ;
3677};
3678#line 747 "include/linux/sched.h"
3679struct task_delay_info {
3680 spinlock_t lock ;
3681 unsigned int flags ;
3682 struct timespec blkio_start ;
3683 struct timespec blkio_end ;
3684 u64 blkio_delay ;
3685 u64 swapin_delay ;
3686 u32 blkio_count ;
3687 u32 swapin_count ;
3688 struct timespec freepages_start ;
3689 struct timespec freepages_end ;
3690 u64 freepages_delay ;
3691 u32 freepages_count ;
3692};
3693#line 1050
3694struct io_context;
3695#line 1050
3696struct io_context;
3697#line 1050
3698struct io_context;
3699#line 1050
3700struct io_context;
3701#line 1059
3702struct audit_context;
3703#line 1060
3704struct mempolicy;
3705#line 1061
3706struct pipe_inode_info;
3707#line 1064
3708struct rq;
3709#line 1064
3710struct rq;
3711#line 1064
3712struct rq;
3713#line 1064
3714struct rq;
3715#line 1084 "include/linux/sched.h"
3716struct sched_class {
3717 struct sched_class const *next ;
3718 void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
3719 void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
3720 void (*yield_task)(struct rq *rq ) ;
3721 bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ;
3722 void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ;
3723 struct task_struct *(*pick_next_task)(struct rq *rq ) ;
3724 void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ;
3725 int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ;
3726 void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ;
3727 void (*post_schedule)(struct rq *this_rq ) ;
3728 void (*task_waking)(struct task_struct *task ) ;
3729 void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ;
3730 void (*set_cpus_allowed)(struct task_struct *p , struct cpumask const *newmask ) ;
3731 void (*rq_online)(struct rq *rq ) ;
3732 void (*rq_offline)(struct rq *rq ) ;
3733 void (*set_curr_task)(struct rq *rq ) ;
3734 void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ;
3735 void (*task_fork)(struct task_struct *p ) ;
3736 void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ;
3737 void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ;
3738 void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ;
3739 unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ;
3740 void (*task_move_group)(struct task_struct *p , int on_rq ) ;
3741};
3742#line 1129 "include/linux/sched.h"
3743struct load_weight {
3744 unsigned long weight ;
3745 unsigned long inv_weight ;
3746};
3747#line 1134 "include/linux/sched.h"
3748struct sched_statistics {
3749 u64 wait_start ;
3750 u64 wait_max ;
3751 u64 wait_count ;
3752 u64 wait_sum ;
3753 u64 iowait_count ;
3754 u64 iowait_sum ;
3755 u64 sleep_start ;
3756 u64 sleep_max ;
3757 s64 sum_sleep_runtime ;
3758 u64 block_start ;
3759 u64 block_max ;
3760 u64 exec_max ;
3761 u64 slice_max ;
3762 u64 nr_migrations_cold ;
3763 u64 nr_failed_migrations_affine ;
3764 u64 nr_failed_migrations_running ;
3765 u64 nr_failed_migrations_hot ;
3766 u64 nr_forced_migrations ;
3767 u64 nr_wakeups ;
3768 u64 nr_wakeups_sync ;
3769 u64 nr_wakeups_migrate ;
3770 u64 nr_wakeups_local ;
3771 u64 nr_wakeups_remote ;
3772 u64 nr_wakeups_affine ;
3773 u64 nr_wakeups_affine_attempts ;
3774 u64 nr_wakeups_passive ;
3775 u64 nr_wakeups_idle ;
3776};
3777#line 1169 "include/linux/sched.h"
3778struct sched_entity {
3779 struct load_weight load ;
3780 struct rb_node run_node ;
3781 struct list_head group_node ;
3782 unsigned int on_rq ;
3783 u64 exec_start ;
3784 u64 sum_exec_runtime ;
3785 u64 vruntime ;
3786 u64 prev_sum_exec_runtime ;
3787 u64 nr_migrations ;
3788 struct sched_statistics statistics ;
3789 struct sched_entity *parent ;
3790 struct cfs_rq *cfs_rq ;
3791 struct cfs_rq *my_q ;
3792};
3793#line 1195
3794struct rt_rq;
3795#line 1195
3796struct rt_rq;
3797#line 1195
3798struct rt_rq;
3799#line 1195 "include/linux/sched.h"
3800struct sched_rt_entity {
3801 struct list_head run_list ;
3802 unsigned long timeout ;
3803 unsigned int time_slice ;
3804 int nr_cpus_allowed ;
3805 struct sched_rt_entity *back ;
3806 struct sched_rt_entity *parent ;
3807 struct rt_rq *rt_rq ;
3808 struct rt_rq *my_q ;
3809};
3810#line 1220
3811struct css_set;
3812#line 1220
3813struct css_set;
3814#line 1220
3815struct css_set;
3816#line 1220
3817struct compat_robust_list_head;
3818#line 1220
3819struct compat_robust_list_head;
3820#line 1220
3821struct compat_robust_list_head;
3822#line 1220
3823struct ftrace_ret_stack;
3824#line 1220
3825struct ftrace_ret_stack;
3826#line 1220
3827struct ftrace_ret_stack;
3828#line 1220
3829struct mem_cgroup;
3830#line 1220
3831struct mem_cgroup;
3832#line 1220
3833struct mem_cgroup;
3834#line 1220 "include/linux/sched.h"
3835struct memcg_batch_info {
3836 int do_batch ;
3837 struct mem_cgroup *memcg ;
3838 unsigned long nr_pages ;
3839 unsigned long memsw_nr_pages ;
3840};
3841#line 1220 "include/linux/sched.h"
3842struct task_struct {
3843 long volatile state ;
3844 void *stack ;
3845 atomic_t usage ;
3846 unsigned int flags ;
3847 unsigned int ptrace ;
3848 struct task_struct *wake_entry ;
3849 int on_cpu ;
3850 int on_rq ;
3851 int prio ;
3852 int static_prio ;
3853 int normal_prio ;
3854 unsigned int rt_priority ;
3855 struct sched_class const *sched_class ;
3856 struct sched_entity se ;
3857 struct sched_rt_entity rt ;
3858 struct hlist_head preempt_notifiers ;
3859 unsigned char fpu_counter ;
3860 unsigned int btrace_seq ;
3861 unsigned int policy ;
3862 cpumask_t cpus_allowed ;
3863 struct sched_info sched_info ;
3864 struct list_head tasks ;
3865 struct plist_node pushable_tasks ;
3866 struct mm_struct *mm ;
3867 struct mm_struct *active_mm ;
3868 unsigned int brk_randomized : 1 ;
3869 int exit_state ;
3870 int exit_code ;
3871 int exit_signal ;
3872 int pdeath_signal ;
3873 unsigned int group_stop ;
3874 unsigned int personality ;
3875 unsigned int did_exec : 1 ;
3876 unsigned int in_execve : 1 ;
3877 unsigned int in_iowait : 1 ;
3878 unsigned int sched_reset_on_fork : 1 ;
3879 unsigned int sched_contributes_to_load : 1 ;
3880 pid_t pid ;
3881 pid_t tgid ;
3882 unsigned long stack_canary ;
3883 struct task_struct *real_parent ;
3884 struct task_struct *parent ;
3885 struct list_head children ;
3886 struct list_head sibling ;
3887 struct task_struct *group_leader ;
3888 struct list_head ptraced ;
3889 struct list_head ptrace_entry ;
3890 struct pid_link pids[3] ;
3891 struct list_head thread_group ;
3892 struct completion *vfork_done ;
3893 int *set_child_tid ;
3894 int *clear_child_tid ;
3895 cputime_t utime ;
3896 cputime_t stime ;
3897 cputime_t utimescaled ;
3898 cputime_t stimescaled ;
3899 cputime_t gtime ;
3900 cputime_t prev_utime ;
3901 cputime_t prev_stime ;
3902 unsigned long nvcsw ;
3903 unsigned long nivcsw ;
3904 struct timespec start_time ;
3905 struct timespec real_start_time ;
3906 unsigned long min_flt ;
3907 unsigned long maj_flt ;
3908 struct task_cputime cputime_expires ;
3909 struct list_head cpu_timers[3] ;
3910 struct cred const *real_cred ;
3911 struct cred const *cred ;
3912 struct cred *replacement_session_keyring ;
3913 char comm[16] ;
3914 int link_count ;
3915 int total_link_count ;
3916 struct sysv_sem sysvsem ;
3917 unsigned long last_switch_count ;
3918 struct thread_struct thread ;
3919 struct fs_struct *fs ;
3920 struct files_struct *files ;
3921 struct nsproxy *nsproxy ;
3922 struct signal_struct *signal ;
3923 struct sighand_struct *sighand ;
3924 sigset_t blocked ;
3925 sigset_t real_blocked ;
3926 sigset_t saved_sigmask ;
3927 struct sigpending pending ;
3928 unsigned long sas_ss_sp ;
3929 size_t sas_ss_size ;
3930 int (*notifier)(void *priv ) ;
3931 void *notifier_data ;
3932 sigset_t *notifier_mask ;
3933 struct audit_context *audit_context ;
3934 uid_t loginuid ;
3935 unsigned int sessionid ;
3936 seccomp_t seccomp ;
3937 u32 parent_exec_id ;
3938 u32 self_exec_id ;
3939 spinlock_t alloc_lock ;
3940 struct irqaction *irqaction ;
3941 raw_spinlock_t pi_lock ;
3942 struct plist_head pi_waiters ;
3943 struct rt_mutex_waiter *pi_blocked_on ;
3944 struct mutex_waiter *blocked_on ;
3945 unsigned int irq_events ;
3946 unsigned long hardirq_enable_ip ;
3947 unsigned long hardirq_disable_ip ;
3948 unsigned int hardirq_enable_event ;
3949 unsigned int hardirq_disable_event ;
3950 int hardirqs_enabled ;
3951 int hardirq_context ;
3952 unsigned long softirq_disable_ip ;
3953 unsigned long softirq_enable_ip ;
3954 unsigned int softirq_disable_event ;
3955 unsigned int softirq_enable_event ;
3956 int softirqs_enabled ;
3957 int softirq_context ;
3958 u64 curr_chain_key ;
3959 int lockdep_depth ;
3960 unsigned int lockdep_recursion ;
3961 struct held_lock held_locks[48UL] ;
3962 gfp_t lockdep_reclaim_gfp ;
3963 void *journal_info ;
3964 struct bio_list *bio_list ;
3965 struct blk_plug *plug ;
3966 struct reclaim_state *reclaim_state ;
3967 struct backing_dev_info *backing_dev_info ;
3968 struct io_context *io_context ;
3969 unsigned long ptrace_message ;
3970 siginfo_t *last_siginfo ;
3971 struct task_io_accounting ioac ;
3972 u64 acct_rss_mem1 ;
3973 u64 acct_vm_mem1 ;
3974 cputime_t acct_timexpd ;
3975 nodemask_t mems_allowed ;
3976 int mems_allowed_change_disable ;
3977 int cpuset_mem_spread_rotor ;
3978 int cpuset_slab_spread_rotor ;
3979 struct css_set *cgroups ;
3980 struct list_head cg_list ;
3981 struct robust_list_head *robust_list ;
3982 struct compat_robust_list_head *compat_robust_list ;
3983 struct list_head pi_state_list ;
3984 struct futex_pi_state *pi_state_cache ;
3985 struct perf_event_context *perf_event_ctxp[2] ;
3986 struct mutex perf_event_mutex ;
3987 struct list_head perf_event_list ;
3988 struct mempolicy *mempolicy ;
3989 short il_next ;
3990 short pref_node_fork ;
3991 atomic_t fs_excl ;
3992 struct rcu_head rcu ;
3993 struct pipe_inode_info *splice_pipe ;
3994 struct task_delay_info *delays ;
3995 int make_it_fail ;
3996 struct prop_local_single dirties ;
3997 int latency_record_count ;
3998 struct latency_record latency_record[32] ;
3999 unsigned long timer_slack_ns ;
4000 unsigned long default_timer_slack_ns ;
4001 struct list_head *scm_work_list ;
4002 int curr_ret_stack ;
4003 struct ftrace_ret_stack *ret_stack ;
4004 unsigned long long ftrace_timestamp ;
4005 atomic_t trace_overrun ;
4006 atomic_t tracing_graph_pause ;
4007 unsigned long trace ;
4008 unsigned long trace_recursion ;
4009 struct memcg_batch_info memcg_batch ;
4010 atomic_t ptrace_bp_refcnt ;
4011};
4012#line 1634
4013struct pid_namespace;
4014#line 25 "include/linux/usb.h"
4015struct usb_device;
4016#line 25
4017struct usb_device;
4018#line 25
4019struct usb_device;
4020#line 25
4021struct usb_device;
4022#line 26
4023struct usb_driver;
4024#line 26
4025struct usb_driver;
4026#line 26
4027struct usb_driver;
4028#line 26
4029struct usb_driver;
4030#line 27
4031struct wusb_dev;
4032#line 27
4033struct wusb_dev;
4034#line 27
4035struct wusb_dev;
4036#line 27
4037struct wusb_dev;
4038#line 47
4039struct ep_device;
4040#line 47
4041struct ep_device;
4042#line 47
4043struct ep_device;
4044#line 47
4045struct ep_device;
4046#line 64 "include/linux/usb.h"
4047struct usb_host_endpoint {
4048 struct usb_endpoint_descriptor desc ;
4049 struct usb_ss_ep_comp_descriptor ss_ep_comp ;
4050 struct list_head urb_list ;
4051 void *hcpriv ;
4052 struct ep_device *ep_dev ;
4053 unsigned char *extra ;
4054 int extralen ;
4055 int enabled ;
4056};
4057#line 77 "include/linux/usb.h"
4058struct usb_host_interface {
4059 struct usb_interface_descriptor desc ;
4060 struct usb_host_endpoint *endpoint ;
4061 char *string ;
4062 unsigned char *extra ;
4063 int extralen ;
4064};
4065#line 90
4066enum usb_interface_condition {
4067 USB_INTERFACE_UNBOUND = 0,
4068 USB_INTERFACE_BINDING = 1,
4069 USB_INTERFACE_BOUND = 2,
4070 USB_INTERFACE_UNBINDING = 3
4071} ;
4072#line 159 "include/linux/usb.h"
4073struct usb_interface {
4074 struct usb_host_interface *altsetting ;
4075 struct usb_host_interface *cur_altsetting ;
4076 unsigned int num_altsetting ;
4077 struct usb_interface_assoc_descriptor *intf_assoc ;
4078 int minor ;
4079 enum usb_interface_condition condition ;
4080 unsigned int sysfs_files_created : 1 ;
4081 unsigned int ep_devs_created : 1 ;
4082 unsigned int unregistering : 1 ;
4083 unsigned int needs_remote_wakeup : 1 ;
4084 unsigned int needs_altsetting0 : 1 ;
4085 unsigned int needs_binding : 1 ;
4086 unsigned int reset_running : 1 ;
4087 unsigned int resetting_device : 1 ;
4088 struct device dev ;
4089 struct device *usb_dev ;
4090 atomic_t pm_usage_cnt ;
4091 struct work_struct reset_ws ;
4092};
4093#line 222 "include/linux/usb.h"
4094struct usb_interface_cache {
4095 unsigned int num_altsetting ;
4096 struct kref ref ;
4097 struct usb_host_interface altsetting[0] ;
4098};
4099#line 274 "include/linux/usb.h"
4100struct usb_host_config {
4101 struct usb_config_descriptor desc ;
4102 char *string ;
4103 struct usb_interface_assoc_descriptor *intf_assoc[16] ;
4104 struct usb_interface *interface[32] ;
4105 struct usb_interface_cache *intf_cache[32] ;
4106 unsigned char *extra ;
4107 int extralen ;
4108};
4109#line 305 "include/linux/usb.h"
4110struct usb_devmap {
4111 unsigned long devicemap[128UL / (8UL * sizeof(unsigned long ))] ;
4112};
4113#line 312
4114struct mon_bus;
4115#line 312
4116struct mon_bus;
4117#line 312
4118struct mon_bus;
4119#line 312 "include/linux/usb.h"
4120struct usb_bus {
4121 struct device *controller ;
4122 int busnum ;
4123 char const *bus_name ;
4124 u8 uses_dma ;
4125 u8 uses_pio_for_control ;
4126 u8 otg_port ;
4127 unsigned int is_b_host : 1 ;
4128 unsigned int b_hnp_enable : 1 ;
4129 unsigned int sg_tablesize ;
4130 int devnum_next ;
4131 struct usb_devmap devmap ;
4132 struct usb_device *root_hub ;
4133 struct usb_bus *hs_companion ;
4134 struct list_head bus_list ;
4135 int bandwidth_allocated ;
4136 int bandwidth_int_reqs ;
4137 int bandwidth_isoc_reqs ;
4138 struct dentry *usbfs_dentry ;
4139 struct mon_bus *mon_bus ;
4140 int monitored ;
4141};
4142#line 367
4143struct usb_tt;
4144#line 367
4145struct usb_tt;
4146#line 367
4147struct usb_tt;
4148#line 367
4149struct usb_tt;
4150#line 426 "include/linux/usb.h"
4151struct usb_device {
4152 int devnum ;
4153 char devpath[16] ;
4154 u32 route ;
4155 enum usb_device_state state ;
4156 enum usb_device_speed speed ;
4157 struct usb_tt *tt ;
4158 int ttport ;
4159 unsigned int toggle[2] ;
4160 struct usb_device *parent ;
4161 struct usb_bus *bus ;
4162 struct usb_host_endpoint ep0 ;
4163 struct device dev ;
4164 struct usb_device_descriptor descriptor ;
4165 struct usb_host_config *config ;
4166 struct usb_host_config *actconfig ;
4167 struct usb_host_endpoint *ep_in[16] ;
4168 struct usb_host_endpoint *ep_out[16] ;
4169 char **rawdescriptors ;
4170 unsigned short bus_mA ;
4171 u8 portnum ;
4172 u8 level ;
4173 unsigned int can_submit : 1 ;
4174 unsigned int persist_enabled : 1 ;
4175 unsigned int have_langid : 1 ;
4176 unsigned int authorized : 1 ;
4177 unsigned int authenticated : 1 ;
4178 unsigned int wusb : 1 ;
4179 int string_langid ;
4180 char *product ;
4181 char *manufacturer ;
4182 char *serial ;
4183 struct list_head filelist ;
4184 struct device *usb_classdev ;
4185 struct dentry *usbfs_dentry ;
4186 int maxchild ;
4187 struct usb_device *children[31] ;
4188 u32 quirks ;
4189 atomic_t urbnum ;
4190 unsigned long active_duration ;
4191 unsigned long connect_time ;
4192 unsigned int do_remote_wakeup : 1 ;
4193 unsigned int reset_resume : 1 ;
4194 struct wusb_dev *wusb_dev ;
4195 int slot_id ;
4196};
4197#line 763 "include/linux/usb.h"
4198struct usb_dynids {
4199 spinlock_t lock ;
4200 struct list_head list ;
4201};
4202#line 782 "include/linux/usb.h"
4203struct usbdrv_wrap {
4204 struct device_driver driver ;
4205 int for_devices ;
4206};
4207#line 843 "include/linux/usb.h"
4208struct usb_driver {
4209 char const *name ;
4210 int (*probe)(struct usb_interface *intf , struct usb_device_id const *id ) ;
4211 void (*disconnect)(struct usb_interface *intf ) ;
4212 int (*unlocked_ioctl)(struct usb_interface *intf , unsigned int code , void *buf ) ;
4213 int (*suspend)(struct usb_interface *intf , pm_message_t message ) ;
4214 int (*resume)(struct usb_interface *intf ) ;
4215 int (*reset_resume)(struct usb_interface *intf ) ;
4216 int (*pre_reset)(struct usb_interface *intf ) ;
4217 int (*post_reset)(struct usb_interface *intf ) ;
4218 struct usb_device_id const *id_table ;
4219 struct usb_dynids dynids ;
4220 struct usbdrv_wrap drvwrap ;
4221 unsigned int no_dynamic_id : 1 ;
4222 unsigned int supports_autosuspend : 1 ;
4223 unsigned int soft_unbind : 1 ;
4224};
4225#line 983 "include/linux/usb.h"
4226struct usb_iso_packet_descriptor {
4227 unsigned int offset ;
4228 unsigned int length ;
4229 unsigned int actual_length ;
4230 int status ;
4231};
4232#line 990
4233struct urb;
4234#line 990
4235struct urb;
4236#line 990
4237struct urb;
4238#line 990
4239struct urb;
4240#line 992 "include/linux/usb.h"
4241struct usb_anchor {
4242 struct list_head urb_list ;
4243 wait_queue_head_t wait ;
4244 spinlock_t lock ;
4245 unsigned int poisoned : 1 ;
4246};
4247#line 1183
4248struct scatterlist;
4249#line 1183
4250struct scatterlist;
4251#line 1183
4252struct scatterlist;
4253#line 1183 "include/linux/usb.h"
4254struct urb {
4255 struct kref kref ;
4256 void *hcpriv ;
4257 atomic_t use_count ;
4258 atomic_t reject ;
4259 int unlinked ;
4260 struct list_head urb_list ;
4261 struct list_head anchor_list ;
4262 struct usb_anchor *anchor ;
4263 struct usb_device *dev ;
4264 struct usb_host_endpoint *ep ;
4265 unsigned int pipe ;
4266 unsigned int stream_id ;
4267 int status ;
4268 unsigned int transfer_flags ;
4269 void *transfer_buffer ;
4270 dma_addr_t transfer_dma ;
4271 struct scatterlist *sg ;
4272 int num_sgs ;
4273 u32 transfer_buffer_length ;
4274 u32 actual_length ;
4275 unsigned char *setup_packet ;
4276 dma_addr_t setup_dma ;
4277 int start_frame ;
4278 int number_of_packets ;
4279 int interval ;
4280 int error_count ;
4281 void *context ;
4282 void (*complete)(struct urb * ) ;
4283 struct usb_iso_packet_descriptor iso_frame_desc[0] ;
4284};
4285#line 1388
4286struct scatterlist;
4287#line 43 "include/linux/input.h"
4288struct input_id {
4289 __u16 bustype ;
4290 __u16 vendor ;
4291 __u16 product ;
4292 __u16 version ;
4293};
4294#line 69 "include/linux/input.h"
4295struct input_absinfo {
4296 __s32 value ;
4297 __s32 minimum ;
4298 __s32 maximum ;
4299 __s32 fuzz ;
4300 __s32 flat ;
4301 __s32 resolution ;
4302};
4303#line 93 "include/linux/input.h"
4304struct input_keymap_entry {
4305 __u8 flags ;
4306 __u8 len ;
4307 __u16 index ;
4308 __u32 keycode ;
4309 __u8 scancode[32] ;
4310};
4311#line 926 "include/linux/input.h"
4312struct ff_replay {
4313 __u16 length ;
4314 __u16 delay ;
4315};
4316#line 936 "include/linux/input.h"
4317struct ff_trigger {
4318 __u16 button ;
4319 __u16 interval ;
4320};
4321#line 953 "include/linux/input.h"
4322struct ff_envelope {
4323 __u16 attack_length ;
4324 __u16 attack_level ;
4325 __u16 fade_length ;
4326 __u16 fade_level ;
4327};
4328#line 965 "include/linux/input.h"
4329struct ff_constant_effect {
4330 __s16 level ;
4331 struct ff_envelope envelope ;
4332};
4333#line 976 "include/linux/input.h"
4334struct ff_ramp_effect {
4335 __s16 start_level ;
4336 __s16 end_level ;
4337 struct ff_envelope envelope ;
4338};
4339#line 992 "include/linux/input.h"
4340struct ff_condition_effect {
4341 __u16 right_saturation ;
4342 __u16 left_saturation ;
4343 __s16 right_coeff ;
4344 __s16 left_coeff ;
4345 __u16 deadband ;
4346 __s16 center ;
4347};
4348#line 1021 "include/linux/input.h"
4349struct ff_periodic_effect {
4350 __u16 waveform ;
4351 __u16 period ;
4352 __s16 magnitude ;
4353 __s16 offset ;
4354 __u16 phase ;
4355 struct ff_envelope envelope ;
4356 __u32 custom_len ;
4357 __s16 *custom_data ;
4358};
4359#line 1042 "include/linux/input.h"
4360struct ff_rumble_effect {
4361 __u16 strong_magnitude ;
4362 __u16 weak_magnitude ;
4363};
4364#line 1070 "include/linux/input.h"
4365union __anonunion_u_247 {
4366 struct ff_constant_effect constant ;
4367 struct ff_ramp_effect ramp ;
4368 struct ff_periodic_effect periodic ;
4369 struct ff_condition_effect condition[2] ;
4370 struct ff_rumble_effect rumble ;
4371};
4372#line 1070 "include/linux/input.h"
4373struct ff_effect {
4374 __u16 type ;
4375 __s16 id ;
4376 __u16 direction ;
4377 struct ff_trigger trigger ;
4378 struct ff_replay replay ;
4379 union __anonunion_u_247 u ;
4380};
4381#line 1219
4382struct ff_device;
4383#line 1219
4384struct ff_device;
4385#line 1219
4386struct ff_device;
4387#line 1219
4388struct input_mt_slot;
4389#line 1219
4390struct input_mt_slot;
4391#line 1219
4392struct input_mt_slot;
4393#line 1219
4394struct input_handle;
4395#line 1219
4396struct input_handle;
4397#line 1219
4398struct input_handle;
4399#line 1219 "include/linux/input.h"
4400struct input_dev {
4401 char const *name ;
4402 char const *phys ;
4403 char const *uniq ;
4404 struct input_id id ;
4405 unsigned long propbit[((32UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4406 unsigned long evbit[((32UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4407 unsigned long keybit[((768UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4408 unsigned long relbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4409 unsigned long absbit[((64UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4410 unsigned long mscbit[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4411 unsigned long ledbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4412 unsigned long sndbit[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4413 unsigned long ffbit[((128UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4414 unsigned long swbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4415 unsigned int hint_events_per_packet ;
4416 unsigned int keycodemax ;
4417 unsigned int keycodesize ;
4418 void *keycode ;
4419 int (*setkeycode)(struct input_dev *dev , struct input_keymap_entry const *ke ,
4420 unsigned int *old_keycode ) ;
4421 int (*getkeycode)(struct input_dev *dev , struct input_keymap_entry *ke ) ;
4422 struct ff_device *ff ;
4423 unsigned int repeat_key ;
4424 struct timer_list timer ;
4425 int rep[2] ;
4426 struct input_mt_slot *mt ;
4427 int mtsize ;
4428 int slot ;
4429 int trkid ;
4430 struct input_absinfo *absinfo ;
4431 unsigned long key[((768UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4432 unsigned long led[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4433 unsigned long snd[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4434 unsigned long sw[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4435 int (*open)(struct input_dev *dev ) ;
4436 void (*close)(struct input_dev *dev ) ;
4437 int (*flush)(struct input_dev *dev , struct file *file ) ;
4438 int (*event)(struct input_dev *dev , unsigned int type , unsigned int code , int value ) ;
4439 struct input_handle *grab ;
4440 spinlock_t event_lock ;
4441 struct mutex mutex ;
4442 unsigned int users ;
4443 bool going_away ;
4444 bool sync ;
4445 struct device dev ;
4446 struct list_head h_list ;
4447 struct list_head node ;
4448};
4449#line 1339
4450struct input_handle;
4451#line 1378 "include/linux/input.h"
4452struct input_handler {
4453 void *private ;
4454 void (*event)(struct input_handle *handle , unsigned int type , unsigned int code ,
4455 int value ) ;
4456 bool (*filter)(struct input_handle *handle , unsigned int type , unsigned int code ,
4457 int value ) ;
4458 bool (*match)(struct input_handler *handler , struct input_dev *dev ) ;
4459 int (*connect)(struct input_handler *handler , struct input_dev *dev , struct input_device_id const *id ) ;
4460 void (*disconnect)(struct input_handle *handle ) ;
4461 void (*start)(struct input_handle *handle ) ;
4462 struct file_operations const *fops ;
4463 int minor ;
4464 char const *name ;
4465 struct input_device_id const *id_table ;
4466 struct list_head h_list ;
4467 struct list_head node ;
4468};
4469#line 1411 "include/linux/input.h"
4470struct input_handle {
4471 void *private ;
4472 int open ;
4473 char const *name ;
4474 struct input_dev *dev ;
4475 struct input_handler *handler ;
4476 struct list_head d_node ;
4477 struct list_head h_node ;
4478};
4479#line 1588 "include/linux/input.h"
4480struct ff_device {
4481 int (*upload)(struct input_dev *dev , struct ff_effect *effect , struct ff_effect *old ) ;
4482 int (*erase)(struct input_dev *dev , int effect_id ) ;
4483 int (*playback)(struct input_dev *dev , int effect_id , int value ) ;
4484 void (*set_gain)(struct input_dev *dev , u16 gain ) ;
4485 void (*set_autocenter)(struct input_dev *dev , u16 magnitude ) ;
4486 void (*destroy)(struct ff_device * ) ;
4487 void *private ;
4488 unsigned long ffbit[((128UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
4489 struct mutex mutex ;
4490 int max_effects ;
4491 struct ff_effect *effects ;
4492 struct file *effect_owners[] ;
4493};
4494#line 32 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
4495struct kbtab {
4496 unsigned char *data ;
4497 dma_addr_t data_dma ;
4498 struct input_dev *dev ;
4499 struct usb_device *usbdev ;
4500 struct urb *irq ;
4501 char phys[32] ;
4502};
4503#line 63 "include/linux/byteorder/little_endian.h"
4504__inline static __u16 __le16_to_cpup(__le16 const *p )
4505{ __le16 __cil_tmp2 ;
4506
4507 {
4508 {
4509#line 65
4510 __cil_tmp2 = *p;
4511#line 65
4512 return ((__u16 )__cil_tmp2);
4513 }
4514}
4515}
4516#line 100 "include/linux/printk.h"
4517extern int printk(char const *fmt , ...) ;
4518#line 295 "include/linux/kernel.h"
4519extern int snprintf(char *buf , size_t size , char const *fmt , ...) ;
4520#line 39 "include/linux/string.h"
4521extern size_t strlcat(char * , char const * , __kernel_size_t ) ;
4522#line 141 "include/linux/slab.h"
4523extern void kfree(void const * ) ;
4524#line 221 "include/linux/slub_def.h"
4525extern void *__kmalloc(size_t size , gfp_t flags ) ;
4526#line 255 "include/linux/slub_def.h"
4527__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
4528 gfp_t flags )
4529{ void *tmp___2 ;
4530
4531 {
4532 {
4533#line 270
4534 tmp___2 = __kmalloc(size, flags);
4535 }
4536#line 270
4537 return (tmp___2);
4538}
4539}
4540#line 318 "include/linux/slab.h"
4541__inline static void *kzalloc(size_t size , gfp_t flags )
4542{ void *tmp ;
4543 unsigned int __cil_tmp4 ;
4544
4545 {
4546 {
4547#line 320
4548 __cil_tmp4 = flags | 32768U;
4549#line 320
4550 tmp = kmalloc(size, __cil_tmp4);
4551 }
4552#line 320
4553 return (tmp);
4554}
4555}
4556#line 303 "include/linux/moduleparam.h"
4557extern struct kernel_param_ops param_ops_int ;
4558#line 79 "include/linux/module.h"
4559int init_module(void) ;
4560#line 80
4561void cleanup_module(void) ;
4562#line 99
4563extern struct module __this_module ;
4564#line 705 "include/linux/device.h"
4565extern void *dev_get_drvdata(struct device const *dev ) __attribute__((__ldv_model__)) ;
4566#line 706
4567extern int dev_set_drvdata(struct device *dev , void *data ) ;
4568#line 191 "include/linux/usb.h"
4569__inline static void *usb_get_intfdata(struct usb_interface *intf ) __attribute__((__ldv_model__)) ;
4570#line 191
4571__inline static void *usb_get_intfdata(struct usb_interface *intf ) __attribute__((__ldv_model__)) ;
4572#line 191 "include/linux/usb.h"
4573__inline static void *usb_get_intfdata(struct usb_interface *intf )
4574{ void *tmp___7 ;
4575 struct device *__cil_tmp3 ;
4576 struct device const *__cil_tmp4 ;
4577
4578 {
4579 {
4580#line 193
4581 __cil_tmp3 = & intf->dev;
4582#line 193
4583 __cil_tmp4 = (struct device const *)__cil_tmp3;
4584#line 193
4585 tmp___7 = dev_get_drvdata(__cil_tmp4);
4586 }
4587#line 193
4588 return (tmp___7);
4589}
4590}
4591#line 196
4592__inline static void usb_set_intfdata(struct usb_interface *intf , void *data ) __attribute__((__ldv_model__)) ;
4593#line 196
4594__inline static void usb_set_intfdata(struct usb_interface *intf , void *data ) __attribute__((__ldv_model__)) ;
4595#line 196 "include/linux/usb.h"
4596__inline static void usb_set_intfdata(struct usb_interface *intf , void *data )
4597{ struct device *__cil_tmp3 ;
4598
4599 {
4600 {
4601#line 198
4602 __cil_tmp3 = & intf->dev;
4603#line 198
4604 dev_set_drvdata(__cil_tmp3, data);
4605 }
4606#line 199
4607 return;
4608}
4609}
4610#line 497 "include/linux/usb.h"
4611__inline static struct usb_device *interface_to_usbdev(struct usb_interface *intf )
4612{ struct device const *__mptr ;
4613 struct device *__cil_tmp3 ;
4614 struct usb_device *__cil_tmp4 ;
4615 struct device *__cil_tmp5 ;
4616 unsigned int __cil_tmp6 ;
4617 char *__cil_tmp7 ;
4618 char *__cil_tmp8 ;
4619
4620 {
4621#line 499
4622 __cil_tmp3 = intf->dev.parent;
4623#line 499
4624 __mptr = (struct device const *)__cil_tmp3;
4625 {
4626#line 499
4627 __cil_tmp4 = (struct usb_device *)0;
4628#line 499
4629 __cil_tmp5 = & __cil_tmp4->dev;
4630#line 499
4631 __cil_tmp6 = (unsigned int )__cil_tmp5;
4632#line 499
4633 __cil_tmp7 = (char *)__mptr;
4634#line 499
4635 __cil_tmp8 = __cil_tmp7 - __cil_tmp6;
4636#line 499
4637 return ((struct usb_device *)__cil_tmp8);
4638 }
4639}
4640}
4641#line 637 "include/linux/usb.h"
4642__inline static int usb_make_path(struct usb_device *dev , char *buf , size_t size )
4643{ int actual ;
4644 int tmp___7 ;
4645 struct usb_bus *__cil_tmp6 ;
4646 char const *__cil_tmp7 ;
4647 char *__cil_tmp8 ;
4648 int __cil_tmp9 ;
4649
4650 {
4651 {
4652#line 640
4653 __cil_tmp6 = dev->bus;
4654#line 640
4655 __cil_tmp7 = __cil_tmp6->bus_name;
4656#line 640
4657 __cil_tmp8 = & dev->devpath[0];
4658#line 640
4659 actual = snprintf(buf, size, "usb-%s-%s", __cil_tmp7, __cil_tmp8);
4660 }
4661 {
4662#line 642
4663 __cil_tmp9 = (int )size;
4664#line 642
4665 if (actual >= __cil_tmp9) {
4666#line 642
4667 tmp___7 = -1;
4668 } else {
4669#line 642
4670 tmp___7 = actual;
4671 }
4672 }
4673#line 642
4674 return (tmp___7);
4675}
4676}
4677#line 929
4678extern int usb_register_driver(struct usb_driver * , struct module * , char const * ) ;
4679#line 931 "include/linux/usb.h"
4680__inline static int usb_register(struct usb_driver *driver )
4681{ int tmp___7 ;
4682
4683 {
4684 {
4685#line 933
4686 tmp___7 = usb_register_driver(driver, & __this_module, "kbtab");
4687 }
4688#line 933
4689 return (tmp___7);
4690}
4691}
4692#line 935
4693extern void usb_deregister(struct usb_driver * ) ;
4694#line 1309 "include/linux/usb.h"
4695__inline static void usb_fill_int_urb(struct urb *urb , struct usb_device *dev , unsigned int pipe ,
4696 void *transfer_buffer , int buffer_length ,
4697 void (*complete_fn)(struct urb * ) , void *context ,
4698 int interval )
4699{ enum usb_device_speed __cil_tmp9 ;
4700 unsigned int __cil_tmp10 ;
4701 int __cil_tmp11 ;
4702 enum usb_device_speed __cil_tmp12 ;
4703 unsigned int __cil_tmp13 ;
4704 int __cil_tmp14 ;
4705
4706 {
4707#line 1318
4708 urb->dev = dev;
4709#line 1319
4710 urb->pipe = pipe;
4711#line 1320
4712 urb->transfer_buffer = transfer_buffer;
4713#line 1321
4714 urb->transfer_buffer_length = (u32 )buffer_length;
4715#line 1322
4716 urb->complete = complete_fn;
4717#line 1323
4718 urb->context = context;
4719 {
4720#line 1324
4721 __cil_tmp9 = dev->speed;
4722#line 1324
4723 __cil_tmp10 = (unsigned int )__cil_tmp9;
4724#line 1324
4725 if (__cil_tmp10 == 3U) {
4726#line 1325
4727 __cil_tmp11 = interval - 1;
4728#line 1325
4729 urb->interval = 1 << __cil_tmp11;
4730 } else {
4731 {
4732#line 1324
4733 __cil_tmp12 = dev->speed;
4734#line 1324
4735 __cil_tmp13 = (unsigned int )__cil_tmp12;
4736#line 1324
4737 if (__cil_tmp13 == 5U) {
4738#line 1325
4739 __cil_tmp14 = interval - 1;
4740#line 1325
4741 urb->interval = 1 << __cil_tmp14;
4742 } else {
4743#line 1327
4744 urb->interval = interval;
4745 }
4746 }
4747 }
4748 }
4749#line 1328
4750 urb->start_frame = -1;
4751#line 1329
4752 return;
4753}
4754}
4755#line 1332
4756struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags ) __attribute__((__ldv_model__)) ;
4757#line 1333
4758void usb_free_urb(struct urb *urb ) __attribute__((__ldv_model__)) ;
4759#line 1336
4760extern int usb_submit_urb(struct urb *urb , gfp_t mem_flags ) ;
4761#line 1338
4762extern void usb_kill_urb(struct urb *urb ) ;
4763#line 1377
4764void *usb_alloc_coherent(struct usb_device *dev , size_t size , gfp_t mem_flags ,
4765 dma_addr_t *dma ) __attribute__((__ldv_model__)) ;
4766#line 1379
4767void usb_free_coherent(struct usb_device *dev , size_t size , void *addr , dma_addr_t dma ) __attribute__((__ldv_model__)) ;
4768#line 1526 "include/linux/usb.h"
4769__inline static unsigned int __create_pipe(struct usb_device *dev , unsigned int endpoint )
4770{ unsigned int __cil_tmp3 ;
4771 int __cil_tmp4 ;
4772 int __cil_tmp5 ;
4773 unsigned int __cil_tmp6 ;
4774
4775 {
4776 {
4777#line 1529
4778 __cil_tmp3 = endpoint << 15;
4779#line 1529
4780 __cil_tmp4 = dev->devnum;
4781#line 1529
4782 __cil_tmp5 = __cil_tmp4 << 8;
4783#line 1529
4784 __cil_tmp6 = (unsigned int )__cil_tmp5;
4785#line 1529
4786 return (__cil_tmp6 | __cil_tmp3);
4787 }
4788}
4789}
4790#line 1425 "include/linux/input.h"
4791extern struct input_dev *input_allocate_device(void) ;
4792#line 1426
4793extern void input_free_device(struct input_dev *dev ) ;
4794#line 1439 "include/linux/input.h"
4795__inline static void *input_get_drvdata(struct input_dev *dev )
4796{ void *tmp___7 ;
4797 struct device *__cil_tmp3 ;
4798 struct device const *__cil_tmp4 ;
4799
4800 {
4801 {
4802#line 1441
4803 __cil_tmp3 = & dev->dev;
4804#line 1441
4805 __cil_tmp4 = (struct device const *)__cil_tmp3;
4806#line 1441
4807 tmp___7 = dev_get_drvdata(__cil_tmp4);
4808 }
4809#line 1441
4810 return (tmp___7);
4811}
4812}
4813#line 1444 "include/linux/input.h"
4814__inline static void input_set_drvdata(struct input_dev *dev , void *data )
4815{ struct device *__cil_tmp3 ;
4816
4817 {
4818 {
4819#line 1446
4820 __cil_tmp3 = & dev->dev;
4821#line 1446
4822 dev_set_drvdata(__cil_tmp3, data);
4823 }
4824#line 1447
4825 return;
4826}
4827}
4828#line 1449
4829extern int __attribute__((__warn_unused_result__)) input_register_device(struct input_dev * ) ;
4830#line 1450
4831extern void input_unregister_device(struct input_dev * ) ;
4832#line 1471
4833extern void input_event(struct input_dev *dev , unsigned int type , unsigned int code ,
4834 int value ) ;
4835#line 1474 "include/linux/input.h"
4836__inline static void input_report_key(struct input_dev *dev , unsigned int code ,
4837 int value )
4838{ int __cil_tmp4 ;
4839 int __cil_tmp5 ;
4840
4841 {
4842 {
4843#line 1476
4844 __cil_tmp4 = ! value;
4845#line 1476
4846 __cil_tmp5 = ! __cil_tmp4;
4847#line 1476
4848 input_event(dev, 1U, code, __cil_tmp5);
4849 }
4850#line 1477
4851 return;
4852}
4853}
4854#line 1484 "include/linux/input.h"
4855__inline static void input_report_abs(struct input_dev *dev , unsigned int code ,
4856 int value )
4857{
4858
4859 {
4860 {
4861#line 1486
4862 input_event(dev, 3U, code, value);
4863 }
4864#line 1487
4865 return;
4866}
4867}
4868#line 1499 "include/linux/input.h"
4869__inline static void input_sync(struct input_dev *dev )
4870{
4871
4872 {
4873 {
4874#line 1501
4875 input_event(dev, 0U, 0U, 0);
4876 }
4877#line 1502
4878 return;
4879}
4880}
4881#line 1527
4882extern void input_set_abs_params(struct input_dev *dev , unsigned int axis , int min ,
4883 int max , int fuzz , int flat ) ;
4884#line 16 "include/linux/usb/input.h"
4885__inline static void usb_to_input_id(struct usb_device const *dev , struct input_id *id )
4886{ __le16 __cil_tmp3 ;
4887 __le16 __cil_tmp4 ;
4888 __le16 __cil_tmp5 ;
4889
4890 {
4891#line 19
4892 id->bustype = (__u16 )3;
4893#line 20
4894 __cil_tmp3 = dev->descriptor.idVendor;
4895#line 20
4896 id->vendor = (__le16 )__cil_tmp3;
4897#line 21
4898 __cil_tmp4 = dev->descriptor.idProduct;
4899#line 21
4900 id->product = (__le16 )__cil_tmp4;
4901#line 22
4902 __cil_tmp5 = dev->descriptor.bcdDevice;
4903#line 22
4904 id->version = (__le16 )__cil_tmp5;
4905#line 23
4906 return;
4907}
4908}
4909#line 7 "include/linux/unaligned/access_ok.h"
4910__inline static u16 get_unaligned_le16(void const *p )
4911{ __u16 tmp___7 ;
4912 __le16 *__cil_tmp3 ;
4913 __le16 const *__cil_tmp4 ;
4914
4915 {
4916 {
4917#line 9
4918 __cil_tmp3 = (__le16 *)p;
4919#line 9
4920 __cil_tmp4 = (__le16 const *)__cil_tmp3;
4921#line 9
4922 tmp___7 = __le16_to_cpup(__cil_tmp4);
4923 }
4924#line 9
4925 return (tmp___7);
4926}
4927}
4928#line 22 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
4929static char const __mod_author22[40] __attribute__((__used__, __unused__, __section__(".modinfo"),
4930__aligned__(1))) =
4931#line 22 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
4932 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
4933 (char const )'o', (char const )'r', (char const )'=', (char const )'J',
4934 (char const )'o', (char const )'s', (char const )'h', (char const )' ',
4935 (char const )'M', (char const )'y', (char const )'e', (char const )'r',
4936 (char const )' ', (char const )'<', (char const )'j', (char const )'o',
4937 (char const )'s', (char const )'h', (char const )'@', (char const )'j',
4938 (char const )'o', (char const )'s', (char const )'h', (char const )'i',
4939 (char const )'s', (char const )'a', (char const )'n', (char const )'e',
4940 (char const )'r', (char const )'d', (char const )'.', (char const )'c',
4941 (char const )'o', (char const )'m', (char const )'>', (char const )'\000'};
4942#line 23 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
4943static char const __mod_description23[48] __attribute__((__used__, __unused__,
4944__section__(".modinfo"), __aligned__(1))) =
4945#line 23
4946 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
4947 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
4948 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
4949 (char const )'U', (char const )'S', (char const )'B', (char const )' ',
4950 (char const )'K', (char const )'B', (char const )' ', (char const )'G',
4951 (char const )'e', (char const )'a', (char const )'r', (char const )' ',
4952 (char const )'J', (char const )'a', (char const )'m', (char const )'S',
4953 (char const )'t', (char const )'u', (char const )'d', (char const )'i',
4954 (char const )'o', (char const )' ', (char const )'T', (char const )'a',
4955 (char const )'b', (char const )'l', (char const )'e', (char const )'t',
4956 (char const )' ', (char const )'d', (char const )'r', (char const )'i',
4957 (char const )'v', (char const )'e', (char const )'r', (char const )'\000'};
4958#line 24 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
4959static char const __mod_license24[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
4960__aligned__(1))) =
4961#line 24
4962 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
4963 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
4964 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
4965#line 28 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
4966static int kb_pressure_click = 16;
4967#line 29 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
4968static char const __param_str_kb_pressure_click[18] =
4969#line 29
4970 { (char const )'k', (char const )'b', (char const )'_', (char const )'p',
4971 (char const )'r', (char const )'e', (char const )'s', (char const )'s',
4972 (char const )'u', (char const )'r', (char const )'e', (char const )'_',
4973 (char const )'c', (char const )'l', (char const )'i', (char const )'c',
4974 (char const )'k', (char const )'\000'};
4975#line 29 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
4976static struct kernel_param const __param_kb_pressure_click __attribute__((__used__,
4977__unused__, __section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_kb_pressure_click, (struct kernel_param_ops const *)(& param_ops_int),
4978 (u16 )0, (u16 )0, {(void *)(& kb_pressure_click)}};
4979#line 29 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
4980static char const __mod_kb_pressure_clicktype29[31] __attribute__((__used__, __unused__,
4981__section__(".modinfo"), __aligned__(1))) =
4982#line 29
4983 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
4984 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
4985 (char const )'=', (char const )'k', (char const )'b', (char const )'_',
4986 (char const )'p', (char const )'r', (char const )'e', (char const )'s',
4987 (char const )'s', (char const )'u', (char const )'r', (char const )'e',
4988 (char const )'_', (char const )'c', (char const )'l', (char const )'i',
4989 (char const )'c', (char const )'k', (char const )':', (char const )'i',
4990 (char const )'n', (char const )'t', (char const )'\000'};
4991#line 30 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
4992static char const __mod_kb_pressure_click30[53] __attribute__((__used__, __unused__,
4993__section__(".modinfo"), __aligned__(1))) =
4994#line 30
4995 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
4996 (char const )'=', (char const )'k', (char const )'b', (char const )'_',
4997 (char const )'p', (char const )'r', (char const )'e', (char const )'s',
4998 (char const )'s', (char const )'u', (char const )'r', (char const )'e',
4999 (char const )'_', (char const )'c', (char const )'l', (char const )'i',
5000 (char const )'c', (char const )'k', (char const )':', (char const )'p',
5001 (char const )'r', (char const )'e', (char const )'s', (char const )'s',
5002 (char const )'u', (char const )'r', (char const )'e', (char const )' ',
5003 (char const )'t', (char const )'h', (char const )'r', (char const )'e',
5004 (char const )'s', (char const )'h', (char const )'o', (char const )'l',
5005 (char const )'d', (char const )' ', (char const )'f', (char const )'o',
5006 (char const )'r', (char const )' ', (char const )'c', (char const )'l',
5007 (char const )'i', (char const )'c', (char const )'k', (char const )'s',
5008 (char const )'\000'};
5009#line 41 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5010static void kbtab_irq(struct urb *urb )
5011{ struct kbtab *kbtab ;
5012 unsigned char *data ;
5013 struct input_dev *dev ;
5014 int pressure ;
5015 int retval ;
5016 u16 tmp___7 ;
5017 u16 tmp___8 ;
5018 int tmp___9 ;
5019 void *__cil_tmp10 ;
5020 int __cil_tmp11 ;
5021 int __cil_tmp12 ;
5022 int __cil_tmp13 ;
5023 int __cil_tmp14 ;
5024 unsigned char *__cil_tmp15 ;
5025 void const *__cil_tmp16 ;
5026 int __cil_tmp17 ;
5027 unsigned char *__cil_tmp18 ;
5028 void const *__cil_tmp19 ;
5029 int __cil_tmp20 ;
5030 unsigned char *__cil_tmp21 ;
5031 unsigned char __cil_tmp22 ;
5032 int __cil_tmp23 ;
5033 int __cil_tmp24 ;
5034 unsigned char *__cil_tmp25 ;
5035 unsigned char __cil_tmp26 ;
5036
5037 {
5038#line 43
5039 __cil_tmp10 = urb->context;
5040#line 43
5041 kbtab = (struct kbtab *)__cil_tmp10;
5042#line 44
5043 data = kbtab->data;
5044#line 45
5045 dev = kbtab->dev;
5046 {
5047#line 50
5048 __cil_tmp11 = urb->status;
5049#line 50
5050 if (__cil_tmp11 == 0) {
5051#line 50
5052 goto case_0;
5053 } else {
5054 {
5055#line 53
5056 __cil_tmp12 = urb->status;
5057#line 53
5058 if (__cil_tmp12 == -104) {
5059#line 53
5060 goto case_neg_104;
5061 } else {
5062 {
5063#line 54
5064 __cil_tmp13 = urb->status;
5065#line 54
5066 if (__cil_tmp13 == -2) {
5067#line 54
5068 goto case_neg_104;
5069 } else {
5070 {
5071#line 55
5072 __cil_tmp14 = urb->status;
5073#line 55
5074 if (__cil_tmp14 == -108) {
5075#line 55
5076 goto case_neg_104;
5077 } else {
5078#line 59
5079 goto switch_default;
5080#line 49
5081 if (0) {
5082 case_0:
5083#line 52
5084 goto switch_break;
5085 case_neg_104:
5086 {
5087#line 57
5088 while (1) {
5089 while_continue: ;
5090
5091#line 57
5092 goto while_break;
5093 }
5094 while_break___1: ;
5095 }
5096
5097 while_break: ;
5098#line 58
5099 return;
5100 switch_default:
5101 {
5102#line 60
5103 while (1) {
5104 while_continue___0: ;
5105
5106#line 60
5107 goto while_break___0;
5108 }
5109 while_break___2: ;
5110 }
5111
5112 while_break___0: ;
5113#line 61
5114 goto exit;
5115 } else {
5116 switch_break: ;
5117 }
5118 }
5119 }
5120 }
5121 }
5122 }
5123 }
5124 }
5125 }
5126 {
5127#line 65
5128 input_report_key(dev, 320U, 1);
5129#line 67
5130 __cil_tmp15 = data + 1;
5131#line 67
5132 __cil_tmp16 = (void const *)__cil_tmp15;
5133#line 67
5134 tmp___7 = get_unaligned_le16(__cil_tmp16);
5135#line 67
5136 __cil_tmp17 = (int )tmp___7;
5137#line 67
5138 input_report_abs(dev, 0U, __cil_tmp17);
5139#line 68
5140 __cil_tmp18 = data + 3;
5141#line 68
5142 __cil_tmp19 = (void const *)__cil_tmp18;
5143#line 68
5144 tmp___8 = get_unaligned_le16(__cil_tmp19);
5145#line 68
5146 __cil_tmp20 = (int )tmp___8;
5147#line 68
5148 input_report_abs(dev, 1U, __cil_tmp20);
5149#line 71
5150 __cil_tmp21 = data + 0;
5151#line 71
5152 __cil_tmp22 = *__cil_tmp21;
5153#line 71
5154 __cil_tmp23 = (int )__cil_tmp22;
5155#line 71
5156 __cil_tmp24 = __cil_tmp23 & 2;
5157#line 71
5158 input_report_key(dev, 273U, __cil_tmp24);
5159#line 73
5160 __cil_tmp25 = data + 5;
5161#line 73
5162 __cil_tmp26 = *__cil_tmp25;
5163#line 73
5164 pressure = (int )__cil_tmp26;
5165 }
5166#line 74
5167 if (kb_pressure_click == -1) {
5168 {
5169#line 75
5170 input_report_abs(dev, 24U, pressure);
5171 }
5172 } else {
5173#line 77
5174 if (pressure > kb_pressure_click) {
5175#line 77
5176 tmp___9 = 1;
5177 } else {
5178#line 77
5179 tmp___9 = 0;
5180 }
5181 {
5182#line 77
5183 input_report_key(dev, 272U, tmp___9);
5184 }
5185 }
5186 {
5187#line 79
5188 input_sync(dev);
5189 }
5190 exit:
5191 {
5192#line 82
5193 retval = usb_submit_urb(urb, 32U);
5194 }
5195#line 83
5196 if (retval) {
5197 {
5198#line 84
5199 printk("<3>kbtab: %s - usb_submit_urb failed with result %d\n", "kbtab_irq", retval);
5200 }
5201 } else {
5202
5203 }
5204#line 86
5205 return;
5206}
5207}
5208#line 88 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5209static struct usb_device_id kbtab_ids[1] = { {(__u16 )3, (__u16 )2126, (__u16 )4097, (unsigned short)0, (unsigned short)0,
5210 (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0,
5211 (unsigned char)0, (kernel_ulong_t )0}};
5212#line 93
5213extern struct usb_device_id const __mod_usb_device_table __attribute__((__unused__,
5214__alias__("kbtab_ids"))) ;
5215#line 95 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5216static int kbtab_open(struct input_dev *dev )
5217{ struct kbtab *kbtab ;
5218 void *tmp___7 ;
5219 int tmp___8 ;
5220 struct urb *__cil_tmp5 ;
5221 struct urb *__cil_tmp6 ;
5222
5223 {
5224 {
5225#line 97
5226 tmp___7 = input_get_drvdata(dev);
5227#line 97
5228 kbtab = (struct kbtab *)tmp___7;
5229#line 99
5230 __cil_tmp5 = kbtab->irq;
5231#line 99
5232 __cil_tmp5->dev = kbtab->usbdev;
5233#line 100
5234 __cil_tmp6 = kbtab->irq;
5235#line 100
5236 tmp___8 = usb_submit_urb(__cil_tmp6, 208U);
5237 }
5238#line 100
5239 if (tmp___8) {
5240#line 101
5241 return (-5);
5242 } else {
5243
5244 }
5245#line 103
5246 return (0);
5247}
5248}
5249#line 106 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5250static void kbtab_close(struct input_dev *dev )
5251{ struct kbtab *kbtab ;
5252 void *tmp___7 ;
5253 struct urb *__cil_tmp4 ;
5254
5255 {
5256 {
5257#line 108
5258 tmp___7 = input_get_drvdata(dev);
5259#line 108
5260 kbtab = (struct kbtab *)tmp___7;
5261#line 110
5262 __cil_tmp4 = kbtab->irq;
5263#line 110
5264 usb_kill_urb(__cil_tmp4);
5265 }
5266#line 111
5267 return;
5268}
5269}
5270#line 113 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5271static int kbtab_probe(struct usb_interface *intf , struct usb_device_id const *id )
5272{ struct usb_device *dev ;
5273 struct usb_device *tmp___7 ;
5274 struct usb_endpoint_descriptor *endpoint ;
5275 struct kbtab *kbtab ;
5276 struct input_dev *input_dev ;
5277 int error ;
5278 void *tmp___8 ;
5279 void *tmp___9 ;
5280 unsigned int tmp___10 ;
5281 int tmp ;
5282 int tmp___11 ;
5283 size_t __cil_tmp14 ;
5284 dma_addr_t *__cil_tmp15 ;
5285 unsigned char *__cil_tmp16 ;
5286 struct urb *__cil_tmp17 ;
5287 char *__cil_tmp18 ;
5288 char *__cil_tmp19 ;
5289 char *__cil_tmp20 ;
5290 struct usb_device const *__cil_tmp21 ;
5291 struct input_id *__cil_tmp22 ;
5292 void *__cil_tmp23 ;
5293 unsigned long __cil_tmp24 ;
5294 unsigned long __cil_tmp25 ;
5295 unsigned long __cil_tmp26 ;
5296 unsigned long __cil_tmp27 ;
5297 unsigned long __cil_tmp28 ;
5298 unsigned long __cil_tmp29 ;
5299 unsigned long __cil_tmp30 ;
5300 unsigned long __cil_tmp31 ;
5301 unsigned long __cil_tmp32 ;
5302 unsigned long __cil_tmp33 ;
5303 unsigned long __cil_tmp34 ;
5304 struct usb_host_interface *__cil_tmp35 ;
5305 struct usb_host_endpoint *__cil_tmp36 ;
5306 struct usb_host_endpoint *__cil_tmp37 ;
5307 __u8 __cil_tmp38 ;
5308 unsigned int __cil_tmp39 ;
5309 struct urb *__cil_tmp40 ;
5310 int __cil_tmp41 ;
5311 unsigned int __cil_tmp42 ;
5312 unsigned int __cil_tmp43 ;
5313 unsigned int __cil_tmp44 ;
5314 unsigned char *__cil_tmp45 ;
5315 void *__cil_tmp46 ;
5316 void *__cil_tmp47 ;
5317 __u8 __cil_tmp48 ;
5318 int __cil_tmp49 ;
5319 struct urb *__cil_tmp50 ;
5320 struct urb *__cil_tmp51 ;
5321 struct urb *__cil_tmp52 ;
5322 unsigned int __cil_tmp53 ;
5323 struct input_dev *__cil_tmp54 ;
5324 void *__cil_tmp55 ;
5325 struct urb *__cil_tmp56 ;
5326 size_t __cil_tmp57 ;
5327 unsigned char *__cil_tmp58 ;
5328 void *__cil_tmp59 ;
5329 dma_addr_t __cil_tmp60 ;
5330 void const *__cil_tmp61 ;
5331
5332 {
5333 {
5334#line 115
5335 tmp___7 = interface_to_usbdev(intf);
5336#line 115
5337 dev = tmp___7;
5338#line 119
5339 error = -12;
5340#line 121
5341 tmp___8 = kzalloc(72UL, 208U);
5342#line 121
5343 kbtab = (struct kbtab *)tmp___8;
5344#line 122
5345 input_dev = input_allocate_device();
5346 }
5347#line 123
5348 if (! kbtab) {
5349#line 124
5350 goto fail1;
5351 } else
5352#line 123
5353 if (! input_dev) {
5354#line 124
5355 goto fail1;
5356 } else {
5357
5358 }
5359 {
5360#line 126
5361 __cil_tmp14 = (size_t )8;
5362#line 126
5363 __cil_tmp15 = & kbtab->data_dma;
5364#line 126
5365 tmp___9 = usb_alloc_coherent(dev, __cil_tmp14, 208U, __cil_tmp15);
5366#line 126
5367 kbtab->data = (unsigned char *)tmp___9;
5368 }
5369 {
5370#line 127
5371 __cil_tmp16 = kbtab->data;
5372#line 127
5373 if (! __cil_tmp16) {
5374#line 128
5375 goto fail1;
5376 } else {
5377
5378 }
5379 }
5380 {
5381#line 130
5382 kbtab->irq = usb_alloc_urb(0, 208U);
5383 }
5384 {
5385#line 131
5386 __cil_tmp17 = kbtab->irq;
5387#line 131
5388 if (! __cil_tmp17) {
5389#line 132
5390 goto fail2;
5391 } else {
5392
5393 }
5394 }
5395 {
5396#line 134
5397 kbtab->usbdev = dev;
5398#line 135
5399 kbtab->dev = input_dev;
5400#line 137
5401 __cil_tmp18 = & kbtab->phys[0];
5402#line 137
5403 usb_make_path(dev, __cil_tmp18, 32UL);
5404#line 138
5405 __cil_tmp19 = & kbtab->phys[0];
5406#line 138
5407 strlcat(__cil_tmp19, "/input0", 32UL);
5408#line 140
5409 input_dev->name = "KB Gear Tablet";
5410#line 141
5411 __cil_tmp20 = & kbtab->phys[0];
5412#line 141
5413 input_dev->phys = (char const *)__cil_tmp20;
5414#line 142
5415 __cil_tmp21 = (struct usb_device const *)dev;
5416#line 142
5417 __cil_tmp22 = & input_dev->id;
5418#line 142
5419 usb_to_input_id(__cil_tmp21, __cil_tmp22);
5420#line 143
5421 input_dev->dev.parent = & intf->dev;
5422#line 145
5423 __cil_tmp23 = (void *)kbtab;
5424#line 145
5425 input_set_drvdata(input_dev, __cil_tmp23);
5426#line 147
5427 input_dev->open = & kbtab_open;
5428#line 148
5429 input_dev->close = & kbtab_close;
5430#line 150
5431 __cil_tmp24 = 1UL << 3;
5432#line 150
5433 __cil_tmp25 = 1UL << 1;
5434#line 150
5435 __cil_tmp26 = __cil_tmp25 | __cil_tmp24;
5436#line 150
5437 __cil_tmp27 = input_dev->evbit[0];
5438#line 150
5439 input_dev->evbit[0] = __cil_tmp27 | __cil_tmp26;
5440#line 151
5441 __cil_tmp28 = 1UL << 17;
5442#line 151
5443 __cil_tmp29 = 1UL << 16;
5444#line 151
5445 __cil_tmp30 = __cil_tmp29 | __cil_tmp28;
5446#line 151
5447 __cil_tmp31 = input_dev->keybit[4];
5448#line 151
5449 input_dev->keybit[4] = __cil_tmp31 | __cil_tmp30;
5450#line 153
5451 __cil_tmp32 = 1UL << 10;
5452#line 153
5453 __cil_tmp33 = 1UL | __cil_tmp32;
5454#line 153
5455 __cil_tmp34 = input_dev->keybit[5];
5456#line 153
5457 input_dev->keybit[5] = __cil_tmp34 | __cil_tmp33;
5458#line 155
5459 input_set_abs_params(input_dev, 0U, 0, 8192, 4, 0);
5460#line 156
5461 input_set_abs_params(input_dev, 1U, 0, 5968, 4, 0);
5462#line 157
5463 input_set_abs_params(input_dev, 24U, 0, 255, 0, 0);
5464#line 159
5465 __cil_tmp35 = intf->cur_altsetting;
5466#line 159
5467 __cil_tmp36 = __cil_tmp35->endpoint;
5468#line 159
5469 __cil_tmp37 = __cil_tmp36 + 0;
5470#line 159
5471 endpoint = & __cil_tmp37->desc;
5472#line 161
5473 __cil_tmp38 = endpoint->bEndpointAddress;
5474#line 161
5475 __cil_tmp39 = (unsigned int )__cil_tmp38;
5476#line 161
5477 tmp___10 = __create_pipe(dev, __cil_tmp39);
5478#line 161
5479 __cil_tmp40 = kbtab->irq;
5480#line 161
5481 __cil_tmp41 = 1 << 30;
5482#line 161
5483 __cil_tmp42 = (unsigned int )__cil_tmp41;
5484#line 161
5485 __cil_tmp43 = __cil_tmp42 | tmp___10;
5486#line 161
5487 __cil_tmp44 = __cil_tmp43 | 128U;
5488#line 161
5489 __cil_tmp45 = kbtab->data;
5490#line 161
5491 __cil_tmp46 = (void *)__cil_tmp45;
5492#line 161
5493 __cil_tmp47 = (void *)kbtab;
5494#line 161
5495 __cil_tmp48 = endpoint->bInterval;
5496#line 161
5497 __cil_tmp49 = (int )__cil_tmp48;
5498#line 161
5499 usb_fill_int_urb(__cil_tmp40, dev, __cil_tmp44, __cil_tmp46, 8, & kbtab_irq, __cil_tmp47,
5500 __cil_tmp49);
5501#line 165
5502 __cil_tmp50 = kbtab->irq;
5503#line 165
5504 __cil_tmp50->transfer_dma = kbtab->data_dma;
5505#line 166
5506 __cil_tmp51 = kbtab->irq;
5507#line 166
5508 __cil_tmp52 = kbtab->irq;
5509#line 166
5510 __cil_tmp53 = __cil_tmp52->transfer_flags;
5511#line 166
5512 __cil_tmp51->transfer_flags = __cil_tmp53 | 4U;
5513#line 168
5514 __cil_tmp54 = kbtab->dev;
5515#line 168
5516 tmp___11 = (int )input_register_device(__cil_tmp54);
5517#line 168
5518 tmp = tmp___11;
5519#line 168
5520 error = tmp;
5521 }
5522#line 169
5523 if (error) {
5524#line 170
5525 goto fail3;
5526 } else {
5527
5528 }
5529 {
5530#line 172
5531 __cil_tmp55 = (void *)kbtab;
5532#line 172
5533 usb_set_intfdata(intf, __cil_tmp55);
5534 }
5535#line 174
5536 return (0);
5537 fail3:
5538 {
5539#line 176
5540 __cil_tmp56 = kbtab->irq;
5541#line 176
5542 usb_free_urb(__cil_tmp56);
5543 }
5544 fail2:
5545 {
5546#line 177
5547 __cil_tmp57 = (size_t )8;
5548#line 177
5549 __cil_tmp58 = kbtab->data;
5550#line 177
5551 __cil_tmp59 = (void *)__cil_tmp58;
5552#line 177
5553 __cil_tmp60 = kbtab->data_dma;
5554#line 177
5555 usb_free_coherent(dev, __cil_tmp57, __cil_tmp59, __cil_tmp60);
5556 }
5557 fail1:
5558 {
5559#line 178
5560 input_free_device(input_dev);
5561#line 179
5562 __cil_tmp61 = (void const *)kbtab;
5563#line 179
5564 kfree(__cil_tmp61);
5565 }
5566#line 180
5567 return (error);
5568}
5569}
5570#line 183 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5571static void kbtab_disconnect(struct usb_interface *intf )
5572{ struct kbtab *kbtab ;
5573 void *tmp___7 ;
5574 void *__cil_tmp4 ;
5575 struct input_dev *__cil_tmp5 ;
5576 struct urb *__cil_tmp6 ;
5577 struct usb_device *__cil_tmp7 ;
5578 size_t __cil_tmp8 ;
5579 unsigned char *__cil_tmp9 ;
5580 void *__cil_tmp10 ;
5581 dma_addr_t __cil_tmp11 ;
5582 void const *__cil_tmp12 ;
5583
5584 {
5585 {
5586#line 185
5587 tmp___7 = usb_get_intfdata(intf);
5588#line 185
5589 kbtab = (struct kbtab *)tmp___7;
5590#line 187
5591 __cil_tmp4 = (void *)0;
5592#line 187
5593 usb_set_intfdata(intf, __cil_tmp4);
5594#line 189
5595 __cil_tmp5 = kbtab->dev;
5596#line 189
5597 input_unregister_device(__cil_tmp5);
5598#line 190
5599 __cil_tmp6 = kbtab->irq;
5600#line 190
5601 usb_free_urb(__cil_tmp6);
5602#line 191
5603 __cil_tmp7 = kbtab->usbdev;
5604#line 191
5605 __cil_tmp8 = (size_t )8;
5606#line 191
5607 __cil_tmp9 = kbtab->data;
5608#line 191
5609 __cil_tmp10 = (void *)__cil_tmp9;
5610#line 191
5611 __cil_tmp11 = kbtab->data_dma;
5612#line 191
5613 usb_free_coherent(__cil_tmp7, __cil_tmp8, __cil_tmp10, __cil_tmp11);
5614#line 192
5615 __cil_tmp12 = (void const *)kbtab;
5616#line 192
5617 kfree(__cil_tmp12);
5618 }
5619#line 193
5620 return;
5621}
5622}
5623#line 195 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5624static struct usb_driver kbtab_driver =
5625#line 195
5626 {"kbtab", & kbtab_probe, & kbtab_disconnect, (int (*)(struct usb_interface *intf ,
5627 unsigned int code , void *buf ))0,
5628 (int (*)(struct usb_interface *intf , pm_message_t message ))0, (int (*)(struct usb_interface *intf ))0,
5629 (int (*)(struct usb_interface *intf ))0, (int (*)(struct usb_interface *intf ))0,
5630 (int (*)(struct usb_interface *intf ))0, (struct usb_device_id const *)(kbtab_ids),
5631 {{{{{0U}, 0U, 0U, (void *)0, {(struct lock_class_key *)0, {(struct lock_class *)0,
5632 (struct lock_class *)0},
5633 (char const *)0, 0, 0UL}}}}, {(struct list_head *)0,
5634 (struct list_head *)0}},
5635 {{(char const *)0, (struct bus_type *)0, (struct module *)0, (char const *)0,
5636 (_Bool)0, (struct of_device_id const *)0, (int (*)(struct device *dev ))0,
5637 (int (*)(struct device *dev ))0, (void (*)(struct device *dev ))0, (int (*)(struct device *dev ,
5638 pm_message_t state ))0,
5639 (int (*)(struct device *dev ))0, (struct attribute_group const **)0, (struct dev_pm_ops const *)0,
5640 (struct driver_private *)0}, 0}, 0U, 0U, 0U};
5641#line 202
5642static int kbtab_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
5643#line 202
5644static int kbtab_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
5645#line 202 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5646static int kbtab_init(void)
5647{ int retval ;
5648
5649 {
5650 {
5651#line 205
5652 retval = usb_register(& kbtab_driver);
5653 }
5654#line 206
5655 if (retval) {
5656#line 207
5657 goto out;
5658 } else {
5659
5660 }
5661 {
5662#line 208
5663 printk("<6>kbtab: v0.0.2:USB KB Gear JamStudio Tablet driver\n");
5664 }
5665 out:
5666#line 211
5667 return (retval);
5668}
5669}
5670#line 214
5671static void kbtab_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
5672#line 214
5673static void kbtab_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
5674#line 214 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5675static void kbtab_exit(void)
5676{
5677
5678 {
5679 {
5680#line 216
5681 usb_deregister(& kbtab_driver);
5682 }
5683#line 217
5684 return;
5685}
5686}
5687#line 219 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5688int init_module(void)
5689{ int tmp___7 ;
5690
5691 {
5692 {
5693#line 219
5694 tmp___7 = kbtab_init();
5695 }
5696#line 219
5697 return (tmp___7);
5698}
5699}
5700#line 220 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5701void cleanup_module(void)
5702{
5703
5704 {
5705 {
5706#line 220
5707 kbtab_exit();
5708 }
5709#line 220
5710 return;
5711}
5712}
5713#line 238
5714void ldv_check_final_state(void) __attribute__((__ldv_model__)) ;
5715#line 241
5716extern void ldv_check_return_value(int res ) ;
5717#line 244
5718extern void ldv_initialize(void) ;
5719#line 247
5720extern int nondet_int(void) ;
5721#line 250 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5722int LDV_IN_INTERRUPT ;
5723#line 273 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5724static int res_kbtab_probe_3 ;
5725#line 253 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/input/tablet/kbtab.c.common.c"
5726void main(void)
5727{ struct usb_interface *var_group1 ;
5728 struct usb_device_id const *var_kbtab_probe_3_p1 ;
5729 int tmp___7 ;
5730 int ldv_s_kbtab_driver_usb_driver ;
5731 int tmp___8 ;
5732 int tmp___9 ;
5733 int __cil_tmp7 ;
5734
5735 {
5736 {
5737#line 289
5738 LDV_IN_INTERRUPT = 1;
5739#line 298
5740 ldv_initialize();
5741#line 310
5742 tmp___7 = kbtab_init();
5743 }
5744#line 310
5745 if (tmp___7) {
5746#line 311
5747 goto ldv_final;
5748 } else {
5749
5750 }
5751#line 312
5752 ldv_s_kbtab_driver_usb_driver = 0;
5753 {
5754#line 315
5755 while (1) {
5756 while_continue: ;
5757 {
5758#line 315
5759 tmp___9 = nondet_int();
5760 }
5761#line 315
5762 if (tmp___9) {
5763
5764 } else {
5765 {
5766#line 315
5767 __cil_tmp7 = ldv_s_kbtab_driver_usb_driver == 0;
5768#line 315
5769 if (! __cil_tmp7) {
5770
5771 } else {
5772#line 315
5773 goto while_break;
5774 }
5775 }
5776 }
5777 {
5778#line 319
5779 tmp___8 = nondet_int();
5780 }
5781#line 321
5782 if (tmp___8 == 0) {
5783#line 321
5784 goto case_0;
5785 } else
5786#line 346
5787 if (tmp___8 == 1) {
5788#line 346
5789 goto case_1;
5790 } else {
5791#line 368
5792 goto switch_default;
5793#line 319
5794 if (0) {
5795 case_0:
5796#line 324
5797 if (ldv_s_kbtab_driver_usb_driver == 0) {
5798 {
5799#line 335
5800 res_kbtab_probe_3 = kbtab_probe(var_group1, var_kbtab_probe_3_p1);
5801#line 336
5802 ldv_check_return_value(res_kbtab_probe_3);
5803 }
5804#line 337
5805 if (res_kbtab_probe_3) {
5806#line 338
5807 goto ldv_module_exit;
5808 } else {
5809
5810 }
5811#line 339
5812 ldv_s_kbtab_driver_usb_driver = ldv_s_kbtab_driver_usb_driver + 1;
5813 } else {
5814
5815 }
5816#line 345
5817 goto switch_break;
5818 case_1:
5819#line 349
5820 if (ldv_s_kbtab_driver_usb_driver == 1) {
5821 {
5822#line 360
5823 kbtab_disconnect(var_group1);
5824#line 361
5825 ldv_s_kbtab_driver_usb_driver = 0;
5826 }
5827 } else {
5828
5829 }
5830#line 367
5831 goto switch_break;
5832 switch_default:
5833#line 368
5834 goto switch_break;
5835 } else {
5836 switch_break: ;
5837 }
5838 }
5839 }
5840 while_break___0: ;
5841 }
5842
5843 while_break: ;
5844 ldv_module_exit:
5845 {
5846#line 386
5847 kbtab_exit();
5848 }
5849 ldv_final:
5850 {
5851#line 389
5852 ldv_check_final_state();
5853 }
5854#line 392
5855 return;
5856}
5857}
5858#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast-assert.h"
5859void ldv_blast_assert(void)
5860{
5861
5862 {
5863 ERROR:
5864#line 6
5865 goto ERROR;
5866}
5867}
5868#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/engine-blast.h"
5869extern void *ldv_undefined_pointer(void) ;
5870#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/model0068.c"
5871void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
5872#line 22
5873void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ;
5874#line 22 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/model0068.c"
5875void ldv_assume_stop(void)
5876{
5877
5878 {
5879 LDV_STOP:
5880#line 23
5881 goto LDV_STOP;
5882}
5883}
5884#line 29 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/model0068.c"
5885int ldv_urb_state = 0;
5886#line 31 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/model0068.c"
5887int ldv_coherent_state = 0;
5888#line 62
5889void *usb_alloc_coherent(struct usb_device *dev , size_t size , gfp_t mem_flags ,
5890 dma_addr_t *dma ) __attribute__((__ldv_model__)) ;
5891#line 62 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/model0068.c"
5892void *usb_alloc_coherent(struct usb_device *dev , size_t size , gfp_t mem_flags ,
5893 dma_addr_t *dma )
5894{ void *arbitrary_memory ;
5895 void *tmp___7 ;
5896
5897 {
5898 {
5899#line 64
5900 while (1) {
5901 while_continue: ;
5902 {
5903#line 64
5904 tmp___7 = ldv_undefined_pointer();
5905#line 64
5906 arbitrary_memory = tmp___7;
5907 }
5908#line 64
5909 if (! arbitrary_memory) {
5910#line 64
5911 return ((void *)0);
5912 } else {
5913
5914 }
5915#line 64
5916 ldv_coherent_state = ldv_coherent_state + 1;
5917#line 64
5918 return (arbitrary_memory);
5919#line 64
5920 goto while_break;
5921 }
5922 while_break___0: ;
5923 }
5924
5925 while_break: ;
5926#line 65
5927 return ((void *)0);
5928}
5929}
5930#line 68
5931void usb_free_coherent(struct usb_device *dev , size_t size , void *addr , dma_addr_t dma ) __attribute__((__ldv_model__)) ;
5932#line 68 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/model0068.c"
5933void usb_free_coherent(struct usb_device *dev , size_t size , void *addr , dma_addr_t dma )
5934{ void *__cil_tmp5 ;
5935 unsigned long __cil_tmp6 ;
5936 unsigned long __cil_tmp7 ;
5937 int __cil_tmp8 ;
5938
5939 {
5940 {
5941#line 70
5942 while (1) {
5943 while_continue: ;
5944
5945 {
5946#line 70
5947 __cil_tmp5 = (void *)0;
5948#line 70
5949 __cil_tmp6 = (unsigned long )__cil_tmp5;
5950#line 70
5951 __cil_tmp7 = (unsigned long )addr;
5952#line 70
5953 __cil_tmp8 = __cil_tmp7 != __cil_tmp6;
5954#line 70
5955 if (! __cil_tmp8) {
5956 {
5957#line 70
5958 ldv_assume_stop();
5959 }
5960 } else {
5961
5962 }
5963 }
5964#line 70
5965 if (addr) {
5966#line 70
5967 if (ldv_coherent_state >= 1) {
5968
5969 } else {
5970 {
5971#line 70
5972 ldv_blast_assert();
5973 }
5974 }
5975#line 70
5976 ldv_coherent_state = ldv_coherent_state - 1;
5977 } else {
5978
5979 }
5980#line 70
5981 goto while_break;
5982 }
5983 while_break___0: ;
5984 }
5985
5986 while_break: ;
5987#line 71
5988 return;
5989}
5990}
5991#line 74
5992struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags ) __attribute__((__ldv_model__)) ;
5993#line 74 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/model0068.c"
5994struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags )
5995{ void *arbitrary_memory ;
5996 void *tmp___7 ;
5997 void *__cil_tmp5 ;
5998
5999 {
6000 {
6001#line 75
6002 while (1) {
6003 while_continue: ;
6004 {
6005#line 75
6006 tmp___7 = ldv_undefined_pointer();
6007#line 75
6008 arbitrary_memory = tmp___7;
6009 }
6010#line 75
6011 if (! arbitrary_memory) {
6012 {
6013#line 75
6014 __cil_tmp5 = (void *)0;
6015#line 75
6016 return ((struct urb *)__cil_tmp5);
6017 }
6018 } else {
6019
6020 }
6021#line 75
6022 ldv_urb_state = ldv_urb_state + 1;
6023#line 75
6024 return ((struct urb *)arbitrary_memory);
6025#line 75
6026 goto while_break;
6027 }
6028 while_break___0: ;
6029 }
6030
6031 while_break: ;
6032#line 76
6033 return ((struct urb *)0);
6034}
6035}
6036#line 79
6037void usb_free_urb(struct urb *urb ) __attribute__((__ldv_model__)) ;
6038#line 79 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/model0068.c"
6039void usb_free_urb(struct urb *urb )
6040{ struct urb *__cil_tmp2 ;
6041 unsigned long __cil_tmp3 ;
6042 unsigned long __cil_tmp4 ;
6043 int __cil_tmp5 ;
6044
6045 {
6046 {
6047#line 80
6048 while (1) {
6049 while_continue: ;
6050
6051 {
6052#line 80
6053 __cil_tmp2 = (struct urb *)0;
6054#line 80
6055 __cil_tmp3 = (unsigned long )__cil_tmp2;
6056#line 80
6057 __cil_tmp4 = (unsigned long )urb;
6058#line 80
6059 __cil_tmp5 = __cil_tmp4 != __cil_tmp3;
6060#line 80
6061 if (! __cil_tmp5) {
6062 {
6063#line 80
6064 ldv_assume_stop();
6065 }
6066 } else {
6067
6068 }
6069 }
6070#line 80
6071 if (urb) {
6072#line 80
6073 if (ldv_urb_state >= 1) {
6074
6075 } else {
6076 {
6077#line 80
6078 ldv_blast_assert();
6079 }
6080 }
6081#line 80
6082 ldv_urb_state = ldv_urb_state - 1;
6083 } else {
6084
6085 }
6086#line 80
6087 goto while_break;
6088 }
6089 while_break___0: ;
6090 }
6091
6092 while_break: ;
6093#line 81
6094 return;
6095}
6096}
6097#line 84
6098void ldv_check_final_state(void) __attribute__((__ldv_model__)) ;
6099#line 84 "/anthill/stuff/tacas-comp/work/current--X--drivers/input/tablet/kbtab.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/kernel-rules/files/model0068.c"
6100void ldv_check_final_state(void)
6101{
6102
6103 {
6104#line 86
6105 if (ldv_urb_state == 0) {
6106
6107 } else {
6108 {
6109#line 86
6110 ldv_blast_assert();
6111 }
6112 }
6113#line 88
6114 if (ldv_coherent_state == 0) {
6115
6116 } else {
6117 {
6118#line 88
6119 ldv_blast_assert();
6120 }
6121 }
6122#line 89
6123 return;
6124}
6125}