Showing error 1278

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