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/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
778enum led_brightness {
779 LED_OFF = 0,
780 LED_HALF = 127,
781 LED_FULL = 255
782} ;
783#line 21
784struct led_trigger;
785#line 21 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
786struct led_classdev {
787 char const *name ;
788 int brightness ;
789 int max_brightness ;
790 int flags ;
791 void (*brightness_set)(struct led_classdev * , enum led_brightness ) ;
792 enum led_brightness (*brightness_get)(struct led_classdev * ) ;
793 int (*blink_set)(struct led_classdev * , unsigned long * , unsigned long * ) ;
794 struct device *dev ;
795 struct list_head node ;
796 char const *default_trigger ;
797 unsigned long blink_delay_on ;
798 unsigned long blink_delay_off ;
799 struct timer_list blink_timer ;
800 int blink_brightness ;
801 struct rw_semaphore trigger_lock ;
802 struct led_trigger *trigger ;
803 struct list_head trig_list ;
804 void *trigger_data ;
805};
806#line 113 "include/linux/leds.h"
807struct led_trigger {
808 char const *name ;
809 void (*activate)(struct led_classdev * ) ;
810 void (*deactivate)(struct led_classdev * ) ;
811 rwlock_t leddev_list_lock ;
812 struct list_head led_cdevs ;
813 struct list_head next_trig ;
814};
815#line 210
816struct platform_device;
817#line 211 "include/linux/leds.h"
818struct led_regulator_platform_data {
819 char *name ;
820 enum led_brightness brightness ;
821};
822#line 45 "include/linux/leds-regulator.h"
823struct klist_node;
824#line 45
825struct klist_node;
826#line 37 "include/linux/klist.h"
827struct klist_node {
828 void *n_klist ;
829 struct list_head n_node ;
830 struct kref n_ref ;
831};
832#line 67
833struct dma_map_ops;
834#line 67 "include/linux/klist.h"
835struct dev_archdata {
836 void *acpi_handle ;
837 struct dma_map_ops *dma_ops ;
838 void *iommu ;
839};
840#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
841struct pdev_archdata {
842
843};
844#line 17
845struct device_private;
846#line 17
847struct device_private;
848#line 18
849struct device_driver;
850#line 18
851struct device_driver;
852#line 19
853struct driver_private;
854#line 19
855struct driver_private;
856#line 20
857struct class;
858#line 20
859struct class;
860#line 21
861struct subsys_private;
862#line 21
863struct subsys_private;
864#line 22
865struct bus_type;
866#line 22
867struct bus_type;
868#line 23
869struct device_node;
870#line 23
871struct device_node;
872#line 24
873struct iommu_ops;
874#line 24
875struct iommu_ops;
876#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
877struct bus_attribute {
878 struct attribute attr ;
879 ssize_t (*show)(struct bus_type * , char * ) ;
880 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
881};
882#line 51 "include/linux/device.h"
883struct device_attribute;
884#line 51
885struct driver_attribute;
886#line 51 "include/linux/device.h"
887struct bus_type {
888 char const *name ;
889 char const *dev_name ;
890 struct device *dev_root ;
891 struct bus_attribute *bus_attrs ;
892 struct device_attribute *dev_attrs ;
893 struct driver_attribute *drv_attrs ;
894 int (*match)(struct device * , struct device_driver * ) ;
895 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
896 int (*probe)(struct device * ) ;
897 int (*remove)(struct device * ) ;
898 void (*shutdown)(struct device * ) ;
899 int (*suspend)(struct device * , pm_message_t ) ;
900 int (*resume)(struct device * ) ;
901 struct dev_pm_ops const *pm ;
902 struct iommu_ops *iommu_ops ;
903 struct subsys_private *p ;
904};
905#line 125
906struct device_type;
907#line 182
908struct of_device_id;
909#line 182 "include/linux/device.h"
910struct device_driver {
911 char const *name ;
912 struct bus_type *bus ;
913 struct module *owner ;
914 char const *mod_name ;
915 bool suppress_bind_attrs ;
916 struct of_device_id const *of_match_table ;
917 int (*probe)(struct device * ) ;
918 int (*remove)(struct device * ) ;
919 void (*shutdown)(struct device * ) ;
920 int (*suspend)(struct device * , pm_message_t ) ;
921 int (*resume)(struct device * ) ;
922 struct attribute_group const **groups ;
923 struct dev_pm_ops const *pm ;
924 struct driver_private *p ;
925};
926#line 245 "include/linux/device.h"
927struct driver_attribute {
928 struct attribute attr ;
929 ssize_t (*show)(struct device_driver * , char * ) ;
930 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
931};
932#line 299
933struct class_attribute;
934#line 299 "include/linux/device.h"
935struct class {
936 char const *name ;
937 struct module *owner ;
938 struct class_attribute *class_attrs ;
939 struct device_attribute *dev_attrs ;
940 struct bin_attribute *dev_bin_attrs ;
941 struct kobject *dev_kobj ;
942 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
943 char *(*devnode)(struct device * , umode_t * ) ;
944 void (*class_release)(struct class * ) ;
945 void (*dev_release)(struct device * ) ;
946 int (*suspend)(struct device * , pm_message_t ) ;
947 int (*resume)(struct device * ) ;
948 struct kobj_ns_type_operations const *ns_type ;
949 void const *(*namespace)(struct device * ) ;
950 struct dev_pm_ops const *pm ;
951 struct subsys_private *p ;
952};
953#line 394 "include/linux/device.h"
954struct class_attribute {
955 struct attribute attr ;
956 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
957 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
958 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
959};
960#line 447 "include/linux/device.h"
961struct device_type {
962 char const *name ;
963 struct attribute_group const **groups ;
964 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
965 char *(*devnode)(struct device * , umode_t * ) ;
966 void (*release)(struct device * ) ;
967 struct dev_pm_ops const *pm ;
968};
969#line 474 "include/linux/device.h"
970struct device_attribute {
971 struct attribute attr ;
972 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
973 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
974 size_t ) ;
975};
976#line 557 "include/linux/device.h"
977struct device_dma_parameters {
978 unsigned int max_segment_size ;
979 unsigned long segment_boundary_mask ;
980};
981#line 567
982struct dma_coherent_mem;
983#line 567 "include/linux/device.h"
984struct device {
985 struct device *parent ;
986 struct device_private *p ;
987 struct kobject kobj ;
988 char const *init_name ;
989 struct device_type const *type ;
990 struct mutex mutex ;
991 struct bus_type *bus ;
992 struct device_driver *driver ;
993 void *platform_data ;
994 struct dev_pm_info power ;
995 struct dev_pm_domain *pm_domain ;
996 int numa_node ;
997 u64 *dma_mask ;
998 u64 coherent_dma_mask ;
999 struct device_dma_parameters *dma_parms ;
1000 struct list_head dma_pools ;
1001 struct dma_coherent_mem *dma_mem ;
1002 struct dev_archdata archdata ;
1003 struct device_node *of_node ;
1004 dev_t devt ;
1005 u32 id ;
1006 spinlock_t devres_lock ;
1007 struct list_head devres_head ;
1008 struct klist_node knode_class ;
1009 struct class *class ;
1010 struct attribute_group const **groups ;
1011 void (*release)(struct device * ) ;
1012};
1013#line 681 "include/linux/device.h"
1014struct wakeup_source {
1015 char const *name ;
1016 struct list_head entry ;
1017 spinlock_t lock ;
1018 struct timer_list timer ;
1019 unsigned long timer_expires ;
1020 ktime_t total_time ;
1021 ktime_t max_time ;
1022 ktime_t last_time ;
1023 unsigned long event_count ;
1024 unsigned long active_count ;
1025 unsigned long relax_count ;
1026 unsigned long hit_count ;
1027 unsigned char active : 1 ;
1028};
1029#line 12 "include/linux/mod_devicetable.h"
1030typedef unsigned long kernel_ulong_t;
1031#line 215 "include/linux/mod_devicetable.h"
1032struct of_device_id {
1033 char name[32U] ;
1034 char type[32U] ;
1035 char compatible[128U] ;
1036 void *data ;
1037};
1038#line 492 "include/linux/mod_devicetable.h"
1039struct platform_device_id {
1040 char name[20U] ;
1041 kernel_ulong_t driver_data ;
1042};
1043#line 584
1044struct mfd_cell;
1045#line 584
1046struct mfd_cell;
1047#line 585 "include/linux/mod_devicetable.h"
1048struct platform_device {
1049 char const *name ;
1050 int id ;
1051 struct device dev ;
1052 u32 num_resources ;
1053 struct resource *resource ;
1054 struct platform_device_id const *id_entry ;
1055 struct mfd_cell *mfd_cell ;
1056 struct pdev_archdata archdata ;
1057};
1058#line 272 "include/linux/platform_device.h"
1059struct regulator;
1060#line 272
1061struct regulator;
1062#line 189 "include/linux/regulator/consumer.h"
1063struct regulator_led {
1064 struct led_classdev cdev ;
1065 enum led_brightness value ;
1066 int enabled ;
1067 struct mutex mutex ;
1068 struct work_struct work ;
1069 struct regulator *vcc ;
1070};
1071#line 1 "<compiler builtins>"
1072long __builtin_expect(long , long ) ;
1073#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
1074void ldv_spin_lock(void) ;
1075#line 3
1076void ldv_spin_unlock(void) ;
1077#line 4
1078int ldv_spin_trylock(void) ;
1079#line 50 "include/linux/dynamic_debug.h"
1080extern int __dynamic_dev_dbg(struct _ddebug * , struct device const * , char const *
1081 , ...) ;
1082#line 24 "include/linux/list.h"
1083__inline static void INIT_LIST_HEAD(struct list_head *list )
1084{ unsigned long __cil_tmp2 ;
1085 unsigned long __cil_tmp3 ;
1086
1087 {
1088#line 26
1089 *((struct list_head **)list) = list;
1090#line 27
1091 __cil_tmp2 = (unsigned long )list;
1092#line 27
1093 __cil_tmp3 = __cil_tmp2 + 8;
1094#line 27
1095 *((struct list_head **)__cil_tmp3) = list;
1096#line 28
1097 return;
1098}
1099}
1100#line 27 "include/linux/err.h"
1101__inline static long PTR_ERR(void const *ptr )
1102{
1103
1104 {
1105#line 29
1106 return ((long )ptr);
1107}
1108}
1109#line 32 "include/linux/err.h"
1110__inline static long IS_ERR(void const *ptr )
1111{ long tmp ;
1112 unsigned long __cil_tmp3 ;
1113 int __cil_tmp4 ;
1114 long __cil_tmp5 ;
1115
1116 {
1117 {
1118#line 34
1119 __cil_tmp3 = (unsigned long )ptr;
1120#line 34
1121 __cil_tmp4 = __cil_tmp3 > 0xfffffffffffff000UL;
1122#line 34
1123 __cil_tmp5 = (long )__cil_tmp4;
1124#line 34
1125 tmp = __builtin_expect(__cil_tmp5, 0L);
1126 }
1127#line 34
1128 return (tmp);
1129}
1130}
1131#line 261 "include/linux/lockdep.h"
1132extern void lockdep_init_map(struct lockdep_map * , char const * , struct lock_class_key * ,
1133 int ) ;
1134#line 115 "include/linux/mutex.h"
1135extern void __mutex_init(struct mutex * , char const * , struct lock_class_key * ) ;
1136#line 134
1137extern void mutex_lock_nested(struct mutex * , unsigned int ) ;
1138#line 169
1139extern void mutex_unlock(struct mutex * ) ;
1140#line 156 "include/linux/workqueue.h"
1141extern void __init_work(struct work_struct * , int ) ;
1142#line 380
1143extern int schedule_work(struct work_struct * ) ;
1144#line 392
1145extern bool cancel_work_sync(struct work_struct * ) ;
1146#line 161 "include/linux/slab.h"
1147extern void kfree(void const * ) ;
1148#line 220 "include/linux/slub_def.h"
1149extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1150#line 223
1151void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1152#line 353 "include/linux/slab.h"
1153__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1154#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
1155extern void *__VERIFIER_nondet_pointer(void) ;
1156#line 11
1157void ldv_check_alloc_flags(gfp_t flags ) ;
1158#line 12
1159void ldv_check_alloc_nonatomic(void) ;
1160#line 14
1161struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1162#line 79 "include/linux/leds.h"
1163extern int led_classdev_register(struct device * , struct led_classdev * ) ;
1164#line 793 "include/linux/device.h"
1165extern int dev_set_drvdata(struct device * , void * ) ;
1166#line 892
1167extern int dev_err(struct device const * , char const * , ...) ;
1168#line 188 "include/linux/platform_device.h"
1169__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )
1170{ unsigned long __cil_tmp3 ;
1171 unsigned long __cil_tmp4 ;
1172 struct device *__cil_tmp5 ;
1173
1174 {
1175 {
1176#line 190
1177 __cil_tmp3 = (unsigned long )pdev;
1178#line 190
1179 __cil_tmp4 = __cil_tmp3 + 16;
1180#line 190
1181 __cil_tmp5 = (struct device *)__cil_tmp4;
1182#line 190
1183 dev_set_drvdata(__cil_tmp5, data);
1184 }
1185#line 191
1186 return;
1187}
1188}
1189#line 138 "include/linux/regulator/consumer.h"
1190extern struct regulator *regulator_get_exclusive(struct device * , char const * ) ;
1191#line 140
1192extern void regulator_put(struct regulator * ) ;
1193#line 144
1194extern int regulator_enable(struct regulator * ) ;
1195#line 145
1196extern int regulator_disable(struct regulator * ) ;
1197#line 147
1198extern int regulator_is_enabled(struct regulator * ) ;
1199#line 163
1200extern int regulator_count_voltages(struct regulator * ) ;
1201#line 164
1202extern int regulator_list_voltage(struct regulator * , unsigned int ) ;
1203#line 167
1204extern int regulator_set_voltage(struct regulator * , int , int ) ;
1205#line 51 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
1206__inline static int led_regulator_get_max_brightness(struct regulator *supply )
1207{ int ret ;
1208 int voltage ;
1209 int tmp ;
1210 int tmp___0 ;
1211
1212 {
1213 {
1214#line 54
1215 tmp = regulator_list_voltage(supply, 0U);
1216#line 54
1217 voltage = tmp;
1218 }
1219#line 56
1220 if (voltage <= 0) {
1221#line 57
1222 return (1);
1223 } else {
1224
1225 }
1226 {
1227#line 63
1228 ret = regulator_set_voltage(supply, voltage, voltage);
1229 }
1230#line 64
1231 if (ret < 0) {
1232#line 65
1233 return (1);
1234 } else {
1235
1236 }
1237 {
1238#line 67
1239 tmp___0 = regulator_count_voltages(supply);
1240 }
1241#line 67
1242 return (tmp___0);
1243}
1244}
1245#line 70 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
1246static int led_regulator_get_voltage(struct regulator *supply , enum led_brightness brightness )
1247{ int tmp ;
1248 unsigned int __cil_tmp4 ;
1249 unsigned int __cil_tmp5 ;
1250 unsigned int __cil_tmp6 ;
1251
1252 {
1253 {
1254#line 73
1255 __cil_tmp4 = (unsigned int )brightness;
1256#line 73
1257 if (__cil_tmp4 == 0U) {
1258#line 74
1259 return (-22);
1260 } else {
1261
1262 }
1263 }
1264 {
1265#line 76
1266 __cil_tmp5 = (unsigned int )brightness;
1267#line 76
1268 __cil_tmp6 = __cil_tmp5 - 1U;
1269#line 76
1270 tmp = regulator_list_voltage(supply, __cil_tmp6);
1271 }
1272#line 76
1273 return (tmp);
1274}
1275}
1276#line 80 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
1277static void regulator_led_enable(struct regulator_led *led )
1278{ int ret ;
1279 unsigned long __cil_tmp3 ;
1280 unsigned long __cil_tmp4 ;
1281 int __cil_tmp5 ;
1282 unsigned long __cil_tmp6 ;
1283 unsigned long __cil_tmp7 ;
1284 struct regulator *__cil_tmp8 ;
1285 unsigned long __cil_tmp9 ;
1286 unsigned long __cil_tmp10 ;
1287 unsigned long __cil_tmp11 ;
1288 struct device *__cil_tmp12 ;
1289 struct device const *__cil_tmp13 ;
1290 unsigned long __cil_tmp14 ;
1291 unsigned long __cil_tmp15 ;
1292
1293 {
1294 {
1295#line 84
1296 __cil_tmp3 = (unsigned long )led;
1297#line 84
1298 __cil_tmp4 = __cil_tmp3 + 412;
1299#line 84
1300 __cil_tmp5 = *((int *)__cil_tmp4);
1301#line 84
1302 if (__cil_tmp5 != 0) {
1303#line 85
1304 return;
1305 } else {
1306
1307 }
1308 }
1309 {
1310#line 87
1311 __cil_tmp6 = (unsigned long )led;
1312#line 87
1313 __cil_tmp7 = __cil_tmp6 + 664;
1314#line 87
1315 __cil_tmp8 = *((struct regulator **)__cil_tmp7);
1316#line 87
1317 ret = regulator_enable(__cil_tmp8);
1318 }
1319#line 88
1320 if (ret != 0) {
1321 {
1322#line 89
1323 __cil_tmp9 = 0 + 48;
1324#line 89
1325 __cil_tmp10 = (unsigned long )led;
1326#line 89
1327 __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
1328#line 89
1329 __cil_tmp12 = *((struct device **)__cil_tmp11);
1330#line 89
1331 __cil_tmp13 = (struct device const *)__cil_tmp12;
1332#line 89
1333 dev_err(__cil_tmp13, "Failed to enable vcc: %d\n", ret);
1334 }
1335#line 90
1336 return;
1337 } else {
1338
1339 }
1340#line 93
1341 __cil_tmp14 = (unsigned long )led;
1342#line 93
1343 __cil_tmp15 = __cil_tmp14 + 412;
1344#line 93
1345 *((int *)__cil_tmp15) = 1;
1346#line 94
1347 return;
1348}
1349}
1350#line 96 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
1351static void regulator_led_disable(struct regulator_led *led )
1352{ int ret ;
1353 unsigned long __cil_tmp3 ;
1354 unsigned long __cil_tmp4 ;
1355 int __cil_tmp5 ;
1356 unsigned long __cil_tmp6 ;
1357 unsigned long __cil_tmp7 ;
1358 struct regulator *__cil_tmp8 ;
1359 unsigned long __cil_tmp9 ;
1360 unsigned long __cil_tmp10 ;
1361 unsigned long __cil_tmp11 ;
1362 struct device *__cil_tmp12 ;
1363 struct device const *__cil_tmp13 ;
1364 unsigned long __cil_tmp14 ;
1365 unsigned long __cil_tmp15 ;
1366
1367 {
1368 {
1369#line 100
1370 __cil_tmp3 = (unsigned long )led;
1371#line 100
1372 __cil_tmp4 = __cil_tmp3 + 412;
1373#line 100
1374 __cil_tmp5 = *((int *)__cil_tmp4);
1375#line 100
1376 if (__cil_tmp5 == 0) {
1377#line 101
1378 return;
1379 } else {
1380
1381 }
1382 }
1383 {
1384#line 103
1385 __cil_tmp6 = (unsigned long )led;
1386#line 103
1387 __cil_tmp7 = __cil_tmp6 + 664;
1388#line 103
1389 __cil_tmp8 = *((struct regulator **)__cil_tmp7);
1390#line 103
1391 ret = regulator_disable(__cil_tmp8);
1392 }
1393#line 104
1394 if (ret != 0) {
1395 {
1396#line 105
1397 __cil_tmp9 = 0 + 48;
1398#line 105
1399 __cil_tmp10 = (unsigned long )led;
1400#line 105
1401 __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
1402#line 105
1403 __cil_tmp12 = *((struct device **)__cil_tmp11);
1404#line 105
1405 __cil_tmp13 = (struct device const *)__cil_tmp12;
1406#line 105
1407 dev_err(__cil_tmp13, "Failed to disable vcc: %d\n", ret);
1408 }
1409#line 106
1410 return;
1411 } else {
1412
1413 }
1414#line 109
1415 __cil_tmp14 = (unsigned long )led;
1416#line 109
1417 __cil_tmp15 = __cil_tmp14 + 412;
1418#line 109
1419 *((int *)__cil_tmp15) = 0;
1420#line 110
1421 return;
1422}
1423}
1424#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
1425static void regulator_led_set_value(struct regulator_led *led )
1426{ int voltage ;
1427 int ret ;
1428 struct _ddebug descriptor ;
1429 long tmp ;
1430 unsigned long __cil_tmp6 ;
1431 unsigned long __cil_tmp7 ;
1432 struct mutex *__cil_tmp8 ;
1433 unsigned long __cil_tmp9 ;
1434 unsigned long __cil_tmp10 ;
1435 enum led_brightness __cil_tmp11 ;
1436 unsigned int __cil_tmp12 ;
1437 unsigned long __cil_tmp13 ;
1438 unsigned long __cil_tmp14 ;
1439 unsigned long __cil_tmp15 ;
1440 int __cil_tmp16 ;
1441 unsigned long __cil_tmp17 ;
1442 unsigned long __cil_tmp18 ;
1443 struct regulator *__cil_tmp19 ;
1444 unsigned long __cil_tmp20 ;
1445 unsigned long __cil_tmp21 ;
1446 enum led_brightness __cil_tmp22 ;
1447 struct _ddebug *__cil_tmp23 ;
1448 unsigned long __cil_tmp24 ;
1449 unsigned long __cil_tmp25 ;
1450 unsigned long __cil_tmp26 ;
1451 unsigned long __cil_tmp27 ;
1452 unsigned long __cil_tmp28 ;
1453 unsigned long __cil_tmp29 ;
1454 unsigned char __cil_tmp30 ;
1455 long __cil_tmp31 ;
1456 long __cil_tmp32 ;
1457 unsigned long __cil_tmp33 ;
1458 unsigned long __cil_tmp34 ;
1459 unsigned long __cil_tmp35 ;
1460 struct device *__cil_tmp36 ;
1461 struct device const *__cil_tmp37 ;
1462 unsigned long __cil_tmp38 ;
1463 unsigned long __cil_tmp39 ;
1464 enum led_brightness __cil_tmp40 ;
1465 unsigned int __cil_tmp41 ;
1466 unsigned long __cil_tmp42 ;
1467 unsigned long __cil_tmp43 ;
1468 struct regulator *__cil_tmp44 ;
1469 unsigned long __cil_tmp45 ;
1470 unsigned long __cil_tmp46 ;
1471 unsigned long __cil_tmp47 ;
1472 struct device *__cil_tmp48 ;
1473 struct device const *__cil_tmp49 ;
1474 unsigned long __cil_tmp50 ;
1475 unsigned long __cil_tmp51 ;
1476 struct mutex *__cil_tmp52 ;
1477
1478 {
1479 {
1480#line 117
1481 __cil_tmp6 = (unsigned long )led;
1482#line 117
1483 __cil_tmp7 = __cil_tmp6 + 416;
1484#line 117
1485 __cil_tmp8 = (struct mutex *)__cil_tmp7;
1486#line 117
1487 mutex_lock_nested(__cil_tmp8, 0U);
1488 }
1489 {
1490#line 119
1491 __cil_tmp9 = (unsigned long )led;
1492#line 119
1493 __cil_tmp10 = __cil_tmp9 + 408;
1494#line 119
1495 __cil_tmp11 = *((enum led_brightness *)__cil_tmp10);
1496#line 119
1497 __cil_tmp12 = (unsigned int )__cil_tmp11;
1498#line 119
1499 if (__cil_tmp12 == 0U) {
1500 {
1501#line 120
1502 regulator_led_disable(led);
1503 }
1504#line 121
1505 goto out;
1506 } else {
1507
1508 }
1509 }
1510 {
1511#line 124
1512 __cil_tmp13 = 0 + 12;
1513#line 124
1514 __cil_tmp14 = (unsigned long )led;
1515#line 124
1516 __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
1517#line 124
1518 __cil_tmp16 = *((int *)__cil_tmp15);
1519#line 124
1520 if (__cil_tmp16 > 1) {
1521 {
1522#line 125
1523 __cil_tmp17 = (unsigned long )led;
1524#line 125
1525 __cil_tmp18 = __cil_tmp17 + 664;
1526#line 125
1527 __cil_tmp19 = *((struct regulator **)__cil_tmp18);
1528#line 125
1529 __cil_tmp20 = (unsigned long )led;
1530#line 125
1531 __cil_tmp21 = __cil_tmp20 + 408;
1532#line 125
1533 __cil_tmp22 = *((enum led_brightness *)__cil_tmp21);
1534#line 125
1535 voltage = led_regulator_get_voltage(__cil_tmp19, __cil_tmp22);
1536#line 126
1537 __cil_tmp23 = & descriptor;
1538#line 126
1539 *((char const **)__cil_tmp23) = "leds_regulator";
1540#line 126
1541 __cil_tmp24 = (unsigned long )(& descriptor) + 8;
1542#line 126
1543 *((char const **)__cil_tmp24) = "regulator_led_set_value";
1544#line 126
1545 __cil_tmp25 = (unsigned long )(& descriptor) + 16;
1546#line 126
1547 *((char const **)__cil_tmp25) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p";
1548#line 126
1549 __cil_tmp26 = (unsigned long )(& descriptor) + 24;
1550#line 126
1551 *((char const **)__cil_tmp26) = "brightness: %d voltage: %d\n";
1552#line 126
1553 __cil_tmp27 = (unsigned long )(& descriptor) + 32;
1554#line 126
1555 *((unsigned int *)__cil_tmp27) = 127U;
1556#line 126
1557 __cil_tmp28 = (unsigned long )(& descriptor) + 35;
1558#line 126
1559 *((unsigned char *)__cil_tmp28) = (unsigned char)0;
1560#line 126
1561 __cil_tmp29 = (unsigned long )(& descriptor) + 35;
1562#line 126
1563 __cil_tmp30 = *((unsigned char *)__cil_tmp29);
1564#line 126
1565 __cil_tmp31 = (long )__cil_tmp30;
1566#line 126
1567 __cil_tmp32 = __cil_tmp31 & 1L;
1568#line 126
1569 tmp = __builtin_expect(__cil_tmp32, 0L);
1570 }
1571#line 126
1572 if (tmp != 0L) {
1573 {
1574#line 126
1575 __cil_tmp33 = 0 + 48;
1576#line 126
1577 __cil_tmp34 = (unsigned long )led;
1578#line 126
1579 __cil_tmp35 = __cil_tmp34 + __cil_tmp33;
1580#line 126
1581 __cil_tmp36 = *((struct device **)__cil_tmp35);
1582#line 126
1583 __cil_tmp37 = (struct device const *)__cil_tmp36;
1584#line 126
1585 __cil_tmp38 = (unsigned long )led;
1586#line 126
1587 __cil_tmp39 = __cil_tmp38 + 408;
1588#line 126
1589 __cil_tmp40 = *((enum led_brightness *)__cil_tmp39);
1590#line 126
1591 __cil_tmp41 = (unsigned int )__cil_tmp40;
1592#line 126
1593 __dynamic_dev_dbg(& descriptor, __cil_tmp37, "brightness: %d voltage: %d\n",
1594 __cil_tmp41, voltage);
1595 }
1596 } else {
1597
1598 }
1599 {
1600#line 129
1601 __cil_tmp42 = (unsigned long )led;
1602#line 129
1603 __cil_tmp43 = __cil_tmp42 + 664;
1604#line 129
1605 __cil_tmp44 = *((struct regulator **)__cil_tmp43);
1606#line 129
1607 ret = regulator_set_voltage(__cil_tmp44, voltage, voltage);
1608 }
1609#line 130
1610 if (ret != 0) {
1611 {
1612#line 131
1613 __cil_tmp45 = 0 + 48;
1614#line 131
1615 __cil_tmp46 = (unsigned long )led;
1616#line 131
1617 __cil_tmp47 = __cil_tmp46 + __cil_tmp45;
1618#line 131
1619 __cil_tmp48 = *((struct device **)__cil_tmp47);
1620#line 131
1621 __cil_tmp49 = (struct device const *)__cil_tmp48;
1622#line 131
1623 dev_err(__cil_tmp49, "Failed to set voltage %d: %d\n", voltage, ret);
1624 }
1625 } else {
1626
1627 }
1628 } else {
1629
1630 }
1631 }
1632 {
1633#line 135
1634 regulator_led_enable(led);
1635 }
1636 out:
1637 {
1638#line 138
1639 __cil_tmp50 = (unsigned long )led;
1640#line 138
1641 __cil_tmp51 = __cil_tmp50 + 416;
1642#line 138
1643 __cil_tmp52 = (struct mutex *)__cil_tmp51;
1644#line 138
1645 mutex_unlock(__cil_tmp52);
1646 }
1647#line 139
1648 return;
1649}
1650}
1651#line 141 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
1652static void led_work(struct work_struct *work )
1653{ struct regulator_led *led ;
1654 struct work_struct const *__mptr ;
1655 struct regulator_led *__cil_tmp4 ;
1656
1657 {
1658 {
1659#line 145
1660 __mptr = (struct work_struct const *)work;
1661#line 145
1662 __cil_tmp4 = (struct regulator_led *)__mptr;
1663#line 145
1664 led = __cil_tmp4 + 0xfffffffffffffdb8UL;
1665#line 146
1666 regulator_led_set_value(led);
1667 }
1668#line 147
1669 return;
1670}
1671}
1672#line 149 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
1673static void regulator_led_brightness_set(struct led_classdev *led_cdev , enum led_brightness value )
1674{ struct regulator_led *led ;
1675 struct led_classdev const *__mptr ;
1676 unsigned long __cil_tmp5 ;
1677 unsigned long __cil_tmp6 ;
1678 unsigned long __cil_tmp7 ;
1679 unsigned long __cil_tmp8 ;
1680 struct work_struct *__cil_tmp9 ;
1681
1682 {
1683 {
1684#line 152
1685 __mptr = (struct led_classdev const *)led_cdev;
1686#line 152
1687 led = (struct regulator_led *)__mptr;
1688#line 154
1689 __cil_tmp5 = (unsigned long )led;
1690#line 154
1691 __cil_tmp6 = __cil_tmp5 + 408;
1692#line 154
1693 *((enum led_brightness *)__cil_tmp6) = value;
1694#line 155
1695 __cil_tmp7 = (unsigned long )led;
1696#line 155
1697 __cil_tmp8 = __cil_tmp7 + 584;
1698#line 155
1699 __cil_tmp9 = (struct work_struct *)__cil_tmp8;
1700#line 155
1701 schedule_work(__cil_tmp9);
1702 }
1703#line 156
1704 return;
1705}
1706}
1707#line 158 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
1708static int regulator_led_probe(struct platform_device *pdev )
1709{ struct led_regulator_platform_data *pdata ;
1710 struct regulator_led *led ;
1711 struct regulator *vcc ;
1712 int ret ;
1713 long tmp ;
1714 long tmp___0 ;
1715 void *tmp___1 ;
1716 int tmp___2 ;
1717 struct lock_class_key __key ;
1718 struct lock_class_key __key___0 ;
1719 atomic_long_t __constr_expr_0 ;
1720 unsigned long __cil_tmp13 ;
1721 unsigned long __cil_tmp14 ;
1722 unsigned long __cil_tmp15 ;
1723 void *__cil_tmp16 ;
1724 struct led_regulator_platform_data *__cil_tmp17 ;
1725 unsigned long __cil_tmp18 ;
1726 unsigned long __cil_tmp19 ;
1727 unsigned long __cil_tmp20 ;
1728 unsigned long __cil_tmp21 ;
1729 struct device *__cil_tmp22 ;
1730 struct device const *__cil_tmp23 ;
1731 unsigned long __cil_tmp24 ;
1732 unsigned long __cil_tmp25 ;
1733 struct device *__cil_tmp26 ;
1734 void const *__cil_tmp27 ;
1735 unsigned long __cil_tmp28 ;
1736 unsigned long __cil_tmp29 ;
1737 struct device *__cil_tmp30 ;
1738 struct device const *__cil_tmp31 ;
1739 char *__cil_tmp32 ;
1740 void const *__cil_tmp33 ;
1741 struct regulator_led *__cil_tmp34 ;
1742 unsigned long __cil_tmp35 ;
1743 unsigned long __cil_tmp36 ;
1744 unsigned long __cil_tmp37 ;
1745 unsigned long __cil_tmp38 ;
1746 unsigned long __cil_tmp39 ;
1747 unsigned long __cil_tmp40 ;
1748 unsigned long __cil_tmp41 ;
1749 unsigned long __cil_tmp42 ;
1750 int __cil_tmp43 ;
1751 unsigned int __cil_tmp44 ;
1752 unsigned long __cil_tmp45 ;
1753 unsigned long __cil_tmp46 ;
1754 enum led_brightness __cil_tmp47 ;
1755 unsigned int __cil_tmp48 ;
1756 unsigned long __cil_tmp49 ;
1757 unsigned long __cil_tmp50 ;
1758 struct device *__cil_tmp51 ;
1759 struct device const *__cil_tmp52 ;
1760 unsigned long __cil_tmp53 ;
1761 unsigned long __cil_tmp54 ;
1762 enum led_brightness __cil_tmp55 ;
1763 unsigned int __cil_tmp56 ;
1764 unsigned long __cil_tmp57 ;
1765 unsigned long __cil_tmp58 ;
1766 unsigned long __cil_tmp59 ;
1767 unsigned long __cil_tmp60 ;
1768 unsigned long __cil_tmp61 ;
1769 unsigned long __cil_tmp62 ;
1770 unsigned long __cil_tmp63 ;
1771 char *__cil_tmp64 ;
1772 unsigned long __cil_tmp65 ;
1773 unsigned long __cil_tmp66 ;
1774 unsigned long __cil_tmp67 ;
1775 unsigned long __cil_tmp68 ;
1776 unsigned long __cil_tmp69 ;
1777 unsigned long __cil_tmp70 ;
1778 int __cil_tmp71 ;
1779 unsigned long __cil_tmp72 ;
1780 unsigned long __cil_tmp73 ;
1781 unsigned long __cil_tmp74 ;
1782 unsigned long __cil_tmp75 ;
1783 struct regulator *__cil_tmp76 ;
1784 unsigned long __cil_tmp77 ;
1785 unsigned long __cil_tmp78 ;
1786 unsigned long __cil_tmp79 ;
1787 unsigned long __cil_tmp80 ;
1788 struct mutex *__cil_tmp81 ;
1789 unsigned long __cil_tmp82 ;
1790 unsigned long __cil_tmp83 ;
1791 struct work_struct *__cil_tmp84 ;
1792 unsigned long __cil_tmp85 ;
1793 unsigned long __cil_tmp86 ;
1794 unsigned long __cil_tmp87 ;
1795 unsigned long __cil_tmp88 ;
1796 unsigned long __cil_tmp89 ;
1797 struct lockdep_map *__cil_tmp90 ;
1798 unsigned long __cil_tmp91 ;
1799 unsigned long __cil_tmp92 ;
1800 unsigned long __cil_tmp93 ;
1801 struct list_head *__cil_tmp94 ;
1802 unsigned long __cil_tmp95 ;
1803 unsigned long __cil_tmp96 ;
1804 unsigned long __cil_tmp97 ;
1805 void *__cil_tmp98 ;
1806 unsigned long __cil_tmp99 ;
1807 unsigned long __cil_tmp100 ;
1808 struct device *__cil_tmp101 ;
1809 struct led_classdev *__cil_tmp102 ;
1810 unsigned long __cil_tmp103 ;
1811 unsigned long __cil_tmp104 ;
1812 struct work_struct *__cil_tmp105 ;
1813 unsigned long __cil_tmp106 ;
1814 unsigned long __cil_tmp107 ;
1815 unsigned long __cil_tmp108 ;
1816 unsigned long __cil_tmp109 ;
1817 unsigned long __cil_tmp110 ;
1818 enum led_brightness __cil_tmp111 ;
1819 void const *__cil_tmp112 ;
1820 long __constr_expr_0_counter113 ;
1821
1822 {
1823#line 160
1824 __cil_tmp13 = 16 + 280;
1825#line 160
1826 __cil_tmp14 = (unsigned long )pdev;
1827#line 160
1828 __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
1829#line 160
1830 __cil_tmp16 = *((void **)__cil_tmp15);
1831#line 160
1832 pdata = (struct led_regulator_platform_data *)__cil_tmp16;
1833#line 163
1834 ret = 0;
1835 {
1836#line 165
1837 __cil_tmp17 = (struct led_regulator_platform_data *)0;
1838#line 165
1839 __cil_tmp18 = (unsigned long )__cil_tmp17;
1840#line 165
1841 __cil_tmp19 = (unsigned long )pdata;
1842#line 165
1843 if (__cil_tmp19 == __cil_tmp18) {
1844 {
1845#line 166
1846 __cil_tmp20 = (unsigned long )pdev;
1847#line 166
1848 __cil_tmp21 = __cil_tmp20 + 16;
1849#line 166
1850 __cil_tmp22 = (struct device *)__cil_tmp21;
1851#line 166
1852 __cil_tmp23 = (struct device const *)__cil_tmp22;
1853#line 166
1854 dev_err(__cil_tmp23, "no platform data\n");
1855 }
1856#line 167
1857 return (-19);
1858 } else {
1859
1860 }
1861 }
1862 {
1863#line 170
1864 __cil_tmp24 = (unsigned long )pdev;
1865#line 170
1866 __cil_tmp25 = __cil_tmp24 + 16;
1867#line 170
1868 __cil_tmp26 = (struct device *)__cil_tmp25;
1869#line 170
1870 vcc = regulator_get_exclusive(__cil_tmp26, "vled");
1871#line 171
1872 __cil_tmp27 = (void const *)vcc;
1873#line 171
1874 tmp___0 = IS_ERR(__cil_tmp27);
1875 }
1876#line 171
1877 if (tmp___0 != 0L) {
1878 {
1879#line 172
1880 __cil_tmp28 = (unsigned long )pdev;
1881#line 172
1882 __cil_tmp29 = __cil_tmp28 + 16;
1883#line 172
1884 __cil_tmp30 = (struct device *)__cil_tmp29;
1885#line 172
1886 __cil_tmp31 = (struct device const *)__cil_tmp30;
1887#line 172
1888 __cil_tmp32 = *((char **)pdata);
1889#line 172
1890 dev_err(__cil_tmp31, "Cannot get vcc for %s\n", __cil_tmp32);
1891#line 173
1892 __cil_tmp33 = (void const *)vcc;
1893#line 173
1894 tmp = PTR_ERR(__cil_tmp33);
1895 }
1896#line 173
1897 return ((int )tmp);
1898 } else {
1899
1900 }
1901 {
1902#line 176
1903 tmp___1 = kzalloc(672UL, 208U);
1904#line 176
1905 led = (struct regulator_led *)tmp___1;
1906 }
1907 {
1908#line 177
1909 __cil_tmp34 = (struct regulator_led *)0;
1910#line 177
1911 __cil_tmp35 = (unsigned long )__cil_tmp34;
1912#line 177
1913 __cil_tmp36 = (unsigned long )led;
1914#line 177
1915 if (__cil_tmp36 == __cil_tmp35) {
1916#line 178
1917 ret = -12;
1918#line 179
1919 goto err_vcc;
1920 } else {
1921
1922 }
1923 }
1924 {
1925#line 182
1926 __cil_tmp37 = 0 + 12;
1927#line 182
1928 __cil_tmp38 = (unsigned long )led;
1929#line 182
1930 __cil_tmp39 = __cil_tmp38 + __cil_tmp37;
1931#line 182
1932 *((int *)__cil_tmp39) = led_regulator_get_max_brightness(vcc);
1933 }
1934 {
1935#line 183
1936 __cil_tmp40 = 0 + 12;
1937#line 183
1938 __cil_tmp41 = (unsigned long )led;
1939#line 183
1940 __cil_tmp42 = __cil_tmp41 + __cil_tmp40;
1941#line 183
1942 __cil_tmp43 = *((int *)__cil_tmp42);
1943#line 183
1944 __cil_tmp44 = (unsigned int )__cil_tmp43;
1945#line 183
1946 __cil_tmp45 = (unsigned long )pdata;
1947#line 183
1948 __cil_tmp46 = __cil_tmp45 + 8;
1949#line 183
1950 __cil_tmp47 = *((enum led_brightness *)__cil_tmp46);
1951#line 183
1952 __cil_tmp48 = (unsigned int )__cil_tmp47;
1953#line 183
1954 if (__cil_tmp48 > __cil_tmp44) {
1955 {
1956#line 184
1957 __cil_tmp49 = (unsigned long )pdev;
1958#line 184
1959 __cil_tmp50 = __cil_tmp49 + 16;
1960#line 184
1961 __cil_tmp51 = (struct device *)__cil_tmp50;
1962#line 184
1963 __cil_tmp52 = (struct device const *)__cil_tmp51;
1964#line 184
1965 __cil_tmp53 = (unsigned long )pdata;
1966#line 184
1967 __cil_tmp54 = __cil_tmp53 + 8;
1968#line 184
1969 __cil_tmp55 = *((enum led_brightness *)__cil_tmp54);
1970#line 184
1971 __cil_tmp56 = (unsigned int )__cil_tmp55;
1972#line 184
1973 dev_err(__cil_tmp52, "Invalid default brightness %d\n", __cil_tmp56);
1974#line 186
1975 ret = -22;
1976 }
1977#line 187
1978 goto err_led;
1979 } else {
1980
1981 }
1982 }
1983 {
1984#line 189
1985 __cil_tmp57 = (unsigned long )led;
1986#line 189
1987 __cil_tmp58 = __cil_tmp57 + 408;
1988#line 189
1989 __cil_tmp59 = (unsigned long )pdata;
1990#line 189
1991 __cil_tmp60 = __cil_tmp59 + 8;
1992#line 189
1993 *((enum led_brightness *)__cil_tmp58) = *((enum led_brightness *)__cil_tmp60);
1994#line 191
1995 __cil_tmp61 = 0 + 24;
1996#line 191
1997 __cil_tmp62 = (unsigned long )led;
1998#line 191
1999 __cil_tmp63 = __cil_tmp62 + __cil_tmp61;
2000#line 191
2001 *((void (**)(struct led_classdev * , enum led_brightness ))__cil_tmp63) = & regulator_led_brightness_set;
2002#line 192
2003 __cil_tmp64 = *((char **)pdata);
2004#line 192
2005 *((char const **)led) = (char const *)__cil_tmp64;
2006#line 193
2007 __cil_tmp65 = 0 + 16;
2008#line 193
2009 __cil_tmp66 = (unsigned long )led;
2010#line 193
2011 __cil_tmp67 = __cil_tmp66 + __cil_tmp65;
2012#line 193
2013 __cil_tmp68 = 0 + 16;
2014#line 193
2015 __cil_tmp69 = (unsigned long )led;
2016#line 193
2017 __cil_tmp70 = __cil_tmp69 + __cil_tmp68;
2018#line 193
2019 __cil_tmp71 = *((int *)__cil_tmp70);
2020#line 193
2021 *((int *)__cil_tmp67) = __cil_tmp71 | 65536;
2022#line 194
2023 __cil_tmp72 = (unsigned long )led;
2024#line 194
2025 __cil_tmp73 = __cil_tmp72 + 664;
2026#line 194
2027 *((struct regulator **)__cil_tmp73) = vcc;
2028#line 197
2029 __cil_tmp74 = (unsigned long )led;
2030#line 197
2031 __cil_tmp75 = __cil_tmp74 + 664;
2032#line 197
2033 __cil_tmp76 = *((struct regulator **)__cil_tmp75);
2034#line 197
2035 tmp___2 = regulator_is_enabled(__cil_tmp76);
2036 }
2037#line 197
2038 if (tmp___2 != 0) {
2039#line 198
2040 __cil_tmp77 = (unsigned long )led;
2041#line 198
2042 __cil_tmp78 = __cil_tmp77 + 412;
2043#line 198
2044 *((int *)__cil_tmp78) = 1;
2045 } else {
2046
2047 }
2048 {
2049#line 200
2050 __cil_tmp79 = (unsigned long )led;
2051#line 200
2052 __cil_tmp80 = __cil_tmp79 + 416;
2053#line 200
2054 __cil_tmp81 = (struct mutex *)__cil_tmp80;
2055#line 200
2056 __mutex_init(__cil_tmp81, "&led->mutex", & __key);
2057#line 201
2058 __cil_tmp82 = (unsigned long )led;
2059#line 201
2060 __cil_tmp83 = __cil_tmp82 + 584;
2061#line 201
2062 __cil_tmp84 = (struct work_struct *)__cil_tmp83;
2063#line 201
2064 __init_work(__cil_tmp84, 0);
2065#line 201
2066 __constr_expr_0_counter113 = 2097664L;
2067#line 201
2068 __cil_tmp85 = (unsigned long )led;
2069#line 201
2070 __cil_tmp86 = __cil_tmp85 + 584;
2071#line 201
2072 ((atomic_long_t *)__cil_tmp86)->counter = __constr_expr_0_counter113;
2073#line 201
2074 __cil_tmp87 = 584 + 32;
2075#line 201
2076 __cil_tmp88 = (unsigned long )led;
2077#line 201
2078 __cil_tmp89 = __cil_tmp88 + __cil_tmp87;
2079#line 201
2080 __cil_tmp90 = (struct lockdep_map *)__cil_tmp89;
2081#line 201
2082 lockdep_init_map(__cil_tmp90, "(&led->work)", & __key___0, 0);
2083#line 201
2084 __cil_tmp91 = 584 + 8;
2085#line 201
2086 __cil_tmp92 = (unsigned long )led;
2087#line 201
2088 __cil_tmp93 = __cil_tmp92 + __cil_tmp91;
2089#line 201
2090 __cil_tmp94 = (struct list_head *)__cil_tmp93;
2091#line 201
2092 INIT_LIST_HEAD(__cil_tmp94);
2093#line 201
2094 __cil_tmp95 = 584 + 24;
2095#line 201
2096 __cil_tmp96 = (unsigned long )led;
2097#line 201
2098 __cil_tmp97 = __cil_tmp96 + __cil_tmp95;
2099#line 201
2100 *((void (**)(struct work_struct * ))__cil_tmp97) = & led_work;
2101#line 203
2102 __cil_tmp98 = (void *)led;
2103#line 203
2104 platform_set_drvdata(pdev, __cil_tmp98);
2105#line 205
2106 __cil_tmp99 = (unsigned long )pdev;
2107#line 205
2108 __cil_tmp100 = __cil_tmp99 + 16;
2109#line 205
2110 __cil_tmp101 = (struct device *)__cil_tmp100;
2111#line 205
2112 __cil_tmp102 = (struct led_classdev *)led;
2113#line 205
2114 ret = led_classdev_register(__cil_tmp101, __cil_tmp102);
2115 }
2116#line 206
2117 if (ret < 0) {
2118 {
2119#line 207
2120 __cil_tmp103 = (unsigned long )led;
2121#line 207
2122 __cil_tmp104 = __cil_tmp103 + 584;
2123#line 207
2124 __cil_tmp105 = (struct work_struct *)__cil_tmp104;
2125#line 207
2126 cancel_work_sync(__cil_tmp105);
2127 }
2128#line 208
2129 goto err_led;
2130 } else {
2131
2132 }
2133 {
2134#line 212
2135 __cil_tmp106 = 0 + 8;
2136#line 212
2137 __cil_tmp107 = (unsigned long )led;
2138#line 212
2139 __cil_tmp108 = __cil_tmp107 + __cil_tmp106;
2140#line 212
2141 __cil_tmp109 = (unsigned long )led;
2142#line 212
2143 __cil_tmp110 = __cil_tmp109 + 408;
2144#line 212
2145 __cil_tmp111 = *((enum led_brightness *)__cil_tmp110);
2146#line 212
2147 *((int *)__cil_tmp108) = (int )__cil_tmp111;
2148#line 215
2149 regulator_led_set_value(led);
2150 }
2151#line 217
2152 return (0);
2153 err_led:
2154 {
2155#line 220
2156 __cil_tmp112 = (void const *)led;
2157#line 220
2158 kfree(__cil_tmp112);
2159 }
2160 err_vcc:
2161 {
2162#line 222
2163 regulator_put(vcc);
2164 }
2165#line 223
2166 return (ret);
2167}
2168}
2169#line 270
2170extern void ldv_check_final_state(void) ;
2171#line 273
2172extern void ldv_check_return_value(int ) ;
2173#line 276
2174extern void ldv_initialize(void) ;
2175#line 279
2176extern int __VERIFIER_nondet_int(void) ;
2177#line 282 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
2178int LDV_IN_INTERRUPT ;
2179#line 285 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
2180void main(void)
2181{ struct platform_device *var_group1 ;
2182 int res_regulator_led_probe_7 ;
2183 int ldv_s_regulator_led_driver_platform_driver ;
2184 int tmp ;
2185 int tmp___0 ;
2186
2187 {
2188 {
2189#line 318
2190 ldv_s_regulator_led_driver_platform_driver = 0;
2191#line 308
2192 LDV_IN_INTERRUPT = 1;
2193#line 317
2194 ldv_initialize();
2195 }
2196#line 321
2197 goto ldv_15564;
2198 ldv_15563:
2199 {
2200#line 325
2201 tmp = __VERIFIER_nondet_int();
2202 }
2203#line 327
2204 if (tmp == 0) {
2205#line 327
2206 goto case_0;
2207 } else {
2208 {
2209#line 349
2210 goto switch_default;
2211#line 325
2212 if (0) {
2213 case_0: ;
2214#line 330
2215 if (ldv_s_regulator_led_driver_platform_driver == 0) {
2216 {
2217#line 338
2218 res_regulator_led_probe_7 = regulator_led_probe(var_group1);
2219#line 339
2220 ldv_check_return_value(res_regulator_led_probe_7);
2221 }
2222#line 340
2223 if (res_regulator_led_probe_7 != 0) {
2224#line 341
2225 goto ldv_module_exit;
2226 } else {
2227
2228 }
2229#line 342
2230 ldv_s_regulator_led_driver_platform_driver = 0;
2231 } else {
2232
2233 }
2234#line 348
2235 goto ldv_15561;
2236 switch_default: ;
2237#line 349
2238 goto ldv_15561;
2239 } else {
2240 switch_break: ;
2241 }
2242 }
2243 }
2244 ldv_15561: ;
2245 ldv_15564:
2246 {
2247#line 321
2248 tmp___0 = __VERIFIER_nondet_int();
2249 }
2250#line 321
2251 if (tmp___0 != 0) {
2252#line 323
2253 goto ldv_15563;
2254 } else
2255#line 321
2256 if (ldv_s_regulator_led_driver_platform_driver != 0) {
2257#line 323
2258 goto ldv_15563;
2259 } else {
2260#line 325
2261 goto ldv_15565;
2262 }
2263 ldv_15565: ;
2264 ldv_module_exit: ;
2265 {
2266#line 358
2267 ldv_check_final_state();
2268 }
2269#line 361
2270 return;
2271}
2272}
2273#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2274void ldv_blast_assert(void)
2275{
2276
2277 {
2278 ERROR: ;
2279#line 6
2280 goto ERROR;
2281}
2282}
2283#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2284extern int __VERIFIER_nondet_int(void) ;
2285#line 382 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
2286int ldv_spin = 0;
2287#line 386 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
2288void ldv_check_alloc_flags(gfp_t flags )
2289{
2290
2291 {
2292#line 389
2293 if (ldv_spin != 0) {
2294#line 389
2295 if (flags != 32U) {
2296 {
2297#line 389
2298 ldv_blast_assert();
2299 }
2300 } else {
2301
2302 }
2303 } else {
2304
2305 }
2306#line 392
2307 return;
2308}
2309}
2310#line 392
2311extern struct page *ldv_some_page(void) ;
2312#line 395 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
2313struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
2314{ struct page *tmp ;
2315
2316 {
2317#line 398
2318 if (ldv_spin != 0) {
2319#line 398
2320 if (flags != 32U) {
2321 {
2322#line 398
2323 ldv_blast_assert();
2324 }
2325 } else {
2326
2327 }
2328 } else {
2329
2330 }
2331 {
2332#line 400
2333 tmp = ldv_some_page();
2334 }
2335#line 400
2336 return (tmp);
2337}
2338}
2339#line 404 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
2340void ldv_check_alloc_nonatomic(void)
2341{
2342
2343 {
2344#line 407
2345 if (ldv_spin != 0) {
2346 {
2347#line 407
2348 ldv_blast_assert();
2349 }
2350 } else {
2351
2352 }
2353#line 410
2354 return;
2355}
2356}
2357#line 411 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
2358void ldv_spin_lock(void)
2359{
2360
2361 {
2362#line 414
2363 ldv_spin = 1;
2364#line 415
2365 return;
2366}
2367}
2368#line 418 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
2369void ldv_spin_unlock(void)
2370{
2371
2372 {
2373#line 421
2374 ldv_spin = 0;
2375#line 422
2376 return;
2377}
2378}
2379#line 425 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
2380int ldv_spin_trylock(void)
2381{ int is_lock ;
2382
2383 {
2384 {
2385#line 430
2386 is_lock = __VERIFIER_nondet_int();
2387 }
2388#line 432
2389 if (is_lock != 0) {
2390#line 435
2391 return (0);
2392 } else {
2393#line 440
2394 ldv_spin = 1;
2395#line 442
2396 return (1);
2397 }
2398}
2399}
2400#line 609 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
2401void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
2402{
2403
2404 {
2405 {
2406#line 615
2407 ldv_check_alloc_flags(ldv_func_arg2);
2408#line 617
2409 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2410 }
2411#line 618
2412 return ((void *)0);
2413}
2414}
2415#line 620 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12454/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-regulator.c.p"
2416__inline static void *kzalloc(size_t size , gfp_t flags )
2417{ void *tmp ;
2418
2419 {
2420 {
2421#line 626
2422 ldv_check_alloc_flags(flags);
2423#line 627
2424 tmp = __VERIFIER_nondet_pointer();
2425 }
2426#line 627
2427 return (tmp);
2428}
2429}