Showing error 687

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