ClabureDB

1/* Generated by CIL v. 1.3.7 */ 2/* print_CIL_Input is true */ 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 15 "include/linux/blk_types.h" 1056struct page; 1057#line 16 1058struct block_device; 1059#line 16 1060struct block_device; 1061#line 16 1062struct block_device; 1063#line 16 1064struct block_device; 1065#line 72 "include/linux/rcupdate.h" 1066struct rcu_head { 1067 struct rcu_head *next ; 1068 void (*func)(struct rcu_head *head ) ; 1069}; 1070#line 33 "include/linux/list_bl.h" 1071struct hlist_bl_node; 1072#line 33 1073struct hlist_bl_node; 1074#line 33 1075struct hlist_bl_node; 1076#line 33 "include/linux/list_bl.h" 1077struct hlist_bl_head { 1078 struct hlist_bl_node *first ; 1079}; 1080#line 37 "include/linux/list_bl.h" 1081struct hlist_bl_node { 1082 struct hlist_bl_node *next ; 1083 struct hlist_bl_node **pprev ; 1084}; 1085#line 13 "include/linux/dcache.h" 1086struct nameidata; 1087#line 13 1088struct nameidata; 1089#line 13 1090struct nameidata; 1091#line 13 1092struct nameidata; 1093#line 14 1094struct path; 1095#line 14 1096struct path; 1097#line 14 1098struct path; 1099#line 14 1100struct path; 1101#line 15 1102struct vfsmount; 1103#line 15 1104struct vfsmount; 1105#line 15 1106struct vfsmount; 1107#line 15 1108struct vfsmount; 1109#line 35 "include/linux/dcache.h" 1110struct qstr { 1111 unsigned int hash ; 1112 unsigned int len ; 1113 unsigned char const *name ; 1114}; 1115#line 116 1116struct inode; 1117#line 116 1118struct inode; 1119#line 116 1120struct inode; 1121#line 116 1122struct dentry_operations; 1123#line 116 1124struct dentry_operations; 1125#line 116 1126struct dentry_operations; 1127#line 116 1128struct super_block; 1129#line 116 1130struct super_block; 1131#line 116 1132struct super_block; 1133#line 116 "include/linux/dcache.h" 1134union __anonunion_d_u_135 { 1135 struct list_head d_child ; 1136 struct rcu_head d_rcu ; 1137}; 1138#line 116 "include/linux/dcache.h" 1139struct dentry { 1140 unsigned int d_flags ; 1141 seqcount_t d_seq ; 1142 struct hlist_bl_node d_hash ; 1143 struct dentry *d_parent ; 1144 struct qstr d_name ; 1145 struct inode *d_inode ; 1146 unsigned char d_iname[32] ; 1147 unsigned int d_count ; 1148 spinlock_t d_lock ; 1149 struct dentry_operations const *d_op ; 1150 struct super_block *d_sb ; 1151 unsigned long d_time ; 1152 void *d_fsdata ; 1153 struct list_head d_lru ; 1154 union __anonunion_d_u_135 d_u ; 1155 struct list_head d_subdirs ; 1156 struct list_head d_alias ; 1157}; 1158#line 159 "include/linux/dcache.h" 1159struct dentry_operations { 1160 int (*d_revalidate)(struct dentry * , struct nameidata * ) ; 1161 int (*d_hash)(struct dentry const * , struct inode const * , struct qstr * ) ; 1162 int (*d_compare)(struct dentry const * , struct inode const * , struct dentry const * , 1163 struct inode const * , unsigned int , char const * , struct qstr const * ) ; 1164 int (*d_delete)(struct dentry const * ) ; 1165 void (*d_release)(struct dentry * ) ; 1166 void (*d_iput)(struct dentry * , struct inode * ) ; 1167 char *(*d_dname)(struct dentry * , char * , int ) ; 1168 struct vfsmount *(*d_automount)(struct path * ) ; 1169 int (*d_manage)(struct dentry * , bool ) ; 1170} __attribute__((__aligned__((1) << (6) ))) ; 1171#line 4 "include/linux/path.h" 1172struct dentry; 1173#line 5 1174struct vfsmount; 1175#line 7 "include/linux/path.h" 1176struct path { 1177 struct vfsmount *mnt ; 1178 struct dentry *dentry ; 1179}; 1180#line 62 "include/linux/stat.h" 1181struct kstat { 1182 u64 ino ; 1183 dev_t dev ; 1184 umode_t mode ; 1185 unsigned int nlink ; 1186 uid_t uid ; 1187 gid_t gid ; 1188 dev_t rdev ; 1189 loff_t size ; 1190 struct timespec atime ; 1191 struct timespec mtime ; 1192 struct timespec ctime ; 1193 unsigned long blksize ; 1194 unsigned long long blocks ; 1195}; 1196#line 57 "include/linux/radix-tree.h" 1197struct radix_tree_node; 1198#line 57 1199struct radix_tree_node; 1200#line 57 1201struct radix_tree_node; 1202#line 57 "include/linux/radix-tree.h" 1203struct radix_tree_root { 1204 unsigned int height ; 1205 gfp_t gfp_mask ; 1206 struct radix_tree_node *rnode ; 1207}; 1208#line 14 "include/linux/prio_tree.h" 1209struct prio_tree_node; 1210#line 14 1211struct prio_tree_node; 1212#line 14 1213struct prio_tree_node; 1214#line 14 "include/linux/prio_tree.h" 1215struct raw_prio_tree_node { 1216 struct prio_tree_node *left ; 1217 struct prio_tree_node *right ; 1218 struct prio_tree_node *parent ; 1219}; 1220#line 20 "include/linux/prio_tree.h" 1221struct prio_tree_node { 1222 struct prio_tree_node *left ; 1223 struct prio_tree_node *right ; 1224 struct prio_tree_node *parent ; 1225 unsigned long start ; 1226 unsigned long last ; 1227}; 1228#line 28 "include/linux/prio_tree.h" 1229struct prio_tree_root { 1230 struct prio_tree_node *prio_tree_node ; 1231 unsigned short index_bits ; 1232 unsigned short raw ; 1233}; 1234#line 6 "include/linux/pid.h" 1235enum pid_type { 1236 PIDTYPE_PID = 0, 1237 PIDTYPE_PGID = 1, 1238 PIDTYPE_SID = 2, 1239 PIDTYPE_MAX = 3 1240} ; 1241#line 50 1242struct pid_namespace; 1243#line 50 1244struct pid_namespace; 1245#line 50 1246struct pid_namespace; 1247#line 50 "include/linux/pid.h" 1248struct upid { 1249 int nr ; 1250 struct pid_namespace *ns ; 1251 struct hlist_node pid_chain ; 1252}; 1253#line 57 "include/linux/pid.h" 1254struct pid { 1255 atomic_t count ; 1256 unsigned int level ; 1257 struct hlist_head tasks[3] ; 1258 struct rcu_head rcu ; 1259 struct upid numbers[1] ; 1260}; 1261#line 69 "include/linux/pid.h" 1262struct pid_link { 1263 struct hlist_node node ; 1264 struct pid *pid ; 1265}; 1266#line 100 1267struct pid_namespace; 1268#line 18 "include/linux/capability.h" 1269struct task_struct; 1270#line 94 "include/linux/capability.h" 1271struct kernel_cap_struct { 1272 __u32 cap[2] ; 1273}; 1274#line 94 "include/linux/capability.h" 1275typedef struct kernel_cap_struct kernel_cap_t; 1276#line 376 1277struct dentry; 1278#line 377 1279struct user_namespace; 1280#line 377 1281struct user_namespace; 1282#line 377 1283struct user_namespace; 1284#line 377 1285struct user_namespace; 1286#line 16 "include/linux/fiemap.h" 1287struct fiemap_extent { 1288 __u64 fe_logical ; 1289 __u64 fe_physical ; 1290 __u64 fe_length ; 1291 __u64 fe_reserved64[2] ; 1292 __u32 fe_flags ; 1293 __u32 fe_reserved[3] ; 1294}; 1295#line 399 "include/linux/fs.h" 1296struct export_operations; 1297#line 399 1298struct export_operations; 1299#line 399 1300struct export_operations; 1301#line 399 1302struct export_operations; 1303#line 401 1304struct iovec; 1305#line 401 1306struct iovec; 1307#line 401 1308struct iovec; 1309#line 401 1310struct iovec; 1311#line 402 1312struct nameidata; 1313#line 403 1314struct kiocb; 1315#line 403 1316struct kiocb; 1317#line 403 1318struct kiocb; 1319#line 403 1320struct kiocb; 1321#line 404 1322struct kobject; 1323#line 405 1324struct pipe_inode_info; 1325#line 405 1326struct pipe_inode_info; 1327#line 405 1328struct pipe_inode_info; 1329#line 405 1330struct pipe_inode_info; 1331#line 406 1332struct poll_table_struct; 1333#line 406 1334struct poll_table_struct; 1335#line 406 1336struct poll_table_struct; 1337#line 406 1338struct poll_table_struct; 1339#line 407 1340struct kstatfs; 1341#line 407 1342struct kstatfs; 1343#line 407 1344struct kstatfs; 1345#line 407 1346struct kstatfs; 1347#line 408 1348struct vm_area_struct; 1349#line 409 1350struct vfsmount; 1351#line 410 1352struct cred; 1353#line 410 1354struct cred; 1355#line 410 1356struct cred; 1357#line 410 1358struct cred; 1359#line 460 "include/linux/fs.h" 1360struct iattr { 1361 unsigned int ia_valid ; 1362 umode_t ia_mode ; 1363 uid_t ia_uid ; 1364 gid_t ia_gid ; 1365 loff_t ia_size ; 1366 struct timespec ia_atime ; 1367 struct timespec ia_mtime ; 1368 struct timespec ia_ctime ; 1369 struct file *ia_file ; 1370}; 1371#line 129 "include/linux/quota.h" 1372struct if_dqinfo { 1373 __u64 dqi_bgrace ; 1374 __u64 dqi_igrace ; 1375 __u32 dqi_flags ; 1376 __u32 dqi_valid ; 1377}; 1378#line 50 "include/linux/dqblk_xfs.h" 1379struct fs_disk_quota { 1380 __s8 d_version ; 1381 __s8 d_flags ; 1382 __u16 d_fieldmask ; 1383 __u32 d_id ; 1384 __u64 d_blk_hardlimit ; 1385 __u64 d_blk_softlimit ; 1386 __u64 d_ino_hardlimit ; 1387 __u64 d_ino_softlimit ; 1388 __u64 d_bcount ; 1389 __u64 d_icount ; 1390 __s32 d_itimer ; 1391 __s32 d_btimer ; 1392 __u16 d_iwarns ; 1393 __u16 d_bwarns ; 1394 __s32 d_padding2 ; 1395 __u64 d_rtb_hardlimit ; 1396 __u64 d_rtb_softlimit ; 1397 __u64 d_rtbcount ; 1398 __s32 d_rtbtimer ; 1399 __u16 d_rtbwarns ; 1400 __s16 d_padding3 ; 1401 char d_padding4[8] ; 1402}; 1403#line 146 "include/linux/dqblk_xfs.h" 1404struct fs_qfilestat { 1405 __u64 qfs_ino ; 1406 __u64 qfs_nblks ; 1407 __u32 qfs_nextents ; 1408}; 1409#line 146 "include/linux/dqblk_xfs.h" 1410typedef struct fs_qfilestat fs_qfilestat_t; 1411#line 152 "include/linux/dqblk_xfs.h" 1412struct fs_quota_stat { 1413 __s8 qs_version ; 1414 __u16 qs_flags ; 1415 __s8 qs_pad ; 1416 fs_qfilestat_t qs_uquota ; 1417 fs_qfilestat_t qs_gquota ; 1418 __u32 qs_incoredqs ; 1419 __s32 qs_btimelimit ; 1420 __s32 qs_itimelimit ; 1421 __s32 qs_rtbtimelimit ; 1422 __u16 qs_bwarnlimit ; 1423 __u16 qs_iwarnlimit ; 1424}; 1425#line 17 "include/linux/dqblk_qtree.h" 1426struct dquot; 1427#line 17 1428struct dquot; 1429#line 17 1430struct dquot; 1431#line 17 1432struct dquot; 1433#line 185 "include/linux/quota.h" 1434typedef __kernel_uid32_t qid_t; 1435#line 186 "include/linux/quota.h" 1436typedef long long qsize_t; 1437#line 200 "include/linux/quota.h" 1438struct mem_dqblk { 1439 qsize_t dqb_bhardlimit ; 1440 qsize_t dqb_bsoftlimit ; 1441 qsize_t dqb_curspace ; 1442 qsize_t dqb_rsvspace ; 1443 qsize_t dqb_ihardlimit ; 1444 qsize_t dqb_isoftlimit ; 1445 qsize_t dqb_curinodes ; 1446 time_t dqb_btime ; 1447 time_t dqb_itime ; 1448}; 1449#line 215 1450struct quota_format_type; 1451#line 215 1452struct quota_format_type; 1453#line 215 1454struct quota_format_type; 1455#line 215 1456struct quota_format_type; 1457#line 217 "include/linux/quota.h" 1458struct mem_dqinfo { 1459 struct quota_format_type *dqi_format ; 1460 int dqi_fmt_id ; 1461 struct list_head dqi_dirty_list ; 1462 unsigned long dqi_flags ; 1463 unsigned int dqi_bgrace ; 1464 unsigned int dqi_igrace ; 1465 qsize_t dqi_maxblimit ; 1466 qsize_t dqi_maxilimit ; 1467 void *dqi_priv ; 1468}; 1469#line 230 1470struct super_block; 1471#line 284 "include/linux/quota.h" 1472struct dquot { 1473 struct hlist_node dq_hash ; 1474 struct list_head dq_inuse ; 1475 struct list_head dq_free ; 1476 struct list_head dq_dirty ; 1477 struct mutex dq_lock ; 1478 atomic_t dq_count ; 1479 wait_queue_head_t dq_wait_unused ; 1480 struct super_block *dq_sb ; 1481 unsigned int dq_id ; 1482 loff_t dq_off ; 1483 unsigned long dq_flags ; 1484 short dq_type ; 1485 struct mem_dqblk dq_dqb ; 1486}; 1487#line 301 "include/linux/quota.h" 1488struct quota_format_ops { 1489 int (*check_quota_file)(struct super_block *sb , int type ) ; 1490 int (*read_file_info)(struct super_block *sb , int type ) ; 1491 int (*write_file_info)(struct super_block *sb , int type ) ; 1492 int (*free_file_info)(struct super_block *sb , int type ) ; 1493 int (*read_dqblk)(struct dquot *dquot ) ; 1494 int (*commit_dqblk)(struct dquot *dquot ) ; 1495 int (*release_dqblk)(struct dquot *dquot ) ; 1496}; 1497#line 312 "include/linux/quota.h" 1498struct dquot_operations { 1499 int (*write_dquot)(struct dquot * ) ; 1500 struct dquot *(*alloc_dquot)(struct super_block * , int ) ; 1501 void (*destroy_dquot)(struct dquot * ) ; 1502 int (*acquire_dquot)(struct dquot * ) ; 1503 int (*release_dquot)(struct dquot * ) ; 1504 int (*mark_dirty)(struct dquot * ) ; 1505 int (*write_info)(struct super_block * , int ) ; 1506 qsize_t *(*get_reserved_space)(struct inode * ) ; 1507}; 1508#line 325 1509struct path; 1510#line 328 "include/linux/quota.h" 1511struct quotactl_ops { 1512 int (*quota_on)(struct super_block * , int , int , struct path * ) ; 1513 int (*quota_on_meta)(struct super_block * , int , int ) ; 1514 int (*quota_off)(struct super_block * , int ) ; 1515 int (*quota_sync)(struct super_block * , int , int ) ; 1516 int (*get_info)(struct super_block * , int , struct if_dqinfo * ) ; 1517 int (*set_info)(struct super_block * , int , struct if_dqinfo * ) ; 1518 int (*get_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ; 1519 int (*set_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ; 1520 int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ; 1521 int (*set_xstate)(struct super_block * , unsigned int , int ) ; 1522}; 1523#line 341 "include/linux/quota.h" 1524struct quota_format_type { 1525 int qf_fmt_id ; 1526 struct quota_format_ops const *qf_ops ; 1527 struct module *qf_owner ; 1528 struct quota_format_type *qf_next ; 1529}; 1530#line 395 "include/linux/quota.h" 1531struct quota_info { 1532 unsigned int flags ; 1533 struct mutex dqio_mutex ; 1534 struct mutex dqonoff_mutex ; 1535 struct rw_semaphore dqptr_sem ; 1536 struct inode *files[2] ; 1537 struct mem_dqinfo info[2] ; 1538 struct quota_format_ops const *ops[2] ; 1539}; 1540#line 523 "include/linux/fs.h" 1541struct page; 1542#line 524 1543struct address_space; 1544#line 524 1545struct address_space; 1546#line 524 1547struct address_space; 1548#line 524 1549struct address_space; 1550#line 525 1551struct writeback_control; 1552#line 525 1553struct writeback_control; 1554#line 525 1555struct writeback_control; 1556#line 525 1557struct writeback_control; 1558#line 568 "include/linux/fs.h" 1559union __anonunion_arg_143 { 1560 char *buf ; 1561 void *data ; 1562}; 1563#line 568 "include/linux/fs.h" 1564struct __anonstruct_read_descriptor_t_142 { 1565 size_t written ; 1566 size_t count ; 1567 union __anonunion_arg_143 arg ; 1568 int error ; 1569}; 1570#line 568 "include/linux/fs.h" 1571typedef struct __anonstruct_read_descriptor_t_142 read_descriptor_t; 1572#line 581 "include/linux/fs.h" 1573struct address_space_operations { 1574 int (*writepage)(struct page *page , struct writeback_control *wbc ) ; 1575 int (*readpage)(struct file * , struct page * ) ; 1576 int (*writepages)(struct address_space * , struct writeback_control * ) ; 1577 int (*set_page_dirty)(struct page *page ) ; 1578 int (*readpages)(struct file *filp , struct address_space *mapping , struct list_head *pages , 1579 unsigned int nr_pages ) ; 1580 int (*write_begin)(struct file * , struct address_space *mapping , loff_t pos , 1581 unsigned int len , unsigned int flags , struct page **pagep , 1582 void **fsdata ) ; 1583 int (*write_end)(struct file * , struct address_space *mapping , loff_t pos , unsigned int len , 1584 unsigned int copied , struct page *page , void *fsdata ) ; 1585 sector_t (*bmap)(struct address_space * , sector_t ) ; 1586 void (*invalidatepage)(struct page * , unsigned long ) ; 1587 int (*releasepage)(struct page * , gfp_t ) ; 1588 void (*freepage)(struct page * ) ; 1589 ssize_t (*direct_IO)(int , struct kiocb * , struct iovec const *iov , loff_t offset , 1590 unsigned long nr_segs ) ; 1591 int (*get_xip_mem)(struct address_space * , unsigned long , int , void ** , unsigned long * ) ; 1592 int (*migratepage)(struct address_space * , struct page * , struct page * ) ; 1593 int (*launder_page)(struct page * ) ; 1594 int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long ) ; 1595 int (*error_remove_page)(struct address_space * , struct page * ) ; 1596}; 1597#line 633 1598struct backing_dev_info; 1599#line 633 1600struct backing_dev_info; 1601#line 633 1602struct backing_dev_info; 1603#line 633 1604struct backing_dev_info; 1605#line 634 "include/linux/fs.h" 1606struct address_space { 1607 struct inode *host ; 1608 struct radix_tree_root page_tree ; 1609 spinlock_t tree_lock ; 1610 unsigned int i_mmap_writable ; 1611 struct prio_tree_root i_mmap ; 1612 struct list_head i_mmap_nonlinear ; 1613 struct mutex i_mmap_mutex ; 1614 unsigned long nrpages ; 1615 unsigned long writeback_index ; 1616 struct address_space_operations const *a_ops ; 1617 unsigned long flags ; 1618 struct backing_dev_info *backing_dev_info ; 1619 spinlock_t private_lock ; 1620 struct list_head private_list ; 1621 struct address_space *assoc_mapping ; 1622} __attribute__((__aligned__(sizeof(long )))) ; 1623#line 658 1624struct hd_struct; 1625#line 658 1626struct hd_struct; 1627#line 658 1628struct hd_struct; 1629#line 658 1630struct gendisk; 1631#line 658 1632struct gendisk; 1633#line 658 1634struct gendisk; 1635#line 658 "include/linux/fs.h" 1636struct block_device { 1637 dev_t bd_dev ; 1638 int bd_openers ; 1639 struct inode *bd_inode ; 1640 struct super_block *bd_super ; 1641 struct mutex bd_mutex ; 1642 struct list_head bd_inodes ; 1643 void *bd_claiming ; 1644 void *bd_holder ; 1645 int bd_holders ; 1646 bool bd_write_holder ; 1647 struct list_head bd_holder_disks ; 1648 struct block_device *bd_contains ; 1649 unsigned int bd_block_size ; 1650 struct hd_struct *bd_part ; 1651 unsigned int bd_part_count ; 1652 int bd_invalidated ; 1653 struct gendisk *bd_disk ; 1654 struct list_head bd_list ; 1655 unsigned long bd_private ; 1656 int bd_fsfreeze_count ; 1657 struct mutex bd_fsfreeze_mutex ; 1658}; 1659#line 735 1660struct posix_acl; 1661#line 735 1662struct posix_acl; 1663#line 735 1664struct posix_acl; 1665#line 735 1666struct posix_acl; 1667#line 738 1668struct inode_operations; 1669#line 738 1670struct inode_operations; 1671#line 738 1672struct inode_operations; 1673#line 738 "include/linux/fs.h" 1674union __anonunion____missing_field_name_144 { 1675 struct list_head i_dentry ; 1676 struct rcu_head i_rcu ; 1677}; 1678#line 738 1679struct file_operations; 1680#line 738 1681struct file_operations; 1682#line 738 1683struct file_operations; 1684#line 738 1685struct file_lock; 1686#line 738 1687struct file_lock; 1688#line 738 1689struct file_lock; 1690#line 738 1691struct cdev; 1692#line 738 1693struct cdev; 1694#line 738 1695struct cdev; 1696#line 738 "include/linux/fs.h" 1697union __anonunion____missing_field_name_145 { 1698 struct pipe_inode_info *i_pipe ; 1699 struct block_device *i_bdev ; 1700 struct cdev *i_cdev ; 1701}; 1702#line 738 "include/linux/fs.h" 1703struct inode { 1704 umode_t i_mode ; 1705 uid_t i_uid ; 1706 gid_t i_gid ; 1707 struct inode_operations const *i_op ; 1708 struct super_block *i_sb ; 1709 spinlock_t i_lock ; 1710 unsigned int i_flags ; 1711 unsigned long i_state ; 1712 void *i_security ; 1713 struct mutex i_mutex ; 1714 unsigned long dirtied_when ; 1715 struct hlist_node i_hash ; 1716 struct list_head i_wb_list ; 1717 struct list_head i_lru ; 1718 struct list_head i_sb_list ; 1719 union __anonunion____missing_field_name_144 __annonCompField29 ; 1720 unsigned long i_ino ; 1721 atomic_t i_count ; 1722 unsigned int i_nlink ; 1723 dev_t i_rdev ; 1724 unsigned int i_blkbits ; 1725 u64 i_version ; 1726 loff_t i_size ; 1727 struct timespec i_atime ; 1728 struct timespec i_mtime ; 1729 struct timespec i_ctime ; 1730 blkcnt_t i_blocks ; 1731 unsigned short i_bytes ; 1732 struct rw_semaphore i_alloc_sem ; 1733 struct file_operations const *i_fop ; 1734 struct file_lock *i_flock ; 1735 struct address_space *i_mapping ; 1736 struct address_space i_data ; 1737 struct dquot *i_dquot[2] ; 1738 struct list_head i_devices ; 1739 union __anonunion____missing_field_name_145 __annonCompField30 ; 1740 __u32 i_generation ; 1741 __u32 i_fsnotify_mask ; 1742 struct hlist_head i_fsnotify_marks ; 1743 atomic_t i_readcount ; 1744 atomic_t i_writecount ; 1745 struct posix_acl *i_acl ; 1746 struct posix_acl *i_default_acl ; 1747 void *i_private ; 1748}; 1749#line 903 "include/linux/fs.h" 1750struct fown_struct { 1751 rwlock_t lock ; 1752 struct pid *pid ; 1753 enum pid_type pid_type ; 1754 uid_t uid ; 1755 uid_t euid ; 1756 int signum ; 1757}; 1758#line 914 "include/linux/fs.h" 1759struct file_ra_state { 1760 unsigned long start ; 1761 unsigned int size ; 1762 unsigned int async_size ; 1763 unsigned int ra_pages ; 1764 unsigned int mmap_miss ; 1765 loff_t prev_pos ; 1766}; 1767#line 937 "include/linux/fs.h" 1768union __anonunion_f_u_146 { 1769 struct list_head fu_list ; 1770 struct rcu_head fu_rcuhead ; 1771}; 1772#line 937 "include/linux/fs.h" 1773struct file { 1774 union __anonunion_f_u_146 f_u ; 1775 struct path f_path ; 1776 struct file_operations const *f_op ; 1777 spinlock_t f_lock ; 1778 int f_sb_list_cpu ; 1779 atomic_long_t f_count ; 1780 unsigned int f_flags ; 1781 fmode_t f_mode ; 1782 loff_t f_pos ; 1783 struct fown_struct f_owner ; 1784 struct cred const *f_cred ; 1785 struct file_ra_state f_ra ; 1786 u64 f_version ; 1787 void *f_security ; 1788 void *private_data ; 1789 struct list_head f_ep_links ; 1790 struct address_space *f_mapping ; 1791 unsigned long f_mnt_write_state ; 1792}; 1793#line 1064 1794struct files_struct; 1795#line 1064 1796struct files_struct; 1797#line 1064 1798struct files_struct; 1799#line 1064 "include/linux/fs.h" 1800typedef struct files_struct *fl_owner_t; 1801#line 1066 "include/linux/fs.h" 1802struct file_lock_operations { 1803 void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ; 1804 void (*fl_release_private)(struct file_lock * ) ; 1805}; 1806#line 1071 "include/linux/fs.h" 1807struct lock_manager_operations { 1808 int (*fl_compare_owner)(struct file_lock * , struct file_lock * ) ; 1809 void (*fl_notify)(struct file_lock * ) ; 1810 int (*fl_grant)(struct file_lock * , struct file_lock * , int ) ; 1811 void (*fl_release_private)(struct file_lock * ) ; 1812 void (*fl_break)(struct file_lock * ) ; 1813 int (*fl_change)(struct file_lock ** , int ) ; 1814}; 1815#line 8 "include/linux/nfs_fs_i.h" 1816struct nlm_lockowner; 1817#line 8 1818struct nlm_lockowner; 1819#line 8 1820struct nlm_lockowner; 1821#line 8 1822struct nlm_lockowner; 1823#line 13 "include/linux/nfs_fs_i.h" 1824struct nfs_lock_info { 1825 u32 state ; 1826 struct nlm_lockowner *owner ; 1827 struct list_head list ; 1828}; 1829#line 19 1830struct nfs4_lock_state; 1831#line 19 1832struct nfs4_lock_state; 1833#line 19 1834struct nfs4_lock_state; 1835#line 19 1836struct nfs4_lock_state; 1837#line 20 "include/linux/nfs_fs_i.h" 1838struct nfs4_lock_info { 1839 struct nfs4_lock_state *owner ; 1840}; 1841#line 1091 "include/linux/fs.h" 1842struct fasync_struct; 1843#line 1091 1844struct fasync_struct; 1845#line 1091 1846struct fasync_struct; 1847#line 1091 "include/linux/fs.h" 1848struct __anonstruct_afs_148 { 1849 struct list_head link ; 1850 int state ; 1851}; 1852#line 1091 "include/linux/fs.h" 1853union __anonunion_fl_u_147 { 1854 struct nfs_lock_info nfs_fl ; 1855 struct nfs4_lock_info nfs4_fl ; 1856 struct __anonstruct_afs_148 afs ; 1857}; 1858#line 1091 "include/linux/fs.h" 1859struct file_lock { 1860 struct file_lock *fl_next ; 1861 struct list_head fl_link ; 1862 struct list_head fl_block ; 1863 fl_owner_t fl_owner ; 1864 unsigned char fl_flags ; 1865 unsigned char fl_type ; 1866 unsigned int fl_pid ; 1867 struct pid *fl_nspid ; 1868 wait_queue_head_t fl_wait ; 1869 struct file *fl_file ; 1870 loff_t fl_start ; 1871 loff_t fl_end ; 1872 struct fasync_struct *fl_fasync ; 1873 unsigned long fl_break_time ; 1874 struct file_lock_operations const *fl_ops ; 1875 struct lock_manager_operations const *fl_lmops ; 1876 union __anonunion_fl_u_147 fl_u ; 1877}; 1878#line 1324 "include/linux/fs.h" 1879struct fasync_struct { 1880 spinlock_t fa_lock ; 1881 int magic ; 1882 int fa_fd ; 1883 struct fasync_struct *fa_next ; 1884 struct file *fa_file ; 1885 struct rcu_head fa_rcu ; 1886}; 1887#line 1364 1888struct file_system_type; 1889#line 1364 1890struct file_system_type; 1891#line 1364 1892struct file_system_type; 1893#line 1364 1894struct super_operations; 1895#line 1364 1896struct super_operations; 1897#line 1364 1898struct super_operations; 1899#line 1364 1900struct xattr_handler; 1901#line 1364 1902struct xattr_handler; 1903#line 1364 1904struct xattr_handler; 1905#line 1364 1906struct mtd_info; 1907#line 1364 1908struct mtd_info; 1909#line 1364 1910struct mtd_info; 1911#line 1364 "include/linux/fs.h" 1912struct super_block { 1913 struct list_head s_list ; 1914 dev_t s_dev ; 1915 unsigned char s_dirt ; 1916 unsigned char s_blocksize_bits ; 1917 unsigned long s_blocksize ; 1918 loff_t s_maxbytes ; 1919 struct file_system_type *s_type ; 1920 struct super_operations const *s_op ; 1921 struct dquot_operations const *dq_op ; 1922 struct quotactl_ops const *s_qcop ; 1923 struct export_operations const *s_export_op ; 1924 unsigned long s_flags ; 1925 unsigned long s_magic ; 1926 struct dentry *s_root ; 1927 struct rw_semaphore s_umount ; 1928 struct mutex s_lock ; 1929 int s_count ; 1930 atomic_t s_active ; 1931 void *s_security ; 1932 struct xattr_handler const **s_xattr ; 1933 struct list_head s_inodes ; 1934 struct hlist_bl_head s_anon ; 1935 struct list_head *s_files ; 1936 struct list_head s_dentry_lru ; 1937 int s_nr_dentry_unused ; 1938 struct block_device *s_bdev ; 1939 struct backing_dev_info *s_bdi ; 1940 struct mtd_info *s_mtd ; 1941 struct list_head s_instances ; 1942 struct quota_info s_dquot ; 1943 int s_frozen ; 1944 wait_queue_head_t s_wait_unfrozen ; 1945 char s_id[32] ; 1946 u8 s_uuid[16] ; 1947 void *s_fs_info ; 1948 fmode_t s_mode ; 1949 u32 s_time_gran ; 1950 struct mutex s_vfs_rename_mutex ; 1951 char *s_subtype ; 1952 char *s_options ; 1953 struct dentry_operations const *s_d_op ; 1954 int cleancache_poolid ; 1955}; 1956#line 1499 "include/linux/fs.h" 1957struct fiemap_extent_info { 1958 unsigned int fi_flags ; 1959 unsigned int fi_extents_mapped ; 1960 unsigned int fi_extents_max ; 1961 struct fiemap_extent *fi_extents_start ; 1962}; 1963#line 1546 "include/linux/fs.h" 1964struct file_operations { 1965 struct module *owner ; 1966 loff_t (*llseek)(struct file * , loff_t , int ) ; 1967 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ; 1968 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ; 1969 ssize_t (*aio_read)(struct kiocb * , struct iovec const * , unsigned long , 1970 loff_t ) ; 1971 ssize_t (*aio_write)(struct kiocb * , struct iovec const * , unsigned long , 1972 loff_t ) ; 1973 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int , 1974 loff_t , u64 , unsigned int ) ) ; 1975 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ; 1976 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ; 1977 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ; 1978 int (*mmap)(struct file * , struct vm_area_struct * ) ; 1979 int (*open)(struct inode * , struct file * ) ; 1980 int (*flush)(struct file * , fl_owner_t id ) ; 1981 int (*release)(struct inode * , struct file * ) ; 1982 int (*fsync)(struct file * , int datasync ) ; 1983 int (*aio_fsync)(struct kiocb * , int datasync ) ; 1984 int (*fasync)(int , struct file * , int ) ; 1985 int (*lock)(struct file * , int , struct file_lock * ) ; 1986 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * , 1987 int ) ; 1988 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long , 1989 unsigned long , unsigned long ) ; 1990 int (*check_flags)(int ) ; 1991 int (*flock)(struct file * , int , struct file_lock * ) ; 1992 ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t , 1993 unsigned int ) ; 1994 ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t , 1995 unsigned int ) ; 1996 int (*setlease)(struct file * , long , struct file_lock ** ) ; 1997 long (*fallocate)(struct file *file , int mode , loff_t offset , loff_t len ) ; 1998}; 1999#line 1578 "include/linux/fs.h" 2000struct inode_operations { 2001 struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ; 2002 void *(*follow_link)(struct dentry * , struct nameidata * ) ; 2003 int (*permission)(struct inode * , int , unsigned int ) ; 2004 int (*check_acl)(struct inode * , int , unsigned int ) ; 2005 int (*readlink)(struct dentry * , char * , int ) ; 2006 void (*put_link)(struct dentry * , struct nameidata * , void * ) ; 2007 int (*create)(struct inode * , struct dentry * , int , struct nameidata * ) ; 2008 int (*link)(struct dentry * , struct inode * , struct dentry * ) ; 2009 int (*unlink)(struct inode * , struct dentry * ) ; 2010 int (*symlink)(struct inode * , struct dentry * , char const * ) ; 2011 int (*mkdir)(struct inode * , struct dentry * , int ) ; 2012 int (*rmdir)(struct inode * , struct dentry * ) ; 2013 int (*mknod)(struct inode * , struct dentry * , int , dev_t ) ; 2014 int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ; 2015 void (*truncate)(struct inode * ) ; 2016 int (*setattr)(struct dentry * , struct iattr * ) ; 2017 int (*getattr)(struct vfsmount *mnt , struct dentry * , struct kstat * ) ; 2018 int (*setxattr)(struct dentry * , char const * , void const * , size_t , int ) ; 2019 ssize_t (*getxattr)(struct dentry * , char const * , void * , size_t ) ; 2020 ssize_t (*listxattr)(struct dentry * , char * , size_t ) ; 2021 int (*removexattr)(struct dentry * , char const * ) ; 2022 void (*truncate_range)(struct inode * , loff_t , loff_t ) ; 2023 int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 start , u64 len ) ; 2024} __attribute__((__aligned__((1) << (6) ))) ; 2025#line 1608 2026struct seq_file; 2027#line 1622 "include/linux/fs.h" 2028struct super_operations { 2029 struct inode *(*alloc_inode)(struct super_block *sb ) ; 2030 void (*destroy_inode)(struct inode * ) ; 2031 void (*dirty_inode)(struct inode * , int flags ) ; 2032 int (*write_inode)(struct inode * , struct writeback_control *wbc ) ; 2033 int (*drop_inode)(struct inode * ) ; 2034 void (*evict_inode)(struct inode * ) ; 2035 void (*put_super)(struct super_block * ) ; 2036 void (*write_super)(struct super_block * ) ; 2037 int (*sync_fs)(struct super_block *sb , int wait ) ; 2038 int (*freeze_fs)(struct super_block * ) ; 2039 int (*unfreeze_fs)(struct super_block * ) ; 2040 int (*statfs)(struct dentry * , struct kstatfs * ) ; 2041 int (*remount_fs)(struct super_block * , int * , char * ) ; 2042 void (*umount_begin)(struct super_block * ) ; 2043 int (*show_options)(struct seq_file * , struct vfsmount * ) ; 2044 int (*show_devname)(struct seq_file * , struct vfsmount * ) ; 2045 int (*show_path)(struct seq_file * , struct vfsmount * ) ; 2046 int (*show_stats)(struct seq_file * , struct vfsmount * ) ; 2047 ssize_t (*quota_read)(struct super_block * , int , char * , size_t , loff_t ) ; 2048 ssize_t (*quota_write)(struct super_block * , int , char const * , size_t , 2049 loff_t ) ; 2050 int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t ) ; 2051}; 2052#line 1802 "include/linux/fs.h" 2053struct file_system_type { 2054 char const *name ; 2055 int fs_flags ; 2056 struct dentry *(*mount)(struct file_system_type * , int , char const * , void * ) ; 2057 void (*kill_sb)(struct super_block * ) ; 2058 struct module *owner ; 2059 struct file_system_type *next ; 2060 struct list_head fs_supers ; 2061 struct lock_class_key s_lock_key ; 2062 struct lock_class_key s_umount_key ; 2063 struct lock_class_key s_vfs_rename_key ; 2064 struct lock_class_key i_lock_key ; 2065 struct lock_class_key i_mutex_key ; 2066 struct lock_class_key i_mutex_dir_key ; 2067 struct lock_class_key i_alloc_sem_key ; 2068}; 2069#line 6 "include/asm-generic/termbits.h" 2070typedef unsigned char cc_t; 2071#line 7 "include/asm-generic/termbits.h" 2072typedef unsigned int speed_t; 2073#line 8 "include/asm-generic/termbits.h" 2074typedef unsigned int tcflag_t; 2075#line 31 "include/asm-generic/termbits.h" 2076struct ktermios { 2077 tcflag_t c_iflag ; 2078 tcflag_t c_oflag ; 2079 tcflag_t c_cflag ; 2080 tcflag_t c_lflag ; 2081 cc_t c_line ; 2082 cc_t c_cc[19] ; 2083 speed_t c_ispeed ; 2084 speed_t c_ospeed ; 2085}; 2086#line 14 "include/asm-generic/termios.h" 2087struct winsize { 2088 unsigned short ws_row ; 2089 unsigned short ws_col ; 2090 unsigned short ws_xpixel ; 2091 unsigned short ws_ypixel ; 2092}; 2093#line 94 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/uaccess.h" 2094struct exception_table_entry { 2095 unsigned long insn ; 2096 unsigned long fixup ; 2097}; 2098#line 9 "include/linux/termios.h" 2099struct termiox { 2100 __u16 x_hflag ; 2101 __u16 x_cflag ; 2102 __u16 x_rflag[5] ; 2103 __u16 x_sflag ; 2104}; 2105#line 8 "include/linux/cdev.h" 2106struct file_operations; 2107#line 9 2108struct inode; 2109#line 10 2110struct module; 2111#line 12 "include/linux/cdev.h" 2112struct cdev { 2113 struct kobject kobj ; 2114 struct module *owner ; 2115 struct file_operations const *ops ; 2116 struct list_head list ; 2117 dev_t dev ; 2118 unsigned int count ; 2119}; 2120#line 239 "include/linux/tty_driver.h" 2121struct tty_struct; 2122#line 239 2123struct tty_struct; 2124#line 239 2125struct tty_struct; 2126#line 239 2127struct tty_struct; 2128#line 240 2129struct tty_driver; 2130#line 240 2131struct tty_driver; 2132#line 240 2133struct tty_driver; 2134#line 240 2135struct tty_driver; 2136#line 241 2137struct serial_icounter_struct; 2138#line 241 2139struct serial_icounter_struct; 2140#line 241 2141struct serial_icounter_struct; 2142#line 241 2143struct serial_icounter_struct; 2144#line 243 "include/linux/tty_driver.h" 2145struct tty_operations { 2146 struct tty_struct *(*lookup)(struct tty_driver *driver , struct inode *inode , 2147 int idx ) ; 2148 int (*install)(struct tty_driver *driver , struct tty_struct *tty ) ; 2149 void (*remove)(struct tty_driver *driver , struct tty_struct *tty ) ; 2150 int (*open)(struct tty_struct *tty , struct file *filp ) ; 2151 void (*close)(struct tty_struct *tty , struct file *filp ) ; 2152 void (*shutdown)(struct tty_struct *tty ) ; 2153 void (*cleanup)(struct tty_struct *tty ) ; 2154 int (*write)(struct tty_struct *tty , unsigned char const *buf , int count ) ; 2155 int (*put_char)(struct tty_struct *tty , unsigned char ch ) ; 2156 void (*flush_chars)(struct tty_struct *tty ) ; 2157 int (*write_room)(struct tty_struct *tty ) ; 2158 int (*chars_in_buffer)(struct tty_struct *tty ) ; 2159 int (*ioctl)(struct tty_struct *tty , unsigned int cmd , unsigned long arg ) ; 2160 long (*compat_ioctl)(struct tty_struct *tty , unsigned int cmd , unsigned long arg ) ; 2161 void (*set_termios)(struct tty_struct *tty , struct ktermios *old ) ; 2162 void (*throttle)(struct tty_struct *tty ) ; 2163 void (*unthrottle)(struct tty_struct *tty ) ; 2164 void (*stop)(struct tty_struct *tty ) ; 2165 void (*start)(struct tty_struct *tty ) ; 2166 void (*hangup)(struct tty_struct *tty ) ; 2167 int (*break_ctl)(struct tty_struct *tty , int state ) ; 2168 void (*flush_buffer)(struct tty_struct *tty ) ; 2169 void (*set_ldisc)(struct tty_struct *tty ) ; 2170 void (*wait_until_sent)(struct tty_struct *tty , int timeout ) ; 2171 void (*send_xchar)(struct tty_struct *tty , char ch ) ; 2172 int (*tiocmget)(struct tty_struct *tty ) ; 2173 int (*tiocmset)(struct tty_struct *tty , unsigned int set , unsigned int clear ) ; 2174 int (*resize)(struct tty_struct *tty , struct winsize *ws ) ; 2175 int (*set_termiox)(struct tty_struct *tty , struct termiox *tnew ) ; 2176 int (*get_icount)(struct tty_struct *tty , struct serial_icounter_struct *icount ) ; 2177 int (*poll_init)(struct tty_driver *driver , int line , char *options ) ; 2178 int (*poll_get_char)(struct tty_driver *driver , int line ) ; 2179 void (*poll_put_char)(struct tty_driver *driver , int line , char ch ) ; 2180 struct file_operations const *proc_fops ; 2181}; 2182#line 288 2183struct proc_dir_entry; 2184#line 288 2185struct proc_dir_entry; 2186#line 288 2187struct proc_dir_entry; 2188#line 288 "include/linux/tty_driver.h" 2189struct tty_driver { 2190 int magic ; 2191 struct kref kref ; 2192 struct cdev cdev ; 2193 struct module *owner ; 2194 char const *driver_name ; 2195 char const *name ; 2196 int name_base ; 2197 int major ; 2198 int minor_start ; 2199 int minor_num ; 2200 int num ; 2201 short type ; 2202 short subtype ; 2203 struct ktermios init_termios ; 2204 int flags ; 2205 struct proc_dir_entry *proc_entry ; 2206 struct tty_driver *other ; 2207 struct tty_struct **ttys ; 2208 struct ktermios **termios ; 2209 struct ktermios **termios_locked ; 2210 void *driver_state ; 2211 struct tty_operations const *ops ; 2212 struct list_head tty_drivers ; 2213}; 2214#line 19 "include/linux/klist.h" 2215struct klist_node; 2216#line 19 2217struct klist_node; 2218#line 19 2219struct klist_node; 2220#line 19 2221struct klist_node; 2222#line 39 "include/linux/klist.h" 2223struct klist_node { 2224 void *n_klist ; 2225 struct list_head n_node ; 2226 struct kref n_ref ; 2227}; 2228#line 29 "include/linux/sysctl.h" 2229struct completion; 2230#line 937 2231struct nsproxy; 2232#line 937 2233struct nsproxy; 2234#line 937 2235struct nsproxy; 2236#line 937 2237struct nsproxy; 2238#line 48 "include/linux/kmod.h" 2239struct cred; 2240#line 49 2241struct file; 2242#line 264 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/elf.h" 2243struct task_struct; 2244#line 10 "include/linux/elf.h" 2245struct file; 2246#line 27 "include/linux/elf.h" 2247typedef __u64 Elf64_Addr; 2248#line 28 "include/linux/elf.h" 2249typedef __u16 Elf64_Half; 2250#line 32 "include/linux/elf.h" 2251typedef __u32 Elf64_Word; 2252#line 33 "include/linux/elf.h" 2253typedef __u64 Elf64_Xword; 2254#line 203 "include/linux/elf.h" 2255struct elf64_sym { 2256 Elf64_Word st_name ; 2257 unsigned char st_info ; 2258 unsigned char st_other ; 2259 Elf64_Half st_shndx ; 2260 Elf64_Addr st_value ; 2261 Elf64_Xword st_size ; 2262}; 2263#line 203 "include/linux/elf.h" 2264typedef struct elf64_sym Elf64_Sym; 2265#line 34 "include/linux/moduleparam.h" 2266struct kernel_param; 2267#line 34 2268struct kernel_param; 2269#line 34 2270struct kernel_param; 2271#line 34 2272struct kernel_param; 2273#line 36 "include/linux/moduleparam.h" 2274struct kernel_param_ops { 2275 int (*set)(char const *val , struct kernel_param const *kp ) ; 2276 int (*get)(char *buffer , struct kernel_param const *kp ) ; 2277 void (*free)(void *arg ) ; 2278}; 2279#line 48 2280struct kparam_string; 2281#line 48 2282struct kparam_string; 2283#line 48 2284struct kparam_string; 2285#line 48 2286struct kparam_array; 2287#line 48 2288struct kparam_array; 2289#line 48 2290struct kparam_array; 2291#line 48 "include/linux/moduleparam.h" 2292union __anonunion____missing_field_name_211 { 2293 void *arg ; 2294 struct kparam_string const *str ; 2295 struct kparam_array const *arr ; 2296}; 2297#line 48 "include/linux/moduleparam.h" 2298struct kernel_param { 2299 char const *name ; 2300 struct kernel_param_ops const *ops ; 2301 u16 perm ; 2302 u16 flags ; 2303 union __anonunion____missing_field_name_211 __annonCompField33 ; 2304}; 2305#line 61 "include/linux/moduleparam.h" 2306struct kparam_string { 2307 unsigned int maxlen ; 2308 char *string ; 2309}; 2310#line 67 "include/linux/moduleparam.h" 2311struct kparam_array { 2312 unsigned int max ; 2313 unsigned int elemsize ; 2314 unsigned int *num ; 2315 struct kernel_param_ops const *ops ; 2316 void *elem ; 2317}; 2318#line 391 2319struct module; 2320#line 26 "include/linux/jump_label.h" 2321struct module; 2322#line 61 "include/linux/jump_label.h" 2323struct jump_label_key { 2324 atomic_t enabled ; 2325}; 2326#line 22 "include/linux/tracepoint.h" 2327struct module; 2328#line 23 2329struct tracepoint; 2330#line 23 2331struct tracepoint; 2332#line 23 2333struct tracepoint; 2334#line 23 2335struct tracepoint; 2336#line 25 "include/linux/tracepoint.h" 2337struct tracepoint_func { 2338 void *func ; 2339 void *data ; 2340}; 2341#line 30 "include/linux/tracepoint.h" 2342struct tracepoint { 2343 char const *name ; 2344 struct jump_label_key key ; 2345 void (*regfunc)(void) ; 2346 void (*unregfunc)(void) ; 2347 struct tracepoint_func *funcs ; 2348}; 2349#line 8 "include/asm-generic/module.h" 2350struct mod_arch_specific { 2351 2352}; 2353#line 21 "include/trace/events/module.h" 2354struct module; 2355#line 37 "include/linux/module.h" 2356struct kernel_symbol { 2357 unsigned long value ; 2358 char const *name ; 2359}; 2360#line 49 2361struct module; 2362#line 51 "include/linux/module.h" 2363struct module_attribute { 2364 struct attribute attr ; 2365 ssize_t (*show)(struct module_attribute * , struct module * , char * ) ; 2366 ssize_t (*store)(struct module_attribute * , struct module * , char const * , 2367 size_t count ) ; 2368 void (*setup)(struct module * , char const * ) ; 2369 int (*test)(struct module * ) ; 2370 void (*free)(struct module * ) ; 2371}; 2372#line 70 2373struct module_param_attrs; 2374#line 70 2375struct module_param_attrs; 2376#line 70 2377struct module_param_attrs; 2378#line 70 "include/linux/module.h" 2379struct module_kobject { 2380 struct kobject kobj ; 2381 struct module *mod ; 2382 struct kobject *drivers_dir ; 2383 struct module_param_attrs *mp ; 2384}; 2385#line 83 2386struct exception_table_entry; 2387#line 265 2388enum module_state { 2389 MODULE_STATE_LIVE = 0, 2390 MODULE_STATE_COMING = 1, 2391 MODULE_STATE_GOING = 2 2392} ; 2393#line 272 2394struct module_sect_attrs; 2395#line 272 2396struct module_sect_attrs; 2397#line 272 2398struct module_sect_attrs; 2399#line 272 2400struct module_notes_attrs; 2401#line 272 2402struct module_notes_attrs; 2403#line 272 2404struct module_notes_attrs; 2405#line 272 2406struct ftrace_event_call; 2407#line 272 2408struct ftrace_event_call; 2409#line 272 2410struct ftrace_event_call; 2411#line 272 "include/linux/module.h" 2412struct module_ref { 2413 unsigned int incs ; 2414 unsigned int decs ; 2415}; 2416#line 272 "include/linux/module.h" 2417struct module { 2418 enum module_state state ; 2419 struct list_head list ; 2420 char name[64UL - sizeof(unsigned long )] ; 2421 struct module_kobject mkobj ; 2422 struct module_attribute *modinfo_attrs ; 2423 char const *version ; 2424 char const *srcversion ; 2425 struct kobject *holders_dir ; 2426 struct kernel_symbol const *syms ; 2427 unsigned long const *crcs ; 2428 unsigned int num_syms ; 2429 struct kernel_param *kp ; 2430 unsigned int num_kp ; 2431 unsigned int num_gpl_syms ; 2432 struct kernel_symbol const *gpl_syms ; 2433 unsigned long const *gpl_crcs ; 2434 struct kernel_symbol const *unused_syms ; 2435 unsigned long const *unused_crcs ; 2436 unsigned int num_unused_syms ; 2437 unsigned int num_unused_gpl_syms ; 2438 struct kernel_symbol const *unused_gpl_syms ; 2439 unsigned long const *unused_gpl_crcs ; 2440 struct kernel_symbol const *gpl_future_syms ; 2441 unsigned long const *gpl_future_crcs ; 2442 unsigned int num_gpl_future_syms ; 2443 unsigned int num_exentries ; 2444 struct exception_table_entry *extable ; 2445 int (*init)(void) ; 2446 void *module_init ; 2447 void *module_core ; 2448 unsigned int init_size ; 2449 unsigned int core_size ; 2450 unsigned int init_text_size ; 2451 unsigned int core_text_size ; 2452 unsigned int init_ro_size ; 2453 unsigned int core_ro_size ; 2454 struct mod_arch_specific arch ; 2455 unsigned int taints ; 2456 unsigned int num_bugs ; 2457 struct list_head bug_list ; 2458 struct bug_entry *bug_table ; 2459 Elf64_Sym *symtab ; 2460 Elf64_Sym *core_symtab ; 2461 unsigned int num_symtab ; 2462 unsigned int core_num_syms ; 2463 char *strtab ; 2464 char *core_strtab ; 2465 struct module_sect_attrs *sect_attrs ; 2466 struct module_notes_attrs *notes_attrs ; 2467 char *args ; 2468 void *percpu ; 2469 unsigned int percpu_size ; 2470 unsigned int num_tracepoints ; 2471 struct tracepoint * const *tracepoints_ptrs ; 2472 unsigned int num_trace_bprintk_fmt ; 2473 char const **trace_bprintk_fmt_start ; 2474 struct ftrace_event_call **trace_events ; 2475 unsigned int num_trace_events ; 2476 unsigned int num_ftrace_callsites ; 2477 unsigned long *ftrace_callsites ; 2478 struct list_head source_list ; 2479 struct list_head target_list ; 2480 struct task_struct *waiter ; 2481 void (*exit)(void) ; 2482 struct module_ref *refptr ; 2483 ctor_fn_t *ctors ; 2484 unsigned int num_ctors ; 2485}; 2486#line 4 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/device.h" 2487struct dma_map_ops; 2488#line 4 2489struct dma_map_ops; 2490#line 4 2491struct dma_map_ops; 2492#line 4 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/device.h" 2493struct dev_archdata { 2494 void *acpi_handle ; 2495 struct dma_map_ops *dma_ops ; 2496 void *iommu ; 2497}; 2498#line 28 "include/linux/device.h" 2499struct device; 2500#line 29 2501struct device_private; 2502#line 29 2503struct device_private; 2504#line 29 2505struct device_private; 2506#line 29 2507struct device_private; 2508#line 30 2509struct device_driver; 2510#line 30 2511struct device_driver; 2512#line 30 2513struct device_driver; 2514#line 30 2515struct device_driver; 2516#line 31 2517struct driver_private; 2518#line 31 2519struct driver_private; 2520#line 31 2521struct driver_private; 2522#line 31 2523struct driver_private; 2524#line 32 2525struct class; 2526#line 32 2527struct class; 2528#line 32 2529struct class; 2530#line 32 2531struct class; 2532#line 33 2533struct subsys_private; 2534#line 33 2535struct subsys_private; 2536#line 33 2537struct subsys_private; 2538#line 33 2539struct subsys_private; 2540#line 34 2541struct bus_type; 2542#line 34 2543struct bus_type; 2544#line 34 2545struct bus_type; 2546#line 34 2547struct bus_type; 2548#line 35 2549struct device_node; 2550#line 35 2551struct device_node; 2552#line 35 2553struct device_node; 2554#line 35 2555struct device_node; 2556#line 37 "include/linux/device.h" 2557struct bus_attribute { 2558 struct attribute attr ; 2559 ssize_t (*show)(struct bus_type *bus , char *buf ) ; 2560 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ; 2561}; 2562#line 82 2563struct device_attribute; 2564#line 82 2565struct device_attribute; 2566#line 82 2567struct device_attribute; 2568#line 82 2569struct driver_attribute; 2570#line 82 2571struct driver_attribute; 2572#line 82 2573struct driver_attribute; 2574#line 82 "include/linux/device.h" 2575struct bus_type { 2576 char const *name ; 2577 struct bus_attribute *bus_attrs ; 2578 struct device_attribute *dev_attrs ; 2579 struct driver_attribute *drv_attrs ; 2580 int (*match)(struct device *dev , struct device_driver *drv ) ; 2581 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ; 2582 int (*probe)(struct device *dev ) ; 2583 int (*remove)(struct device *dev ) ; 2584 void (*shutdown)(struct device *dev ) ; 2585 int (*suspend)(struct device *dev , pm_message_t state ) ; 2586 int (*resume)(struct device *dev ) ; 2587 struct dev_pm_ops const *pm ; 2588 struct subsys_private *p ; 2589}; 2590#line 185 2591struct of_device_id; 2592#line 185 2593struct of_device_id; 2594#line 185 2595struct of_device_id; 2596#line 185 "include/linux/device.h" 2597struct device_driver { 2598 char const *name ; 2599 struct bus_type *bus ; 2600 struct module *owner ; 2601 char const *mod_name ; 2602 bool suppress_bind_attrs ; 2603 struct of_device_id const *of_match_table ; 2604 int (*probe)(struct device *dev ) ; 2605 int (*remove)(struct device *dev ) ; 2606 void (*shutdown)(struct device *dev ) ; 2607 int (*suspend)(struct device *dev , pm_message_t state ) ; 2608 int (*resume)(struct device *dev ) ; 2609 struct attribute_group const **groups ; 2610 struct dev_pm_ops const *pm ; 2611 struct driver_private *p ; 2612}; 2613#line 222 "include/linux/device.h" 2614struct driver_attribute { 2615 struct attribute attr ; 2616 ssize_t (*show)(struct device_driver *driver , char *buf ) ; 2617 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ; 2618}; 2619#line 280 2620struct class_attribute; 2621#line 280 2622struct class_attribute; 2623#line 280 2624struct class_attribute; 2625#line 280 "include/linux/device.h" 2626struct class { 2627 char const *name ; 2628 struct module *owner ; 2629 struct class_attribute *class_attrs ; 2630 struct device_attribute *dev_attrs ; 2631 struct bin_attribute *dev_bin_attrs ; 2632 struct kobject *dev_kobj ; 2633 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ; 2634 char *(*devnode)(struct device *dev , mode_t *mode ) ; 2635 void (*class_release)(struct class *class ) ; 2636 void (*dev_release)(struct device *dev ) ; 2637 int (*suspend)(struct device *dev , pm_message_t state ) ; 2638 int (*resume)(struct device *dev ) ; 2639 struct kobj_ns_type_operations const *ns_type ; 2640 void const *(*namespace)(struct device *dev ) ; 2641 struct dev_pm_ops const *pm ; 2642 struct subsys_private *p ; 2643}; 2644#line 306 2645struct device_type; 2646#line 306 2647struct device_type; 2648#line 306 2649struct device_type; 2650#line 347 "include/linux/device.h" 2651struct class_attribute { 2652 struct attribute attr ; 2653 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ; 2654 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf , 2655 size_t count ) ; 2656}; 2657#line 413 "include/linux/device.h" 2658struct device_type { 2659 char const *name ; 2660 struct attribute_group const **groups ; 2661 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ; 2662 char *(*devnode)(struct device *dev , mode_t *mode ) ; 2663 void (*release)(struct device *dev ) ; 2664 struct dev_pm_ops const *pm ; 2665}; 2666#line 424 "include/linux/device.h" 2667struct device_attribute { 2668 struct attribute attr ; 2669 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ; 2670 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf , 2671 size_t count ) ; 2672}; 2673#line 484 "include/linux/device.h" 2674struct device_dma_parameters { 2675 unsigned int max_segment_size ; 2676 unsigned long segment_boundary_mask ; 2677}; 2678#line 551 2679struct dma_coherent_mem; 2680#line 551 2681struct dma_coherent_mem; 2682#line 551 2683struct dma_coherent_mem; 2684#line 551 "include/linux/device.h" 2685struct device { 2686 struct device *parent ; 2687 struct device_private *p ; 2688 struct kobject kobj ; 2689 char const *init_name ; 2690 struct device_type const *type ; 2691 struct mutex mutex ; 2692 struct bus_type *bus ; 2693 struct device_driver *driver ; 2694 void *platform_data ; 2695 struct dev_pm_info power ; 2696 struct dev_power_domain *pwr_domain ; 2697 int numa_node ; 2698 u64 *dma_mask ; 2699 u64 coherent_dma_mask ; 2700 struct device_dma_parameters *dma_parms ; 2701 struct list_head dma_pools ; 2702 struct dma_coherent_mem *dma_mem ; 2703 struct dev_archdata archdata ; 2704 struct device_node *of_node ; 2705 dev_t devt ; 2706 spinlock_t devres_lock ; 2707 struct list_head devres_head ; 2708 struct klist_node knode_class ; 2709 struct class *class ; 2710 struct attribute_group const **groups ; 2711 void (*release)(struct device *dev ) ; 2712}; 2713#line 43 "include/linux/pm_wakeup.h" 2714struct wakeup_source { 2715 char *name ; 2716 struct list_head entry ; 2717 spinlock_t lock ; 2718 struct timer_list timer ; 2719 unsigned long timer_expires ; 2720 ktime_t total_time ; 2721 ktime_t max_time ; 2722 ktime_t last_time ; 2723 unsigned long event_count ; 2724 unsigned long active_count ; 2725 unsigned long relax_count ; 2726 unsigned long hit_count ; 2727 unsigned int active : 1 ; 2728}; 2729#line 49 "include/linux/pps_kernel.h" 2730struct pps_event_time { 2731 struct timespec ts_real ; 2732}; 2733#line 114 "include/linux/tty_ldisc.h" 2734struct tty_ldisc_ops { 2735 int magic ; 2736 char *name ; 2737 int num ; 2738 int flags ; 2739 int (*open)(struct tty_struct * ) ; 2740 void (*close)(struct tty_struct * ) ; 2741 void (*flush_buffer)(struct tty_struct *tty ) ; 2742 ssize_t (*chars_in_buffer)(struct tty_struct *tty ) ; 2743 ssize_t (*read)(struct tty_struct *tty , struct file *file , unsigned char *buf , 2744 size_t nr ) ; 2745 ssize_t (*write)(struct tty_struct *tty , struct file *file , unsigned char const *buf , 2746 size_t nr ) ; 2747 int (*ioctl)(struct tty_struct *tty , struct file *file , unsigned int cmd , unsigned long arg ) ; 2748 long (*compat_ioctl)(struct tty_struct *tty , struct file *file , unsigned int cmd , 2749 unsigned long arg ) ; 2750 void (*set_termios)(struct tty_struct *tty , struct ktermios *old ) ; 2751 unsigned int (*poll)(struct tty_struct * , struct file * , struct poll_table_struct * ) ; 2752 int (*hangup)(struct tty_struct *tty ) ; 2753 void (*receive_buf)(struct tty_struct * , unsigned char const *cp , char *fp , 2754 int count ) ; 2755 void (*write_wakeup)(struct tty_struct * ) ; 2756 void (*dcd_change)(struct tty_struct * , unsigned int , struct pps_event_time * ) ; 2757 struct module *owner ; 2758 int refcount ; 2759}; 2760#line 154 "include/linux/tty_ldisc.h" 2761struct tty_ldisc { 2762 struct tty_ldisc_ops *ops ; 2763 atomic_t users ; 2764}; 2765#line 63 "include/linux/tty.h" 2766struct tty_buffer { 2767 struct tty_buffer *next ; 2768 char *char_buf_ptr ; 2769 unsigned char *flag_buf_ptr ; 2770 int used ; 2771 int size ; 2772 int commit ; 2773 int read ; 2774 unsigned long data[0] ; 2775}; 2776#line 86 "include/linux/tty.h" 2777struct tty_bufhead { 2778 struct work_struct work ; 2779 spinlock_t lock ; 2780 struct tty_buffer *head ; 2781 struct tty_buffer *tail ; 2782 struct tty_buffer *free ; 2783 int memory_used ; 2784}; 2785#line 187 2786struct device; 2787#line 188 2788struct signal_struct; 2789#line 188 2790struct signal_struct; 2791#line 188 2792struct signal_struct; 2793#line 188 2794struct signal_struct; 2795#line 201 2796struct tty_port; 2797#line 201 2798struct tty_port; 2799#line 201 2800struct tty_port; 2801#line 201 2802struct tty_port; 2803#line 203 "include/linux/tty.h" 2804struct tty_port_operations { 2805 int (*carrier_raised)(struct tty_port *port ) ; 2806 void (*dtr_rts)(struct tty_port *port , int raise ) ; 2807 void (*shutdown)(struct tty_port *port ) ; 2808 void (*drop)(struct tty_port *port ) ; 2809 int (*activate)(struct tty_port *port , struct tty_struct *tty ) ; 2810 void (*destruct)(struct tty_port *port ) ; 2811}; 2812#line 222 "include/linux/tty.h" 2813struct tty_port { 2814 struct tty_struct *tty ; 2815 struct tty_port_operations const *ops ; 2816 spinlock_t lock ; 2817 int blocked_open ; 2818 int count ; 2819 wait_queue_head_t open_wait ; 2820 wait_queue_head_t close_wait ; 2821 wait_queue_head_t delta_msr_wait ; 2822 unsigned long flags ; 2823 unsigned char console : 1 ; 2824 struct mutex mutex ; 2825 struct mutex buf_mutex ; 2826 unsigned char *xmit_buf ; 2827 unsigned int close_delay ; 2828 unsigned int closing_wait ; 2829 int drain_delay ; 2830 struct kref kref ; 2831}; 2832#line 256 2833struct tty_operations; 2834#line 258 "include/linux/tty.h" 2835struct tty_struct { 2836 int magic ; 2837 struct kref kref ; 2838 struct device *dev ; 2839 struct tty_driver *driver ; 2840 struct tty_operations const *ops ; 2841 int index ; 2842 struct mutex ldisc_mutex ; 2843 struct tty_ldisc *ldisc ; 2844 struct mutex termios_mutex ; 2845 spinlock_t ctrl_lock ; 2846 struct ktermios *termios ; 2847 struct ktermios *termios_locked ; 2848 struct termiox *termiox ; 2849 char name[64] ; 2850 struct pid *pgrp ; 2851 struct pid *session ; 2852 unsigned long flags ; 2853 int count ; 2854 struct winsize winsize ; 2855 unsigned char stopped : 1 ; 2856 unsigned char hw_stopped : 1 ; 2857 unsigned char flow_stopped : 1 ; 2858 unsigned char packet : 1 ; 2859 unsigned char low_latency : 1 ; 2860 unsigned char warned : 1 ; 2861 unsigned char ctrl_status ; 2862 unsigned int receive_room ; 2863 struct tty_struct *link ; 2864 struct fasync_struct *fasync ; 2865 struct tty_bufhead buf ; 2866 int alt_speed ; 2867 wait_queue_head_t write_wait ; 2868 wait_queue_head_t read_wait ; 2869 struct work_struct hangup_work ; 2870 void *disc_data ; 2871 void *driver_data ; 2872 struct list_head tty_files ; 2873 unsigned int column ; 2874 unsigned char lnext : 1 ; 2875 unsigned char erasing : 1 ; 2876 unsigned char raw : 1 ; 2877 unsigned char real_raw : 1 ; 2878 unsigned char icanon : 1 ; 2879 unsigned char closing : 1 ; 2880 unsigned char echo_overrun : 1 ; 2881 unsigned short minimum_to_wake ; 2882 unsigned long overrun_time ; 2883 int num_overrun ; 2884 unsigned long process_char_map[256UL / (8UL * sizeof(unsigned long ))] ; 2885 char *read_buf ; 2886 int read_head ; 2887 int read_tail ; 2888 int read_cnt ; 2889 unsigned long read_flags[4096UL / (8UL * sizeof(unsigned long ))] ; 2890 unsigned char *echo_buf ; 2891 unsigned int echo_pos ; 2892 unsigned int echo_cnt ; 2893 int canon_data ; 2894 unsigned long canon_head ; 2895 unsigned int canon_column ; 2896 struct mutex atomic_read_lock ; 2897 struct mutex atomic_write_lock ; 2898 struct mutex output_lock ; 2899 struct mutex echo_lock ; 2900 unsigned char *write_buf ; 2901 int write_cnt ; 2902 spinlock_t read_lock ; 2903 struct work_struct SAK_work ; 2904 struct tty_port *port ; 2905}; 2906#line 12 "include/linux/mod_devicetable.h" 2907typedef unsigned long kernel_ulong_t; 2908#line 98 "include/linux/mod_devicetable.h" 2909struct usb_device_id { 2910 __u16 match_flags ; 2911 __u16 idVendor ; 2912 __u16 idProduct ; 2913 __u16 bcdDevice_lo ; 2914 __u16 bcdDevice_hi ; 2915 __u8 bDeviceClass ; 2916 __u8 bDeviceSubClass ; 2917 __u8 bDeviceProtocol ; 2918 __u8 bInterfaceClass ; 2919 __u8 bInterfaceSubClass ; 2920 __u8 bInterfaceProtocol ; 2921 kernel_ulong_t driver_info ; 2922}; 2923#line 219 "include/linux/mod_devicetable.h" 2924struct of_device_id { 2925 char name[32] ; 2926 char type[32] ; 2927 char compatible[128] ; 2928 void *data ; 2929}; 2930#line 244 "include/linux/usb/ch9.h" 2931struct usb_device_descriptor { 2932 __u8 bLength ; 2933 __u8 bDescriptorType ; 2934 __le16 bcdUSB ; 2935 __u8 bDeviceClass ; 2936 __u8 bDeviceSubClass ; 2937 __u8 bDeviceProtocol ; 2938 __u8 bMaxPacketSize0 ; 2939 __le16 idVendor ; 2940 __le16 idProduct ; 2941 __le16 bcdDevice ; 2942 __u8 iManufacturer ; 2943 __u8 iProduct ; 2944 __u8 iSerialNumber ; 2945 __u8 bNumConfigurations ; 2946} __attribute__((__packed__)) ; 2947#line 300 "include/linux/usb/ch9.h" 2948struct usb_config_descriptor { 2949 __u8 bLength ; 2950 __u8 bDescriptorType ; 2951 __le16 wTotalLength ; 2952 __u8 bNumInterfaces ; 2953 __u8 bConfigurationValue ; 2954 __u8 iConfiguration ; 2955 __u8 bmAttributes ; 2956 __u8 bMaxPower ; 2957} __attribute__((__packed__)) ; 2958#line 337 "include/linux/usb/ch9.h" 2959struct usb_interface_descriptor { 2960 __u8 bLength ; 2961 __u8 bDescriptorType ; 2962 __u8 bInterfaceNumber ; 2963 __u8 bAlternateSetting ; 2964 __u8 bNumEndpoints ; 2965 __u8 bInterfaceClass ; 2966 __u8 bInterfaceSubClass ; 2967 __u8 bInterfaceProtocol ; 2968 __u8 iInterface ; 2969} __attribute__((__packed__)) ; 2970#line 355 "include/linux/usb/ch9.h" 2971struct usb_endpoint_descriptor { 2972 __u8 bLength ; 2973 __u8 bDescriptorType ; 2974 __u8 bEndpointAddress ; 2975 __u8 bmAttributes ; 2976 __le16 wMaxPacketSize ; 2977 __u8 bInterval ; 2978 __u8 bRefresh ; 2979 __u8 bSynchAddress ; 2980} __attribute__((__packed__)) ; 2981#line 576 "include/linux/usb/ch9.h" 2982struct usb_ss_ep_comp_descriptor { 2983 __u8 bLength ; 2984 __u8 bDescriptorType ; 2985 __u8 bMaxBurst ; 2986 __u8 bmAttributes ; 2987 __le16 wBytesPerInterval ; 2988} __attribute__((__packed__)) ; 2989#line 637 "include/linux/usb/ch9.h" 2990struct usb_interface_assoc_descriptor { 2991 __u8 bLength ; 2992 __u8 bDescriptorType ; 2993 __u8 bFirstInterface ; 2994 __u8 bInterfaceCount ; 2995 __u8 bFunctionClass ; 2996 __u8 bFunctionSubClass ; 2997 __u8 bFunctionProtocol ; 2998 __u8 iFunction ; 2999} __attribute__((__packed__)) ; 3000#line 846 3001enum usb_device_speed { 3002 USB_SPEED_UNKNOWN = 0, 3003 USB_SPEED_LOW = 1, 3004 USB_SPEED_FULL = 2, 3005 USB_SPEED_HIGH = 3, 3006 USB_SPEED_WIRELESS = 4, 3007 USB_SPEED_SUPER = 5 3008} ; 3009#line 854 3010enum usb_device_state { 3011 USB_STATE_NOTATTACHED = 0, 3012 USB_STATE_ATTACHED = 1, 3013 USB_STATE_POWERED = 2, 3014 USB_STATE_RECONNECTING = 3, 3015 USB_STATE_UNAUTHENTICATED = 4, 3016 USB_STATE_DEFAULT = 5, 3017 USB_STATE_ADDRESS = 6, 3018 USB_STATE_CONFIGURED = 7, 3019 USB_STATE_SUSPENDED = 8 3020} ; 3021#line 10 "include/linux/irqreturn.h" 3022enum irqreturn { 3023 IRQ_NONE = 0, 3024 IRQ_HANDLED = 1, 3025 IRQ_WAKE_THREAD = 2 3026} ; 3027#line 16 "include/linux/irqreturn.h" 3028typedef enum irqreturn irqreturn_t; 3029#line 31 "include/linux/irq.h" 3030struct seq_file; 3031#line 12 "include/linux/irqdesc.h" 3032struct proc_dir_entry; 3033#line 39 3034struct irqaction; 3035#line 39 3036struct irqaction; 3037#line 39 3038struct irqaction; 3039#line 16 "include/linux/profile.h" 3040struct proc_dir_entry; 3041#line 17 3042struct pt_regs; 3043#line 65 3044struct task_struct; 3045#line 66 3046struct mm_struct; 3047#line 88 3048struct pt_regs; 3049#line 363 "include/linux/irq.h" 3050struct irqaction; 3051#line 132 "include/linux/hardirq.h" 3052struct task_struct; 3053#line 100 "include/linux/rbtree.h" 3054struct rb_node { 3055 unsigned long rb_parent_color ; 3056 struct rb_node *rb_right ; 3057 struct rb_node *rb_left ; 3058} __attribute__((__aligned__(sizeof(long )))) ; 3059#line 110 "include/linux/rbtree.h" 3060struct rb_root { 3061 struct rb_node *rb_node ; 3062}; 3063#line 8 "include/linux/timerqueue.h" 3064struct timerqueue_node { 3065 struct rb_node node ; 3066 ktime_t expires ; 3067}; 3068#line 13 "include/linux/timerqueue.h" 3069struct timerqueue_head { 3070 struct rb_root head ; 3071 struct timerqueue_node *next ; 3072}; 3073#line 27 "include/linux/hrtimer.h" 3074struct hrtimer_clock_base; 3075#line 27 3076struct hrtimer_clock_base; 3077#line 27 3078struct hrtimer_clock_base; 3079#line 27 3080struct hrtimer_clock_base; 3081#line 28 3082struct hrtimer_cpu_base; 3083#line 28 3084struct hrtimer_cpu_base; 3085#line 28 3086struct hrtimer_cpu_base; 3087#line 28 3088struct hrtimer_cpu_base; 3089#line 44 3090enum hrtimer_restart { 3091 HRTIMER_NORESTART = 0, 3092 HRTIMER_RESTART = 1 3093} ; 3094#line 108 "include/linux/hrtimer.h" 3095struct hrtimer { 3096 struct timerqueue_node node ; 3097 ktime_t _softexpires ; 3098 enum hrtimer_restart (*function)(struct hrtimer * ) ; 3099 struct hrtimer_clock_base *base ; 3100 unsigned long state ; 3101 int start_pid ; 3102 void *start_site ; 3103 char start_comm[16] ; 3104}; 3105#line 145 "include/linux/hrtimer.h" 3106struct hrtimer_clock_base { 3107 struct hrtimer_cpu_base *cpu_base ; 3108 int index ; 3109 clockid_t clockid ; 3110 struct timerqueue_head active ; 3111 ktime_t resolution ; 3112 ktime_t (*get_time)(void) ; 3113 ktime_t softirq_time ; 3114 ktime_t offset ; 3115}; 3116#line 178 "include/linux/hrtimer.h" 3117struct hrtimer_cpu_base { 3118 raw_spinlock_t lock ; 3119 unsigned long active_bases ; 3120 ktime_t expires_next ; 3121 int hres_active ; 3122 int hang_detected ; 3123 unsigned long nr_events ; 3124 unsigned long nr_retries ; 3125 unsigned long nr_hangs ; 3126 ktime_t max_hang_time ; 3127 struct hrtimer_clock_base clock_base[3] ; 3128}; 3129#line 9 "include/trace/events/irq.h" 3130struct irqaction; 3131#line 106 "include/linux/interrupt.h" 3132struct irqaction { 3133 irqreturn_t (*handler)(int , void * ) ; 3134 unsigned long flags ; 3135 void *dev_id ; 3136 struct irqaction *next ; 3137 int irq ; 3138 irqreturn_t (*thread_fn)(int , void * ) ; 3139 struct task_struct *thread ; 3140 unsigned long thread_flags ; 3141 unsigned long thread_mask ; 3142 char const *name ; 3143 struct proc_dir_entry *dir ; 3144} __attribute__((__aligned__((1) << (12) ))) ; 3145#line 172 3146struct device; 3147#line 682 3148struct seq_file; 3149#line 23 "include/linux/mm_types.h" 3150struct address_space; 3151#line 34 "include/linux/mm_types.h" 3152struct __anonstruct____missing_field_name_223 { 3153 u16 inuse ; 3154 u16 objects ; 3155}; 3156#line 34 "include/linux/mm_types.h" 3157union __anonunion____missing_field_name_222 { 3158 atomic_t _mapcount ; 3159 struct __anonstruct____missing_field_name_223 __annonCompField34 ; 3160}; 3161#line 34 "include/linux/mm_types.h" 3162struct __anonstruct____missing_field_name_225 { 3163 unsigned long private ; 3164 struct address_space *mapping ; 3165}; 3166#line 34 "include/linux/mm_types.h" 3167union __anonunion____missing_field_name_224 { 3168 struct __anonstruct____missing_field_name_225 __annonCompField36 ; 3169 struct kmem_cache *slab ; 3170 struct page *first_page ; 3171}; 3172#line 34 "include/linux/mm_types.h" 3173union __anonunion____missing_field_name_226 { 3174 unsigned long index ; 3175 void *freelist ; 3176}; 3177#line 34 "include/linux/mm_types.h" 3178struct page { 3179 unsigned long flags ; 3180 atomic_t _count ; 3181 union __anonunion____missing_field_name_222 __annonCompField35 ; 3182 union __anonunion____missing_field_name_224 __annonCompField37 ; 3183 union __anonunion____missing_field_name_226 __annonCompField38 ; 3184 struct list_head lru ; 3185}; 3186#line 132 "include/linux/mm_types.h" 3187struct __anonstruct_vm_set_228 { 3188 struct list_head list ; 3189 void *parent ; 3190 struct vm_area_struct *head ; 3191}; 3192#line 132 "include/linux/mm_types.h" 3193union __anonunion_shared_227 { 3194 struct __anonstruct_vm_set_228 vm_set ; 3195 struct raw_prio_tree_node prio_tree_node ; 3196}; 3197#line 132 3198struct anon_vma; 3199#line 132 3200struct anon_vma; 3201#line 132 3202struct anon_vma; 3203#line 132 3204struct vm_operations_struct; 3205#line 132 3206struct vm_operations_struct; 3207#line 132 3208struct vm_operations_struct; 3209#line 132 3210struct mempolicy; 3211#line 132 3212struct mempolicy; 3213#line 132 3214struct mempolicy; 3215#line 132 "include/linux/mm_types.h" 3216struct vm_area_struct { 3217 struct mm_struct *vm_mm ; 3218 unsigned long vm_start ; 3219 unsigned long vm_end ; 3220 struct vm_area_struct *vm_next ; 3221 struct vm_area_struct *vm_prev ; 3222 pgprot_t vm_page_prot ; 3223 unsigned long vm_flags ; 3224 struct rb_node vm_rb ; 3225 union __anonunion_shared_227 shared ; 3226 struct list_head anon_vma_chain ; 3227 struct anon_vma *anon_vma ; 3228 struct vm_operations_struct const *vm_ops ; 3229 unsigned long vm_pgoff ; 3230 struct file *vm_file ; 3231 void *vm_private_data ; 3232 struct mempolicy *vm_policy ; 3233}; 3234#line 189 "include/linux/mm_types.h" 3235struct core_thread { 3236 struct task_struct *task ; 3237 struct core_thread *next ; 3238}; 3239#line 194 "include/linux/mm_types.h" 3240struct core_state { 3241 atomic_t nr_threads ; 3242 struct core_thread dumper ; 3243 struct completion startup ; 3244}; 3245#line 216 "include/linux/mm_types.h" 3246struct mm_rss_stat { 3247 atomic_long_t count[3] ; 3248}; 3249#line 220 3250struct linux_binfmt; 3251#line 220 3252struct linux_binfmt; 3253#line 220 3254struct linux_binfmt; 3255#line 220 3256struct mmu_notifier_mm; 3257#line 220 3258struct mmu_notifier_mm; 3259#line 220 3260struct mmu_notifier_mm; 3261#line 220 "include/linux/mm_types.h" 3262struct mm_struct { 3263 struct vm_area_struct *mmap ; 3264 struct rb_root mm_rb ; 3265 struct vm_area_struct *mmap_cache ; 3266 unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len , 3267 unsigned long pgoff , unsigned long flags ) ; 3268 void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ; 3269 unsigned long mmap_base ; 3270 unsigned long task_size ; 3271 unsigned long cached_hole_size ; 3272 unsigned long free_area_cache ; 3273 pgd_t *pgd ; 3274 atomic_t mm_users ; 3275 atomic_t mm_count ; 3276 int map_count ; 3277 spinlock_t page_table_lock ; 3278 struct rw_semaphore mmap_sem ; 3279 struct list_head mmlist ; 3280 unsigned long hiwater_rss ; 3281 unsigned long hiwater_vm ; 3282 unsigned long total_vm ; 3283 unsigned long locked_vm ; 3284 unsigned long shared_vm ; 3285 unsigned long exec_vm ; 3286 unsigned long stack_vm ; 3287 unsigned long reserved_vm ; 3288 unsigned long def_flags ; 3289 unsigned long nr_ptes ; 3290 unsigned long start_code ; 3291 unsigned long end_code ; 3292 unsigned long start_data ; 3293 unsigned long end_data ; 3294 unsigned long start_brk ; 3295 unsigned long brk ; 3296 unsigned long start_stack ; 3297 unsigned long arg_start ; 3298 unsigned long arg_end ; 3299 unsigned long env_start ; 3300 unsigned long env_end ; 3301 unsigned long saved_auxv[44] ; 3302 struct mm_rss_stat rss_stat ; 3303 struct linux_binfmt *binfmt ; 3304 cpumask_var_t cpu_vm_mask_var ; 3305 mm_context_t context ; 3306 unsigned int faultstamp ; 3307 unsigned int token_priority ; 3308 unsigned int last_interval ; 3309 atomic_t oom_disable_count ; 3310 unsigned long flags ; 3311 struct core_state *core_state ; 3312 spinlock_t ioctx_lock ; 3313 struct hlist_head ioctx_list ; 3314 struct task_struct *owner ; 3315 struct file *exe_file ; 3316 unsigned long num_exe_file_vmas ; 3317 struct mmu_notifier_mm *mmu_notifier_mm ; 3318 pgtable_t pmd_huge_pte ; 3319 struct cpumask cpumask_allocation ; 3320}; 3321#line 7 "include/asm-generic/cputime.h" 3322typedef unsigned long cputime_t; 3323#line 84 "include/linux/sem.h" 3324struct task_struct; 3325#line 122 3326struct sem_undo_list; 3327#line 122 3328struct sem_undo_list; 3329#line 122 3330struct sem_undo_list; 3331#line 135 "include/linux/sem.h" 3332struct sem_undo_list { 3333 atomic_t refcnt ; 3334 spinlock_t lock ; 3335 struct list_head list_proc ; 3336}; 3337#line 141 "include/linux/sem.h" 3338struct sysv_sem { 3339 struct sem_undo_list *undo_list ; 3340}; 3341#line 10 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h" 3342struct siginfo; 3343#line 10 3344struct siginfo; 3345#line 10 3346struct siginfo; 3347#line 10 3348struct siginfo; 3349#line 30 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h" 3350struct __anonstruct_sigset_t_230 { 3351 unsigned long sig[1] ; 3352}; 3353#line 30 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h" 3354typedef struct __anonstruct_sigset_t_230 sigset_t; 3355#line 17 "include/asm-generic/signal-defs.h" 3356typedef void __signalfn_t(int ); 3357#line 18 "include/asm-generic/signal-defs.h" 3358typedef __signalfn_t *__sighandler_t; 3359#line 20 "include/asm-generic/signal-defs.h" 3360typedef void __restorefn_t(void); 3361#line 21 "include/asm-generic/signal-defs.h" 3362typedef __restorefn_t *__sigrestore_t; 3363#line 167 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h" 3364struct sigaction { 3365 __sighandler_t sa_handler ; 3366 unsigned long sa_flags ; 3367 __sigrestore_t sa_restorer ; 3368 sigset_t sa_mask ; 3369}; 3370#line 174 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/signal.h" 3371struct k_sigaction { 3372 struct sigaction sa ; 3373}; 3374#line 7 "include/asm-generic/siginfo.h" 3375union sigval { 3376 int sival_int ; 3377 void *sival_ptr ; 3378}; 3379#line 7 "include/asm-generic/siginfo.h" 3380typedef union sigval sigval_t; 3381#line 40 "include/asm-generic/siginfo.h" 3382struct __anonstruct__kill_232 { 3383 __kernel_pid_t _pid ; 3384 __kernel_uid32_t _uid ; 3385}; 3386#line 40 "include/asm-generic/siginfo.h" 3387struct __anonstruct__timer_233 { 3388 __kernel_timer_t _tid ; 3389 int _overrun ; 3390 char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ; 3391 sigval_t _sigval ; 3392 int _sys_private ; 3393}; 3394#line 40 "include/asm-generic/siginfo.h" 3395struct __anonstruct__rt_234 { 3396 __kernel_pid_t _pid ; 3397 __kernel_uid32_t _uid ; 3398 sigval_t _sigval ; 3399}; 3400#line 40 "include/asm-generic/siginfo.h" 3401struct __anonstruct__sigchld_235 { 3402 __kernel_pid_t _pid ; 3403 __kernel_uid32_t _uid ; 3404 int _status ; 3405 __kernel_clock_t _utime ; 3406 __kernel_clock_t _stime ; 3407}; 3408#line 40 "include/asm-generic/siginfo.h" 3409struct __anonstruct__sigfault_236 { 3410 void *_addr ; 3411 short _addr_lsb ; 3412}; 3413#line 40 "include/asm-generic/siginfo.h" 3414struct __anonstruct__sigpoll_237 { 3415 long _band ; 3416 int _fd ; 3417}; 3418#line 40 "include/asm-generic/siginfo.h" 3419union __anonunion__sifields_231 { 3420 int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ; 3421 struct __anonstruct__kill_232 _kill ; 3422 struct __anonstruct__timer_233 _timer ; 3423 struct __anonstruct__rt_234 _rt ; 3424 struct __anonstruct__sigchld_235 _sigchld ; 3425 struct __anonstruct__sigfault_236 _sigfault ; 3426 struct __anonstruct__sigpoll_237 _sigpoll ; 3427}; 3428#line 40 "include/asm-generic/siginfo.h" 3429struct siginfo { 3430 int si_signo ; 3431 int si_errno ; 3432 int si_code ; 3433 union __anonunion__sifields_231 _sifields ; 3434}; 3435#line 40 "include/asm-generic/siginfo.h" 3436typedef struct siginfo siginfo_t; 3437#line 280 3438struct siginfo; 3439#line 10 "include/linux/signal.h" 3440struct task_struct; 3441#line 18 3442struct user_struct; 3443#line 18 3444struct user_struct; 3445#line 18 3446struct user_struct; 3447#line 28 "include/linux/signal.h" 3448struct sigpending { 3449 struct list_head list ; 3450 sigset_t signal ; 3451}; 3452#line 239 3453struct timespec; 3454#line 240 3455struct pt_regs; 3456#line 97 "include/linux/proportions.h" 3457struct prop_local_single { 3458 unsigned long events ; 3459 unsigned long period ; 3460 int shift ; 3461 spinlock_t lock ; 3462}; 3463#line 10 "include/linux/seccomp.h" 3464struct __anonstruct_seccomp_t_240 { 3465 int mode ; 3466}; 3467#line 10 "include/linux/seccomp.h" 3468typedef struct __anonstruct_seccomp_t_240 seccomp_t; 3469#line 82 "include/linux/plist.h" 3470struct plist_head { 3471 struct list_head node_list ; 3472 raw_spinlock_t *rawlock ; 3473 spinlock_t *spinlock ; 3474}; 3475#line 90 "include/linux/plist.h" 3476struct plist_node { 3477 int prio ; 3478 struct list_head prio_list ; 3479 struct list_head node_list ; 3480}; 3481#line 40 "include/linux/rtmutex.h" 3482struct rt_mutex_waiter; 3483#line 40 3484struct rt_mutex_waiter; 3485#line 40 3486struct rt_mutex_waiter; 3487#line 40 3488struct rt_mutex_waiter; 3489#line 42 "include/linux/resource.h" 3490struct rlimit { 3491 unsigned long rlim_cur ; 3492 unsigned long rlim_max ; 3493}; 3494#line 81 3495struct task_struct; 3496#line 11 "include/linux/task_io_accounting.h" 3497struct task_io_accounting { 3498 u64 rchar ; 3499 u64 wchar ; 3500 u64 syscr ; 3501 u64 syscw ; 3502 u64 read_bytes ; 3503 u64 write_bytes ; 3504 u64 cancelled_write_bytes ; 3505}; 3506#line 18 "include/linux/latencytop.h" 3507struct latency_record { 3508 unsigned long backtrace[12] ; 3509 unsigned int count ; 3510 unsigned long time ; 3511 unsigned long max ; 3512}; 3513#line 26 3514struct task_struct; 3515#line 29 "include/linux/key.h" 3516typedef int32_t key_serial_t; 3517#line 32 "include/linux/key.h" 3518typedef uint32_t key_perm_t; 3519#line 34 3520struct key; 3521#line 34 3522struct key; 3523#line 34 3524struct key; 3525#line 34 3526struct key; 3527#line 74 3528struct seq_file; 3529#line 75 3530struct user_struct; 3531#line 76 3532struct signal_struct; 3533#line 77 3534struct cred; 3535#line 79 3536struct key_type; 3537#line 79 3538struct key_type; 3539#line 79 3540struct key_type; 3541#line 79 3542struct key_type; 3543#line 81 3544struct keyring_list; 3545#line 81 3546struct keyring_list; 3547#line 81 3548struct keyring_list; 3549#line 81 3550struct keyring_list; 3551#line 124 3552struct key_user; 3553#line 124 3554struct key_user; 3555#line 124 3556struct key_user; 3557#line 124 "include/linux/key.h" 3558union __anonunion____missing_field_name_241 { 3559 time_t expiry ; 3560 time_t revoked_at ; 3561}; 3562#line 124 "include/linux/key.h" 3563union __anonunion_type_data_242 { 3564 struct list_head link ; 3565 unsigned long x[2] ; 3566 void *p[2] ; 3567 int reject_error ; 3568}; 3569#line 124 "include/linux/key.h" 3570union __anonunion_payload_243 { 3571 unsigned long value ; 3572 void *rcudata ; 3573 void *data ; 3574 struct keyring_list *subscriptions ; 3575}; 3576#line 124 "include/linux/key.h" 3577struct key { 3578 atomic_t usage ; 3579 key_serial_t serial ; 3580 struct rb_node serial_node ; 3581 struct key_type *type ; 3582 struct rw_semaphore sem ; 3583 struct key_user *user ; 3584 void *security ; 3585 union __anonunion____missing_field_name_241 __annonCompField39 ; 3586 uid_t uid ; 3587 gid_t gid ; 3588 key_perm_t perm ; 3589 unsigned short quotalen ; 3590 unsigned short datalen ; 3591 unsigned long flags ; 3592 char *description ; 3593 union __anonunion_type_data_242 type_data ; 3594 union __anonunion_payload_243 payload ; 3595}; 3596#line 18 "include/linux/selinux.h" 3597struct audit_context; 3598#line 18 3599struct audit_context; 3600#line 18 3601struct audit_context; 3602#line 18 3603struct audit_context; 3604#line 21 "include/linux/cred.h" 3605struct user_struct; 3606#line 22 3607struct cred; 3608#line 23 3609struct inode; 3610#line 31 "include/linux/cred.h" 3611struct group_info { 3612 atomic_t usage ; 3613 int ngroups ; 3614 int nblocks ; 3615 gid_t small_block[32] ; 3616 gid_t *blocks[0] ; 3617}; 3618#line 83 "include/linux/cred.h" 3619struct thread_group_cred { 3620 atomic_t usage ; 3621 pid_t tgid ; 3622 spinlock_t lock ; 3623 struct key *session_keyring ; 3624 struct key *process_keyring ; 3625 struct rcu_head rcu ; 3626}; 3627#line 116 "include/linux/cred.h" 3628struct cred { 3629 atomic_t usage ; 3630 atomic_t subscribers ; 3631 void *put_addr ; 3632 unsigned int magic ; 3633 uid_t uid ; 3634 gid_t gid ; 3635 uid_t suid ; 3636 gid_t sgid ; 3637 uid_t euid ; 3638 gid_t egid ; 3639 uid_t fsuid ; 3640 gid_t fsgid ; 3641 unsigned int securebits ; 3642 kernel_cap_t cap_inheritable ; 3643 kernel_cap_t cap_permitted ; 3644 kernel_cap_t cap_effective ; 3645 kernel_cap_t cap_bset ; 3646 unsigned char jit_keyring ; 3647 struct key *thread_keyring ; 3648 struct key *request_key_auth ; 3649 struct thread_group_cred *tgcred ; 3650 void *security ; 3651 struct user_struct *user ; 3652 struct user_namespace *user_ns ; 3653 struct group_info *group_info ; 3654 struct rcu_head rcu ; 3655}; 3656#line 97 "include/linux/sched.h" 3657struct futex_pi_state; 3658#line 97 3659struct futex_pi_state; 3660#line 97 3661struct futex_pi_state; 3662#line 97 3663struct futex_pi_state; 3664#line 98 3665struct robust_list_head; 3666#line 98 3667struct robust_list_head; 3668#line 98 3669struct robust_list_head; 3670#line 98 3671struct robust_list_head; 3672#line 99 3673struct bio_list; 3674#line 99 3675struct bio_list; 3676#line 99 3677struct bio_list; 3678#line 99 3679struct bio_list; 3680#line 100 3681struct fs_struct; 3682#line 100 3683struct fs_struct; 3684#line 100 3685struct fs_struct; 3686#line 100 3687struct fs_struct; 3688#line 101 3689struct perf_event_context; 3690#line 101 3691struct perf_event_context; 3692#line 101 3693struct perf_event_context; 3694#line 101 3695struct perf_event_context; 3696#line 102 3697struct blk_plug; 3698#line 102 3699struct blk_plug; 3700#line 102 3701struct blk_plug; 3702#line 102 3703struct blk_plug; 3704#line 150 3705struct seq_file; 3706#line 151 3707struct cfs_rq; 3708#line 151 3709struct cfs_rq; 3710#line 151 3711struct cfs_rq; 3712#line 151 3713struct cfs_rq; 3714#line 259 3715struct task_struct; 3716#line 364 3717struct nsproxy; 3718#line 365 3719struct user_namespace; 3720#line 58 "include/linux/aio_abi.h" 3721struct io_event { 3722 __u64 data ; 3723 __u64 obj ; 3724 __s64 res ; 3725 __s64 res2 ; 3726}; 3727#line 16 "include/linux/uio.h" 3728struct iovec { 3729 void *iov_base ; 3730 __kernel_size_t iov_len ; 3731}; 3732#line 15 "include/linux/aio.h" 3733struct kioctx; 3734#line 15 3735struct kioctx; 3736#line 15 3737struct kioctx; 3738#line 15 3739struct kioctx; 3740#line 87 "include/linux/aio.h" 3741union __anonunion_ki_obj_245 { 3742 void *user ; 3743 struct task_struct *tsk ; 3744}; 3745#line 87 3746struct eventfd_ctx; 3747#line 87 3748struct eventfd_ctx; 3749#line 87 3750struct eventfd_ctx; 3751#line 87 "include/linux/aio.h" 3752struct kiocb { 3753 struct list_head ki_run_list ; 3754 unsigned long ki_flags ; 3755 int ki_users ; 3756 unsigned int ki_key ; 3757 struct file *ki_filp ; 3758 struct kioctx *ki_ctx ; 3759 int (*ki_cancel)(struct kiocb * , struct io_event * ) ; 3760 ssize_t (*ki_retry)(struct kiocb * ) ; 3761 void (*ki_dtor)(struct kiocb * ) ; 3762 union __anonunion_ki_obj_245 ki_obj ; 3763 __u64 ki_user_data ; 3764 loff_t ki_pos ; 3765 void *private ; 3766 unsigned short ki_opcode ; 3767 size_t ki_nbytes ; 3768 char *ki_buf ; 3769 size_t ki_left ; 3770 struct iovec ki_inline_vec ; 3771 struct iovec *ki_iovec ; 3772 unsigned long ki_nr_segs ; 3773 unsigned long ki_cur_seg ; 3774 struct list_head ki_list ; 3775 struct eventfd_ctx *ki_eventfd ; 3776}; 3777#line 165 "include/linux/aio.h" 3778struct aio_ring_info { 3779 unsigned long mmap_base ; 3780 unsigned long mmap_size ; 3781 struct page **ring_pages ; 3782 spinlock_t ring_lock ; 3783 long nr_pages ; 3784 unsigned int nr ; 3785 unsigned int tail ; 3786 struct page *internal_pages[8] ; 3787}; 3788#line 178 "include/linux/aio.h" 3789struct kioctx { 3790 atomic_t users ; 3791 int dead ; 3792 struct mm_struct *mm ; 3793 unsigned long user_id ; 3794 struct hlist_node list ; 3795 wait_queue_head_t wait ; 3796 spinlock_t ctx_lock ; 3797 int reqs_active ; 3798 struct list_head active_reqs ; 3799 struct list_head run_list ; 3800 unsigned int max_reqs ; 3801 struct aio_ring_info ring_info ; 3802 struct delayed_work wq ; 3803 struct rcu_head rcu_head ; 3804}; 3805#line 213 3806struct mm_struct; 3807#line 441 "include/linux/sched.h" 3808struct sighand_struct { 3809 atomic_t count ; 3810 struct k_sigaction action[64] ; 3811 spinlock_t siglock ; 3812 wait_queue_head_t signalfd_wqh ; 3813}; 3814#line 448 "include/linux/sched.h" 3815struct pacct_struct { 3816 int ac_flag ; 3817 long ac_exitcode ; 3818 unsigned long ac_mem ; 3819 cputime_t ac_utime ; 3820 cputime_t ac_stime ; 3821 unsigned long ac_minflt ; 3822 unsigned long ac_majflt ; 3823}; 3824#line 456 "include/linux/sched.h" 3825struct cpu_itimer { 3826 cputime_t expires ; 3827 cputime_t incr ; 3828 u32 error ; 3829 u32 incr_error ; 3830}; 3831#line 474 "include/linux/sched.h" 3832struct task_cputime { 3833 cputime_t utime ; 3834 cputime_t stime ; 3835 unsigned long long sum_exec_runtime ; 3836}; 3837#line 510 "include/linux/sched.h" 3838struct thread_group_cputimer { 3839 struct task_cputime cputime ; 3840 int running ; 3841 spinlock_t lock ; 3842}; 3843#line 517 3844struct autogroup; 3845#line 517 3846struct autogroup; 3847#line 517 3848struct autogroup; 3849#line 517 3850struct autogroup; 3851#line 526 3852struct taskstats; 3853#line 526 3854struct taskstats; 3855#line 526 3856struct taskstats; 3857#line 526 3858struct tty_audit_buf; 3859#line 526 3860struct tty_audit_buf; 3861#line 526 3862struct tty_audit_buf; 3863#line 526 "include/linux/sched.h" 3864struct signal_struct { 3865 atomic_t sigcnt ; 3866 atomic_t live ; 3867 int nr_threads ; 3868 wait_queue_head_t wait_chldexit ; 3869 struct task_struct *curr_target ; 3870 struct sigpending shared_pending ; 3871 int group_exit_code ; 3872 int notify_count ; 3873 struct task_struct *group_exit_task ; 3874 int group_stop_count ; 3875 unsigned int flags ; 3876 struct list_head posix_timers ; 3877 struct hrtimer real_timer ; 3878 struct pid *leader_pid ; 3879 ktime_t it_real_incr ; 3880 struct cpu_itimer it[2] ; 3881 struct thread_group_cputimer cputimer ; 3882 struct task_cputime cputime_expires ; 3883 struct list_head cpu_timers[3] ; 3884 struct pid *tty_old_pgrp ; 3885 int leader ; 3886 struct tty_struct *tty ; 3887 struct autogroup *autogroup ; 3888 cputime_t utime ; 3889 cputime_t stime ; 3890 cputime_t cutime ; 3891 cputime_t cstime ; 3892 cputime_t gtime ; 3893 cputime_t cgtime ; 3894 cputime_t prev_utime ; 3895 cputime_t prev_stime ; 3896 unsigned long nvcsw ; 3897 unsigned long nivcsw ; 3898 unsigned long cnvcsw ; 3899 unsigned long cnivcsw ; 3900 unsigned long min_flt ; 3901 unsigned long maj_flt ; 3902 unsigned long cmin_flt ; 3903 unsigned long cmaj_flt ; 3904 unsigned long inblock ; 3905 unsigned long oublock ; 3906 unsigned long cinblock ; 3907 unsigned long coublock ; 3908 unsigned long maxrss ; 3909 unsigned long cmaxrss ; 3910 struct task_io_accounting ioac ; 3911 unsigned long long sum_sched_runtime ; 3912 struct rlimit rlim[16] ; 3913 struct pacct_struct pacct ; 3914 struct taskstats *stats ; 3915 unsigned int audit_tty ; 3916 struct tty_audit_buf *tty_audit_buf ; 3917 struct rw_semaphore threadgroup_fork_lock ; 3918 int oom_adj ; 3919 int oom_score_adj ; 3920 int oom_score_adj_min ; 3921 struct mutex cred_guard_mutex ; 3922}; 3923#line 687 "include/linux/sched.h" 3924struct user_struct { 3925 atomic_t __count ; 3926 atomic_t processes ; 3927 atomic_t files ; 3928 atomic_t sigpending ; 3929 atomic_t inotify_watches ; 3930 atomic_t inotify_devs ; 3931 atomic_t fanotify_listeners ; 3932 atomic_long_t epoll_watches ; 3933 unsigned long mq_bytes ; 3934 unsigned long locked_shm ; 3935 struct key *uid_keyring ; 3936 struct key *session_keyring ; 3937 struct hlist_node uidhash_node ; 3938 uid_t uid ; 3939 struct user_namespace *user_ns ; 3940 atomic_long_t locked_vm ; 3941}; 3942#line 731 3943struct backing_dev_info; 3944#line 732 3945struct reclaim_state; 3946#line 732 3947struct reclaim_state; 3948#line 732 3949struct reclaim_state; 3950#line 732 3951struct reclaim_state; 3952#line 735 "include/linux/sched.h" 3953struct sched_info { 3954 unsigned long pcount ; 3955 unsigned long long run_delay ; 3956 unsigned long long last_arrival ; 3957 unsigned long long last_queued ; 3958}; 3959#line 747 "include/linux/sched.h" 3960struct task_delay_info { 3961 spinlock_t lock ; 3962 unsigned int flags ; 3963 struct timespec blkio_start ; 3964 struct timespec blkio_end ; 3965 u64 blkio_delay ; 3966 u64 swapin_delay ; 3967 u32 blkio_count ; 3968 u32 swapin_count ; 3969 struct timespec freepages_start ; 3970 struct timespec freepages_end ; 3971 u64 freepages_delay ; 3972 u32 freepages_count ; 3973}; 3974#line 1050 3975struct io_context; 3976#line 1050 3977struct io_context; 3978#line 1050 3979struct io_context; 3980#line 1050 3981struct io_context; 3982#line 1059 3983struct audit_context; 3984#line 1060 3985struct mempolicy; 3986#line 1061 3987struct pipe_inode_info; 3988#line 1064 3989struct rq; 3990#line 1064 3991struct rq; 3992#line 1064 3993struct rq; 3994#line 1064 3995struct rq; 3996#line 1084 "include/linux/sched.h" 3997struct sched_class { 3998 struct sched_class const *next ; 3999 void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ; 4000 void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ; 4001 void (*yield_task)(struct rq *rq ) ; 4002 bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ; 4003 void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ; 4004 struct task_struct *(*pick_next_task)(struct rq *rq ) ; 4005 void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ; 4006 int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ; 4007 void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ; 4008 void (*post_schedule)(struct rq *this_rq ) ; 4009 void (*task_waking)(struct task_struct *task ) ; 4010 void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ; 4011 void (*set_cpus_allowed)(struct task_struct *p , struct cpumask const *newmask ) ; 4012 void (*rq_online)(struct rq *rq ) ; 4013 void (*rq_offline)(struct rq *rq ) ; 4014 void (*set_curr_task)(struct rq *rq ) ; 4015 void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ; 4016 void (*task_fork)(struct task_struct *p ) ; 4017 void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ; 4018 void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ; 4019 void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ; 4020 unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ; 4021 void (*task_move_group)(struct task_struct *p , int on_rq ) ; 4022}; 4023#line 1129 "include/linux/sched.h" 4024struct load_weight { 4025 unsigned long weight ; 4026 unsigned long inv_weight ; 4027}; 4028#line 1134 "include/linux/sched.h" 4029struct sched_statistics { 4030 u64 wait_start ; 4031 u64 wait_max ; 4032 u64 wait_count ; 4033 u64 wait_sum ; 4034 u64 iowait_count ; 4035 u64 iowait_sum ; 4036 u64 sleep_start ; 4037 u64 sleep_max ; 4038 s64 sum_sleep_runtime ; 4039 u64 block_start ; 4040 u64 block_max ; 4041 u64 exec_max ; 4042 u64 slice_max ; 4043 u64 nr_migrations_cold ; 4044 u64 nr_failed_migrations_affine ; 4045 u64 nr_failed_migrations_running ; 4046 u64 nr_failed_migrations_hot ; 4047 u64 nr_forced_migrations ; 4048 u64 nr_wakeups ; 4049 u64 nr_wakeups_sync ; 4050 u64 nr_wakeups_migrate ; 4051 u64 nr_wakeups_local ; 4052 u64 nr_wakeups_remote ; 4053 u64 nr_wakeups_affine ; 4054 u64 nr_wakeups_affine_attempts ; 4055 u64 nr_wakeups_passive ; 4056 u64 nr_wakeups_idle ; 4057}; 4058#line 1169 "include/linux/sched.h" 4059struct sched_entity { 4060 struct load_weight load ; 4061 struct rb_node run_node ; 4062 struct list_head group_node ; 4063 unsigned int on_rq ; 4064 u64 exec_start ; 4065 u64 sum_exec_runtime ; 4066 u64 vruntime ; 4067 u64 prev_sum_exec_runtime ; 4068 u64 nr_migrations ; 4069 struct sched_statistics statistics ; 4070 struct sched_entity *parent ; 4071 struct cfs_rq *cfs_rq ; 4072 struct cfs_rq *my_q ; 4073}; 4074#line 1195 4075struct rt_rq; 4076#line 1195 4077struct rt_rq; 4078#line 1195 4079struct rt_rq; 4080#line 1195 "include/linux/sched.h" 4081struct sched_rt_entity { 4082 struct list_head run_list ; 4083 unsigned long timeout ; 4084 unsigned int time_slice ; 4085 int nr_cpus_allowed ; 4086 struct sched_rt_entity *back ; 4087 struct sched_rt_entity *parent ; 4088 struct rt_rq *rt_rq ; 4089 struct rt_rq *my_q ; 4090}; 4091#line 1220 4092struct css_set; 4093#line 1220 4094struct css_set; 4095#line 1220 4096struct css_set; 4097#line 1220 4098struct compat_robust_list_head; 4099#line 1220 4100struct compat_robust_list_head; 4101#line 1220 4102struct compat_robust_list_head; 4103#line 1220 4104struct ftrace_ret_stack; 4105#line 1220 4106struct ftrace_ret_stack; 4107#line 1220 4108struct ftrace_ret_stack; 4109#line 1220 4110struct mem_cgroup; 4111#line 1220 4112struct mem_cgroup; 4113#line 1220 4114struct mem_cgroup; 4115#line 1220 "include/linux/sched.h" 4116struct memcg_batch_info { 4117 int do_batch ; 4118 struct mem_cgroup *memcg ; 4119 unsigned long nr_pages ; 4120 unsigned long memsw_nr_pages ; 4121}; 4122#line 1220 "include/linux/sched.h" 4123struct task_struct { 4124 long volatile state ; 4125 void *stack ; 4126 atomic_t usage ; 4127 unsigned int flags ; 4128 unsigned int ptrace ; 4129 struct task_struct *wake_entry ; 4130 int on_cpu ; 4131 int on_rq ; 4132 int prio ; 4133 int static_prio ; 4134 int normal_prio ; 4135 unsigned int rt_priority ; 4136 struct sched_class const *sched_class ; 4137 struct sched_entity se ; 4138 struct sched_rt_entity rt ; 4139 struct hlist_head preempt_notifiers ; 4140 unsigned char fpu_counter ; 4141 unsigned int btrace_seq ; 4142 unsigned int policy ; 4143 cpumask_t cpus_allowed ; 4144 struct sched_info sched_info ; 4145 struct list_head tasks ; 4146 struct plist_node pushable_tasks ; 4147 struct mm_struct *mm ; 4148 struct mm_struct *active_mm ; 4149 unsigned int brk_randomized : 1 ; 4150 int exit_state ; 4151 int exit_code ; 4152 int exit_signal ; 4153 int pdeath_signal ; 4154 unsigned int group_stop ; 4155 unsigned int personality ; 4156 unsigned int did_exec : 1 ; 4157 unsigned int in_execve : 1 ; 4158 unsigned int in_iowait : 1 ; 4159 unsigned int sched_reset_on_fork : 1 ; 4160 unsigned int sched_contributes_to_load : 1 ; 4161 pid_t pid ; 4162 pid_t tgid ; 4163 unsigned long stack_canary ; 4164 struct task_struct *real_parent ; 4165 struct task_struct *parent ; 4166 struct list_head children ; 4167 struct list_head sibling ; 4168 struct task_struct *group_leader ; 4169 struct list_head ptraced ; 4170 struct list_head ptrace_entry ; 4171 struct pid_link pids[3] ; 4172 struct list_head thread_group ; 4173 struct completion *vfork_done ; 4174 int *set_child_tid ; 4175 int *clear_child_tid ; 4176 cputime_t utime ; 4177 cputime_t stime ; 4178 cputime_t utimescaled ; 4179 cputime_t stimescaled ; 4180 cputime_t gtime ; 4181 cputime_t prev_utime ; 4182 cputime_t prev_stime ; 4183 unsigned long nvcsw ; 4184 unsigned long nivcsw ; 4185 struct timespec start_time ; 4186 struct timespec real_start_time ; 4187 unsigned long min_flt ; 4188 unsigned long maj_flt ; 4189 struct task_cputime cputime_expires ; 4190 struct list_head cpu_timers[3] ; 4191 struct cred const *real_cred ; 4192 struct cred const *cred ; 4193 struct cred *replacement_session_keyring ; 4194 char comm[16] ; 4195 int link_count ; 4196 int total_link_count ; 4197 struct sysv_sem sysvsem ; 4198 unsigned long last_switch_count ; 4199 struct thread_struct thread ; 4200 struct fs_struct *fs ; 4201 struct files_struct *files ; 4202 struct nsproxy *nsproxy ; 4203 struct signal_struct *signal ; 4204 struct sighand_struct *sighand ; 4205 sigset_t blocked ; 4206 sigset_t real_blocked ; 4207 sigset_t saved_sigmask ; 4208 struct sigpending pending ; 4209 unsigned long sas_ss_sp ; 4210 size_t sas_ss_size ; 4211 int (*notifier)(void *priv ) ; 4212 void *notifier_data ; 4213 sigset_t *notifier_mask ; 4214 struct audit_context *audit_context ; 4215 uid_t loginuid ; 4216 unsigned int sessionid ; 4217 seccomp_t seccomp ; 4218 u32 parent_exec_id ; 4219 u32 self_exec_id ; 4220 spinlock_t alloc_lock ; 4221 struct irqaction *irqaction ; 4222 raw_spinlock_t pi_lock ; 4223 struct plist_head pi_waiters ; 4224 struct rt_mutex_waiter *pi_blocked_on ; 4225 struct mutex_waiter *blocked_on ; 4226 unsigned int irq_events ; 4227 unsigned long hardirq_enable_ip ; 4228 unsigned long hardirq_disable_ip ; 4229 unsigned int hardirq_enable_event ; 4230 unsigned int hardirq_disable_event ; 4231 int hardirqs_enabled ; 4232 int hardirq_context ; 4233 unsigned long softirq_disable_ip ; 4234 unsigned long softirq_enable_ip ; 4235 unsigned int softirq_disable_event ; 4236 unsigned int softirq_enable_event ; 4237 int softirqs_enabled ; 4238 int softirq_context ; 4239 u64 curr_chain_key ; 4240 int lockdep_depth ; 4241 unsigned int lockdep_recursion ; 4242 struct held_lock held_locks[48UL] ; 4243 gfp_t lockdep_reclaim_gfp ; 4244 void *journal_info ; 4245 struct bio_list *bio_list ; 4246 struct blk_plug *plug ; 4247 struct reclaim_state *reclaim_state ; 4248 struct backing_dev_info *backing_dev_info ; 4249 struct io_context *io_context ; 4250 unsigned long ptrace_message ; 4251 siginfo_t *last_siginfo ; 4252 struct task_io_accounting ioac ; 4253 u64 acct_rss_mem1 ; 4254 u64 acct_vm_mem1 ; 4255 cputime_t acct_timexpd ; 4256 nodemask_t mems_allowed ; 4257 int mems_allowed_change_disable ; 4258 int cpuset_mem_spread_rotor ; 4259 int cpuset_slab_spread_rotor ; 4260 struct css_set *cgroups ; 4261 struct list_head cg_list ; 4262 struct robust_list_head *robust_list ; 4263 struct compat_robust_list_head *compat_robust_list ; 4264 struct list_head pi_state_list ; 4265 struct futex_pi_state *pi_state_cache ; 4266 struct perf_event_context *perf_event_ctxp[2] ; 4267 struct mutex perf_event_mutex ; 4268 struct list_head perf_event_list ; 4269 struct mempolicy *mempolicy ; 4270 short il_next ; 4271 short pref_node_fork ; 4272 atomic_t fs_excl ; 4273 struct rcu_head rcu ; 4274 struct pipe_inode_info *splice_pipe ; 4275 struct task_delay_info *delays ; 4276 int make_it_fail ; 4277 struct prop_local_single dirties ; 4278 int latency_record_count ; 4279 struct latency_record latency_record[32] ; 4280 unsigned long timer_slack_ns ; 4281 unsigned long default_timer_slack_ns ; 4282 struct list_head *scm_work_list ; 4283 int curr_ret_stack ; 4284 struct ftrace_ret_stack *ret_stack ; 4285 unsigned long long ftrace_timestamp ; 4286 atomic_t trace_overrun ; 4287 atomic_t tracing_graph_pause ; 4288 unsigned long trace ; 4289 unsigned long trace_recursion ; 4290 struct memcg_batch_info memcg_batch ; 4291 atomic_t ptrace_bp_refcnt ; 4292}; 4293#line 1634 4294struct pid_namespace; 4295#line 25 "include/linux/usb.h" 4296struct usb_device; 4297#line 25 4298struct usb_device; 4299#line 25 4300struct usb_device; 4301#line 25 4302struct usb_device; 4303#line 26 4304struct usb_driver; 4305#line 26 4306struct usb_driver; 4307#line 26 4308struct usb_driver; 4309#line 26 4310struct usb_driver; 4311#line 27 4312struct wusb_dev; 4313#line 27 4314struct wusb_dev; 4315#line 27 4316struct wusb_dev; 4317#line 27 4318struct wusb_dev; 4319#line 47 4320struct ep_device; 4321#line 47 4322struct ep_device; 4323#line 47 4324struct ep_device; 4325#line 47 4326struct ep_device; 4327#line 64 "include/linux/usb.h" 4328struct usb_host_endpoint { 4329 struct usb_endpoint_descriptor desc ; 4330 struct usb_ss_ep_comp_descriptor ss_ep_comp ; 4331 struct list_head urb_list ; 4332 void *hcpriv ; 4333 struct ep_device *ep_dev ; 4334 unsigned char *extra ; 4335 int extralen ; 4336 int enabled ; 4337}; 4338#line 77 "include/linux/usb.h" 4339struct usb_host_interface { 4340 struct usb_interface_descriptor desc ; 4341 struct usb_host_endpoint *endpoint ; 4342 char *string ; 4343 unsigned char *extra ; 4344 int extralen ; 4345}; 4346#line 90 4347enum usb_interface_condition { 4348 USB_INTERFACE_UNBOUND = 0, 4349 USB_INTERFACE_BINDING = 1, 4350 USB_INTERFACE_BOUND = 2, 4351 USB_INTERFACE_UNBINDING = 3 4352} ; 4353#line 159 "include/linux/usb.h" 4354struct usb_interface { 4355 struct usb_host_interface *altsetting ; 4356 struct usb_host_interface *cur_altsetting ; 4357 unsigned int num_altsetting ; 4358 struct usb_interface_assoc_descriptor *intf_assoc ; 4359 int minor ; 4360 enum usb_interface_condition condition ; 4361 unsigned int sysfs_files_created : 1 ; 4362 unsigned int ep_devs_created : 1 ; 4363 unsigned int unregistering : 1 ; 4364 unsigned int needs_remote_wakeup : 1 ; 4365 unsigned int needs_altsetting0 : 1 ; 4366 unsigned int needs_binding : 1 ; 4367 unsigned int reset_running : 1 ; 4368 unsigned int resetting_device : 1 ; 4369 struct device dev ; 4370 struct device *usb_dev ; 4371 atomic_t pm_usage_cnt ; 4372 struct work_struct reset_ws ; 4373}; 4374#line 222 "include/linux/usb.h" 4375struct usb_interface_cache { 4376 unsigned int num_altsetting ; 4377 struct kref ref ; 4378 struct usb_host_interface altsetting[0] ; 4379}; 4380#line 274 "include/linux/usb.h" 4381struct usb_host_config { 4382 struct usb_config_descriptor desc ; 4383 char *string ; 4384 struct usb_interface_assoc_descriptor *intf_assoc[16] ; 4385 struct usb_interface *interface[32] ; 4386 struct usb_interface_cache *intf_cache[32] ; 4387 unsigned char *extra ; 4388 int extralen ; 4389}; 4390#line 305 "include/linux/usb.h" 4391struct usb_devmap { 4392 unsigned long devicemap[128UL / (8UL * sizeof(unsigned long ))] ; 4393}; 4394#line 312 4395struct mon_bus; 4396#line 312 4397struct mon_bus; 4398#line 312 4399struct mon_bus; 4400#line 312 "include/linux/usb.h" 4401struct usb_bus { 4402 struct device *controller ; 4403 int busnum ; 4404 char const *bus_name ; 4405 u8 uses_dma ; 4406 u8 uses_pio_for_control ; 4407 u8 otg_port ; 4408 unsigned int is_b_host : 1 ; 4409 unsigned int b_hnp_enable : 1 ; 4410 unsigned int sg_tablesize ; 4411 int devnum_next ; 4412 struct usb_devmap devmap ; 4413 struct usb_device *root_hub ; 4414 struct usb_bus *hs_companion ; 4415 struct list_head bus_list ; 4416 int bandwidth_allocated ; 4417 int bandwidth_int_reqs ; 4418 int bandwidth_isoc_reqs ; 4419 struct dentry *usbfs_dentry ; 4420 struct mon_bus *mon_bus ; 4421 int monitored ; 4422}; 4423#line 367 4424struct usb_tt; 4425#line 367 4426struct usb_tt; 4427#line 367 4428struct usb_tt; 4429#line 367 4430struct usb_tt; 4431#line 426 "include/linux/usb.h" 4432struct usb_device { 4433 int devnum ; 4434 char devpath[16] ; 4435 u32 route ; 4436 enum usb_device_state state ; 4437 enum usb_device_speed speed ; 4438 struct usb_tt *tt ; 4439 int ttport ; 4440 unsigned int toggle[2] ; 4441 struct usb_device *parent ; 4442 struct usb_bus *bus ; 4443 struct usb_host_endpoint ep0 ; 4444 struct device dev ; 4445 struct usb_device_descriptor descriptor ; 4446 struct usb_host_config *config ; 4447 struct usb_host_config *actconfig ; 4448 struct usb_host_endpoint *ep_in[16] ; 4449 struct usb_host_endpoint *ep_out[16] ; 4450 char **rawdescriptors ; 4451 unsigned short bus_mA ; 4452 u8 portnum ; 4453 u8 level ; 4454 unsigned int can_submit : 1 ; 4455 unsigned int persist_enabled : 1 ; 4456 unsigned int have_langid : 1 ; 4457 unsigned int authorized : 1 ; 4458 unsigned int authenticated : 1 ; 4459 unsigned int wusb : 1 ; 4460 int string_langid ; 4461 char *product ; 4462 char *manufacturer ; 4463 char *serial ; 4464 struct list_head filelist ; 4465 struct device *usb_classdev ; 4466 struct dentry *usbfs_dentry ; 4467 int maxchild ; 4468 struct usb_device *children[31] ; 4469 u32 quirks ; 4470 atomic_t urbnum ; 4471 unsigned long active_duration ; 4472 unsigned long connect_time ; 4473 unsigned int do_remote_wakeup : 1 ; 4474 unsigned int reset_resume : 1 ; 4475 struct wusb_dev *wusb_dev ; 4476 int slot_id ; 4477}; 4478#line 763 "include/linux/usb.h" 4479struct usb_dynids { 4480 spinlock_t lock ; 4481 struct list_head list ; 4482}; 4483#line 782 "include/linux/usb.h" 4484struct usbdrv_wrap { 4485 struct device_driver driver ; 4486 int for_devices ; 4487}; 4488#line 843 "include/linux/usb.h" 4489struct usb_driver { 4490 char const *name ; 4491 int (*probe)(struct usb_interface *intf , struct usb_device_id const *id ) ; 4492 void (*disconnect)(struct usb_interface *intf ) ; 4493 int (*unlocked_ioctl)(struct usb_interface *intf , unsigned int code , void *buf ) ; 4494 int (*suspend)(struct usb_interface *intf , pm_message_t message ) ; 4495 int (*resume)(struct usb_interface *intf ) ; 4496 int (*reset_resume)(struct usb_interface *intf ) ; 4497 int (*pre_reset)(struct usb_interface *intf ) ; 4498 int (*post_reset)(struct usb_interface *intf ) ; 4499 struct usb_device_id const *id_table ; 4500 struct usb_dynids dynids ; 4501 struct usbdrv_wrap drvwrap ; 4502 unsigned int no_dynamic_id : 1 ; 4503 unsigned int supports_autosuspend : 1 ; 4504 unsigned int soft_unbind : 1 ; 4505}; 4506#line 983 "include/linux/usb.h" 4507struct usb_iso_packet_descriptor { 4508 unsigned int offset ; 4509 unsigned int length ; 4510 unsigned int actual_length ; 4511 int status ; 4512}; 4513#line 990 4514struct urb; 4515#line 990 4516struct urb; 4517#line 990 4518struct urb; 4519#line 990 4520struct urb; 4521#line 992 "include/linux/usb.h" 4522struct usb_anchor { 4523 struct list_head urb_list ; 4524 wait_queue_head_t wait ; 4525 spinlock_t lock ; 4526 unsigned int poisoned : 1 ; 4527}; 4528#line 1183 4529struct scatterlist; 4530#line 1183 4531struct scatterlist; 4532#line 1183 4533struct scatterlist; 4534#line 1183 "include/linux/usb.h" 4535struct urb { 4536 struct kref kref ; 4537 void *hcpriv ; 4538 atomic_t use_count ; 4539 atomic_t reject ; 4540 int unlinked ; 4541 struct list_head urb_list ; 4542 struct list_head anchor_list ; 4543 struct usb_anchor *anchor ; 4544 struct usb_device *dev ; 4545 struct usb_host_endpoint *ep ; 4546 unsigned int pipe ; 4547 unsigned int stream_id ; 4548 int status ; 4549 unsigned int transfer_flags ; 4550 void *transfer_buffer ; 4551 dma_addr_t transfer_dma ; 4552 struct scatterlist *sg ; 4553 int num_sgs ; 4554 u32 transfer_buffer_length ; 4555 u32 actual_length ; 4556 unsigned char *setup_packet ; 4557 dma_addr_t setup_dma ; 4558 int start_frame ; 4559 int number_of_packets ; 4560 int interval ; 4561 int error_count ; 4562 void *context ; 4563 void (*complete)(struct urb * ) ; 4564 struct usb_iso_packet_descriptor iso_frame_desc[0] ; 4565}; 4566#line 1388 4567struct scatterlist; 4568#line 6 "include/asm-generic/scatterlist.h" 4569struct scatterlist { 4570 unsigned long sg_magic ; 4571 unsigned long page_link ; 4572 unsigned int offset ; 4573 unsigned int length ; 4574 dma_addr_t dma_address ; 4575 unsigned int dma_length ; 4576}; 4577#line 19 "include/linux/mm.h" 4578struct mempolicy; 4579#line 20 4580struct anon_vma; 4581#line 21 4582struct file_ra_state; 4583#line 22 4584struct user_struct; 4585#line 23 4586struct writeback_control; 4587#line 41 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable_64.h" 4588struct mm_struct; 4589#line 656 "/anthill/stuff/tacas-comp/inst/current/envs/linux-3.0.1/linux-3.0.1/arch/x86/include/asm/pgtable.h" 4590struct vm_area_struct; 4591#line 185 "include/linux/mm.h" 4592struct vm_fault { 4593 unsigned int flags ; 4594 unsigned long pgoff ; 4595 void *virtual_address ; 4596 struct page *page ; 4597}; 4598#line 202 "include/linux/mm.h" 4599struct vm_operations_struct { 4600 void (*open)(struct vm_area_struct *area ) ; 4601 void (*close)(struct vm_area_struct *area ) ; 4602 int (*fault)(struct vm_area_struct *vma , struct vm_fault *vmf ) ; 4603 int (*page_mkwrite)(struct vm_area_struct *vma , struct vm_fault *vmf ) ; 4604 int (*access)(struct vm_area_struct *vma , unsigned long addr , void *buf , int len , 4605 int write ) ; 4606 int (*set_policy)(struct vm_area_struct *vma , struct mempolicy *new ) ; 4607 struct mempolicy *(*get_policy)(struct vm_area_struct *vma , unsigned long addr ) ; 4608 int (*migrate)(struct vm_area_struct *vma , nodemask_t const *from , nodemask_t const *to , 4609 unsigned long flags ) ; 4610}; 4611#line 244 4612struct inode; 4613#line 197 "include/linux/page-flags.h" 4614struct page; 4615#line 58 "include/linux/kfifo.h" 4616struct __kfifo { 4617 unsigned int in ; 4618 unsigned int out ; 4619 unsigned int mask ; 4620 unsigned int esize ; 4621 void *data ; 4622}; 4623#line 96 "include/linux/kfifo.h" 4624union __anonunion____missing_field_name_247 { 4625 struct __kfifo kfifo ; 4626 unsigned char *type ; 4627 char (*rectype)[0] ; 4628 void *ptr ; 4629 void const *ptr_const ; 4630}; 4631#line 96 "include/linux/kfifo.h" 4632struct kfifo { 4633 union __anonunion____missing_field_name_247 __annonCompField41 ; 4634 unsigned char buf[0] ; 4635}; 4636#line 31 "include/linux/usb/serial.h" 4637enum port_dev_state { 4638 PORT_UNREGISTERED = 0, 4639 PORT_REGISTERING = 1, 4640 PORT_REGISTERED = 2, 4641 PORT_UNREGISTERING = 3 4642} ; 4643#line 82 4644struct usb_serial; 4645#line 82 4646struct usb_serial; 4647#line 82 4648struct usb_serial; 4649#line 82 "include/linux/usb/serial.h" 4650struct usb_serial_port { 4651 struct usb_serial *serial ; 4652 struct tty_port port ; 4653 spinlock_t lock ; 4654 unsigned char number ; 4655 unsigned char *interrupt_in_buffer ; 4656 struct urb *interrupt_in_urb ; 4657 __u8 interrupt_in_endpointAddress ; 4658 unsigned char *interrupt_out_buffer ; 4659 int interrupt_out_size ; 4660 struct urb *interrupt_out_urb ; 4661 __u8 interrupt_out_endpointAddress ; 4662 unsigned char *bulk_in_buffer ; 4663 int bulk_in_size ; 4664 struct urb *read_urb ; 4665 __u8 bulk_in_endpointAddress ; 4666 unsigned char *bulk_out_buffer ; 4667 int bulk_out_size ; 4668 struct urb *write_urb ; 4669 struct kfifo write_fifo ; 4670 int write_urb_busy ; 4671 unsigned char *bulk_out_buffers[2] ; 4672 struct urb *write_urbs[2] ; 4673 unsigned long write_urbs_free ; 4674 __u8 bulk_out_endpointAddress ; 4675 int tx_bytes ; 4676 unsigned long flags ; 4677 wait_queue_head_t write_wait ; 4678 struct work_struct work ; 4679 char throttled ; 4680 char throttle_req ; 4681 unsigned long sysrq ; 4682 struct device dev ; 4683 enum port_dev_state dev_state ; 4684}; 4685#line 155 4686struct usb_serial_driver; 4687#line 155 4688struct usb_serial_driver; 4689#line 155 4690struct usb_serial_driver; 4691#line 155 "include/linux/usb/serial.h" 4692struct usb_serial { 4693 struct usb_device *dev ; 4694 struct usb_serial_driver *type ; 4695 struct usb_interface *interface ; 4696 unsigned char disconnected : 1 ; 4697 unsigned char suspending : 1 ; 4698 unsigned char attached : 1 ; 4699 unsigned char minor ; 4700 unsigned char num_ports ; 4701 unsigned char num_port_pointers ; 4702 char num_interrupt_in ; 4703 char num_interrupt_out ; 4704 char num_bulk_in ; 4705 char num_bulk_out ; 4706 struct usb_serial_port *port[8] ; 4707 struct kref kref ; 4708 struct mutex disc_mutex ; 4709 void *private ; 4710}; 4711#line 230 "include/linux/usb/serial.h" 4712struct usb_serial_driver { 4713 char const *description ; 4714 struct usb_device_id const *id_table ; 4715 char num_ports ; 4716 struct list_head driver_list ; 4717 struct device_driver driver ; 4718 struct usb_driver *usb_driver ; 4719 struct usb_dynids dynids ; 4720 size_t bulk_in_size ; 4721 size_t bulk_out_size ; 4722 int (*probe)(struct usb_serial *serial , struct usb_device_id const *id ) ; 4723 int (*attach)(struct usb_serial *serial ) ; 4724 int (*calc_num_ports)(struct usb_serial *serial ) ; 4725 void (*disconnect)(struct usb_serial *serial ) ; 4726 void (*release)(struct usb_serial *serial ) ; 4727 int (*port_probe)(struct usb_serial_port *port ) ; 4728 int (*port_remove)(struct usb_serial_port *port ) ; 4729 int (*suspend)(struct usb_serial *serial , pm_message_t message ) ; 4730 int (*resume)(struct usb_serial *serial ) ; 4731 int (*open)(struct tty_struct *tty , struct usb_serial_port *port ) ; 4732 void (*close)(struct usb_serial_port *port ) ; 4733 int (*write)(struct tty_struct *tty , struct usb_serial_port *port , unsigned char const *buf , 4734 int count ) ; 4735 int (*write_room)(struct tty_struct *tty ) ; 4736 int (*ioctl)(struct tty_struct *tty , unsigned int cmd , unsigned long arg ) ; 4737 void (*set_termios)(struct tty_struct *tty , struct usb_serial_port *port , struct ktermios *old ) ; 4738 void (*break_ctl)(struct tty_struct *tty , int break_state ) ; 4739 int (*chars_in_buffer)(struct tty_struct *tty ) ; 4740 void (*throttle)(struct tty_struct *tty ) ; 4741 void (*unthrottle)(struct tty_struct *tty ) ; 4742 int (*tiocmget)(struct tty_struct *tty ) ; 4743 int (*tiocmset)(struct tty_struct *tty , unsigned int set , unsigned int clear ) ; 4744 int (*get_icount)(struct tty_struct *tty , struct serial_icounter_struct *icount ) ; 4745 void (*dtr_rts)(struct usb_serial_port *port , int on ) ; 4746 int (*carrier_raised)(struct usb_serial_port *port ) ; 4747 void (*init_termios)(struct tty_struct *tty ) ; 4748 void (*read_int_callback)(struct urb *urb ) ; 4749 void (*write_int_callback)(struct urb *urb ) ; 4750 void (*read_bulk_callback)(struct urb *urb ) ; 4751 void (*write_bulk_callback)(struct urb *urb ) ; 4752 void (*process_read_urb)(struct urb *urb ) ; 4753 int (*prepare_write_buffer)(struct usb_serial_port *port , void *dest , size_t size ) ; 4754}; 4755#line 89 "include/linux/usb/irda.h" 4756struct usb_irda_cs_descriptor { 4757 __u8 bLength ; 4758 __u8 bDescriptorType ; 4759 __le16 bcdSpecRevision ; 4760 __u8 bmDataSize ; 4761 __u8 bmWindowSize ; 4762 __u8 bmMinTurnaroundTime ; 4763 __le16 wBaudRate ; 4764 __u8 bmAdditionalBOFs ; 4765 __u8 bIrdaRateSniff ; 4766 __u8 bMaxUnicastList ; 4767} __attribute__((__packed__)) ; 4768#line 300 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 4769struct __anonstruct_250 { 4770 int : 0 ; 4771}; 4772#line 100 "include/linux/printk.h" 4773extern int printk(char const *fmt , ...) ; 4774#line 32 "include/linux/spinlock_api_smp.h" 4775extern unsigned long _raw_spin_lock_irqsave(raw_spinlock_t *lock ) __attribute__((__section__(".spinlock.text"))) ; 4776#line 42 4777extern void _raw_spin_unlock_irqrestore(raw_spinlock_t *lock , unsigned long flags ) __attribute__((__section__(".spinlock.text"))) ; 4778#line 272 "include/linux/spinlock.h" 4779__inline static raw_spinlock_t *spinlock_check(spinlock_t *lock ) 4780{ 4781 4782 { 4783#line 274 4784 return (& lock->__annonCompField18.rlock); 4785} 4786} 4787#line 338 "include/linux/spinlock.h" 4788__inline static void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags ) 4789{ struct raw_spinlock *__cil_tmp3 ; 4790 4791 { 4792 { 4793#line 340 4794 while (1) { 4795 while_continue: /* CIL Label */ ; 4796 { 4797#line 340 4798 __cil_tmp3 = & lock->__annonCompField18.rlock; 4799#line 340 4800 _raw_spin_unlock_irqrestore(__cil_tmp3, flags); 4801 } 4802#line 340 4803 goto while_break; 4804 } 4805 while_break___0: /* CIL Label */ ; 4806 } 4807 4808 while_break: ; 4809#line 341 4810 return; 4811} 4812} 4813#line 141 "include/linux/slab.h" 4814extern void kfree(void const * ) ; 4815#line 221 "include/linux/slub_def.h" 4816extern void *__kmalloc(size_t size , gfp_t flags ) ; 4817#line 255 "include/linux/slub_def.h" 4818__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size , 4819 gfp_t flags ) 4820{ void *tmp___2 ; 4821 4822 { 4823 { 4824#line 270 4825 tmp___2 = __kmalloc(size, flags); 4826 } 4827#line 270 4828 return (tmp___2); 4829} 4830} 4831#line 318 "include/linux/slab.h" 4832__inline static void *kzalloc(size_t size , gfp_t flags ) 4833{ void *tmp ; 4834 unsigned int __cil_tmp4 ; 4835 4836 { 4837 { 4838#line 320 4839 __cil_tmp4 = flags | 32768U; 4840#line 320 4841 tmp = kmalloc(size, __cil_tmp4); 4842 } 4843#line 320 4844 return (tmp); 4845} 4846} 4847#line 303 "include/linux/moduleparam.h" 4848extern struct kernel_param_ops param_ops_int ; 4849#line 329 4850extern struct kernel_param_ops param_ops_bool ; 4851#line 79 "include/linux/module.h" 4852int init_module(void) ; 4853#line 80 4854void cleanup_module(void) ; 4855#line 99 4856extern struct module __this_module ; 4857#line 797 "include/linux/device.h" 4858extern int dev_err(struct device const *dev , char const *fmt , ...) ; 4859#line 399 "include/linux/tty.h" 4860extern void tty_kref_put(struct tty_struct *tty ) ; 4861#line 439 4862extern void tty_flip_buffer_push(struct tty_struct *tty ) ; 4863#line 444 4864extern speed_t tty_get_baud_rate(struct tty_struct *tty ) ; 4865#line 449 4866extern void tty_encode_baud_rate(struct tty_struct *tty , speed_t ibaud , speed_t obaud ) ; 4867#line 451 4868extern void tty_termios_copy_hw(struct ktermios *new , struct ktermios *old ) ; 4869#line 505 4870extern struct tty_struct *tty_port_tty_get(struct tty_port *port ) ; 4871#line 6 "include/linux/tty_flip.h" 4872extern int tty_insert_flip_string_fixed_flag(struct tty_struct *tty , unsigned char const *chars , 4873 char flag , size_t size ) ; 4874#line 23 "include/linux/tty_flip.h" 4875__inline static int tty_insert_flip_string(struct tty_struct *tty , unsigned char const *chars , 4876 size_t size ) 4877{ int tmp ; 4878 4879 { 4880 { 4881#line 25 4882 tmp = tty_insert_flip_string_fixed_flag(tty, chars, (char)0, size); 4883 } 4884#line 25 4885 return (tmp); 4886} 4887} 4888#line 929 "include/linux/usb.h" 4889extern int usb_register_driver(struct usb_driver * , struct module * , char const * ) ; 4890#line 931 "include/linux/usb.h" 4891__inline static int usb_register(struct usb_driver *driver ) 4892{ int tmp___7 ; 4893 4894 { 4895 { 4896#line 933 4897 tmp___7 = usb_register_driver(driver, & __this_module, "ir_usb"); 4898 } 4899#line 933 4900 return (tmp___7); 4901} 4902} 4903#line 935 4904extern void usb_deregister(struct usb_driver * ) ; 4905#line 1268 "include/linux/usb.h" 4906__inline static void usb_fill_bulk_urb(struct urb *urb , struct usb_device *dev , 4907 unsigned int pipe , void *transfer_buffer , 4908 int buffer_length , void (*complete_fn)(struct urb * ) , 4909 void *context ) 4910{ 4911 4912 { 4913#line 1276 4914 urb->dev = dev; 4915#line 1277 4916 urb->pipe = pipe; 4917#line 1278 4918 urb->transfer_buffer = transfer_buffer; 4919#line 1279 4920 urb->transfer_buffer_length = (u32 )buffer_length; 4921#line 1280 4922 urb->complete = complete_fn; 4923#line 1281 4924 urb->context = context; 4925#line 1282 4926 return; 4927} 4928} 4929#line 1332 4930struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags ) __attribute__((__ldv_model__)) ; 4931#line 1333 4932void usb_free_urb(struct urb *urb ) __attribute__((__ldv_model__)) ; 4933#line 1336 4934extern int usb_submit_urb(struct urb *urb , gfp_t mem_flags ) ; 4935#line 1377 4936void *usb_alloc_coherent(struct usb_device *dev , size_t size , gfp_t mem_flags , 4937 dma_addr_t *dma ) __attribute__((__ldv_model__)) ; 4938#line 1379 4939void usb_free_coherent(struct usb_device *dev , size_t size , void *addr , dma_addr_t dma ) __attribute__((__ldv_model__)) ; 4940#line 1402 4941extern int usb_control_msg(struct usb_device *dev , unsigned int pipe , __u8 request , 4942 __u8 requesttype , __u16 value , __u16 index , void *data , 4943 __u16 size , int timeout ) ; 4944#line 1526 "include/linux/usb.h" 4945__inline static unsigned int __create_pipe(struct usb_device *dev , unsigned int endpoint ) 4946{ unsigned int __cil_tmp3 ; 4947 int __cil_tmp4 ; 4948 int __cil_tmp5 ; 4949 unsigned int __cil_tmp6 ; 4950 4951 { 4952 { 4953#line 1529 4954 __cil_tmp3 = endpoint << 15; 4955#line 1529 4956 __cil_tmp4 = dev->devnum; 4957#line 1529 4958 __cil_tmp5 = __cil_tmp4 << 8; 4959#line 1529 4960 __cil_tmp6 = (unsigned int )__cil_tmp5; 4961#line 1529 4962 return (__cil_tmp6 | __cil_tmp3); 4963 } 4964} 4965} 4966#line 174 "include/linux/kfifo.h" 4967__inline static unsigned int __attribute__((__warn_unused_result__)) __kfifo_uint_must_check_helper(unsigned int val ) 4968{ 4969 4970 { 4971#line 177 4972 return (val); 4973} 4974} 4975#line 801 4976extern unsigned int __kfifo_out(struct __kfifo *fifo , void *buf , unsigned int len ) ; 4977#line 822 4978extern unsigned int __kfifo_out_r(struct __kfifo *fifo , void *buf , unsigned int len , 4979 size_t recsize ) ; 4980#line 298 "include/linux/usb/serial.h" 4981extern int usb_serial_register(struct usb_serial_driver *driver ) ; 4982#line 299 4983extern void usb_serial_deregister(struct usb_serial_driver *driver ) ; 4984#line 302 4985extern int usb_serial_probe(struct usb_interface *iface , struct usb_device_id const *id ) ; 4986#line 304 4987extern void usb_serial_disconnect(struct usb_interface *iface ) ; 4988#line 327 4989extern int usb_serial_generic_open(struct tty_struct *tty , struct usb_serial_port *port ) ; 4990#line 81 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 4991static int debug ; 4992#line 85 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 4993static int buffer_size ; 4994#line 88 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 4995static int xbof = -1; 4996#line 90 4997static int ir_startup(struct usb_serial *serial ) ; 4998#line 91 4999static int ir_open(struct tty_struct *tty , struct usb_serial_port *port ) ; 5000#line 92 5001static int ir_prepare_write_buffer(struct usb_serial_port *port , void *dest , size_t size ) ; 5002#line 94 5003static void ir_process_read_urb(struct urb *urb ) ; 5004#line 95 5005static void ir_set_termios(struct tty_struct *tty , struct usb_serial_port *port , 5006 struct ktermios *old_termios ) ; 5007#line 99 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 5008static u8 ir_baud ; 5009#line 100 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 5010static u8 ir_xbof ; 5011#line 101 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 5012static u8 ir_add_bof ; 5013#line 103 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 5014static struct usb_device_id const ir_id_table[4] = { {(__u16 )3, (__u16 )1295, (__u16 )384, (unsigned short)0, (unsigned short)0, 5015 (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0, 5016 (unsigned char)0, 0UL}, 5017 {(__u16 )3, (__u16 )2281, (__u16 )256, (unsigned short)0, (unsigned short)0, 5018 (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0, 5019 (unsigned char)0, 0UL}, 5020 {(__u16 )3, (__u16 )2500, (__u16 )17, (unsigned short)0, (unsigned short)0, (unsigned char)0, 5021 (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0, 5022 0UL}, 5023 {(__u16 )896, (unsigned short)0, (unsigned short)0, (unsigned short)0, (unsigned short)0, 5024 (unsigned char)0, (unsigned char)0, (unsigned char)0, (__u8 )254, (__u8 )2, 5025 (__u8 )0, 0UL}}; 5026#line 111 5027extern struct usb_device_id const __mod_usb_device_table __attribute__((__unused__, 5028__alias__("ir_id_table"))) ; 5029#line 113 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 5030static struct usb_driver ir_driver = 5031#line 113 5032 {"ir-usb", & usb_serial_probe, & usb_serial_disconnect, (int (*)(struct usb_interface *intf , 5033 unsigned int code , 5034 void *buf ))0, 5035 (int (*)(struct usb_interface *intf , pm_message_t message ))0, (int (*)(struct usb_interface *intf ))0, 5036 (int (*)(struct usb_interface *intf ))0, (int (*)(struct usb_interface *intf ))0, 5037 (int (*)(struct usb_interface *intf ))0, ir_id_table, {{{{{0U}, 0U, 0U, (void *)0, 5038 {(struct lock_class_key *)0, 5039 {(struct lock_class *)0, 5040 (struct lock_class *)0}, 5041 (char const *)0, 5042 0, 0UL}}}}, {(struct list_head *)0, 5043 (struct list_head *)0}}, 5044 {{(char const *)0, (struct bus_type *)0, (struct module *)0, (char const *)0, 5045 (_Bool)0, (struct of_device_id const *)0, (int (*)(struct device *dev ))0, 5046 (int (*)(struct device *dev ))0, (void (*)(struct device *dev ))0, (int (*)(struct device *dev , 5047 pm_message_t state ))0, 5048 (int (*)(struct device *dev ))0, (struct attribute_group const **)0, (struct dev_pm_ops const *)0, 5049 (struct driver_private *)0}, 0}, 1U, 0U, 0U}; 5050#line 121 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 5051static struct usb_serial_driver ir_device = 5052#line 121 5053 {"IR Dongle", ir_id_table, (char)1, {(struct list_head *)0, (struct list_head *)0}, 5054 {"ir-usb", (struct bus_type *)0, & __this_module, (char const *)0, (_Bool)0, 5055 (struct of_device_id const *)0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0, 5056 (void (*)(struct device *dev ))0, (int (*)(struct device *dev , pm_message_t state ))0, 5057 (int (*)(struct device *dev ))0, (struct attribute_group const **)0, (struct dev_pm_ops const *)0, 5058 (struct driver_private *)0}, & ir_driver, {{{{{0U}, 0U, 0U, (void *)0, {(struct lock_class_key *)0, 5059 {(struct lock_class *)0, 5060 (struct lock_class *)0}, 5061 (char const *)0, 5062 0, 0UL}}}}, 5063 {(struct list_head *)0, (struct list_head *)0}}, 5064 0UL, 0UL, (int (*)(struct usb_serial *serial , struct usb_device_id const *id ))0, 5065 & ir_startup, (int (*)(struct usb_serial *serial ))0, (void (*)(struct usb_serial *serial ))0, 5066 (void (*)(struct usb_serial *serial ))0, (int (*)(struct usb_serial_port *port ))0, 5067 (int (*)(struct usb_serial_port *port ))0, (int (*)(struct usb_serial *serial , 5068 pm_message_t message ))0, 5069 (int (*)(struct usb_serial *serial ))0, & ir_open, (void (*)(struct usb_serial_port *port ))0, 5070 (int (*)(struct tty_struct *tty , struct usb_serial_port *port , unsigned char const *buf , 5071 int count ))0, (int (*)(struct tty_struct *tty ))0, (int (*)(struct tty_struct *tty , 5072 unsigned int cmd , 5073 unsigned long arg ))0, 5074 & ir_set_termios, (void (*)(struct tty_struct *tty , int break_state ))0, (int (*)(struct tty_struct *tty ))0, 5075 (void (*)(struct tty_struct *tty ))0, (void (*)(struct tty_struct *tty ))0, (int (*)(struct tty_struct *tty ))0, 5076 (int (*)(struct tty_struct *tty , unsigned int set , unsigned int clear ))0, (int (*)(struct tty_struct *tty , 5077 struct serial_icounter_struct *icount ))0, 5078 (void (*)(struct usb_serial_port *port , int on ))0, (int (*)(struct usb_serial_port *port ))0, 5079 (void (*)(struct tty_struct *tty ))0, (void (*)(struct urb *urb ))0, (void (*)(struct urb *urb ))0, 5080 (void (*)(struct urb *urb ))0, (void (*)(struct urb *urb ))0, & ir_process_read_urb, 5081 & ir_prepare_write_buffer}; 5082#line 137 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 5083__inline static void irda_usb_dump_class_desc(struct usb_irda_cs_descriptor *desc ) 5084{ __u8 __cil_tmp2 ; 5085 int __cil_tmp3 ; 5086 __u8 __cil_tmp4 ; 5087 int __cil_tmp5 ; 5088 __le16 __cil_tmp6 ; 5089 int __cil_tmp7 ; 5090 __u8 __cil_tmp8 ; 5091 int __cil_tmp9 ; 5092 __u8 __cil_tmp10 ; 5093 int __cil_tmp11 ; 5094 __u8 __cil_tmp12 ; 5095 int __cil_tmp13 ; 5096 __le16 __cil_tmp14 ; 5097 int __cil_tmp15 ; 5098 __u8 __cil_tmp16 ; 5099 int __cil_tmp17 ; 5100 __u8 __cil_tmp18 ; 5101 int __cil_tmp19 ; 5102 __u8 __cil_tmp20 ; 5103 int __cil_tmp21 ; 5104 5105 { 5106 { 5107#line 139 5108 while (1) { 5109 while_continue: /* CIL Label */ ; 5110 5111#line 139 5112 if (debug) { 5113 { 5114#line 139 5115 __cil_tmp2 = desc->bLength; 5116#line 139 5117 __cil_tmp3 = (int )__cil_tmp2; 5118#line 139 5119 printk("<7>%s: bLength=%x\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5120 __cil_tmp3); 5121 } 5122 } else { 5123 5124 } 5125#line 139 5126 goto while_break; 5127 } 5128 while_break___9: /* CIL Label */ ; 5129 } 5130 5131 while_break: ; 5132 { 5133#line 140 5134 while (1) { 5135 while_continue___0: /* CIL Label */ ; 5136 5137#line 140 5138 if (debug) { 5139 { 5140#line 140 5141 __cil_tmp4 = desc->bDescriptorType; 5142#line 140 5143 __cil_tmp5 = (int )__cil_tmp4; 5144#line 140 5145 printk("<7>%s: bDescriptorType=%x\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5146 __cil_tmp5); 5147 } 5148 } else { 5149 5150 } 5151#line 140 5152 goto while_break___0; 5153 } 5154 while_break___10: /* CIL Label */ ; 5155 } 5156 5157 while_break___0: ; 5158 { 5159#line 141 5160 while (1) { 5161 while_continue___1: /* CIL Label */ ; 5162 5163#line 141 5164 if (debug) { 5165 { 5166#line 141 5167 __cil_tmp6 = desc->bcdSpecRevision; 5168#line 141 5169 __cil_tmp7 = (int )__cil_tmp6; 5170#line 141 5171 printk("<7>%s: bcdSpecRevision=%x\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5172 __cil_tmp7); 5173 } 5174 } else { 5175 5176 } 5177#line 141 5178 goto while_break___1; 5179 } 5180 while_break___11: /* CIL Label */ ; 5181 } 5182 5183 while_break___1: ; 5184 { 5185#line 142 5186 while (1) { 5187 while_continue___2: /* CIL Label */ ; 5188 5189#line 142 5190 if (debug) { 5191 { 5192#line 142 5193 __cil_tmp8 = desc->bmDataSize; 5194#line 142 5195 __cil_tmp9 = (int )__cil_tmp8; 5196#line 142 5197 printk("<7>%s: bmDataSize=%x\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5198 __cil_tmp9); 5199 } 5200 } else { 5201 5202 } 5203#line 142 5204 goto while_break___2; 5205 } 5206 while_break___12: /* CIL Label */ ; 5207 } 5208 5209 while_break___2: ; 5210 { 5211#line 143 5212 while (1) { 5213 while_continue___3: /* CIL Label */ ; 5214 5215#line 143 5216 if (debug) { 5217 { 5218#line 143 5219 __cil_tmp10 = desc->bmWindowSize; 5220#line 143 5221 __cil_tmp11 = (int )__cil_tmp10; 5222#line 143 5223 printk("<7>%s: bmWindowSize=%x\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5224 __cil_tmp11); 5225 } 5226 } else { 5227 5228 } 5229#line 143 5230 goto while_break___3; 5231 } 5232 while_break___13: /* CIL Label */ ; 5233 } 5234 5235 while_break___3: ; 5236 { 5237#line 144 5238 while (1) { 5239 while_continue___4: /* CIL Label */ ; 5240 5241#line 144 5242 if (debug) { 5243 { 5244#line 144 5245 __cil_tmp12 = desc->bmMinTurnaroundTime; 5246#line 144 5247 __cil_tmp13 = (int )__cil_tmp12; 5248#line 144 5249 printk("<7>%s: bmMinTurnaroundTime=%d\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5250 __cil_tmp13); 5251 } 5252 } else { 5253 5254 } 5255#line 144 5256 goto while_break___4; 5257 } 5258 while_break___14: /* CIL Label */ ; 5259 } 5260 5261 while_break___4: ; 5262 { 5263#line 145 5264 while (1) { 5265 while_continue___5: /* CIL Label */ ; 5266 5267#line 145 5268 if (debug) { 5269 { 5270#line 145 5271 __cil_tmp14 = desc->wBaudRate; 5272#line 145 5273 __cil_tmp15 = (int )__cil_tmp14; 5274#line 145 5275 printk("<7>%s: wBaudRate=%x\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5276 __cil_tmp15); 5277 } 5278 } else { 5279 5280 } 5281#line 145 5282 goto while_break___5; 5283 } 5284 while_break___15: /* CIL Label */ ; 5285 } 5286 5287 while_break___5: ; 5288 { 5289#line 146 5290 while (1) { 5291 while_continue___6: /* CIL Label */ ; 5292 5293#line 146 5294 if (debug) { 5295 { 5296#line 146 5297 __cil_tmp16 = desc->bmAdditionalBOFs; 5298#line 146 5299 __cil_tmp17 = (int )__cil_tmp16; 5300#line 146 5301 printk("<7>%s: bmAdditionalBOFs=%x\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5302 __cil_tmp17); 5303 } 5304 } else { 5305 5306 } 5307#line 146 5308 goto while_break___6; 5309 } 5310 while_break___16: /* CIL Label */ ; 5311 } 5312 5313 while_break___6: ; 5314 { 5315#line 147 5316 while (1) { 5317 while_continue___7: /* CIL Label */ ; 5318 5319#line 147 5320 if (debug) { 5321 { 5322#line 147 5323 __cil_tmp18 = desc->bIrdaRateSniff; 5324#line 147 5325 __cil_tmp19 = (int )__cil_tmp18; 5326#line 147 5327 printk("<7>%s: bIrdaRateSniff=%x\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5328 __cil_tmp19); 5329 } 5330 } else { 5331 5332 } 5333#line 147 5334 goto while_break___7; 5335 } 5336 while_break___17: /* CIL Label */ ; 5337 } 5338 5339 while_break___7: ; 5340 { 5341#line 148 5342 while (1) { 5343 while_continue___8: /* CIL Label */ ; 5344 5345#line 148 5346 if (debug) { 5347 { 5348#line 148 5349 __cil_tmp20 = desc->bMaxUnicastList; 5350#line 148 5351 __cil_tmp21 = (int )__cil_tmp20; 5352#line 148 5353 printk("<7>%s: bMaxUnicastList=%x\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5354 __cil_tmp21); 5355 } 5356 } else { 5357 5358 } 5359#line 148 5360 goto while_break___8; 5361 } 5362 while_break___18: /* CIL Label */ ; 5363 } 5364 5365 while_break___8: ; 5366#line 149 5367 return; 5368} 5369} 5370#line 163 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 5371static struct usb_irda_cs_descriptor *irda_usb_find_class_desc(struct usb_device *dev , 5372 unsigned int ifnum ) 5373{ struct usb_irda_cs_descriptor *desc ; 5374 int ret ; 5375 void *tmp___7 ; 5376 unsigned int tmp___8 ; 5377 char const *tmp___9 ; 5378 void *__cil_tmp8 ; 5379 int __cil_tmp9 ; 5380 unsigned int __cil_tmp10 ; 5381 unsigned int __cil_tmp11 ; 5382 unsigned int __cil_tmp12 ; 5383 __u8 __cil_tmp13 ; 5384 int __cil_tmp14 ; 5385 int __cil_tmp15 ; 5386 int __cil_tmp16 ; 5387 __u8 __cil_tmp17 ; 5388 __u16 __cil_tmp18 ; 5389 __u16 __cil_tmp19 ; 5390 void *__cil_tmp20 ; 5391 __u16 __cil_tmp21 ; 5392 unsigned long __cil_tmp22 ; 5393 __u8 __cil_tmp23 ; 5394 int __cil_tmp24 ; 5395 void const *__cil_tmp25 ; 5396 void *__cil_tmp26 ; 5397 5398 { 5399 { 5400#line 169 5401 tmp___7 = kzalloc(12UL, 208U); 5402#line 169 5403 desc = (struct usb_irda_cs_descriptor *)tmp___7; 5404 } 5405#line 170 5406 if (! desc) { 5407 { 5408#line 171 5409 __cil_tmp8 = (void *)0; 5410#line 171 5411 return ((struct usb_irda_cs_descriptor *)__cil_tmp8); 5412 } 5413 } else { 5414 5415 } 5416 { 5417#line 173 5418 tmp___8 = __create_pipe(dev, 0U); 5419#line 173 5420 __cil_tmp9 = 2 << 30; 5421#line 173 5422 __cil_tmp10 = (unsigned int )__cil_tmp9; 5423#line 173 5424 __cil_tmp11 = __cil_tmp10 | tmp___8; 5425#line 173 5426 __cil_tmp12 = __cil_tmp11 | 128U; 5427#line 173 5428 __cil_tmp13 = (__u8 )6; 5429#line 173 5430 __cil_tmp14 = 1 << 5; 5431#line 173 5432 __cil_tmp15 = 128 | __cil_tmp14; 5433#line 173 5434 __cil_tmp16 = __cil_tmp15 | 1; 5435#line 173 5436 __cil_tmp17 = (__u8 )__cil_tmp16; 5437#line 173 5438 __cil_tmp18 = (__u16 )0; 5439#line 173 5440 __cil_tmp19 = (__u16 )ifnum; 5441#line 173 5442 __cil_tmp20 = (void *)desc; 5443#line 173 5444 __cil_tmp21 = (__u16 )12UL; 5445#line 173 5446 ret = usb_control_msg(dev, __cil_tmp12, __cil_tmp13, __cil_tmp17, __cil_tmp18, __cil_tmp19, 5447 __cil_tmp20, __cil_tmp21, 1000); 5448 } 5449 { 5450#line 178 5451 while (1) { 5452 while_continue: /* CIL Label */ ; 5453 5454#line 178 5455 if (debug) { 5456 { 5457#line 178 5458 printk("<7>%s: %s - ret=%d\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5459 "irda_usb_find_class_desc", ret); 5460 } 5461 } else { 5462 5463 } 5464#line 178 5465 goto while_break; 5466 } 5467 while_break___2: /* CIL Label */ ; 5468 } 5469 5470 while_break: ; 5471 { 5472#line 179 5473 __cil_tmp22 = (unsigned long )ret; 5474#line 179 5475 if (__cil_tmp22 < 12UL) { 5476 { 5477#line 180 5478 while (1) { 5479 while_continue___0: /* CIL Label */ ; 5480 5481#line 180 5482 if (debug) { 5483#line 180 5484 if (ret < 0) { 5485#line 180 5486 tmp___9 = "failed"; 5487 } else { 5488#line 180 5489 tmp___9 = "too short"; 5490 } 5491 { 5492#line 180 5493 printk("<7>%s: %s - class descriptor read %s (%d)\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5494 "irda_usb_find_class_desc", tmp___9, ret); 5495 } 5496 } else { 5497 5498 } 5499#line 180 5500 goto while_break___0; 5501 } 5502 while_break___3: /* CIL Label */ ; 5503 } 5504 5505 while_break___0: ; 5506#line 184 5507 goto error; 5508 } else { 5509 5510 } 5511 } 5512 { 5513#line 186 5514 __cil_tmp23 = desc->bDescriptorType; 5515#line 186 5516 __cil_tmp24 = (int )__cil_tmp23; 5517#line 186 5518 if (__cil_tmp24 != 33) { 5519 { 5520#line 187 5521 while (1) { 5522 while_continue___1: /* CIL Label */ ; 5523 5524#line 187 5525 if (debug) { 5526 { 5527#line 187 5528 printk("<7>%s: %s - bad class descriptor type\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5529 "irda_usb_find_class_desc"); 5530 } 5531 } else { 5532 5533 } 5534#line 187 5535 goto while_break___1; 5536 } 5537 while_break___4: /* CIL Label */ ; 5538 } 5539 5540 while_break___1: ; 5541#line 188 5542 goto error; 5543 } else { 5544 5545 } 5546 } 5547 { 5548#line 191 5549 irda_usb_dump_class_desc(desc); 5550 } 5551#line 192 5552 return (desc); 5553 error: 5554 { 5555#line 195 5556 __cil_tmp25 = (void const *)desc; 5557#line 195 5558 kfree(__cil_tmp25); 5559 } 5560 { 5561#line 196 5562 __cil_tmp26 = (void *)0; 5563#line 196 5564 return ((struct usb_irda_cs_descriptor *)__cil_tmp26); 5565 } 5566} 5567} 5568#line 199 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 5569static u8 ir_xbof_change(u8 xbof___0 ) 5570{ u8 result ; 5571 int __cil_tmp3 ; 5572 int __cil_tmp4 ; 5573 int __cil_tmp5 ; 5574 int __cil_tmp6 ; 5575 int __cil_tmp7 ; 5576 int __cil_tmp8 ; 5577 int __cil_tmp9 ; 5578 int __cil_tmp10 ; 5579 int __cil_tmp11 ; 5580 5581 { 5582 { 5583#line 205 5584 __cil_tmp3 = (int )xbof___0; 5585#line 205 5586 if (__cil_tmp3 == 48) { 5587#line 205 5588 goto case_48; 5589 } else { 5590 { 5591#line 208 5592 __cil_tmp4 = (int )xbof___0; 5593#line 208 5594 if (__cil_tmp4 == 28) { 5595#line 208 5596 goto case_28; 5597 } else { 5598 { 5599#line 209 5600 __cil_tmp5 = (int )xbof___0; 5601#line 209 5602 if (__cil_tmp5 == 24) { 5603#line 209 5604 goto case_28; 5605 } else { 5606 { 5607#line 216 5608 __cil_tmp6 = (int )xbof___0; 5609#line 216 5610 if (__cil_tmp6 == 5) { 5611#line 216 5612 goto case_5; 5613 } else { 5614 { 5615#line 217 5616 __cil_tmp7 = (int )xbof___0; 5617#line 217 5618 if (__cil_tmp7 == 6) { 5619#line 217 5620 goto case_5; 5621 } else { 5622 { 5623#line 220 5624 __cil_tmp8 = (int )xbof___0; 5625#line 220 5626 if (__cil_tmp8 == 3) { 5627#line 220 5628 goto case_3; 5629 } else { 5630 { 5631#line 223 5632 __cil_tmp9 = (int )xbof___0; 5633#line 223 5634 if (__cil_tmp9 == 2) { 5635#line 223 5636 goto case_2; 5637 } else { 5638 { 5639#line 226 5640 __cil_tmp10 = (int )xbof___0; 5641#line 226 5642 if (__cil_tmp10 == 1) { 5643#line 226 5644 goto case_1; 5645 } else { 5646 { 5647#line 229 5648 __cil_tmp11 = (int )xbof___0; 5649#line 229 5650 if (__cil_tmp11 == 0) { 5651#line 229 5652 goto case_0; 5653 } else { 5654#line 212 5655 goto switch_default; 5656#line 204 5657 if (0) { 5658 case_48: 5659#line 206 5660 result = (u8 )16; 5661#line 207 5662 goto switch_break; 5663 case_28: 5664#line 210 5665 result = (u8 )32; 5666#line 211 5667 goto switch_break; 5668 switch_default: 5669#line 214 5670 result = (u8 )48; 5671#line 215 5672 goto switch_break; 5673 case_5: 5674#line 218 5675 result = (u8 )64; 5676#line 219 5677 goto switch_break; 5678 case_3: 5679#line 221 5680 result = (u8 )80; 5681#line 222 5682 goto switch_break; 5683 case_2: 5684#line 224 5685 result = (u8 )96; 5686#line 225 5687 goto switch_break; 5688 case_1: 5689#line 227 5690 result = (u8 )112; 5691#line 228 5692 goto switch_break; 5693 case_0: 5694#line 230 5695 result = (u8 )128; 5696#line 231 5697 goto switch_break; 5698 } else { 5699 switch_break: ; 5700 } 5701 } 5702 } 5703 } 5704 } 5705 } 5706 } 5707 } 5708 } 5709 } 5710 } 5711 } 5712 } 5713 } 5714 } 5715 } 5716 } 5717 } 5718 } 5719#line 234 5720 return (result); 5721} 5722} 5723#line 237 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 5724static int ir_startup(struct usb_serial *serial ) 5725{ struct usb_irda_cs_descriptor *irda_desc ; 5726 char const *tmp___7 ; 5727 char const *tmp___8 ; 5728 char const *tmp___9 ; 5729 char const *tmp___10 ; 5730 char const *tmp___11 ; 5731 char const *tmp___12 ; 5732 char const *tmp___13 ; 5733 char const *tmp___14 ; 5734 char const *tmp___15 ; 5735 struct usb_device *__cil_tmp12 ; 5736 struct usb_device *__cil_tmp13 ; 5737 struct device *__cil_tmp14 ; 5738 struct device const *__cil_tmp15 ; 5739 int __cil_tmp16 ; 5740 __le16 __cil_tmp17 ; 5741 int __cil_tmp18 ; 5742 int __cil_tmp19 ; 5743 __le16 __cil_tmp20 ; 5744 int __cil_tmp21 ; 5745 int __cil_tmp22 ; 5746 __le16 __cil_tmp23 ; 5747 int __cil_tmp24 ; 5748 int __cil_tmp25 ; 5749 __le16 __cil_tmp26 ; 5750 int __cil_tmp27 ; 5751 int __cil_tmp28 ; 5752 __le16 __cil_tmp29 ; 5753 int __cil_tmp30 ; 5754 int __cil_tmp31 ; 5755 __le16 __cil_tmp32 ; 5756 int __cil_tmp33 ; 5757 int __cil_tmp34 ; 5758 __le16 __cil_tmp35 ; 5759 int __cil_tmp36 ; 5760 int __cil_tmp37 ; 5761 __le16 __cil_tmp38 ; 5762 int __cil_tmp39 ; 5763 __le16 __cil_tmp40 ; 5764 int __cil_tmp41 ; 5765 __u8 __cil_tmp42 ; 5766 int __cil_tmp43 ; 5767 int __cil_tmp44 ; 5768 __u8 __cil_tmp45 ; 5769 int __cil_tmp46 ; 5770 int __cil_tmp47 ; 5771 __u8 __cil_tmp48 ; 5772 int __cil_tmp49 ; 5773 int __cil_tmp50 ; 5774 __u8 __cil_tmp51 ; 5775 int __cil_tmp52 ; 5776 int __cil_tmp53 ; 5777 __u8 __cil_tmp54 ; 5778 int __cil_tmp55 ; 5779 int __cil_tmp56 ; 5780 __u8 __cil_tmp57 ; 5781 int __cil_tmp58 ; 5782 int __cil_tmp59 ; 5783 __u8 __cil_tmp60 ; 5784 int __cil_tmp61 ; 5785 int __cil_tmp62 ; 5786 __u8 __cil_tmp63 ; 5787 int __cil_tmp64 ; 5788 void const *__cil_tmp65 ; 5789 5790 { 5791 { 5792#line 241 5793 __cil_tmp12 = serial->dev; 5794#line 241 5795 irda_desc = irda_usb_find_class_desc(__cil_tmp12, 0U); 5796 } 5797#line 242 5798 if (! irda_desc) { 5799 { 5800#line 243 5801 __cil_tmp13 = serial->dev; 5802#line 243 5803 __cil_tmp14 = & __cil_tmp13->dev; 5804#line 243 5805 __cil_tmp15 = (struct device const *)__cil_tmp14; 5806#line 243 5807 dev_err(__cil_tmp15, "IRDA class descriptor not found, device not bound\n"); 5808 } 5809#line 245 5810 return (-19); 5811 } else { 5812 5813 } 5814 { 5815#line 248 5816 while (1) { 5817 while_continue: /* CIL Label */ ; 5818 5819#line 248 5820 if (debug) { 5821 { 5822#line 248 5823 __cil_tmp16 = 1 << 8; 5824#line 248 5825 __cil_tmp17 = irda_desc->wBaudRate; 5826#line 248 5827 __cil_tmp18 = (int )__cil_tmp17; 5828#line 248 5829 if (__cil_tmp18 & __cil_tmp16) { 5830#line 248 5831 tmp___7 = " 4000000"; 5832 } else { 5833#line 248 5834 tmp___7 = ""; 5835 } 5836 } 5837 { 5838#line 248 5839 __cil_tmp19 = 1 << 7; 5840#line 248 5841 __cil_tmp20 = irda_desc->wBaudRate; 5842#line 248 5843 __cil_tmp21 = (int )__cil_tmp20; 5844#line 248 5845 if (__cil_tmp21 & __cil_tmp19) { 5846#line 248 5847 tmp___8 = " 1152000"; 5848 } else { 5849#line 248 5850 tmp___8 = ""; 5851 } 5852 } 5853 { 5854#line 248 5855 __cil_tmp22 = 1 << 6; 5856#line 248 5857 __cil_tmp23 = irda_desc->wBaudRate; 5858#line 248 5859 __cil_tmp24 = (int )__cil_tmp23; 5860#line 248 5861 if (__cil_tmp24 & __cil_tmp22) { 5862#line 248 5863 tmp___9 = " 576000"; 5864 } else { 5865#line 248 5866 tmp___9 = ""; 5867 } 5868 } 5869 { 5870#line 248 5871 __cil_tmp25 = 1 << 5; 5872#line 248 5873 __cil_tmp26 = irda_desc->wBaudRate; 5874#line 248 5875 __cil_tmp27 = (int )__cil_tmp26; 5876#line 248 5877 if (__cil_tmp27 & __cil_tmp25) { 5878#line 248 5879 tmp___10 = " 115200"; 5880 } else { 5881#line 248 5882 tmp___10 = ""; 5883 } 5884 } 5885 { 5886#line 248 5887 __cil_tmp28 = 1 << 4; 5888#line 248 5889 __cil_tmp29 = irda_desc->wBaudRate; 5890#line 248 5891 __cil_tmp30 = (int )__cil_tmp29; 5892#line 248 5893 if (__cil_tmp30 & __cil_tmp28) { 5894#line 248 5895 tmp___11 = " 57600"; 5896 } else { 5897#line 248 5898 tmp___11 = ""; 5899 } 5900 } 5901 { 5902#line 248 5903 __cil_tmp31 = 1 << 3; 5904#line 248 5905 __cil_tmp32 = irda_desc->wBaudRate; 5906#line 248 5907 __cil_tmp33 = (int )__cil_tmp32; 5908#line 248 5909 if (__cil_tmp33 & __cil_tmp31) { 5910#line 248 5911 tmp___12 = " 38400"; 5912 } else { 5913#line 248 5914 tmp___12 = ""; 5915 } 5916 } 5917 { 5918#line 248 5919 __cil_tmp34 = 1 << 2; 5920#line 248 5921 __cil_tmp35 = irda_desc->wBaudRate; 5922#line 248 5923 __cil_tmp36 = (int )__cil_tmp35; 5924#line 248 5925 if (__cil_tmp36 & __cil_tmp34) { 5926#line 248 5927 tmp___13 = " 19200"; 5928 } else { 5929#line 248 5930 tmp___13 = ""; 5931 } 5932 } 5933 { 5934#line 248 5935 __cil_tmp37 = 1 << 1; 5936#line 248 5937 __cil_tmp38 = irda_desc->wBaudRate; 5938#line 248 5939 __cil_tmp39 = (int )__cil_tmp38; 5940#line 248 5941 if (__cil_tmp39 & __cil_tmp37) { 5942#line 248 5943 tmp___14 = " 9600"; 5944 } else { 5945#line 248 5946 tmp___14 = ""; 5947 } 5948 } 5949 { 5950#line 248 5951 __cil_tmp40 = irda_desc->wBaudRate; 5952#line 248 5953 __cil_tmp41 = (int )__cil_tmp40; 5954#line 248 5955 if (__cil_tmp41 & 1) { 5956#line 248 5957 tmp___15 = " 2400"; 5958 } else { 5959#line 248 5960 tmp___15 = ""; 5961 } 5962 } 5963 { 5964#line 248 5965 printk("<7>%s: %s - Baud rates supported:%s%s%s%s%s%s%s%s%s\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 5966 "ir_startup", tmp___15, tmp___14, tmp___13, tmp___12, tmp___11, tmp___10, 5967 tmp___9, tmp___8, tmp___7); 5968 } 5969 } else { 5970 5971 } 5972#line 248 5973 goto while_break; 5974 } 5975 while_break___0: /* CIL Label */ ; 5976 } 5977 5978 while_break: ; 5979 { 5980#line 261 5981 __cil_tmp42 = irda_desc->bmAdditionalBOFs; 5982#line 261 5983 __cil_tmp43 = (int )__cil_tmp42; 5984#line 261 5985 if (__cil_tmp43 == 1) { 5986#line 261 5987 goto case_1; 5988 } else { 5989 { 5990#line 264 5991 __cil_tmp44 = 1 << 1; 5992#line 264 5993 __cil_tmp45 = irda_desc->bmAdditionalBOFs; 5994#line 264 5995 __cil_tmp46 = (int )__cil_tmp45; 5996#line 264 5997 if (__cil_tmp46 == __cil_tmp44) { 5998#line 264 5999 goto case_exp; 6000 } else { 6001 { 6002#line 267 6003 __cil_tmp47 = 1 << 2; 6004#line 267 6005 __cil_tmp48 = irda_desc->bmAdditionalBOFs; 6006#line 267 6007 __cil_tmp49 = (int )__cil_tmp48; 6008#line 267 6009 if (__cil_tmp49 == __cil_tmp47) { 6010#line 267 6011 goto case_exp___0; 6012 } else { 6013 { 6014#line 270 6015 __cil_tmp50 = 1 << 3; 6016#line 270 6017 __cil_tmp51 = irda_desc->bmAdditionalBOFs; 6018#line 270 6019 __cil_tmp52 = (int )__cil_tmp51; 6020#line 270 6021 if (__cil_tmp52 == __cil_tmp50) { 6022#line 270 6023 goto case_exp___1; 6024 } else { 6025 { 6026#line 273 6027 __cil_tmp53 = 1 << 4; 6028#line 273 6029 __cil_tmp54 = irda_desc->bmAdditionalBOFs; 6030#line 273 6031 __cil_tmp55 = (int )__cil_tmp54; 6032#line 273 6033 if (__cil_tmp55 == __cil_tmp53) { 6034#line 273 6035 goto case_exp___2; 6036 } else { 6037 { 6038#line 276 6039 __cil_tmp56 = 1 << 5; 6040#line 276 6041 __cil_tmp57 = irda_desc->bmAdditionalBOFs; 6042#line 276 6043 __cil_tmp58 = (int )__cil_tmp57; 6044#line 276 6045 if (__cil_tmp58 == __cil_tmp56) { 6046#line 276 6047 goto case_exp___3; 6048 } else { 6049 { 6050#line 279 6051 __cil_tmp59 = 1 << 6; 6052#line 279 6053 __cil_tmp60 = irda_desc->bmAdditionalBOFs; 6054#line 279 6055 __cil_tmp61 = (int )__cil_tmp60; 6056#line 279 6057 if (__cil_tmp61 == __cil_tmp59) { 6058#line 279 6059 goto case_exp___4; 6060 } else { 6061 { 6062#line 282 6063 __cil_tmp62 = 1 << 7; 6064#line 282 6065 __cil_tmp63 = irda_desc->bmAdditionalBOFs; 6066#line 282 6067 __cil_tmp64 = (int )__cil_tmp63; 6068#line 282 6069 if (__cil_tmp64 == __cil_tmp62) { 6070#line 282 6071 goto case_exp___5; 6072 } else { 6073#line 285 6074 goto switch_default; 6075#line 260 6076 if (0) { 6077 case_1: 6078#line 262 6079 ir_add_bof = (u8 )48; 6080#line 263 6081 goto switch_break; 6082 case_exp: 6083#line 265 6084 ir_add_bof = (u8 )24; 6085#line 266 6086 goto switch_break; 6087 case_exp___0: 6088#line 268 6089 ir_add_bof = (u8 )12; 6090#line 269 6091 goto switch_break; 6092 case_exp___1: 6093#line 271 6094 ir_add_bof = (u8 )6; 6095#line 272 6096 goto switch_break; 6097 case_exp___2: 6098#line 274 6099 ir_add_bof = (u8 )3; 6100#line 275 6101 goto switch_break; 6102 case_exp___3: 6103#line 277 6104 ir_add_bof = (u8 )2; 6105#line 278 6106 goto switch_break; 6107 case_exp___4: 6108#line 280 6109 ir_add_bof = (u8 )1; 6110#line 281 6111 goto switch_break; 6112 case_exp___5: 6113#line 283 6114 ir_add_bof = (u8 )0; 6115#line 284 6116 goto switch_break; 6117 switch_default: 6118#line 286 6119 goto switch_break; 6120 } else { 6121 switch_break: ; 6122 } 6123 } 6124 } 6125 } 6126 } 6127 } 6128 } 6129 } 6130 } 6131 } 6132 } 6133 } 6134 } 6135 } 6136 } 6137 } 6138 } 6139 { 6140#line 289 6141 __cil_tmp65 = (void const *)irda_desc; 6142#line 289 6143 kfree(__cil_tmp65); 6144 } 6145#line 291 6146 return (0); 6147} 6148} 6149#line 294 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 6150static int ir_open(struct tty_struct *tty , struct usb_serial_port *port ) 6151{ int i ; 6152 int tmp___7 ; 6153 unsigned char __cil_tmp5 ; 6154 int __cil_tmp6 ; 6155 unsigned long __cil_tmp7 ; 6156 unsigned long __cil_tmp8 ; 6157 unsigned long __cil_tmp9 ; 6158 struct urb *__cil_tmp10 ; 6159 6160 { 6161 { 6162#line 298 6163 while (1) { 6164 while_continue: /* CIL Label */ ; 6165 6166#line 298 6167 if (debug) { 6168 { 6169#line 298 6170 __cil_tmp5 = port->number; 6171#line 298 6172 __cil_tmp6 = (int )__cil_tmp5; 6173#line 298 6174 printk("<7>%s: %s - port %d\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 6175 "ir_open", __cil_tmp6); 6176 } 6177 } else { 6178 6179 } 6180#line 298 6181 goto while_break; 6182 } 6183 while_break___1: /* CIL Label */ ; 6184 } 6185 6186 while_break: 6187#line 300 6188 i = 0; 6189 { 6190#line 300 6191 while (1) { 6192 while_continue___0: /* CIL Label */ ; 6193 6194 { 6195#line 300 6196 __cil_tmp7 = 16UL / 8UL; 6197#line 300 6198 __cil_tmp8 = __cil_tmp7 + 0UL; 6199#line 300 6200 __cil_tmp9 = (unsigned long )i; 6201#line 300 6202 if (__cil_tmp9 < __cil_tmp8) { 6203 6204 } else { 6205#line 300 6206 goto while_break___0; 6207 } 6208 } 6209#line 301 6210 __cil_tmp10 = port->write_urbs[i]; 6211#line 301 6212 __cil_tmp10->transfer_flags = 64U; 6213#line 300 6214 i = i + 1; 6215 } 6216 while_break___2: /* CIL Label */ ; 6217 } 6218 6219 while_break___0: 6220 { 6221#line 304 6222 tmp___7 = usb_serial_generic_open(tty, port); 6223 } 6224#line 304 6225 return (tmp___7); 6226} 6227} 6228#line 307 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 6229static int ir_prepare_write_buffer(struct usb_serial_port *port , void *dest , size_t size ) 6230{ unsigned char *buf ; 6231 int count ; 6232 unsigned long __flags ; 6233 unsigned int __ret ; 6234 raw_spinlock_t *tmp___7 ; 6235 struct kfifo *__tmp ; 6236 unsigned char *__buf ; 6237 unsigned long __n ; 6238 size_t __recsize ; 6239 struct __kfifo *__kfifo ; 6240 unsigned int tmp___8 ; 6241 unsigned int tmp___9 ; 6242 unsigned int tmp___10 ; 6243 unsigned int tmp___11 ; 6244 unsigned int tmp ; 6245 unsigned int tmp___12 ; 6246 unsigned int tmp___13 ; 6247 unsigned int tmp___14 ; 6248 int __cil_tmp22 ; 6249 int __cil_tmp23 ; 6250 int __cil_tmp24 ; 6251 spinlock_t *__cil_tmp25 ; 6252 void *__cil_tmp26 ; 6253 unsigned int __cil_tmp27 ; 6254 void *__cil_tmp28 ; 6255 unsigned int __cil_tmp29 ; 6256 spinlock_t *__cil_tmp30 ; 6257 6258 { 6259#line 310 6260 buf = (unsigned char *)dest; 6261#line 320 6262 __cil_tmp22 = (int )ir_baud; 6263#line 320 6264 __cil_tmp23 = (int )ir_xbof; 6265#line 320 6266 __cil_tmp24 = __cil_tmp23 | __cil_tmp22; 6267#line 320 6268 *buf = (unsigned char )__cil_tmp24; 6269 { 6270#line 322 6271 while (1) { 6272 while_continue: /* CIL Label */ ; 6273 6274 { 6275#line 322 6276 while (1) { 6277 while_continue___0: /* CIL Label */ ; 6278 { 6279#line 322 6280 __cil_tmp25 = & port->lock; 6281#line 322 6282 tmp___7 = spinlock_check(__cil_tmp25); 6283#line 322 6284 __flags = _raw_spin_lock_irqsave(tmp___7); 6285 } 6286#line 322 6287 goto while_break___0; 6288 } 6289 while_break___2: /* CIL Label */ ; 6290 } 6291 6292 while_break___0: ; 6293#line 322 6294 goto while_break; 6295 } 6296 while_break___1: /* CIL Label */ ; 6297 } 6298 6299 while_break: 6300#line 322 6301 __tmp = & port->write_fifo; 6302#line 322 6303 __buf = buf + 1; 6304#line 322 6305 __n = size - 1UL; 6306#line 322 6307 __recsize = 0UL; 6308#line 322 6309 __kfifo = & __tmp->__annonCompField41.kfifo; 6310#line 322 6311 if (__recsize) { 6312 { 6313#line 322 6314 __cil_tmp26 = (void *)__buf; 6315#line 322 6316 __cil_tmp27 = (unsigned int )__n; 6317#line 322 6318 tmp___8 = __kfifo_out_r(__kfifo, __cil_tmp26, __cil_tmp27, __recsize); 6319#line 322 6320 tmp___10 = tmp___8; 6321 } 6322 } else { 6323 { 6324#line 322 6325 __cil_tmp28 = (void *)__buf; 6326#line 322 6327 __cil_tmp29 = (unsigned int )__n; 6328#line 322 6329 tmp___9 = __kfifo_out(__kfifo, __cil_tmp28, __cil_tmp29); 6330#line 322 6331 tmp___10 = tmp___9; 6332 } 6333 } 6334 { 6335#line 322 6336 tmp___13 = (unsigned int )__kfifo_uint_must_check_helper(tmp___10); 6337#line 322 6338 tmp = tmp___13; 6339#line 322 6340 __ret = tmp; 6341#line 322 6342 __cil_tmp30 = & port->lock; 6343#line 322 6344 spin_unlock_irqrestore(__cil_tmp30, __flags); 6345#line 322 6346 tmp___14 = (unsigned int )__kfifo_uint_must_check_helper(__ret); 6347#line 322 6348 tmp___12 = tmp___14; 6349#line 322 6350 tmp___11 = tmp___12; 6351#line 322 6352 count = (int )tmp___11; 6353 } 6354#line 324 6355 return (count + 1); 6356} 6357} 6358#line 327 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 6359static void ir_process_read_urb(struct urb *urb ) 6360{ struct usb_serial_port *port ; 6361 unsigned char *data ; 6362 struct tty_struct *tty ; 6363 void *__cil_tmp5 ; 6364 void *__cil_tmp6 ; 6365 u32 __cil_tmp7 ; 6366 unsigned char __cil_tmp8 ; 6367 int __cil_tmp9 ; 6368 unsigned char __cil_tmp10 ; 6369 int __cil_tmp11 ; 6370 int __cil_tmp12 ; 6371 u32 __cil_tmp13 ; 6372 struct tty_port *__cil_tmp14 ; 6373 unsigned char *__cil_tmp15 ; 6374 unsigned char const *__cil_tmp16 ; 6375 u32 __cil_tmp17 ; 6376 u32 __cil_tmp18 ; 6377 size_t __cil_tmp19 ; 6378 6379 { 6380#line 329 6381 __cil_tmp5 = urb->context; 6382#line 329 6383 port = (struct usb_serial_port *)__cil_tmp5; 6384#line 330 6385 __cil_tmp6 = urb->transfer_buffer; 6386#line 330 6387 data = (unsigned char *)__cil_tmp6; 6388 { 6389#line 333 6390 __cil_tmp7 = urb->actual_length; 6391#line 333 6392 if (! __cil_tmp7) { 6393#line 334 6394 return; 6395 } else { 6396 6397 } 6398 } 6399 { 6400#line 340 6401 __cil_tmp8 = *data; 6402#line 340 6403 __cil_tmp9 = (int )__cil_tmp8; 6404#line 340 6405 if (__cil_tmp9 & 15) { 6406#line 341 6407 __cil_tmp10 = *data; 6408#line 341 6409 __cil_tmp11 = (int )__cil_tmp10; 6410#line 341 6411 __cil_tmp12 = __cil_tmp11 & 15; 6412#line 341 6413 ir_baud = (u8 )__cil_tmp12; 6414 } else { 6415 6416 } 6417 } 6418 { 6419#line 343 6420 __cil_tmp13 = urb->actual_length; 6421#line 343 6422 if (__cil_tmp13 == 1U) { 6423#line 344 6424 return; 6425 } else { 6426 6427 } 6428 } 6429 { 6430#line 346 6431 __cil_tmp14 = & port->port; 6432#line 346 6433 tty = tty_port_tty_get(__cil_tmp14); 6434 } 6435#line 347 6436 if (! tty) { 6437#line 348 6438 return; 6439 } else { 6440 6441 } 6442 { 6443#line 349 6444 __cil_tmp15 = data + 1; 6445#line 349 6446 __cil_tmp16 = (unsigned char const *)__cil_tmp15; 6447#line 349 6448 __cil_tmp17 = urb->actual_length; 6449#line 349 6450 __cil_tmp18 = __cil_tmp17 - 1U; 6451#line 349 6452 __cil_tmp19 = (size_t )__cil_tmp18; 6453#line 349 6454 tty_insert_flip_string(tty, __cil_tmp16, __cil_tmp19); 6455#line 350 6456 tty_flip_buffer_push(tty); 6457#line 351 6458 tty_kref_put(tty); 6459 } 6460#line 352 6461 return; 6462} 6463} 6464#line 354 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 6465static void ir_set_termios_callback(struct urb *urb ) 6466{ struct usb_serial_port *port ; 6467 int status ; 6468 void *__cil_tmp4 ; 6469 unsigned char __cil_tmp5 ; 6470 int __cil_tmp6 ; 6471 void *__cil_tmp7 ; 6472 void const *__cil_tmp8 ; 6473 6474 { 6475#line 356 6476 __cil_tmp4 = urb->context; 6477#line 356 6478 port = (struct usb_serial_port *)__cil_tmp4; 6479#line 357 6480 status = urb->status; 6481 { 6482#line 359 6483 while (1) { 6484 while_continue: /* CIL Label */ ; 6485 6486#line 359 6487 if (debug) { 6488 { 6489#line 359 6490 __cil_tmp5 = port->number; 6491#line 359 6492 __cil_tmp6 = (int )__cil_tmp5; 6493#line 359 6494 printk("<7>%s: %s - port %d\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 6495 "ir_set_termios_callback", __cil_tmp6); 6496 } 6497 } else { 6498 6499 } 6500#line 359 6501 goto while_break; 6502 } 6503 while_break___1: /* CIL Label */ ; 6504 } 6505 6506 while_break: 6507 { 6508#line 361 6509 __cil_tmp7 = urb->transfer_buffer; 6510#line 361 6511 __cil_tmp8 = (void const *)__cil_tmp7; 6512#line 361 6513 kfree(__cil_tmp8); 6514 } 6515#line 363 6516 if (status) { 6517 { 6518#line 364 6519 while (1) { 6520 while_continue___0: /* CIL Label */ ; 6521 6522#line 364 6523 if (debug) { 6524 { 6525#line 364 6526 printk("<7>%s: %s - non-zero urb status: %d\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 6527 "ir_set_termios_callback", status); 6528 } 6529 } else { 6530 6531 } 6532#line 364 6533 goto while_break___0; 6534 } 6535 while_break___2: /* CIL Label */ ; 6536 } 6537 6538 while_break___0: ; 6539 } else { 6540 6541 } 6542#line 365 6543 return; 6544} 6545} 6546#line 367 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 6547static void ir_set_termios(struct tty_struct *tty , struct usb_serial_port *port , 6548 struct ktermios *old_termios ) 6549{ struct urb *urb ; 6550 unsigned char *transfer_buffer ; 6551 int result ; 6552 speed_t baud ; 6553 int ir_baud___0 ; 6554 void *tmp___7 ; 6555 unsigned int tmp___8 ; 6556 unsigned char __cil_tmp11 ; 6557 int __cil_tmp12 ; 6558 int __cil_tmp13 ; 6559 int __cil_tmp14 ; 6560 int __cil_tmp15 ; 6561 int __cil_tmp16 ; 6562 int __cil_tmp17 ; 6563 int __cil_tmp18 ; 6564 int __cil_tmp19 ; 6565 int __cil_tmp20 ; 6566 int __cil_tmp21 ; 6567 u8 __cil_tmp22 ; 6568 struct ktermios *__cil_tmp23 ; 6569 struct device *__cil_tmp24 ; 6570 struct device const *__cil_tmp25 ; 6571 size_t __cil_tmp26 ; 6572 struct device *__cil_tmp27 ; 6573 struct device const *__cil_tmp28 ; 6574 int __cil_tmp29 ; 6575 int __cil_tmp30 ; 6576 struct usb_serial *__cil_tmp31 ; 6577 struct usb_device *__cil_tmp32 ; 6578 __u8 __cil_tmp33 ; 6579 unsigned int __cil_tmp34 ; 6580 struct usb_serial *__cil_tmp35 ; 6581 struct usb_device *__cil_tmp36 ; 6582 int __cil_tmp37 ; 6583 unsigned int __cil_tmp38 ; 6584 unsigned int __cil_tmp39 ; 6585 void *__cil_tmp40 ; 6586 void *__cil_tmp41 ; 6587 struct device *__cil_tmp42 ; 6588 struct device const *__cil_tmp43 ; 6589 void const *__cil_tmp44 ; 6590 6591 { 6592 { 6593#line 376 6594 while (1) { 6595 while_continue: /* CIL Label */ ; 6596 6597#line 376 6598 if (debug) { 6599 { 6600#line 376 6601 __cil_tmp11 = port->number; 6602#line 376 6603 __cil_tmp12 = (int )__cil_tmp11; 6604#line 376 6605 printk("<7>%s: %s - port %d\n", "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c", 6606 "ir_set_termios", __cil_tmp12); 6607 } 6608 } else { 6609 6610 } 6611#line 376 6612 goto while_break; 6613 } 6614 while_break___0: /* CIL Label */ ; 6615 } 6616 6617 while_break: 6618 { 6619#line 378 6620 baud = tty_get_baud_rate(tty); 6621 } 6622 { 6623#line 387 6624 __cil_tmp13 = (int )baud; 6625#line 387 6626 if (__cil_tmp13 == 2400) { 6627#line 387 6628 goto case_2400; 6629 } else { 6630 { 6631#line 390 6632 __cil_tmp14 = (int )baud; 6633#line 390 6634 if (__cil_tmp14 == 9600) { 6635#line 390 6636 goto case_9600; 6637 } else { 6638 { 6639#line 393 6640 __cil_tmp15 = (int )baud; 6641#line 393 6642 if (__cil_tmp15 == 19200) { 6643#line 393 6644 goto case_19200; 6645 } else { 6646 { 6647#line 396 6648 __cil_tmp16 = (int )baud; 6649#line 396 6650 if (__cil_tmp16 == 38400) { 6651#line 396 6652 goto case_38400; 6653 } else { 6654 { 6655#line 399 6656 __cil_tmp17 = (int )baud; 6657#line 399 6658 if (__cil_tmp17 == 57600) { 6659#line 399 6660 goto case_57600; 6661 } else { 6662 { 6663#line 402 6664 __cil_tmp18 = (int )baud; 6665#line 402 6666 if (__cil_tmp18 == 115200) { 6667#line 402 6668 goto case_115200; 6669 } else { 6670 { 6671#line 405 6672 __cil_tmp19 = (int )baud; 6673#line 405 6674 if (__cil_tmp19 == 576000) { 6675#line 405 6676 goto case_576000; 6677 } else { 6678 { 6679#line 408 6680 __cil_tmp20 = (int )baud; 6681#line 408 6682 if (__cil_tmp20 == 1152000) { 6683#line 408 6684 goto case_1152000; 6685 } else { 6686 { 6687#line 411 6688 __cil_tmp21 = (int )baud; 6689#line 411 6690 if (__cil_tmp21 == 4000000) { 6691#line 411 6692 goto case_4000000; 6693 } else { 6694#line 414 6695 goto switch_default; 6696#line 386 6697 if (0) { 6698 case_2400: 6699#line 388 6700 ir_baud___0 = 1; 6701#line 389 6702 goto switch_break; 6703 case_9600: 6704#line 391 6705 ir_baud___0 = 1 << 1; 6706#line 392 6707 goto switch_break; 6708 case_19200: 6709#line 394 6710 ir_baud___0 = 1 << 2; 6711#line 395 6712 goto switch_break; 6713 case_38400: 6714#line 397 6715 ir_baud___0 = 1 << 3; 6716#line 398 6717 goto switch_break; 6718 case_57600: 6719#line 400 6720 ir_baud___0 = 1 << 4; 6721#line 401 6722 goto switch_break; 6723 case_115200: 6724#line 403 6725 ir_baud___0 = 1 << 5; 6726#line 404 6727 goto switch_break; 6728 case_576000: 6729#line 406 6730 ir_baud___0 = 1 << 6; 6731#line 407 6732 goto switch_break; 6733 case_1152000: 6734#line 409 6735 ir_baud___0 = 1 << 7; 6736#line 410 6737 goto switch_break; 6738 case_4000000: 6739#line 412 6740 ir_baud___0 = 1 << 8; 6741#line 413 6742 goto switch_break; 6743 switch_default: 6744#line 415 6745 ir_baud___0 = 1 << 1; 6746#line 416 6747 baud = (speed_t )9600; 6748 } else { 6749 switch_break: ; 6750 } 6751 } 6752 } 6753 } 6754 } 6755 } 6756 } 6757 } 6758 } 6759 } 6760 } 6761 } 6762 } 6763 } 6764 } 6765 } 6766 } 6767 } 6768 } 6769#line 419 6770 if (xbof == -1) { 6771 { 6772#line 420 6773 ir_xbof = ir_xbof_change(ir_add_bof); 6774 } 6775 } else { 6776 { 6777#line 422 6778 __cil_tmp22 = (u8 )xbof; 6779#line 422 6780 ir_xbof = ir_xbof_change(__cil_tmp22); 6781 } 6782 } 6783 { 6784#line 425 6785 __cil_tmp23 = tty->termios; 6786#line 425 6787 tty_termios_copy_hw(__cil_tmp23, old_termios); 6788#line 426 6789 tty_encode_baud_rate(tty, baud, baud); 6790#line 431 6791 urb = usb_alloc_urb(0, 208U); 6792 } 6793#line 432 6794 if (! urb) { 6795 { 6796#line 433 6797 __cil_tmp24 = & port->dev; 6798#line 433 6799 __cil_tmp25 = (struct device const *)__cil_tmp24; 6800#line 433 6801 dev_err(__cil_tmp25, "%s - no more urbs\n", "ir_set_termios"); 6802 } 6803#line 434 6804 return; 6805 } else { 6806 6807 } 6808 { 6809#line 436 6810 __cil_tmp26 = (size_t )1; 6811#line 436 6812 tmp___7 = kmalloc(__cil_tmp26, 208U); 6813#line 436 6814 transfer_buffer = (unsigned char *)tmp___7; 6815 } 6816#line 437 6817 if (! transfer_buffer) { 6818 { 6819#line 438 6820 __cil_tmp27 = & port->dev; 6821#line 438 6822 __cil_tmp28 = (struct device const *)__cil_tmp27; 6823#line 438 6824 dev_err(__cil_tmp28, "%s - out of memory\n", "ir_set_termios"); 6825 } 6826#line 439 6827 goto err_buf; 6828 } else { 6829 6830 } 6831 { 6832#line 442 6833 __cil_tmp29 = (int )ir_xbof; 6834#line 442 6835 __cil_tmp30 = __cil_tmp29 | ir_baud___0; 6836#line 442 6837 *transfer_buffer = (unsigned char )__cil_tmp30; 6838#line 444 6839 __cil_tmp31 = port->serial; 6840#line 444 6841 __cil_tmp32 = __cil_tmp31->dev; 6842#line 444 6843 __cil_tmp33 = port->bulk_out_endpointAddress; 6844#line 444 6845 __cil_tmp34 = (unsigned int )__cil_tmp33; 6846#line 444 6847 tmp___8 = __create_pipe(__cil_tmp32, __cil_tmp34); 6848#line 444 6849 __cil_tmp35 = port->serial; 6850#line 444 6851 __cil_tmp36 = __cil_tmp35->dev; 6852#line 444 6853 __cil_tmp37 = 3 << 30; 6854#line 444 6855 __cil_tmp38 = (unsigned int )__cil_tmp37; 6856#line 444 6857 __cil_tmp39 = __cil_tmp38 | tmp___8; 6858#line 444 6859 __cil_tmp40 = (void *)transfer_buffer; 6860#line 444 6861 __cil_tmp41 = (void *)port; 6862#line 444 6863 usb_fill_bulk_urb(urb, __cil_tmp36, __cil_tmp39, __cil_tmp40, 1, & ir_set_termios_callback, 6864 __cil_tmp41); 6865#line 454 6866 urb->transfer_flags = 64U; 6867#line 456 6868 result = usb_submit_urb(urb, 208U); 6869 } 6870#line 457 6871 if (result) { 6872 { 6873#line 458 6874 __cil_tmp42 = & port->dev; 6875#line 458 6876 __cil_tmp43 = (struct device const *)__cil_tmp42; 6877#line 458 6878 dev_err(__cil_tmp43, "%s - failed to submit urb: %d\n", "ir_set_termios", result); 6879 } 6880#line 460 6881 goto err_subm; 6882 } else { 6883 6884 } 6885 { 6886#line 463 6887 usb_free_urb(urb); 6888 } 6889#line 465 6890 return; 6891 err_subm: 6892 { 6893#line 467 6894 __cil_tmp44 = (void const *)transfer_buffer; 6895#line 467 6896 kfree(__cil_tmp44); 6897 } 6898 err_buf: 6899 { 6900#line 469 6901 usb_free_urb(urb); 6902 } 6903#line 470 6904 return; 6905} 6906} 6907#line 472 6908static int ir_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ; 6909#line 472 6910static int ir_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ; 6911#line 472 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 6912static int ir_init(void) 6913{ int retval ; 6914 6915 { 6916#line 476 6917 if (buffer_size) { 6918#line 477 6919 ir_device.bulk_in_size = (size_t )buffer_size; 6920#line 478 6921 ir_device.bulk_out_size = (size_t )buffer_size; 6922 } else { 6923 6924 } 6925 { 6926#line 481 6927 retval = usb_serial_register(& ir_device); 6928 } 6929#line 482 6930 if (retval) { 6931#line 483 6932 goto failed_usb_serial_register; 6933 } else { 6934 6935 } 6936 { 6937#line 485 6938 retval = usb_register(& ir_driver); 6939 } 6940#line 486 6941 if (retval) { 6942#line 487 6943 goto failed_usb_register; 6944 } else { 6945 6946 } 6947 { 6948#line 489 6949 printk("<6>ir_usb: v0.5:USB IR Dongle driver\n"); 6950 } 6951#line 492 6952 return (0); 6953 failed_usb_register: 6954 { 6955#line 495 6956 usb_serial_deregister(& ir_device); 6957 } 6958 failed_usb_serial_register: 6959#line 498 6960 return (retval); 6961} 6962} 6963#line 501 6964static void ir_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ; 6965#line 501 6966static void ir_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ; 6967#line 501 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 6968static void ir_exit(void) 6969{ 6970 6971 { 6972 { 6973#line 503 6974 usb_deregister(& ir_driver); 6975#line 504 6976 usb_serial_deregister(& ir_device); 6977 } 6978#line 505 6979 return; 6980} 6981} 6982#line 508 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 6983int init_module(void) 6984{ int tmp___7 ; 6985 6986 { 6987 { 6988#line 508 6989 tmp___7 = ir_init(); 6990 } 6991#line 508 6992 return (tmp___7); 6993} 6994} 6995#line 509 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 6996void cleanup_module(void) 6997{ 6998 6999 { 7000 { 7001#line 509 7002 ir_exit(); 7003 } 7004#line 509 7005 return; 7006} 7007} 7008#line 511 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7009static char const __mod_author511[77] __attribute__((__used__, __unused__, __section__(".modinfo"), 7010__aligned__(1))) = 7011#line 511 7012 { (char const )'a', (char const )'u', (char const )'t', (char const )'h', 7013 (char const )'o', (char const )'r', (char const )'=', (char const )'G', 7014 (char const )'r', (char const )'e', (char const )'g', (char const )' ', 7015 (char const )'K', (char const )'r', (char const )'o', (char const )'a', 7016 (char const )'h', (char const )'-', (char const )'H', (char const )'a', 7017 (char const )'r', (char const )'t', (char const )'m', (char const )'a', 7018 (char const )'n', (char const )' ', (char const )'<', (char const )'g', 7019 (char const )'r', (char const )'e', (char const )'g', (char const )'@', 7020 (char const )'k', (char const )'r', (char const )'o', (char const )'a', 7021 (char const )'h', (char const )'.', (char const )'c', (char const )'o', 7022 (char const )'m', (char const )'>', (char const )',', (char const )' ', 7023 (char const )'J', (char const )'o', (char const )'h', (char const )'a', 7024 (char const )'n', (char const )' ', (char const )'H', (char const )'o', 7025 (char const )'v', (char const )'o', (char const )'l', (char const )'d', 7026 (char const )' ', (char const )'<', (char const )'j', (char const )'h', 7027 (char const )'o', (char const )'v', (char const )'o', (char const )'l', 7028 (char const )'d', (char const )'@', (char const )'g', (char const )'m', 7029 (char const )'a', (char const )'i', (char const )'l', (char const )'.', 7030 (char const )'c', (char const )'o', (char const )'m', (char const )'>', 7031 (char const )'\000'}; 7032#line 512 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7033static char const __mod_description512[33] __attribute__((__used__, __unused__, 7034__section__(".modinfo"), __aligned__(1))) = 7035#line 512 7036 { (char const )'d', (char const )'e', (char const )'s', (char const )'c', 7037 (char const )'r', (char const )'i', (char const )'p', (char const )'t', 7038 (char const )'i', (char const )'o', (char const )'n', (char const )'=', 7039 (char const )'U', (char const )'S', (char const )'B', (char const )' ', 7040 (char const )'I', (char const )'R', (char const )' ', (char const )'D', 7041 (char const )'o', (char const )'n', (char const )'g', (char const )'l', 7042 (char const )'e', (char const )' ', (char const )'d', (char const )'r', 7043 (char const )'i', (char const )'v', (char const )'e', (char const )'r', 7044 (char const )'\000'}; 7045#line 513 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7046static char const __mod_license513[12] __attribute__((__used__, __unused__, __section__(".modinfo"), 7047__aligned__(1))) = 7048#line 513 7049 { (char const )'l', (char const )'i', (char const )'c', (char const )'e', 7050 (char const )'n', (char const )'s', (char const )'e', (char const )'=', 7051 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'}; 7052#line 515 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7053static char const __param_str_debug[6] = { (char const )'d', (char const )'e', (char const )'b', (char const )'u', 7054 (char const )'g', (char const )'\000'}; 7055#line 515 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7056static struct kernel_param const __param_debug __attribute__((__used__, __unused__, 7057__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_debug, (struct kernel_param_ops const *)(& param_ops_bool), (u16 )420, 7058 (u16 )0, {(void *)(& debug)}}; 7059#line 515 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7060static char const __mod_debugtype515[20] __attribute__((__used__, __unused__, __section__(".modinfo"), 7061__aligned__(1))) = 7062#line 515 7063 { (char const )'p', (char const )'a', (char const )'r', (char const )'m', 7064 (char const )'t', (char const )'y', (char const )'p', (char const )'e', 7065 (char const )'=', (char const )'d', (char const )'e', (char const )'b', 7066 (char const )'u', (char const )'g', (char const )':', (char const )'b', 7067 (char const )'o', (char const )'o', (char const )'l', (char const )'\000'}; 7068#line 516 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7069static char const __mod_debug516[32] __attribute__((__used__, __unused__, __section__(".modinfo"), 7070__aligned__(1))) = 7071#line 516 7072 { (char const )'p', (char const )'a', (char const )'r', (char const )'m', 7073 (char const )'=', (char const )'d', (char const )'e', (char const )'b', 7074 (char const )'u', (char const )'g', (char const )':', (char const )'D', 7075 (char const )'e', (char const )'b', (char const )'u', (char const )'g', 7076 (char const )' ', (char const )'e', (char const )'n', (char const )'a', 7077 (char const )'b', (char const )'l', (char const )'e', (char const )'d', 7078 (char const )' ', (char const )'o', (char const )'r', (char const )' ', 7079 (char const )'n', (char const )'o', (char const )'t', (char const )'\000'}; 7080#line 517 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7081static char const __param_str_xbof[5] = { (char const )'x', (char const )'b', (char const )'o', (char const )'f', 7082 (char const )'\000'}; 7083#line 517 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7084static struct kernel_param const __param_xbof __attribute__((__used__, __unused__, 7085__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_xbof, (struct kernel_param_ops const *)(& param_ops_int), (u16 )0, 7086 (u16 )0, {(void *)(& xbof)}}; 7087#line 517 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7088static char const __mod_xboftype517[18] __attribute__((__used__, __unused__, __section__(".modinfo"), 7089__aligned__(1))) = 7090#line 517 7091 { (char const )'p', (char const )'a', (char const )'r', (char const )'m', 7092 (char const )'t', (char const )'y', (char const )'p', (char const )'e', 7093 (char const )'=', (char const )'x', (char const )'b', (char const )'o', 7094 (char const )'f', (char const )':', (char const )'i', (char const )'n', 7095 (char const )'t', (char const )'\000'}; 7096#line 518 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7097static char const __mod_xbof518[41] __attribute__((__used__, __unused__, __section__(".modinfo"), 7098__aligned__(1))) = 7099#line 518 7100 { (char const )'p', (char const )'a', (char const )'r', (char const )'m', 7101 (char const )'=', (char const )'x', (char const )'b', (char const )'o', 7102 (char const )'f', (char const )':', (char const )'F', (char const )'o', 7103 (char const )'r', (char const )'c', (char const )'e', (char const )' ', 7104 (char const )'s', (char const )'p', (char const )'e', (char const )'c', 7105 (char const )'i', (char const )'f', (char const )'i', (char const )'c', 7106 (char const )' ', (char const )'n', (char const )'u', (char const )'m', 7107 (char const )'b', (char const )'e', (char const )'r', (char const )' ', 7108 (char const )'o', (char const )'f', (char const )' ', (char const )'X', 7109 (char const )'B', (char const )'O', (char const )'F', (char const )'s', 7110 (char const )'\000'}; 7111#line 519 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7112static char const __param_str_buffer_size[12] = 7113#line 519 7114 { (char const )'b', (char const )'u', (char const )'f', (char const )'f', 7115 (char const )'e', (char const )'r', (char const )'_', (char const )'s', 7116 (char const )'i', (char const )'z', (char const )'e', (char const )'\000'}; 7117#line 519 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7118static struct kernel_param const __param_buffer_size __attribute__((__used__, __unused__, 7119__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_buffer_size, (struct kernel_param_ops const *)(& param_ops_int), 7120 (u16 )0, (u16 )0, {(void *)(& buffer_size)}}; 7121#line 519 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7122static char const __mod_buffer_sizetype519[25] __attribute__((__used__, __unused__, 7123__section__(".modinfo"), __aligned__(1))) = 7124#line 519 7125 { (char const )'p', (char const )'a', (char const )'r', (char const )'m', 7126 (char const )'t', (char const )'y', (char const )'p', (char const )'e', 7127 (char const )'=', (char const )'b', (char const )'u', (char const )'f', 7128 (char const )'f', (char const )'e', (char const )'r', (char const )'_', 7129 (char const )'s', (char const )'i', (char const )'z', (char const )'e', 7130 (char const )':', (char const )'i', (char const )'n', (char const )'t', 7131 (char const )'\000'}; 7132#line 520 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7133static char const __mod_buffer_size520[46] __attribute__((__used__, __unused__, 7134__section__(".modinfo"), __aligned__(1))) = 7135#line 520 7136 { (char const )'p', (char const )'a', (char const )'r', (char const )'m', 7137 (char const )'=', (char const )'b', (char const )'u', (char const )'f', 7138 (char const )'f', (char const )'e', (char const )'r', (char const )'_', 7139 (char const )'s', (char const )'i', (char const )'z', (char const )'e', 7140 (char const )':', (char const )'S', (char const )'i', (char const )'z', 7141 (char const )'e', (char const )' ', (char const )'o', (char const )'f', 7142 (char const )' ', (char const )'t', (char const )'h', (char const )'e', 7143 (char const )' ', (char const )'t', (char const )'r', (char const )'a', 7144 (char const )'n', (char const )'s', (char const )'f', (char const )'e', 7145 (char const )'r', (char const )' ', (char const )'b', (char const )'u', 7146 (char const )'f', (char const )'f', (char const )'e', (char const )'r', 7147 (char const )'s', (char const )'\000'}; 7148#line 539 7149void ldv_check_final_state(void) __attribute__((__ldv_model__)) ; 7150#line 542 7151extern void ldv_check_return_value(int res ) ; 7152#line 545 7153extern void ldv_initialize(void) ; 7154#line 548 7155extern int nondet_int(void) ; 7156#line 551 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7157int LDV_IN_INTERRUPT ; 7158#line 588 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7159static int res_ir_open_4 ; 7160#line 554 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.ko--X--bulklinux-3.0.1--X--68_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/68_1/drivers/usb/serial/ir-usb.c.common.c" 7161void main(void) 7162{ struct tty_struct *var_group1 ; 7163 struct usb_serial_port *var_group2 ; 7164 struct ktermios *var_ir_set_termios_8_p2 ; 7165 struct usb_serial *var_group3 ; 7166 void *var_ir_prepare_write_buffer_5_p1 ; 7167 size_t var_ir_prepare_write_buffer_5_p2 ; 7168 struct urb *var_group4 ; 7169 int tmp___7 ; 7170 int ldv_s_ir_device_usb_serial_driver ; 7171 int tmp___8 ; 7172 int tmp___9 ; 7173 int __cil_tmp12 ; 7174 7175 { 7176 { 7177#line 614 7178 LDV_IN_INTERRUPT = 1; 7179#line 623 7180 ldv_initialize(); 7181#line 633 7182 tmp___7 = ir_init(); 7183 } 7184#line 633 7185 if (tmp___7) { 7186#line 634 7187 goto ldv_final; 7188 } else { 7189 7190 } 7191#line 635 7192 ldv_s_ir_device_usb_serial_driver = 0; 7193 { 7194#line 639 7195 while (1) { 7196 while_continue: /* CIL Label */ ; 7197 { 7198#line 639 7199 tmp___9 = nondet_int(); 7200 } 7201#line 639 7202 if (tmp___9) { 7203 7204 } else { 7205 { 7206#line 639 7207 __cil_tmp12 = ldv_s_ir_device_usb_serial_driver == 0; 7208#line 639 7209 if (! __cil_tmp12) { 7210 7211 } else { 7212#line 639 7213 goto while_break; 7214 } 7215 } 7216 } 7217 { 7218#line 643 7219 tmp___8 = nondet_int(); 7220 } 7221#line 645 7222 if (tmp___8 == 0) { 7223#line 645 7224 goto case_0; 7225 } else 7226#line 668 7227 if (tmp___8 == 1) { 7228#line 668 7229 goto case_1; 7230 } else 7231#line 688 7232 if (tmp___8 == 2) { 7233#line 688 7234 goto case_2; 7235 } else 7236#line 708 7237 if (tmp___8 == 3) { 7238#line 708 7239 goto case_3; 7240 } else 7241#line 728 7242 if (tmp___8 == 4) { 7243#line 728 7244 goto case_4; 7245 } else { 7246#line 748 7247 goto switch_default; 7248#line 643 7249 if (0) { 7250 case_0: 7251#line 648 7252 if (ldv_s_ir_device_usb_serial_driver == 0) { 7253 { 7254#line 657 7255 res_ir_open_4 = ir_open(var_group1, var_group2); 7256#line 658 7257 ldv_check_return_value(res_ir_open_4); 7258 } 7259#line 659 7260 if (res_ir_open_4) { 7261#line 660 7262 goto ldv_module_exit; 7263 } else { 7264 7265 } 7266#line 661 7267 ldv_s_ir_device_usb_serial_driver = 0; 7268 } else { 7269 7270 } 7271#line 667 7272 goto switch_break; 7273 case_1: 7274 { 7275#line 680 7276 ir_set_termios(var_group1, var_group2, var_ir_set_termios_8_p2); 7277 } 7278#line 687 7279 goto switch_break; 7280 case_2: 7281 { 7282#line 700 7283 ir_startup(var_group3); 7284 } 7285#line 707 7286 goto switch_break; 7287 case_3: 7288 { 7289#line 720 7290 ir_prepare_write_buffer(var_group2, var_ir_prepare_write_buffer_5_p1, var_ir_prepare_write_buffer_5_p2); 7291 } 7292#line 727 7293 goto switch_break; 7294 case_4: 7295 { 7296#line 740 7297 ir_process_read_urb(var_group4); 7298 } 7299#line 747 7300 goto switch_break; 7301 switch_default: 7302#line 748 7303 goto switch_break; 7304 } else { 7305 switch_break: ; 7306 } 7307 } 7308 } 7309 while_break___0: /* CIL Label */ ; 7310 } 7311 7312 while_break: ; 7313 ldv_module_exit: 7314 { 7315#line 764 7316 ir_exit(); 7317 } 7318 ldv_final: 7319 { 7320#line 767 7321 ldv_check_final_state(); 7322 } 7323#line 770 7324 return; 7325} 7326} 7327#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.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" 7328void ldv_blast_assert(void) 7329{ 7330 7331 { 7332 ERROR: 7333#line 6 7334 goto ERROR; 7335} 7336} 7337#line 7 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.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" 7338extern void *ldv_undefined_pointer(void) ; 7339#line 10 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.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" 7340void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ; 7341#line 22 7342void ldv_assume_stop(void) __attribute__((__ldv_model_inline__)) ; 7343#line 22 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.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" 7344void ldv_assume_stop(void) 7345{ 7346 7347 { 7348 LDV_STOP: 7349#line 23 7350 goto LDV_STOP; 7351} 7352} 7353#line 29 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.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" 7354int ldv_urb_state = 0; 7355#line 31 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.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" 7356int ldv_coherent_state = 0; 7357#line 62 7358void *usb_alloc_coherent(struct usb_device *dev , size_t size , gfp_t mem_flags , 7359 dma_addr_t *dma ) __attribute__((__ldv_model__)) ; 7360#line 62 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.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" 7361void *usb_alloc_coherent(struct usb_device *dev , size_t size , gfp_t mem_flags , 7362 dma_addr_t *dma ) 7363{ void *arbitrary_memory ; 7364 void *tmp___7 ; 7365 7366 { 7367 { 7368#line 64 7369 while (1) { 7370 while_continue: /* CIL Label */ ; 7371 { 7372#line 64 7373 tmp___7 = ldv_undefined_pointer(); 7374#line 64 7375 arbitrary_memory = tmp___7; 7376 } 7377#line 64 7378 if (! arbitrary_memory) { 7379#line 64 7380 return ((void *)0); 7381 } else { 7382 7383 } 7384#line 64 7385 ldv_coherent_state = ldv_coherent_state + 1; 7386#line 64 7387 return (arbitrary_memory); 7388#line 64 7389 goto while_break; 7390 } 7391 while_break___0: /* CIL Label */ ; 7392 } 7393 7394 while_break: ; 7395#line 65 7396 return ((void *)0); 7397} 7398} 7399#line 68 7400void usb_free_coherent(struct usb_device *dev , size_t size , void *addr , dma_addr_t dma ) __attribute__((__ldv_model__)) ; 7401#line 68 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.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" 7402void usb_free_coherent(struct usb_device *dev , size_t size , void *addr , dma_addr_t dma ) 7403{ void *__cil_tmp5 ; 7404 unsigned long __cil_tmp6 ; 7405 unsigned long __cil_tmp7 ; 7406 int __cil_tmp8 ; 7407 7408 { 7409 { 7410#line 70 7411 while (1) { 7412 while_continue: /* CIL Label */ ; 7413 7414 { 7415#line 70 7416 __cil_tmp5 = (void *)0; 7417#line 70 7418 __cil_tmp6 = (unsigned long )__cil_tmp5; 7419#line 70 7420 __cil_tmp7 = (unsigned long )addr; 7421#line 70 7422 __cil_tmp8 = __cil_tmp7 != __cil_tmp6; 7423#line 70 7424 if (! __cil_tmp8) { 7425 { 7426#line 70 7427 ldv_assume_stop(); 7428 } 7429 } else { 7430 7431 } 7432 } 7433#line 70 7434 if (addr) { 7435#line 70 7436 if (ldv_coherent_state >= 1) { 7437 7438 } else { 7439 { 7440#line 70 7441 ldv_blast_assert(); 7442 } 7443 } 7444#line 70 7445 ldv_coherent_state = ldv_coherent_state - 1; 7446 } else { 7447 7448 } 7449#line 70 7450 goto while_break; 7451 } 7452 while_break___0: /* CIL Label */ ; 7453 } 7454 7455 while_break: ; 7456#line 71 7457 return; 7458} 7459} 7460#line 74 7461struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags ) __attribute__((__ldv_model__)) ; 7462#line 74 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.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" 7463struct urb *usb_alloc_urb(int iso_packets , gfp_t mem_flags ) 7464{ void *arbitrary_memory ; 7465 void *tmp___7 ; 7466 void *__cil_tmp5 ; 7467 7468 { 7469 { 7470#line 75 7471 while (1) { 7472 while_continue: /* CIL Label */ ; 7473 { 7474#line 75 7475 tmp___7 = ldv_undefined_pointer(); 7476#line 75 7477 arbitrary_memory = tmp___7; 7478 } 7479#line 75 7480 if (! arbitrary_memory) { 7481 { 7482#line 75 7483 __cil_tmp5 = (void *)0; 7484#line 75 7485 return ((struct urb *)__cil_tmp5); 7486 } 7487 } else { 7488 7489 } 7490#line 75 7491 ldv_urb_state = ldv_urb_state + 1; 7492#line 75 7493 return ((struct urb *)arbitrary_memory); 7494#line 75 7495 goto while_break; 7496 } 7497 while_break___0: /* CIL Label */ ; 7498 } 7499 7500 while_break: ; 7501#line 76 7502 return ((struct urb *)0); 7503} 7504} 7505#line 79 7506void usb_free_urb(struct urb *urb ) __attribute__((__ldv_model__)) ; 7507#line 79 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.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" 7508void usb_free_urb(struct urb *urb ) 7509{ struct urb *__cil_tmp2 ; 7510 unsigned long __cil_tmp3 ; 7511 unsigned long __cil_tmp4 ; 7512 int __cil_tmp5 ; 7513 7514 { 7515 { 7516#line 80 7517 while (1) { 7518 while_continue: /* CIL Label */ ; 7519 7520 { 7521#line 80 7522 __cil_tmp2 = (struct urb *)0; 7523#line 80 7524 __cil_tmp3 = (unsigned long )__cil_tmp2; 7525#line 80 7526 __cil_tmp4 = (unsigned long )urb; 7527#line 80 7528 __cil_tmp5 = __cil_tmp4 != __cil_tmp3; 7529#line 80 7530 if (! __cil_tmp5) { 7531 { 7532#line 80 7533 ldv_assume_stop(); 7534 } 7535 } else { 7536 7537 } 7538 } 7539#line 80 7540 if (urb) { 7541#line 80 7542 if (ldv_urb_state >= 1) { 7543 7544 } else { 7545 { 7546#line 80 7547 ldv_blast_assert(); 7548 } 7549 } 7550#line 80 7551 ldv_urb_state = ldv_urb_state - 1; 7552 } else { 7553 7554 } 7555#line 80 7556 goto while_break; 7557 } 7558 while_break___0: /* CIL Label */ ; 7559 } 7560 7561 while_break: ; 7562#line 81 7563 return; 7564} 7565} 7566#line 84 7567void ldv_check_final_state(void) __attribute__((__ldv_model__)) ; 7568#line 84 "/anthill/stuff/tacas-comp/work/current--X--drivers/usb/serial/ir-usb.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" 7569void ldv_check_final_state(void) 7570{ 7571 7572 { 7573#line 86 7574 if (ldv_urb_state == 0) { 7575 7576 } else { 7577 { 7578#line 86 7579 ldv_blast_assert(); 7580 } 7581 } 7582#line 88 7583 if (ldv_coherent_state == 0) { 7584 7585 } else { 7586 { 7587#line 88 7588 ldv_blast_assert(); 7589 } 7590 } 7591#line 89 7592 return; 7593} 7594}

User:	Jiri Slaby
Error type:	Reachable Error Location
Error type description:	A specified error location is reachable in some program path
File location:	ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko_safe.cil.out.i.pp.cil.c
Line in file:	7332
Project:	SV-COMP 2013
Project version:	2.6.28
Tools:	Manual Work
Entered:	2013-01-17 16:57:54 UTC

ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 147

Source: