Showing error 491

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