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 46 "include/linux/dynamic_debug.h"
78struct device;
79#line 46
80struct device;
81#line 57
82struct completion;
83#line 57
84struct completion;
85#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
86struct page;
87#line 58
88struct page;
89#line 26 "include/asm-generic/getorder.h"
90struct task_struct;
91#line 26
92struct task_struct;
93#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
94struct file;
95#line 290
96struct file;
97#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
98struct arch_spinlock;
99#line 327
100struct arch_spinlock;
101#line 306 "include/linux/bitmap.h"
102struct bug_entry {
103 int bug_addr_disp ;
104 int file_disp ;
105 unsigned short line ;
106 unsigned short flags ;
107};
108#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
109struct static_key;
110#line 234
111struct static_key;
112#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
113struct kmem_cache;
114#line 23 "include/asm-generic/atomic-long.h"
115typedef atomic64_t atomic_long_t;
116#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
117typedef u16 __ticket_t;
118#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
119typedef u32 __ticketpair_t;
120#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
121struct __raw_tickets {
122 __ticket_t head ;
123 __ticket_t tail ;
124};
125#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
126union __anonunion_ldv_5907_29 {
127 __ticketpair_t head_tail ;
128 struct __raw_tickets tickets ;
129};
130#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
131struct arch_spinlock {
132 union __anonunion_ldv_5907_29 ldv_5907 ;
133};
134#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
135typedef struct arch_spinlock arch_spinlock_t;
136#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
137struct __anonstruct_ldv_5914_31 {
138 u32 read ;
139 s32 write ;
140};
141#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
142union __anonunion_arch_rwlock_t_30 {
143 s64 lock ;
144 struct __anonstruct_ldv_5914_31 ldv_5914 ;
145};
146#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
147typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
148#line 34
149struct lockdep_map;
150#line 34
151struct lockdep_map;
152#line 55 "include/linux/debug_locks.h"
153struct stack_trace {
154 unsigned int nr_entries ;
155 unsigned int max_entries ;
156 unsigned long *entries ;
157 int skip ;
158};
159#line 26 "include/linux/stacktrace.h"
160struct lockdep_subclass_key {
161 char __one_byte ;
162};
163#line 53 "include/linux/lockdep.h"
164struct lock_class_key {
165 struct lockdep_subclass_key subkeys[8U] ;
166};
167#line 59 "include/linux/lockdep.h"
168struct lock_class {
169 struct list_head hash_entry ;
170 struct list_head lock_entry ;
171 struct lockdep_subclass_key *key ;
172 unsigned int subclass ;
173 unsigned int dep_gen_id ;
174 unsigned long usage_mask ;
175 struct stack_trace usage_traces[13U] ;
176 struct list_head locks_after ;
177 struct list_head locks_before ;
178 unsigned int version ;
179 unsigned long ops ;
180 char const *name ;
181 int name_version ;
182 unsigned long contention_point[4U] ;
183 unsigned long contending_point[4U] ;
184};
185#line 144 "include/linux/lockdep.h"
186struct lockdep_map {
187 struct lock_class_key *key ;
188 struct lock_class *class_cache[2U] ;
189 char const *name ;
190 int cpu ;
191 unsigned long ip ;
192};
193#line 556 "include/linux/lockdep.h"
194struct raw_spinlock {
195 arch_spinlock_t raw_lock ;
196 unsigned int magic ;
197 unsigned int owner_cpu ;
198 void *owner ;
199 struct lockdep_map dep_map ;
200};
201#line 32 "include/linux/spinlock_types.h"
202typedef struct raw_spinlock raw_spinlock_t;
203#line 33 "include/linux/spinlock_types.h"
204struct __anonstruct_ldv_6122_33 {
205 u8 __padding[24U] ;
206 struct lockdep_map dep_map ;
207};
208#line 33 "include/linux/spinlock_types.h"
209union __anonunion_ldv_6123_32 {
210 struct raw_spinlock rlock ;
211 struct __anonstruct_ldv_6122_33 ldv_6122 ;
212};
213#line 33 "include/linux/spinlock_types.h"
214struct spinlock {
215 union __anonunion_ldv_6123_32 ldv_6123 ;
216};
217#line 76 "include/linux/spinlock_types.h"
218typedef struct spinlock spinlock_t;
219#line 23 "include/linux/rwlock_types.h"
220struct __anonstruct_rwlock_t_34 {
221 arch_rwlock_t raw_lock ;
222 unsigned int magic ;
223 unsigned int owner_cpu ;
224 void *owner ;
225 struct lockdep_map dep_map ;
226};
227#line 23 "include/linux/rwlock_types.h"
228typedef struct __anonstruct_rwlock_t_34 rwlock_t;
229#line 48 "include/linux/wait.h"
230struct __wait_queue_head {
231 spinlock_t lock ;
232 struct list_head task_list ;
233};
234#line 53 "include/linux/wait.h"
235typedef struct __wait_queue_head wait_queue_head_t;
236#line 670 "include/linux/mmzone.h"
237struct mutex {
238 atomic_t count ;
239 spinlock_t wait_lock ;
240 struct list_head wait_list ;
241 struct task_struct *owner ;
242 char const *name ;
243 void *magic ;
244 struct lockdep_map dep_map ;
245};
246#line 171 "include/linux/mutex.h"
247struct rw_semaphore;
248#line 171
249struct rw_semaphore;
250#line 172 "include/linux/mutex.h"
251struct rw_semaphore {
252 long count ;
253 raw_spinlock_t wait_lock ;
254 struct list_head wait_list ;
255 struct lockdep_map dep_map ;
256};
257#line 128 "include/linux/rwsem.h"
258struct completion {
259 unsigned int done ;
260 wait_queue_head_t wait ;
261};
262#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
263struct resource {
264 resource_size_t start ;
265 resource_size_t end ;
266 char const *name ;
267 unsigned long flags ;
268 struct resource *parent ;
269 struct resource *sibling ;
270 struct resource *child ;
271};
272#line 312 "include/linux/jiffies.h"
273union ktime {
274 s64 tv64 ;
275};
276#line 59 "include/linux/ktime.h"
277typedef union ktime ktime_t;
278#line 341
279struct tvec_base;
280#line 341
281struct tvec_base;
282#line 342 "include/linux/ktime.h"
283struct timer_list {
284 struct list_head entry ;
285 unsigned long expires ;
286 struct tvec_base *base ;
287 void (*function)(unsigned long ) ;
288 unsigned long data ;
289 int slack ;
290 int start_pid ;
291 void *start_site ;
292 char start_comm[16U] ;
293 struct lockdep_map lockdep_map ;
294};
295#line 302 "include/linux/timer.h"
296struct work_struct;
297#line 302
298struct work_struct;
299#line 45 "include/linux/workqueue.h"
300struct work_struct {
301 atomic_long_t data ;
302 struct list_head entry ;
303 void (*func)(struct work_struct * ) ;
304 struct lockdep_map lockdep_map ;
305};
306#line 46 "include/linux/pm.h"
307struct pm_message {
308 int event ;
309};
310#line 52 "include/linux/pm.h"
311typedef struct pm_message pm_message_t;
312#line 53 "include/linux/pm.h"
313struct dev_pm_ops {
314 int (*prepare)(struct device * ) ;
315 void (*complete)(struct device * ) ;
316 int (*suspend)(struct device * ) ;
317 int (*resume)(struct device * ) ;
318 int (*freeze)(struct device * ) ;
319 int (*thaw)(struct device * ) ;
320 int (*poweroff)(struct device * ) ;
321 int (*restore)(struct device * ) ;
322 int (*suspend_late)(struct device * ) ;
323 int (*resume_early)(struct device * ) ;
324 int (*freeze_late)(struct device * ) ;
325 int (*thaw_early)(struct device * ) ;
326 int (*poweroff_late)(struct device * ) ;
327 int (*restore_early)(struct device * ) ;
328 int (*suspend_noirq)(struct device * ) ;
329 int (*resume_noirq)(struct device * ) ;
330 int (*freeze_noirq)(struct device * ) ;
331 int (*thaw_noirq)(struct device * ) ;
332 int (*poweroff_noirq)(struct device * ) ;
333 int (*restore_noirq)(struct device * ) ;
334 int (*runtime_suspend)(struct device * ) ;
335 int (*runtime_resume)(struct device * ) ;
336 int (*runtime_idle)(struct device * ) ;
337};
338#line 289
339enum rpm_status {
340 RPM_ACTIVE = 0,
341 RPM_RESUMING = 1,
342 RPM_SUSPENDED = 2,
343 RPM_SUSPENDING = 3
344} ;
345#line 296
346enum rpm_request {
347 RPM_REQ_NONE = 0,
348 RPM_REQ_IDLE = 1,
349 RPM_REQ_SUSPEND = 2,
350 RPM_REQ_AUTOSUSPEND = 3,
351 RPM_REQ_RESUME = 4
352} ;
353#line 304
354struct wakeup_source;
355#line 304
356struct wakeup_source;
357#line 494 "include/linux/pm.h"
358struct pm_subsys_data {
359 spinlock_t lock ;
360 unsigned int refcount ;
361};
362#line 499
363struct dev_pm_qos_request;
364#line 499
365struct pm_qos_constraints;
366#line 499 "include/linux/pm.h"
367struct dev_pm_info {
368 pm_message_t power_state ;
369 unsigned char can_wakeup : 1 ;
370 unsigned char async_suspend : 1 ;
371 bool is_prepared ;
372 bool is_suspended ;
373 bool ignore_children ;
374 spinlock_t lock ;
375 struct list_head entry ;
376 struct completion completion ;
377 struct wakeup_source *wakeup ;
378 bool wakeup_path ;
379 struct timer_list suspend_timer ;
380 unsigned long timer_expires ;
381 struct work_struct work ;
382 wait_queue_head_t wait_queue ;
383 atomic_t usage_count ;
384 atomic_t child_count ;
385 unsigned char disable_depth : 3 ;
386 unsigned char idle_notification : 1 ;
387 unsigned char request_pending : 1 ;
388 unsigned char deferred_resume : 1 ;
389 unsigned char run_wake : 1 ;
390 unsigned char runtime_auto : 1 ;
391 unsigned char no_callbacks : 1 ;
392 unsigned char irq_safe : 1 ;
393 unsigned char use_autosuspend : 1 ;
394 unsigned char timer_autosuspends : 1 ;
395 enum rpm_request request ;
396 enum rpm_status runtime_status ;
397 int runtime_error ;
398 int autosuspend_delay ;
399 unsigned long last_busy ;
400 unsigned long active_jiffies ;
401 unsigned long suspended_jiffies ;
402 unsigned long accounting_timestamp ;
403 ktime_t suspend_time ;
404 s64 max_time_suspended_ns ;
405 struct dev_pm_qos_request *pq_req ;
406 struct pm_subsys_data *subsys_data ;
407 struct pm_qos_constraints *constraints ;
408};
409#line 558 "include/linux/pm.h"
410struct dev_pm_domain {
411 struct dev_pm_ops ops ;
412};
413#line 18 "include/asm-generic/pci_iomap.h"
414struct vm_area_struct;
415#line 18
416struct vm_area_struct;
417#line 18 "include/linux/elf.h"
418typedef __u64 Elf64_Addr;
419#line 19 "include/linux/elf.h"
420typedef __u16 Elf64_Half;
421#line 23 "include/linux/elf.h"
422typedef __u32 Elf64_Word;
423#line 24 "include/linux/elf.h"
424typedef __u64 Elf64_Xword;
425#line 193 "include/linux/elf.h"
426struct elf64_sym {
427 Elf64_Word st_name ;
428 unsigned char st_info ;
429 unsigned char st_other ;
430 Elf64_Half st_shndx ;
431 Elf64_Addr st_value ;
432 Elf64_Xword st_size ;
433};
434#line 201 "include/linux/elf.h"
435typedef struct elf64_sym Elf64_Sym;
436#line 445
437struct sock;
438#line 445
439struct sock;
440#line 446
441struct kobject;
442#line 446
443struct kobject;
444#line 447
445enum kobj_ns_type {
446 KOBJ_NS_TYPE_NONE = 0,
447 KOBJ_NS_TYPE_NET = 1,
448 KOBJ_NS_TYPES = 2
449} ;
450#line 453 "include/linux/elf.h"
451struct kobj_ns_type_operations {
452 enum kobj_ns_type type ;
453 void *(*grab_current_ns)(void) ;
454 void const *(*netlink_ns)(struct sock * ) ;
455 void const *(*initial_ns)(void) ;
456 void (*drop_ns)(void * ) ;
457};
458#line 57 "include/linux/kobject_ns.h"
459struct attribute {
460 char const *name ;
461 umode_t mode ;
462 struct lock_class_key *key ;
463 struct lock_class_key skey ;
464};
465#line 33 "include/linux/sysfs.h"
466struct attribute_group {
467 char const *name ;
468 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
469 struct attribute **attrs ;
470};
471#line 62 "include/linux/sysfs.h"
472struct bin_attribute {
473 struct attribute attr ;
474 size_t size ;
475 void *private ;
476 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
477 loff_t , size_t ) ;
478 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
479 loff_t , size_t ) ;
480 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
481};
482#line 98 "include/linux/sysfs.h"
483struct sysfs_ops {
484 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
485 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
486 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
487};
488#line 117
489struct sysfs_dirent;
490#line 117
491struct sysfs_dirent;
492#line 182 "include/linux/sysfs.h"
493struct kref {
494 atomic_t refcount ;
495};
496#line 49 "include/linux/kobject.h"
497struct kset;
498#line 49
499struct kobj_type;
500#line 49 "include/linux/kobject.h"
501struct kobject {
502 char const *name ;
503 struct list_head entry ;
504 struct kobject *parent ;
505 struct kset *kset ;
506 struct kobj_type *ktype ;
507 struct sysfs_dirent *sd ;
508 struct kref kref ;
509 unsigned char state_initialized : 1 ;
510 unsigned char state_in_sysfs : 1 ;
511 unsigned char state_add_uevent_sent : 1 ;
512 unsigned char state_remove_uevent_sent : 1 ;
513 unsigned char uevent_suppress : 1 ;
514};
515#line 107 "include/linux/kobject.h"
516struct kobj_type {
517 void (*release)(struct kobject * ) ;
518 struct sysfs_ops const *sysfs_ops ;
519 struct attribute **default_attrs ;
520 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
521 void const *(*namespace)(struct kobject * ) ;
522};
523#line 115 "include/linux/kobject.h"
524struct kobj_uevent_env {
525 char *envp[32U] ;
526 int envp_idx ;
527 char buf[2048U] ;
528 int buflen ;
529};
530#line 122 "include/linux/kobject.h"
531struct kset_uevent_ops {
532 int (* const filter)(struct kset * , struct kobject * ) ;
533 char const *(* const name)(struct kset * , struct kobject * ) ;
534 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
535};
536#line 139 "include/linux/kobject.h"
537struct kset {
538 struct list_head list ;
539 spinlock_t list_lock ;
540 struct kobject kobj ;
541 struct kset_uevent_ops const *uevent_ops ;
542};
543#line 215
544struct kernel_param;
545#line 215
546struct kernel_param;
547#line 216 "include/linux/kobject.h"
548struct kernel_param_ops {
549 int (*set)(char const * , struct kernel_param const * ) ;
550 int (*get)(char * , struct kernel_param const * ) ;
551 void (*free)(void * ) ;
552};
553#line 49 "include/linux/moduleparam.h"
554struct kparam_string;
555#line 49
556struct kparam_array;
557#line 49 "include/linux/moduleparam.h"
558union __anonunion_ldv_13363_134 {
559 void *arg ;
560 struct kparam_string const *str ;
561 struct kparam_array const *arr ;
562};
563#line 49 "include/linux/moduleparam.h"
564struct kernel_param {
565 char const *name ;
566 struct kernel_param_ops const *ops ;
567 u16 perm ;
568 s16 level ;
569 union __anonunion_ldv_13363_134 ldv_13363 ;
570};
571#line 61 "include/linux/moduleparam.h"
572struct kparam_string {
573 unsigned int maxlen ;
574 char *string ;
575};
576#line 67 "include/linux/moduleparam.h"
577struct kparam_array {
578 unsigned int max ;
579 unsigned int elemsize ;
580 unsigned int *num ;
581 struct kernel_param_ops const *ops ;
582 void *elem ;
583};
584#line 458 "include/linux/moduleparam.h"
585struct static_key {
586 atomic_t enabled ;
587};
588#line 225 "include/linux/jump_label.h"
589struct tracepoint;
590#line 225
591struct tracepoint;
592#line 226 "include/linux/jump_label.h"
593struct tracepoint_func {
594 void *func ;
595 void *data ;
596};
597#line 29 "include/linux/tracepoint.h"
598struct tracepoint {
599 char const *name ;
600 struct static_key key ;
601 void (*regfunc)(void) ;
602 void (*unregfunc)(void) ;
603 struct tracepoint_func *funcs ;
604};
605#line 86 "include/linux/tracepoint.h"
606struct kernel_symbol {
607 unsigned long value ;
608 char const *name ;
609};
610#line 27 "include/linux/export.h"
611struct mod_arch_specific {
612
613};
614#line 34 "include/linux/module.h"
615struct module_param_attrs;
616#line 34 "include/linux/module.h"
617struct module_kobject {
618 struct kobject kobj ;
619 struct module *mod ;
620 struct kobject *drivers_dir ;
621 struct module_param_attrs *mp ;
622};
623#line 43 "include/linux/module.h"
624struct module_attribute {
625 struct attribute attr ;
626 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
627 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
628 size_t ) ;
629 void (*setup)(struct module * , char const * ) ;
630 int (*test)(struct module * ) ;
631 void (*free)(struct module * ) ;
632};
633#line 69
634struct exception_table_entry;
635#line 69
636struct exception_table_entry;
637#line 198
638enum module_state {
639 MODULE_STATE_LIVE = 0,
640 MODULE_STATE_COMING = 1,
641 MODULE_STATE_GOING = 2
642} ;
643#line 204 "include/linux/module.h"
644struct module_ref {
645 unsigned long incs ;
646 unsigned long decs ;
647};
648#line 219
649struct module_sect_attrs;
650#line 219
651struct module_notes_attrs;
652#line 219
653struct ftrace_event_call;
654#line 219 "include/linux/module.h"
655struct module {
656 enum module_state state ;
657 struct list_head list ;
658 char name[56U] ;
659 struct module_kobject mkobj ;
660 struct module_attribute *modinfo_attrs ;
661 char const *version ;
662 char const *srcversion ;
663 struct kobject *holders_dir ;
664 struct kernel_symbol const *syms ;
665 unsigned long const *crcs ;
666 unsigned int num_syms ;
667 struct kernel_param *kp ;
668 unsigned int num_kp ;
669 unsigned int num_gpl_syms ;
670 struct kernel_symbol const *gpl_syms ;
671 unsigned long const *gpl_crcs ;
672 struct kernel_symbol const *unused_syms ;
673 unsigned long const *unused_crcs ;
674 unsigned int num_unused_syms ;
675 unsigned int num_unused_gpl_syms ;
676 struct kernel_symbol const *unused_gpl_syms ;
677 unsigned long const *unused_gpl_crcs ;
678 struct kernel_symbol const *gpl_future_syms ;
679 unsigned long const *gpl_future_crcs ;
680 unsigned int num_gpl_future_syms ;
681 unsigned int num_exentries ;
682 struct exception_table_entry *extable ;
683 int (*init)(void) ;
684 void *module_init ;
685 void *module_core ;
686 unsigned int init_size ;
687 unsigned int core_size ;
688 unsigned int init_text_size ;
689 unsigned int core_text_size ;
690 unsigned int init_ro_size ;
691 unsigned int core_ro_size ;
692 struct mod_arch_specific arch ;
693 unsigned int taints ;
694 unsigned int num_bugs ;
695 struct list_head bug_list ;
696 struct bug_entry *bug_table ;
697 Elf64_Sym *symtab ;
698 Elf64_Sym *core_symtab ;
699 unsigned int num_symtab ;
700 unsigned int core_num_syms ;
701 char *strtab ;
702 char *core_strtab ;
703 struct module_sect_attrs *sect_attrs ;
704 struct module_notes_attrs *notes_attrs ;
705 char *args ;
706 void *percpu ;
707 unsigned int percpu_size ;
708 unsigned int num_tracepoints ;
709 struct tracepoint * const *tracepoints_ptrs ;
710 unsigned int num_trace_bprintk_fmt ;
711 char const **trace_bprintk_fmt_start ;
712 struct ftrace_event_call **trace_events ;
713 unsigned int num_trace_events ;
714 struct list_head source_list ;
715 struct list_head target_list ;
716 struct task_struct *waiter ;
717 void (*exit)(void) ;
718 struct module_ref *refptr ;
719 ctor_fn_t (**ctors)(void) ;
720 unsigned int num_ctors ;
721};
722#line 88 "include/linux/kmemleak.h"
723struct kmem_cache_cpu {
724 void **freelist ;
725 unsigned long tid ;
726 struct page *page ;
727 struct page *partial ;
728 int node ;
729 unsigned int stat[26U] ;
730};
731#line 55 "include/linux/slub_def.h"
732struct kmem_cache_node {
733 spinlock_t list_lock ;
734 unsigned long nr_partial ;
735 struct list_head partial ;
736 atomic_long_t nr_slabs ;
737 atomic_long_t total_objects ;
738 struct list_head full ;
739};
740#line 66 "include/linux/slub_def.h"
741struct kmem_cache_order_objects {
742 unsigned long x ;
743};
744#line 76 "include/linux/slub_def.h"
745struct kmem_cache {
746 struct kmem_cache_cpu *cpu_slab ;
747 unsigned long flags ;
748 unsigned long min_partial ;
749 int size ;
750 int objsize ;
751 int offset ;
752 int cpu_partial ;
753 struct kmem_cache_order_objects oo ;
754 struct kmem_cache_order_objects max ;
755 struct kmem_cache_order_objects min ;
756 gfp_t allocflags ;
757 int refcount ;
758 void (*ctor)(void * ) ;
759 int inuse ;
760 int align ;
761 int reserved ;
762 char const *name ;
763 struct list_head list ;
764 struct kobject kobj ;
765 int remote_node_defrag_ratio ;
766 struct kmem_cache_node *node[1024U] ;
767};
768#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
769struct klist_node;
770#line 15
771struct klist_node;
772#line 37 "include/linux/klist.h"
773struct klist_node {
774 void *n_klist ;
775 struct list_head n_node ;
776 struct kref n_ref ;
777};
778#line 67
779struct dma_map_ops;
780#line 67 "include/linux/klist.h"
781struct dev_archdata {
782 void *acpi_handle ;
783 struct dma_map_ops *dma_ops ;
784 void *iommu ;
785};
786#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
787struct pdev_archdata {
788
789};
790#line 17
791struct device_private;
792#line 17
793struct device_private;
794#line 18
795struct device_driver;
796#line 18
797struct device_driver;
798#line 19
799struct driver_private;
800#line 19
801struct driver_private;
802#line 20
803struct class;
804#line 20
805struct class;
806#line 21
807struct subsys_private;
808#line 21
809struct subsys_private;
810#line 22
811struct bus_type;
812#line 22
813struct bus_type;
814#line 23
815struct device_node;
816#line 23
817struct device_node;
818#line 24
819struct iommu_ops;
820#line 24
821struct iommu_ops;
822#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
823struct bus_attribute {
824 struct attribute attr ;
825 ssize_t (*show)(struct bus_type * , char * ) ;
826 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
827};
828#line 51 "include/linux/device.h"
829struct device_attribute;
830#line 51
831struct driver_attribute;
832#line 51 "include/linux/device.h"
833struct bus_type {
834 char const *name ;
835 char const *dev_name ;
836 struct device *dev_root ;
837 struct bus_attribute *bus_attrs ;
838 struct device_attribute *dev_attrs ;
839 struct driver_attribute *drv_attrs ;
840 int (*match)(struct device * , struct device_driver * ) ;
841 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
842 int (*probe)(struct device * ) ;
843 int (*remove)(struct device * ) ;
844 void (*shutdown)(struct device * ) ;
845 int (*suspend)(struct device * , pm_message_t ) ;
846 int (*resume)(struct device * ) ;
847 struct dev_pm_ops const *pm ;
848 struct iommu_ops *iommu_ops ;
849 struct subsys_private *p ;
850};
851#line 125
852struct device_type;
853#line 182
854struct of_device_id;
855#line 182 "include/linux/device.h"
856struct device_driver {
857 char const *name ;
858 struct bus_type *bus ;
859 struct module *owner ;
860 char const *mod_name ;
861 bool suppress_bind_attrs ;
862 struct of_device_id const *of_match_table ;
863 int (*probe)(struct device * ) ;
864 int (*remove)(struct device * ) ;
865 void (*shutdown)(struct device * ) ;
866 int (*suspend)(struct device * , pm_message_t ) ;
867 int (*resume)(struct device * ) ;
868 struct attribute_group const **groups ;
869 struct dev_pm_ops const *pm ;
870 struct driver_private *p ;
871};
872#line 245 "include/linux/device.h"
873struct driver_attribute {
874 struct attribute attr ;
875 ssize_t (*show)(struct device_driver * , char * ) ;
876 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
877};
878#line 299
879struct class_attribute;
880#line 299 "include/linux/device.h"
881struct class {
882 char const *name ;
883 struct module *owner ;
884 struct class_attribute *class_attrs ;
885 struct device_attribute *dev_attrs ;
886 struct bin_attribute *dev_bin_attrs ;
887 struct kobject *dev_kobj ;
888 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
889 char *(*devnode)(struct device * , umode_t * ) ;
890 void (*class_release)(struct class * ) ;
891 void (*dev_release)(struct device * ) ;
892 int (*suspend)(struct device * , pm_message_t ) ;
893 int (*resume)(struct device * ) ;
894 struct kobj_ns_type_operations const *ns_type ;
895 void const *(*namespace)(struct device * ) ;
896 struct dev_pm_ops const *pm ;
897 struct subsys_private *p ;
898};
899#line 394 "include/linux/device.h"
900struct class_attribute {
901 struct attribute attr ;
902 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
903 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
904 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
905};
906#line 447 "include/linux/device.h"
907struct device_type {
908 char const *name ;
909 struct attribute_group const **groups ;
910 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
911 char *(*devnode)(struct device * , umode_t * ) ;
912 void (*release)(struct device * ) ;
913 struct dev_pm_ops const *pm ;
914};
915#line 474 "include/linux/device.h"
916struct device_attribute {
917 struct attribute attr ;
918 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
919 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
920 size_t ) ;
921};
922#line 557 "include/linux/device.h"
923struct device_dma_parameters {
924 unsigned int max_segment_size ;
925 unsigned long segment_boundary_mask ;
926};
927#line 567
928struct dma_coherent_mem;
929#line 567 "include/linux/device.h"
930struct device {
931 struct device *parent ;
932 struct device_private *p ;
933 struct kobject kobj ;
934 char const *init_name ;
935 struct device_type const *type ;
936 struct mutex mutex ;
937 struct bus_type *bus ;
938 struct device_driver *driver ;
939 void *platform_data ;
940 struct dev_pm_info power ;
941 struct dev_pm_domain *pm_domain ;
942 int numa_node ;
943 u64 *dma_mask ;
944 u64 coherent_dma_mask ;
945 struct device_dma_parameters *dma_parms ;
946 struct list_head dma_pools ;
947 struct dma_coherent_mem *dma_mem ;
948 struct dev_archdata archdata ;
949 struct device_node *of_node ;
950 dev_t devt ;
951 u32 id ;
952 spinlock_t devres_lock ;
953 struct list_head devres_head ;
954 struct klist_node knode_class ;
955 struct class *class ;
956 struct attribute_group const **groups ;
957 void (*release)(struct device * ) ;
958};
959#line 681 "include/linux/device.h"
960struct wakeup_source {
961 char const *name ;
962 struct list_head entry ;
963 spinlock_t lock ;
964 struct timer_list timer ;
965 unsigned long timer_expires ;
966 ktime_t total_time ;
967 ktime_t max_time ;
968 ktime_t last_time ;
969 unsigned long event_count ;
970 unsigned long active_count ;
971 unsigned long relax_count ;
972 unsigned long hit_count ;
973 unsigned char active : 1 ;
974};
975#line 12 "include/linux/mod_devicetable.h"
976typedef unsigned long kernel_ulong_t;
977#line 215 "include/linux/mod_devicetable.h"
978struct of_device_id {
979 char name[32U] ;
980 char type[32U] ;
981 char compatible[128U] ;
982 void *data ;
983};
984#line 492 "include/linux/mod_devicetable.h"
985struct platform_device_id {
986 char name[20U] ;
987 kernel_ulong_t driver_data ;
988};
989#line 584
990struct mfd_cell;
991#line 584
992struct mfd_cell;
993#line 585 "include/linux/mod_devicetable.h"
994struct platform_device {
995 char const *name ;
996 int id ;
997 struct device dev ;
998 u32 num_resources ;
999 struct resource *resource ;
1000 struct platform_device_id const *id_entry ;
1001 struct mfd_cell *mfd_cell ;
1002 struct pdev_archdata archdata ;
1003};
1004#line 272 "include/linux/platform_device.h"
1005enum led_brightness {
1006 LED_OFF = 0,
1007 LED_HALF = 127,
1008 LED_FULL = 255
1009} ;
1010#line 278
1011struct led_trigger;
1012#line 278 "include/linux/platform_device.h"
1013struct led_classdev {
1014 char const *name ;
1015 int brightness ;
1016 int max_brightness ;
1017 int flags ;
1018 void (*brightness_set)(struct led_classdev * , enum led_brightness ) ;
1019 enum led_brightness (*brightness_get)(struct led_classdev * ) ;
1020 int (*blink_set)(struct led_classdev * , unsigned long * , unsigned long * ) ;
1021 struct device *dev ;
1022 struct list_head node ;
1023 char const *default_trigger ;
1024 unsigned long blink_delay_on ;
1025 unsigned long blink_delay_off ;
1026 struct timer_list blink_timer ;
1027 int blink_brightness ;
1028 struct rw_semaphore trigger_lock ;
1029 struct led_trigger *trigger ;
1030 struct list_head trig_list ;
1031 void *trigger_data ;
1032};
1033#line 113 "include/linux/leds.h"
1034struct led_trigger {
1035 char const *name ;
1036 void (*activate)(struct led_classdev * ) ;
1037 void (*deactivate)(struct led_classdev * ) ;
1038 rwlock_t leddev_list_lock ;
1039 struct list_head led_cdevs ;
1040 struct list_head next_trig ;
1041};
1042#line 261
1043enum power_supply_property {
1044 POWER_SUPPLY_PROP_STATUS = 0,
1045 POWER_SUPPLY_PROP_CHARGE_TYPE = 1,
1046 POWER_SUPPLY_PROP_HEALTH = 2,
1047 POWER_SUPPLY_PROP_PRESENT = 3,
1048 POWER_SUPPLY_PROP_ONLINE = 4,
1049 POWER_SUPPLY_PROP_TECHNOLOGY = 5,
1050 POWER_SUPPLY_PROP_CYCLE_COUNT = 6,
1051 POWER_SUPPLY_PROP_VOLTAGE_MAX = 7,
1052 POWER_SUPPLY_PROP_VOLTAGE_MIN = 8,
1053 POWER_SUPPLY_PROP_VOLTAGE_MAX_DESIGN = 9,
1054 POWER_SUPPLY_PROP_VOLTAGE_MIN_DESIGN = 10,
1055 POWER_SUPPLY_PROP_VOLTAGE_NOW = 11,
1056 POWER_SUPPLY_PROP_VOLTAGE_AVG = 12,
1057 POWER_SUPPLY_PROP_CURRENT_MAX = 13,
1058 POWER_SUPPLY_PROP_CURRENT_NOW = 14,
1059 POWER_SUPPLY_PROP_CURRENT_AVG = 15,
1060 POWER_SUPPLY_PROP_POWER_NOW = 16,
1061 POWER_SUPPLY_PROP_POWER_AVG = 17,
1062 POWER_SUPPLY_PROP_CHARGE_FULL_DESIGN = 18,
1063 POWER_SUPPLY_PROP_CHARGE_EMPTY_DESIGN = 19,
1064 POWER_SUPPLY_PROP_CHARGE_FULL = 20,
1065 POWER_SUPPLY_PROP_CHARGE_EMPTY = 21,
1066 POWER_SUPPLY_PROP_CHARGE_NOW = 22,
1067 POWER_SUPPLY_PROP_CHARGE_AVG = 23,
1068 POWER_SUPPLY_PROP_CHARGE_COUNTER = 24,
1069 POWER_SUPPLY_PROP_ENERGY_FULL_DESIGN = 25,
1070 POWER_SUPPLY_PROP_ENERGY_EMPTY_DESIGN = 26,
1071 POWER_SUPPLY_PROP_ENERGY_FULL = 27,
1072 POWER_SUPPLY_PROP_ENERGY_EMPTY = 28,
1073 POWER_SUPPLY_PROP_ENERGY_NOW = 29,
1074 POWER_SUPPLY_PROP_ENERGY_AVG = 30,
1075 POWER_SUPPLY_PROP_CAPACITY = 31,
1076 POWER_SUPPLY_PROP_CAPACITY_LEVEL = 32,
1077 POWER_SUPPLY_PROP_TEMP = 33,
1078 POWER_SUPPLY_PROP_TEMP_AMBIENT = 34,
1079 POWER_SUPPLY_PROP_TIME_TO_EMPTY_NOW = 35,
1080 POWER_SUPPLY_PROP_TIME_TO_EMPTY_AVG = 36,
1081 POWER_SUPPLY_PROP_TIME_TO_FULL_NOW = 37,
1082 POWER_SUPPLY_PROP_TIME_TO_FULL_AVG = 38,
1083 POWER_SUPPLY_PROP_TYPE = 39,
1084 POWER_SUPPLY_PROP_SCOPE = 40,
1085 POWER_SUPPLY_PROP_MODEL_NAME = 41,
1086 POWER_SUPPLY_PROP_MANUFACTURER = 42,
1087 POWER_SUPPLY_PROP_SERIAL_NUMBER = 43
1088} ;
1089#line 308
1090enum power_supply_type {
1091 POWER_SUPPLY_TYPE_UNKNOWN = 0,
1092 POWER_SUPPLY_TYPE_BATTERY = 1,
1093 POWER_SUPPLY_TYPE_UPS = 2,
1094 POWER_SUPPLY_TYPE_MAINS = 3,
1095 POWER_SUPPLY_TYPE_USB = 4,
1096 POWER_SUPPLY_TYPE_USB_DCP = 5,
1097 POWER_SUPPLY_TYPE_USB_CDP = 6,
1098 POWER_SUPPLY_TYPE_USB_ACA = 7
1099} ;
1100#line 319 "include/linux/leds.h"
1101union power_supply_propval {
1102 int intval ;
1103 char const *strval ;
1104};
1105#line 148 "include/linux/power_supply.h"
1106struct power_supply {
1107 char const *name ;
1108 enum power_supply_type type ;
1109 enum power_supply_property *properties ;
1110 size_t num_properties ;
1111 char **supplied_to ;
1112 size_t num_supplicants ;
1113 int (*get_property)(struct power_supply * , enum power_supply_property , union power_supply_propval * ) ;
1114 int (*set_property)(struct power_supply * , enum power_supply_property , union power_supply_propval const * ) ;
1115 int (*property_is_writeable)(struct power_supply * , enum power_supply_property ) ;
1116 void (*external_power_changed)(struct power_supply * ) ;
1117 void (*set_charged)(struct power_supply * ) ;
1118 int use_for_apm ;
1119 struct device *dev ;
1120 struct work_struct changed_work ;
1121 struct led_trigger *charging_full_trig ;
1122 char *charging_full_trig_name ;
1123 struct led_trigger *charging_trig ;
1124 char *charging_trig_name ;
1125 struct led_trigger *full_trig ;
1126 char *full_trig_name ;
1127 struct led_trigger *online_trig ;
1128 char *online_trig_name ;
1129 struct led_trigger *charging_blink_full_solid_trig ;
1130 char *charging_blink_full_solid_trig_name ;
1131};
1132#line 41 "include/asm-generic/sections.h"
1133struct exception_table_entry {
1134 unsigned long insn ;
1135 unsigned long fixup ;
1136};
1137#line 704 "include/linux/interrupt.h"
1138struct regmap;
1139#line 704
1140struct regmap;
1141#line 231 "include/linux/regmap.h"
1142struct wm831x;
1143#line 231
1144struct wm831x;
1145#line 232
1146enum wm831x_auxadc;
1147#line 232
1148enum wm831x_auxadc;
1149#line 359 "include/linux/mfd/wm831x/core.h"
1150struct wm831x {
1151 struct mutex io_lock ;
1152 struct device *dev ;
1153 struct regmap *regmap ;
1154 int irq ;
1155 struct mutex irq_lock ;
1156 int irq_base ;
1157 int irq_masks_cur[5U] ;
1158 int irq_masks_cache[5U] ;
1159 bool soft_shutdown ;
1160 unsigned char has_gpio_ena : 1 ;
1161 unsigned char has_cs_sts : 1 ;
1162 unsigned char charger_irq_wake : 1 ;
1163 int num_gpio ;
1164 int gpio_update[16U] ;
1165 bool gpio_level[16U] ;
1166 struct mutex auxadc_lock ;
1167 struct list_head auxadc_pending ;
1168 u16 auxadc_active ;
1169 int (*auxadc_read)(struct wm831x * , enum wm831x_auxadc ) ;
1170 struct mutex key_lock ;
1171 unsigned char locked : 1 ;
1172};
1173#line 421
1174enum wm831x_auxadc {
1175 WM831X_AUX_CAL = 15,
1176 WM831X_AUX_BKUP_BATT = 10,
1177 WM831X_AUX_WALL = 9,
1178 WM831X_AUX_BATT = 8,
1179 WM831X_AUX_USB = 7,
1180 WM831X_AUX_SYSVDD = 6,
1181 WM831X_AUX_BATT_TEMP = 5,
1182 WM831X_AUX_CHIP_TEMP = 4,
1183 WM831X_AUX_AUX4 = 3,
1184 WM831X_AUX_AUX3 = 2,
1185 WM831X_AUX_AUX2 = 1,
1186 WM831X_AUX_AUX1 = 0
1187} ;
1188#line 215 "include/linux/mfd/wm831x/auxadc.h"
1189struct regulator_init_data;
1190#line 215
1191struct regulator_init_data;
1192#line 216 "include/linux/mfd/wm831x/auxadc.h"
1193struct wm831x_backlight_pdata {
1194 int isink ;
1195 int max_uA ;
1196};
1197#line 25 "include/linux/mfd/wm831x/pdata.h"
1198struct wm831x_backup_pdata {
1199 int charger_enable ;
1200 int no_constant_voltage ;
1201 int vlim ;
1202 int ilim ;
1203};
1204#line 32 "include/linux/mfd/wm831x/pdata.h"
1205struct wm831x_battery_pdata {
1206 int enable ;
1207 int fast_enable ;
1208 int off_mask ;
1209 int trickle_ilim ;
1210 int vsel ;
1211 int eoc_iterm ;
1212 int fast_ilim ;
1213 int timeout ;
1214};
1215#line 60
1216enum wm831x_status_src {
1217 WM831X_STATUS_PRESERVE = 0,
1218 WM831X_STATUS_OTP = 1,
1219 WM831X_STATUS_POWER = 2,
1220 WM831X_STATUS_CHARGER = 3,
1221 WM831X_STATUS_MANUAL = 4
1222} ;
1223#line 68 "include/linux/mfd/wm831x/pdata.h"
1224struct wm831x_status_pdata {
1225 enum wm831x_status_src default_src ;
1226 char const *name ;
1227 char const *default_trigger ;
1228};
1229#line 77 "include/linux/mfd/wm831x/pdata.h"
1230struct wm831x_touch_pdata {
1231 int fivewire ;
1232 int isel ;
1233 int rpu ;
1234 int pressure ;
1235 unsigned int data_irq ;
1236 int data_irqf ;
1237 unsigned int pd_irq ;
1238 int pd_irqf ;
1239};
1240#line 88
1241enum wm831x_watchdog_action {
1242 WM831X_WDOG_NONE = 0,
1243 WM831X_WDOG_INTERRUPT = 1,
1244 WM831X_WDOG_RESET = 2,
1245 WM831X_WDOG_WAKE = 3
1246} ;
1247#line 95 "include/linux/mfd/wm831x/pdata.h"
1248struct wm831x_watchdog_pdata {
1249 enum wm831x_watchdog_action primary ;
1250 enum wm831x_watchdog_action secondary ;
1251 int update_gpio ;
1252 unsigned char software : 1 ;
1253};
1254#line 101 "include/linux/mfd/wm831x/pdata.h"
1255struct wm831x_pdata {
1256 int wm831x_num ;
1257 int (*pre_init)(struct wm831x * ) ;
1258 int (*post_init)(struct wm831x * ) ;
1259 bool irq_cmos ;
1260 bool disable_touch ;
1261 bool soft_shutdown ;
1262 int irq_base ;
1263 int gpio_base ;
1264 int gpio_defaults[16U] ;
1265 struct wm831x_backlight_pdata *backlight ;
1266 struct wm831x_backup_pdata *backup ;
1267 struct wm831x_battery_pdata *battery ;
1268 struct wm831x_touch_pdata *touch ;
1269 struct wm831x_watchdog_pdata *watchdog ;
1270 struct wm831x_status_pdata *status[2U] ;
1271 struct regulator_init_data *dcdc[4U] ;
1272 struct regulator_init_data *epe[2U] ;
1273 struct regulator_init_data *ldo[11U] ;
1274 struct regulator_init_data *isink[2U] ;
1275};
1276#line 149 "include/linux/mfd/wm831x/pdata.h"
1277struct wm831x_backup {
1278 struct wm831x *wm831x ;
1279 struct power_supply backup ;
1280 char name[20U] ;
1281};
1282#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
1283void ldv_spin_lock(void) ;
1284#line 3
1285void ldv_spin_unlock(void) ;
1286#line 4
1287int ldv_spin_trylock(void) ;
1288#line 323 "include/linux/kernel.h"
1289extern int snprintf(char * , size_t , char const * , ...) ;
1290#line 161 "include/linux/slab.h"
1291extern void kfree(void const * ) ;
1292#line 220 "include/linux/slub_def.h"
1293extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1294#line 223
1295void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1296#line 353 "include/linux/slab.h"
1297__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1298#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
1299extern void *__VERIFIER_nondet_pointer(void) ;
1300#line 11
1301void ldv_check_alloc_flags(gfp_t flags ) ;
1302#line 12
1303void ldv_check_alloc_nonatomic(void) ;
1304#line 14
1305struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1306#line 792 "include/linux/device.h"
1307extern void *dev_get_drvdata(struct device const * ) ;
1308#line 793
1309extern int dev_set_drvdata(struct device * , void * ) ;
1310#line 892
1311extern int dev_err(struct device const * , char const * , ...) ;
1312#line 894
1313extern int dev_warn(struct device const * , char const * , ...) ;
1314#line 188 "include/linux/platform_device.h"
1315__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )
1316{ unsigned long __cil_tmp3 ;
1317 unsigned long __cil_tmp4 ;
1318 struct device *__cil_tmp5 ;
1319
1320 {
1321 {
1322#line 190
1323 __cil_tmp3 = (unsigned long )pdev;
1324#line 190
1325 __cil_tmp4 = __cil_tmp3 + 16;
1326#line 190
1327 __cil_tmp5 = (struct device *)__cil_tmp4;
1328#line 190
1329 dev_set_drvdata(__cil_tmp5, data);
1330 }
1331#line 191
1332 return;
1333}
1334}
1335#line 220 "include/linux/power_supply.h"
1336extern int power_supply_register(struct device * , struct power_supply * ) ;
1337#line 402 "include/linux/mfd/wm831x/core.h"
1338extern int wm831x_reg_read(struct wm831x * , unsigned short ) ;
1339#line 405
1340extern void wm831x_reg_lock(struct wm831x * ) ;
1341#line 406
1342extern int wm831x_reg_unlock(struct wm831x * ) ;
1343#line 407
1344extern int wm831x_set_bits(struct wm831x * , unsigned short , unsigned short , unsigned short ) ;
1345#line 214 "include/linux/mfd/wm831x/auxadc.h"
1346extern int wm831x_auxadc_read_uv(struct wm831x * , enum wm831x_auxadc ) ;
1347#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
1348static int wm831x_backup_read_voltage(struct wm831x *wm831x , enum wm831x_auxadc src ,
1349 union power_supply_propval *val )
1350{ int ret ;
1351
1352 {
1353 {
1354#line 49
1355 ret = wm831x_auxadc_read_uv(wm831x, src);
1356 }
1357#line 50
1358 if (ret >= 0) {
1359#line 51
1360 *((int *)val) = ret;
1361 } else {
1362
1363 }
1364#line 53
1365 return (ret);
1366}
1367}
1368#line 60 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
1369static void wm831x_config_backup(struct wm831x *wm831x )
1370{ struct wm831x_pdata *wm831x_pdata ;
1371 struct wm831x_backup_pdata *pdata ;
1372 int ret ;
1373 int reg ;
1374 unsigned long __cil_tmp6 ;
1375 unsigned long __cil_tmp7 ;
1376 struct device *__cil_tmp8 ;
1377 unsigned long __cil_tmp9 ;
1378 unsigned long __cil_tmp10 ;
1379 void *__cil_tmp11 ;
1380 struct wm831x_pdata *__cil_tmp12 ;
1381 unsigned long __cil_tmp13 ;
1382 unsigned long __cil_tmp14 ;
1383 unsigned long __cil_tmp15 ;
1384 unsigned long __cil_tmp16 ;
1385 struct device *__cil_tmp17 ;
1386 struct device const *__cil_tmp18 ;
1387 struct wm831x_backup_pdata *__cil_tmp19 ;
1388 unsigned long __cil_tmp20 ;
1389 unsigned long __cil_tmp21 ;
1390 unsigned long __cil_tmp22 ;
1391 struct wm831x_backup_pdata *__cil_tmp23 ;
1392 unsigned long __cil_tmp24 ;
1393 unsigned long __cil_tmp25 ;
1394 unsigned long __cil_tmp26 ;
1395 struct device *__cil_tmp27 ;
1396 struct device const *__cil_tmp28 ;
1397 unsigned long __cil_tmp29 ;
1398 unsigned long __cil_tmp30 ;
1399 int __cil_tmp31 ;
1400 unsigned long __cil_tmp32 ;
1401 unsigned long __cil_tmp33 ;
1402 int __cil_tmp34 ;
1403 unsigned long __cil_tmp35 ;
1404 unsigned long __cil_tmp36 ;
1405 unsigned long __cil_tmp37 ;
1406 unsigned long __cil_tmp38 ;
1407 struct device *__cil_tmp39 ;
1408 struct device const *__cil_tmp40 ;
1409 unsigned long __cil_tmp41 ;
1410 unsigned long __cil_tmp42 ;
1411 int __cil_tmp43 ;
1412 unsigned long __cil_tmp44 ;
1413 unsigned long __cil_tmp45 ;
1414 unsigned long __cil_tmp46 ;
1415 unsigned long __cil_tmp47 ;
1416 struct device *__cil_tmp48 ;
1417 struct device const *__cil_tmp49 ;
1418 unsigned long __cil_tmp50 ;
1419 unsigned long __cil_tmp51 ;
1420 int __cil_tmp52 ;
1421 unsigned long __cil_tmp53 ;
1422 unsigned long __cil_tmp54 ;
1423 struct device *__cil_tmp55 ;
1424 struct device const *__cil_tmp56 ;
1425 unsigned short __cil_tmp57 ;
1426 int __cil_tmp58 ;
1427 unsigned short __cil_tmp59 ;
1428 unsigned long __cil_tmp60 ;
1429 unsigned long __cil_tmp61 ;
1430 struct device *__cil_tmp62 ;
1431 struct device const *__cil_tmp63 ;
1432
1433 {
1434#line 62
1435 __cil_tmp6 = (unsigned long )wm831x;
1436#line 62
1437 __cil_tmp7 = __cil_tmp6 + 168;
1438#line 62
1439 __cil_tmp8 = *((struct device **)__cil_tmp7);
1440#line 62
1441 __cil_tmp9 = (unsigned long )__cil_tmp8;
1442#line 62
1443 __cil_tmp10 = __cil_tmp9 + 280;
1444#line 62
1445 __cil_tmp11 = *((void **)__cil_tmp10);
1446#line 62
1447 wm831x_pdata = (struct wm831x_pdata *)__cil_tmp11;
1448 {
1449#line 66
1450 __cil_tmp12 = (struct wm831x_pdata *)0;
1451#line 66
1452 __cil_tmp13 = (unsigned long )__cil_tmp12;
1453#line 66
1454 __cil_tmp14 = (unsigned long )wm831x_pdata;
1455#line 66
1456 if (__cil_tmp14 == __cil_tmp13) {
1457 {
1458#line 67
1459 __cil_tmp15 = (unsigned long )wm831x;
1460#line 67
1461 __cil_tmp16 = __cil_tmp15 + 168;
1462#line 67
1463 __cil_tmp17 = *((struct device **)__cil_tmp16);
1464#line 67
1465 __cil_tmp18 = (struct device const *)__cil_tmp17;
1466#line 67
1467 dev_warn(__cil_tmp18, "No backup battery charger configuration\n");
1468 }
1469#line 69
1470 return;
1471 } else {
1472 {
1473#line 66
1474 __cil_tmp19 = (struct wm831x_backup_pdata *)0;
1475#line 66
1476 __cil_tmp20 = (unsigned long )__cil_tmp19;
1477#line 66
1478 __cil_tmp21 = (unsigned long )wm831x_pdata;
1479#line 66
1480 __cil_tmp22 = __cil_tmp21 + 112;
1481#line 66
1482 __cil_tmp23 = *((struct wm831x_backup_pdata **)__cil_tmp22);
1483#line 66
1484 __cil_tmp24 = (unsigned long )__cil_tmp23;
1485#line 66
1486 if (__cil_tmp24 == __cil_tmp20) {
1487 {
1488#line 67
1489 __cil_tmp25 = (unsigned long )wm831x;
1490#line 67
1491 __cil_tmp26 = __cil_tmp25 + 168;
1492#line 67
1493 __cil_tmp27 = *((struct device **)__cil_tmp26);
1494#line 67
1495 __cil_tmp28 = (struct device const *)__cil_tmp27;
1496#line 67
1497 dev_warn(__cil_tmp28, "No backup battery charger configuration\n");
1498 }
1499#line 69
1500 return;
1501 } else {
1502
1503 }
1504 }
1505 }
1506 }
1507#line 72
1508 __cil_tmp29 = (unsigned long )wm831x_pdata;
1509#line 72
1510 __cil_tmp30 = __cil_tmp29 + 112;
1511#line 72
1512 pdata = *((struct wm831x_backup_pdata **)__cil_tmp30);
1513#line 74
1514 reg = 0;
1515 {
1516#line 76
1517 __cil_tmp31 = *((int *)pdata);
1518#line 76
1519 if (__cil_tmp31 != 0) {
1520#line 77
1521 reg = reg | 34816;
1522 } else {
1523
1524 }
1525 }
1526 {
1527#line 78
1528 __cil_tmp32 = (unsigned long )pdata;
1529#line 78
1530 __cil_tmp33 = __cil_tmp32 + 4;
1531#line 78
1532 __cil_tmp34 = *((int *)__cil_tmp33);
1533#line 78
1534 if (__cil_tmp34 != 0) {
1535#line 79
1536 reg = reg | 4096;
1537 } else {
1538
1539 }
1540 }
1541 {
1542#line 81
1543 __cil_tmp35 = (unsigned long )pdata;
1544#line 81
1545 __cil_tmp36 = __cil_tmp35 + 8;
1546#line 82
1547 if (*((int *)__cil_tmp36) == 2500) {
1548#line 82
1549 goto case_2500;
1550 } else
1551#line 84
1552 if (*((int *)__cil_tmp36) == 3100) {
1553#line 84
1554 goto case_3100;
1555 } else {
1556 {
1557#line 87
1558 goto switch_default;
1559#line 81
1560 if (0) {
1561 case_2500: ;
1562#line 83
1563 goto ldv_17503;
1564 case_3100:
1565#line 85
1566 reg = reg | 16;
1567#line 86
1568 goto ldv_17503;
1569 switch_default:
1570 {
1571#line 88
1572 __cil_tmp37 = (unsigned long )wm831x;
1573#line 88
1574 __cil_tmp38 = __cil_tmp37 + 168;
1575#line 88
1576 __cil_tmp39 = *((struct device **)__cil_tmp38);
1577#line 88
1578 __cil_tmp40 = (struct device const *)__cil_tmp39;
1579#line 88
1580 __cil_tmp41 = (unsigned long )pdata;
1581#line 88
1582 __cil_tmp42 = __cil_tmp41 + 8;
1583#line 88
1584 __cil_tmp43 = *((int *)__cil_tmp42);
1585#line 88
1586 dev_err(__cil_tmp40, "Invalid backup voltage limit %dmV\n", __cil_tmp43);
1587 }
1588 } else {
1589 switch_break: ;
1590 }
1591 }
1592 }
1593 }
1594 ldv_17503: ;
1595 {
1596#line 92
1597 __cil_tmp44 = (unsigned long )pdata;
1598#line 92
1599 __cil_tmp45 = __cil_tmp44 + 12;
1600#line 93
1601 if (*((int *)__cil_tmp45) == 100) {
1602#line 93
1603 goto case_100;
1604 } else
1605#line 95
1606 if (*((int *)__cil_tmp45) == 200) {
1607#line 95
1608 goto case_200;
1609 } else
1610#line 98
1611 if (*((int *)__cil_tmp45) == 300) {
1612#line 98
1613 goto case_300;
1614 } else
1615#line 101
1616 if (*((int *)__cil_tmp45) == 400) {
1617#line 101
1618 goto case_400;
1619 } else {
1620 {
1621#line 104
1622 goto switch_default___0;
1623#line 92
1624 if (0) {
1625 case_100: ;
1626#line 94
1627 goto ldv_17507;
1628 case_200:
1629#line 96
1630 reg = reg | 1;
1631#line 97
1632 goto ldv_17507;
1633 case_300:
1634#line 99
1635 reg = reg | 2;
1636#line 100
1637 goto ldv_17507;
1638 case_400:
1639#line 102
1640 reg = reg | 3;
1641#line 103
1642 goto ldv_17507;
1643 switch_default___0:
1644 {
1645#line 105
1646 __cil_tmp46 = (unsigned long )wm831x;
1647#line 105
1648 __cil_tmp47 = __cil_tmp46 + 168;
1649#line 105
1650 __cil_tmp48 = *((struct device **)__cil_tmp47);
1651#line 105
1652 __cil_tmp49 = (struct device const *)__cil_tmp48;
1653#line 105
1654 __cil_tmp50 = (unsigned long )pdata;
1655#line 105
1656 __cil_tmp51 = __cil_tmp50 + 12;
1657#line 105
1658 __cil_tmp52 = *((int *)__cil_tmp51);
1659#line 105
1660 dev_err(__cil_tmp49, "Invalid backup current limit %duA\n", __cil_tmp52);
1661 }
1662 } else {
1663 switch_break___0: ;
1664 }
1665 }
1666 }
1667 }
1668 ldv_17507:
1669 {
1670#line 109
1671 ret = wm831x_reg_unlock(wm831x);
1672 }
1673#line 110
1674 if (ret != 0) {
1675 {
1676#line 111
1677 __cil_tmp53 = (unsigned long )wm831x;
1678#line 111
1679 __cil_tmp54 = __cil_tmp53 + 168;
1680#line 111
1681 __cil_tmp55 = *((struct device **)__cil_tmp54);
1682#line 111
1683 __cil_tmp56 = (struct device const *)__cil_tmp55;
1684#line 111
1685 dev_err(__cil_tmp56, "Failed to unlock registers: %d\n", ret);
1686 }
1687#line 112
1688 return;
1689 } else {
1690
1691 }
1692 {
1693#line 115
1694 __cil_tmp57 = (unsigned short )reg;
1695#line 115
1696 __cil_tmp58 = (int )__cil_tmp57;
1697#line 115
1698 __cil_tmp59 = (unsigned short )__cil_tmp58;
1699#line 115
1700 ret = wm831x_set_bits(wm831x, (unsigned short)16459, (unsigned short)38931, __cil_tmp59);
1701 }
1702#line 122
1703 if (ret != 0) {
1704 {
1705#line 123
1706 __cil_tmp60 = (unsigned long )wm831x;
1707#line 123
1708 __cil_tmp61 = __cil_tmp60 + 168;
1709#line 123
1710 __cil_tmp62 = *((struct device **)__cil_tmp61);
1711#line 123
1712 __cil_tmp63 = (struct device const *)__cil_tmp62;
1713#line 123
1714 dev_err(__cil_tmp63, "Failed to set backup charger config: %d\n", ret);
1715 }
1716 } else {
1717
1718 }
1719 {
1720#line 126
1721 wm831x_reg_lock(wm831x);
1722 }
1723#line 127
1724 return;
1725}
1726}
1727#line 129 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
1728static int wm831x_backup_get_prop(struct power_supply *psy , enum power_supply_property psp ,
1729 union power_supply_propval *val )
1730{ struct wm831x_backup *devdata ;
1731 void *tmp ;
1732 struct wm831x *wm831x ;
1733 int ret ;
1734 unsigned long __cil_tmp8 ;
1735 unsigned long __cil_tmp9 ;
1736 struct device *__cil_tmp10 ;
1737 struct device *__cil_tmp11 ;
1738 struct device const *__cil_tmp12 ;
1739 unsigned int __cil_tmp13 ;
1740 int __cil_tmp14 ;
1741 enum wm831x_auxadc __cil_tmp15 ;
1742 int __cil_tmp16 ;
1743
1744 {
1745 {
1746#line 133
1747 __cil_tmp8 = (unsigned long )psy;
1748#line 133
1749 __cil_tmp9 = __cil_tmp8 + 96;
1750#line 133
1751 __cil_tmp10 = *((struct device **)__cil_tmp9);
1752#line 133
1753 __cil_tmp11 = *((struct device **)__cil_tmp10);
1754#line 133
1755 __cil_tmp12 = (struct device const *)__cil_tmp11;
1756#line 133
1757 tmp = dev_get_drvdata(__cil_tmp12);
1758#line 133
1759 devdata = (struct wm831x_backup *)tmp;
1760#line 134
1761 wm831x = *((struct wm831x **)devdata);
1762#line 135
1763 ret = 0;
1764#line 137
1765 ret = wm831x_reg_read(wm831x, (unsigned short)16459);
1766 }
1767#line 138
1768 if (ret < 0) {
1769#line 139
1770 return (ret);
1771 } else {
1772
1773 }
1774 {
1775#line 141
1776 __cil_tmp13 = (unsigned int )psp;
1777#line 142
1778 if ((int )__cil_tmp13 == 0) {
1779#line 142
1780 goto case_0;
1781 } else
1782#line 149
1783 if ((int )__cil_tmp13 == 11) {
1784#line 149
1785 goto case_11;
1786 } else
1787#line 154
1788 if ((int )__cil_tmp13 == 3) {
1789#line 154
1790 goto case_3;
1791 } else {
1792 {
1793#line 161
1794 goto switch_default;
1795#line 141
1796 if (0) {
1797 case_0: ;
1798 {
1799#line 143
1800 __cil_tmp14 = ret & 16384;
1801#line 143
1802 if (__cil_tmp14 != 0) {
1803#line 144
1804 *((int *)val) = 1;
1805 } else {
1806#line 146
1807 *((int *)val) = 3;
1808 }
1809 }
1810#line 147
1811 goto ldv_17521;
1812 case_11:
1813 {
1814#line 150
1815 __cil_tmp15 = (enum wm831x_auxadc )10;
1816#line 150
1817 ret = wm831x_backup_read_voltage(wm831x, __cil_tmp15, val);
1818 }
1819#line 152
1820 goto ldv_17521;
1821 case_3: ;
1822 {
1823#line 155
1824 __cil_tmp16 = ret & 16384;
1825#line 155
1826 if (__cil_tmp16 != 0) {
1827#line 156
1828 *((int *)val) = 1;
1829 } else {
1830#line 158
1831 *((int *)val) = 0;
1832 }
1833 }
1834#line 159
1835 goto ldv_17521;
1836 switch_default:
1837#line 162
1838 ret = -22;
1839#line 163
1840 goto ldv_17521;
1841 } else {
1842 switch_break: ;
1843 }
1844 }
1845 }
1846 }
1847 ldv_17521: ;
1848#line 166
1849 return (ret);
1850}
1851}
1852#line 169 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
1853static enum power_supply_property wm831x_backup_props[3U] = { (enum power_supply_property )0, (enum power_supply_property )11, (enum power_supply_property )3};
1854#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
1855static int wm831x_backup_probe(struct platform_device *pdev )
1856{ struct wm831x *wm831x ;
1857 void *tmp ;
1858 struct wm831x_pdata *wm831x_pdata ;
1859 struct wm831x_backup *devdata ;
1860 struct power_supply *backup ;
1861 int ret ;
1862 void *tmp___0 ;
1863 unsigned long __cil_tmp9 ;
1864 unsigned long __cil_tmp10 ;
1865 struct device *__cil_tmp11 ;
1866 struct device const *__cil_tmp12 ;
1867 unsigned long __cil_tmp13 ;
1868 unsigned long __cil_tmp14 ;
1869 struct device *__cil_tmp15 ;
1870 unsigned long __cil_tmp16 ;
1871 unsigned long __cil_tmp17 ;
1872 void *__cil_tmp18 ;
1873 struct wm831x_backup *__cil_tmp19 ;
1874 unsigned long __cil_tmp20 ;
1875 unsigned long __cil_tmp21 ;
1876 void *__cil_tmp22 ;
1877 unsigned long __cil_tmp23 ;
1878 unsigned long __cil_tmp24 ;
1879 struct wm831x_pdata *__cil_tmp25 ;
1880 unsigned long __cil_tmp26 ;
1881 unsigned long __cil_tmp27 ;
1882 int __cil_tmp28 ;
1883 unsigned long __cil_tmp29 ;
1884 unsigned long __cil_tmp30 ;
1885 char (*__cil_tmp31)[20U] ;
1886 char *__cil_tmp32 ;
1887 int __cil_tmp33 ;
1888 unsigned long __cil_tmp34 ;
1889 unsigned long __cil_tmp35 ;
1890 char (*__cil_tmp36)[20U] ;
1891 char *__cil_tmp37 ;
1892 unsigned long __cil_tmp38 ;
1893 unsigned long __cil_tmp39 ;
1894 char (*__cil_tmp40)[20U] ;
1895 char *__cil_tmp41 ;
1896 unsigned long __cil_tmp42 ;
1897 unsigned long __cil_tmp43 ;
1898 char (*__cil_tmp44)[20U] ;
1899 unsigned long __cil_tmp45 ;
1900 unsigned long __cil_tmp46 ;
1901 unsigned long __cil_tmp47 ;
1902 unsigned long __cil_tmp48 ;
1903 unsigned long __cil_tmp49 ;
1904 unsigned long __cil_tmp50 ;
1905 unsigned long __cil_tmp51 ;
1906 unsigned long __cil_tmp52 ;
1907 unsigned long __cil_tmp53 ;
1908 unsigned long __cil_tmp54 ;
1909 struct device *__cil_tmp55 ;
1910 void const *__cil_tmp56 ;
1911
1912 {
1913 {
1914#line 181
1915 __cil_tmp9 = (unsigned long )pdev;
1916#line 181
1917 __cil_tmp10 = __cil_tmp9 + 16;
1918#line 181
1919 __cil_tmp11 = *((struct device **)__cil_tmp10);
1920#line 181
1921 __cil_tmp12 = (struct device const *)__cil_tmp11;
1922#line 181
1923 tmp = dev_get_drvdata(__cil_tmp12);
1924#line 181
1925 wm831x = (struct wm831x *)tmp;
1926#line 182
1927 __cil_tmp13 = (unsigned long )wm831x;
1928#line 182
1929 __cil_tmp14 = __cil_tmp13 + 168;
1930#line 182
1931 __cil_tmp15 = *((struct device **)__cil_tmp14);
1932#line 182
1933 __cil_tmp16 = (unsigned long )__cil_tmp15;
1934#line 182
1935 __cil_tmp17 = __cil_tmp16 + 280;
1936#line 182
1937 __cil_tmp18 = *((void **)__cil_tmp17);
1938#line 182
1939 wm831x_pdata = (struct wm831x_pdata *)__cil_tmp18;
1940#line 187
1941 tmp___0 = kzalloc(296UL, 208U);
1942#line 187
1943 devdata = (struct wm831x_backup *)tmp___0;
1944 }
1945 {
1946#line 188
1947 __cil_tmp19 = (struct wm831x_backup *)0;
1948#line 188
1949 __cil_tmp20 = (unsigned long )__cil_tmp19;
1950#line 188
1951 __cil_tmp21 = (unsigned long )devdata;
1952#line 188
1953 if (__cil_tmp21 == __cil_tmp20) {
1954#line 189
1955 return (-12);
1956 } else {
1957
1958 }
1959 }
1960 {
1961#line 191
1962 *((struct wm831x **)devdata) = wm831x;
1963#line 192
1964 __cil_tmp22 = (void *)devdata;
1965#line 192
1966 platform_set_drvdata(pdev, __cil_tmp22);
1967#line 194
1968 __cil_tmp23 = (unsigned long )devdata;
1969#line 194
1970 __cil_tmp24 = __cil_tmp23 + 8;
1971#line 194
1972 backup = (struct power_supply *)__cil_tmp24;
1973#line 200
1974 wm831x_config_backup(wm831x);
1975 }
1976 {
1977#line 202
1978 __cil_tmp25 = (struct wm831x_pdata *)0;
1979#line 202
1980 __cil_tmp26 = (unsigned long )__cil_tmp25;
1981#line 202
1982 __cil_tmp27 = (unsigned long )wm831x_pdata;
1983#line 202
1984 if (__cil_tmp27 != __cil_tmp26) {
1985 {
1986#line 202
1987 __cil_tmp28 = *((int *)wm831x_pdata);
1988#line 202
1989 if (__cil_tmp28 != 0) {
1990 {
1991#line 203
1992 __cil_tmp29 = (unsigned long )devdata;
1993#line 203
1994 __cil_tmp30 = __cil_tmp29 + 272;
1995#line 203
1996 __cil_tmp31 = (char (*)[20U])__cil_tmp30;
1997#line 203
1998 __cil_tmp32 = (char *)__cil_tmp31;
1999#line 203
2000 __cil_tmp33 = *((int *)wm831x_pdata);
2001#line 203
2002 snprintf(__cil_tmp32, 20UL, "wm831x-backup.%d", __cil_tmp33);
2003 }
2004 } else {
2005 {
2006#line 206
2007 __cil_tmp34 = (unsigned long )devdata;
2008#line 206
2009 __cil_tmp35 = __cil_tmp34 + 272;
2010#line 206
2011 __cil_tmp36 = (char (*)[20U])__cil_tmp35;
2012#line 206
2013 __cil_tmp37 = (char *)__cil_tmp36;
2014#line 206
2015 snprintf(__cil_tmp37, 20UL, "wm831x-backup");
2016 }
2017 }
2018 }
2019 } else {
2020 {
2021#line 206
2022 __cil_tmp38 = (unsigned long )devdata;
2023#line 206
2024 __cil_tmp39 = __cil_tmp38 + 272;
2025#line 206
2026 __cil_tmp40 = (char (*)[20U])__cil_tmp39;
2027#line 206
2028 __cil_tmp41 = (char *)__cil_tmp40;
2029#line 206
2030 snprintf(__cil_tmp41, 20UL, "wm831x-backup");
2031 }
2032 }
2033 }
2034 {
2035#line 209
2036 __cil_tmp42 = (unsigned long )devdata;
2037#line 209
2038 __cil_tmp43 = __cil_tmp42 + 272;
2039#line 209
2040 __cil_tmp44 = (char (*)[20U])__cil_tmp43;
2041#line 209
2042 *((char const **)backup) = (char const *)__cil_tmp44;
2043#line 210
2044 __cil_tmp45 = (unsigned long )backup;
2045#line 210
2046 __cil_tmp46 = __cil_tmp45 + 8;
2047#line 210
2048 *((enum power_supply_type *)__cil_tmp46) = (enum power_supply_type )1;
2049#line 211
2050 __cil_tmp47 = (unsigned long )backup;
2051#line 211
2052 __cil_tmp48 = __cil_tmp47 + 16;
2053#line 211
2054 *((enum power_supply_property **)__cil_tmp48) = (enum power_supply_property *)(& wm831x_backup_props);
2055#line 212
2056 __cil_tmp49 = (unsigned long )backup;
2057#line 212
2058 __cil_tmp50 = __cil_tmp49 + 24;
2059#line 212
2060 *((size_t *)__cil_tmp50) = 3UL;
2061#line 213
2062 __cil_tmp51 = (unsigned long )backup;
2063#line 213
2064 __cil_tmp52 = __cil_tmp51 + 48;
2065#line 213
2066 *((int (**)(struct power_supply * , enum power_supply_property , union power_supply_propval * ))__cil_tmp52) = & wm831x_backup_get_prop;
2067#line 214
2068 __cil_tmp53 = (unsigned long )pdev;
2069#line 214
2070 __cil_tmp54 = __cil_tmp53 + 16;
2071#line 214
2072 __cil_tmp55 = (struct device *)__cil_tmp54;
2073#line 214
2074 ret = power_supply_register(__cil_tmp55, backup);
2075 }
2076#line 215
2077 if (ret != 0) {
2078#line 216
2079 goto err_kmalloc;
2080 } else {
2081
2082 }
2083#line 218
2084 return (ret);
2085 err_kmalloc:
2086 {
2087#line 221
2088 __cil_tmp56 = (void const *)devdata;
2089#line 221
2090 kfree(__cil_tmp56);
2091 }
2092#line 222
2093 return (ret);
2094}
2095}
2096#line 267
2097extern void ldv_check_final_state(void) ;
2098#line 270
2099extern void ldv_check_return_value(int ) ;
2100#line 273
2101extern void ldv_initialize(void) ;
2102#line 276
2103extern int __VERIFIER_nondet_int(void) ;
2104#line 279 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2105int LDV_IN_INTERRUPT ;
2106#line 282 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2107void main(void)
2108{ struct platform_device *var_group1 ;
2109 int res_wm831x_backup_probe_3 ;
2110 int ldv_s_wm831x_backup_driver_platform_driver ;
2111 int tmp ;
2112 int tmp___0 ;
2113
2114 {
2115 {
2116#line 312
2117 ldv_s_wm831x_backup_driver_platform_driver = 0;
2118#line 302
2119 LDV_IN_INTERRUPT = 1;
2120#line 311
2121 ldv_initialize();
2122 }
2123#line 315
2124 goto ldv_17582;
2125 ldv_17581:
2126 {
2127#line 319
2128 tmp = __VERIFIER_nondet_int();
2129 }
2130#line 321
2131 if (tmp == 0) {
2132#line 321
2133 goto case_0;
2134 } else {
2135 {
2136#line 340
2137 goto switch_default;
2138#line 319
2139 if (0) {
2140 case_0: ;
2141#line 324
2142 if (ldv_s_wm831x_backup_driver_platform_driver == 0) {
2143 {
2144#line 329
2145 res_wm831x_backup_probe_3 = wm831x_backup_probe(var_group1);
2146#line 330
2147 ldv_check_return_value(res_wm831x_backup_probe_3);
2148 }
2149#line 331
2150 if (res_wm831x_backup_probe_3 != 0) {
2151#line 332
2152 goto ldv_module_exit;
2153 } else {
2154
2155 }
2156#line 333
2157 ldv_s_wm831x_backup_driver_platform_driver = 0;
2158 } else {
2159
2160 }
2161#line 339
2162 goto ldv_17579;
2163 switch_default: ;
2164#line 340
2165 goto ldv_17579;
2166 } else {
2167 switch_break: ;
2168 }
2169 }
2170 }
2171 ldv_17579: ;
2172 ldv_17582:
2173 {
2174#line 315
2175 tmp___0 = __VERIFIER_nondet_int();
2176 }
2177#line 315
2178 if (tmp___0 != 0) {
2179#line 317
2180 goto ldv_17581;
2181 } else
2182#line 315
2183 if (ldv_s_wm831x_backup_driver_platform_driver != 0) {
2184#line 317
2185 goto ldv_17581;
2186 } else {
2187#line 319
2188 goto ldv_17583;
2189 }
2190 ldv_17583: ;
2191 ldv_module_exit: ;
2192 {
2193#line 349
2194 ldv_check_final_state();
2195 }
2196#line 352
2197 return;
2198}
2199}
2200#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2201void ldv_blast_assert(void)
2202{
2203
2204 {
2205 ERROR: ;
2206#line 6
2207 goto ERROR;
2208}
2209}
2210#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2211extern int __VERIFIER_nondet_int(void) ;
2212#line 373 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2213int ldv_spin = 0;
2214#line 377 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2215void ldv_check_alloc_flags(gfp_t flags )
2216{
2217
2218 {
2219#line 380
2220 if (ldv_spin != 0) {
2221#line 380
2222 if (flags != 32U) {
2223 {
2224#line 380
2225 ldv_blast_assert();
2226 }
2227 } else {
2228
2229 }
2230 } else {
2231
2232 }
2233#line 383
2234 return;
2235}
2236}
2237#line 383
2238extern struct page *ldv_some_page(void) ;
2239#line 386 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2240struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
2241{ struct page *tmp ;
2242
2243 {
2244#line 389
2245 if (ldv_spin != 0) {
2246#line 389
2247 if (flags != 32U) {
2248 {
2249#line 389
2250 ldv_blast_assert();
2251 }
2252 } else {
2253
2254 }
2255 } else {
2256
2257 }
2258 {
2259#line 391
2260 tmp = ldv_some_page();
2261 }
2262#line 391
2263 return (tmp);
2264}
2265}
2266#line 395 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2267void ldv_check_alloc_nonatomic(void)
2268{
2269
2270 {
2271#line 398
2272 if (ldv_spin != 0) {
2273 {
2274#line 398
2275 ldv_blast_assert();
2276 }
2277 } else {
2278
2279 }
2280#line 401
2281 return;
2282}
2283}
2284#line 402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2285void ldv_spin_lock(void)
2286{
2287
2288 {
2289#line 405
2290 ldv_spin = 1;
2291#line 406
2292 return;
2293}
2294}
2295#line 409 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2296void ldv_spin_unlock(void)
2297{
2298
2299 {
2300#line 412
2301 ldv_spin = 0;
2302#line 413
2303 return;
2304}
2305}
2306#line 416 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2307int ldv_spin_trylock(void)
2308{ int is_lock ;
2309
2310 {
2311 {
2312#line 421
2313 is_lock = __VERIFIER_nondet_int();
2314 }
2315#line 423
2316 if (is_lock != 0) {
2317#line 426
2318 return (0);
2319 } else {
2320#line 431
2321 ldv_spin = 1;
2322#line 433
2323 return (1);
2324 }
2325}
2326}
2327#line 600 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2328void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
2329{
2330
2331 {
2332 {
2333#line 606
2334 ldv_check_alloc_flags(ldv_func_arg2);
2335#line 608
2336 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2337 }
2338#line 609
2339 return ((void *)0);
2340}
2341}
2342#line 611 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2343__inline static void *kzalloc(size_t size , gfp_t flags )
2344{ void *tmp ;
2345
2346 {
2347 {
2348#line 617
2349 ldv_check_alloc_flags(flags);
2350#line 618
2351 tmp = __VERIFIER_nondet_pointer();
2352 }
2353#line 618
2354 return (tmp);
2355}
2356}