Showing error 723

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