Showing error 677

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