Showing error 206

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 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

   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<