Showing error 594

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