Showing error 586

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--regulator--gpio-regulator.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 5179
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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