Showing error 593

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