Showing error 591

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