Showing error 312

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