Showing error 495

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--misc--isl29020.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3667
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 20 "include/asm-generic/int-ll64.h"
   5typedef unsigned char __u8;
   6#line 23 "include/asm-generic/int-ll64.h"
   7typedef unsigned short __u16;
   8#line 25 "include/asm-generic/int-ll64.h"
   9typedef int __s32;
  10#line 26 "include/asm-generic/int-ll64.h"
  11typedef unsigned int __u32;
  12#line 30 "include/asm-generic/int-ll64.h"
  13typedef unsigned long long __u64;
  14#line 43 "include/asm-generic/int-ll64.h"
  15typedef unsigned char u8;
  16#line 45 "include/asm-generic/int-ll64.h"
  17typedef short s16;
  18#line 46 "include/asm-generic/int-ll64.h"
  19typedef unsigned short u16;
  20#line 48 "include/asm-generic/int-ll64.h"
  21typedef int s32;
  22#line 49 "include/asm-generic/int-ll64.h"
  23typedef unsigned int u32;
  24#line 51 "include/asm-generic/int-ll64.h"
  25typedef long long s64;
  26#line 52 "include/asm-generic/int-ll64.h"
  27typedef unsigned long long u64;
  28#line 14 "include/asm-generic/posix_types.h"
  29typedef long __kernel_long_t;
  30#line 15 "include/asm-generic/posix_types.h"
  31typedef unsigned long __kernel_ulong_t;
  32#line 31 "include/asm-generic/posix_types.h"
  33typedef int __kernel_pid_t;
  34#line 52 "include/asm-generic/posix_types.h"
  35typedef unsigned int __kernel_uid32_t;
  36#line 53 "include/asm-generic/posix_types.h"
  37typedef unsigned int __kernel_gid32_t;
  38#line 75 "include/asm-generic/posix_types.h"
  39typedef __kernel_ulong_t __kernel_size_t;
  40#line 76 "include/asm-generic/posix_types.h"
  41typedef __kernel_long_t __kernel_ssize_t;
  42#line 91 "include/asm-generic/posix_types.h"
  43typedef long long __kernel_loff_t;
  44#line 92 "include/asm-generic/posix_types.h"
  45typedef __kernel_long_t __kernel_time_t;
  46#line 93 "include/asm-generic/posix_types.h"
  47typedef __kernel_long_t __kernel_clock_t;
  48#line 94 "include/asm-generic/posix_types.h"
  49typedef int __kernel_timer_t;
  50#line 95 "include/asm-generic/posix_types.h"
  51typedef int __kernel_clockid_t;
  52#line 21 "include/linux/types.h"
  53typedef __u32 __kernel_dev_t;
  54#line 24 "include/linux/types.h"
  55typedef __kernel_dev_t dev_t;
  56#line 27 "include/linux/types.h"
  57typedef unsigned short umode_t;
  58#line 30 "include/linux/types.h"
  59typedef __kernel_pid_t pid_t;
  60#line 35 "include/linux/types.h"
  61typedef __kernel_clockid_t clockid_t;
  62#line 38 "include/linux/types.h"
  63typedef _Bool bool;
  64#line 40 "include/linux/types.h"
  65typedef __kernel_uid32_t uid_t;
  66#line 41 "include/linux/types.h"
  67typedef __kernel_gid32_t gid_t;
  68#line 54 "include/linux/types.h"
  69typedef __kernel_loff_t loff_t;
  70#line 63 "include/linux/types.h"
  71typedef __kernel_size_t size_t;
  72#line 68 "include/linux/types.h"
  73typedef __kernel_ssize_t ssize_t;
  74#line 78 "include/linux/types.h"
  75typedef __kernel_time_t time_t;
  76#line 111 "include/linux/types.h"
  77typedef __s32 int32_t;
  78#line 117 "include/linux/types.h"
  79typedef __u32 uint32_t;
  80#line 202 "include/linux/types.h"
  81typedef unsigned int gfp_t;
  82#line 219 "include/linux/types.h"
  83struct __anonstruct_atomic_t_7 {
  84   int counter ;
  85};
  86#line 219 "include/linux/types.h"
  87typedef struct __anonstruct_atomic_t_7 atomic_t;
  88#line 224 "include/linux/types.h"
  89struct __anonstruct_atomic64_t_8 {
  90   long counter ;
  91};
  92#line 224 "include/linux/types.h"
  93typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  94#line 229 "include/linux/types.h"
  95struct list_head {
  96   struct list_head *next ;
  97   struct list_head *prev ;
  98};
  99#line 233
 100struct hlist_node;
 101#line 233 "include/linux/types.h"
 102struct hlist_head {
 103   struct hlist_node *first ;
 104};
 105#line 237 "include/linux/types.h"
 106struct hlist_node {
 107   struct hlist_node *next ;
 108   struct hlist_node **pprev ;
 109};
 110#line 253 "include/linux/types.h"
 111struct rcu_head {
 112   struct rcu_head *next ;
 113   void (*func)(struct rcu_head *head ) ;
 114};
 115#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 116struct module;
 117#line 56
 118struct module;
 119#line 146 "include/linux/init.h"
 120typedef void (*ctor_fn_t)(void);
 121#line 47 "include/linux/dynamic_debug.h"
 122struct device;
 123#line 47
 124struct device;
 125#line 135 "include/linux/kernel.h"
 126struct completion;
 127#line 135
 128struct completion;
 129#line 136
 130struct pt_regs;
 131#line 136
 132struct pt_regs;
 133#line 349
 134struct pid;
 135#line 349
 136struct pid;
 137#line 12 "include/linux/thread_info.h"
 138struct timespec;
 139#line 12
 140struct timespec;
 141#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
 142struct page;
 143#line 18
 144struct page;
 145#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
 146struct task_struct;
 147#line 20
 148struct task_struct;
 149#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 150struct task_struct;
 151#line 8
 152struct mm_struct;
 153#line 8
 154struct mm_struct;
 155#line 99 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 156struct pt_regs {
 157   unsigned long r15 ;
 158   unsigned long r14 ;
 159   unsigned long r13 ;
 160   unsigned long r12 ;
 161   unsigned long bp ;
 162   unsigned long bx ;
 163   unsigned long r11 ;
 164   unsigned long r10 ;
 165   unsigned long r9 ;
 166   unsigned long r8 ;
 167   unsigned long ax ;
 168   unsigned long cx ;
 169   unsigned long dx ;
 170   unsigned long si ;
 171   unsigned long di ;
 172   unsigned long orig_ax ;
 173   unsigned long ip ;
 174   unsigned long cs ;
 175   unsigned long flags ;
 176   unsigned long sp ;
 177   unsigned long ss ;
 178};
 179#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 180struct __anonstruct____missing_field_name_15 {
 181   unsigned int a ;
 182   unsigned int b ;
 183};
 184#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 185struct __anonstruct____missing_field_name_16 {
 186   u16 limit0 ;
 187   u16 base0 ;
 188   unsigned int base1 : 8 ;
 189   unsigned int type : 4 ;
 190   unsigned int s : 1 ;
 191   unsigned int dpl : 2 ;
 192   unsigned int p : 1 ;
 193   unsigned int limit : 4 ;
 194   unsigned int avl : 1 ;
 195   unsigned int l : 1 ;
 196   unsigned int d : 1 ;
 197   unsigned int g : 1 ;
 198   unsigned int base2 : 8 ;
 199};
 200#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 201union __anonunion____missing_field_name_14 {
 202   struct __anonstruct____missing_field_name_15 __annonCompField5 ;
 203   struct __anonstruct____missing_field_name_16 __annonCompField6 ;
 204};
 205#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 206struct desc_struct {
 207   union __anonunion____missing_field_name_14 __annonCompField7 ;
 208} __attribute__((__packed__)) ;
 209#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 210typedef unsigned long pgdval_t;
 211#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 212typedef unsigned long pgprotval_t;
 213#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 214struct pgprot {
 215   pgprotval_t pgprot ;
 216};
 217#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 218typedef struct pgprot pgprot_t;
 219#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 220struct __anonstruct_pgd_t_20 {
 221   pgdval_t pgd ;
 222};
 223#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 224typedef struct __anonstruct_pgd_t_20 pgd_t;
 225#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 226typedef struct page *pgtable_t;
 227#line 295
 228struct file;
 229#line 295
 230struct file;
 231#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 232struct page;
 233#line 47
 234struct thread_struct;
 235#line 47
 236struct thread_struct;
 237#line 50
 238struct mm_struct;
 239#line 51
 240struct desc_struct;
 241#line 52
 242struct task_struct;
 243#line 53
 244struct cpumask;
 245#line 53
 246struct cpumask;
 247#line 329
 248struct arch_spinlock;
 249#line 329
 250struct arch_spinlock;
 251#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 252struct task_struct;
 253#line 141 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
 254struct kernel_vm86_regs {
 255   struct pt_regs pt ;
 256   unsigned short es ;
 257   unsigned short __esh ;
 258   unsigned short ds ;
 259   unsigned short __dsh ;
 260   unsigned short fs ;
 261   unsigned short __fsh ;
 262   unsigned short gs ;
 263   unsigned short __gsh ;
 264};
 265#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 266union __anonunion____missing_field_name_24 {
 267   struct pt_regs *regs ;
 268   struct kernel_vm86_regs *vm86 ;
 269};
 270#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 271struct math_emu_info {
 272   long ___orig_eip ;
 273   union __anonunion____missing_field_name_24 __annonCompField8 ;
 274};
 275#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 276struct task_struct;
 277#line 10 "include/asm-generic/bug.h"
 278struct bug_entry {
 279   int bug_addr_disp ;
 280   int file_disp ;
 281   unsigned short line ;
 282   unsigned short flags ;
 283};
 284#line 12 "include/linux/bug.h"
 285struct pt_regs;
 286#line 14 "include/linux/cpumask.h"
 287struct cpumask {
 288   unsigned long bits[((4096UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 289};
 290#line 14 "include/linux/cpumask.h"
 291typedef struct cpumask cpumask_t;
 292#line 637 "include/linux/cpumask.h"
 293typedef struct cpumask *cpumask_var_t;
 294#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 295struct static_key;
 296#line 234
 297struct static_key;
 298#line 11 "include/linux/personality.h"
 299struct pt_regs;
 300#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 301struct i387_fsave_struct {
 302   u32 cwd ;
 303   u32 swd ;
 304   u32 twd ;
 305   u32 fip ;
 306   u32 fcs ;
 307   u32 foo ;
 308   u32 fos ;
 309   u32 st_space[20] ;
 310   u32 status ;
 311};
 312#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 313struct __anonstruct____missing_field_name_31 {
 314   u64 rip ;
 315   u64 rdp ;
 316};
 317#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 318struct __anonstruct____missing_field_name_32 {
 319   u32 fip ;
 320   u32 fcs ;
 321   u32 foo ;
 322   u32 fos ;
 323};
 324#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 325union __anonunion____missing_field_name_30 {
 326   struct __anonstruct____missing_field_name_31 __annonCompField12 ;
 327   struct __anonstruct____missing_field_name_32 __annonCompField13 ;
 328};
 329#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 330union __anonunion____missing_field_name_33 {
 331   u32 padding1[12] ;
 332   u32 sw_reserved[12] ;
 333};
 334#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 335struct i387_fxsave_struct {
 336   u16 cwd ;
 337   u16 swd ;
 338   u16 twd ;
 339   u16 fop ;
 340   union __anonunion____missing_field_name_30 __annonCompField14 ;
 341   u32 mxcsr ;
 342   u32 mxcsr_mask ;
 343   u32 st_space[32] ;
 344   u32 xmm_space[64] ;
 345   u32 padding[12] ;
 346   union __anonunion____missing_field_name_33 __annonCompField15 ;
 347} __attribute__((__aligned__(16))) ;
 348#line 341 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 349struct i387_soft_struct {
 350   u32 cwd ;
 351   u32 swd ;
 352   u32 twd ;
 353   u32 fip ;
 354   u32 fcs ;
 355   u32 foo ;
 356   u32 fos ;
 357   u32 st_space[20] ;
 358   u8 ftop ;
 359   u8 changed ;
 360   u8 lookahead ;
 361   u8 no_update ;
 362   u8 rm ;
 363   u8 alimit ;
 364   struct math_emu_info *info ;
 365   u32 entry_eip ;
 366};
 367#line 361 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 368struct ymmh_struct {
 369   u32 ymmh_space[64] ;
 370};
 371#line 366 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 372struct xsave_hdr_struct {
 373   u64 xstate_bv ;
 374   u64 reserved1[2] ;
 375   u64 reserved2[5] ;
 376} __attribute__((__packed__)) ;
 377#line 372 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 378struct xsave_struct {
 379   struct i387_fxsave_struct i387 ;
 380   struct xsave_hdr_struct xsave_hdr ;
 381   struct ymmh_struct ymmh ;
 382} __attribute__((__packed__, __aligned__(64))) ;
 383#line 379 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 384union thread_xstate {
 385   struct i387_fsave_struct fsave ;
 386   struct i387_fxsave_struct fxsave ;
 387   struct i387_soft_struct soft ;
 388   struct xsave_struct xsave ;
 389};
 390#line 386 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 391struct fpu {
 392   unsigned int last_cpu ;
 393   unsigned int has_fpu ;
 394   union thread_xstate *state ;
 395};
 396#line 433
 397struct kmem_cache;
 398#line 435
 399struct perf_event;
 400#line 435
 401struct perf_event;
 402#line 437 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 403struct thread_struct {
 404   struct desc_struct tls_array[3] ;
 405   unsigned long sp0 ;
 406   unsigned long sp ;
 407   unsigned long usersp ;
 408   unsigned short es ;
 409   unsigned short ds ;
 410   unsigned short fsindex ;
 411   unsigned short gsindex ;
 412   unsigned long fs ;
 413   unsigned long gs ;
 414   struct perf_event *ptrace_bps[4] ;
 415   unsigned long debugreg6 ;
 416   unsigned long ptrace_dr7 ;
 417   unsigned long cr2 ;
 418   unsigned long trap_nr ;
 419   unsigned long error_code ;
 420   struct fpu fpu ;
 421   unsigned long *io_bitmap_ptr ;
 422   unsigned long iopl ;
 423   unsigned int io_bitmap_max ;
 424};
 425#line 23 "include/asm-generic/atomic-long.h"
 426typedef atomic64_t atomic_long_t;
 427#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 428typedef u16 __ticket_t;
 429#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 430typedef u32 __ticketpair_t;
 431#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 432struct __raw_tickets {
 433   __ticket_t head ;
 434   __ticket_t tail ;
 435};
 436#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 437union __anonunion____missing_field_name_36 {
 438   __ticketpair_t head_tail ;
 439   struct __raw_tickets tickets ;
 440};
 441#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 442struct arch_spinlock {
 443   union __anonunion____missing_field_name_36 __annonCompField17 ;
 444};
 445#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 446typedef struct arch_spinlock arch_spinlock_t;
 447#line 12 "include/linux/lockdep.h"
 448struct task_struct;
 449#line 20 "include/linux/spinlock_types.h"
 450struct raw_spinlock {
 451   arch_spinlock_t raw_lock ;
 452   unsigned int magic ;
 453   unsigned int owner_cpu ;
 454   void *owner ;
 455};
 456#line 20 "include/linux/spinlock_types.h"
 457typedef struct raw_spinlock raw_spinlock_t;
 458#line 64 "include/linux/spinlock_types.h"
 459union __anonunion____missing_field_name_39 {
 460   struct raw_spinlock rlock ;
 461};
 462#line 64 "include/linux/spinlock_types.h"
 463struct spinlock {
 464   union __anonunion____missing_field_name_39 __annonCompField19 ;
 465};
 466#line 64 "include/linux/spinlock_types.h"
 467typedef struct spinlock spinlock_t;
 468#line 119 "include/linux/seqlock.h"
 469struct seqcount {
 470   unsigned int sequence ;
 471};
 472#line 119 "include/linux/seqlock.h"
 473typedef struct seqcount seqcount_t;
 474#line 14 "include/linux/time.h"
 475struct timespec {
 476   __kernel_time_t tv_sec ;
 477   long tv_nsec ;
 478};
 479#line 49 "include/linux/wait.h"
 480struct __wait_queue_head {
 481   spinlock_t lock ;
 482   struct list_head task_list ;
 483};
 484#line 53 "include/linux/wait.h"
 485typedef struct __wait_queue_head wait_queue_head_t;
 486#line 55
 487struct task_struct;
 488#line 98 "include/linux/nodemask.h"
 489struct __anonstruct_nodemask_t_42 {
 490   unsigned long bits[(((unsigned long )(1 << 10) + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 491};
 492#line 98 "include/linux/nodemask.h"
 493typedef struct __anonstruct_nodemask_t_42 nodemask_t;
 494#line 60 "include/linux/pageblock-flags.h"
 495struct page;
 496#line 48 "include/linux/mutex.h"
 497struct mutex {
 498   atomic_t count ;
 499   spinlock_t wait_lock ;
 500   struct list_head wait_list ;
 501   struct task_struct *owner ;
 502   char const   *name ;
 503   void *magic ;
 504};
 505#line 69 "include/linux/mutex.h"
 506struct mutex_waiter {
 507   struct list_head list ;
 508   struct task_struct *task ;
 509   void *magic ;
 510};
 511#line 19 "include/linux/rwsem.h"
 512struct rw_semaphore;
 513#line 19
 514struct rw_semaphore;
 515#line 25 "include/linux/rwsem.h"
 516struct rw_semaphore {
 517   long count ;
 518   raw_spinlock_t wait_lock ;
 519   struct list_head wait_list ;
 520};
 521#line 25 "include/linux/completion.h"
 522struct completion {
 523   unsigned int done ;
 524   wait_queue_head_t wait ;
 525};
 526#line 9 "include/linux/memory_hotplug.h"
 527struct page;
 528#line 202 "include/linux/ioport.h"
 529struct device;
 530#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 531struct device;
 532#line 46 "include/linux/ktime.h"
 533union ktime {
 534   s64 tv64 ;
 535};
 536#line 59 "include/linux/ktime.h"
 537typedef union ktime ktime_t;
 538#line 10 "include/linux/timer.h"
 539struct tvec_base;
 540#line 10
 541struct tvec_base;
 542#line 12 "include/linux/timer.h"
 543struct timer_list {
 544   struct list_head entry ;
 545   unsigned long expires ;
 546   struct tvec_base *base ;
 547   void (*function)(unsigned long  ) ;
 548   unsigned long data ;
 549   int slack ;
 550   int start_pid ;
 551   void *start_site ;
 552   char start_comm[16] ;
 553};
 554#line 289
 555struct hrtimer;
 556#line 289
 557struct hrtimer;
 558#line 290
 559enum hrtimer_restart;
 560#line 17 "include/linux/workqueue.h"
 561struct work_struct;
 562#line 17
 563struct work_struct;
 564#line 79 "include/linux/workqueue.h"
 565struct work_struct {
 566   atomic_long_t data ;
 567   struct list_head entry ;
 568   void (*func)(struct work_struct *work ) ;
 569};
 570#line 42 "include/linux/pm.h"
 571struct device;
 572#line 50 "include/linux/pm.h"
 573struct pm_message {
 574   int event ;
 575};
 576#line 50 "include/linux/pm.h"
 577typedef struct pm_message pm_message_t;
 578#line 264 "include/linux/pm.h"
 579struct dev_pm_ops {
 580   int (*prepare)(struct device *dev ) ;
 581   void (*complete)(struct device *dev ) ;
 582   int (*suspend)(struct device *dev ) ;
 583   int (*resume)(struct device *dev ) ;
 584   int (*freeze)(struct device *dev ) ;
 585   int (*thaw)(struct device *dev ) ;
 586   int (*poweroff)(struct device *dev ) ;
 587   int (*restore)(struct device *dev ) ;
 588   int (*suspend_late)(struct device *dev ) ;
 589   int (*resume_early)(struct device *dev ) ;
 590   int (*freeze_late)(struct device *dev ) ;
 591   int (*thaw_early)(struct device *dev ) ;
 592   int (*poweroff_late)(struct device *dev ) ;
 593   int (*restore_early)(struct device *dev ) ;
 594   int (*suspend_noirq)(struct device *dev ) ;
 595   int (*resume_noirq)(struct device *dev ) ;
 596   int (*freeze_noirq)(struct device *dev ) ;
 597   int (*thaw_noirq)(struct device *dev ) ;
 598   int (*poweroff_noirq)(struct device *dev ) ;
 599   int (*restore_noirq)(struct device *dev ) ;
 600   int (*runtime_suspend)(struct device *dev ) ;
 601   int (*runtime_resume)(struct device *dev ) ;
 602   int (*runtime_idle)(struct device *dev ) ;
 603};
 604#line 458
 605enum rpm_status {
 606    RPM_ACTIVE = 0,
 607    RPM_RESUMING = 1,
 608    RPM_SUSPENDED = 2,
 609    RPM_SUSPENDING = 3
 610} ;
 611#line 480
 612enum rpm_request {
 613    RPM_REQ_NONE = 0,
 614    RPM_REQ_IDLE = 1,
 615    RPM_REQ_SUSPEND = 2,
 616    RPM_REQ_AUTOSUSPEND = 3,
 617    RPM_REQ_RESUME = 4
 618} ;
 619#line 488
 620struct wakeup_source;
 621#line 488
 622struct wakeup_source;
 623#line 495 "include/linux/pm.h"
 624struct pm_subsys_data {
 625   spinlock_t lock ;
 626   unsigned int refcount ;
 627};
 628#line 506
 629struct dev_pm_qos_request;
 630#line 506
 631struct pm_qos_constraints;
 632#line 506 "include/linux/pm.h"
 633struct dev_pm_info {
 634   pm_message_t power_state ;
 635   unsigned int can_wakeup : 1 ;
 636   unsigned int async_suspend : 1 ;
 637   bool is_prepared : 1 ;
 638   bool is_suspended : 1 ;
 639   bool ignore_children : 1 ;
 640   spinlock_t lock ;
 641   struct list_head entry ;
 642   struct completion completion ;
 643   struct wakeup_source *wakeup ;
 644   bool wakeup_path : 1 ;
 645   struct timer_list suspend_timer ;
 646   unsigned long timer_expires ;
 647   struct work_struct work ;
 648   wait_queue_head_t wait_queue ;
 649   atomic_t usage_count ;
 650   atomic_t child_count ;
 651   unsigned int disable_depth : 3 ;
 652   unsigned int idle_notification : 1 ;
 653   unsigned int request_pending : 1 ;
 654   unsigned int deferred_resume : 1 ;
 655   unsigned int run_wake : 1 ;
 656   unsigned int runtime_auto : 1 ;
 657   unsigned int no_callbacks : 1 ;
 658   unsigned int irq_safe : 1 ;
 659   unsigned int use_autosuspend : 1 ;
 660   unsigned int timer_autosuspends : 1 ;
 661   enum rpm_request request ;
 662   enum rpm_status runtime_status ;
 663   int runtime_error ;
 664   int autosuspend_delay ;
 665   unsigned long last_busy ;
 666   unsigned long active_jiffies ;
 667   unsigned long suspended_jiffies ;
 668   unsigned long accounting_timestamp ;
 669   ktime_t suspend_time ;
 670   s64 max_time_suspended_ns ;
 671   struct dev_pm_qos_request *pq_req ;
 672   struct pm_subsys_data *subsys_data ;
 673   struct pm_qos_constraints *constraints ;
 674};
 675#line 564 "include/linux/pm.h"
 676struct dev_pm_domain {
 677   struct dev_pm_ops ops ;
 678};
 679#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 680struct __anonstruct_mm_context_t_112 {
 681   void *ldt ;
 682   int size ;
 683   unsigned short ia32_compat ;
 684   struct mutex lock ;
 685   void *vdso ;
 686};
 687#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 688typedef struct __anonstruct_mm_context_t_112 mm_context_t;
 689#line 8 "include/linux/vmalloc.h"
 690struct vm_area_struct;
 691#line 8
 692struct vm_area_struct;
 693#line 994 "include/linux/mmzone.h"
 694struct page;
 695#line 10 "include/linux/gfp.h"
 696struct vm_area_struct;
 697#line 29 "include/linux/sysctl.h"
 698struct completion;
 699#line 100 "include/linux/rbtree.h"
 700struct rb_node {
 701   unsigned long rb_parent_color ;
 702   struct rb_node *rb_right ;
 703   struct rb_node *rb_left ;
 704} __attribute__((__aligned__(sizeof(long )))) ;
 705#line 110 "include/linux/rbtree.h"
 706struct rb_root {
 707   struct rb_node *rb_node ;
 708};
 709#line 939 "include/linux/sysctl.h"
 710struct nsproxy;
 711#line 939
 712struct nsproxy;
 713#line 48 "include/linux/kmod.h"
 714struct cred;
 715#line 48
 716struct cred;
 717#line 49
 718struct file;
 719#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 720struct task_struct;
 721#line 18 "include/linux/elf.h"
 722typedef __u64 Elf64_Addr;
 723#line 19 "include/linux/elf.h"
 724typedef __u16 Elf64_Half;
 725#line 23 "include/linux/elf.h"
 726typedef __u32 Elf64_Word;
 727#line 24 "include/linux/elf.h"
 728typedef __u64 Elf64_Xword;
 729#line 194 "include/linux/elf.h"
 730struct elf64_sym {
 731   Elf64_Word st_name ;
 732   unsigned char st_info ;
 733   unsigned char st_other ;
 734   Elf64_Half st_shndx ;
 735   Elf64_Addr st_value ;
 736   Elf64_Xword st_size ;
 737};
 738#line 194 "include/linux/elf.h"
 739typedef struct elf64_sym Elf64_Sym;
 740#line 438
 741struct file;
 742#line 20 "include/linux/kobject_ns.h"
 743struct sock;
 744#line 20
 745struct sock;
 746#line 21
 747struct kobject;
 748#line 21
 749struct kobject;
 750#line 27
 751enum kobj_ns_type {
 752    KOBJ_NS_TYPE_NONE = 0,
 753    KOBJ_NS_TYPE_NET = 1,
 754    KOBJ_NS_TYPES = 2
 755} ;
 756#line 40 "include/linux/kobject_ns.h"
 757struct kobj_ns_type_operations {
 758   enum kobj_ns_type type ;
 759   void *(*grab_current_ns)(void) ;
 760   void const   *(*netlink_ns)(struct sock *sk ) ;
 761   void const   *(*initial_ns)(void) ;
 762   void (*drop_ns)(void * ) ;
 763};
 764#line 22 "include/linux/sysfs.h"
 765struct kobject;
 766#line 23
 767struct module;
 768#line 24
 769enum kobj_ns_type;
 770#line 26 "include/linux/sysfs.h"
 771struct attribute {
 772   char const   *name ;
 773   umode_t mode ;
 774};
 775#line 56 "include/linux/sysfs.h"
 776struct attribute_group {
 777   char const   *name ;
 778   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 779   struct attribute **attrs ;
 780};
 781#line 85
 782struct file;
 783#line 86
 784struct vm_area_struct;
 785#line 88 "include/linux/sysfs.h"
 786struct bin_attribute {
 787   struct attribute attr ;
 788   size_t size ;
 789   void *private ;
 790   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 791                   loff_t  , size_t  ) ;
 792   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 793                    loff_t  , size_t  ) ;
 794   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 795};
 796#line 112 "include/linux/sysfs.h"
 797struct sysfs_ops {
 798   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 799   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 800   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 801};
 802#line 118
 803struct sysfs_dirent;
 804#line 118
 805struct sysfs_dirent;
 806#line 22 "include/linux/kref.h"
 807struct kref {
 808   atomic_t refcount ;
 809};
 810#line 60 "include/linux/kobject.h"
 811struct kset;
 812#line 60
 813struct kobj_type;
 814#line 60 "include/linux/kobject.h"
 815struct kobject {
 816   char const   *name ;
 817   struct list_head entry ;
 818   struct kobject *parent ;
 819   struct kset *kset ;
 820   struct kobj_type *ktype ;
 821   struct sysfs_dirent *sd ;
 822   struct kref kref ;
 823   unsigned int state_initialized : 1 ;
 824   unsigned int state_in_sysfs : 1 ;
 825   unsigned int state_add_uevent_sent : 1 ;
 826   unsigned int state_remove_uevent_sent : 1 ;
 827   unsigned int uevent_suppress : 1 ;
 828};
 829#line 108 "include/linux/kobject.h"
 830struct kobj_type {
 831   void (*release)(struct kobject *kobj ) ;
 832   struct sysfs_ops  const  *sysfs_ops ;
 833   struct attribute **default_attrs ;
 834   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 835   void const   *(*namespace)(struct kobject *kobj ) ;
 836};
 837#line 116 "include/linux/kobject.h"
 838struct kobj_uevent_env {
 839   char *envp[32] ;
 840   int envp_idx ;
 841   char buf[2048] ;
 842   int buflen ;
 843};
 844#line 123 "include/linux/kobject.h"
 845struct kset_uevent_ops {
 846   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 847   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 848   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 849};
 850#line 140
 851struct sock;
 852#line 159 "include/linux/kobject.h"
 853struct kset {
 854   struct list_head list ;
 855   spinlock_t list_lock ;
 856   struct kobject kobj ;
 857   struct kset_uevent_ops  const  *uevent_ops ;
 858};
 859#line 39 "include/linux/moduleparam.h"
 860struct kernel_param;
 861#line 39
 862struct kernel_param;
 863#line 41 "include/linux/moduleparam.h"
 864struct kernel_param_ops {
 865   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
 866   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
 867   void (*free)(void *arg ) ;
 868};
 869#line 50
 870struct kparam_string;
 871#line 50
 872struct kparam_array;
 873#line 50 "include/linux/moduleparam.h"
 874union __anonunion____missing_field_name_199 {
 875   void *arg ;
 876   struct kparam_string  const  *str ;
 877   struct kparam_array  const  *arr ;
 878};
 879#line 50 "include/linux/moduleparam.h"
 880struct kernel_param {
 881   char const   *name ;
 882   struct kernel_param_ops  const  *ops ;
 883   u16 perm ;
 884   s16 level ;
 885   union __anonunion____missing_field_name_199 __annonCompField32 ;
 886};
 887#line 63 "include/linux/moduleparam.h"
 888struct kparam_string {
 889   unsigned int maxlen ;
 890   char *string ;
 891};
 892#line 69 "include/linux/moduleparam.h"
 893struct kparam_array {
 894   unsigned int max ;
 895   unsigned int elemsize ;
 896   unsigned int *num ;
 897   struct kernel_param_ops  const  *ops ;
 898   void *elem ;
 899};
 900#line 445
 901struct module;
 902#line 80 "include/linux/jump_label.h"
 903struct module;
 904#line 143 "include/linux/jump_label.h"
 905struct static_key {
 906   atomic_t enabled ;
 907};
 908#line 22 "include/linux/tracepoint.h"
 909struct module;
 910#line 23
 911struct tracepoint;
 912#line 23
 913struct tracepoint;
 914#line 25 "include/linux/tracepoint.h"
 915struct tracepoint_func {
 916   void *func ;
 917   void *data ;
 918};
 919#line 30 "include/linux/tracepoint.h"
 920struct tracepoint {
 921   char const   *name ;
 922   struct static_key key ;
 923   void (*regfunc)(void) ;
 924   void (*unregfunc)(void) ;
 925   struct tracepoint_func *funcs ;
 926};
 927#line 19 "include/linux/export.h"
 928struct kernel_symbol {
 929   unsigned long value ;
 930   char const   *name ;
 931};
 932#line 8 "include/asm-generic/module.h"
 933struct mod_arch_specific {
 934
 935};
 936#line 35 "include/linux/module.h"
 937struct module;
 938#line 37
 939struct module_param_attrs;
 940#line 37 "include/linux/module.h"
 941struct module_kobject {
 942   struct kobject kobj ;
 943   struct module *mod ;
 944   struct kobject *drivers_dir ;
 945   struct module_param_attrs *mp ;
 946};
 947#line 44 "include/linux/module.h"
 948struct module_attribute {
 949   struct attribute attr ;
 950   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 951   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 952                    size_t count ) ;
 953   void (*setup)(struct module * , char const   * ) ;
 954   int (*test)(struct module * ) ;
 955   void (*free)(struct module * ) ;
 956};
 957#line 71
 958struct exception_table_entry;
 959#line 71
 960struct exception_table_entry;
 961#line 199
 962enum module_state {
 963    MODULE_STATE_LIVE = 0,
 964    MODULE_STATE_COMING = 1,
 965    MODULE_STATE_GOING = 2
 966} ;
 967#line 215 "include/linux/module.h"
 968struct module_ref {
 969   unsigned long incs ;
 970   unsigned long decs ;
 971} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 972#line 220
 973struct module_sect_attrs;
 974#line 220
 975struct module_notes_attrs;
 976#line 220
 977struct ftrace_event_call;
 978#line 220 "include/linux/module.h"
 979struct module {
 980   enum module_state state ;
 981   struct list_head list ;
 982   char name[64UL - sizeof(unsigned long )] ;
 983   struct module_kobject mkobj ;
 984   struct module_attribute *modinfo_attrs ;
 985   char const   *version ;
 986   char const   *srcversion ;
 987   struct kobject *holders_dir ;
 988   struct kernel_symbol  const  *syms ;
 989   unsigned long const   *crcs ;
 990   unsigned int num_syms ;
 991   struct kernel_param *kp ;
 992   unsigned int num_kp ;
 993   unsigned int num_gpl_syms ;
 994   struct kernel_symbol  const  *gpl_syms ;
 995   unsigned long const   *gpl_crcs ;
 996   struct kernel_symbol  const  *unused_syms ;
 997   unsigned long const   *unused_crcs ;
 998   unsigned int num_unused_syms ;
 999   unsigned int num_unused_gpl_syms ;
1000   struct kernel_symbol  const  *unused_gpl_syms ;
1001   unsigned long const   *unused_gpl_crcs ;
1002   struct kernel_symbol  const  *gpl_future_syms ;
1003   unsigned long const   *gpl_future_crcs ;
1004   unsigned int num_gpl_future_syms ;
1005   unsigned int num_exentries ;
1006   struct exception_table_entry *extable ;
1007   int (*init)(void) ;
1008   void *module_init ;
1009   void *module_core ;
1010   unsigned int init_size ;
1011   unsigned int core_size ;
1012   unsigned int init_text_size ;
1013   unsigned int core_text_size ;
1014   unsigned int init_ro_size ;
1015   unsigned int core_ro_size ;
1016   struct mod_arch_specific arch ;
1017   unsigned int taints ;
1018   unsigned int num_bugs ;
1019   struct list_head bug_list ;
1020   struct bug_entry *bug_table ;
1021   Elf64_Sym *symtab ;
1022   Elf64_Sym *core_symtab ;
1023   unsigned int num_symtab ;
1024   unsigned int core_num_syms ;
1025   char *strtab ;
1026   char *core_strtab ;
1027   struct module_sect_attrs *sect_attrs ;
1028   struct module_notes_attrs *notes_attrs ;
1029   char *args ;
1030   void *percpu ;
1031   unsigned int percpu_size ;
1032   unsigned int num_tracepoints ;
1033   struct tracepoint * const  *tracepoints_ptrs ;
1034   unsigned int num_trace_bprintk_fmt ;
1035   char const   **trace_bprintk_fmt_start ;
1036   struct ftrace_event_call **trace_events ;
1037   unsigned int num_trace_events ;
1038   struct list_head source_list ;
1039   struct list_head target_list ;
1040   struct task_struct *waiter ;
1041   void (*exit)(void) ;
1042   struct module_ref *refptr ;
1043   ctor_fn_t *ctors ;
1044   unsigned int num_ctors ;
1045};
1046#line 46 "include/linux/slub_def.h"
1047struct kmem_cache_cpu {
1048   void **freelist ;
1049   unsigned long tid ;
1050   struct page *page ;
1051   struct page *partial ;
1052   int node ;
1053   unsigned int stat[26] ;
1054};
1055#line 57 "include/linux/slub_def.h"
1056struct kmem_cache_node {
1057   spinlock_t list_lock ;
1058   unsigned long nr_partial ;
1059   struct list_head partial ;
1060   atomic_long_t nr_slabs ;
1061   atomic_long_t total_objects ;
1062   struct list_head full ;
1063};
1064#line 73 "include/linux/slub_def.h"
1065struct kmem_cache_order_objects {
1066   unsigned long x ;
1067};
1068#line 80 "include/linux/slub_def.h"
1069struct kmem_cache {
1070   struct kmem_cache_cpu *cpu_slab ;
1071   unsigned long flags ;
1072   unsigned long min_partial ;
1073   int size ;
1074   int objsize ;
1075   int offset ;
1076   int cpu_partial ;
1077   struct kmem_cache_order_objects oo ;
1078   struct kmem_cache_order_objects max ;
1079   struct kmem_cache_order_objects min ;
1080   gfp_t allocflags ;
1081   int refcount ;
1082   void (*ctor)(void * ) ;
1083   int inuse ;
1084   int align ;
1085   int reserved ;
1086   char const   *name ;
1087   struct list_head list ;
1088   struct kobject kobj ;
1089   int remote_node_defrag_ratio ;
1090   struct kmem_cache_node *node[1 << 10] ;
1091};
1092#line 12 "include/linux/mod_devicetable.h"
1093typedef unsigned long kernel_ulong_t;
1094#line 219 "include/linux/mod_devicetable.h"
1095struct of_device_id {
1096   char name[32] ;
1097   char type[32] ;
1098   char compatible[128] ;
1099   void *data ;
1100};
1101#line 431 "include/linux/mod_devicetable.h"
1102struct i2c_device_id {
1103   char name[20] ;
1104   kernel_ulong_t driver_data  __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
1105};
1106#line 19 "include/linux/klist.h"
1107struct klist_node;
1108#line 19
1109struct klist_node;
1110#line 39 "include/linux/klist.h"
1111struct klist_node {
1112   void *n_klist ;
1113   struct list_head n_node ;
1114   struct kref n_ref ;
1115};
1116#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1117struct dma_map_ops;
1118#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1119struct dev_archdata {
1120   void *acpi_handle ;
1121   struct dma_map_ops *dma_ops ;
1122   void *iommu ;
1123};
1124#line 28 "include/linux/device.h"
1125struct device;
1126#line 29
1127struct device_private;
1128#line 29
1129struct device_private;
1130#line 30
1131struct device_driver;
1132#line 30
1133struct device_driver;
1134#line 31
1135struct driver_private;
1136#line 31
1137struct driver_private;
1138#line 32
1139struct module;
1140#line 33
1141struct class;
1142#line 33
1143struct class;
1144#line 34
1145struct subsys_private;
1146#line 34
1147struct subsys_private;
1148#line 35
1149struct bus_type;
1150#line 35
1151struct bus_type;
1152#line 36
1153struct device_node;
1154#line 36
1155struct device_node;
1156#line 37
1157struct iommu_ops;
1158#line 37
1159struct iommu_ops;
1160#line 39 "include/linux/device.h"
1161struct bus_attribute {
1162   struct attribute attr ;
1163   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
1164   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
1165};
1166#line 89
1167struct device_attribute;
1168#line 89
1169struct driver_attribute;
1170#line 89 "include/linux/device.h"
1171struct bus_type {
1172   char const   *name ;
1173   char const   *dev_name ;
1174   struct device *dev_root ;
1175   struct bus_attribute *bus_attrs ;
1176   struct device_attribute *dev_attrs ;
1177   struct driver_attribute *drv_attrs ;
1178   int (*match)(struct device *dev , struct device_driver *drv ) ;
1179   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1180   int (*probe)(struct device *dev ) ;
1181   int (*remove)(struct device *dev ) ;
1182   void (*shutdown)(struct device *dev ) ;
1183   int (*suspend)(struct device *dev , pm_message_t state ) ;
1184   int (*resume)(struct device *dev ) ;
1185   struct dev_pm_ops  const  *pm ;
1186   struct iommu_ops *iommu_ops ;
1187   struct subsys_private *p ;
1188};
1189#line 127
1190struct device_type;
1191#line 214 "include/linux/device.h"
1192struct device_driver {
1193   char const   *name ;
1194   struct bus_type *bus ;
1195   struct module *owner ;
1196   char const   *mod_name ;
1197   bool suppress_bind_attrs ;
1198   struct of_device_id  const  *of_match_table ;
1199   int (*probe)(struct device *dev ) ;
1200   int (*remove)(struct device *dev ) ;
1201   void (*shutdown)(struct device *dev ) ;
1202   int (*suspend)(struct device *dev , pm_message_t state ) ;
1203   int (*resume)(struct device *dev ) ;
1204   struct attribute_group  const  **groups ;
1205   struct dev_pm_ops  const  *pm ;
1206   struct driver_private *p ;
1207};
1208#line 249 "include/linux/device.h"
1209struct driver_attribute {
1210   struct attribute attr ;
1211   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
1212   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
1213};
1214#line 330
1215struct class_attribute;
1216#line 330 "include/linux/device.h"
1217struct class {
1218   char const   *name ;
1219   struct module *owner ;
1220   struct class_attribute *class_attrs ;
1221   struct device_attribute *dev_attrs ;
1222   struct bin_attribute *dev_bin_attrs ;
1223   struct kobject *dev_kobj ;
1224   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1225   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1226   void (*class_release)(struct class *class ) ;
1227   void (*dev_release)(struct device *dev ) ;
1228   int (*suspend)(struct device *dev , pm_message_t state ) ;
1229   int (*resume)(struct device *dev ) ;
1230   struct kobj_ns_type_operations  const  *ns_type ;
1231   void const   *(*namespace)(struct device *dev ) ;
1232   struct dev_pm_ops  const  *pm ;
1233   struct subsys_private *p ;
1234};
1235#line 397 "include/linux/device.h"
1236struct class_attribute {
1237   struct attribute attr ;
1238   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
1239   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
1240                    size_t count ) ;
1241   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
1242};
1243#line 465 "include/linux/device.h"
1244struct device_type {
1245   char const   *name ;
1246   struct attribute_group  const  **groups ;
1247   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1248   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1249   void (*release)(struct device *dev ) ;
1250   struct dev_pm_ops  const  *pm ;
1251};
1252#line 476 "include/linux/device.h"
1253struct device_attribute {
1254   struct attribute attr ;
1255   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
1256   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
1257                    size_t count ) ;
1258};
1259#line 559 "include/linux/device.h"
1260struct device_dma_parameters {
1261   unsigned int max_segment_size ;
1262   unsigned long segment_boundary_mask ;
1263};
1264#line 627
1265struct dma_coherent_mem;
1266#line 627 "include/linux/device.h"
1267struct device {
1268   struct device *parent ;
1269   struct device_private *p ;
1270   struct kobject kobj ;
1271   char const   *init_name ;
1272   struct device_type  const  *type ;
1273   struct mutex mutex ;
1274   struct bus_type *bus ;
1275   struct device_driver *driver ;
1276   void *platform_data ;
1277   struct dev_pm_info power ;
1278   struct dev_pm_domain *pm_domain ;
1279   int numa_node ;
1280   u64 *dma_mask ;
1281   u64 coherent_dma_mask ;
1282   struct device_dma_parameters *dma_parms ;
1283   struct list_head dma_pools ;
1284   struct dma_coherent_mem *dma_mem ;
1285   struct dev_archdata archdata ;
1286   struct device_node *of_node ;
1287   dev_t devt ;
1288   u32 id ;
1289   spinlock_t devres_lock ;
1290   struct list_head devres_head ;
1291   struct klist_node knode_class ;
1292   struct class *class ;
1293   struct attribute_group  const  **groups ;
1294   void (*release)(struct device *dev ) ;
1295};
1296#line 43 "include/linux/pm_wakeup.h"
1297struct wakeup_source {
1298   char const   *name ;
1299   struct list_head entry ;
1300   spinlock_t lock ;
1301   struct timer_list timer ;
1302   unsigned long timer_expires ;
1303   ktime_t total_time ;
1304   ktime_t max_time ;
1305   ktime_t last_time ;
1306   unsigned long event_count ;
1307   unsigned long active_count ;
1308   unsigned long relax_count ;
1309   unsigned long hit_count ;
1310   unsigned int active : 1 ;
1311};
1312#line 18 "include/linux/capability.h"
1313struct task_struct;
1314#line 94 "include/linux/capability.h"
1315struct kernel_cap_struct {
1316   __u32 cap[2] ;
1317};
1318#line 94 "include/linux/capability.h"
1319typedef struct kernel_cap_struct kernel_cap_t;
1320#line 378
1321struct user_namespace;
1322#line 378
1323struct user_namespace;
1324#line 14 "include/linux/prio_tree.h"
1325struct prio_tree_node;
1326#line 14 "include/linux/prio_tree.h"
1327struct raw_prio_tree_node {
1328   struct prio_tree_node *left ;
1329   struct prio_tree_node *right ;
1330   struct prio_tree_node *parent ;
1331};
1332#line 20 "include/linux/prio_tree.h"
1333struct prio_tree_node {
1334   struct prio_tree_node *left ;
1335   struct prio_tree_node *right ;
1336   struct prio_tree_node *parent ;
1337   unsigned long start ;
1338   unsigned long last ;
1339};
1340#line 23 "include/linux/mm_types.h"
1341struct address_space;
1342#line 23
1343struct address_space;
1344#line 40 "include/linux/mm_types.h"
1345union __anonunion____missing_field_name_204 {
1346   unsigned long index ;
1347   void *freelist ;
1348};
1349#line 40 "include/linux/mm_types.h"
1350struct __anonstruct____missing_field_name_208 {
1351   unsigned int inuse : 16 ;
1352   unsigned int objects : 15 ;
1353   unsigned int frozen : 1 ;
1354};
1355#line 40 "include/linux/mm_types.h"
1356union __anonunion____missing_field_name_207 {
1357   atomic_t _mapcount ;
1358   struct __anonstruct____missing_field_name_208 __annonCompField34 ;
1359};
1360#line 40 "include/linux/mm_types.h"
1361struct __anonstruct____missing_field_name_206 {
1362   union __anonunion____missing_field_name_207 __annonCompField35 ;
1363   atomic_t _count ;
1364};
1365#line 40 "include/linux/mm_types.h"
1366union __anonunion____missing_field_name_205 {
1367   unsigned long counters ;
1368   struct __anonstruct____missing_field_name_206 __annonCompField36 ;
1369};
1370#line 40 "include/linux/mm_types.h"
1371struct __anonstruct____missing_field_name_203 {
1372   union __anonunion____missing_field_name_204 __annonCompField33 ;
1373   union __anonunion____missing_field_name_205 __annonCompField37 ;
1374};
1375#line 40 "include/linux/mm_types.h"
1376struct __anonstruct____missing_field_name_210 {
1377   struct page *next ;
1378   int pages ;
1379   int pobjects ;
1380};
1381#line 40 "include/linux/mm_types.h"
1382union __anonunion____missing_field_name_209 {
1383   struct list_head lru ;
1384   struct __anonstruct____missing_field_name_210 __annonCompField39 ;
1385};
1386#line 40 "include/linux/mm_types.h"
1387union __anonunion____missing_field_name_211 {
1388   unsigned long private ;
1389   struct kmem_cache *slab ;
1390   struct page *first_page ;
1391};
1392#line 40 "include/linux/mm_types.h"
1393struct page {
1394   unsigned long flags ;
1395   struct address_space *mapping ;
1396   struct __anonstruct____missing_field_name_203 __annonCompField38 ;
1397   union __anonunion____missing_field_name_209 __annonCompField40 ;
1398   union __anonunion____missing_field_name_211 __annonCompField41 ;
1399   unsigned long debug_flags ;
1400} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
1401#line 200 "include/linux/mm_types.h"
1402struct __anonstruct_vm_set_213 {
1403   struct list_head list ;
1404   void *parent ;
1405   struct vm_area_struct *head ;
1406};
1407#line 200 "include/linux/mm_types.h"
1408union __anonunion_shared_212 {
1409   struct __anonstruct_vm_set_213 vm_set ;
1410   struct raw_prio_tree_node prio_tree_node ;
1411};
1412#line 200
1413struct anon_vma;
1414#line 200
1415struct vm_operations_struct;
1416#line 200
1417struct mempolicy;
1418#line 200 "include/linux/mm_types.h"
1419struct vm_area_struct {
1420   struct mm_struct *vm_mm ;
1421   unsigned long vm_start ;
1422   unsigned long vm_end ;
1423   struct vm_area_struct *vm_next ;
1424   struct vm_area_struct *vm_prev ;
1425   pgprot_t vm_page_prot ;
1426   unsigned long vm_flags ;
1427   struct rb_node vm_rb ;
1428   union __anonunion_shared_212 shared ;
1429   struct list_head anon_vma_chain ;
1430   struct anon_vma *anon_vma ;
1431   struct vm_operations_struct  const  *vm_ops ;
1432   unsigned long vm_pgoff ;
1433   struct file *vm_file ;
1434   void *vm_private_data ;
1435   struct mempolicy *vm_policy ;
1436};
1437#line 257 "include/linux/mm_types.h"
1438struct core_thread {
1439   struct task_struct *task ;
1440   struct core_thread *next ;
1441};
1442#line 262 "include/linux/mm_types.h"
1443struct core_state {
1444   atomic_t nr_threads ;
1445   struct core_thread dumper ;
1446   struct completion startup ;
1447};
1448#line 284 "include/linux/mm_types.h"
1449struct mm_rss_stat {
1450   atomic_long_t count[3] ;
1451};
1452#line 288
1453struct linux_binfmt;
1454#line 288
1455struct mmu_notifier_mm;
1456#line 288 "include/linux/mm_types.h"
1457struct mm_struct {
1458   struct vm_area_struct *mmap ;
1459   struct rb_root mm_rb ;
1460   struct vm_area_struct *mmap_cache ;
1461   unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
1462                                      unsigned long pgoff , unsigned long flags ) ;
1463   void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
1464   unsigned long mmap_base ;
1465   unsigned long task_size ;
1466   unsigned long cached_hole_size ;
1467   unsigned long free_area_cache ;
1468   pgd_t *pgd ;
1469   atomic_t mm_users ;
1470   atomic_t mm_count ;
1471   int map_count ;
1472   spinlock_t page_table_lock ;
1473   struct rw_semaphore mmap_sem ;
1474   struct list_head mmlist ;
1475   unsigned long hiwater_rss ;
1476   unsigned long hiwater_vm ;
1477   unsigned long total_vm ;
1478   unsigned long locked_vm ;
1479   unsigned long pinned_vm ;
1480   unsigned long shared_vm ;
1481   unsigned long exec_vm ;
1482   unsigned long stack_vm ;
1483   unsigned long reserved_vm ;
1484   unsigned long def_flags ;
1485   unsigned long nr_ptes ;
1486   unsigned long start_code ;
1487   unsigned long end_code ;
1488   unsigned long start_data ;
1489   unsigned long end_data ;
1490   unsigned long start_brk ;
1491   unsigned long brk ;
1492   unsigned long start_stack ;
1493   unsigned long arg_start ;
1494   unsigned long arg_end ;
1495   unsigned long env_start ;
1496   unsigned long env_end ;
1497   unsigned long saved_auxv[44] ;
1498   struct mm_rss_stat rss_stat ;
1499   struct linux_binfmt *binfmt ;
1500   cpumask_var_t cpu_vm_mask_var ;
1501   mm_context_t context ;
1502   unsigned int faultstamp ;
1503   unsigned int token_priority ;
1504   unsigned int last_interval ;
1505   unsigned long flags ;
1506   struct core_state *core_state ;
1507   spinlock_t ioctx_lock ;
1508   struct hlist_head ioctx_list ;
1509   struct task_struct *owner ;
1510   struct file *exe_file ;
1511   unsigned long num_exe_file_vmas ;
1512   struct mmu_notifier_mm *mmu_notifier_mm ;
1513   pgtable_t pmd_huge_pte ;
1514   struct cpumask cpumask_allocation ;
1515};
1516#line 7 "include/asm-generic/cputime.h"
1517typedef unsigned long cputime_t;
1518#line 84 "include/linux/sem.h"
1519struct task_struct;
1520#line 101
1521struct sem_undo_list;
1522#line 101 "include/linux/sem.h"
1523struct sysv_sem {
1524   struct sem_undo_list *undo_list ;
1525};
1526#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1527struct siginfo;
1528#line 10
1529struct siginfo;
1530#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1531struct __anonstruct_sigset_t_215 {
1532   unsigned long sig[1] ;
1533};
1534#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1535typedef struct __anonstruct_sigset_t_215 sigset_t;
1536#line 17 "include/asm-generic/signal-defs.h"
1537typedef void __signalfn_t(int  );
1538#line 18 "include/asm-generic/signal-defs.h"
1539typedef __signalfn_t *__sighandler_t;
1540#line 20 "include/asm-generic/signal-defs.h"
1541typedef void __restorefn_t(void);
1542#line 21 "include/asm-generic/signal-defs.h"
1543typedef __restorefn_t *__sigrestore_t;
1544#line 167 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1545struct sigaction {
1546   __sighandler_t sa_handler ;
1547   unsigned long sa_flags ;
1548   __sigrestore_t sa_restorer ;
1549   sigset_t sa_mask ;
1550};
1551#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1552struct k_sigaction {
1553   struct sigaction sa ;
1554};
1555#line 7 "include/asm-generic/siginfo.h"
1556union sigval {
1557   int sival_int ;
1558   void *sival_ptr ;
1559};
1560#line 7 "include/asm-generic/siginfo.h"
1561typedef union sigval sigval_t;
1562#line 48 "include/asm-generic/siginfo.h"
1563struct __anonstruct__kill_217 {
1564   __kernel_pid_t _pid ;
1565   __kernel_uid32_t _uid ;
1566};
1567#line 48 "include/asm-generic/siginfo.h"
1568struct __anonstruct__timer_218 {
1569   __kernel_timer_t _tid ;
1570   int _overrun ;
1571   char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ;
1572   sigval_t _sigval ;
1573   int _sys_private ;
1574};
1575#line 48 "include/asm-generic/siginfo.h"
1576struct __anonstruct__rt_219 {
1577   __kernel_pid_t _pid ;
1578   __kernel_uid32_t _uid ;
1579   sigval_t _sigval ;
1580};
1581#line 48 "include/asm-generic/siginfo.h"
1582struct __anonstruct__sigchld_220 {
1583   __kernel_pid_t _pid ;
1584   __kernel_uid32_t _uid ;
1585   int _status ;
1586   __kernel_clock_t _utime ;
1587   __kernel_clock_t _stime ;
1588};
1589#line 48 "include/asm-generic/siginfo.h"
1590struct __anonstruct__sigfault_221 {
1591   void *_addr ;
1592   short _addr_lsb ;
1593};
1594#line 48 "include/asm-generic/siginfo.h"
1595struct __anonstruct__sigpoll_222 {
1596   long _band ;
1597   int _fd ;
1598};
1599#line 48 "include/asm-generic/siginfo.h"
1600union __anonunion__sifields_216 {
1601   int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ;
1602   struct __anonstruct__kill_217 _kill ;
1603   struct __anonstruct__timer_218 _timer ;
1604   struct __anonstruct__rt_219 _rt ;
1605   struct __anonstruct__sigchld_220 _sigchld ;
1606   struct __anonstruct__sigfault_221 _sigfault ;
1607   struct __anonstruct__sigpoll_222 _sigpoll ;
1608};
1609#line 48 "include/asm-generic/siginfo.h"
1610struct siginfo {
1611   int si_signo ;
1612   int si_errno ;
1613   int si_code ;
1614   union __anonunion__sifields_216 _sifields ;
1615};
1616#line 48 "include/asm-generic/siginfo.h"
1617typedef struct siginfo siginfo_t;
1618#line 288
1619struct siginfo;
1620#line 10 "include/linux/signal.h"
1621struct task_struct;
1622#line 18
1623struct user_struct;
1624#line 28 "include/linux/signal.h"
1625struct sigpending {
1626   struct list_head list ;
1627   sigset_t signal ;
1628};
1629#line 239
1630struct timespec;
1631#line 240
1632struct pt_regs;
1633#line 50 "include/linux/pid.h"
1634struct pid_namespace;
1635#line 50 "include/linux/pid.h"
1636struct upid {
1637   int nr ;
1638   struct pid_namespace *ns ;
1639   struct hlist_node pid_chain ;
1640};
1641#line 57 "include/linux/pid.h"
1642struct pid {
1643   atomic_t count ;
1644   unsigned int level ;
1645   struct hlist_head tasks[3] ;
1646   struct rcu_head rcu ;
1647   struct upid numbers[1] ;
1648};
1649#line 69 "include/linux/pid.h"
1650struct pid_link {
1651   struct hlist_node node ;
1652   struct pid *pid ;
1653};
1654#line 100
1655struct pid_namespace;
1656#line 10 "include/linux/seccomp.h"
1657struct __anonstruct_seccomp_t_225 {
1658   int mode ;
1659};
1660#line 10 "include/linux/seccomp.h"
1661typedef struct __anonstruct_seccomp_t_225 seccomp_t;
1662#line 81 "include/linux/plist.h"
1663struct plist_head {
1664   struct list_head node_list ;
1665};
1666#line 85 "include/linux/plist.h"
1667struct plist_node {
1668   int prio ;
1669   struct list_head prio_list ;
1670   struct list_head node_list ;
1671};
1672#line 28 "include/linux/rtmutex.h"
1673struct rt_mutex {
1674   raw_spinlock_t wait_lock ;
1675   struct plist_head wait_list ;
1676   struct task_struct *owner ;
1677   int save_state ;
1678   char const   *name ;
1679   char const   *file ;
1680   int line ;
1681   void *magic ;
1682};
1683#line 40
1684struct rt_mutex_waiter;
1685#line 40
1686struct rt_mutex_waiter;
1687#line 42 "include/linux/resource.h"
1688struct rlimit {
1689   unsigned long rlim_cur ;
1690   unsigned long rlim_max ;
1691};
1692#line 81
1693struct task_struct;
1694#line 8 "include/linux/timerqueue.h"
1695struct timerqueue_node {
1696   struct rb_node node ;
1697   ktime_t expires ;
1698};
1699#line 13 "include/linux/timerqueue.h"
1700struct timerqueue_head {
1701   struct rb_root head ;
1702   struct timerqueue_node *next ;
1703};
1704#line 27 "include/linux/hrtimer.h"
1705struct hrtimer_clock_base;
1706#line 27
1707struct hrtimer_clock_base;
1708#line 28
1709struct hrtimer_cpu_base;
1710#line 28
1711struct hrtimer_cpu_base;
1712#line 44
1713enum hrtimer_restart {
1714    HRTIMER_NORESTART = 0,
1715    HRTIMER_RESTART = 1
1716} ;
1717#line 108 "include/linux/hrtimer.h"
1718struct hrtimer {
1719   struct timerqueue_node node ;
1720   ktime_t _softexpires ;
1721   enum hrtimer_restart (*function)(struct hrtimer * ) ;
1722   struct hrtimer_clock_base *base ;
1723   unsigned long state ;
1724   int start_pid ;
1725   void *start_site ;
1726   char start_comm[16] ;
1727};
1728#line 145 "include/linux/hrtimer.h"
1729struct hrtimer_clock_base {
1730   struct hrtimer_cpu_base *cpu_base ;
1731   int index ;
1732   clockid_t clockid ;
1733   struct timerqueue_head active ;
1734   ktime_t resolution ;
1735   ktime_t (*get_time)(void) ;
1736   ktime_t softirq_time ;
1737   ktime_t offset ;
1738};
1739#line 178 "include/linux/hrtimer.h"
1740struct hrtimer_cpu_base {
1741   raw_spinlock_t lock ;
1742   unsigned long active_bases ;
1743   ktime_t expires_next ;
1744   int hres_active ;
1745   int hang_detected ;
1746   unsigned long nr_events ;
1747   unsigned long nr_retries ;
1748   unsigned long nr_hangs ;
1749   ktime_t max_hang_time ;
1750   struct hrtimer_clock_base clock_base[3] ;
1751};
1752#line 11 "include/linux/task_io_accounting.h"
1753struct task_io_accounting {
1754   u64 rchar ;
1755   u64 wchar ;
1756   u64 syscr ;
1757   u64 syscw ;
1758   u64 read_bytes ;
1759   u64 write_bytes ;
1760   u64 cancelled_write_bytes ;
1761};
1762#line 13 "include/linux/latencytop.h"
1763struct task_struct;
1764#line 20 "include/linux/latencytop.h"
1765struct latency_record {
1766   unsigned long backtrace[12] ;
1767   unsigned int count ;
1768   unsigned long time ;
1769   unsigned long max ;
1770};
1771#line 29 "include/linux/key.h"
1772typedef int32_t key_serial_t;
1773#line 32 "include/linux/key.h"
1774typedef uint32_t key_perm_t;
1775#line 34
1776struct key;
1777#line 34
1778struct key;
1779#line 75
1780struct user_struct;
1781#line 76
1782struct signal_struct;
1783#line 76
1784struct signal_struct;
1785#line 77
1786struct cred;
1787#line 79
1788struct key_type;
1789#line 79
1790struct key_type;
1791#line 81
1792struct keyring_list;
1793#line 81
1794struct keyring_list;
1795#line 124
1796struct key_user;
1797#line 124 "include/linux/key.h"
1798union __anonunion____missing_field_name_226 {
1799   time_t expiry ;
1800   time_t revoked_at ;
1801};
1802#line 124 "include/linux/key.h"
1803union __anonunion_type_data_227 {
1804   struct list_head link ;
1805   unsigned long x[2] ;
1806   void *p[2] ;
1807   int reject_error ;
1808};
1809#line 124 "include/linux/key.h"
1810union __anonunion_payload_228 {
1811   unsigned long value ;
1812   void *rcudata ;
1813   void *data ;
1814   struct keyring_list *subscriptions ;
1815};
1816#line 124 "include/linux/key.h"
1817struct key {
1818   atomic_t usage ;
1819   key_serial_t serial ;
1820   struct rb_node serial_node ;
1821   struct key_type *type ;
1822   struct rw_semaphore sem ;
1823   struct key_user *user ;
1824   void *security ;
1825   union __anonunion____missing_field_name_226 __annonCompField42 ;
1826   uid_t uid ;
1827   gid_t gid ;
1828   key_perm_t perm ;
1829   unsigned short quotalen ;
1830   unsigned short datalen ;
1831   unsigned long flags ;
1832   char *description ;
1833   union __anonunion_type_data_227 type_data ;
1834   union __anonunion_payload_228 payload ;
1835};
1836#line 18 "include/linux/selinux.h"
1837struct audit_context;
1838#line 18
1839struct audit_context;
1840#line 21 "include/linux/cred.h"
1841struct user_struct;
1842#line 22
1843struct cred;
1844#line 31 "include/linux/cred.h"
1845struct group_info {
1846   atomic_t usage ;
1847   int ngroups ;
1848   int nblocks ;
1849   gid_t small_block[32] ;
1850   gid_t *blocks[0] ;
1851};
1852#line 83 "include/linux/cred.h"
1853struct thread_group_cred {
1854   atomic_t usage ;
1855   pid_t tgid ;
1856   spinlock_t lock ;
1857   struct key *session_keyring ;
1858   struct key *process_keyring ;
1859   struct rcu_head rcu ;
1860};
1861#line 116 "include/linux/cred.h"
1862struct cred {
1863   atomic_t usage ;
1864   atomic_t subscribers ;
1865   void *put_addr ;
1866   unsigned int magic ;
1867   uid_t uid ;
1868   gid_t gid ;
1869   uid_t suid ;
1870   gid_t sgid ;
1871   uid_t euid ;
1872   gid_t egid ;
1873   uid_t fsuid ;
1874   gid_t fsgid ;
1875   unsigned int securebits ;
1876   kernel_cap_t cap_inheritable ;
1877   kernel_cap_t cap_permitted ;
1878   kernel_cap_t cap_effective ;
1879   kernel_cap_t cap_bset ;
1880   unsigned char jit_keyring ;
1881   struct key *thread_keyring ;
1882   struct key *request_key_auth ;
1883   struct thread_group_cred *tgcred ;
1884   void *security ;
1885   struct user_struct *user ;
1886   struct user_namespace *user_ns ;
1887   struct group_info *group_info ;
1888   struct rcu_head rcu ;
1889};
1890#line 61 "include/linux/llist.h"
1891struct llist_node;
1892#line 65 "include/linux/llist.h"
1893struct llist_node {
1894   struct llist_node *next ;
1895};
1896#line 97 "include/linux/sched.h"
1897struct futex_pi_state;
1898#line 97
1899struct futex_pi_state;
1900#line 98
1901struct robust_list_head;
1902#line 98
1903struct robust_list_head;
1904#line 99
1905struct bio_list;
1906#line 99
1907struct bio_list;
1908#line 100
1909struct fs_struct;
1910#line 100
1911struct fs_struct;
1912#line 101
1913struct perf_event_context;
1914#line 101
1915struct perf_event_context;
1916#line 102
1917struct blk_plug;
1918#line 102
1919struct blk_plug;
1920#line 151
1921struct cfs_rq;
1922#line 151
1923struct cfs_rq;
1924#line 259
1925struct task_struct;
1926#line 366
1927struct nsproxy;
1928#line 367
1929struct user_namespace;
1930#line 214 "include/linux/aio.h"
1931struct mm_struct;
1932#line 443 "include/linux/sched.h"
1933struct sighand_struct {
1934   atomic_t count ;
1935   struct k_sigaction action[64] ;
1936   spinlock_t siglock ;
1937   wait_queue_head_t signalfd_wqh ;
1938};
1939#line 450 "include/linux/sched.h"
1940struct pacct_struct {
1941   int ac_flag ;
1942   long ac_exitcode ;
1943   unsigned long ac_mem ;
1944   cputime_t ac_utime ;
1945   cputime_t ac_stime ;
1946   unsigned long ac_minflt ;
1947   unsigned long ac_majflt ;
1948};
1949#line 458 "include/linux/sched.h"
1950struct cpu_itimer {
1951   cputime_t expires ;
1952   cputime_t incr ;
1953   u32 error ;
1954   u32 incr_error ;
1955};
1956#line 476 "include/linux/sched.h"
1957struct task_cputime {
1958   cputime_t utime ;
1959   cputime_t stime ;
1960   unsigned long long sum_exec_runtime ;
1961};
1962#line 512 "include/linux/sched.h"
1963struct thread_group_cputimer {
1964   struct task_cputime cputime ;
1965   int running ;
1966   raw_spinlock_t lock ;
1967};
1968#line 519
1969struct autogroup;
1970#line 519
1971struct autogroup;
1972#line 528
1973struct tty_struct;
1974#line 528
1975struct taskstats;
1976#line 528
1977struct tty_audit_buf;
1978#line 528 "include/linux/sched.h"
1979struct signal_struct {
1980   atomic_t sigcnt ;
1981   atomic_t live ;
1982   int nr_threads ;
1983   wait_queue_head_t wait_chldexit ;
1984   struct task_struct *curr_target ;
1985   struct sigpending shared_pending ;
1986   int group_exit_code ;
1987   int notify_count ;
1988   struct task_struct *group_exit_task ;
1989   int group_stop_count ;
1990   unsigned int flags ;
1991   unsigned int is_child_subreaper : 1 ;
1992   unsigned int has_child_subreaper : 1 ;
1993   struct list_head posix_timers ;
1994   struct hrtimer real_timer ;
1995   struct pid *leader_pid ;
1996   ktime_t it_real_incr ;
1997   struct cpu_itimer it[2] ;
1998   struct thread_group_cputimer cputimer ;
1999   struct task_cputime cputime_expires ;
2000   struct list_head cpu_timers[3] ;
2001   struct pid *tty_old_pgrp ;
2002   int leader ;
2003   struct tty_struct *tty ;
2004   struct autogroup *autogroup ;
2005   cputime_t utime ;
2006   cputime_t stime ;
2007   cputime_t cutime ;
2008   cputime_t cstime ;
2009   cputime_t gtime ;
2010   cputime_t cgtime ;
2011   cputime_t prev_utime ;
2012   cputime_t prev_stime ;
2013   unsigned long nvcsw ;
2014   unsigned long nivcsw ;
2015   unsigned long cnvcsw ;
2016   unsigned long cnivcsw ;
2017   unsigned long min_flt ;
2018   unsigned long maj_flt ;
2019   unsigned long cmin_flt ;
2020   unsigned long cmaj_flt ;
2021   unsigned long inblock ;
2022   unsigned long oublock ;
2023   unsigned long cinblock ;
2024   unsigned long coublock ;
2025   unsigned long maxrss ;
2026   unsigned long cmaxrss ;
2027   struct task_io_accounting ioac ;
2028   unsigned long long sum_sched_runtime ;
2029   struct rlimit rlim[16] ;
2030   struct pacct_struct pacct ;
2031   struct taskstats *stats ;
2032   unsigned int audit_tty ;
2033   struct tty_audit_buf *tty_audit_buf ;
2034   struct rw_semaphore group_rwsem ;
2035   int oom_adj ;
2036   int oom_score_adj ;
2037   int oom_score_adj_min ;
2038   struct mutex cred_guard_mutex ;
2039};
2040#line 703 "include/linux/sched.h"
2041struct user_struct {
2042   atomic_t __count ;
2043   atomic_t processes ;
2044   atomic_t files ;
2045   atomic_t sigpending ;
2046   atomic_t inotify_watches ;
2047   atomic_t inotify_devs ;
2048   atomic_t fanotify_listeners ;
2049   atomic_long_t epoll_watches ;
2050   unsigned long mq_bytes ;
2051   unsigned long locked_shm ;
2052   struct key *uid_keyring ;
2053   struct key *session_keyring ;
2054   struct hlist_node uidhash_node ;
2055   uid_t uid ;
2056   struct user_namespace *user_ns ;
2057   atomic_long_t locked_vm ;
2058};
2059#line 747
2060struct backing_dev_info;
2061#line 747
2062struct backing_dev_info;
2063#line 748
2064struct reclaim_state;
2065#line 748
2066struct reclaim_state;
2067#line 751 "include/linux/sched.h"
2068struct sched_info {
2069   unsigned long pcount ;
2070   unsigned long long run_delay ;
2071   unsigned long long last_arrival ;
2072   unsigned long long last_queued ;
2073};
2074#line 763 "include/linux/sched.h"
2075struct task_delay_info {
2076   spinlock_t lock ;
2077   unsigned int flags ;
2078   struct timespec blkio_start ;
2079   struct timespec blkio_end ;
2080   u64 blkio_delay ;
2081   u64 swapin_delay ;
2082   u32 blkio_count ;
2083   u32 swapin_count ;
2084   struct timespec freepages_start ;
2085   struct timespec freepages_end ;
2086   u64 freepages_delay ;
2087   u32 freepages_count ;
2088};
2089#line 1088
2090struct io_context;
2091#line 1088
2092struct io_context;
2093#line 1097
2094struct audit_context;
2095#line 1098
2096struct mempolicy;
2097#line 1099
2098struct pipe_inode_info;
2099#line 1099
2100struct pipe_inode_info;
2101#line 1102
2102struct rq;
2103#line 1102
2104struct rq;
2105#line 1122 "include/linux/sched.h"
2106struct sched_class {
2107   struct sched_class  const  *next ;
2108   void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
2109   void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
2110   void (*yield_task)(struct rq *rq ) ;
2111   bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ;
2112   void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ;
2113   struct task_struct *(*pick_next_task)(struct rq *rq ) ;
2114   void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ;
2115   int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ;
2116   void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ;
2117   void (*post_schedule)(struct rq *this_rq ) ;
2118   void (*task_waking)(struct task_struct *task ) ;
2119   void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ;
2120   void (*set_cpus_allowed)(struct task_struct *p , struct cpumask  const  *newmask ) ;
2121   void (*rq_online)(struct rq *rq ) ;
2122   void (*rq_offline)(struct rq *rq ) ;
2123   void (*set_curr_task)(struct rq *rq ) ;
2124   void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ;
2125   void (*task_fork)(struct task_struct *p ) ;
2126   void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ;
2127   void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ;
2128   void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ;
2129   unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ;
2130   void (*task_move_group)(struct task_struct *p , int on_rq ) ;
2131};
2132#line 1167 "include/linux/sched.h"
2133struct load_weight {
2134   unsigned long weight ;
2135   unsigned long inv_weight ;
2136};
2137#line 1172 "include/linux/sched.h"
2138struct sched_statistics {
2139   u64 wait_start ;
2140   u64 wait_max ;
2141   u64 wait_count ;
2142   u64 wait_sum ;
2143   u64 iowait_count ;
2144   u64 iowait_sum ;
2145   u64 sleep_start ;
2146   u64 sleep_max ;
2147   s64 sum_sleep_runtime ;
2148   u64 block_start ;
2149   u64 block_max ;
2150   u64 exec_max ;
2151   u64 slice_max ;
2152   u64 nr_migrations_cold ;
2153   u64 nr_failed_migrations_affine ;
2154   u64 nr_failed_migrations_running ;
2155   u64 nr_failed_migrations_hot ;
2156   u64 nr_forced_migrations ;
2157   u64 nr_wakeups ;
2158   u64 nr_wakeups_sync ;
2159   u64 nr_wakeups_migrate ;
2160   u64 nr_wakeups_local ;
2161   u64 nr_wakeups_remote ;
2162   u64 nr_wakeups_affine ;
2163   u64 nr_wakeups_affine_attempts ;
2164   u64 nr_wakeups_passive ;
2165   u64 nr_wakeups_idle ;
2166};
2167#line 1207 "include/linux/sched.h"
2168struct sched_entity {
2169   struct load_weight load ;
2170   struct rb_node run_node ;
2171   struct list_head group_node ;
2172   unsigned int on_rq ;
2173   u64 exec_start ;
2174   u64 sum_exec_runtime ;
2175   u64 vruntime ;
2176   u64 prev_sum_exec_runtime ;
2177   u64 nr_migrations ;
2178   struct sched_statistics statistics ;
2179   struct sched_entity *parent ;
2180   struct cfs_rq *cfs_rq ;
2181   struct cfs_rq *my_q ;
2182};
2183#line 1233
2184struct rt_rq;
2185#line 1233 "include/linux/sched.h"
2186struct sched_rt_entity {
2187   struct list_head run_list ;
2188   unsigned long timeout ;
2189   unsigned int time_slice ;
2190   int nr_cpus_allowed ;
2191   struct sched_rt_entity *back ;
2192   struct sched_rt_entity *parent ;
2193   struct rt_rq *rt_rq ;
2194   struct rt_rq *my_q ;
2195};
2196#line 1264
2197struct files_struct;
2198#line 1264
2199struct css_set;
2200#line 1264
2201struct compat_robust_list_head;
2202#line 1264
2203struct mem_cgroup;
2204#line 1264 "include/linux/sched.h"
2205struct memcg_batch_info {
2206   int do_batch ;
2207   struct mem_cgroup *memcg ;
2208   unsigned long nr_pages ;
2209   unsigned long memsw_nr_pages ;
2210};
2211#line 1264 "include/linux/sched.h"
2212struct task_struct {
2213   long volatile   state ;
2214   void *stack ;
2215   atomic_t usage ;
2216   unsigned int flags ;
2217   unsigned int ptrace ;
2218   struct llist_node wake_entry ;
2219   int on_cpu ;
2220   int on_rq ;
2221   int prio ;
2222   int static_prio ;
2223   int normal_prio ;
2224   unsigned int rt_priority ;
2225   struct sched_class  const  *sched_class ;
2226   struct sched_entity se ;
2227   struct sched_rt_entity rt ;
2228   struct hlist_head preempt_notifiers ;
2229   unsigned char fpu_counter ;
2230   unsigned int policy ;
2231   cpumask_t cpus_allowed ;
2232   struct sched_info sched_info ;
2233   struct list_head tasks ;
2234   struct plist_node pushable_tasks ;
2235   struct mm_struct *mm ;
2236   struct mm_struct *active_mm ;
2237   unsigned int brk_randomized : 1 ;
2238   int exit_state ;
2239   int exit_code ;
2240   int exit_signal ;
2241   int pdeath_signal ;
2242   unsigned int jobctl ;
2243   unsigned int personality ;
2244   unsigned int did_exec : 1 ;
2245   unsigned int in_execve : 1 ;
2246   unsigned int in_iowait : 1 ;
2247   unsigned int sched_reset_on_fork : 1 ;
2248   unsigned int sched_contributes_to_load : 1 ;
2249   unsigned int irq_thread : 1 ;
2250   pid_t pid ;
2251   pid_t tgid ;
2252   unsigned long stack_canary ;
2253   struct task_struct *real_parent ;
2254   struct task_struct *parent ;
2255   struct list_head children ;
2256   struct list_head sibling ;
2257   struct task_struct *group_leader ;
2258   struct list_head ptraced ;
2259   struct list_head ptrace_entry ;
2260   struct pid_link pids[3] ;
2261   struct list_head thread_group ;
2262   struct completion *vfork_done ;
2263   int *set_child_tid ;
2264   int *clear_child_tid ;
2265   cputime_t utime ;
2266   cputime_t stime ;
2267   cputime_t utimescaled ;
2268   cputime_t stimescaled ;
2269   cputime_t gtime ;
2270   cputime_t prev_utime ;
2271   cputime_t prev_stime ;
2272   unsigned long nvcsw ;
2273   unsigned long nivcsw ;
2274   struct timespec start_time ;
2275   struct timespec real_start_time ;
2276   unsigned long min_flt ;
2277   unsigned long maj_flt ;
2278   struct task_cputime cputime_expires ;
2279   struct list_head cpu_timers[3] ;
2280   struct cred  const  *real_cred ;
2281   struct cred  const  *cred ;
2282   struct cred *replacement_session_keyring ;
2283   char comm[16] ;
2284   int link_count ;
2285   int total_link_count ;
2286   struct sysv_sem sysvsem ;
2287   unsigned long last_switch_count ;
2288   struct thread_struct thread ;
2289   struct fs_struct *fs ;
2290   struct files_struct *files ;
2291   struct nsproxy *nsproxy ;
2292   struct signal_struct *signal ;
2293   struct sighand_struct *sighand ;
2294   sigset_t blocked ;
2295   sigset_t real_blocked ;
2296   sigset_t saved_sigmask ;
2297   struct sigpending pending ;
2298   unsigned long sas_ss_sp ;
2299   size_t sas_ss_size ;
2300   int (*notifier)(void *priv ) ;
2301   void *notifier_data ;
2302   sigset_t *notifier_mask ;
2303   struct audit_context *audit_context ;
2304   uid_t loginuid ;
2305   unsigned int sessionid ;
2306   seccomp_t seccomp ;
2307   u32 parent_exec_id ;
2308   u32 self_exec_id ;
2309   spinlock_t alloc_lock ;
2310   raw_spinlock_t pi_lock ;
2311   struct plist_head pi_waiters ;
2312   struct rt_mutex_waiter *pi_blocked_on ;
2313   struct mutex_waiter *blocked_on ;
2314   unsigned int irq_events ;
2315   unsigned long hardirq_enable_ip ;
2316   unsigned long hardirq_disable_ip ;
2317   unsigned int hardirq_enable_event ;
2318   unsigned int hardirq_disable_event ;
2319   int hardirqs_enabled ;
2320   int hardirq_context ;
2321   unsigned long softirq_disable_ip ;
2322   unsigned long softirq_enable_ip ;
2323   unsigned int softirq_disable_event ;
2324   unsigned int softirq_enable_event ;
2325   int softirqs_enabled ;
2326   int softirq_context ;
2327   void *journal_info ;
2328   struct bio_list *bio_list ;
2329   struct blk_plug *plug ;
2330   struct reclaim_state *reclaim_state ;
2331   struct backing_dev_info *backing_dev_info ;
2332   struct io_context *io_context ;
2333   unsigned long ptrace_message ;
2334   siginfo_t *last_siginfo ;
2335   struct task_io_accounting ioac ;
2336   u64 acct_rss_mem1 ;
2337   u64 acct_vm_mem1 ;
2338   cputime_t acct_timexpd ;
2339   nodemask_t mems_allowed ;
2340   seqcount_t mems_allowed_seq ;
2341   int cpuset_mem_spread_rotor ;
2342   int cpuset_slab_spread_rotor ;
2343   struct css_set *cgroups ;
2344   struct list_head cg_list ;
2345   struct robust_list_head *robust_list ;
2346   struct compat_robust_list_head *compat_robust_list ;
2347   struct list_head pi_state_list ;
2348   struct futex_pi_state *pi_state_cache ;
2349   struct perf_event_context *perf_event_ctxp[2] ;
2350   struct mutex perf_event_mutex ;
2351   struct list_head perf_event_list ;
2352   struct mempolicy *mempolicy ;
2353   short il_next ;
2354   short pref_node_fork ;
2355   struct rcu_head rcu ;
2356   struct pipe_inode_info *splice_pipe ;
2357   struct task_delay_info *delays ;
2358   int make_it_fail ;
2359   int nr_dirtied ;
2360   int nr_dirtied_pause ;
2361   unsigned long dirty_paused_when ;
2362   int latency_record_count ;
2363   struct latency_record latency_record[32] ;
2364   unsigned long timer_slack_ns ;
2365   unsigned long default_timer_slack_ns ;
2366   struct list_head *scm_work_list ;
2367   unsigned long trace ;
2368   unsigned long trace_recursion ;
2369   struct memcg_batch_info memcg_batch ;
2370   atomic_t ptrace_bp_refcnt ;
2371};
2372#line 1681
2373struct pid_namespace;
2374#line 28 "include/linux/of.h"
2375typedef u32 phandle;
2376#line 31 "include/linux/of.h"
2377struct property {
2378   char *name ;
2379   int length ;
2380   void *value ;
2381   struct property *next ;
2382   unsigned long _flags ;
2383   unsigned int unique_id ;
2384};
2385#line 44
2386struct proc_dir_entry;
2387#line 44 "include/linux/of.h"
2388struct device_node {
2389   char const   *name ;
2390   char const   *type ;
2391   phandle phandle ;
2392   char *full_name ;
2393   struct property *properties ;
2394   struct property *deadprops ;
2395   struct device_node *parent ;
2396   struct device_node *child ;
2397   struct device_node *sibling ;
2398   struct device_node *next ;
2399   struct device_node *allnext ;
2400   struct proc_dir_entry *pde ;
2401   struct kref kref ;
2402   unsigned long _flags ;
2403   void *data ;
2404};
2405#line 44 "include/linux/i2c.h"
2406struct i2c_msg;
2407#line 44
2408struct i2c_msg;
2409#line 45
2410struct i2c_algorithm;
2411#line 45
2412struct i2c_algorithm;
2413#line 46
2414struct i2c_adapter;
2415#line 46
2416struct i2c_adapter;
2417#line 47
2418struct i2c_client;
2419#line 47
2420struct i2c_client;
2421#line 48
2422struct i2c_driver;
2423#line 48
2424struct i2c_driver;
2425#line 49
2426union i2c_smbus_data;
2427#line 49
2428union i2c_smbus_data;
2429#line 50
2430struct i2c_board_info;
2431#line 50
2432struct i2c_board_info;
2433#line 52
2434struct module;
2435#line 161 "include/linux/i2c.h"
2436struct i2c_driver {
2437   unsigned int class ;
2438   int (*attach_adapter)(struct i2c_adapter * )  __attribute__((__deprecated__)) ;
2439   int (*detach_adapter)(struct i2c_adapter * )  __attribute__((__deprecated__)) ;
2440   int (*probe)(struct i2c_client * , struct i2c_device_id  const  * ) ;
2441   int (*remove)(struct i2c_client * ) ;
2442   void (*shutdown)(struct i2c_client * ) ;
2443   int (*suspend)(struct i2c_client * , pm_message_t mesg ) ;
2444   int (*resume)(struct i2c_client * ) ;
2445   void (*alert)(struct i2c_client * , unsigned int data ) ;
2446   int (*command)(struct i2c_client *client , unsigned int cmd , void *arg ) ;
2447   struct device_driver driver ;
2448   struct i2c_device_id  const  *id_table ;
2449   int (*detect)(struct i2c_client * , struct i2c_board_info * ) ;
2450   unsigned short const   *address_list ;
2451   struct list_head clients ;
2452};
2453#line 220 "include/linux/i2c.h"
2454struct i2c_client {
2455   unsigned short flags ;
2456   unsigned short addr ;
2457   char name[20] ;
2458   struct i2c_adapter *adapter ;
2459   struct i2c_driver *driver ;
2460   struct device dev ;
2461   int irq ;
2462   struct list_head detected ;
2463};
2464#line 273 "include/linux/i2c.h"
2465struct i2c_board_info {
2466   char type[20] ;
2467   unsigned short flags ;
2468   unsigned short addr ;
2469   void *platform_data ;
2470   struct dev_archdata *archdata ;
2471   struct device_node *of_node ;
2472   int irq ;
2473};
2474#line 352 "include/linux/i2c.h"
2475struct i2c_algorithm {
2476   int (*master_xfer)(struct i2c_adapter *adap , struct i2c_msg *msgs , int num ) ;
2477   int (*smbus_xfer)(struct i2c_adapter *adap , u16 addr , unsigned short flags ,
2478                     char read_write , u8 command , int size , union i2c_smbus_data *data ) ;
2479   u32 (*functionality)(struct i2c_adapter * ) ;
2480};
2481#line 373 "include/linux/i2c.h"
2482struct i2c_adapter {
2483   struct module *owner ;
2484   unsigned int class ;
2485   struct i2c_algorithm  const  *algo ;
2486   void *algo_data ;
2487   struct rt_mutex bus_lock ;
2488   int timeout ;
2489   int retries ;
2490   struct device dev ;
2491   int nr ;
2492   char name[48] ;
2493   struct completion dev_released ;
2494   struct mutex userspace_clients_lock ;
2495   struct list_head userspace_clients ;
2496};
2497#line 538 "include/linux/i2c.h"
2498struct i2c_msg {
2499   __u16 addr ;
2500   __u16 flags ;
2501   __u16 len ;
2502   __u8 *buf ;
2503};
2504#line 596 "include/linux/i2c.h"
2505union i2c_smbus_data {
2506   __u8 byte ;
2507   __u16 word ;
2508   __u8 block[34] ;
2509};
2510#line 1 "<compiler builtins>"
2511long __builtin_expect(long val , long res ) ;
2512#line 215 "include/linux/kernel.h"
2513extern int __attribute__((__warn_unused_result__))  _kstrtoul(char const   *s , unsigned int base ,
2514                                                              unsigned long *res ) ;
2515#line 218
2516extern int __attribute__((__warn_unused_result__))  kstrtoull(char const   *s , unsigned int base ,
2517                                                              unsigned long long *res ) ;
2518#line 220
2519__inline static int __attribute__((__warn_unused_result__))  kstrtoul(char const   *s ,
2520                                                                      unsigned int base ,
2521                                                                      unsigned long *res )  __attribute__((__no_instrument_function__)) ;
2522#line 220 "include/linux/kernel.h"
2523__inline static int __attribute__((__warn_unused_result__))  kstrtoul(char const   *s ,
2524                                                                      unsigned int base ,
2525                                                                      unsigned long *res ) 
2526{ int tmp ;
2527  int tmp___0 ;
2528  unsigned long long *__cil_tmp6 ;
2529
2530  {
2531#line 226
2532  if (8UL == 8UL) {
2533#line 226
2534    if (8UL == 8UL) {
2535      {
2536#line 228
2537      __cil_tmp6 = (unsigned long long *)res;
2538#line 228
2539      tmp = (int )kstrtoull(s, base, __cil_tmp6);
2540      }
2541#line 228
2542      return (tmp);
2543    } else {
2544      {
2545#line 230
2546      tmp___0 = (int )_kstrtoul(s, base, res);
2547      }
2548#line 230
2549      return (tmp___0);
2550    }
2551  } else {
2552    {
2553#line 230
2554    tmp___0 = (int )_kstrtoul(s, base, res);
2555    }
2556#line 230
2557    return (tmp___0);
2558  }
2559}
2560}
2561#line 320
2562extern int ( /* format attribute */  sprintf)(char *buf , char const   *fmt  , ...) ;
2563#line 152 "include/linux/mutex.h"
2564void mutex_lock(struct mutex *lock ) ;
2565#line 153
2566int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
2567#line 154
2568int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
2569#line 168
2570int mutex_trylock(struct mutex *lock ) ;
2571#line 169
2572void mutex_unlock(struct mutex *lock ) ;
2573#line 170
2574int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
2575#line 158 "include/linux/sysfs.h"
2576extern int __attribute__((__warn_unused_result__))  sysfs_create_group(struct kobject *kobj ,
2577                                                                       struct attribute_group  const  *grp ) ;
2578#line 162
2579extern void sysfs_remove_group(struct kobject *kobj , struct attribute_group  const  *grp ) ;
2580#line 26 "include/linux/export.h"
2581extern struct module __this_module ;
2582#line 67 "include/linux/module.h"
2583int init_module(void) ;
2584#line 68
2585void cleanup_module(void) ;
2586#line 891 "include/linux/device.h"
2587extern int ( /* format attribute */  dev_err)(struct device  const  *dev , char const   *fmt 
2588                                              , ...) ;
2589#line 897
2590extern int ( /* format attribute */  _dev_info)(struct device  const  *dev , char const   *fmt 
2591                                                , ...) ;
2592#line 86 "include/linux/i2c.h"
2593extern s32 i2c_smbus_read_byte_data(struct i2c_client  const  *client , u8 command ) ;
2594#line 88
2595extern s32 i2c_smbus_write_byte_data(struct i2c_client  const  *client , u8 command ,
2596                                     u8 value ) ;
2597#line 450
2598extern int i2c_register_driver(struct module * , struct i2c_driver * ) ;
2599#line 451
2600extern void i2c_del_driver(struct i2c_driver * ) ;
2601#line 46 "include/linux/delay.h"
2602extern void msleep(unsigned int msecs ) ;
2603#line 30 "include/linux/pm_runtime.h"
2604extern int __pm_runtime_idle(struct device *dev , int rpmflags ) ;
2605#line 32
2606extern int __pm_runtime_resume(struct device *dev , int rpmflags ) ;
2607#line 36
2608extern void pm_runtime_enable(struct device *dev ) ;
2609#line 198
2610__inline static int pm_runtime_get_sync(struct device *dev )  __attribute__((__no_instrument_function__)) ;
2611#line 198 "include/linux/pm_runtime.h"
2612__inline static int pm_runtime_get_sync(struct device *dev ) 
2613{ int tmp___7 ;
2614
2615  {
2616  {
2617#line 200
2618  tmp___7 = __pm_runtime_resume(dev, 4);
2619  }
2620#line 200
2621  return (tmp___7);
2622}
2623}
2624#line 214
2625__inline static int pm_runtime_put_sync(struct device *dev )  __attribute__((__no_instrument_function__)) ;
2626#line 214 "include/linux/pm_runtime.h"
2627__inline static int pm_runtime_put_sync(struct device *dev ) 
2628{ int tmp___7 ;
2629
2630  {
2631  {
2632#line 216
2633  tmp___7 = __pm_runtime_idle(dev, 4);
2634  }
2635#line 216
2636  return (tmp___7);
2637}
2638}
2639#line 35 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
2640static struct mutex mutex  =    {{1}, {{{{{(__ticketpair_t )0}}, 3735899821U, 4294967295U, (void *)-1L}}}, {& mutex.wait_list,
2641                                                                               & mutex.wait_list},
2642    (struct task_struct *)0, (char const   *)0, (void *)(& mutex)};
2643#line 37 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
2644static ssize_t als_sensing_range_show(struct device *dev , struct device_attribute *attr ,
2645                                      char *buf ) 
2646{ struct i2c_client *client ;
2647  struct device  const  *__mptr ;
2648  int val ;
2649  int tmp___7 ;
2650  struct i2c_client *__cil_tmp8 ;
2651  unsigned long __cil_tmp9 ;
2652  unsigned long __cil_tmp10 ;
2653  struct device *__cil_tmp11 ;
2654  unsigned int __cil_tmp12 ;
2655  char *__cil_tmp13 ;
2656  char *__cil_tmp14 ;
2657  struct i2c_client  const  *__cil_tmp15 ;
2658  u8 __cil_tmp16 ;
2659  int __cil_tmp17 ;
2660  int __cil_tmp18 ;
2661  int __cil_tmp19 ;
2662
2663  {
2664  {
2665#line 40
2666  __mptr = (struct device  const  *)dev;
2667#line 40
2668  __cil_tmp8 = (struct i2c_client *)0;
2669#line 40
2670  __cil_tmp9 = (unsigned long )__cil_tmp8;
2671#line 40
2672  __cil_tmp10 = __cil_tmp9 + 40;
2673#line 40
2674  __cil_tmp11 = (struct device *)__cil_tmp10;
2675#line 40
2676  __cil_tmp12 = (unsigned int )__cil_tmp11;
2677#line 40
2678  __cil_tmp13 = (char *)__mptr;
2679#line 40
2680  __cil_tmp14 = __cil_tmp13 - __cil_tmp12;
2681#line 40
2682  client = (struct i2c_client *)__cil_tmp14;
2683#line 43
2684  __cil_tmp15 = (struct i2c_client  const  *)client;
2685#line 43
2686  __cil_tmp16 = (u8 )0;
2687#line 43
2688  val = i2c_smbus_read_byte_data(__cil_tmp15, __cil_tmp16);
2689  }
2690#line 45
2691  if (val < 0) {
2692#line 46
2693    return ((ssize_t )val);
2694  } else {
2695
2696  }
2697  {
2698#line 47
2699  __cil_tmp17 = val & 3;
2700#line 47
2701  __cil_tmp18 = 2 * __cil_tmp17;
2702#line 47
2703  __cil_tmp19 = 1 << __cil_tmp18;
2704#line 47
2705  tmp___7 = sprintf(buf, "%d000\n", __cil_tmp19);
2706  }
2707#line 47
2708  return ((ssize_t )tmp___7);
2709}
2710}
2711#line 51 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
2712static ssize_t als_lux_input_data_show(struct device *dev , struct device_attribute *attr ,
2713                                       char *buf ) 
2714{ struct i2c_client *client ;
2715  struct device  const  *__mptr ;
2716  int ret_val ;
2717  int val ;
2718  unsigned long lux ;
2719  int temp ;
2720  int tmp___7 ;
2721  struct i2c_client *__cil_tmp11 ;
2722  unsigned long __cil_tmp12 ;
2723  unsigned long __cil_tmp13 ;
2724  struct device *__cil_tmp14 ;
2725  unsigned int __cil_tmp15 ;
2726  char *__cil_tmp16 ;
2727  char *__cil_tmp17 ;
2728  struct i2c_client  const  *__cil_tmp18 ;
2729  u8 __cil_tmp19 ;
2730  struct i2c_client  const  *__cil_tmp20 ;
2731  u8 __cil_tmp21 ;
2732  int __cil_tmp22 ;
2733  struct i2c_client  const  *__cil_tmp23 ;
2734  u8 __cil_tmp24 ;
2735  int __cil_tmp25 ;
2736  int __cil_tmp26 ;
2737  int __cil_tmp27 ;
2738  int __cil_tmp28 ;
2739  int __cil_tmp29 ;
2740  int __cil_tmp30 ;
2741
2742  {
2743  {
2744#line 54
2745  __mptr = (struct device  const  *)dev;
2746#line 54
2747  __cil_tmp11 = (struct i2c_client *)0;
2748#line 54
2749  __cil_tmp12 = (unsigned long )__cil_tmp11;
2750#line 54
2751  __cil_tmp13 = __cil_tmp12 + 40;
2752#line 54
2753  __cil_tmp14 = (struct device *)__cil_tmp13;
2754#line 54
2755  __cil_tmp15 = (unsigned int )__cil_tmp14;
2756#line 54
2757  __cil_tmp16 = (char *)__mptr;
2758#line 54
2759  __cil_tmp17 = __cil_tmp16 - __cil_tmp15;
2760#line 54
2761  client = (struct i2c_client *)__cil_tmp17;
2762#line 59
2763  pm_runtime_get_sync(dev);
2764#line 60
2765  msleep(100U);
2766#line 62
2767  mutex_lock(& mutex);
2768#line 63
2769  __cil_tmp18 = (struct i2c_client  const  *)client;
2770#line 63
2771  __cil_tmp19 = (u8 )2;
2772#line 63
2773  temp = i2c_smbus_read_byte_data(__cil_tmp18, __cil_tmp19);
2774  }
2775#line 64
2776  if (temp < 0) {
2777    {
2778#line 65
2779    pm_runtime_put_sync(dev);
2780#line 66
2781    mutex_unlock(& mutex);
2782    }
2783#line 67
2784    return ((ssize_t )temp);
2785  } else {
2786
2787  }
2788  {
2789#line 70
2790  __cil_tmp20 = (struct i2c_client  const  *)client;
2791#line 70
2792  __cil_tmp21 = (u8 )1;
2793#line 70
2794  ret_val = i2c_smbus_read_byte_data(__cil_tmp20, __cil_tmp21);
2795#line 71
2796  mutex_unlock(& mutex);
2797  }
2798#line 73
2799  if (ret_val < 0) {
2800    {
2801#line 74
2802    pm_runtime_put_sync(dev);
2803    }
2804#line 75
2805    return ((ssize_t )ret_val);
2806  } else {
2807
2808  }
2809  {
2810#line 78
2811  __cil_tmp22 = temp << 8;
2812#line 78
2813  ret_val = ret_val | __cil_tmp22;
2814#line 79
2815  __cil_tmp23 = (struct i2c_client  const  *)client;
2816#line 79
2817  __cil_tmp24 = (u8 )0;
2818#line 79
2819  val = i2c_smbus_read_byte_data(__cil_tmp23, __cil_tmp24);
2820#line 80
2821  pm_runtime_put_sync(dev);
2822  }
2823#line 81
2824  if (val < 0) {
2825#line 82
2826    return ((ssize_t )val);
2827  } else {
2828
2829  }
2830  {
2831#line 83
2832  __cil_tmp25 = val & 3;
2833#line 83
2834  __cil_tmp26 = 2 * __cil_tmp25;
2835#line 83
2836  __cil_tmp27 = 1 << __cil_tmp26;
2837#line 83
2838  __cil_tmp28 = __cil_tmp27 * 1000;
2839#line 83
2840  __cil_tmp29 = __cil_tmp28 * ret_val;
2841#line 83
2842  __cil_tmp30 = __cil_tmp29 / 65536;
2843#line 83
2844  lux = (unsigned long )__cil_tmp30;
2845#line 84
2846  tmp___7 = sprintf(buf, "%ld\n", lux);
2847  }
2848#line 84
2849  return ((ssize_t )tmp___7);
2850}
2851}
2852#line 87 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
2853static ssize_t als_sensing_range_store(struct device *dev , struct device_attribute *attr ,
2854                                       char const   *buf , size_t count ) 
2855{ struct i2c_client *client ;
2856  struct device  const  *__mptr ;
2857  int ret_val ;
2858  unsigned long val ;
2859  int tmp___7 ;
2860  struct i2c_client *__cil_tmp10 ;
2861  unsigned long __cil_tmp11 ;
2862  unsigned long __cil_tmp12 ;
2863  struct device *__cil_tmp13 ;
2864  unsigned int __cil_tmp14 ;
2865  char *__cil_tmp15 ;
2866  char *__cil_tmp16 ;
2867  unsigned long *__cil_tmp17 ;
2868  unsigned long __cil_tmp18 ;
2869  unsigned long *__cil_tmp19 ;
2870  unsigned long __cil_tmp20 ;
2871  unsigned long *__cil_tmp21 ;
2872  unsigned long __cil_tmp22 ;
2873  unsigned long *__cil_tmp23 ;
2874  unsigned long *__cil_tmp24 ;
2875  unsigned long __cil_tmp25 ;
2876  unsigned long *__cil_tmp26 ;
2877  unsigned long *__cil_tmp27 ;
2878  unsigned long __cil_tmp28 ;
2879  unsigned long *__cil_tmp29 ;
2880  unsigned long *__cil_tmp30 ;
2881  struct i2c_client  const  *__cil_tmp31 ;
2882  u8 __cil_tmp32 ;
2883  unsigned long *__cil_tmp33 ;
2884  unsigned long __cil_tmp34 ;
2885  unsigned long __cil_tmp35 ;
2886  unsigned long __cil_tmp36 ;
2887  unsigned long __cil_tmp37 ;
2888  struct i2c_client  const  *__cil_tmp38 ;
2889  u8 __cil_tmp39 ;
2890  u8 __cil_tmp40 ;
2891
2892  {
2893  {
2894#line 90
2895  __mptr = (struct device  const  *)dev;
2896#line 90
2897  __cil_tmp10 = (struct i2c_client *)0;
2898#line 90
2899  __cil_tmp11 = (unsigned long )__cil_tmp10;
2900#line 90
2901  __cil_tmp12 = __cil_tmp11 + 40;
2902#line 90
2903  __cil_tmp13 = (struct device *)__cil_tmp12;
2904#line 90
2905  __cil_tmp14 = (unsigned int )__cil_tmp13;
2906#line 90
2907  __cil_tmp15 = (char *)__mptr;
2908#line 90
2909  __cil_tmp16 = __cil_tmp15 - __cil_tmp14;
2910#line 90
2911  client = (struct i2c_client *)__cil_tmp16;
2912#line 94
2913  tmp___7 = (int )kstrtoul(buf, 10U, & val);
2914  }
2915#line 94
2916  if (tmp___7) {
2917#line 95
2918    return ((ssize_t )-22);
2919  } else {
2920
2921  }
2922  {
2923#line 96
2924  __cil_tmp17 = & val;
2925#line 96
2926  __cil_tmp18 = *__cil_tmp17;
2927#line 96
2928  if (__cil_tmp18 < 1UL) {
2929#line 97
2930    return ((ssize_t )-22);
2931  } else {
2932    {
2933#line 96
2934    __cil_tmp19 = & val;
2935#line 96
2936    __cil_tmp20 = *__cil_tmp19;
2937#line 96
2938    if (__cil_tmp20 > 64000UL) {
2939#line 97
2940      return ((ssize_t )-22);
2941    } else {
2942
2943    }
2944    }
2945  }
2946  }
2947  {
2948#line 100
2949  __cil_tmp21 = & val;
2950#line 100
2951  __cil_tmp22 = *__cil_tmp21;
2952#line 100
2953  if (__cil_tmp22 <= 1000UL) {
2954#line 101
2955    __cil_tmp23 = & val;
2956#line 101
2957    *__cil_tmp23 = 1UL;
2958  } else {
2959    {
2960#line 102
2961    __cil_tmp24 = & val;
2962#line 102
2963    __cil_tmp25 = *__cil_tmp24;
2964#line 102
2965    if (__cil_tmp25 <= 4000UL) {
2966#line 103
2967      __cil_tmp26 = & val;
2968#line 103
2969      *__cil_tmp26 = 2UL;
2970    } else {
2971      {
2972#line 104
2973      __cil_tmp27 = & val;
2974#line 104
2975      __cil_tmp28 = *__cil_tmp27;
2976#line 104
2977      if (__cil_tmp28 <= 16000UL) {
2978#line 105
2979        __cil_tmp29 = & val;
2980#line 105
2981        *__cil_tmp29 = 3UL;
2982      } else {
2983#line 107
2984        __cil_tmp30 = & val;
2985#line 107
2986        *__cil_tmp30 = 4UL;
2987      }
2988      }
2989    }
2990    }
2991  }
2992  }
2993  {
2994#line 109
2995  __cil_tmp31 = (struct i2c_client  const  *)client;
2996#line 109
2997  __cil_tmp32 = (u8 )0;
2998#line 109
2999  ret_val = i2c_smbus_read_byte_data(__cil_tmp31, __cil_tmp32);
3000  }
3001#line 110
3002  if (ret_val < 0) {
3003#line 111
3004    return ((ssize_t )ret_val);
3005  } else {
3006
3007  }
3008  {
3009#line 113
3010  ret_val = ret_val & 252;
3011#line 114
3012  __cil_tmp33 = & val;
3013#line 114
3014  __cil_tmp34 = *__cil_tmp33;
3015#line 114
3016  __cil_tmp35 = __cil_tmp34 - 1UL;
3017#line 114
3018  __cil_tmp36 = (unsigned long )ret_val;
3019#line 114
3020  __cil_tmp37 = __cil_tmp36 | __cil_tmp35;
3021#line 114
3022  ret_val = (int )__cil_tmp37;
3023#line 115
3024  __cil_tmp38 = (struct i2c_client  const  *)client;
3025#line 115
3026  __cil_tmp39 = (u8 )0;
3027#line 115
3028  __cil_tmp40 = (u8 )ret_val;
3029#line 115
3030  ret_val = i2c_smbus_write_byte_data(__cil_tmp38, __cil_tmp39, __cil_tmp40);
3031  }
3032#line 117
3033  if (ret_val < 0) {
3034#line 118
3035    return ((ssize_t )ret_val);
3036  } else {
3037
3038  }
3039#line 119
3040  return ((ssize_t )count);
3041}
3042}
3043#line 122 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3044static void als_set_power_state(struct i2c_client *client , int enable ) 
3045{ int ret_val ;
3046  struct i2c_client  const  *__cil_tmp4 ;
3047  u8 __cil_tmp5 ;
3048  struct i2c_client  const  *__cil_tmp6 ;
3049  u8 __cil_tmp7 ;
3050  u8 __cil_tmp8 ;
3051
3052  {
3053  {
3054#line 126
3055  __cil_tmp4 = (struct i2c_client  const  *)client;
3056#line 126
3057  __cil_tmp5 = (u8 )0;
3058#line 126
3059  ret_val = i2c_smbus_read_byte_data(__cil_tmp4, __cil_tmp5);
3060  }
3061#line 127
3062  if (ret_val < 0) {
3063#line 128
3064    return;
3065  } else {
3066
3067  }
3068#line 130
3069  if (enable) {
3070#line 131
3071    ret_val = ret_val | 128;
3072  } else {
3073#line 133
3074    ret_val = ret_val & 127;
3075  }
3076  {
3077#line 135
3078  __cil_tmp6 = (struct i2c_client  const  *)client;
3079#line 135
3080  __cil_tmp7 = (u8 )0;
3081#line 135
3082  __cil_tmp8 = (u8 )ret_val;
3083#line 135
3084  i2c_smbus_write_byte_data(__cil_tmp6, __cil_tmp7, __cil_tmp8);
3085  }
3086#line 136
3087  return;
3088}
3089}
3090#line 138 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3091static struct device_attribute dev_attr_lux0_sensor_range  =    {{"lux0_sensor_range", (umode_t )420}, & als_sensing_range_show, & als_sensing_range_store};
3092#line 140 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3093static struct device_attribute dev_attr_lux0_input  =    {{"lux0_input", (umode_t )292}, & als_lux_input_data_show, (ssize_t (*)(struct device *dev ,
3094                                                                           struct device_attribute *attr ,
3095                                                                           char const   *buf ,
3096                                                                           size_t count ))((void *)0)};
3097#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3098static struct attribute *mid_att_als[3]  = {      & dev_attr_lux0_sensor_range.attr,      & dev_attr_lux0_input.attr,      (struct attribute *)((void *)0)};
3099#line 148 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3100static struct attribute_group m_als_gr  =    {"isl29020", (umode_t (*)(struct kobject * , struct attribute * , int  ))0, mid_att_als};
3101#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3102static int als_set_default_config(struct i2c_client *client ) 
3103{ int retval ;
3104  struct i2c_client  const  *__cil_tmp3 ;
3105  u8 __cil_tmp4 ;
3106  u8 __cil_tmp5 ;
3107  unsigned long __cil_tmp6 ;
3108  unsigned long __cil_tmp7 ;
3109  struct device *__cil_tmp8 ;
3110  struct device  const  *__cil_tmp9 ;
3111
3112  {
3113  {
3114#line 157
3115  __cil_tmp3 = (struct i2c_client  const  *)client;
3116#line 157
3117  __cil_tmp4 = (u8 )0;
3118#line 157
3119  __cil_tmp5 = (u8 )192;
3120#line 157
3121  retval = i2c_smbus_write_byte_data(__cil_tmp3, __cil_tmp4, __cil_tmp5);
3122  }
3123#line 158
3124  if (retval < 0) {
3125    {
3126#line 159
3127    __cil_tmp6 = (unsigned long )client;
3128#line 159
3129    __cil_tmp7 = __cil_tmp6 + 40;
3130#line 159
3131    __cil_tmp8 = (struct device *)__cil_tmp7;
3132#line 159
3133    __cil_tmp9 = (struct device  const  *)__cil_tmp8;
3134#line 159
3135    dev_err(__cil_tmp9, "default write failed.");
3136    }
3137#line 160
3138    return (retval);
3139  } else {
3140
3141  }
3142#line 162
3143  return (0);
3144}
3145}
3146#line 165 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3147static int isl29020_probe(struct i2c_client *client , struct i2c_device_id  const  *id ) 
3148{ int res ;
3149  unsigned long __cil_tmp4 ;
3150  unsigned long __cil_tmp5 ;
3151  unsigned long __cil_tmp6 ;
3152  struct kobject *__cil_tmp7 ;
3153  struct attribute_group  const  *__cil_tmp8 ;
3154  unsigned long __cil_tmp9 ;
3155  unsigned long __cil_tmp10 ;
3156  struct device *__cil_tmp11 ;
3157  struct device  const  *__cil_tmp12 ;
3158  unsigned long __cil_tmp13 ;
3159  unsigned long __cil_tmp14 ;
3160  struct device *__cil_tmp15 ;
3161  struct device  const  *__cil_tmp16 ;
3162  unsigned long __cil_tmp17 ;
3163  unsigned long __cil_tmp18 ;
3164  unsigned long __cil_tmp19 ;
3165  unsigned long __cil_tmp20 ;
3166  char *__cil_tmp21 ;
3167  unsigned long __cil_tmp22 ;
3168  unsigned long __cil_tmp23 ;
3169  struct device *__cil_tmp24 ;
3170
3171  {
3172  {
3173#line 170
3174  res = als_set_default_config(client);
3175  }
3176#line 171
3177  if (res < 0) {
3178#line 172
3179    return (res);
3180  } else {
3181
3182  }
3183  {
3184#line 174
3185  __cil_tmp4 = 40 + 16;
3186#line 174
3187  __cil_tmp5 = (unsigned long )client;
3188#line 174
3189  __cil_tmp6 = __cil_tmp5 + __cil_tmp4;
3190#line 174
3191  __cil_tmp7 = (struct kobject *)__cil_tmp6;
3192#line 174
3193  __cil_tmp8 = (struct attribute_group  const  *)(& m_als_gr);
3194#line 174
3195  res = (int )sysfs_create_group(__cil_tmp7, __cil_tmp8);
3196  }
3197#line 175
3198  if (res) {
3199    {
3200#line 176
3201    __cil_tmp9 = (unsigned long )client;
3202#line 176
3203    __cil_tmp10 = __cil_tmp9 + 40;
3204#line 176
3205    __cil_tmp11 = (struct device *)__cil_tmp10;
3206#line 176
3207    __cil_tmp12 = (struct device  const  *)__cil_tmp11;
3208#line 176
3209    dev_err(__cil_tmp12, "isl29020: device create file failed\n");
3210    }
3211#line 177
3212    return (res);
3213  } else {
3214
3215  }
3216  {
3217#line 179
3218  __cil_tmp13 = (unsigned long )client;
3219#line 179
3220  __cil_tmp14 = __cil_tmp13 + 40;
3221#line 179
3222  __cil_tmp15 = (struct device *)__cil_tmp14;
3223#line 179
3224  __cil_tmp16 = (struct device  const  *)__cil_tmp15;
3225#line 179
3226  __cil_tmp17 = 0 * 1UL;
3227#line 179
3228  __cil_tmp18 = 4 + __cil_tmp17;
3229#line 179
3230  __cil_tmp19 = (unsigned long )client;
3231#line 179
3232  __cil_tmp20 = __cil_tmp19 + __cil_tmp18;
3233#line 179
3234  __cil_tmp21 = (char *)__cil_tmp20;
3235#line 179
3236  _dev_info(__cil_tmp16, "%s isl29020: ALS chip found\n", __cil_tmp21);
3237#line 180
3238  als_set_power_state(client, 0);
3239#line 181
3240  __cil_tmp22 = (unsigned long )client;
3241#line 181
3242  __cil_tmp23 = __cil_tmp22 + 40;
3243#line 181
3244  __cil_tmp24 = (struct device *)__cil_tmp23;
3245#line 181
3246  pm_runtime_enable(__cil_tmp24);
3247  }
3248#line 182
3249  return (res);
3250}
3251}
3252#line 185 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3253static int isl29020_remove(struct i2c_client *client ) 
3254{ unsigned long __cil_tmp2 ;
3255  unsigned long __cil_tmp3 ;
3256  unsigned long __cil_tmp4 ;
3257  struct kobject *__cil_tmp5 ;
3258  struct attribute_group  const  *__cil_tmp6 ;
3259
3260  {
3261  {
3262#line 187
3263  __cil_tmp2 = 40 + 16;
3264#line 187
3265  __cil_tmp3 = (unsigned long )client;
3266#line 187
3267  __cil_tmp4 = __cil_tmp3 + __cil_tmp2;
3268#line 187
3269  __cil_tmp5 = (struct kobject *)__cil_tmp4;
3270#line 187
3271  __cil_tmp6 = (struct attribute_group  const  *)(& m_als_gr);
3272#line 187
3273  sysfs_remove_group(__cil_tmp5, __cil_tmp6);
3274  }
3275#line 188
3276  return (0);
3277}
3278}
3279#line 191 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3280static struct i2c_device_id isl29020_id[1]  = {      {{(char )'i', (char )'s', (char )'l', (char )'2', (char )'9', (char )'0', (char )'2',
3281       (char )'0', (char )'\000', (char)0, (char)0, (char)0, (char)0, (char)0, (char)0,
3282       (char)0, (char)0, (char)0, (char)0, (char)0}, (kernel_ulong_t )0}};
3283#line 196
3284extern struct i2c_device_id  const  __mod_i2c_device_table  __attribute__((__unused__,
3285__alias__("isl29020_id"))) ;
3286#line 200 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3287static int isl29020_runtime_suspend(struct device *dev ) 
3288{ struct i2c_client *client ;
3289  struct device  const  *__mptr ;
3290  struct i2c_client *__cil_tmp4 ;
3291  unsigned long __cil_tmp5 ;
3292  unsigned long __cil_tmp6 ;
3293  struct device *__cil_tmp7 ;
3294  unsigned int __cil_tmp8 ;
3295  char *__cil_tmp9 ;
3296  char *__cil_tmp10 ;
3297
3298  {
3299  {
3300#line 202
3301  __mptr = (struct device  const  *)dev;
3302#line 202
3303  __cil_tmp4 = (struct i2c_client *)0;
3304#line 202
3305  __cil_tmp5 = (unsigned long )__cil_tmp4;
3306#line 202
3307  __cil_tmp6 = __cil_tmp5 + 40;
3308#line 202
3309  __cil_tmp7 = (struct device *)__cil_tmp6;
3310#line 202
3311  __cil_tmp8 = (unsigned int )__cil_tmp7;
3312#line 202
3313  __cil_tmp9 = (char *)__mptr;
3314#line 202
3315  __cil_tmp10 = __cil_tmp9 - __cil_tmp8;
3316#line 202
3317  client = (struct i2c_client *)__cil_tmp10;
3318#line 203
3319  als_set_power_state(client, 0);
3320  }
3321#line 204
3322  return (0);
3323}
3324}
3325#line 207 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3326static int isl29020_runtime_resume(struct device *dev ) 
3327{ struct i2c_client *client ;
3328  struct device  const  *__mptr ;
3329  struct i2c_client *__cil_tmp4 ;
3330  unsigned long __cil_tmp5 ;
3331  unsigned long __cil_tmp6 ;
3332  struct device *__cil_tmp7 ;
3333  unsigned int __cil_tmp8 ;
3334  char *__cil_tmp9 ;
3335  char *__cil_tmp10 ;
3336
3337  {
3338  {
3339#line 209
3340  __mptr = (struct device  const  *)dev;
3341#line 209
3342  __cil_tmp4 = (struct i2c_client *)0;
3343#line 209
3344  __cil_tmp5 = (unsigned long )__cil_tmp4;
3345#line 209
3346  __cil_tmp6 = __cil_tmp5 + 40;
3347#line 209
3348  __cil_tmp7 = (struct device *)__cil_tmp6;
3349#line 209
3350  __cil_tmp8 = (unsigned int )__cil_tmp7;
3351#line 209
3352  __cil_tmp9 = (char *)__mptr;
3353#line 209
3354  __cil_tmp10 = __cil_tmp9 - __cil_tmp8;
3355#line 209
3356  client = (struct i2c_client *)__cil_tmp10;
3357#line 210
3358  als_set_power_state(client, 1);
3359  }
3360#line 211
3361  return (0);
3362}
3363}
3364#line 214 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3365static struct dev_pm_ops  const  isl29020_pm_ops  = 
3366#line 214
3367     {(int (*)(struct device *dev ))0, (void (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
3368    (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
3369    (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
3370    (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
3371    (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
3372    (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
3373    (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0, & isl29020_runtime_suspend,
3374    & isl29020_runtime_resume, (int (*)(struct device *dev ))0};
3375#line 224 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3376static struct i2c_driver isl29020_driver  = 
3377#line 224
3378     {0U, (int (*)(struct i2c_adapter * ))0, (int (*)(struct i2c_adapter * ))0, & isl29020_probe,
3379    & isl29020_remove, (void (*)(struct i2c_client * ))0, (int (*)(struct i2c_client * ,
3380                                                                   pm_message_t mesg ))0,
3381    (int (*)(struct i2c_client * ))0, (void (*)(struct i2c_client * , unsigned int data ))0,
3382    (int (*)(struct i2c_client *client , unsigned int cmd , void *arg ))0, {"isl29020",
3383                                                                            (struct bus_type *)0,
3384                                                                            (struct module *)0,
3385                                                                            (char const   *)0,
3386                                                                            (_Bool)0,
3387                                                                            (struct of_device_id  const  *)0,
3388                                                                            (int (*)(struct device *dev ))0,
3389                                                                            (int (*)(struct device *dev ))0,
3390                                                                            (void (*)(struct device *dev ))0,
3391                                                                            (int (*)(struct device *dev ,
3392                                                                                     pm_message_t state ))0,
3393                                                                            (int (*)(struct device *dev ))0,
3394                                                                            (struct attribute_group  const  **)0,
3395                                                                            & isl29020_pm_ops,
3396                                                                            (struct driver_private *)0},
3397    (struct i2c_device_id  const  *)(isl29020_id), (int (*)(struct i2c_client * ,
3398                                                            struct i2c_board_info * ))0,
3399    (unsigned short const   *)0, {(struct list_head *)0, (struct list_head *)0}};
3400#line 234
3401static int isl29020_driver_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
3402#line 234 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3403static int isl29020_driver_init(void) 
3404{ int tmp___7 ;
3405
3406  {
3407  {
3408#line 234
3409  tmp___7 = i2c_register_driver(& __this_module, & isl29020_driver);
3410  }
3411#line 234
3412  return (tmp___7);
3413}
3414}
3415#line 234 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3416int init_module(void) 
3417{ int tmp___7 ;
3418
3419  {
3420  {
3421#line 234
3422  tmp___7 = isl29020_driver_init();
3423  }
3424#line 234
3425  return (tmp___7);
3426}
3427}
3428#line 234
3429static void isl29020_driver_exit(void)  __attribute__((__section__(".exit.text"),
3430__no_instrument_function__)) ;
3431#line 234 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3432static void isl29020_driver_exit(void) 
3433{ 
3434
3435  {
3436  {
3437#line 234
3438  i2c_del_driver(& isl29020_driver);
3439  }
3440#line 234
3441  return;
3442}
3443}
3444#line 234 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3445void cleanup_module(void) 
3446{ 
3447
3448  {
3449  {
3450#line 234
3451  isl29020_driver_exit();
3452  }
3453#line 234
3454  return;
3455}
3456}
3457#line 236 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3458static char const   __mod_author236[47]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3459__aligned__(1)))  = 
3460#line 236
3461  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
3462        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'K', 
3463        (char const   )'a',      (char const   )'l',      (char const   )'h',      (char const   )'a', 
3464        (char const   )'n',      (char const   )' ',      (char const   )'T',      (char const   )'r', 
3465        (char const   )'i',      (char const   )'s',      (char const   )'a',      (char const   )'l', 
3466        (char const   )' ',      (char const   )'<',      (char const   )'k',      (char const   )'a', 
3467        (char const   )'l',      (char const   )'h',      (char const   )'a',      (char const   )'n', 
3468        (char const   )'.',      (char const   )'t',      (char const   )'r',      (char const   )'i', 
3469        (char const   )'s',      (char const   )'a',      (char const   )'l',      (char const   )'@', 
3470        (char const   )'i',      (char const   )'n',      (char const   )'t',      (char const   )'e', 
3471        (char const   )'l',      (char const   )'.',      (char const   )'c',      (char const   )'o', 
3472        (char const   )'m',      (char const   )'>',      (char const   )'\000'};
3473#line 237 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3474static char const   __mod_description237[41]  __attribute__((__used__, __unused__,
3475__section__(".modinfo"), __aligned__(1)))  = 
3476#line 237
3477  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
3478        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
3479        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
3480        (char const   )'I',      (char const   )'n',      (char const   )'t',      (char const   )'e', 
3481        (char const   )'r',      (char const   )'s',      (char const   )'i',      (char const   )'l', 
3482        (char const   )' ',      (char const   )'i',      (char const   )'s',      (char const   )'l', 
3483        (char const   )'2',      (char const   )'9',      (char const   )'0',      (char const   )'2', 
3484        (char const   )'0',      (char const   )' ',      (char const   )'A',      (char const   )'L', 
3485        (char const   )'S',      (char const   )' ',      (char const   )'D',      (char const   )'r', 
3486        (char const   )'i',      (char const   )'v',      (char const   )'e',      (char const   )'r', 
3487        (char const   )'\000'};
3488#line 238 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3489static char const   __mod_license238[15]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3490__aligned__(1)))  = 
3491#line 238
3492  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
3493        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
3494        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )' ', 
3495        (char const   )'v',      (char const   )'2',      (char const   )'\000'};
3496#line 256
3497void ldv_check_final_state(void) ;
3498#line 259
3499extern void ldv_check_return_value(int res ) ;
3500#line 262
3501extern void ldv_initialize(void) ;
3502#line 265
3503extern int __VERIFIER_nondet_int(void) ;
3504#line 268 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3505int LDV_IN_INTERRUPT  ;
3506#line 309 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3507static int res_isl29020_probe_5  ;
3508#line 320 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3509static int res_isl29020_remove_6  ;
3510#line 271 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3511void main(void) 
3512{ struct device *var_group1 ;
3513  struct i2c_client *var_group2 ;
3514  struct i2c_device_id  const  *var_isl29020_probe_5_p1 ;
3515  int ldv_s_isl29020_driver_i2c_driver ;
3516  int tmp___7 ;
3517  int tmp___8 ;
3518  int __cil_tmp7 ;
3519
3520  {
3521  {
3522#line 335
3523  LDV_IN_INTERRUPT = 1;
3524#line 344
3525  ldv_initialize();
3526#line 347
3527  ldv_s_isl29020_driver_i2c_driver = 0;
3528  }
3529  {
3530#line 350
3531  while (1) {
3532    while_continue: /* CIL Label */ ;
3533    {
3534#line 350
3535    tmp___8 = __VERIFIER_nondet_int();
3536    }
3537#line 350
3538    if (tmp___8) {
3539
3540    } else {
3541      {
3542#line 350
3543      __cil_tmp7 = ldv_s_isl29020_driver_i2c_driver == 0;
3544#line 350
3545      if (! __cil_tmp7) {
3546
3547      } else {
3548#line 350
3549        goto while_break;
3550      }
3551      }
3552    }
3553    {
3554#line 354
3555    tmp___7 = __VERIFIER_nondet_int();
3556    }
3557#line 356
3558    if (tmp___7 == 0) {
3559#line 356
3560      goto case_0;
3561    } else
3562#line 380
3563    if (tmp___7 == 1) {
3564#line 380
3565      goto case_1;
3566    } else
3567#line 404
3568    if (tmp___7 == 2) {
3569#line 404
3570      goto case_2;
3571    } else
3572#line 430
3573    if (tmp___7 == 3) {
3574#line 430
3575      goto case_3;
3576    } else {
3577      {
3578#line 456
3579      goto switch_default;
3580#line 354
3581      if (0) {
3582        case_0: /* CIL Label */ 
3583        {
3584#line 366
3585        isl29020_runtime_suspend(var_group1);
3586        }
3587#line 379
3588        goto switch_break;
3589        case_1: /* CIL Label */ 
3590        {
3591#line 390
3592        isl29020_runtime_resume(var_group1);
3593        }
3594#line 403
3595        goto switch_break;
3596        case_2: /* CIL Label */ 
3597#line 407
3598        if (ldv_s_isl29020_driver_i2c_driver == 0) {
3599          {
3600#line 412
3601          res_isl29020_probe_5 = isl29020_probe(var_group2, var_isl29020_probe_5_p1);
3602#line 413
3603          ldv_check_return_value(res_isl29020_probe_5);
3604          }
3605#line 414
3606          if (res_isl29020_probe_5) {
3607#line 415
3608            goto ldv_module_exit;
3609          } else {
3610
3611          }
3612#line 423
3613          ldv_s_isl29020_driver_i2c_driver = ldv_s_isl29020_driver_i2c_driver + 1;
3614        } else {
3615
3616        }
3617#line 429
3618        goto switch_break;
3619        case_3: /* CIL Label */ 
3620#line 433
3621        if (ldv_s_isl29020_driver_i2c_driver == 1) {
3622          {
3623#line 438
3624          res_isl29020_remove_6 = isl29020_remove(var_group2);
3625#line 439
3626          ldv_check_return_value(res_isl29020_remove_6);
3627          }
3628#line 440
3629          if (res_isl29020_remove_6) {
3630#line 441
3631            goto ldv_module_exit;
3632          } else {
3633
3634          }
3635#line 449
3636          ldv_s_isl29020_driver_i2c_driver = 0;
3637        } else {
3638
3639        }
3640#line 455
3641        goto switch_break;
3642        switch_default: /* CIL Label */ 
3643#line 456
3644        goto switch_break;
3645      } else {
3646        switch_break: /* CIL Label */ ;
3647      }
3648      }
3649    }
3650  }
3651  while_break: /* CIL Label */ ;
3652  }
3653  ldv_module_exit: 
3654  {
3655#line 465
3656  ldv_check_final_state();
3657  }
3658#line 468
3659  return;
3660}
3661}
3662#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3663void ldv_blast_assert(void) 
3664{ 
3665
3666  {
3667  ERROR: 
3668#line 6
3669  goto ERROR;
3670}
3671}
3672#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3673extern int __VERIFIER_nondet_int(void) ;
3674#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3675int ldv_mutex  =    1;
3676#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3677int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
3678{ int nondetermined ;
3679
3680  {
3681#line 29
3682  if (ldv_mutex == 1) {
3683
3684  } else {
3685    {
3686#line 29
3687    ldv_blast_assert();
3688    }
3689  }
3690  {
3691#line 32
3692  nondetermined = __VERIFIER_nondet_int();
3693  }
3694#line 35
3695  if (nondetermined) {
3696#line 38
3697    ldv_mutex = 2;
3698#line 40
3699    return (0);
3700  } else {
3701#line 45
3702    return (-4);
3703  }
3704}
3705}
3706#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3707int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
3708{ int nondetermined ;
3709
3710  {
3711#line 57
3712  if (ldv_mutex == 1) {
3713
3714  } else {
3715    {
3716#line 57
3717    ldv_blast_assert();
3718    }
3719  }
3720  {
3721#line 60
3722  nondetermined = __VERIFIER_nondet_int();
3723  }
3724#line 63
3725  if (nondetermined) {
3726#line 66
3727    ldv_mutex = 2;
3728#line 68
3729    return (0);
3730  } else {
3731#line 73
3732    return (-4);
3733  }
3734}
3735}
3736#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3737int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
3738{ int atomic_value_after_dec ;
3739
3740  {
3741#line 83
3742  if (ldv_mutex == 1) {
3743
3744  } else {
3745    {
3746#line 83
3747    ldv_blast_assert();
3748    }
3749  }
3750  {
3751#line 86
3752  atomic_value_after_dec = __VERIFIER_nondet_int();
3753  }
3754#line 89
3755  if (atomic_value_after_dec == 0) {
3756#line 92
3757    ldv_mutex = 2;
3758#line 94
3759    return (1);
3760  } else {
3761
3762  }
3763#line 98
3764  return (0);
3765}
3766}
3767#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3768void mutex_lock(struct mutex *lock ) 
3769{ 
3770
3771  {
3772#line 108
3773  if (ldv_mutex == 1) {
3774
3775  } else {
3776    {
3777#line 108
3778    ldv_blast_assert();
3779    }
3780  }
3781#line 110
3782  ldv_mutex = 2;
3783#line 111
3784  return;
3785}
3786}
3787#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3788int mutex_trylock(struct mutex *lock ) 
3789{ int nondetermined ;
3790
3791  {
3792#line 121
3793  if (ldv_mutex == 1) {
3794
3795  } else {
3796    {
3797#line 121
3798    ldv_blast_assert();
3799    }
3800  }
3801  {
3802#line 124
3803  nondetermined = __VERIFIER_nondet_int();
3804  }
3805#line 127
3806  if (nondetermined) {
3807#line 130
3808    ldv_mutex = 2;
3809#line 132
3810    return (1);
3811  } else {
3812#line 137
3813    return (0);
3814  }
3815}
3816}
3817#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3818void mutex_unlock(struct mutex *lock ) 
3819{ 
3820
3821  {
3822#line 147
3823  if (ldv_mutex == 2) {
3824
3825  } else {
3826    {
3827#line 147
3828    ldv_blast_assert();
3829    }
3830  }
3831#line 149
3832  ldv_mutex = 1;
3833#line 150
3834  return;
3835}
3836}
3837#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3838void ldv_check_final_state(void) 
3839{ 
3840
3841  {
3842#line 156
3843  if (ldv_mutex == 1) {
3844
3845  } else {
3846    {
3847#line 156
3848    ldv_blast_assert();
3849    }
3850  }
3851#line 157
3852  return;
3853}
3854}
3855#line 477 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4887/dscv_tempdir/dscv/ri/32_1/drivers/misc/isl29020.c.common.c"
3856long s__builtin_expect(long val , long res ) 
3857{ 
3858
3859  {
3860#line 478
3861  return (val);
3862}
3863}