Showing error 305

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