Showing error 1184

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