1
2
3
4#line 23 "include/asm-generic/int-ll64.h"
5typedef unsigned short __u16;
6#line 26 "include/asm-generic/int-ll64.h"
7typedef unsigned int __u32;
8#line 30 "include/asm-generic/int-ll64.h"
9typedef unsigned long long __u64;
10#line 43 "include/asm-generic/int-ll64.h"
11typedef unsigned char u8;
12#line 45 "include/asm-generic/int-ll64.h"
13typedef short s16;
14#line 46 "include/asm-generic/int-ll64.h"
15typedef unsigned short u16;
16#line 48 "include/asm-generic/int-ll64.h"
17typedef int s32;
18#line 49 "include/asm-generic/int-ll64.h"
19typedef unsigned int u32;
20#line 51 "include/asm-generic/int-ll64.h"
21typedef long long s64;
22#line 52 "include/asm-generic/int-ll64.h"
23typedef unsigned long long u64;
24#line 14 "include/asm-generic/posix_types.h"
25typedef long __kernel_long_t;
26#line 15 "include/asm-generic/posix_types.h"
27typedef unsigned long __kernel_ulong_t;
28#line 75 "include/asm-generic/posix_types.h"
29typedef __kernel_ulong_t __kernel_size_t;
30#line 76 "include/asm-generic/posix_types.h"
31typedef __kernel_long_t __kernel_ssize_t;
32#line 91 "include/asm-generic/posix_types.h"
33typedef long long __kernel_loff_t;
34#line 21 "include/linux/types.h"
35typedef __u32 __kernel_dev_t;
36#line 24 "include/linux/types.h"
37typedef __kernel_dev_t dev_t;
38#line 27 "include/linux/types.h"
39typedef unsigned short umode_t;
40#line 38 "include/linux/types.h"
41typedef _Bool bool;
42#line 54 "include/linux/types.h"
43typedef __kernel_loff_t loff_t;
44#line 63 "include/linux/types.h"
45typedef __kernel_size_t size_t;
46#line 68 "include/linux/types.h"
47typedef __kernel_ssize_t ssize_t;
48#line 202 "include/linux/types.h"
49typedef unsigned int gfp_t;
50#line 206 "include/linux/types.h"
51typedef u64 phys_addr_t;
52#line 211 "include/linux/types.h"
53typedef phys_addr_t resource_size_t;
54#line 221 "include/linux/types.h"
55struct __anonstruct_atomic_t_6 {
56 int counter ;
57};
58#line 221 "include/linux/types.h"
59typedef struct __anonstruct_atomic_t_6 atomic_t;
60#line 226 "include/linux/types.h"
61struct __anonstruct_atomic64_t_7 {
62 long counter ;
63};
64#line 226 "include/linux/types.h"
65typedef struct __anonstruct_atomic64_t_7 atomic64_t;
66#line 227 "include/linux/types.h"
67struct list_head {
68 struct list_head *next ;
69 struct list_head *prev ;
70};
71#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
72struct module;
73#line 55
74struct module;
75#line 146 "include/linux/init.h"
76typedef void (*ctor_fn_t)(void);
77#line 305 "include/linux/printk.h"
78struct _ddebug {
79 char const *modname ;
80 char const *function ;
81 char const *filename ;
82 char const *format ;
83 unsigned int lineno : 18 ;
84 unsigned char flags ;
85};
86#line 46 "include/linux/dynamic_debug.h"
87struct device;
88#line 46
89struct device;
90#line 57
91struct completion;
92#line 57
93struct completion;
94#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
95struct page;
96#line 58
97struct page;
98#line 26 "include/asm-generic/getorder.h"
99struct task_struct;
100#line 26
101struct task_struct;
102#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
103struct file;
104#line 290
105struct file;
106#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
107struct arch_spinlock;
108#line 327
109struct arch_spinlock;
110#line 306 "include/linux/bitmap.h"
111struct bug_entry {
112 int bug_addr_disp ;
113 int file_disp ;
114 unsigned short line ;
115 unsigned short flags ;
116};
117#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
118struct static_key;
119#line 234
120struct static_key;
121#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
122struct kmem_cache;
123#line 23 "include/asm-generic/atomic-long.h"
124typedef atomic64_t atomic_long_t;
125#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
126typedef u16 __ticket_t;
127#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
128typedef u32 __ticketpair_t;
129#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
130struct __raw_tickets {
131 __ticket_t head ;
132 __ticket_t tail ;
133};
134#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
135union __anonunion_ldv_5907_29 {
136 __ticketpair_t head_tail ;
137 struct __raw_tickets tickets ;
138};
139#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
140struct arch_spinlock {
141 union __anonunion_ldv_5907_29 ldv_5907 ;
142};
143#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
144typedef struct arch_spinlock arch_spinlock_t;
145#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
146struct __anonstruct_ldv_5914_31 {
147 u32 read ;
148 s32 write ;
149};
150#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
151union __anonunion_arch_rwlock_t_30 {
152 s64 lock ;
153 struct __anonstruct_ldv_5914_31 ldv_5914 ;
154};
155#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
156typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
157#line 34
158struct lockdep_map;
159#line 34
160struct lockdep_map;
161#line 55 "include/linux/debug_locks.h"
162struct stack_trace {
163 unsigned int nr_entries ;
164 unsigned int max_entries ;
165 unsigned long *entries ;
166 int skip ;
167};
168#line 26 "include/linux/stacktrace.h"
169struct lockdep_subclass_key {
170 char __one_byte ;
171};
172#line 53 "include/linux/lockdep.h"
173struct lock_class_key {
174 struct lockdep_subclass_key subkeys[8U] ;
175};
176#line 59 "include/linux/lockdep.h"
177struct lock_class {
178 struct list_head hash_entry ;
179 struct list_head lock_entry ;
180 struct lockdep_subclass_key *key ;
181 unsigned int subclass ;
182 unsigned int dep_gen_id ;
183 unsigned long usage_mask ;
184 struct stack_trace usage_traces[13U] ;
185 struct list_head locks_after ;
186 struct list_head locks_before ;
187 unsigned int version ;
188 unsigned long ops ;
189 char const *name ;
190 int name_version ;
191 unsigned long contention_point[4U] ;
192 unsigned long contending_point[4U] ;
193};
194#line 144 "include/linux/lockdep.h"
195struct lockdep_map {
196 struct lock_class_key *key ;
197 struct lock_class *class_cache[2U] ;
198 char const *name ;
199 int cpu ;
200 unsigned long ip ;
201};
202#line 556 "include/linux/lockdep.h"
203struct raw_spinlock {
204 arch_spinlock_t raw_lock ;
205 unsigned int magic ;
206 unsigned int owner_cpu ;
207 void *owner ;
208 struct lockdep_map dep_map ;
209};
210#line 32 "include/linux/spinlock_types.h"
211typedef struct raw_spinlock raw_spinlock_t;
212#line 33 "include/linux/spinlock_types.h"
213struct __anonstruct_ldv_6122_33 {
214 u8 __padding[24U] ;
215 struct lockdep_map dep_map ;
216};
217#line 33 "include/linux/spinlock_types.h"
218union __anonunion_ldv_6123_32 {
219 struct raw_spinlock rlock ;
220 struct __anonstruct_ldv_6122_33 ldv_6122 ;
221};
222#line 33 "include/linux/spinlock_types.h"
223struct spinlock {
224 union __anonunion_ldv_6123_32 ldv_6123 ;
225};
226#line 76 "include/linux/spinlock_types.h"
227typedef struct spinlock spinlock_t;
228#line 23 "include/linux/rwlock_types.h"
229struct __anonstruct_rwlock_t_34 {
230 arch_rwlock_t raw_lock ;
231 unsigned int magic ;
232 unsigned int owner_cpu ;
233 void *owner ;
234 struct lockdep_map dep_map ;
235};
236#line 23 "include/linux/rwlock_types.h"
237typedef struct __anonstruct_rwlock_t_34 rwlock_t;
238#line 48 "include/linux/wait.h"
239struct __wait_queue_head {
240 spinlock_t lock ;
241 struct list_head task_list ;
242};
243#line 53 "include/linux/wait.h"
244typedef struct __wait_queue_head wait_queue_head_t;
245#line 670 "include/linux/mmzone.h"
246struct mutex {
247 atomic_t count ;
248 spinlock_t wait_lock ;
249 struct list_head wait_list ;
250 struct task_struct *owner ;
251 char const *name ;
252 void *magic ;
253 struct lockdep_map dep_map ;
254};
255#line 171 "include/linux/mutex.h"
256struct rw_semaphore;
257#line 171
258struct rw_semaphore;
259#line 172 "include/linux/mutex.h"
260struct rw_semaphore {
261 long count ;
262 raw_spinlock_t wait_lock ;
263 struct list_head wait_list ;
264 struct lockdep_map dep_map ;
265};
266#line 128 "include/linux/rwsem.h"
267struct completion {
268 unsigned int done ;
269 wait_queue_head_t wait ;
270};
271#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
272struct resource {
273 resource_size_t start ;
274 resource_size_t end ;
275 char const *name ;
276 unsigned long flags ;
277 struct resource *parent ;
278 struct resource *sibling ;
279 struct resource *child ;
280};
281#line 312 "include/linux/jiffies.h"
282union ktime {
283 s64 tv64 ;
284};
285#line 59 "include/linux/ktime.h"
286typedef union ktime ktime_t;
287#line 341
288struct tvec_base;
289#line 341
290struct tvec_base;
291#line 342 "include/linux/ktime.h"
292struct timer_list {
293 struct list_head entry ;
294 unsigned long expires ;
295 struct tvec_base *base ;
296 void (*function)(unsigned long ) ;
297 unsigned long data ;
298 int slack ;
299 int start_pid ;
300 void *start_site ;
301 char start_comm[16U] ;
302 struct lockdep_map lockdep_map ;
303};
304#line 302 "include/linux/timer.h"
305struct work_struct;
306#line 302
307struct work_struct;
308#line 45 "include/linux/workqueue.h"
309struct work_struct {
310 atomic_long_t data ;
311 struct list_head entry ;
312 void (*func)(struct work_struct * ) ;
313 struct lockdep_map lockdep_map ;
314};
315#line 46 "include/linux/pm.h"
316struct pm_message {
317 int event ;
318};
319#line 52 "include/linux/pm.h"
320typedef struct pm_message pm_message_t;
321#line 53 "include/linux/pm.h"
322struct dev_pm_ops {
323 int (*prepare)(struct device * ) ;
324 void (*complete)(struct device * ) ;
325 int (*suspend)(struct device * ) ;
326 int (*resume)(struct device * ) ;
327 int (*freeze)(struct device * ) ;
328 int (*thaw)(struct device * ) ;
329 int (*poweroff)(struct device * ) ;
330 int (*restore)(struct device * ) ;
331 int (*suspend_late)(struct device * ) ;
332 int (*resume_early)(struct device * ) ;
333 int (*freeze_late)(struct device * ) ;
334 int (*thaw_early)(struct device * ) ;
335 int (*poweroff_late)(struct device * ) ;
336 int (*restore_early)(struct device * ) ;
337 int (*suspend_noirq)(struct device * ) ;
338 int (*resume_noirq)(struct device * ) ;
339 int (*freeze_noirq)(struct device * ) ;
340 int (*thaw_noirq)(struct device * ) ;
341 int (*poweroff_noirq)(struct device * ) ;
342 int (*restore_noirq)(struct device * ) ;
343 int (*runtime_suspend)(struct device * ) ;
344 int (*runtime_resume)(struct device * ) ;
345 int (*runtime_idle)(struct device * ) ;
346};
347#line 289
348enum rpm_status {
349 RPM_ACTIVE = 0,
350 RPM_RESUMING = 1,
351 RPM_SUSPENDED = 2,
352 RPM_SUSPENDING = 3
353} ;
354#line 296
355enum rpm_request {
356 RPM_REQ_NONE = 0,
357 RPM_REQ_IDLE = 1,
358 RPM_REQ_SUSPEND = 2,
359 RPM_REQ_AUTOSUSPEND = 3,
360 RPM_REQ_RESUME = 4
361} ;
362#line 304
363struct wakeup_source;
364#line 304
365struct wakeup_source;
366#line 494 "include/linux/pm.h"
367struct pm_subsys_data {
368 spinlock_t lock ;
369 unsigned int refcount ;
370};
371#line 499
372struct dev_pm_qos_request;
373#line 499
374struct pm_qos_constraints;
375#line 499 "include/linux/pm.h"
376struct dev_pm_info {
377 pm_message_t power_state ;
378 unsigned char can_wakeup : 1 ;
379 unsigned char async_suspend : 1 ;
380 bool is_prepared ;
381 bool is_suspended ;
382 bool ignore_children ;
383 spinlock_t lock ;
384 struct list_head entry ;
385 struct completion completion ;
386 struct wakeup_source *wakeup ;
387 bool wakeup_path ;
388 struct timer_list suspend_timer ;
389 unsigned long timer_expires ;
390 struct work_struct work ;
391 wait_queue_head_t wait_queue ;
392 atomic_t usage_count ;
393 atomic_t child_count ;
394 unsigned char disable_depth : 3 ;
395 unsigned char idle_notification : 1 ;
396 unsigned char request_pending : 1 ;
397 unsigned char deferred_resume : 1 ;
398 unsigned char run_wake : 1 ;
399 unsigned char runtime_auto : 1 ;
400 unsigned char no_callbacks : 1 ;
401 unsigned char irq_safe : 1 ;
402 unsigned char use_autosuspend : 1 ;
403 unsigned char timer_autosuspends : 1 ;
404 enum rpm_request request ;
405 enum rpm_status runtime_status ;
406 int runtime_error ;
407 int autosuspend_delay ;
408 unsigned long last_busy ;
409 unsigned long active_jiffies ;
410 unsigned long suspended_jiffies ;
411 unsigned long accounting_timestamp ;
412 ktime_t suspend_time ;
413 s64 max_time_suspended_ns ;
414 struct dev_pm_qos_request *pq_req ;
415 struct pm_subsys_data *subsys_data ;
416 struct pm_qos_constraints *constraints ;
417};
418#line 558 "include/linux/pm.h"
419struct dev_pm_domain {
420 struct dev_pm_ops ops ;
421};
422#line 18 "include/asm-generic/pci_iomap.h"
423struct vm_area_struct;
424#line 18
425struct vm_area_struct;
426#line 18 "include/linux/elf.h"
427typedef __u64 Elf64_Addr;
428#line 19 "include/linux/elf.h"
429typedef __u16 Elf64_Half;
430#line 23 "include/linux/elf.h"
431typedef __u32 Elf64_Word;
432#line 24 "include/linux/elf.h"
433typedef __u64 Elf64_Xword;
434#line 193 "include/linux/elf.h"
435struct elf64_sym {
436 Elf64_Word st_name ;
437 unsigned char st_info ;
438 unsigned char st_other ;
439 Elf64_Half st_shndx ;
440 Elf64_Addr st_value ;
441 Elf64_Xword st_size ;
442};
443#line 201 "include/linux/elf.h"
444typedef struct elf64_sym Elf64_Sym;
445#line 445
446struct sock;
447#line 445
448struct sock;
449#line 446
450struct kobject;
451#line 446
452struct kobject;
453#line 447
454enum kobj_ns_type {
455 KOBJ_NS_TYPE_NONE = 0,
456 KOBJ_NS_TYPE_NET = 1,
457 KOBJ_NS_TYPES = 2
458} ;
459#line 453 "include/linux/elf.h"
460struct kobj_ns_type_operations {
461 enum kobj_ns_type type ;
462 void *(*grab_current_ns)(void) ;
463 void const *(*netlink_ns)(struct sock * ) ;
464 void const *(*initial_ns)(void) ;
465 void (*drop_ns)(void * ) ;
466};
467#line 57 "include/linux/kobject_ns.h"
468struct attribute {
469 char const *name ;
470 umode_t mode ;
471 struct lock_class_key *key ;
472 struct lock_class_key skey ;
473};
474#line 33 "include/linux/sysfs.h"
475struct attribute_group {
476 char const *name ;
477 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
478 struct attribute **attrs ;
479};
480#line 62 "include/linux/sysfs.h"
481struct bin_attribute {
482 struct attribute attr ;
483 size_t size ;
484 void *private ;
485 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
486 loff_t , size_t ) ;
487 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
488 loff_t , size_t ) ;
489 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
490};
491#line 98 "include/linux/sysfs.h"
492struct sysfs_ops {
493 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
494 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
495 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
496};
497#line 117
498struct sysfs_dirent;
499#line 117
500struct sysfs_dirent;
501#line 182 "include/linux/sysfs.h"
502struct kref {
503 atomic_t refcount ;
504};
505#line 49 "include/linux/kobject.h"
506struct kset;
507#line 49
508struct kobj_type;
509#line 49 "include/linux/kobject.h"
510struct kobject {
511 char const *name ;
512 struct list_head entry ;
513 struct kobject *parent ;
514 struct kset *kset ;
515 struct kobj_type *ktype ;
516 struct sysfs_dirent *sd ;
517 struct kref kref ;
518 unsigned char state_initialized : 1 ;
519 unsigned char state_in_sysfs : 1 ;
520 unsigned char state_add_uevent_sent : 1 ;
521 unsigned char state_remove_uevent_sent : 1 ;
522 unsigned char uevent_suppress : 1 ;
523};
524#line 107 "include/linux/kobject.h"
525struct kobj_type {
526 void (*release)(struct kobject * ) ;
527 struct sysfs_ops const *sysfs_ops ;
528 struct attribute **default_attrs ;
529 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
530 void const *(*namespace)(struct kobject * ) ;
531};
532#line 115 "include/linux/kobject.h"
533struct kobj_uevent_env {
534 char *envp[32U] ;
535 int envp_idx ;
536 char buf[2048U] ;
537 int buflen ;
538};
539#line 122 "include/linux/kobject.h"
540struct kset_uevent_ops {
541 int (* const filter)(struct kset * , struct kobject * ) ;
542 char const *(* const name)(struct kset * , struct kobject * ) ;
543 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
544};
545#line 139 "include/linux/kobject.h"
546struct kset {
547 struct list_head list ;
548 spinlock_t list_lock ;
549 struct kobject kobj ;
550 struct kset_uevent_ops const *uevent_ops ;
551};
552#line 215
553struct kernel_param;
554#line 215
555struct kernel_param;
556#line 216 "include/linux/kobject.h"
557struct kernel_param_ops {
558 int (*set)(char const * , struct kernel_param const * ) ;
559 int (*get)(char * , struct kernel_param const * ) ;
560 void (*free)(void * ) ;
561};
562#line 49 "include/linux/moduleparam.h"
563struct kparam_string;
564#line 49
565struct kparam_array;
566#line 49 "include/linux/moduleparam.h"
567union __anonunion_ldv_13363_134 {
568 void *arg ;
569 struct kparam_string const *str ;
570 struct kparam_array const *arr ;
571};
572#line 49 "include/linux/moduleparam.h"
573struct kernel_param {
574 char const *name ;
575 struct kernel_param_ops const *ops ;
576 u16 perm ;
577 s16 level ;
578 union __anonunion_ldv_13363_134 ldv_13363 ;
579};
580#line 61 "include/linux/moduleparam.h"
581struct kparam_string {
582 unsigned int maxlen ;
583 char *string ;
584};
585#line 67 "include/linux/moduleparam.h"
586struct kparam_array {
587 unsigned int max ;
588 unsigned int elemsize ;
589 unsigned int *num ;
590 struct kernel_param_ops const *ops ;
591 void *elem ;
592};
593#line 458 "include/linux/moduleparam.h"
594struct static_key {
595 atomic_t enabled ;
596};
597#line 225 "include/linux/jump_label.h"
598struct tracepoint;
599#line 225
600struct tracepoint;
601#line 226 "include/linux/jump_label.h"
602struct tracepoint_func {
603 void *func ;
604 void *data ;
605};
606#line 29 "include/linux/tracepoint.h"
607struct tracepoint {
608 char const *name ;
609 struct static_key key ;
610 void (*regfunc)(void) ;
611 void (*unregfunc)(void) ;
612 struct tracepoint_func *funcs ;
613};
614#line 86 "include/linux/tracepoint.h"
615struct kernel_symbol {
616 unsigned long value ;
617 char const *name ;
618};
619#line 27 "include/linux/export.h"
620struct mod_arch_specific {
621
622};
623#line 34 "include/linux/module.h"
624struct module_param_attrs;
625#line 34 "include/linux/module.h"
626struct module_kobject {
627 struct kobject kobj ;
628 struct module *mod ;
629 struct kobject *drivers_dir ;
630 struct module_param_attrs *mp ;
631};
632#line 43 "include/linux/module.h"
633struct module_attribute {
634 struct attribute attr ;
635 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
636 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
637 size_t ) ;
638 void (*setup)(struct module * , char const * ) ;
639 int (*test)(struct module * ) ;
640 void (*free)(struct module * ) ;
641};
642#line 69
643struct exception_table_entry;
644#line 69
645struct exception_table_entry;
646#line 198
647enum module_state {
648 MODULE_STATE_LIVE = 0,
649 MODULE_STATE_COMING = 1,
650 MODULE_STATE_GOING = 2
651} ;
652#line 204 "include/linux/module.h"
653struct module_ref {
654 unsigned long incs ;
655 unsigned long decs ;
656};
657#line 219
658struct module_sect_attrs;
659#line 219
660struct module_notes_attrs;
661#line 219
662struct ftrace_event_call;
663#line 219 "include/linux/module.h"
664struct module {
665 enum module_state state ;
666 struct list_head list ;
667 char name[56U] ;
668 struct module_kobject mkobj ;
669 struct module_attribute *modinfo_attrs ;
670 char const *version ;
671 char const *srcversion ;
672 struct kobject *holders_dir ;
673 struct kernel_symbol const *syms ;
674 unsigned long const *crcs ;
675 unsigned int num_syms ;
676 struct kernel_param *kp ;
677 unsigned int num_kp ;
678 unsigned int num_gpl_syms ;
679 struct kernel_symbol const *gpl_syms ;
680 unsigned long const *gpl_crcs ;
681 struct kernel_symbol const *unused_syms ;
682 unsigned long const *unused_crcs ;
683 unsigned int num_unused_syms ;
684 unsigned int num_unused_gpl_syms ;
685 struct kernel_symbol const *unused_gpl_syms ;
686 unsigned long const *unused_gpl_crcs ;
687 struct kernel_symbol const *gpl_future_syms ;
688 unsigned long const *gpl_future_crcs ;
689 unsigned int num_gpl_future_syms ;
690 unsigned int num_exentries ;
691 struct exception_table_entry *extable ;
692 int (*init)(void) ;
693 void *module_init ;
694 void *module_core ;
695 unsigned int init_size ;
696 unsigned int core_size ;
697 unsigned int init_text_size ;
698 unsigned int core_text_size ;
699 unsigned int init_ro_size ;
700 unsigned int core_ro_size ;
701 struct mod_arch_specific arch ;
702 unsigned int taints ;
703 unsigned int num_bugs ;
704 struct list_head bug_list ;
705 struct bug_entry *bug_table ;
706 Elf64_Sym *symtab ;
707 Elf64_Sym *core_symtab ;
708 unsigned int num_symtab ;
709 unsigned int core_num_syms ;
710 char *strtab ;
711 char *core_strtab ;
712 struct module_sect_attrs *sect_attrs ;
713 struct module_notes_attrs *notes_attrs ;
714 char *args ;
715 void *percpu ;
716 unsigned int percpu_size ;
717 unsigned int num_tracepoints ;
718 struct tracepoint * const *tracepoints_ptrs ;
719 unsigned int num_trace_bprintk_fmt ;
720 char const **trace_bprintk_fmt_start ;
721 struct ftrace_event_call **trace_events ;
722 unsigned int num_trace_events ;
723 struct list_head source_list ;
724 struct list_head target_list ;
725 struct task_struct *waiter ;
726 void (*exit)(void) ;
727 struct module_ref *refptr ;
728 ctor_fn_t (**ctors)(void) ;
729 unsigned int num_ctors ;
730};
731#line 88 "include/linux/kmemleak.h"
732struct kmem_cache_cpu {
733 void **freelist ;
734 unsigned long tid ;
735 struct page *page ;
736 struct page *partial ;
737 int node ;
738 unsigned int stat[26U] ;
739};
740#line 55 "include/linux/slub_def.h"
741struct kmem_cache_node {
742 spinlock_t list_lock ;
743 unsigned long nr_partial ;
744 struct list_head partial ;
745 atomic_long_t nr_slabs ;
746 atomic_long_t total_objects ;
747 struct list_head full ;
748};
749#line 66 "include/linux/slub_def.h"
750struct kmem_cache_order_objects {
751 unsigned long x ;
752};
753#line 76 "include/linux/slub_def.h"
754struct kmem_cache {
755 struct kmem_cache_cpu *cpu_slab ;
756 unsigned long flags ;
757 unsigned long min_partial ;
758 int size ;
759 int objsize ;
760 int offset ;
761 int cpu_partial ;
762 struct kmem_cache_order_objects oo ;
763 struct kmem_cache_order_objects max ;
764 struct kmem_cache_order_objects min ;
765 gfp_t allocflags ;
766 int refcount ;
767 void (*ctor)(void * ) ;
768 int inuse ;
769 int align ;
770 int reserved ;
771 char const *name ;
772 struct list_head list ;
773 struct kobject kobj ;
774 int remote_node_defrag_ratio ;
775 struct kmem_cache_node *node[1024U] ;
776};
777#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
778struct klist_node;
779#line 15
780struct klist_node;
781#line 37 "include/linux/klist.h"
782struct klist_node {
783 void *n_klist ;
784 struct list_head n_node ;
785 struct kref n_ref ;
786};
787#line 67
788struct dma_map_ops;
789#line 67 "include/linux/klist.h"
790struct dev_archdata {
791 void *acpi_handle ;
792 struct dma_map_ops *dma_ops ;
793 void *iommu ;
794};
795#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
796struct pdev_archdata {
797
798};
799#line 17
800struct device_private;
801#line 17
802struct device_private;
803#line 18
804struct device_driver;
805#line 18
806struct device_driver;
807#line 19
808struct driver_private;
809#line 19
810struct driver_private;
811#line 20
812struct class;
813#line 20
814struct class;
815#line 21
816struct subsys_private;
817#line 21
818struct subsys_private;
819#line 22
820struct bus_type;
821#line 22
822struct bus_type;
823#line 23
824struct device_node;
825#line 23
826struct device_node;
827#line 24
828struct iommu_ops;
829#line 24
830struct iommu_ops;
831#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
832struct bus_attribute {
833 struct attribute attr ;
834 ssize_t (*show)(struct bus_type * , char * ) ;
835 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
836};
837#line 51 "include/linux/device.h"
838struct device_attribute;
839#line 51
840struct driver_attribute;
841#line 51 "include/linux/device.h"
842struct bus_type {
843 char const *name ;
844 char const *dev_name ;
845 struct device *dev_root ;
846 struct bus_attribute *bus_attrs ;
847 struct device_attribute *dev_attrs ;
848 struct driver_attribute *drv_attrs ;
849 int (*match)(struct device * , struct device_driver * ) ;
850 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
851 int (*probe)(struct device * ) ;
852 int (*remove)(struct device * ) ;
853 void (*shutdown)(struct device * ) ;
854 int (*suspend)(struct device * , pm_message_t ) ;
855 int (*resume)(struct device * ) ;
856 struct dev_pm_ops const *pm ;
857 struct iommu_ops *iommu_ops ;
858 struct subsys_private *p ;
859};
860#line 125
861struct device_type;
862#line 182
863struct of_device_id;
864#line 182 "include/linux/device.h"
865struct device_driver {
866 char const *name ;
867 struct bus_type *bus ;
868 struct module *owner ;
869 char const *mod_name ;
870 bool suppress_bind_attrs ;
871 struct of_device_id const *of_match_table ;
872 int (*probe)(struct device * ) ;
873 int (*remove)(struct device * ) ;
874 void (*shutdown)(struct device * ) ;
875 int (*suspend)(struct device * , pm_message_t ) ;
876 int (*resume)(struct device * ) ;
877 struct attribute_group const **groups ;
878 struct dev_pm_ops const *pm ;
879 struct driver_private *p ;
880};
881#line 245 "include/linux/device.h"
882struct driver_attribute {
883 struct attribute attr ;
884 ssize_t (*show)(struct device_driver * , char * ) ;
885 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
886};
887#line 299
888struct class_attribute;
889#line 299 "include/linux/device.h"
890struct class {
891 char const *name ;
892 struct module *owner ;
893 struct class_attribute *class_attrs ;
894 struct device_attribute *dev_attrs ;
895 struct bin_attribute *dev_bin_attrs ;
896 struct kobject *dev_kobj ;
897 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
898 char *(*devnode)(struct device * , umode_t * ) ;
899 void (*class_release)(struct class * ) ;
900 void (*dev_release)(struct device * ) ;
901 int (*suspend)(struct device * , pm_message_t ) ;
902 int (*resume)(struct device * ) ;
903 struct kobj_ns_type_operations const *ns_type ;
904 void const *(*namespace)(struct device * ) ;
905 struct dev_pm_ops const *pm ;
906 struct subsys_private *p ;
907};
908#line 394 "include/linux/device.h"
909struct class_attribute {
910 struct attribute attr ;
911 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
912 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
913 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
914};
915#line 447 "include/linux/device.h"
916struct device_type {
917 char const *name ;
918 struct attribute_group const **groups ;
919 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
920 char *(*devnode)(struct device * , umode_t * ) ;
921 void (*release)(struct device * ) ;
922 struct dev_pm_ops const *pm ;
923};
924#line 474 "include/linux/device.h"
925struct device_attribute {
926 struct attribute attr ;
927 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
928 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
929 size_t ) ;
930};
931#line 557 "include/linux/device.h"
932struct device_dma_parameters {
933 unsigned int max_segment_size ;
934 unsigned long segment_boundary_mask ;
935};
936#line 567
937struct dma_coherent_mem;
938#line 567 "include/linux/device.h"
939struct device {
940 struct device *parent ;
941 struct device_private *p ;
942 struct kobject kobj ;
943 char const *init_name ;
944 struct device_type const *type ;
945 struct mutex mutex ;
946 struct bus_type *bus ;
947 struct device_driver *driver ;
948 void *platform_data ;
949 struct dev_pm_info power ;
950 struct dev_pm_domain *pm_domain ;
951 int numa_node ;
952 u64 *dma_mask ;
953 u64 coherent_dma_mask ;
954 struct device_dma_parameters *dma_parms ;
955 struct list_head dma_pools ;
956 struct dma_coherent_mem *dma_mem ;
957 struct dev_archdata archdata ;
958 struct device_node *of_node ;
959 dev_t devt ;
960 u32 id ;
961 spinlock_t devres_lock ;
962 struct list_head devres_head ;
963 struct klist_node knode_class ;
964 struct class *class ;
965 struct attribute_group const **groups ;
966 void (*release)(struct device * ) ;
967};
968#line 681 "include/linux/device.h"
969struct wakeup_source {
970 char const *name ;
971 struct list_head entry ;
972 spinlock_t lock ;
973 struct timer_list timer ;
974 unsigned long timer_expires ;
975 ktime_t total_time ;
976 ktime_t max_time ;
977 ktime_t last_time ;
978 unsigned long event_count ;
979 unsigned long active_count ;
980 unsigned long relax_count ;
981 unsigned long hit_count ;
982 unsigned char active : 1 ;
983};
984#line 12 "include/linux/mod_devicetable.h"
985typedef unsigned long kernel_ulong_t;
986#line 215 "include/linux/mod_devicetable.h"
987struct of_device_id {
988 char name[32U] ;
989 char type[32U] ;
990 char compatible[128U] ;
991 void *data ;
992};
993#line 492 "include/linux/mod_devicetable.h"
994struct platform_device_id {
995 char name[20U] ;
996 kernel_ulong_t driver_data ;
997};
998#line 584
999struct mfd_cell;
1000#line 584
1001struct mfd_cell;
1002#line 585 "include/linux/mod_devicetable.h"
1003struct platform_device {
1004 char const *name ;
1005 int id ;
1006 struct device dev ;
1007 u32 num_resources ;
1008 struct resource *resource ;
1009 struct platform_device_id const *id_entry ;
1010 struct mfd_cell *mfd_cell ;
1011 struct pdev_archdata archdata ;
1012};
1013#line 272 "include/linux/platform_device.h"
1014enum led_brightness {
1015 LED_OFF = 0,
1016 LED_HALF = 127,
1017 LED_FULL = 255
1018} ;
1019#line 278
1020struct led_trigger;
1021#line 278 "include/linux/platform_device.h"
1022struct led_classdev {
1023 char const *name ;
1024 int brightness ;
1025 int max_brightness ;
1026 int flags ;
1027 void (*brightness_set)(struct led_classdev * , enum led_brightness ) ;
1028 enum led_brightness (*brightness_get)(struct led_classdev * ) ;
1029 int (*blink_set)(struct led_classdev * , unsigned long * , unsigned long * ) ;
1030 struct device *dev ;
1031 struct list_head node ;
1032 char const *default_trigger ;
1033 unsigned long blink_delay_on ;
1034 unsigned long blink_delay_off ;
1035 struct timer_list blink_timer ;
1036 int blink_brightness ;
1037 struct rw_semaphore trigger_lock ;
1038 struct led_trigger *trigger ;
1039 struct list_head trig_list ;
1040 void *trigger_data ;
1041};
1042#line 113 "include/linux/leds.h"
1043struct led_trigger {
1044 char const *name ;
1045 void (*activate)(struct led_classdev * ) ;
1046 void (*deactivate)(struct led_classdev * ) ;
1047 rwlock_t leddev_list_lock ;
1048 struct list_head led_cdevs ;
1049 struct list_head next_trig ;
1050};
1051#line 261
1052enum power_supply_property {
1053 POWER_SUPPLY_PROP_STATUS = 0,
1054 POWER_SUPPLY_PROP_CHARGE_TYPE = 1,
1055 POWER_SUPPLY_PROP_HEALTH = 2,
1056 POWER_SUPPLY_PROP_PRESENT = 3,
1057 POWER_SUPPLY_PROP_ONLINE = 4,
1058 POWER_SUPPLY_PROP_TECHNOLOGY = 5,
1059 POWER_SUPPLY_PROP_CYCLE_COUNT = 6,
1060 POWER_SUPPLY_PROP_VOLTAGE_MAX = 7,
1061 POWER_SUPPLY_PROP_VOLTAGE_MIN = 8,
1062 POWER_SUPPLY_PROP_VOLTAGE_MAX_DESIGN = 9,
1063 POWER_SUPPLY_PROP_VOLTAGE_MIN_DESIGN = 10,
1064 POWER_SUPPLY_PROP_VOLTAGE_NOW = 11,
1065 POWER_SUPPLY_PROP_VOLTAGE_AVG = 12,
1066 POWER_SUPPLY_PROP_CURRENT_MAX = 13,
1067 POWER_SUPPLY_PROP_CURRENT_NOW = 14,
1068 POWER_SUPPLY_PROP_CURRENT_AVG = 15,
1069 POWER_SUPPLY_PROP_POWER_NOW = 16,
1070 POWER_SUPPLY_PROP_POWER_AVG = 17,
1071 POWER_SUPPLY_PROP_CHARGE_FULL_DESIGN = 18,
1072 POWER_SUPPLY_PROP_CHARGE_EMPTY_DESIGN = 19,
1073 POWER_SUPPLY_PROP_CHARGE_FULL = 20,
1074 POWER_SUPPLY_PROP_CHARGE_EMPTY = 21,
1075 POWER_SUPPLY_PROP_CHARGE_NOW = 22,
1076 POWER_SUPPLY_PROP_CHARGE_AVG = 23,
1077 POWER_SUPPLY_PROP_CHARGE_COUNTER = 24,
1078 POWER_SUPPLY_PROP_ENERGY_FULL_DESIGN = 25,
1079 POWER_SUPPLY_PROP_ENERGY_EMPTY_DESIGN = 26,
1080 POWER_SUPPLY_PROP_ENERGY_FULL = 27,
1081 POWER_SUPPLY_PROP_ENERGY_EMPTY = 28,
1082 POWER_SUPPLY_PROP_ENERGY_NOW = 29,
1083 POWER_SUPPLY_PROP_ENERGY_AVG = 30,
1084 POWER_SUPPLY_PROP_CAPACITY = 31,
1085 POWER_SUPPLY_PROP_CAPACITY_LEVEL = 32,
1086 POWER_SUPPLY_PROP_TEMP = 33,
1087 POWER_SUPPLY_PROP_TEMP_AMBIENT = 34,
1088 POWER_SUPPLY_PROP_TIME_TO_EMPTY_NOW = 35,
1089 POWER_SUPPLY_PROP_TIME_TO_EMPTY_AVG = 36,
1090 POWER_SUPPLY_PROP_TIME_TO_FULL_NOW = 37,
1091 POWER_SUPPLY_PROP_TIME_TO_FULL_AVG = 38,
1092 POWER_SUPPLY_PROP_TYPE = 39,
1093 POWER_SUPPLY_PROP_SCOPE = 40,
1094 POWER_SUPPLY_PROP_MODEL_NAME = 41,
1095 POWER_SUPPLY_PROP_MANUFACTURER = 42,
1096 POWER_SUPPLY_PROP_SERIAL_NUMBER = 43
1097} ;
1098#line 308
1099enum power_supply_type {
1100 POWER_SUPPLY_TYPE_UNKNOWN = 0,
1101 POWER_SUPPLY_TYPE_BATTERY = 1,
1102 POWER_SUPPLY_TYPE_UPS = 2,
1103 POWER_SUPPLY_TYPE_MAINS = 3,
1104 POWER_SUPPLY_TYPE_USB = 4,
1105 POWER_SUPPLY_TYPE_USB_DCP = 5,
1106 POWER_SUPPLY_TYPE_USB_CDP = 6,
1107 POWER_SUPPLY_TYPE_USB_ACA = 7
1108} ;
1109#line 319 "include/linux/leds.h"
1110union power_supply_propval {
1111 int intval ;
1112 char const *strval ;
1113};
1114#line 148 "include/linux/power_supply.h"
1115struct power_supply {
1116 char const *name ;
1117 enum power_supply_type type ;
1118 enum power_supply_property *properties ;
1119 size_t num_properties ;
1120 char **supplied_to ;
1121 size_t num_supplicants ;
1122 int (*get_property)(struct power_supply * , enum power_supply_property , union power_supply_propval * ) ;
1123 int (*set_property)(struct power_supply * , enum power_supply_property , union power_supply_propval const * ) ;
1124 int (*property_is_writeable)(struct power_supply * , enum power_supply_property ) ;
1125 void (*external_power_changed)(struct power_supply * ) ;
1126 void (*set_charged)(struct power_supply * ) ;
1127 int use_for_apm ;
1128 struct device *dev ;
1129 struct work_struct changed_work ;
1130 struct led_trigger *charging_full_trig ;
1131 char *charging_full_trig_name ;
1132 struct led_trigger *charging_trig ;
1133 char *charging_trig_name ;
1134 struct led_trigger *full_trig ;
1135 char *full_trig_name ;
1136 struct led_trigger *online_trig ;
1137 char *online_trig_name ;
1138 struct led_trigger *charging_blink_full_solid_trig ;
1139 char *charging_blink_full_solid_trig_name ;
1140};
1141#line 272
1142enum irqreturn {
1143 IRQ_NONE = 0,
1144 IRQ_HANDLED = 1,
1145 IRQ_WAKE_THREAD = 2
1146} ;
1147#line 16 "include/linux/irqreturn.h"
1148typedef enum irqreturn irqreturn_t;
1149#line 41 "include/asm-generic/sections.h"
1150struct exception_table_entry {
1151 unsigned long insn ;
1152 unsigned long fixup ;
1153};
1154#line 704 "include/linux/interrupt.h"
1155struct regmap;
1156#line 704
1157struct regmap;
1158#line 231 "include/linux/regmap.h"
1159struct wm831x;
1160#line 231
1161struct wm831x;
1162#line 232
1163enum wm831x_auxadc;
1164#line 232
1165enum wm831x_auxadc;
1166#line 359 "include/linux/mfd/wm831x/core.h"
1167struct wm831x {
1168 struct mutex io_lock ;
1169 struct device *dev ;
1170 struct regmap *regmap ;
1171 int irq ;
1172 struct mutex irq_lock ;
1173 int irq_base ;
1174 int irq_masks_cur[5U] ;
1175 int irq_masks_cache[5U] ;
1176 bool soft_shutdown ;
1177 unsigned char has_gpio_ena : 1 ;
1178 unsigned char has_cs_sts : 1 ;
1179 unsigned char charger_irq_wake : 1 ;
1180 int num_gpio ;
1181 int gpio_update[16U] ;
1182 bool gpio_level[16U] ;
1183 struct mutex auxadc_lock ;
1184 struct list_head auxadc_pending ;
1185 u16 auxadc_active ;
1186 int (*auxadc_read)(struct wm831x * , enum wm831x_auxadc ) ;
1187 struct mutex key_lock ;
1188 unsigned char locked : 1 ;
1189};
1190#line 421
1191enum wm831x_auxadc {
1192 WM831X_AUX_CAL = 15,
1193 WM831X_AUX_BKUP_BATT = 10,
1194 WM831X_AUX_WALL = 9,
1195 WM831X_AUX_BATT = 8,
1196 WM831X_AUX_USB = 7,
1197 WM831X_AUX_SYSVDD = 6,
1198 WM831X_AUX_BATT_TEMP = 5,
1199 WM831X_AUX_CHIP_TEMP = 4,
1200 WM831X_AUX_AUX4 = 3,
1201 WM831X_AUX_AUX3 = 2,
1202 WM831X_AUX_AUX2 = 1,
1203 WM831X_AUX_AUX1 = 0
1204} ;
1205#line 215 "include/linux/mfd/wm831x/auxadc.h"
1206struct regulator_init_data;
1207#line 215
1208struct regulator_init_data;
1209#line 216 "include/linux/mfd/wm831x/auxadc.h"
1210struct wm831x_backlight_pdata {
1211 int isink ;
1212 int max_uA ;
1213};
1214#line 25 "include/linux/mfd/wm831x/pdata.h"
1215struct wm831x_backup_pdata {
1216 int charger_enable ;
1217 int no_constant_voltage ;
1218 int vlim ;
1219 int ilim ;
1220};
1221#line 32 "include/linux/mfd/wm831x/pdata.h"
1222struct wm831x_battery_pdata {
1223 int enable ;
1224 int fast_enable ;
1225 int off_mask ;
1226 int trickle_ilim ;
1227 int vsel ;
1228 int eoc_iterm ;
1229 int fast_ilim ;
1230 int timeout ;
1231};
1232#line 60
1233enum wm831x_status_src {
1234 WM831X_STATUS_PRESERVE = 0,
1235 WM831X_STATUS_OTP = 1,
1236 WM831X_STATUS_POWER = 2,
1237 WM831X_STATUS_CHARGER = 3,
1238 WM831X_STATUS_MANUAL = 4
1239} ;
1240#line 68 "include/linux/mfd/wm831x/pdata.h"
1241struct wm831x_status_pdata {
1242 enum wm831x_status_src default_src ;
1243 char const *name ;
1244 char const *default_trigger ;
1245};
1246#line 77 "include/linux/mfd/wm831x/pdata.h"
1247struct wm831x_touch_pdata {
1248 int fivewire ;
1249 int isel ;
1250 int rpu ;
1251 int pressure ;
1252 unsigned int data_irq ;
1253 int data_irqf ;
1254 unsigned int pd_irq ;
1255 int pd_irqf ;
1256};
1257#line 88
1258enum wm831x_watchdog_action {
1259 WM831X_WDOG_NONE = 0,
1260 WM831X_WDOG_INTERRUPT = 1,
1261 WM831X_WDOG_RESET = 2,
1262 WM831X_WDOG_WAKE = 3
1263} ;
1264#line 95 "include/linux/mfd/wm831x/pdata.h"
1265struct wm831x_watchdog_pdata {
1266 enum wm831x_watchdog_action primary ;
1267 enum wm831x_watchdog_action secondary ;
1268 int update_gpio ;
1269 unsigned char software : 1 ;
1270};
1271#line 101 "include/linux/mfd/wm831x/pdata.h"
1272struct wm831x_pdata {
1273 int wm831x_num ;
1274 int (*pre_init)(struct wm831x * ) ;
1275 int (*post_init)(struct wm831x * ) ;
1276 bool irq_cmos ;
1277 bool disable_touch ;
1278 bool soft_shutdown ;
1279 int irq_base ;
1280 int gpio_base ;
1281 int gpio_defaults[16U] ;
1282 struct wm831x_backlight_pdata *backlight ;
1283 struct wm831x_backup_pdata *backup ;
1284 struct wm831x_battery_pdata *battery ;
1285 struct wm831x_touch_pdata *touch ;
1286 struct wm831x_watchdog_pdata *watchdog ;
1287 struct wm831x_status_pdata *status[2U] ;
1288 struct regulator_init_data *dcdc[4U] ;
1289 struct regulator_init_data *epe[2U] ;
1290 struct regulator_init_data *ldo[11U] ;
1291 struct regulator_init_data *isink[2U] ;
1292};
1293#line 149 "include/linux/mfd/wm831x/pdata.h"
1294struct wm831x_power {
1295 struct wm831x *wm831x ;
1296 struct power_supply wall ;
1297 struct power_supply usb ;
1298 struct power_supply battery ;
1299 char wall_name[20U] ;
1300 char usb_name[20U] ;
1301 char battery_name[20U] ;
1302 bool have_battery ;
1303};
1304#line 136 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1305struct chg_map {
1306 int val ;
1307 int reg_val ;
1308};
1309#line 1 "<compiler builtins>"
1310long __builtin_expect(long , long ) ;
1311#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1312void ldv_spin_lock(void) ;
1313#line 3
1314void ldv_spin_unlock(void) ;
1315#line 4
1316int ldv_spin_trylock(void) ;
1317#line 50 "include/linux/dynamic_debug.h"
1318extern int __dynamic_dev_dbg(struct _ddebug * , struct device const * , char const *
1319 , ...) ;
1320#line 323 "include/linux/kernel.h"
1321extern int snprintf(char * , size_t , char const * , ...) ;
1322#line 161 "include/linux/slab.h"
1323extern void kfree(void const * ) ;
1324#line 220 "include/linux/slub_def.h"
1325extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1326#line 223
1327void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1328#line 353 "include/linux/slab.h"
1329__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1330#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1331extern void *__VERIFIER_nondet_pointer(void) ;
1332#line 11
1333void ldv_check_alloc_flags(gfp_t flags ) ;
1334#line 12
1335void ldv_check_alloc_nonatomic(void) ;
1336#line 14
1337struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1338#line 792 "include/linux/device.h"
1339extern void *dev_get_drvdata(struct device const * ) ;
1340#line 793
1341extern int dev_set_drvdata(struct device * , void * ) ;
1342#line 890
1343extern int dev_crit(struct device const * , char const * , ...) ;
1344#line 892
1345extern int dev_err(struct device const * , char const * , ...) ;
1346#line 894
1347extern int dev_warn(struct device const * , char const * , ...) ;
1348#line 898
1349extern int _dev_info(struct device const * , char const * , ...) ;
1350#line 49 "include/linux/platform_device.h"
1351extern int platform_get_irq_byname(struct platform_device * , char const * ) ;
1352#line 188 "include/linux/platform_device.h"
1353__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )
1354{ unsigned long __cil_tmp3 ;
1355 unsigned long __cil_tmp4 ;
1356 struct device *__cil_tmp5 ;
1357
1358 {
1359 {
1360#line 190
1361 __cil_tmp3 = (unsigned long )pdev;
1362#line 190
1363 __cil_tmp4 = __cil_tmp3 + 16;
1364#line 190
1365 __cil_tmp5 = (struct device *)__cil_tmp4;
1366#line 190
1367 dev_set_drvdata(__cil_tmp5, data);
1368 }
1369#line 191
1370 return;
1371}
1372}
1373#line 210 "include/linux/power_supply.h"
1374extern void power_supply_changed(struct power_supply * ) ;
1375#line 220
1376extern int power_supply_register(struct device * , struct power_supply * ) ;
1377#line 222
1378extern void power_supply_unregister(struct power_supply * ) ;
1379#line 127 "include/linux/interrupt.h"
1380extern int request_threaded_irq(unsigned int , irqreturn_t (*)(int , void * ) ,
1381 irqreturn_t (*)(int , void * ) , unsigned long ,
1382 char const * , void * ) ;
1383#line 184
1384extern void free_irq(unsigned int , void * ) ;
1385#line 402 "include/linux/mfd/wm831x/core.h"
1386extern int wm831x_reg_read(struct wm831x * , unsigned short ) ;
1387#line 405
1388extern void wm831x_reg_lock(struct wm831x * ) ;
1389#line 406
1390extern int wm831x_reg_unlock(struct wm831x * ) ;
1391#line 407
1392extern int wm831x_set_bits(struct wm831x * , unsigned short , unsigned short , unsigned short ) ;
1393#line 214 "include/linux/mfd/wm831x/auxadc.h"
1394extern int wm831x_auxadc_read_uv(struct wm831x * , enum wm831x_auxadc ) ;
1395#line 48 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1396static int wm831x_power_check_online(struct wm831x *wm831x , int supply , union power_supply_propval *val )
1397{ int ret ;
1398 int __cil_tmp5 ;
1399
1400 {
1401 {
1402#line 53
1403 ret = wm831x_reg_read(wm831x, (unsigned short)16397);
1404 }
1405#line 54
1406 if (ret < 0) {
1407#line 55
1408 return (ret);
1409 } else {
1410
1411 }
1412 {
1413#line 57
1414 __cil_tmp5 = ret & supply;
1415#line 57
1416 if (__cil_tmp5 != 0) {
1417#line 58
1418 *((int *)val) = 1;
1419 } else {
1420#line 60
1421 *((int *)val) = 0;
1422 }
1423 }
1424#line 62
1425 return (0);
1426}
1427}
1428#line 65 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1429static int wm831x_power_read_voltage(struct wm831x *wm831x , enum wm831x_auxadc src ,
1430 union power_supply_propval *val )
1431{ int ret ;
1432
1433 {
1434 {
1435#line 71
1436 ret = wm831x_auxadc_read_uv(wm831x, src);
1437 }
1438#line 72
1439 if (ret >= 0) {
1440#line 73
1441 *((int *)val) = ret;
1442 } else {
1443
1444 }
1445#line 75
1446 return (ret);
1447}
1448}
1449#line 81 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1450static int wm831x_wall_get_prop(struct power_supply *psy , enum power_supply_property psp ,
1451 union power_supply_propval *val )
1452{ struct wm831x_power *wm831x_power ;
1453 void *tmp ;
1454 struct wm831x *wm831x ;
1455 int ret ;
1456 unsigned long __cil_tmp8 ;
1457 unsigned long __cil_tmp9 ;
1458 struct device *__cil_tmp10 ;
1459 struct device *__cil_tmp11 ;
1460 struct device const *__cil_tmp12 ;
1461 unsigned int __cil_tmp13 ;
1462 enum wm831x_auxadc __cil_tmp14 ;
1463
1464 {
1465 {
1466#line 85
1467 __cil_tmp8 = (unsigned long )psy;
1468#line 85
1469 __cil_tmp9 = __cil_tmp8 + 96;
1470#line 85
1471 __cil_tmp10 = *((struct device **)__cil_tmp9);
1472#line 85
1473 __cil_tmp11 = *((struct device **)__cil_tmp10);
1474#line 85
1475 __cil_tmp12 = (struct device const *)__cil_tmp11;
1476#line 85
1477 tmp = dev_get_drvdata(__cil_tmp12);
1478#line 85
1479 wm831x_power = (struct wm831x_power *)tmp;
1480#line 86
1481 wm831x = *((struct wm831x **)wm831x_power);
1482#line 87
1483 ret = 0;
1484 }
1485 {
1486#line 89
1487 __cil_tmp13 = (unsigned int )psp;
1488#line 90
1489 if ((int )__cil_tmp13 == 4) {
1490#line 90
1491 goto case_4;
1492 } else
1493#line 93
1494 if ((int )__cil_tmp13 == 11) {
1495#line 93
1496 goto case_11;
1497 } else {
1498 {
1499#line 96
1500 goto switch_default;
1501#line 89
1502 if (0) {
1503 case_4:
1504 {
1505#line 91
1506 ret = wm831x_power_check_online(wm831x, 512, val);
1507 }
1508#line 92
1509 goto ldv_17515;
1510 case_11:
1511 {
1512#line 94
1513 __cil_tmp14 = (enum wm831x_auxadc )9;
1514#line 94
1515 ret = wm831x_power_read_voltage(wm831x, __cil_tmp14, val);
1516 }
1517#line 95
1518 goto ldv_17515;
1519 switch_default:
1520#line 97
1521 ret = -22;
1522#line 98
1523 goto ldv_17515;
1524 } else {
1525 switch_break: ;
1526 }
1527 }
1528 }
1529 }
1530 ldv_17515: ;
1531#line 101
1532 return (ret);
1533}
1534}
1535#line 104 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1536static enum power_supply_property wm831x_wall_props[2U] = { (enum power_supply_property )4, (enum power_supply_property )11};
1537#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1538static int wm831x_usb_get_prop(struct power_supply *psy , enum power_supply_property psp ,
1539 union power_supply_propval *val )
1540{ struct wm831x_power *wm831x_power ;
1541 void *tmp ;
1542 struct wm831x *wm831x ;
1543 int ret ;
1544 unsigned long __cil_tmp8 ;
1545 unsigned long __cil_tmp9 ;
1546 struct device *__cil_tmp10 ;
1547 struct device *__cil_tmp11 ;
1548 struct device const *__cil_tmp12 ;
1549 unsigned int __cil_tmp13 ;
1550 enum wm831x_auxadc __cil_tmp14 ;
1551
1552 {
1553 {
1554#line 116
1555 __cil_tmp8 = (unsigned long )psy;
1556#line 116
1557 __cil_tmp9 = __cil_tmp8 + 96;
1558#line 116
1559 __cil_tmp10 = *((struct device **)__cil_tmp9);
1560#line 116
1561 __cil_tmp11 = *((struct device **)__cil_tmp10);
1562#line 116
1563 __cil_tmp12 = (struct device const *)__cil_tmp11;
1564#line 116
1565 tmp = dev_get_drvdata(__cil_tmp12);
1566#line 116
1567 wm831x_power = (struct wm831x_power *)tmp;
1568#line 117
1569 wm831x = *((struct wm831x **)wm831x_power);
1570#line 118
1571 ret = 0;
1572 }
1573 {
1574#line 120
1575 __cil_tmp13 = (unsigned int )psp;
1576#line 121
1577 if ((int )__cil_tmp13 == 4) {
1578#line 121
1579 goto case_4;
1580 } else
1581#line 124
1582 if ((int )__cil_tmp13 == 11) {
1583#line 124
1584 goto case_11;
1585 } else {
1586 {
1587#line 127
1588 goto switch_default;
1589#line 120
1590 if (0) {
1591 case_4:
1592 {
1593#line 122
1594 ret = wm831x_power_check_online(wm831x, 256, val);
1595 }
1596#line 123
1597 goto ldv_17528;
1598 case_11:
1599 {
1600#line 125
1601 __cil_tmp14 = (enum wm831x_auxadc )7;
1602#line 125
1603 ret = wm831x_power_read_voltage(wm831x, __cil_tmp14, val);
1604 }
1605#line 126
1606 goto ldv_17528;
1607 switch_default:
1608#line 128
1609 ret = -22;
1610#line 129
1611 goto ldv_17528;
1612 } else {
1613 switch_break: ;
1614 }
1615 }
1616 }
1617 }
1618 ldv_17528: ;
1619#line 132
1620 return (ret);
1621}
1622}
1623#line 135 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1624static enum power_supply_property wm831x_usb_props[2U] = { (enum power_supply_property )4, (enum power_supply_property )11};
1625#line 149 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1626static struct chg_map trickle_ilims[4U] = { {50, 0},
1627 {100, 64},
1628 {150, 128},
1629 {200, 192}};
1630#line 156 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1631static struct chg_map vsels[4U] = { {4050, 0},
1632 {4100, 16},
1633 {4150, 32},
1634 {4200, 48}};
1635#line 163 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1636static struct chg_map fast_ilims[16U] =
1637#line 163
1638 { {0, 0},
1639 {50, 1},
1640 {100, 2},
1641 {150, 3},
1642 {200, 4},
1643 {250, 5},
1644 {300, 6},
1645 {350, 7},
1646 {400, 8},
1647 {450, 9},
1648 {500, 10},
1649 {600, 11},
1650 {700, 12},
1651 {800, 13},
1652 {900, 14},
1653 {1000, 15}};
1654#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1655static struct chg_map eoc_iterms[8U] =
1656#line 182
1657 { {20, 0},
1658 {30, 1024},
1659 {40, 2048},
1660 {50, 3072},
1661 {60, 4096},
1662 {70, 5120},
1663 {80, 6144},
1664 {90, 7168}};
1665#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1666static struct chg_map chg_times[16U] =
1667#line 193
1668 { {60, 0},
1669 {90, 256},
1670 {120, 512},
1671 {150, 768},
1672 {180, 1024},
1673 {210, 1280},
1674 {240, 1536},
1675 {270, 1792},
1676 {300, 2048},
1677 {330, 2304},
1678 {360, 2560},
1679 {390, 2816},
1680 {420, 3072},
1681 {450, 3328},
1682 {480, 3584},
1683 {510, 3840}};
1684#line 212 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1685static void wm831x_battey_apply_config(struct wm831x *wm831x , struct chg_map *map ,
1686 int count , int val , int *reg , char const *name ,
1687 char const *units )
1688{ int i ;
1689 struct _ddebug descriptor ;
1690 long tmp ;
1691 unsigned long __cil_tmp11 ;
1692 struct chg_map *__cil_tmp12 ;
1693 int __cil_tmp13 ;
1694 unsigned long __cil_tmp14 ;
1695 unsigned long __cil_tmp15 ;
1696 struct device *__cil_tmp16 ;
1697 struct device const *__cil_tmp17 ;
1698 unsigned long __cil_tmp18 ;
1699 struct chg_map *__cil_tmp19 ;
1700 unsigned long __cil_tmp20 ;
1701 unsigned long __cil_tmp21 ;
1702 int __cil_tmp22 ;
1703 int __cil_tmp23 ;
1704 struct _ddebug *__cil_tmp24 ;
1705 unsigned long __cil_tmp25 ;
1706 unsigned long __cil_tmp26 ;
1707 unsigned long __cil_tmp27 ;
1708 unsigned long __cil_tmp28 ;
1709 unsigned long __cil_tmp29 ;
1710 unsigned long __cil_tmp30 ;
1711 unsigned char __cil_tmp31 ;
1712 long __cil_tmp32 ;
1713 long __cil_tmp33 ;
1714 unsigned long __cil_tmp34 ;
1715 unsigned long __cil_tmp35 ;
1716 struct device *__cil_tmp36 ;
1717 struct device const *__cil_tmp37 ;
1718
1719 {
1720#line 219
1721 i = 0;
1722#line 219
1723 goto ldv_17552;
1724 ldv_17551: ;
1725 {
1726#line 220
1727 __cil_tmp11 = (unsigned long )i;
1728#line 220
1729 __cil_tmp12 = map + __cil_tmp11;
1730#line 220
1731 __cil_tmp13 = *((int *)__cil_tmp12);
1732#line 220
1733 if (__cil_tmp13 == val) {
1734#line 221
1735 goto ldv_17550;
1736 } else {
1737
1738 }
1739 }
1740#line 219
1741 i = i + 1;
1742 ldv_17552: ;
1743#line 219
1744 if (i < count) {
1745#line 220
1746 goto ldv_17551;
1747 } else {
1748#line 222
1749 goto ldv_17550;
1750 }
1751 ldv_17550: ;
1752#line 222
1753 if (i == count) {
1754 {
1755#line 223
1756 __cil_tmp14 = (unsigned long )wm831x;
1757#line 223
1758 __cil_tmp15 = __cil_tmp14 + 168;
1759#line 223
1760 __cil_tmp16 = *((struct device **)__cil_tmp15);
1761#line 223
1762 __cil_tmp17 = (struct device const *)__cil_tmp16;
1763#line 223
1764 dev_err(__cil_tmp17, "Invalid %s %d%s\n", name, val, units);
1765 }
1766 } else {
1767 {
1768#line 226
1769 __cil_tmp18 = (unsigned long )i;
1770#line 226
1771 __cil_tmp19 = map + __cil_tmp18;
1772#line 226
1773 __cil_tmp20 = (unsigned long )__cil_tmp19;
1774#line 226
1775 __cil_tmp21 = __cil_tmp20 + 4;
1776#line 226
1777 __cil_tmp22 = *((int *)__cil_tmp21);
1778#line 226
1779 __cil_tmp23 = *reg;
1780#line 226
1781 *reg = __cil_tmp23 | __cil_tmp22;
1782#line 227
1783 __cil_tmp24 = & descriptor;
1784#line 227
1785 *((char const **)__cil_tmp24) = "wm831x_power";
1786#line 227
1787 __cil_tmp25 = (unsigned long )(& descriptor) + 8;
1788#line 227
1789 *((char const **)__cil_tmp25) = "wm831x_battey_apply_config";
1790#line 227
1791 __cil_tmp26 = (unsigned long )(& descriptor) + 16;
1792#line 227
1793 *((char const **)__cil_tmp26) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p";
1794#line 227
1795 __cil_tmp27 = (unsigned long )(& descriptor) + 24;
1796#line 227
1797 *((char const **)__cil_tmp27) = "Set %s of %d%s\n";
1798#line 227
1799 __cil_tmp28 = (unsigned long )(& descriptor) + 32;
1800#line 227
1801 *((unsigned int *)__cil_tmp28) = 227U;
1802#line 227
1803 __cil_tmp29 = (unsigned long )(& descriptor) + 35;
1804#line 227
1805 *((unsigned char *)__cil_tmp29) = (unsigned char)1;
1806#line 227
1807 __cil_tmp30 = (unsigned long )(& descriptor) + 35;
1808#line 227
1809 __cil_tmp31 = *((unsigned char *)__cil_tmp30);
1810#line 227
1811 __cil_tmp32 = (long )__cil_tmp31;
1812#line 227
1813 __cil_tmp33 = __cil_tmp32 & 1L;
1814#line 227
1815 tmp = __builtin_expect(__cil_tmp33, 0L);
1816 }
1817#line 227
1818 if (tmp != 0L) {
1819 {
1820#line 227
1821 __cil_tmp34 = (unsigned long )wm831x;
1822#line 227
1823 __cil_tmp35 = __cil_tmp34 + 168;
1824#line 227
1825 __cil_tmp36 = *((struct device **)__cil_tmp35);
1826#line 227
1827 __cil_tmp37 = (struct device const *)__cil_tmp36;
1828#line 227
1829 __dynamic_dev_dbg(& descriptor, __cil_tmp37, "Set %s of %d%s\n", name, val,
1830 units);
1831 }
1832 } else {
1833
1834 }
1835 }
1836#line 230
1837 return;
1838}
1839}
1840#line 231 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
1841static void wm831x_config_battery(struct wm831x *wm831x )
1842{ struct wm831x_pdata *wm831x_pdata ;
1843 struct wm831x_battery_pdata *pdata ;
1844 int ret ;
1845 int reg1 ;
1846 int reg2 ;
1847 unsigned long __cil_tmp7 ;
1848 unsigned long __cil_tmp8 ;
1849 struct device *__cil_tmp9 ;
1850 unsigned long __cil_tmp10 ;
1851 unsigned long __cil_tmp11 ;
1852 void *__cil_tmp12 ;
1853 struct wm831x_pdata *__cil_tmp13 ;
1854 unsigned long __cil_tmp14 ;
1855 unsigned long __cil_tmp15 ;
1856 unsigned long __cil_tmp16 ;
1857 unsigned long __cil_tmp17 ;
1858 struct device *__cil_tmp18 ;
1859 struct device const *__cil_tmp19 ;
1860 struct wm831x_battery_pdata *__cil_tmp20 ;
1861 unsigned long __cil_tmp21 ;
1862 unsigned long __cil_tmp22 ;
1863 unsigned long __cil_tmp23 ;
1864 struct wm831x_battery_pdata *__cil_tmp24 ;
1865 unsigned long __cil_tmp25 ;
1866 unsigned long __cil_tmp26 ;
1867 unsigned long __cil_tmp27 ;
1868 struct device *__cil_tmp28 ;
1869 struct device const *__cil_tmp29 ;
1870 unsigned long __cil_tmp30 ;
1871 unsigned long __cil_tmp31 ;
1872 int *__cil_tmp32 ;
1873 int *__cil_tmp33 ;
1874 int __cil_tmp34 ;
1875 unsigned long __cil_tmp35 ;
1876 unsigned long __cil_tmp36 ;
1877 struct device *__cil_tmp37 ;
1878 struct device const *__cil_tmp38 ;
1879 int *__cil_tmp39 ;
1880 int *__cil_tmp40 ;
1881 int __cil_tmp41 ;
1882 unsigned long __cil_tmp42 ;
1883 unsigned long __cil_tmp43 ;
1884 int __cil_tmp44 ;
1885 int *__cil_tmp45 ;
1886 int *__cil_tmp46 ;
1887 int __cil_tmp47 ;
1888 unsigned long __cil_tmp48 ;
1889 unsigned long __cil_tmp49 ;
1890 int __cil_tmp50 ;
1891 int *__cil_tmp51 ;
1892 int *__cil_tmp52 ;
1893 int __cil_tmp53 ;
1894 struct chg_map *__cil_tmp54 ;
1895 unsigned long __cil_tmp55 ;
1896 unsigned long __cil_tmp56 ;
1897 int __cil_tmp57 ;
1898 struct chg_map *__cil_tmp58 ;
1899 unsigned long __cil_tmp59 ;
1900 unsigned long __cil_tmp60 ;
1901 int __cil_tmp61 ;
1902 struct chg_map *__cil_tmp62 ;
1903 unsigned long __cil_tmp63 ;
1904 unsigned long __cil_tmp64 ;
1905 int __cil_tmp65 ;
1906 struct chg_map *__cil_tmp66 ;
1907 unsigned long __cil_tmp67 ;
1908 unsigned long __cil_tmp68 ;
1909 int __cil_tmp69 ;
1910 struct chg_map *__cil_tmp70 ;
1911 unsigned long __cil_tmp71 ;
1912 unsigned long __cil_tmp72 ;
1913 int __cil_tmp73 ;
1914 unsigned long __cil_tmp74 ;
1915 unsigned long __cil_tmp75 ;
1916 struct device *__cil_tmp76 ;
1917 struct device const *__cil_tmp77 ;
1918 int *__cil_tmp78 ;
1919 int __cil_tmp79 ;
1920 unsigned short __cil_tmp80 ;
1921 int __cil_tmp81 ;
1922 unsigned short __cil_tmp82 ;
1923 unsigned long __cil_tmp83 ;
1924 unsigned long __cil_tmp84 ;
1925 struct device *__cil_tmp85 ;
1926 struct device const *__cil_tmp86 ;
1927 int *__cil_tmp87 ;
1928 int __cil_tmp88 ;
1929 unsigned short __cil_tmp89 ;
1930 int __cil_tmp90 ;
1931 unsigned short __cil_tmp91 ;
1932 unsigned long __cil_tmp92 ;
1933 unsigned long __cil_tmp93 ;
1934 struct device *__cil_tmp94 ;
1935 struct device const *__cil_tmp95 ;
1936
1937 {
1938#line 233
1939 __cil_tmp7 = (unsigned long )wm831x;
1940#line 233
1941 __cil_tmp8 = __cil_tmp7 + 168;
1942#line 233
1943 __cil_tmp9 = *((struct device **)__cil_tmp8);
1944#line 233
1945 __cil_tmp10 = (unsigned long )__cil_tmp9;
1946#line 233
1947 __cil_tmp11 = __cil_tmp10 + 280;
1948#line 233
1949 __cil_tmp12 = *((void **)__cil_tmp11);
1950#line 233
1951 wm831x_pdata = (struct wm831x_pdata *)__cil_tmp12;
1952 {
1953#line 237
1954 __cil_tmp13 = (struct wm831x_pdata *)0;
1955#line 237
1956 __cil_tmp14 = (unsigned long )__cil_tmp13;
1957#line 237
1958 __cil_tmp15 = (unsigned long )wm831x_pdata;
1959#line 237
1960 if (__cil_tmp15 == __cil_tmp14) {
1961 {
1962#line 238
1963 __cil_tmp16 = (unsigned long )wm831x;
1964#line 238
1965 __cil_tmp17 = __cil_tmp16 + 168;
1966#line 238
1967 __cil_tmp18 = *((struct device **)__cil_tmp17);
1968#line 238
1969 __cil_tmp19 = (struct device const *)__cil_tmp18;
1970#line 238
1971 dev_warn(__cil_tmp19, "No battery charger configuration\n");
1972 }
1973#line 240
1974 return;
1975 } else {
1976 {
1977#line 237
1978 __cil_tmp20 = (struct wm831x_battery_pdata *)0;
1979#line 237
1980 __cil_tmp21 = (unsigned long )__cil_tmp20;
1981#line 237
1982 __cil_tmp22 = (unsigned long )wm831x_pdata;
1983#line 237
1984 __cil_tmp23 = __cil_tmp22 + 120;
1985#line 237
1986 __cil_tmp24 = *((struct wm831x_battery_pdata **)__cil_tmp23);
1987#line 237
1988 __cil_tmp25 = (unsigned long )__cil_tmp24;
1989#line 237
1990 if (__cil_tmp25 == __cil_tmp21) {
1991 {
1992#line 238
1993 __cil_tmp26 = (unsigned long )wm831x;
1994#line 238
1995 __cil_tmp27 = __cil_tmp26 + 168;
1996#line 238
1997 __cil_tmp28 = *((struct device **)__cil_tmp27);
1998#line 238
1999 __cil_tmp29 = (struct device const *)__cil_tmp28;
2000#line 238
2001 dev_warn(__cil_tmp29, "No battery charger configuration\n");
2002 }
2003#line 240
2004 return;
2005 } else {
2006
2007 }
2008 }
2009 }
2010 }
2011#line 243
2012 __cil_tmp30 = (unsigned long )wm831x_pdata;
2013#line 243
2014 __cil_tmp31 = __cil_tmp30 + 120;
2015#line 243
2016 pdata = *((struct wm831x_battery_pdata **)__cil_tmp31);
2017#line 245
2018 __cil_tmp32 = & reg1;
2019#line 245
2020 *__cil_tmp32 = 0;
2021#line 246
2022 __cil_tmp33 = & reg2;
2023#line 246
2024 *__cil_tmp33 = 0;
2025 {
2026#line 248
2027 __cil_tmp34 = *((int *)pdata);
2028#line 248
2029 if (__cil_tmp34 == 0) {
2030 {
2031#line 249
2032 __cil_tmp35 = (unsigned long )wm831x;
2033#line 249
2034 __cil_tmp36 = __cil_tmp35 + 168;
2035#line 249
2036 __cil_tmp37 = *((struct device **)__cil_tmp36);
2037#line 249
2038 __cil_tmp38 = (struct device const *)__cil_tmp37;
2039#line 249
2040 _dev_info(__cil_tmp38, "Battery charger disabled\n");
2041 }
2042#line 250
2043 return;
2044 } else {
2045
2046 }
2047 }
2048#line 253
2049 __cil_tmp39 = & reg1;
2050#line 253
2051 __cil_tmp40 = & reg1;
2052#line 253
2053 __cil_tmp41 = *__cil_tmp40;
2054#line 253
2055 *__cil_tmp39 = __cil_tmp41 | 32768;
2056 {
2057#line 254
2058 __cil_tmp42 = (unsigned long )pdata;
2059#line 254
2060 __cil_tmp43 = __cil_tmp42 + 8;
2061#line 254
2062 __cil_tmp44 = *((int *)__cil_tmp43);
2063#line 254
2064 if (__cil_tmp44 != 0) {
2065#line 255
2066 __cil_tmp45 = & reg2;
2067#line 255
2068 __cil_tmp46 = & reg2;
2069#line 255
2070 __cil_tmp47 = *__cil_tmp46;
2071#line 255
2072 *__cil_tmp45 = __cil_tmp47 | 16384;
2073 } else {
2074
2075 }
2076 }
2077 {
2078#line 256
2079 __cil_tmp48 = (unsigned long )pdata;
2080#line 256
2081 __cil_tmp49 = __cil_tmp48 + 4;
2082#line 256
2083 __cil_tmp50 = *((int *)__cil_tmp49);
2084#line 256
2085 if (__cil_tmp50 != 0) {
2086#line 257
2087 __cil_tmp51 = & reg1;
2088#line 257
2089 __cil_tmp52 = & reg1;
2090#line 257
2091 __cil_tmp53 = *__cil_tmp52;
2092#line 257
2093 *__cil_tmp51 = __cil_tmp53 | 32;
2094 } else {
2095
2096 }
2097 }
2098 {
2099#line 259
2100 __cil_tmp54 = (struct chg_map *)(& trickle_ilims);
2101#line 259
2102 __cil_tmp55 = (unsigned long )pdata;
2103#line 259
2104 __cil_tmp56 = __cil_tmp55 + 12;
2105#line 259
2106 __cil_tmp57 = *((int *)__cil_tmp56);
2107#line 259
2108 wm831x_battey_apply_config(wm831x, __cil_tmp54, 4, __cil_tmp57, & reg2, "trickle charge current limit",
2109 "mA");
2110#line 264
2111 __cil_tmp58 = (struct chg_map *)(& vsels);
2112#line 264
2113 __cil_tmp59 = (unsigned long )pdata;
2114#line 264
2115 __cil_tmp60 = __cil_tmp59 + 16;
2116#line 264
2117 __cil_tmp61 = *((int *)__cil_tmp60);
2118#line 264
2119 wm831x_battey_apply_config(wm831x, __cil_tmp58, 4, __cil_tmp61, & reg2, "target voltage",
2120 "mV");
2121#line 268
2122 __cil_tmp62 = (struct chg_map *)(& fast_ilims);
2123#line 268
2124 __cil_tmp63 = (unsigned long )pdata;
2125#line 268
2126 __cil_tmp64 = __cil_tmp63 + 24;
2127#line 268
2128 __cil_tmp65 = *((int *)__cil_tmp64);
2129#line 268
2130 wm831x_battey_apply_config(wm831x, __cil_tmp62, 16, __cil_tmp65, & reg2, "fast charge current limit",
2131 "mA");
2132#line 272
2133 __cil_tmp66 = (struct chg_map *)(& eoc_iterms);
2134#line 272
2135 __cil_tmp67 = (unsigned long )pdata;
2136#line 272
2137 __cil_tmp68 = __cil_tmp67 + 20;
2138#line 272
2139 __cil_tmp69 = *((int *)__cil_tmp68);
2140#line 272
2141 wm831x_battey_apply_config(wm831x, __cil_tmp66, 8, __cil_tmp69, & reg1, "end of charge current threshold",
2142 "mA");
2143#line 276
2144 __cil_tmp70 = (struct chg_map *)(& chg_times);
2145#line 276
2146 __cil_tmp71 = (unsigned long )pdata;
2147#line 276
2148 __cil_tmp72 = __cil_tmp71 + 28;
2149#line 276
2150 __cil_tmp73 = *((int *)__cil_tmp72);
2151#line 276
2152 wm831x_battey_apply_config(wm831x, __cil_tmp70, 16, __cil_tmp73, & reg2, "charger timeout",
2153 "min");
2154#line 280
2155 ret = wm831x_reg_unlock(wm831x);
2156 }
2157#line 281
2158 if (ret != 0) {
2159 {
2160#line 282
2161 __cil_tmp74 = (unsigned long )wm831x;
2162#line 282
2163 __cil_tmp75 = __cil_tmp74 + 168;
2164#line 282
2165 __cil_tmp76 = *((struct device **)__cil_tmp75);
2166#line 282
2167 __cil_tmp77 = (struct device const *)__cil_tmp76;
2168#line 282
2169 dev_err(__cil_tmp77, "Failed to unlock registers: %d\n", ret);
2170 }
2171#line 283
2172 return;
2173 } else {
2174
2175 }
2176 {
2177#line 286
2178 __cil_tmp78 = & reg1;
2179#line 286
2180 __cil_tmp79 = *__cil_tmp78;
2181#line 286
2182 __cil_tmp80 = (unsigned short )__cil_tmp79;
2183#line 286
2184 __cil_tmp81 = (int )__cil_tmp80;
2185#line 286
2186 __cil_tmp82 = (unsigned short )__cil_tmp81;
2187#line 286
2188 ret = wm831x_set_bits(wm831x, (unsigned short)16456, (unsigned short)39968, __cil_tmp82);
2189 }
2190#line 291
2191 if (ret != 0) {
2192 {
2193#line 292
2194 __cil_tmp83 = (unsigned long )wm831x;
2195#line 292
2196 __cil_tmp84 = __cil_tmp83 + 168;
2197#line 292
2198 __cil_tmp85 = *((struct device **)__cil_tmp84);
2199#line 292
2200 __cil_tmp86 = (struct device const *)__cil_tmp85;
2201#line 292
2202 dev_err(__cil_tmp86, "Failed to set charger control 1: %d\n", ret);
2203 }
2204 } else {
2205
2206 }
2207 {
2208#line 295
2209 __cil_tmp87 = & reg2;
2210#line 295
2211 __cil_tmp88 = *__cil_tmp87;
2212#line 295
2213 __cil_tmp89 = (unsigned short )__cil_tmp88;
2214#line 295
2215 __cil_tmp90 = (int )__cil_tmp89;
2216#line 295
2217 __cil_tmp91 = (unsigned short )__cil_tmp90;
2218#line 295
2219 ret = wm831x_set_bits(wm831x, (unsigned short)16457, (unsigned short)20479, __cil_tmp91);
2220 }
2221#line 302
2222 if (ret != 0) {
2223 {
2224#line 303
2225 __cil_tmp92 = (unsigned long )wm831x;
2226#line 303
2227 __cil_tmp93 = __cil_tmp92 + 168;
2228#line 303
2229 __cil_tmp94 = *((struct device **)__cil_tmp93);
2230#line 303
2231 __cil_tmp95 = (struct device const *)__cil_tmp94;
2232#line 303
2233 dev_err(__cil_tmp95, "Failed to set charger control 2: %d\n", ret);
2234 }
2235 } else {
2236
2237 }
2238 {
2239#line 306
2240 wm831x_reg_lock(wm831x);
2241 }
2242#line 307
2243 return;
2244}
2245}
2246#line 309 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
2247static int wm831x_bat_check_status(struct wm831x *wm831x , int *status )
2248{ int ret ;
2249 int __cil_tmp4 ;
2250
2251 {
2252 {
2253#line 313
2254 ret = wm831x_reg_read(wm831x, (unsigned short)16397);
2255 }
2256#line 314
2257 if (ret < 0) {
2258#line 315
2259 return (ret);
2260 } else {
2261
2262 }
2263 {
2264#line 317
2265 __cil_tmp4 = ret & 1024;
2266#line 317
2267 if (__cil_tmp4 != 0) {
2268#line 318
2269 *status = 2;
2270#line 319
2271 return (0);
2272 } else {
2273
2274 }
2275 }
2276 {
2277#line 322
2278 ret = wm831x_reg_read(wm831x, (unsigned short)16458);
2279 }
2280#line 323
2281 if (ret < 0) {
2282#line 324
2283 return (ret);
2284 } else {
2285
2286 }
2287#line 327
2288 if ((ret & 28672) == 0) {
2289#line 327
2290 goto case_0;
2291 } else
2292#line 330
2293 if ((ret & 28672) == 4096) {
2294#line 330
2295 goto case_4096;
2296 } else
2297#line 331
2298 if ((ret & 28672) == 8192) {
2299#line 331
2300 goto case_8192;
2301 } else {
2302 {
2303#line 335
2304 goto switch_default;
2305#line 326
2306 if (0) {
2307 case_0:
2308#line 328
2309 *status = 3;
2310#line 329
2311 goto ldv_17579;
2312 case_4096: ;
2313 case_8192:
2314#line 332
2315 *status = 1;
2316#line 333
2317 goto ldv_17579;
2318 switch_default:
2319#line 336
2320 *status = 0;
2321#line 337
2322 goto ldv_17579;
2323 } else {
2324 switch_break: ;
2325 }
2326 }
2327 }
2328 ldv_17579: ;
2329#line 340
2330 return (0);
2331}
2332}
2333#line 343 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
2334static int wm831x_bat_check_type(struct wm831x *wm831x , int *type )
2335{ int ret ;
2336
2337 {
2338 {
2339#line 347
2340 ret = wm831x_reg_read(wm831x, (unsigned short)16458);
2341 }
2342#line 348
2343 if (ret < 0) {
2344#line 349
2345 return (ret);
2346 } else {
2347
2348 }
2349#line 352
2350 if ((ret & 28672) == 4096) {
2351#line 352
2352 goto case_4096;
2353 } else
2354#line 353
2355 if ((ret & 28672) == 12288) {
2356#line 353
2357 goto case_12288;
2358 } else
2359#line 356
2360 if ((ret & 28672) == 8192) {
2361#line 356
2362 goto case_8192;
2363 } else
2364#line 357
2365 if ((ret & 28672) == 16384) {
2366#line 357
2367 goto case_16384;
2368 } else {
2369 {
2370#line 360
2371 goto switch_default;
2372#line 351
2373 if (0) {
2374 case_4096: ;
2375 case_12288:
2376#line 354
2377 *type = 2;
2378#line 355
2379 goto ldv_17590;
2380 case_8192: ;
2381 case_16384:
2382#line 358
2383 *type = 3;
2384#line 359
2385 goto ldv_17590;
2386 switch_default:
2387#line 361
2388 *type = 1;
2389#line 362
2390 goto ldv_17590;
2391 } else {
2392 switch_break: ;
2393 }
2394 }
2395 }
2396 ldv_17590: ;
2397#line 365
2398 return (0);
2399}
2400}
2401#line 368 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
2402static int wm831x_bat_check_health(struct wm831x *wm831x , int *health )
2403{ int ret ;
2404 int __cil_tmp4 ;
2405 int __cil_tmp5 ;
2406 int __cil_tmp6 ;
2407
2408 {
2409 {
2410#line 372
2411 ret = wm831x_reg_read(wm831x, (unsigned short)16458);
2412 }
2413#line 373
2414 if (ret < 0) {
2415#line 374
2416 return (ret);
2417 } else {
2418
2419 }
2420 {
2421#line 376
2422 __cil_tmp4 = ret & 2048;
2423#line 376
2424 if (__cil_tmp4 != 0) {
2425#line 377
2426 *health = 2;
2427#line 378
2428 return (0);
2429 } else {
2430
2431 }
2432 }
2433 {
2434#line 381
2435 __cil_tmp5 = ret & 1024;
2436#line 381
2437 if (__cil_tmp5 != 0) {
2438#line 382
2439 *health = 6;
2440#line 383
2441 return (0);
2442 } else {
2443
2444 }
2445 }
2446 {
2447#line 386
2448 __cil_tmp6 = ret & 32768;
2449#line 386
2450 if (__cil_tmp6 != 0) {
2451#line 387
2452 *health = 4;
2453#line 388
2454 return (0);
2455 } else {
2456
2457 }
2458 }
2459#line 392
2460 if ((ret & 28672) == 12288) {
2461#line 392
2462 goto case_12288;
2463 } else
2464#line 393
2465 if ((ret & 28672) == 16384) {
2466#line 393
2467 goto case_16384;
2468 } else
2469#line 396
2470 if ((ret & 28672) == 20480) {
2471#line 396
2472 goto case_20480;
2473 } else {
2474 {
2475#line 399
2476 goto switch_default;
2477#line 391
2478 if (0) {
2479 case_12288: ;
2480 case_16384:
2481#line 394
2482 *health = 2;
2483#line 395
2484 goto ldv_17601;
2485 case_20480:
2486#line 397
2487 *health = 5;
2488#line 398
2489 goto ldv_17601;
2490 switch_default:
2491#line 400
2492 *health = 1;
2493#line 401
2494 goto ldv_17601;
2495 } else {
2496 switch_break: ;
2497 }
2498 }
2499 }
2500 ldv_17601: ;
2501#line 404
2502 return (0);
2503}
2504}
2505#line 407 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
2506static int wm831x_bat_get_prop(struct power_supply *psy , enum power_supply_property psp ,
2507 union power_supply_propval *val )
2508{ struct wm831x_power *wm831x_power ;
2509 void *tmp ;
2510 struct wm831x *wm831x ;
2511 int ret ;
2512 unsigned long __cil_tmp8 ;
2513 unsigned long __cil_tmp9 ;
2514 struct device *__cil_tmp10 ;
2515 struct device *__cil_tmp11 ;
2516 struct device const *__cil_tmp12 ;
2517 unsigned int __cil_tmp13 ;
2518 int *__cil_tmp14 ;
2519 enum wm831x_auxadc __cil_tmp15 ;
2520 int *__cil_tmp16 ;
2521 int *__cil_tmp17 ;
2522
2523 {
2524 {
2525#line 411
2526 __cil_tmp8 = (unsigned long )psy;
2527#line 411
2528 __cil_tmp9 = __cil_tmp8 + 96;
2529#line 411
2530 __cil_tmp10 = *((struct device **)__cil_tmp9);
2531#line 411
2532 __cil_tmp11 = *((struct device **)__cil_tmp10);
2533#line 411
2534 __cil_tmp12 = (struct device const *)__cil_tmp11;
2535#line 411
2536 tmp = dev_get_drvdata(__cil_tmp12);
2537#line 411
2538 wm831x_power = (struct wm831x_power *)tmp;
2539#line 412
2540 wm831x = *((struct wm831x **)wm831x_power);
2541#line 413
2542 ret = 0;
2543 }
2544 {
2545#line 415
2546 __cil_tmp13 = (unsigned int )psp;
2547#line 416
2548 if ((int )__cil_tmp13 == 0) {
2549#line 416
2550 goto case_0;
2551 } else
2552#line 419
2553 if ((int )__cil_tmp13 == 4) {
2554#line 419
2555 goto case_4;
2556 } else
2557#line 423
2558 if ((int )__cil_tmp13 == 11) {
2559#line 423
2560 goto case_11;
2561 } else
2562#line 426
2563 if ((int )__cil_tmp13 == 2) {
2564#line 426
2565 goto case_2;
2566 } else
2567#line 429
2568 if ((int )__cil_tmp13 == 1) {
2569#line 429
2570 goto case_1;
2571 } else {
2572 {
2573#line 432
2574 goto switch_default;
2575#line 415
2576 if (0) {
2577 case_0:
2578 {
2579#line 417
2580 __cil_tmp14 = (int *)val;
2581#line 417
2582 ret = wm831x_bat_check_status(wm831x, __cil_tmp14);
2583 }
2584#line 418
2585 goto ldv_17613;
2586 case_4:
2587 {
2588#line 420
2589 ret = wm831x_power_check_online(wm831x, 1024, val);
2590 }
2591#line 422
2592 goto ldv_17613;
2593 case_11:
2594 {
2595#line 424
2596 __cil_tmp15 = (enum wm831x_auxadc )8;
2597#line 424
2598 ret = wm831x_power_read_voltage(wm831x, __cil_tmp15, val);
2599 }
2600#line 425
2601 goto ldv_17613;
2602 case_2:
2603 {
2604#line 427
2605 __cil_tmp16 = (int *)val;
2606#line 427
2607 ret = wm831x_bat_check_health(wm831x, __cil_tmp16);
2608 }
2609#line 428
2610 goto ldv_17613;
2611 case_1:
2612 {
2613#line 430
2614 __cil_tmp17 = (int *)val;
2615#line 430
2616 ret = wm831x_bat_check_type(wm831x, __cil_tmp17);
2617 }
2618#line 431
2619 goto ldv_17613;
2620 switch_default:
2621#line 433
2622 ret = -22;
2623#line 434
2624 goto ldv_17613;
2625 } else {
2626 switch_break: ;
2627 }
2628 }
2629 }
2630 }
2631 ldv_17613: ;
2632#line 437
2633 return (ret);
2634}
2635}
2636#line 440 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
2637static enum power_supply_property wm831x_bat_props[5U] = { (enum power_supply_property )0, (enum power_supply_property )4, (enum power_supply_property )11, (enum power_supply_property )2,
2638 (enum power_supply_property )1};
2639#line 448 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
2640static char const *wm831x_bat_irqs[8U] =
2641#line 448
2642 { "BATT HOT", "BATT COLD", "BATT FAIL", "OV",
2643 "END", "TO", "MODE", "START"};
2644#line 459 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
2645static irqreturn_t wm831x_bat_irq(int irq , void *data )
2646{ struct wm831x_power *wm831x_power ;
2647 struct wm831x *wm831x ;
2648 struct _ddebug descriptor ;
2649 long tmp ;
2650 struct _ddebug *__cil_tmp7 ;
2651 unsigned long __cil_tmp8 ;
2652 unsigned long __cil_tmp9 ;
2653 unsigned long __cil_tmp10 ;
2654 unsigned long __cil_tmp11 ;
2655 unsigned long __cil_tmp12 ;
2656 unsigned long __cil_tmp13 ;
2657 unsigned char __cil_tmp14 ;
2658 long __cil_tmp15 ;
2659 long __cil_tmp16 ;
2660 unsigned long __cil_tmp17 ;
2661 unsigned long __cil_tmp18 ;
2662 struct device *__cil_tmp19 ;
2663 struct device const *__cil_tmp20 ;
2664 unsigned long __cil_tmp21 ;
2665 unsigned long __cil_tmp22 ;
2666 bool __cil_tmp23 ;
2667 unsigned long __cil_tmp24 ;
2668 unsigned long __cil_tmp25 ;
2669 struct power_supply *__cil_tmp26 ;
2670
2671 {
2672 {
2673#line 461
2674 wm831x_power = (struct wm831x_power *)data;
2675#line 462
2676 wm831x = *((struct wm831x **)wm831x_power);
2677#line 464
2678 __cil_tmp7 = & descriptor;
2679#line 464
2680 *((char const **)__cil_tmp7) = "wm831x_power";
2681#line 464
2682 __cil_tmp8 = (unsigned long )(& descriptor) + 8;
2683#line 464
2684 *((char const **)__cil_tmp8) = "wm831x_bat_irq";
2685#line 464
2686 __cil_tmp9 = (unsigned long )(& descriptor) + 16;
2687#line 464
2688 *((char const **)__cil_tmp9) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p";
2689#line 464
2690 __cil_tmp10 = (unsigned long )(& descriptor) + 24;
2691#line 464
2692 *((char const **)__cil_tmp10) = "Battery status changed: %d\n";
2693#line 464
2694 __cil_tmp11 = (unsigned long )(& descriptor) + 32;
2695#line 464
2696 *((unsigned int *)__cil_tmp11) = 464U;
2697#line 464
2698 __cil_tmp12 = (unsigned long )(& descriptor) + 35;
2699#line 464
2700 *((unsigned char *)__cil_tmp12) = (unsigned char)1;
2701#line 464
2702 __cil_tmp13 = (unsigned long )(& descriptor) + 35;
2703#line 464
2704 __cil_tmp14 = *((unsigned char *)__cil_tmp13);
2705#line 464
2706 __cil_tmp15 = (long )__cil_tmp14;
2707#line 464
2708 __cil_tmp16 = __cil_tmp15 & 1L;
2709#line 464
2710 tmp = __builtin_expect(__cil_tmp16, 0L);
2711 }
2712#line 464
2713 if (tmp != 0L) {
2714 {
2715#line 464
2716 __cil_tmp17 = (unsigned long )wm831x;
2717#line 464
2718 __cil_tmp18 = __cil_tmp17 + 168;
2719#line 464
2720 __cil_tmp19 = *((struct device **)__cil_tmp18);
2721#line 464
2722 __cil_tmp20 = (struct device const *)__cil_tmp19;
2723#line 464
2724 __dynamic_dev_dbg(& descriptor, __cil_tmp20, "Battery status changed: %d\n", irq);
2725 }
2726 } else {
2727
2728 }
2729 {
2730#line 468
2731 __cil_tmp21 = (unsigned long )wm831x_power;
2732#line 468
2733 __cil_tmp22 = __cil_tmp21 + 860;
2734#line 468
2735 __cil_tmp23 = *((bool *)__cil_tmp22);
2736#line 468
2737 if ((int )__cil_tmp23) {
2738 {
2739#line 469
2740 __cil_tmp24 = (unsigned long )wm831x_power;
2741#line 469
2742 __cil_tmp25 = __cil_tmp24 + 536;
2743#line 469
2744 __cil_tmp26 = (struct power_supply *)__cil_tmp25;
2745#line 469
2746 power_supply_changed(__cil_tmp26);
2747 }
2748 } else {
2749
2750 }
2751 }
2752#line 471
2753 return ((irqreturn_t )1);
2754}
2755}
2756#line 479 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
2757static irqreturn_t wm831x_syslo_irq(int irq , void *data )
2758{ struct wm831x_power *wm831x_power ;
2759 struct wm831x *wm831x ;
2760 unsigned long __cil_tmp5 ;
2761 unsigned long __cil_tmp6 ;
2762 struct device *__cil_tmp7 ;
2763 struct device const *__cil_tmp8 ;
2764
2765 {
2766 {
2767#line 481
2768 wm831x_power = (struct wm831x_power *)data;
2769#line 482
2770 wm831x = *((struct wm831x **)wm831x_power);
2771#line 486
2772 __cil_tmp5 = (unsigned long )wm831x;
2773#line 486
2774 __cil_tmp6 = __cil_tmp5 + 168;
2775#line 486
2776 __cil_tmp7 = *((struct device **)__cil_tmp6);
2777#line 486
2778 __cil_tmp8 = (struct device const *)__cil_tmp7;
2779#line 486
2780 dev_crit(__cil_tmp8, "SYSVDD under voltage\n");
2781 }
2782#line 488
2783 return ((irqreturn_t )1);
2784}
2785}
2786#line 491 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
2787static irqreturn_t wm831x_pwr_src_irq(int irq , void *data )
2788{ struct wm831x_power *wm831x_power ;
2789 struct wm831x *wm831x ;
2790 struct _ddebug descriptor ;
2791 long tmp ;
2792 struct _ddebug *__cil_tmp7 ;
2793 unsigned long __cil_tmp8 ;
2794 unsigned long __cil_tmp9 ;
2795 unsigned long __cil_tmp10 ;
2796 unsigned long __cil_tmp11 ;
2797 unsigned long __cil_tmp12 ;
2798 unsigned long __cil_tmp13 ;
2799 unsigned char __cil_tmp14 ;
2800 long __cil_tmp15 ;
2801 long __cil_tmp16 ;
2802 unsigned long __cil_tmp17 ;
2803 unsigned long __cil_tmp18 ;
2804 struct device *__cil_tmp19 ;
2805 struct device const *__cil_tmp20 ;
2806 unsigned long __cil_tmp21 ;
2807 unsigned long __cil_tmp22 ;
2808 bool __cil_tmp23 ;
2809 unsigned long __cil_tmp24 ;
2810 unsigned long __cil_tmp25 ;
2811 struct power_supply *__cil_tmp26 ;
2812 unsigned long __cil_tmp27 ;
2813 unsigned long __cil_tmp28 ;
2814 struct power_supply *__cil_tmp29 ;
2815 unsigned long __cil_tmp30 ;
2816 unsigned long __cil_tmp31 ;
2817 struct power_supply *__cil_tmp32 ;
2818
2819 {
2820 {
2821#line 493
2822 wm831x_power = (struct wm831x_power *)data;
2823#line 494
2824 wm831x = *((struct wm831x **)wm831x_power);
2825#line 496
2826 __cil_tmp7 = & descriptor;
2827#line 496
2828 *((char const **)__cil_tmp7) = "wm831x_power";
2829#line 496
2830 __cil_tmp8 = (unsigned long )(& descriptor) + 8;
2831#line 496
2832 *((char const **)__cil_tmp8) = "wm831x_pwr_src_irq";
2833#line 496
2834 __cil_tmp9 = (unsigned long )(& descriptor) + 16;
2835#line 496
2836 *((char const **)__cil_tmp9) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p";
2837#line 496
2838 __cil_tmp10 = (unsigned long )(& descriptor) + 24;
2839#line 496
2840 *((char const **)__cil_tmp10) = "Power source changed\n";
2841#line 496
2842 __cil_tmp11 = (unsigned long )(& descriptor) + 32;
2843#line 496
2844 *((unsigned int *)__cil_tmp11) = 496U;
2845#line 496
2846 __cil_tmp12 = (unsigned long )(& descriptor) + 35;
2847#line 496
2848 *((unsigned char *)__cil_tmp12) = (unsigned char)1;
2849#line 496
2850 __cil_tmp13 = (unsigned long )(& descriptor) + 35;
2851#line 496
2852 __cil_tmp14 = *((unsigned char *)__cil_tmp13);
2853#line 496
2854 __cil_tmp15 = (long )__cil_tmp14;
2855#line 496
2856 __cil_tmp16 = __cil_tmp15 & 1L;
2857#line 496
2858 tmp = __builtin_expect(__cil_tmp16, 0L);
2859 }
2860#line 496
2861 if (tmp != 0L) {
2862 {
2863#line 496
2864 __cil_tmp17 = (unsigned long )wm831x;
2865#line 496
2866 __cil_tmp18 = __cil_tmp17 + 168;
2867#line 496
2868 __cil_tmp19 = *((struct device **)__cil_tmp18);
2869#line 496
2870 __cil_tmp20 = (struct device const *)__cil_tmp19;
2871#line 496
2872 __dynamic_dev_dbg(& descriptor, __cil_tmp20, "Power source changed\n");
2873 }
2874 } else {
2875
2876 }
2877 {
2878#line 499
2879 __cil_tmp21 = (unsigned long )wm831x_power;
2880#line 499
2881 __cil_tmp22 = __cil_tmp21 + 860;
2882#line 499
2883 __cil_tmp23 = *((bool *)__cil_tmp22);
2884#line 499
2885 if ((int )__cil_tmp23) {
2886 {
2887#line 500
2888 __cil_tmp24 = (unsigned long )wm831x_power;
2889#line 500
2890 __cil_tmp25 = __cil_tmp24 + 536;
2891#line 500
2892 __cil_tmp26 = (struct power_supply *)__cil_tmp25;
2893#line 500
2894 power_supply_changed(__cil_tmp26);
2895 }
2896 } else {
2897
2898 }
2899 }
2900 {
2901#line 501
2902 __cil_tmp27 = (unsigned long )wm831x_power;
2903#line 501
2904 __cil_tmp28 = __cil_tmp27 + 272;
2905#line 501
2906 __cil_tmp29 = (struct power_supply *)__cil_tmp28;
2907#line 501
2908 power_supply_changed(__cil_tmp29);
2909#line 502
2910 __cil_tmp30 = (unsigned long )wm831x_power;
2911#line 502
2912 __cil_tmp31 = __cil_tmp30 + 8;
2913#line 502
2914 __cil_tmp32 = (struct power_supply *)__cil_tmp31;
2915#line 502
2916 power_supply_changed(__cil_tmp32);
2917 }
2918#line 504
2919 return ((irqreturn_t )1);
2920}
2921}
2922#line 507 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
2923static int wm831x_power_probe(struct platform_device *pdev )
2924{ struct wm831x *wm831x ;
2925 void *tmp ;
2926 struct wm831x_pdata *wm831x_pdata ;
2927 struct wm831x_power *power ;
2928 struct power_supply *usb ;
2929 struct power_supply *battery ;
2930 struct power_supply *wall ;
2931 int ret ;
2932 int irq ;
2933 int i ;
2934 void *tmp___0 ;
2935 unsigned long __cil_tmp13 ;
2936 unsigned long __cil_tmp14 ;
2937 struct device *__cil_tmp15 ;
2938 struct device const *__cil_tmp16 ;
2939 unsigned long __cil_tmp17 ;
2940 unsigned long __cil_tmp18 ;
2941 struct device *__cil_tmp19 ;
2942 unsigned long __cil_tmp20 ;
2943 unsigned long __cil_tmp21 ;
2944 void *__cil_tmp22 ;
2945 struct wm831x_power *__cil_tmp23 ;
2946 unsigned long __cil_tmp24 ;
2947 unsigned long __cil_tmp25 ;
2948 void *__cil_tmp26 ;
2949 unsigned long __cil_tmp27 ;
2950 unsigned long __cil_tmp28 ;
2951 unsigned long __cil_tmp29 ;
2952 unsigned long __cil_tmp30 ;
2953 unsigned long __cil_tmp31 ;
2954 unsigned long __cil_tmp32 ;
2955 struct wm831x_pdata *__cil_tmp33 ;
2956 unsigned long __cil_tmp34 ;
2957 unsigned long __cil_tmp35 ;
2958 int __cil_tmp36 ;
2959 unsigned long __cil_tmp37 ;
2960 unsigned long __cil_tmp38 ;
2961 char (*__cil_tmp39)[20U] ;
2962 char *__cil_tmp40 ;
2963 int __cil_tmp41 ;
2964 unsigned long __cil_tmp42 ;
2965 unsigned long __cil_tmp43 ;
2966 char (*__cil_tmp44)[20U] ;
2967 char *__cil_tmp45 ;
2968 int __cil_tmp46 ;
2969 unsigned long __cil_tmp47 ;
2970 unsigned long __cil_tmp48 ;
2971 char (*__cil_tmp49)[20U] ;
2972 char *__cil_tmp50 ;
2973 int __cil_tmp51 ;
2974 unsigned long __cil_tmp52 ;
2975 unsigned long __cil_tmp53 ;
2976 char (*__cil_tmp54)[20U] ;
2977 char *__cil_tmp55 ;
2978 unsigned long __cil_tmp56 ;
2979 unsigned long __cil_tmp57 ;
2980 char (*__cil_tmp58)[20U] ;
2981 char *__cil_tmp59 ;
2982 unsigned long __cil_tmp60 ;
2983 unsigned long __cil_tmp61 ;
2984 char (*__cil_tmp62)[20U] ;
2985 char *__cil_tmp63 ;
2986 unsigned long __cil_tmp64 ;
2987 unsigned long __cil_tmp65 ;
2988 char (*__cil_tmp66)[20U] ;
2989 char *__cil_tmp67 ;
2990 unsigned long __cil_tmp68 ;
2991 unsigned long __cil_tmp69 ;
2992 char (*__cil_tmp70)[20U] ;
2993 char *__cil_tmp71 ;
2994 unsigned long __cil_tmp72 ;
2995 unsigned long __cil_tmp73 ;
2996 char (*__cil_tmp74)[20U] ;
2997 char *__cil_tmp75 ;
2998 unsigned long __cil_tmp76 ;
2999 unsigned long __cil_tmp77 ;
3000 char (*__cil_tmp78)[20U] ;
3001 unsigned long __cil_tmp79 ;
3002 unsigned long __cil_tmp80 ;
3003 unsigned long __cil_tmp81 ;
3004 unsigned long __cil_tmp82 ;
3005 unsigned long __cil_tmp83 ;
3006 unsigned long __cil_tmp84 ;
3007 unsigned long __cil_tmp85 ;
3008 unsigned long __cil_tmp86 ;
3009 unsigned long __cil_tmp87 ;
3010 unsigned long __cil_tmp88 ;
3011 struct device *__cil_tmp89 ;
3012 unsigned long __cil_tmp90 ;
3013 unsigned long __cil_tmp91 ;
3014 char (*__cil_tmp92)[20U] ;
3015 unsigned long __cil_tmp93 ;
3016 unsigned long __cil_tmp94 ;
3017 unsigned long __cil_tmp95 ;
3018 unsigned long __cil_tmp96 ;
3019 unsigned long __cil_tmp97 ;
3020 unsigned long __cil_tmp98 ;
3021 unsigned long __cil_tmp99 ;
3022 unsigned long __cil_tmp100 ;
3023 unsigned long __cil_tmp101 ;
3024 unsigned long __cil_tmp102 ;
3025 struct device *__cil_tmp103 ;
3026 unsigned long __cil_tmp104 ;
3027 unsigned long __cil_tmp105 ;
3028 int __cil_tmp106 ;
3029 int __cil_tmp107 ;
3030 unsigned long __cil_tmp108 ;
3031 unsigned long __cil_tmp109 ;
3032 bool __cil_tmp110 ;
3033 unsigned long __cil_tmp111 ;
3034 unsigned long __cil_tmp112 ;
3035 char (*__cil_tmp113)[20U] ;
3036 unsigned long __cil_tmp114 ;
3037 unsigned long __cil_tmp115 ;
3038 unsigned long __cil_tmp116 ;
3039 unsigned long __cil_tmp117 ;
3040 unsigned long __cil_tmp118 ;
3041 unsigned long __cil_tmp119 ;
3042 unsigned long __cil_tmp120 ;
3043 unsigned long __cil_tmp121 ;
3044 unsigned long __cil_tmp122 ;
3045 unsigned long __cil_tmp123 ;
3046 struct device *__cil_tmp124 ;
3047 unsigned int __cil_tmp125 ;
3048 irqreturn_t (*__cil_tmp126)(int , void * ) ;
3049 void *__cil_tmp127 ;
3050 unsigned long __cil_tmp128 ;
3051 unsigned long __cil_tmp129 ;
3052 struct device *__cil_tmp130 ;
3053 struct device const *__cil_tmp131 ;
3054 unsigned int __cil_tmp132 ;
3055 irqreturn_t (*__cil_tmp133)(int , void * ) ;
3056 void *__cil_tmp134 ;
3057 unsigned long __cil_tmp135 ;
3058 unsigned long __cil_tmp136 ;
3059 struct device *__cil_tmp137 ;
3060 struct device const *__cil_tmp138 ;
3061 unsigned long __cil_tmp139 ;
3062 unsigned long __cil_tmp140 ;
3063 char const *__cil_tmp141 ;
3064 unsigned int __cil_tmp142 ;
3065 irqreturn_t (*__cil_tmp143)(int , void * ) ;
3066 unsigned long __cil_tmp144 ;
3067 unsigned long __cil_tmp145 ;
3068 char const *__cil_tmp146 ;
3069 void *__cil_tmp147 ;
3070 unsigned long __cil_tmp148 ;
3071 unsigned long __cil_tmp149 ;
3072 struct device *__cil_tmp150 ;
3073 struct device const *__cil_tmp151 ;
3074 unsigned long __cil_tmp152 ;
3075 unsigned long __cil_tmp153 ;
3076 char const *__cil_tmp154 ;
3077 unsigned int __cil_tmp155 ;
3078 unsigned long __cil_tmp156 ;
3079 unsigned long __cil_tmp157 ;
3080 char const *__cil_tmp158 ;
3081 unsigned int __cil_tmp159 ;
3082 void *__cil_tmp160 ;
3083 unsigned int __cil_tmp161 ;
3084 void *__cil_tmp162 ;
3085 unsigned int __cil_tmp163 ;
3086 void *__cil_tmp164 ;
3087 unsigned long __cil_tmp165 ;
3088 unsigned long __cil_tmp166 ;
3089 bool __cil_tmp167 ;
3090 void const *__cil_tmp168 ;
3091
3092 {
3093 {
3094#line 509
3095 __cil_tmp13 = (unsigned long )pdev;
3096#line 509
3097 __cil_tmp14 = __cil_tmp13 + 16;
3098#line 509
3099 __cil_tmp15 = *((struct device **)__cil_tmp14);
3100#line 509
3101 __cil_tmp16 = (struct device const *)__cil_tmp15;
3102#line 509
3103 tmp = dev_get_drvdata(__cil_tmp16);
3104#line 509
3105 wm831x = (struct wm831x *)tmp;
3106#line 510
3107 __cil_tmp17 = (unsigned long )wm831x;
3108#line 510
3109 __cil_tmp18 = __cil_tmp17 + 168;
3110#line 510
3111 __cil_tmp19 = *((struct device **)__cil_tmp18);
3112#line 510
3113 __cil_tmp20 = (unsigned long )__cil_tmp19;
3114#line 510
3115 __cil_tmp21 = __cil_tmp20 + 280;
3116#line 510
3117 __cil_tmp22 = *((void **)__cil_tmp21);
3118#line 510
3119 wm831x_pdata = (struct wm831x_pdata *)__cil_tmp22;
3120#line 517
3121 tmp___0 = kzalloc(864UL, 208U);
3122#line 517
3123 power = (struct wm831x_power *)tmp___0;
3124 }
3125 {
3126#line 518
3127 __cil_tmp23 = (struct wm831x_power *)0;
3128#line 518
3129 __cil_tmp24 = (unsigned long )__cil_tmp23;
3130#line 518
3131 __cil_tmp25 = (unsigned long )power;
3132#line 518
3133 if (__cil_tmp25 == __cil_tmp24) {
3134#line 519
3135 return (-12);
3136 } else {
3137
3138 }
3139 }
3140 {
3141#line 521
3142 *((struct wm831x **)power) = wm831x;
3143#line 522
3144 __cil_tmp26 = (void *)power;
3145#line 522
3146 platform_set_drvdata(pdev, __cil_tmp26);
3147#line 524
3148 __cil_tmp27 = (unsigned long )power;
3149#line 524
3150 __cil_tmp28 = __cil_tmp27 + 272;
3151#line 524
3152 usb = (struct power_supply *)__cil_tmp28;
3153#line 525
3154 __cil_tmp29 = (unsigned long )power;
3155#line 525
3156 __cil_tmp30 = __cil_tmp29 + 536;
3157#line 525
3158 battery = (struct power_supply *)__cil_tmp30;
3159#line 526
3160 __cil_tmp31 = (unsigned long )power;
3161#line 526
3162 __cil_tmp32 = __cil_tmp31 + 8;
3163#line 526
3164 wall = (struct power_supply *)__cil_tmp32;
3165 }
3166 {
3167#line 528
3168 __cil_tmp33 = (struct wm831x_pdata *)0;
3169#line 528
3170 __cil_tmp34 = (unsigned long )__cil_tmp33;
3171#line 528
3172 __cil_tmp35 = (unsigned long )wm831x_pdata;
3173#line 528
3174 if (__cil_tmp35 != __cil_tmp34) {
3175 {
3176#line 528
3177 __cil_tmp36 = *((int *)wm831x_pdata);
3178#line 528
3179 if (__cil_tmp36 != 0) {
3180 {
3181#line 529
3182 __cil_tmp37 = (unsigned long )power;
3183#line 529
3184 __cil_tmp38 = __cil_tmp37 + 800;
3185#line 529
3186 __cil_tmp39 = (char (*)[20U])__cil_tmp38;
3187#line 529
3188 __cil_tmp40 = (char *)__cil_tmp39;
3189#line 529
3190 __cil_tmp41 = *((int *)wm831x_pdata);
3191#line 529
3192 snprintf(__cil_tmp40, 20UL, "wm831x-wall.%d", __cil_tmp41);
3193#line 531
3194 __cil_tmp42 = (unsigned long )power;
3195#line 531
3196 __cil_tmp43 = __cil_tmp42 + 840;
3197#line 531
3198 __cil_tmp44 = (char (*)[20U])__cil_tmp43;
3199#line 531
3200 __cil_tmp45 = (char *)__cil_tmp44;
3201#line 531
3202 __cil_tmp46 = *((int *)wm831x_pdata);
3203#line 531
3204 snprintf(__cil_tmp45, 20UL, "wm831x-battery.%d", __cil_tmp46);
3205#line 533
3206 __cil_tmp47 = (unsigned long )power;
3207#line 533
3208 __cil_tmp48 = __cil_tmp47 + 820;
3209#line 533
3210 __cil_tmp49 = (char (*)[20U])__cil_tmp48;
3211#line 533
3212 __cil_tmp50 = (char *)__cil_tmp49;
3213#line 533
3214 __cil_tmp51 = *((int *)wm831x_pdata);
3215#line 533
3216 snprintf(__cil_tmp50, 20UL, "wm831x-usb.%d", __cil_tmp51);
3217 }
3218 } else {
3219 {
3220#line 536
3221 __cil_tmp52 = (unsigned long )power;
3222#line 536
3223 __cil_tmp53 = __cil_tmp52 + 800;
3224#line 536
3225 __cil_tmp54 = (char (*)[20U])__cil_tmp53;
3226#line 536
3227 __cil_tmp55 = (char *)__cil_tmp54;
3228#line 536
3229 snprintf(__cil_tmp55, 20UL, "wm831x-wall");
3230#line 538
3231 __cil_tmp56 = (unsigned long )power;
3232#line 538
3233 __cil_tmp57 = __cil_tmp56 + 840;
3234#line 538
3235 __cil_tmp58 = (char (*)[20U])__cil_tmp57;
3236#line 538
3237 __cil_tmp59 = (char *)__cil_tmp58;
3238#line 538
3239 snprintf(__cil_tmp59, 20UL, "wm831x-battery");
3240#line 540
3241 __cil_tmp60 = (unsigned long )power;
3242#line 540
3243 __cil_tmp61 = __cil_tmp60 + 820;
3244#line 540
3245 __cil_tmp62 = (char (*)[20U])__cil_tmp61;
3246#line 540
3247 __cil_tmp63 = (char *)__cil_tmp62;
3248#line 540
3249 snprintf(__cil_tmp63, 20UL, "wm831x-usb");
3250 }
3251 }
3252 }
3253 } else {
3254 {
3255#line 536
3256 __cil_tmp64 = (unsigned long )power;
3257#line 536
3258 __cil_tmp65 = __cil_tmp64 + 800;
3259#line 536
3260 __cil_tmp66 = (char (*)[20U])__cil_tmp65;
3261#line 536
3262 __cil_tmp67 = (char *)__cil_tmp66;
3263#line 536
3264 snprintf(__cil_tmp67, 20UL, "wm831x-wall");
3265#line 538
3266 __cil_tmp68 = (unsigned long )power;
3267#line 538
3268 __cil_tmp69 = __cil_tmp68 + 840;
3269#line 538
3270 __cil_tmp70 = (char (*)[20U])__cil_tmp69;
3271#line 538
3272 __cil_tmp71 = (char *)__cil_tmp70;
3273#line 538
3274 snprintf(__cil_tmp71, 20UL, "wm831x-battery");
3275#line 540
3276 __cil_tmp72 = (unsigned long )power;
3277#line 540
3278 __cil_tmp73 = __cil_tmp72 + 820;
3279#line 540
3280 __cil_tmp74 = (char (*)[20U])__cil_tmp73;
3281#line 540
3282 __cil_tmp75 = (char *)__cil_tmp74;
3283#line 540
3284 snprintf(__cil_tmp75, 20UL, "wm831x-usb");
3285 }
3286 }
3287 }
3288 {
3289#line 547
3290 wm831x_config_battery(wm831x);
3291#line 549
3292 __cil_tmp76 = (unsigned long )power;
3293#line 549
3294 __cil_tmp77 = __cil_tmp76 + 800;
3295#line 549
3296 __cil_tmp78 = (char (*)[20U])__cil_tmp77;
3297#line 549
3298 *((char const **)wall) = (char const *)__cil_tmp78;
3299#line 550
3300 __cil_tmp79 = (unsigned long )wall;
3301#line 550
3302 __cil_tmp80 = __cil_tmp79 + 8;
3303#line 550
3304 *((enum power_supply_type *)__cil_tmp80) = (enum power_supply_type )3;
3305#line 551
3306 __cil_tmp81 = (unsigned long )wall;
3307#line 551
3308 __cil_tmp82 = __cil_tmp81 + 16;
3309#line 551
3310 *((enum power_supply_property **)__cil_tmp82) = (enum power_supply_property *)(& wm831x_wall_props);
3311#line 552
3312 __cil_tmp83 = (unsigned long )wall;
3313#line 552
3314 __cil_tmp84 = __cil_tmp83 + 24;
3315#line 552
3316 *((size_t *)__cil_tmp84) = 2UL;
3317#line 553
3318 __cil_tmp85 = (unsigned long )wall;
3319#line 553
3320 __cil_tmp86 = __cil_tmp85 + 48;
3321#line 553
3322 *((int (**)(struct power_supply * , enum power_supply_property , union power_supply_propval * ))__cil_tmp86) = & wm831x_wall_get_prop;
3323#line 554
3324 __cil_tmp87 = (unsigned long )pdev;
3325#line 554
3326 __cil_tmp88 = __cil_tmp87 + 16;
3327#line 554
3328 __cil_tmp89 = (struct device *)__cil_tmp88;
3329#line 554
3330 ret = power_supply_register(__cil_tmp89, wall);
3331 }
3332#line 555
3333 if (ret != 0) {
3334#line 556
3335 goto err_kmalloc;
3336 } else {
3337
3338 }
3339 {
3340#line 558
3341 __cil_tmp90 = (unsigned long )power;
3342#line 558
3343 __cil_tmp91 = __cil_tmp90 + 820;
3344#line 558
3345 __cil_tmp92 = (char (*)[20U])__cil_tmp91;
3346#line 558
3347 *((char const **)usb) = (char const *)__cil_tmp92;
3348#line 558
3349 __cil_tmp93 = (unsigned long )usb;
3350#line 558
3351 __cil_tmp94 = __cil_tmp93 + 8;
3352#line 558
3353 *((enum power_supply_type *)__cil_tmp94) = (enum power_supply_type )4;
3354#line 560
3355 __cil_tmp95 = (unsigned long )usb;
3356#line 560
3357 __cil_tmp96 = __cil_tmp95 + 16;
3358#line 560
3359 *((enum power_supply_property **)__cil_tmp96) = (enum power_supply_property *)(& wm831x_usb_props);
3360#line 561
3361 __cil_tmp97 = (unsigned long )usb;
3362#line 561
3363 __cil_tmp98 = __cil_tmp97 + 24;
3364#line 561
3365 *((size_t *)__cil_tmp98) = 2UL;
3366#line 562
3367 __cil_tmp99 = (unsigned long )usb;
3368#line 562
3369 __cil_tmp100 = __cil_tmp99 + 48;
3370#line 562
3371 *((int (**)(struct power_supply * , enum power_supply_property , union power_supply_propval * ))__cil_tmp100) = & wm831x_usb_get_prop;
3372#line 563
3373 __cil_tmp101 = (unsigned long )pdev;
3374#line 563
3375 __cil_tmp102 = __cil_tmp101 + 16;
3376#line 563
3377 __cil_tmp103 = (struct device *)__cil_tmp102;
3378#line 563
3379 ret = power_supply_register(__cil_tmp103, usb);
3380 }
3381#line 564
3382 if (ret != 0) {
3383#line 565
3384 goto err_wall;
3385 } else {
3386
3387 }
3388 {
3389#line 567
3390 ret = wm831x_reg_read(wm831x, (unsigned short)16456);
3391 }
3392#line 568
3393 if (ret < 0) {
3394#line 569
3395 goto err_wall;
3396 } else {
3397
3398 }
3399#line 570
3400 __cil_tmp104 = (unsigned long )power;
3401#line 570
3402 __cil_tmp105 = __cil_tmp104 + 860;
3403#line 570
3404 __cil_tmp106 = ret & 32768;
3405#line 570
3406 __cil_tmp107 = __cil_tmp106 != 0;
3407#line 570
3408 *((bool *)__cil_tmp105) = (bool )__cil_tmp107;
3409 {
3410#line 572
3411 __cil_tmp108 = (unsigned long )power;
3412#line 572
3413 __cil_tmp109 = __cil_tmp108 + 860;
3414#line 572
3415 __cil_tmp110 = *((bool *)__cil_tmp109);
3416#line 572
3417 if ((int )__cil_tmp110) {
3418 {
3419#line 573
3420 __cil_tmp111 = (unsigned long )power;
3421#line 573
3422 __cil_tmp112 = __cil_tmp111 + 840;
3423#line 573
3424 __cil_tmp113 = (char (*)[20U])__cil_tmp112;
3425#line 573
3426 *((char const **)battery) = (char const *)__cil_tmp113;
3427#line 574
3428 __cil_tmp114 = (unsigned long )battery;
3429#line 574
3430 __cil_tmp115 = __cil_tmp114 + 16;
3431#line 574
3432 *((enum power_supply_property **)__cil_tmp115) = (enum power_supply_property *)(& wm831x_bat_props);
3433#line 575
3434 __cil_tmp116 = (unsigned long )battery;
3435#line 575
3436 __cil_tmp117 = __cil_tmp116 + 24;
3437#line 575
3438 *((size_t *)__cil_tmp117) = 5UL;
3439#line 576
3440 __cil_tmp118 = (unsigned long )battery;
3441#line 576
3442 __cil_tmp119 = __cil_tmp118 + 48;
3443#line 576
3444 *((int (**)(struct power_supply * , enum power_supply_property , union power_supply_propval * ))__cil_tmp119) = & wm831x_bat_get_prop;
3445#line 577
3446 __cil_tmp120 = (unsigned long )battery;
3447#line 577
3448 __cil_tmp121 = __cil_tmp120 + 88;
3449#line 577
3450 *((int *)__cil_tmp121) = 1;
3451#line 578
3452 __cil_tmp122 = (unsigned long )pdev;
3453#line 578
3454 __cil_tmp123 = __cil_tmp122 + 16;
3455#line 578
3456 __cil_tmp124 = (struct device *)__cil_tmp123;
3457#line 578
3458 ret = power_supply_register(__cil_tmp124, battery);
3459 }
3460#line 579
3461 if (ret != 0) {
3462#line 580
3463 goto err_usb;
3464 } else {
3465
3466 }
3467 } else {
3468
3469 }
3470 }
3471 {
3472#line 583
3473 irq = platform_get_irq_byname(pdev, "SYSLO");
3474#line 584
3475 __cil_tmp125 = (unsigned int )irq;
3476#line 584
3477 __cil_tmp126 = (irqreturn_t (*)(int , void * ))0;
3478#line 584
3479 __cil_tmp127 = (void *)power;
3480#line 584
3481 ret = request_threaded_irq(__cil_tmp125, __cil_tmp126, & wm831x_syslo_irq, 1UL,
3482 "System power low", __cil_tmp127);
3483 }
3484#line 587
3485 if (ret != 0) {
3486 {
3487#line 588
3488 __cil_tmp128 = (unsigned long )pdev;
3489#line 588
3490 __cil_tmp129 = __cil_tmp128 + 16;
3491#line 588
3492 __cil_tmp130 = (struct device *)__cil_tmp129;
3493#line 588
3494 __cil_tmp131 = (struct device const *)__cil_tmp130;
3495#line 588
3496 dev_err(__cil_tmp131, "Failed to request SYSLO IRQ %d: %d\n", irq, ret);
3497 }
3498#line 590
3499 goto err_battery;
3500 } else {
3501
3502 }
3503 {
3504#line 593
3505 irq = platform_get_irq_byname(pdev, "PWR SRC");
3506#line 594
3507 __cil_tmp132 = (unsigned int )irq;
3508#line 594
3509 __cil_tmp133 = (irqreturn_t (*)(int , void * ))0;
3510#line 594
3511 __cil_tmp134 = (void *)power;
3512#line 594
3513 ret = request_threaded_irq(__cil_tmp132, __cil_tmp133, & wm831x_pwr_src_irq, 1UL,
3514 "Power source", __cil_tmp134);
3515 }
3516#line 597
3517 if (ret != 0) {
3518 {
3519#line 598
3520 __cil_tmp135 = (unsigned long )pdev;
3521#line 598
3522 __cil_tmp136 = __cil_tmp135 + 16;
3523#line 598
3524 __cil_tmp137 = (struct device *)__cil_tmp136;
3525#line 598
3526 __cil_tmp138 = (struct device const *)__cil_tmp137;
3527#line 598
3528 dev_err(__cil_tmp138, "Failed to request PWR SRC IRQ %d: %d\n", irq, ret);
3529 }
3530#line 600
3531 goto err_syslo;
3532 } else {
3533
3534 }
3535#line 603
3536 i = 0;
3537#line 603
3538 goto ldv_17670;
3539 ldv_17669:
3540 {
3541#line 604
3542 __cil_tmp139 = i * 8UL;
3543#line 604
3544 __cil_tmp140 = (unsigned long )(wm831x_bat_irqs) + __cil_tmp139;
3545#line 604
3546 __cil_tmp141 = *((char const **)__cil_tmp140);
3547#line 604
3548 irq = platform_get_irq_byname(pdev, __cil_tmp141);
3549#line 605
3550 __cil_tmp142 = (unsigned int )irq;
3551#line 605
3552 __cil_tmp143 = (irqreturn_t (*)(int , void * ))0;
3553#line 605
3554 __cil_tmp144 = i * 8UL;
3555#line 605
3556 __cil_tmp145 = (unsigned long )(wm831x_bat_irqs) + __cil_tmp144;
3557#line 605
3558 __cil_tmp146 = *((char const **)__cil_tmp145);
3559#line 605
3560 __cil_tmp147 = (void *)power;
3561#line 605
3562 ret = request_threaded_irq(__cil_tmp142, __cil_tmp143, & wm831x_bat_irq, 1UL, __cil_tmp146,
3563 __cil_tmp147);
3564 }
3565#line 609
3566 if (ret != 0) {
3567 {
3568#line 610
3569 __cil_tmp148 = (unsigned long )pdev;
3570#line 610
3571 __cil_tmp149 = __cil_tmp148 + 16;
3572#line 610
3573 __cil_tmp150 = (struct device *)__cil_tmp149;
3574#line 610
3575 __cil_tmp151 = (struct device const *)__cil_tmp150;
3576#line 610
3577 __cil_tmp152 = i * 8UL;
3578#line 610
3579 __cil_tmp153 = (unsigned long )(wm831x_bat_irqs) + __cil_tmp152;
3580#line 610
3581 __cil_tmp154 = *((char const **)__cil_tmp153);
3582#line 610
3583 dev_err(__cil_tmp151, "Failed to request %s IRQ %d: %d\n", __cil_tmp154, irq,
3584 ret);
3585 }
3586#line 613
3587 goto err_bat_irq;
3588 } else {
3589
3590 }
3591#line 603
3592 i = i + 1;
3593 ldv_17670: ;
3594 {
3595#line 603
3596 __cil_tmp155 = (unsigned int )i;
3597#line 603
3598 if (__cil_tmp155 <= 7U) {
3599#line 604
3600 goto ldv_17669;
3601 } else {
3602#line 606
3603 goto ldv_17671;
3604 }
3605 }
3606 ldv_17671: ;
3607#line 617
3608 return (ret);
3609 err_bat_irq: ;
3610#line 620
3611 goto ldv_17673;
3612 ldv_17672:
3613 {
3614#line 621
3615 __cil_tmp156 = i * 8UL;
3616#line 621
3617 __cil_tmp157 = (unsigned long )(wm831x_bat_irqs) + __cil_tmp156;
3618#line 621
3619 __cil_tmp158 = *((char const **)__cil_tmp157);
3620#line 621
3621 irq = platform_get_irq_byname(pdev, __cil_tmp158);
3622#line 622
3623 __cil_tmp159 = (unsigned int )irq;
3624#line 622
3625 __cil_tmp160 = (void *)power;
3626#line 622
3627 free_irq(__cil_tmp159, __cil_tmp160);
3628#line 620
3629 i = i - 1;
3630 }
3631 ldv_17673: ;
3632#line 620
3633 if (i >= 0) {
3634#line 621
3635 goto ldv_17672;
3636 } else {
3637#line 623
3638 goto ldv_17674;
3639 }
3640 ldv_17674:
3641 {
3642#line 624
3643 irq = platform_get_irq_byname(pdev, "PWR SRC");
3644#line 625
3645 __cil_tmp161 = (unsigned int )irq;
3646#line 625
3647 __cil_tmp162 = (void *)power;
3648#line 625
3649 free_irq(__cil_tmp161, __cil_tmp162);
3650 }
3651 err_syslo:
3652 {
3653#line 627
3654 irq = platform_get_irq_byname(pdev, "SYSLO");
3655#line 628
3656 __cil_tmp163 = (unsigned int )irq;
3657#line 628
3658 __cil_tmp164 = (void *)power;
3659#line 628
3660 free_irq(__cil_tmp163, __cil_tmp164);
3661 }
3662 err_battery: ;
3663 {
3664#line 630
3665 __cil_tmp165 = (unsigned long )power;
3666#line 630
3667 __cil_tmp166 = __cil_tmp165 + 860;
3668#line 630
3669 __cil_tmp167 = *((bool *)__cil_tmp166);
3670#line 630
3671 if ((int )__cil_tmp167) {
3672 {
3673#line 631
3674 power_supply_unregister(battery);
3675 }
3676 } else {
3677
3678 }
3679 }
3680 err_usb:
3681 {
3682#line 633
3683 power_supply_unregister(usb);
3684 }
3685 err_wall:
3686 {
3687#line 635
3688 power_supply_unregister(wall);
3689 }
3690 err_kmalloc:
3691 {
3692#line 637
3693 __cil_tmp168 = (void const *)power;
3694#line 637
3695 kfree(__cil_tmp168);
3696 }
3697#line 638
3698 return (ret);
3699}
3700}
3701#line 696
3702extern void ldv_check_final_state(void) ;
3703#line 699
3704extern void ldv_check_return_value(int ) ;
3705#line 702
3706extern void ldv_initialize(void) ;
3707#line 705
3708extern int __VERIFIER_nondet_int(void) ;
3709#line 708 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
3710int LDV_IN_INTERRUPT ;
3711#line 711 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
3712void main(void)
3713{ struct platform_device *var_group1 ;
3714 int res_wm831x_power_probe_13 ;
3715 int var_wm831x_bat_irq_10_p0 ;
3716 void *var_wm831x_bat_irq_10_p1 ;
3717 int var_wm831x_pwr_src_irq_12_p0 ;
3718 void *var_wm831x_pwr_src_irq_12_p1 ;
3719 int var_wm831x_syslo_irq_11_p0 ;
3720 void *var_wm831x_syslo_irq_11_p1 ;
3721 int ldv_s_wm831x_power_driver_platform_driver ;
3722 int tmp ;
3723 int tmp___0 ;
3724
3725 {
3726 {
3727#line 761
3728 ldv_s_wm831x_power_driver_platform_driver = 0;
3729#line 751
3730 LDV_IN_INTERRUPT = 1;
3731#line 760
3732 ldv_initialize();
3733 }
3734#line 766
3735 goto ldv_17736;
3736 ldv_17735:
3737 {
3738#line 770
3739 tmp = __VERIFIER_nondet_int();
3740 }
3741#line 772
3742 if (tmp == 0) {
3743#line 772
3744 goto case_0;
3745 } else
3746#line 791
3747 if (tmp == 1) {
3748#line 791
3749 goto case_1;
3750 } else
3751#line 807
3752 if (tmp == 2) {
3753#line 807
3754 goto case_2;
3755 } else
3756#line 823
3757 if (tmp == 3) {
3758#line 823
3759 goto case_3;
3760 } else {
3761 {
3762#line 839
3763 goto switch_default;
3764#line 770
3765 if (0) {
3766 case_0: ;
3767#line 775
3768 if (ldv_s_wm831x_power_driver_platform_driver == 0) {
3769 {
3770#line 780
3771 res_wm831x_power_probe_13 = wm831x_power_probe(var_group1);
3772#line 781
3773 ldv_check_return_value(res_wm831x_power_probe_13);
3774 }
3775#line 782
3776 if (res_wm831x_power_probe_13 != 0) {
3777#line 783
3778 goto ldv_module_exit;
3779 } else {
3780
3781 }
3782#line 784
3783 ldv_s_wm831x_power_driver_platform_driver = 0;
3784 } else {
3785
3786 }
3787#line 790
3788 goto ldv_17730;
3789 case_1:
3790 {
3791#line 794
3792 LDV_IN_INTERRUPT = 2;
3793#line 799
3794 wm831x_bat_irq(var_wm831x_bat_irq_10_p0, var_wm831x_bat_irq_10_p1);
3795#line 800
3796 LDV_IN_INTERRUPT = 1;
3797 }
3798#line 806
3799 goto ldv_17730;
3800 case_2:
3801 {
3802#line 810
3803 LDV_IN_INTERRUPT = 2;
3804#line 815
3805 wm831x_pwr_src_irq(var_wm831x_pwr_src_irq_12_p0, var_wm831x_pwr_src_irq_12_p1);
3806#line 816
3807 LDV_IN_INTERRUPT = 1;
3808 }
3809#line 822
3810 goto ldv_17730;
3811 case_3:
3812 {
3813#line 826
3814 LDV_IN_INTERRUPT = 2;
3815#line 831
3816 wm831x_syslo_irq(var_wm831x_syslo_irq_11_p0, var_wm831x_syslo_irq_11_p1);
3817#line 832
3818 LDV_IN_INTERRUPT = 1;
3819 }
3820#line 838
3821 goto ldv_17730;
3822 switch_default: ;
3823#line 839
3824 goto ldv_17730;
3825 } else {
3826 switch_break: ;
3827 }
3828 }
3829 }
3830 ldv_17730: ;
3831 ldv_17736:
3832 {
3833#line 766
3834 tmp___0 = __VERIFIER_nondet_int();
3835 }
3836#line 766
3837 if (tmp___0 != 0) {
3838#line 768
3839 goto ldv_17735;
3840 } else
3841#line 766
3842 if (ldv_s_wm831x_power_driver_platform_driver != 0) {
3843#line 768
3844 goto ldv_17735;
3845 } else {
3846#line 770
3847 goto ldv_17737;
3848 }
3849 ldv_17737: ;
3850 ldv_module_exit: ;
3851 {
3852#line 848
3853 ldv_check_final_state();
3854 }
3855#line 851
3856 return;
3857}
3858}
3859#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3860void ldv_blast_assert(void)
3861{
3862
3863 {
3864 ERROR: ;
3865#line 6
3866 goto ERROR;
3867}
3868}
3869#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3870extern int __VERIFIER_nondet_int(void) ;
3871#line 872 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
3872int ldv_spin = 0;
3873#line 876 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
3874void ldv_check_alloc_flags(gfp_t flags )
3875{
3876
3877 {
3878#line 879
3879 if (ldv_spin != 0) {
3880#line 879
3881 if (flags != 32U) {
3882 {
3883#line 879
3884 ldv_blast_assert();
3885 }
3886 } else {
3887
3888 }
3889 } else {
3890
3891 }
3892#line 882
3893 return;
3894}
3895}
3896#line 882
3897extern struct page *ldv_some_page(void) ;
3898#line 885 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
3899struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
3900{ struct page *tmp ;
3901
3902 {
3903#line 888
3904 if (ldv_spin != 0) {
3905#line 888
3906 if (flags != 32U) {
3907 {
3908#line 888
3909 ldv_blast_assert();
3910 }
3911 } else {
3912
3913 }
3914 } else {
3915
3916 }
3917 {
3918#line 890
3919 tmp = ldv_some_page();
3920 }
3921#line 890
3922 return (tmp);
3923}
3924}
3925#line 894 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
3926void ldv_check_alloc_nonatomic(void)
3927{
3928
3929 {
3930#line 897
3931 if (ldv_spin != 0) {
3932 {
3933#line 897
3934 ldv_blast_assert();
3935 }
3936 } else {
3937
3938 }
3939#line 900
3940 return;
3941}
3942}
3943#line 901 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
3944void ldv_spin_lock(void)
3945{
3946
3947 {
3948#line 904
3949 ldv_spin = 1;
3950#line 905
3951 return;
3952}
3953}
3954#line 908 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
3955void ldv_spin_unlock(void)
3956{
3957
3958 {
3959#line 911
3960 ldv_spin = 0;
3961#line 912
3962 return;
3963}
3964}
3965#line 915 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
3966int ldv_spin_trylock(void)
3967{ int is_lock ;
3968
3969 {
3970 {
3971#line 920
3972 is_lock = __VERIFIER_nondet_int();
3973 }
3974#line 922
3975 if (is_lock != 0) {
3976#line 925
3977 return (0);
3978 } else {
3979#line 930
3980 ldv_spin = 1;
3981#line 932
3982 return (1);
3983 }
3984}
3985}
3986#line 1099 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
3987void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
3988{
3989
3990 {
3991 {
3992#line 1105
3993 ldv_check_alloc_flags(ldv_func_arg2);
3994#line 1107
3995 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
3996 }
3997#line 1108
3998 return ((void *)0);
3999}
4000}
4001#line 1110 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4730/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_power.c.p"
4002__inline static void *kzalloc(size_t size , gfp_t flags )
4003{ void *tmp ;
4004
4005 {
4006 {
4007#line 1116
4008 ldv_check_alloc_flags(flags);
4009#line 1117
4010 tmp = __VERIFIER_nondet_pointer();
4011 }
4012#line 1117
4013 return (tmp);
4014}
4015}