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 45 "include/asm-generic/int-ll64.h"
11typedef short s16;
12#line 46 "include/asm-generic/int-ll64.h"
13typedef unsigned short u16;
14#line 48 "include/asm-generic/int-ll64.h"
15typedef int s32;
16#line 49 "include/asm-generic/int-ll64.h"
17typedef unsigned int u32;
18#line 51 "include/asm-generic/int-ll64.h"
19typedef long long s64;
20#line 52 "include/asm-generic/int-ll64.h"
21typedef unsigned long long u64;
22#line 14 "include/asm-generic/posix_types.h"
23typedef long __kernel_long_t;
24#line 15 "include/asm-generic/posix_types.h"
25typedef unsigned long __kernel_ulong_t;
26#line 75 "include/asm-generic/posix_types.h"
27typedef __kernel_ulong_t __kernel_size_t;
28#line 76 "include/asm-generic/posix_types.h"
29typedef __kernel_long_t __kernel_ssize_t;
30#line 91 "include/asm-generic/posix_types.h"
31typedef long long __kernel_loff_t;
32#line 21 "include/linux/types.h"
33typedef __u32 __kernel_dev_t;
34#line 24 "include/linux/types.h"
35typedef __kernel_dev_t dev_t;
36#line 27 "include/linux/types.h"
37typedef unsigned short umode_t;
38#line 38 "include/linux/types.h"
39typedef _Bool bool;
40#line 54 "include/linux/types.h"
41typedef __kernel_loff_t loff_t;
42#line 63 "include/linux/types.h"
43typedef __kernel_size_t size_t;
44#line 68 "include/linux/types.h"
45typedef __kernel_ssize_t ssize_t;
46#line 202 "include/linux/types.h"
47typedef unsigned int gfp_t;
48#line 206 "include/linux/types.h"
49typedef u64 phys_addr_t;
50#line 211 "include/linux/types.h"
51typedef phys_addr_t resource_size_t;
52#line 219 "include/linux/types.h"
53struct __anonstruct_atomic_t_7 {
54 int counter ;
55};
56#line 219 "include/linux/types.h"
57typedef struct __anonstruct_atomic_t_7 atomic_t;
58#line 224 "include/linux/types.h"
59struct __anonstruct_atomic64_t_8 {
60 long counter ;
61};
62#line 224 "include/linux/types.h"
63typedef struct __anonstruct_atomic64_t_8 atomic64_t;
64#line 229 "include/linux/types.h"
65struct list_head {
66 struct list_head *next ;
67 struct list_head *prev ;
68};
69#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
70struct module;
71#line 56
72struct module;
73#line 146 "include/linux/init.h"
74typedef void (*ctor_fn_t)(void);
75#line 9 "include/linux/dynamic_debug.h"
76struct _ddebug {
77 char const *modname ;
78 char const *function ;
79 char const *filename ;
80 char const *format ;
81 unsigned int lineno : 18 ;
82 unsigned int flags : 8 ;
83} __attribute__((__aligned__(8))) ;
84#line 47
85struct device;
86#line 47
87struct device;
88#line 135 "include/linux/kernel.h"
89struct completion;
90#line 135
91struct completion;
92#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
93struct page;
94#line 18
95struct page;
96#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
97struct task_struct;
98#line 20
99struct task_struct;
100#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
101struct task_struct;
102#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
103struct file;
104#line 295
105struct file;
106#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
107struct page;
108#line 52
109struct task_struct;
110#line 329
111struct arch_spinlock;
112#line 329
113struct arch_spinlock;
114#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
115struct task_struct;
116#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
117struct task_struct;
118#line 10 "include/asm-generic/bug.h"
119struct bug_entry {
120 int bug_addr_disp ;
121 int file_disp ;
122 unsigned short line ;
123 unsigned short flags ;
124};
125#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
126struct static_key;
127#line 234
128struct static_key;
129#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
130struct kmem_cache;
131#line 23 "include/asm-generic/atomic-long.h"
132typedef atomic64_t atomic_long_t;
133#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
134typedef u16 __ticket_t;
135#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
136typedef u32 __ticketpair_t;
137#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
138struct __raw_tickets {
139 __ticket_t head ;
140 __ticket_t tail ;
141};
142#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
143union __anonunion____missing_field_name_36 {
144 __ticketpair_t head_tail ;
145 struct __raw_tickets tickets ;
146};
147#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
148struct arch_spinlock {
149 union __anonunion____missing_field_name_36 __annonCompField17 ;
150};
151#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
152typedef struct arch_spinlock arch_spinlock_t;
153#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
154struct __anonstruct____missing_field_name_38 {
155 u32 read ;
156 s32 write ;
157};
158#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
159union __anonunion_arch_rwlock_t_37 {
160 s64 lock ;
161 struct __anonstruct____missing_field_name_38 __annonCompField18 ;
162};
163#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
164typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_t;
165#line 12 "include/linux/lockdep.h"
166struct task_struct;
167#line 391 "include/linux/lockdep.h"
168struct lock_class_key {
169
170};
171#line 20 "include/linux/spinlock_types.h"
172struct raw_spinlock {
173 arch_spinlock_t raw_lock ;
174 unsigned int magic ;
175 unsigned int owner_cpu ;
176 void *owner ;
177};
178#line 20 "include/linux/spinlock_types.h"
179typedef struct raw_spinlock raw_spinlock_t;
180#line 64 "include/linux/spinlock_types.h"
181union __anonunion____missing_field_name_39 {
182 struct raw_spinlock rlock ;
183};
184#line 64 "include/linux/spinlock_types.h"
185struct spinlock {
186 union __anonunion____missing_field_name_39 __annonCompField19 ;
187};
188#line 64 "include/linux/spinlock_types.h"
189typedef struct spinlock spinlock_t;
190#line 11 "include/linux/rwlock_types.h"
191struct __anonstruct_rwlock_t_40 {
192 arch_rwlock_t raw_lock ;
193 unsigned int magic ;
194 unsigned int owner_cpu ;
195 void *owner ;
196};
197#line 11 "include/linux/rwlock_types.h"
198typedef struct __anonstruct_rwlock_t_40 rwlock_t;
199#line 49 "include/linux/wait.h"
200struct __wait_queue_head {
201 spinlock_t lock ;
202 struct list_head task_list ;
203};
204#line 53 "include/linux/wait.h"
205typedef struct __wait_queue_head wait_queue_head_t;
206#line 55
207struct task_struct;
208#line 60 "include/linux/pageblock-flags.h"
209struct page;
210#line 48 "include/linux/mutex.h"
211struct mutex {
212 atomic_t count ;
213 spinlock_t wait_lock ;
214 struct list_head wait_list ;
215 struct task_struct *owner ;
216 char const *name ;
217 void *magic ;
218};
219#line 19 "include/linux/rwsem.h"
220struct rw_semaphore;
221#line 19
222struct rw_semaphore;
223#line 25 "include/linux/rwsem.h"
224struct rw_semaphore {
225 long count ;
226 raw_spinlock_t wait_lock ;
227 struct list_head wait_list ;
228};
229#line 25 "include/linux/completion.h"
230struct completion {
231 unsigned int done ;
232 wait_queue_head_t wait ;
233};
234#line 9 "include/linux/memory_hotplug.h"
235struct page;
236#line 18 "include/linux/ioport.h"
237struct resource {
238 resource_size_t start ;
239 resource_size_t end ;
240 char const *name ;
241 unsigned long flags ;
242 struct resource *parent ;
243 struct resource *sibling ;
244 struct resource *child ;
245};
246#line 202
247struct device;
248#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
249struct device;
250#line 46 "include/linux/ktime.h"
251union ktime {
252 s64 tv64 ;
253};
254#line 59 "include/linux/ktime.h"
255typedef union ktime ktime_t;
256#line 10 "include/linux/timer.h"
257struct tvec_base;
258#line 10
259struct tvec_base;
260#line 12 "include/linux/timer.h"
261struct timer_list {
262 struct list_head entry ;
263 unsigned long expires ;
264 struct tvec_base *base ;
265 void (*function)(unsigned long ) ;
266 unsigned long data ;
267 int slack ;
268 int start_pid ;
269 void *start_site ;
270 char start_comm[16] ;
271};
272#line 17 "include/linux/workqueue.h"
273struct work_struct;
274#line 17
275struct work_struct;
276#line 79 "include/linux/workqueue.h"
277struct work_struct {
278 atomic_long_t data ;
279 struct list_head entry ;
280 void (*func)(struct work_struct *work ) ;
281};
282#line 42 "include/linux/pm.h"
283struct device;
284#line 50 "include/linux/pm.h"
285struct pm_message {
286 int event ;
287};
288#line 50 "include/linux/pm.h"
289typedef struct pm_message pm_message_t;
290#line 264 "include/linux/pm.h"
291struct dev_pm_ops {
292 int (*prepare)(struct device *dev ) ;
293 void (*complete)(struct device *dev ) ;
294 int (*suspend)(struct device *dev ) ;
295 int (*resume)(struct device *dev ) ;
296 int (*freeze)(struct device *dev ) ;
297 int (*thaw)(struct device *dev ) ;
298 int (*poweroff)(struct device *dev ) ;
299 int (*restore)(struct device *dev ) ;
300 int (*suspend_late)(struct device *dev ) ;
301 int (*resume_early)(struct device *dev ) ;
302 int (*freeze_late)(struct device *dev ) ;
303 int (*thaw_early)(struct device *dev ) ;
304 int (*poweroff_late)(struct device *dev ) ;
305 int (*restore_early)(struct device *dev ) ;
306 int (*suspend_noirq)(struct device *dev ) ;
307 int (*resume_noirq)(struct device *dev ) ;
308 int (*freeze_noirq)(struct device *dev ) ;
309 int (*thaw_noirq)(struct device *dev ) ;
310 int (*poweroff_noirq)(struct device *dev ) ;
311 int (*restore_noirq)(struct device *dev ) ;
312 int (*runtime_suspend)(struct device *dev ) ;
313 int (*runtime_resume)(struct device *dev ) ;
314 int (*runtime_idle)(struct device *dev ) ;
315};
316#line 458
317enum rpm_status {
318 RPM_ACTIVE = 0,
319 RPM_RESUMING = 1,
320 RPM_SUSPENDED = 2,
321 RPM_SUSPENDING = 3
322} ;
323#line 480
324enum rpm_request {
325 RPM_REQ_NONE = 0,
326 RPM_REQ_IDLE = 1,
327 RPM_REQ_SUSPEND = 2,
328 RPM_REQ_AUTOSUSPEND = 3,
329 RPM_REQ_RESUME = 4
330} ;
331#line 488
332struct wakeup_source;
333#line 488
334struct wakeup_source;
335#line 495 "include/linux/pm.h"
336struct pm_subsys_data {
337 spinlock_t lock ;
338 unsigned int refcount ;
339};
340#line 506
341struct dev_pm_qos_request;
342#line 506
343struct pm_qos_constraints;
344#line 506 "include/linux/pm.h"
345struct dev_pm_info {
346 pm_message_t power_state ;
347 unsigned int can_wakeup : 1 ;
348 unsigned int async_suspend : 1 ;
349 bool is_prepared : 1 ;
350 bool is_suspended : 1 ;
351 bool ignore_children : 1 ;
352 spinlock_t lock ;
353 struct list_head entry ;
354 struct completion completion ;
355 struct wakeup_source *wakeup ;
356 bool wakeup_path : 1 ;
357 struct timer_list suspend_timer ;
358 unsigned long timer_expires ;
359 struct work_struct work ;
360 wait_queue_head_t wait_queue ;
361 atomic_t usage_count ;
362 atomic_t child_count ;
363 unsigned int disable_depth : 3 ;
364 unsigned int idle_notification : 1 ;
365 unsigned int request_pending : 1 ;
366 unsigned int deferred_resume : 1 ;
367 unsigned int run_wake : 1 ;
368 unsigned int runtime_auto : 1 ;
369 unsigned int no_callbacks : 1 ;
370 unsigned int irq_safe : 1 ;
371 unsigned int use_autosuspend : 1 ;
372 unsigned int timer_autosuspends : 1 ;
373 enum rpm_request request ;
374 enum rpm_status runtime_status ;
375 int runtime_error ;
376 int autosuspend_delay ;
377 unsigned long last_busy ;
378 unsigned long active_jiffies ;
379 unsigned long suspended_jiffies ;
380 unsigned long accounting_timestamp ;
381 ktime_t suspend_time ;
382 s64 max_time_suspended_ns ;
383 struct dev_pm_qos_request *pq_req ;
384 struct pm_subsys_data *subsys_data ;
385 struct pm_qos_constraints *constraints ;
386};
387#line 564 "include/linux/pm.h"
388struct dev_pm_domain {
389 struct dev_pm_ops ops ;
390};
391#line 8 "include/linux/vmalloc.h"
392struct vm_area_struct;
393#line 8
394struct vm_area_struct;
395#line 994 "include/linux/mmzone.h"
396struct page;
397#line 10 "include/linux/gfp.h"
398struct vm_area_struct;
399#line 29 "include/linux/sysctl.h"
400struct completion;
401#line 49 "include/linux/kmod.h"
402struct file;
403#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
404struct task_struct;
405#line 18 "include/linux/elf.h"
406typedef __u64 Elf64_Addr;
407#line 19 "include/linux/elf.h"
408typedef __u16 Elf64_Half;
409#line 23 "include/linux/elf.h"
410typedef __u32 Elf64_Word;
411#line 24 "include/linux/elf.h"
412typedef __u64 Elf64_Xword;
413#line 194 "include/linux/elf.h"
414struct elf64_sym {
415 Elf64_Word st_name ;
416 unsigned char st_info ;
417 unsigned char st_other ;
418 Elf64_Half st_shndx ;
419 Elf64_Addr st_value ;
420 Elf64_Xword st_size ;
421};
422#line 194 "include/linux/elf.h"
423typedef struct elf64_sym Elf64_Sym;
424#line 438
425struct file;
426#line 20 "include/linux/kobject_ns.h"
427struct sock;
428#line 20
429struct sock;
430#line 21
431struct kobject;
432#line 21
433struct kobject;
434#line 27
435enum kobj_ns_type {
436 KOBJ_NS_TYPE_NONE = 0,
437 KOBJ_NS_TYPE_NET = 1,
438 KOBJ_NS_TYPES = 2
439} ;
440#line 40 "include/linux/kobject_ns.h"
441struct kobj_ns_type_operations {
442 enum kobj_ns_type type ;
443 void *(*grab_current_ns)(void) ;
444 void const *(*netlink_ns)(struct sock *sk ) ;
445 void const *(*initial_ns)(void) ;
446 void (*drop_ns)(void * ) ;
447};
448#line 22 "include/linux/sysfs.h"
449struct kobject;
450#line 23
451struct module;
452#line 24
453enum kobj_ns_type;
454#line 26 "include/linux/sysfs.h"
455struct attribute {
456 char const *name ;
457 umode_t mode ;
458};
459#line 56 "include/linux/sysfs.h"
460struct attribute_group {
461 char const *name ;
462 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
463 struct attribute **attrs ;
464};
465#line 85
466struct file;
467#line 86
468struct vm_area_struct;
469#line 88 "include/linux/sysfs.h"
470struct bin_attribute {
471 struct attribute attr ;
472 size_t size ;
473 void *private ;
474 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
475 loff_t , size_t ) ;
476 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
477 loff_t , size_t ) ;
478 int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
479};
480#line 112 "include/linux/sysfs.h"
481struct sysfs_ops {
482 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
483 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
484 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
485};
486#line 118
487struct sysfs_dirent;
488#line 118
489struct sysfs_dirent;
490#line 22 "include/linux/kref.h"
491struct kref {
492 atomic_t refcount ;
493};
494#line 60 "include/linux/kobject.h"
495struct kset;
496#line 60
497struct kobj_type;
498#line 60 "include/linux/kobject.h"
499struct kobject {
500 char const *name ;
501 struct list_head entry ;
502 struct kobject *parent ;
503 struct kset *kset ;
504 struct kobj_type *ktype ;
505 struct sysfs_dirent *sd ;
506 struct kref kref ;
507 unsigned int state_initialized : 1 ;
508 unsigned int state_in_sysfs : 1 ;
509 unsigned int state_add_uevent_sent : 1 ;
510 unsigned int state_remove_uevent_sent : 1 ;
511 unsigned int uevent_suppress : 1 ;
512};
513#line 108 "include/linux/kobject.h"
514struct kobj_type {
515 void (*release)(struct kobject *kobj ) ;
516 struct sysfs_ops const *sysfs_ops ;
517 struct attribute **default_attrs ;
518 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
519 void const *(*namespace)(struct kobject *kobj ) ;
520};
521#line 116 "include/linux/kobject.h"
522struct kobj_uevent_env {
523 char *envp[32] ;
524 int envp_idx ;
525 char buf[2048] ;
526 int buflen ;
527};
528#line 123 "include/linux/kobject.h"
529struct kset_uevent_ops {
530 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
531 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
532 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
533};
534#line 140
535struct sock;
536#line 159 "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 39 "include/linux/moduleparam.h"
544struct kernel_param;
545#line 39
546struct kernel_param;
547#line 41 "include/linux/moduleparam.h"
548struct kernel_param_ops {
549 int (*set)(char const *val , struct kernel_param const *kp ) ;
550 int (*get)(char *buffer , struct kernel_param const *kp ) ;
551 void (*free)(void *arg ) ;
552};
553#line 50
554struct kparam_string;
555#line 50
556struct kparam_array;
557#line 50 "include/linux/moduleparam.h"
558union __anonunion____missing_field_name_199 {
559 void *arg ;
560 struct kparam_string const *str ;
561 struct kparam_array const *arr ;
562};
563#line 50 "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____missing_field_name_199 __annonCompField32 ;
570};
571#line 63 "include/linux/moduleparam.h"
572struct kparam_string {
573 unsigned int maxlen ;
574 char *string ;
575};
576#line 69 "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 445
585struct module;
586#line 80 "include/linux/jump_label.h"
587struct module;
588#line 143 "include/linux/jump_label.h"
589struct static_key {
590 atomic_t enabled ;
591};
592#line 22 "include/linux/tracepoint.h"
593struct module;
594#line 23
595struct tracepoint;
596#line 23
597struct tracepoint;
598#line 25 "include/linux/tracepoint.h"
599struct tracepoint_func {
600 void *func ;
601 void *data ;
602};
603#line 30 "include/linux/tracepoint.h"
604struct tracepoint {
605 char const *name ;
606 struct static_key key ;
607 void (*regfunc)(void) ;
608 void (*unregfunc)(void) ;
609 struct tracepoint_func *funcs ;
610};
611#line 19 "include/linux/export.h"
612struct kernel_symbol {
613 unsigned long value ;
614 char const *name ;
615};
616#line 8 "include/asm-generic/module.h"
617struct mod_arch_specific {
618
619};
620#line 35 "include/linux/module.h"
621struct module;
622#line 37
623struct module_param_attrs;
624#line 37 "include/linux/module.h"
625struct module_kobject {
626 struct kobject kobj ;
627 struct module *mod ;
628 struct kobject *drivers_dir ;
629 struct module_param_attrs *mp ;
630};
631#line 44 "include/linux/module.h"
632struct module_attribute {
633 struct attribute attr ;
634 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
635 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
636 size_t count ) ;
637 void (*setup)(struct module * , char const * ) ;
638 int (*test)(struct module * ) ;
639 void (*free)(struct module * ) ;
640};
641#line 71
642struct exception_table_entry;
643#line 71
644struct exception_table_entry;
645#line 199
646enum module_state {
647 MODULE_STATE_LIVE = 0,
648 MODULE_STATE_COMING = 1,
649 MODULE_STATE_GOING = 2
650} ;
651#line 215 "include/linux/module.h"
652struct module_ref {
653 unsigned long incs ;
654 unsigned long decs ;
655} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ;
656#line 220
657struct module_sect_attrs;
658#line 220
659struct module_notes_attrs;
660#line 220
661struct ftrace_event_call;
662#line 220 "include/linux/module.h"
663struct module {
664 enum module_state state ;
665 struct list_head list ;
666 char name[64UL - sizeof(unsigned long )] ;
667 struct module_kobject mkobj ;
668 struct module_attribute *modinfo_attrs ;
669 char const *version ;
670 char const *srcversion ;
671 struct kobject *holders_dir ;
672 struct kernel_symbol const *syms ;
673 unsigned long const *crcs ;
674 unsigned int num_syms ;
675 struct kernel_param *kp ;
676 unsigned int num_kp ;
677 unsigned int num_gpl_syms ;
678 struct kernel_symbol const *gpl_syms ;
679 unsigned long const *gpl_crcs ;
680 struct kernel_symbol const *unused_syms ;
681 unsigned long const *unused_crcs ;
682 unsigned int num_unused_syms ;
683 unsigned int num_unused_gpl_syms ;
684 struct kernel_symbol const *unused_gpl_syms ;
685 unsigned long const *unused_gpl_crcs ;
686 struct kernel_symbol const *gpl_future_syms ;
687 unsigned long const *gpl_future_crcs ;
688 unsigned int num_gpl_future_syms ;
689 unsigned int num_exentries ;
690 struct exception_table_entry *extable ;
691 int (*init)(void) ;
692 void *module_init ;
693 void *module_core ;
694 unsigned int init_size ;
695 unsigned int core_size ;
696 unsigned int init_text_size ;
697 unsigned int core_text_size ;
698 unsigned int init_ro_size ;
699 unsigned int core_ro_size ;
700 struct mod_arch_specific arch ;
701 unsigned int taints ;
702 unsigned int num_bugs ;
703 struct list_head bug_list ;
704 struct bug_entry *bug_table ;
705 Elf64_Sym *symtab ;
706 Elf64_Sym *core_symtab ;
707 unsigned int num_symtab ;
708 unsigned int core_num_syms ;
709 char *strtab ;
710 char *core_strtab ;
711 struct module_sect_attrs *sect_attrs ;
712 struct module_notes_attrs *notes_attrs ;
713 char *args ;
714 void *percpu ;
715 unsigned int percpu_size ;
716 unsigned int num_tracepoints ;
717 struct tracepoint * const *tracepoints_ptrs ;
718 unsigned int num_trace_bprintk_fmt ;
719 char const **trace_bprintk_fmt_start ;
720 struct ftrace_event_call **trace_events ;
721 unsigned int num_trace_events ;
722 struct list_head source_list ;
723 struct list_head target_list ;
724 struct task_struct *waiter ;
725 void (*exit)(void) ;
726 struct module_ref *refptr ;
727 ctor_fn_t *ctors ;
728 unsigned int num_ctors ;
729};
730#line 46 "include/linux/slub_def.h"
731struct kmem_cache_cpu {
732 void **freelist ;
733 unsigned long tid ;
734 struct page *page ;
735 struct page *partial ;
736 int node ;
737 unsigned int stat[26] ;
738};
739#line 57 "include/linux/slub_def.h"
740struct kmem_cache_node {
741 spinlock_t list_lock ;
742 unsigned long nr_partial ;
743 struct list_head partial ;
744 atomic_long_t nr_slabs ;
745 atomic_long_t total_objects ;
746 struct list_head full ;
747};
748#line 73 "include/linux/slub_def.h"
749struct kmem_cache_order_objects {
750 unsigned long x ;
751};
752#line 80 "include/linux/slub_def.h"
753struct kmem_cache {
754 struct kmem_cache_cpu *cpu_slab ;
755 unsigned long flags ;
756 unsigned long min_partial ;
757 int size ;
758 int objsize ;
759 int offset ;
760 int cpu_partial ;
761 struct kmem_cache_order_objects oo ;
762 struct kmem_cache_order_objects max ;
763 struct kmem_cache_order_objects min ;
764 gfp_t allocflags ;
765 int refcount ;
766 void (*ctor)(void * ) ;
767 int inuse ;
768 int align ;
769 int reserved ;
770 char const *name ;
771 struct list_head list ;
772 struct kobject kobj ;
773 int remote_node_defrag_ratio ;
774 struct kmem_cache_node *node[1 << 10] ;
775};
776#line 20 "include/linux/leds.h"
777struct device;
778#line 25
779enum led_brightness {
780 LED_OFF = 0,
781 LED_HALF = 127,
782 LED_FULL = 255
783} ;
784#line 31
785struct led_trigger;
786#line 31 "include/linux/leds.h"
787struct led_classdev {
788 char const *name ;
789 int brightness ;
790 int max_brightness ;
791 int flags ;
792 void (*brightness_set)(struct led_classdev *led_cdev , enum led_brightness brightness ) ;
793 enum led_brightness (*brightness_get)(struct led_classdev *led_cdev ) ;
794 int (*blink_set)(struct led_classdev *led_cdev , unsigned long *delay_on , unsigned long *delay_off ) ;
795 struct device *dev ;
796 struct list_head node ;
797 char const *default_trigger ;
798 unsigned long blink_delay_on ;
799 unsigned long blink_delay_off ;
800 struct timer_list blink_timer ;
801 int blink_brightness ;
802 struct rw_semaphore trigger_lock ;
803 struct led_trigger *trigger ;
804 struct list_head trig_list ;
805 void *trigger_data ;
806};
807#line 122 "include/linux/leds.h"
808struct led_trigger {
809 char const *name ;
810 void (*activate)(struct led_classdev *led_cdev ) ;
811 void (*deactivate)(struct led_classdev *led_cdev ) ;
812 rwlock_t leddev_list_lock ;
813 struct list_head led_cdevs ;
814 struct list_head next_trig ;
815};
816#line 210
817struct platform_device;
818#line 41 "include/linux/leds-regulator.h"
819struct led_regulator_platform_data {
820 char *name ;
821 enum led_brightness brightness ;
822};
823#line 19 "include/linux/klist.h"
824struct klist_node;
825#line 19
826struct klist_node;
827#line 39 "include/linux/klist.h"
828struct klist_node {
829 void *n_klist ;
830 struct list_head n_node ;
831 struct kref n_ref ;
832};
833#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
834struct dma_map_ops;
835#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
836struct dev_archdata {
837 void *acpi_handle ;
838 struct dma_map_ops *dma_ops ;
839 void *iommu ;
840};
841#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
842struct pdev_archdata {
843
844};
845#line 28 "include/linux/device.h"
846struct device;
847#line 29
848struct device_private;
849#line 29
850struct device_private;
851#line 30
852struct device_driver;
853#line 30
854struct device_driver;
855#line 31
856struct driver_private;
857#line 31
858struct driver_private;
859#line 32
860struct module;
861#line 33
862struct class;
863#line 33
864struct class;
865#line 34
866struct subsys_private;
867#line 34
868struct subsys_private;
869#line 35
870struct bus_type;
871#line 35
872struct bus_type;
873#line 36
874struct device_node;
875#line 36
876struct device_node;
877#line 37
878struct iommu_ops;
879#line 37
880struct iommu_ops;
881#line 39 "include/linux/device.h"
882struct bus_attribute {
883 struct attribute attr ;
884 ssize_t (*show)(struct bus_type *bus , char *buf ) ;
885 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ;
886};
887#line 89
888struct device_attribute;
889#line 89
890struct driver_attribute;
891#line 89 "include/linux/device.h"
892struct bus_type {
893 char const *name ;
894 char const *dev_name ;
895 struct device *dev_root ;
896 struct bus_attribute *bus_attrs ;
897 struct device_attribute *dev_attrs ;
898 struct driver_attribute *drv_attrs ;
899 int (*match)(struct device *dev , struct device_driver *drv ) ;
900 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
901 int (*probe)(struct device *dev ) ;
902 int (*remove)(struct device *dev ) ;
903 void (*shutdown)(struct device *dev ) ;
904 int (*suspend)(struct device *dev , pm_message_t state ) ;
905 int (*resume)(struct device *dev ) ;
906 struct dev_pm_ops const *pm ;
907 struct iommu_ops *iommu_ops ;
908 struct subsys_private *p ;
909};
910#line 127
911struct device_type;
912#line 214
913struct of_device_id;
914#line 214 "include/linux/device.h"
915struct device_driver {
916 char const *name ;
917 struct bus_type *bus ;
918 struct module *owner ;
919 char const *mod_name ;
920 bool suppress_bind_attrs ;
921 struct of_device_id const *of_match_table ;
922 int (*probe)(struct device *dev ) ;
923 int (*remove)(struct device *dev ) ;
924 void (*shutdown)(struct device *dev ) ;
925 int (*suspend)(struct device *dev , pm_message_t state ) ;
926 int (*resume)(struct device *dev ) ;
927 struct attribute_group const **groups ;
928 struct dev_pm_ops const *pm ;
929 struct driver_private *p ;
930};
931#line 249 "include/linux/device.h"
932struct driver_attribute {
933 struct attribute attr ;
934 ssize_t (*show)(struct device_driver *driver , char *buf ) ;
935 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ;
936};
937#line 330
938struct class_attribute;
939#line 330 "include/linux/device.h"
940struct class {
941 char const *name ;
942 struct module *owner ;
943 struct class_attribute *class_attrs ;
944 struct device_attribute *dev_attrs ;
945 struct bin_attribute *dev_bin_attrs ;
946 struct kobject *dev_kobj ;
947 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
948 char *(*devnode)(struct device *dev , umode_t *mode ) ;
949 void (*class_release)(struct class *class ) ;
950 void (*dev_release)(struct device *dev ) ;
951 int (*suspend)(struct device *dev , pm_message_t state ) ;
952 int (*resume)(struct device *dev ) ;
953 struct kobj_ns_type_operations const *ns_type ;
954 void const *(*namespace)(struct device *dev ) ;
955 struct dev_pm_ops const *pm ;
956 struct subsys_private *p ;
957};
958#line 397 "include/linux/device.h"
959struct class_attribute {
960 struct attribute attr ;
961 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
962 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf ,
963 size_t count ) ;
964 void const *(*namespace)(struct class *class , struct class_attribute const *attr ) ;
965};
966#line 465 "include/linux/device.h"
967struct device_type {
968 char const *name ;
969 struct attribute_group const **groups ;
970 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
971 char *(*devnode)(struct device *dev , umode_t *mode ) ;
972 void (*release)(struct device *dev ) ;
973 struct dev_pm_ops const *pm ;
974};
975#line 476 "include/linux/device.h"
976struct device_attribute {
977 struct attribute attr ;
978 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
979 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf ,
980 size_t count ) ;
981};
982#line 559 "include/linux/device.h"
983struct device_dma_parameters {
984 unsigned int max_segment_size ;
985 unsigned long segment_boundary_mask ;
986};
987#line 627
988struct dma_coherent_mem;
989#line 627 "include/linux/device.h"
990struct device {
991 struct device *parent ;
992 struct device_private *p ;
993 struct kobject kobj ;
994 char const *init_name ;
995 struct device_type const *type ;
996 struct mutex mutex ;
997 struct bus_type *bus ;
998 struct device_driver *driver ;
999 void *platform_data ;
1000 struct dev_pm_info power ;
1001 struct dev_pm_domain *pm_domain ;
1002 int numa_node ;
1003 u64 *dma_mask ;
1004 u64 coherent_dma_mask ;
1005 struct device_dma_parameters *dma_parms ;
1006 struct list_head dma_pools ;
1007 struct dma_coherent_mem *dma_mem ;
1008 struct dev_archdata archdata ;
1009 struct device_node *of_node ;
1010 dev_t devt ;
1011 u32 id ;
1012 spinlock_t devres_lock ;
1013 struct list_head devres_head ;
1014 struct klist_node knode_class ;
1015 struct class *class ;
1016 struct attribute_group const **groups ;
1017 void (*release)(struct device *dev ) ;
1018};
1019#line 43 "include/linux/pm_wakeup.h"
1020struct wakeup_source {
1021 char const *name ;
1022 struct list_head entry ;
1023 spinlock_t lock ;
1024 struct timer_list timer ;
1025 unsigned long timer_expires ;
1026 ktime_t total_time ;
1027 ktime_t max_time ;
1028 ktime_t last_time ;
1029 unsigned long event_count ;
1030 unsigned long active_count ;
1031 unsigned long relax_count ;
1032 unsigned long hit_count ;
1033 unsigned int active : 1 ;
1034};
1035#line 12 "include/linux/mod_devicetable.h"
1036typedef unsigned long kernel_ulong_t;
1037#line 219 "include/linux/mod_devicetable.h"
1038struct of_device_id {
1039 char name[32] ;
1040 char type[32] ;
1041 char compatible[128] ;
1042 void *data ;
1043};
1044#line 506 "include/linux/mod_devicetable.h"
1045struct platform_device_id {
1046 char name[20] ;
1047 kernel_ulong_t driver_data __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
1048};
1049#line 17 "include/linux/platform_device.h"
1050struct mfd_cell;
1051#line 17
1052struct mfd_cell;
1053#line 19 "include/linux/platform_device.h"
1054struct platform_device {
1055 char const *name ;
1056 int id ;
1057 struct device dev ;
1058 u32 num_resources ;
1059 struct resource *resource ;
1060 struct platform_device_id const *id_entry ;
1061 struct mfd_cell *mfd_cell ;
1062 struct pdev_archdata archdata ;
1063};
1064#line 164 "include/linux/platform_device.h"
1065struct platform_driver {
1066 int (*probe)(struct platform_device * ) ;
1067 int (*remove)(struct platform_device * ) ;
1068 void (*shutdown)(struct platform_device * ) ;
1069 int (*suspend)(struct platform_device * , pm_message_t state ) ;
1070 int (*resume)(struct platform_device * ) ;
1071 struct device_driver driver ;
1072 struct platform_device_id const *id_table ;
1073};
1074#line 38 "include/linux/regulator/consumer.h"
1075struct device;
1076#line 109
1077struct regulator;
1078#line 109
1079struct regulator;
1080#line 27 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1081struct regulator_led {
1082 struct led_classdev cdev ;
1083 enum led_brightness value ;
1084 int enabled ;
1085 struct mutex mutex ;
1086 struct work_struct work ;
1087 struct regulator *vcc ;
1088};
1089#line 1 "<compiler builtins>"
1090long __builtin_expect(long val , long res ) ;
1091#line 24 "include/linux/list.h"
1092__inline static void INIT_LIST_HEAD(struct list_head *list ) __attribute__((__no_instrument_function__)) ;
1093#line 24 "include/linux/list.h"
1094__inline static void INIT_LIST_HEAD(struct list_head *list )
1095{ unsigned long __cil_tmp2 ;
1096 unsigned long __cil_tmp3 ;
1097
1098 {
1099#line 26
1100 *((struct list_head **)list) = list;
1101#line 27
1102 __cil_tmp2 = (unsigned long )list;
1103#line 27
1104 __cil_tmp3 = __cil_tmp2 + 8;
1105#line 27
1106 *((struct list_head **)__cil_tmp3) = list;
1107#line 28
1108 return;
1109}
1110}
1111#line 49 "include/linux/dynamic_debug.h"
1112extern int ( __dynamic_dev_dbg)(struct _ddebug *descriptor ,
1113 struct device const *dev ,
1114 char const *fmt , ...) ;
1115#line 27 "include/linux/err.h"
1116__inline static long __attribute__((__warn_unused_result__)) PTR_ERR(void const *ptr ) __attribute__((__no_instrument_function__)) ;
1117#line 27 "include/linux/err.h"
1118__inline static long __attribute__((__warn_unused_result__)) PTR_ERR(void const *ptr )
1119{
1120
1121 {
1122#line 29
1123 return ((long )ptr);
1124}
1125}
1126#line 32
1127__inline static long __attribute__((__warn_unused_result__)) IS_ERR(void const *ptr ) __attribute__((__no_instrument_function__)) ;
1128#line 32 "include/linux/err.h"
1129__inline static long __attribute__((__warn_unused_result__)) IS_ERR(void const *ptr )
1130{ long tmp ;
1131 unsigned long __cil_tmp3 ;
1132 int __cil_tmp4 ;
1133 int __cil_tmp5 ;
1134 int __cil_tmp6 ;
1135 long __cil_tmp7 ;
1136
1137 {
1138 {
1139#line 34
1140 __cil_tmp3 = (unsigned long )ptr;
1141#line 34
1142 __cil_tmp4 = __cil_tmp3 >= 0xfffffffffffff001UL;
1143#line 34
1144 __cil_tmp5 = ! __cil_tmp4;
1145#line 34
1146 __cil_tmp6 = ! __cil_tmp5;
1147#line 34
1148 __cil_tmp7 = (long )__cil_tmp6;
1149#line 34
1150 tmp = __builtin_expect(__cil_tmp7, 0L);
1151 }
1152#line 34
1153 return (tmp);
1154}
1155}
1156#line 115 "include/linux/mutex.h"
1157extern void __mutex_init(struct mutex *lock , char const *name , struct lock_class_key *key ) ;
1158#line 152
1159void mutex_lock(struct mutex *lock ) ;
1160#line 153
1161int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
1162#line 154
1163int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
1164#line 168
1165int mutex_trylock(struct mutex *lock ) ;
1166#line 169
1167void mutex_unlock(struct mutex *lock ) ;
1168#line 170
1169int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
1170#line 156 "include/linux/workqueue.h"
1171extern void __init_work(struct work_struct *work , int onstack ) ;
1172#line 380
1173extern int schedule_work(struct work_struct *work ) ;
1174#line 392
1175extern bool cancel_work_sync(struct work_struct *work ) ;
1176#line 26 "include/linux/export.h"
1177extern struct module __this_module ;
1178#line 67 "include/linux/module.h"
1179int init_module(void) ;
1180#line 68
1181void cleanup_module(void) ;
1182#line 161 "include/linux/slab.h"
1183extern void kfree(void const * ) ;
1184#line 221 "include/linux/slub_def.h"
1185extern void *__kmalloc(size_t size , gfp_t flags ) ;
1186#line 268
1187__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
1188 gfp_t flags ) __attribute__((__no_instrument_function__)) ;
1189#line 268 "include/linux/slub_def.h"
1190__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
1191 gfp_t flags )
1192{ void *tmp___2 ;
1193
1194 {
1195 {
1196#line 283
1197 tmp___2 = __kmalloc(size, flags);
1198 }
1199#line 283
1200 return (tmp___2);
1201}
1202}
1203#line 349 "include/linux/slab.h"
1204__inline static void *kzalloc(size_t size , gfp_t flags ) __attribute__((__no_instrument_function__)) ;
1205#line 349 "include/linux/slab.h"
1206__inline static void *kzalloc(size_t size , gfp_t flags )
1207{ void *tmp ;
1208 unsigned int __cil_tmp4 ;
1209
1210 {
1211 {
1212#line 351
1213 __cil_tmp4 = flags | 32768U;
1214#line 351
1215 tmp = kmalloc(size, __cil_tmp4);
1216 }
1217#line 351
1218 return (tmp);
1219}
1220}
1221#line 79 "include/linux/leds.h"
1222extern int led_classdev_register(struct device *parent , struct led_classdev *led_cdev ) ;
1223#line 81
1224extern void led_classdev_unregister(struct led_classdev *led_cdev ) ;
1225#line 792 "include/linux/device.h"
1226extern void *dev_get_drvdata(struct device const *dev ) ;
1227#line 793
1228extern int dev_set_drvdata(struct device *dev , void *data ) ;
1229#line 891
1230extern int ( dev_err)(struct device const *dev , char const *fmt
1231 , ...) ;
1232#line 174 "include/linux/platform_device.h"
1233extern int platform_driver_register(struct platform_driver * ) ;
1234#line 175
1235extern void platform_driver_unregister(struct platform_driver * ) ;
1236#line 183
1237__inline static void *platform_get_drvdata(struct platform_device const *pdev ) __attribute__((__no_instrument_function__)) ;
1238#line 183 "include/linux/platform_device.h"
1239__inline static void *platform_get_drvdata(struct platform_device const *pdev )
1240{ void *tmp ;
1241 unsigned long __cil_tmp3 ;
1242 unsigned long __cil_tmp4 ;
1243 struct device const *__cil_tmp5 ;
1244
1245 {
1246 {
1247#line 185
1248 __cil_tmp3 = (unsigned long )pdev;
1249#line 185
1250 __cil_tmp4 = __cil_tmp3 + 16;
1251#line 185
1252 __cil_tmp5 = (struct device const *)__cil_tmp4;
1253#line 185
1254 tmp = dev_get_drvdata(__cil_tmp5);
1255 }
1256#line 185
1257 return (tmp);
1258}
1259}
1260#line 188
1261__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) __attribute__((__no_instrument_function__)) ;
1262#line 188 "include/linux/platform_device.h"
1263__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )
1264{ unsigned long __cil_tmp3 ;
1265 unsigned long __cil_tmp4 ;
1266 struct device *__cil_tmp5 ;
1267
1268 {
1269 {
1270#line 190
1271 __cil_tmp3 = (unsigned long )pdev;
1272#line 190
1273 __cil_tmp4 = __cil_tmp3 + 16;
1274#line 190
1275 __cil_tmp5 = (struct device *)__cil_tmp4;
1276#line 190
1277 dev_set_drvdata(__cil_tmp5, data);
1278 }
1279#line 191
1280 return;
1281}
1282}
1283#line 138 "include/linux/regulator/consumer.h"
1284extern struct regulator * __attribute__((__warn_unused_result__)) regulator_get_exclusive(struct device *dev ,
1285 char const *id ) ;
1286#line 140
1287extern void regulator_put(struct regulator *regulator ) ;
1288#line 144
1289extern int regulator_enable(struct regulator *regulator ) ;
1290#line 145
1291extern int regulator_disable(struct regulator *regulator ) ;
1292#line 147
1293extern int regulator_is_enabled(struct regulator *regulator ) ;
1294#line 163
1295extern int regulator_count_voltages(struct regulator *regulator ) ;
1296#line 164
1297extern int regulator_list_voltage(struct regulator *regulator , unsigned int selector ) ;
1298#line 167
1299extern int regulator_set_voltage(struct regulator *regulator , int min_uV , int max_uV ) ;
1300#line 37 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1301__inline static int led_regulator_get_max_brightness(struct regulator *supply ) __attribute__((__no_instrument_function__)) ;
1302#line 37 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1303__inline static int led_regulator_get_max_brightness(struct regulator *supply )
1304{ int ret ;
1305 int voltage ;
1306 int tmp ;
1307 int tmp___0 ;
1308
1309 {
1310 {
1311#line 40
1312 tmp = regulator_list_voltage(supply, 0U);
1313#line 40
1314 voltage = tmp;
1315 }
1316#line 42
1317 if (voltage <= 0) {
1318#line 43
1319 return (1);
1320 } else {
1321
1322 }
1323 {
1324#line 49
1325 ret = regulator_set_voltage(supply, voltage, voltage);
1326 }
1327#line 50
1328 if (ret < 0) {
1329#line 51
1330 return (1);
1331 } else {
1332
1333 }
1334 {
1335#line 53
1336 tmp___0 = regulator_count_voltages(supply);
1337 }
1338#line 53
1339 return (tmp___0);
1340}
1341}
1342#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1343static int led_regulator_get_voltage(struct regulator *supply , enum led_brightness brightness )
1344{ int tmp ;
1345 unsigned int __cil_tmp4 ;
1346 unsigned int __cil_tmp5 ;
1347 unsigned int __cil_tmp6 ;
1348
1349 {
1350 {
1351#line 59
1352 __cil_tmp4 = (unsigned int )brightness;
1353#line 59
1354 if (__cil_tmp4 == 0U) {
1355#line 60
1356 return (-22);
1357 } else {
1358
1359 }
1360 }
1361 {
1362#line 62
1363 __cil_tmp5 = (unsigned int )brightness;
1364#line 62
1365 __cil_tmp6 = __cil_tmp5 - 1U;
1366#line 62
1367 tmp = regulator_list_voltage(supply, __cil_tmp6);
1368 }
1369#line 62
1370 return (tmp);
1371}
1372}
1373#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1374static void regulator_led_enable(struct regulator_led *led )
1375{ int ret ;
1376 unsigned long __cil_tmp3 ;
1377 unsigned long __cil_tmp4 ;
1378 unsigned long __cil_tmp5 ;
1379 unsigned long __cil_tmp6 ;
1380 struct regulator *__cil_tmp7 ;
1381 unsigned long __cil_tmp8 ;
1382 unsigned long __cil_tmp9 ;
1383 unsigned long __cil_tmp10 ;
1384 struct device *__cil_tmp11 ;
1385 struct device const *__cil_tmp12 ;
1386 unsigned long __cil_tmp13 ;
1387 unsigned long __cil_tmp14 ;
1388
1389 {
1390 {
1391#line 70
1392 __cil_tmp3 = (unsigned long )led;
1393#line 70
1394 __cil_tmp4 = __cil_tmp3 + 268;
1395#line 70
1396 if (*((int *)__cil_tmp4)) {
1397#line 71
1398 return;
1399 } else {
1400
1401 }
1402 }
1403 {
1404#line 73
1405 __cil_tmp5 = (unsigned long )led;
1406#line 73
1407 __cil_tmp6 = __cil_tmp5 + 376;
1408#line 73
1409 __cil_tmp7 = *((struct regulator **)__cil_tmp6);
1410#line 73
1411 ret = regulator_enable(__cil_tmp7);
1412 }
1413#line 74
1414 if (ret != 0) {
1415 {
1416#line 75
1417 __cil_tmp8 = 0 + 48;
1418#line 75
1419 __cil_tmp9 = (unsigned long )led;
1420#line 75
1421 __cil_tmp10 = __cil_tmp9 + __cil_tmp8;
1422#line 75
1423 __cil_tmp11 = *((struct device **)__cil_tmp10);
1424#line 75
1425 __cil_tmp12 = (struct device const *)__cil_tmp11;
1426#line 75
1427 dev_err(__cil_tmp12, "Failed to enable vcc: %d\n", ret);
1428 }
1429#line 76
1430 return;
1431 } else {
1432
1433 }
1434#line 79
1435 __cil_tmp13 = (unsigned long )led;
1436#line 79
1437 __cil_tmp14 = __cil_tmp13 + 268;
1438#line 79
1439 *((int *)__cil_tmp14) = 1;
1440#line 80
1441 return;
1442}
1443}
1444#line 82 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1445static void regulator_led_disable(struct regulator_led *led )
1446{ int ret ;
1447 unsigned long __cil_tmp3 ;
1448 unsigned long __cil_tmp4 ;
1449 int __cil_tmp5 ;
1450 unsigned long __cil_tmp6 ;
1451 unsigned long __cil_tmp7 ;
1452 struct regulator *__cil_tmp8 ;
1453 unsigned long __cil_tmp9 ;
1454 unsigned long __cil_tmp10 ;
1455 unsigned long __cil_tmp11 ;
1456 struct device *__cil_tmp12 ;
1457 struct device const *__cil_tmp13 ;
1458 unsigned long __cil_tmp14 ;
1459 unsigned long __cil_tmp15 ;
1460
1461 {
1462 {
1463#line 86
1464 __cil_tmp3 = (unsigned long )led;
1465#line 86
1466 __cil_tmp4 = __cil_tmp3 + 268;
1467#line 86
1468 __cil_tmp5 = *((int *)__cil_tmp4);
1469#line 86
1470 if (! __cil_tmp5) {
1471#line 87
1472 return;
1473 } else {
1474
1475 }
1476 }
1477 {
1478#line 89
1479 __cil_tmp6 = (unsigned long )led;
1480#line 89
1481 __cil_tmp7 = __cil_tmp6 + 376;
1482#line 89
1483 __cil_tmp8 = *((struct regulator **)__cil_tmp7);
1484#line 89
1485 ret = regulator_disable(__cil_tmp8);
1486 }
1487#line 90
1488 if (ret != 0) {
1489 {
1490#line 91
1491 __cil_tmp9 = 0 + 48;
1492#line 91
1493 __cil_tmp10 = (unsigned long )led;
1494#line 91
1495 __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
1496#line 91
1497 __cil_tmp12 = *((struct device **)__cil_tmp11);
1498#line 91
1499 __cil_tmp13 = (struct device const *)__cil_tmp12;
1500#line 91
1501 dev_err(__cil_tmp13, "Failed to disable vcc: %d\n", ret);
1502 }
1503#line 92
1504 return;
1505 } else {
1506
1507 }
1508#line 95
1509 __cil_tmp14 = (unsigned long )led;
1510#line 95
1511 __cil_tmp15 = __cil_tmp14 + 268;
1512#line 95
1513 *((int *)__cil_tmp15) = 0;
1514#line 96
1515 return;
1516}
1517}
1518#line 112
1519static void regulator_led_set_value(struct regulator_led *led ) ;
1520#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1521static struct _ddebug __attribute__((__aligned__(8))) descriptor __attribute__((__used__,
1522__section__("__verbose"))) = {"leds_regulator", "regulator_led_set_value", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c",
1523 "brightness: %d voltage: %d\n", 113U, 0U};
1524#line 98 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1525static void regulator_led_set_value(struct regulator_led *led )
1526{ int voltage ;
1527 int ret ;
1528 long tmp ;
1529 unsigned long __cil_tmp5 ;
1530 unsigned long __cil_tmp6 ;
1531 struct mutex *__cil_tmp7 ;
1532 unsigned long __cil_tmp8 ;
1533 unsigned long __cil_tmp9 ;
1534 enum led_brightness __cil_tmp10 ;
1535 unsigned int __cil_tmp11 ;
1536 unsigned long __cil_tmp12 ;
1537 unsigned long __cil_tmp13 ;
1538 unsigned long __cil_tmp14 ;
1539 int __cil_tmp15 ;
1540 unsigned long __cil_tmp16 ;
1541 unsigned long __cil_tmp17 ;
1542 struct regulator *__cil_tmp18 ;
1543 unsigned long __cil_tmp19 ;
1544 unsigned long __cil_tmp20 ;
1545 enum led_brightness __cil_tmp21 ;
1546 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp22 ;
1547 unsigned int __cil_tmp23 ;
1548 unsigned int __cil_tmp24 ;
1549 int __cil_tmp25 ;
1550 int __cil_tmp26 ;
1551 long __cil_tmp27 ;
1552 unsigned long __cil_tmp28 ;
1553 unsigned long __cil_tmp29 ;
1554 unsigned long __cil_tmp30 ;
1555 struct device *__cil_tmp31 ;
1556 struct device const *__cil_tmp32 ;
1557 unsigned long __cil_tmp33 ;
1558 unsigned long __cil_tmp34 ;
1559 enum led_brightness __cil_tmp35 ;
1560 unsigned int __cil_tmp36 ;
1561 unsigned long __cil_tmp37 ;
1562 unsigned long __cil_tmp38 ;
1563 struct regulator *__cil_tmp39 ;
1564 unsigned long __cil_tmp40 ;
1565 unsigned long __cil_tmp41 ;
1566 unsigned long __cil_tmp42 ;
1567 struct device *__cil_tmp43 ;
1568 struct device const *__cil_tmp44 ;
1569 unsigned long __cil_tmp45 ;
1570 unsigned long __cil_tmp46 ;
1571 struct mutex *__cil_tmp47 ;
1572
1573 {
1574 {
1575#line 103
1576 __cil_tmp5 = (unsigned long )led;
1577#line 103
1578 __cil_tmp6 = __cil_tmp5 + 272;
1579#line 103
1580 __cil_tmp7 = (struct mutex *)__cil_tmp6;
1581#line 103
1582 mutex_lock(__cil_tmp7);
1583 }
1584 {
1585#line 105
1586 __cil_tmp8 = (unsigned long )led;
1587#line 105
1588 __cil_tmp9 = __cil_tmp8 + 264;
1589#line 105
1590 __cil_tmp10 = *((enum led_brightness *)__cil_tmp9);
1591#line 105
1592 __cil_tmp11 = (unsigned int )__cil_tmp10;
1593#line 105
1594 if (__cil_tmp11 == 0U) {
1595 {
1596#line 106
1597 regulator_led_disable(led);
1598 }
1599#line 107
1600 goto out;
1601 } else {
1602
1603 }
1604 }
1605 {
1606#line 110
1607 __cil_tmp12 = 0 + 12;
1608#line 110
1609 __cil_tmp13 = (unsigned long )led;
1610#line 110
1611 __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
1612#line 110
1613 __cil_tmp15 = *((int *)__cil_tmp14);
1614#line 110
1615 if (__cil_tmp15 > 1) {
1616 {
1617#line 111
1618 __cil_tmp16 = (unsigned long )led;
1619#line 111
1620 __cil_tmp17 = __cil_tmp16 + 376;
1621#line 111
1622 __cil_tmp18 = *((struct regulator **)__cil_tmp17);
1623#line 111
1624 __cil_tmp19 = (unsigned long )led;
1625#line 111
1626 __cil_tmp20 = __cil_tmp19 + 264;
1627#line 111
1628 __cil_tmp21 = *((enum led_brightness *)__cil_tmp20);
1629#line 111
1630 voltage = led_regulator_get_voltage(__cil_tmp18, __cil_tmp21);
1631 }
1632 {
1633#line 112
1634 while (1) {
1635 while_continue: ;
1636 {
1637#line 112
1638 while (1) {
1639 while_continue___0: ;
1640 {
1641#line 112
1642 __cil_tmp22 = & descriptor;
1643#line 112
1644 __cil_tmp23 = __cil_tmp22->flags;
1645#line 112
1646 __cil_tmp24 = __cil_tmp23 & 1U;
1647#line 112
1648 __cil_tmp25 = ! __cil_tmp24;
1649#line 112
1650 __cil_tmp26 = ! __cil_tmp25;
1651#line 112
1652 __cil_tmp27 = (long )__cil_tmp26;
1653#line 112
1654 tmp = __builtin_expect(__cil_tmp27, 0L);
1655 }
1656#line 112
1657 if (tmp) {
1658 {
1659#line 112
1660 __cil_tmp28 = 0 + 48;
1661#line 112
1662 __cil_tmp29 = (unsigned long )led;
1663#line 112
1664 __cil_tmp30 = __cil_tmp29 + __cil_tmp28;
1665#line 112
1666 __cil_tmp31 = *((struct device **)__cil_tmp30);
1667#line 112
1668 __cil_tmp32 = (struct device const *)__cil_tmp31;
1669#line 112
1670 __cil_tmp33 = (unsigned long )led;
1671#line 112
1672 __cil_tmp34 = __cil_tmp33 + 264;
1673#line 112
1674 __cil_tmp35 = *((enum led_brightness *)__cil_tmp34);
1675#line 112
1676 __cil_tmp36 = (unsigned int )__cil_tmp35;
1677#line 112
1678 __dynamic_dev_dbg(& descriptor, __cil_tmp32, "brightness: %d voltage: %d\n",
1679 __cil_tmp36, voltage);
1680 }
1681 } else {
1682
1683 }
1684#line 112
1685 goto while_break___0;
1686 }
1687 while_break___0: ;
1688 }
1689#line 112
1690 goto while_break;
1691 }
1692 while_break: ;
1693 }
1694 {
1695#line 115
1696 __cil_tmp37 = (unsigned long )led;
1697#line 115
1698 __cil_tmp38 = __cil_tmp37 + 376;
1699#line 115
1700 __cil_tmp39 = *((struct regulator **)__cil_tmp38);
1701#line 115
1702 ret = regulator_set_voltage(__cil_tmp39, voltage, voltage);
1703 }
1704#line 116
1705 if (ret != 0) {
1706 {
1707#line 117
1708 __cil_tmp40 = 0 + 48;
1709#line 117
1710 __cil_tmp41 = (unsigned long )led;
1711#line 117
1712 __cil_tmp42 = __cil_tmp41 + __cil_tmp40;
1713#line 117
1714 __cil_tmp43 = *((struct device **)__cil_tmp42);
1715#line 117
1716 __cil_tmp44 = (struct device const *)__cil_tmp43;
1717#line 117
1718 dev_err(__cil_tmp44, "Failed to set voltage %d: %d\n", voltage, ret);
1719 }
1720 } else {
1721
1722 }
1723 } else {
1724
1725 }
1726 }
1727 {
1728#line 121
1729 regulator_led_enable(led);
1730 }
1731 out:
1732 {
1733#line 124
1734 __cil_tmp45 = (unsigned long )led;
1735#line 124
1736 __cil_tmp46 = __cil_tmp45 + 272;
1737#line 124
1738 __cil_tmp47 = (struct mutex *)__cil_tmp46;
1739#line 124
1740 mutex_unlock(__cil_tmp47);
1741 }
1742#line 125
1743 return;
1744}
1745}
1746#line 127 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1747static void led_work(struct work_struct *work )
1748{ struct regulator_led *led ;
1749 struct work_struct const *__mptr ;
1750 struct regulator_led *__cil_tmp4 ;
1751 unsigned long __cil_tmp5 ;
1752 unsigned long __cil_tmp6 ;
1753 struct work_struct *__cil_tmp7 ;
1754 unsigned int __cil_tmp8 ;
1755 char *__cil_tmp9 ;
1756 char *__cil_tmp10 ;
1757
1758 {
1759 {
1760#line 131
1761 __mptr = (struct work_struct const *)work;
1762#line 131
1763 __cil_tmp4 = (struct regulator_led *)0;
1764#line 131
1765 __cil_tmp5 = (unsigned long )__cil_tmp4;
1766#line 131
1767 __cil_tmp6 = __cil_tmp5 + 344;
1768#line 131
1769 __cil_tmp7 = (struct work_struct *)__cil_tmp6;
1770#line 131
1771 __cil_tmp8 = (unsigned int )__cil_tmp7;
1772#line 131
1773 __cil_tmp9 = (char *)__mptr;
1774#line 131
1775 __cil_tmp10 = __cil_tmp9 - __cil_tmp8;
1776#line 131
1777 led = (struct regulator_led *)__cil_tmp10;
1778#line 132
1779 regulator_led_set_value(led);
1780 }
1781#line 133
1782 return;
1783}
1784}
1785#line 135 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1786static void regulator_led_brightness_set(struct led_classdev *led_cdev , enum led_brightness value )
1787{ struct regulator_led *led ;
1788 struct led_classdev const *__mptr ;
1789 struct regulator_led *__cil_tmp5 ;
1790 struct led_classdev *__cil_tmp6 ;
1791 unsigned int __cil_tmp7 ;
1792 char *__cil_tmp8 ;
1793 char *__cil_tmp9 ;
1794 unsigned long __cil_tmp10 ;
1795 unsigned long __cil_tmp11 ;
1796 unsigned long __cil_tmp12 ;
1797 unsigned long __cil_tmp13 ;
1798 struct work_struct *__cil_tmp14 ;
1799
1800 {
1801 {
1802#line 138
1803 __mptr = (struct led_classdev const *)led_cdev;
1804#line 138
1805 __cil_tmp5 = (struct regulator_led *)0;
1806#line 138
1807 __cil_tmp6 = (struct led_classdev *)__cil_tmp5;
1808#line 138
1809 __cil_tmp7 = (unsigned int )__cil_tmp6;
1810#line 138
1811 __cil_tmp8 = (char *)__mptr;
1812#line 138
1813 __cil_tmp9 = __cil_tmp8 - __cil_tmp7;
1814#line 138
1815 led = (struct regulator_led *)__cil_tmp9;
1816#line 140
1817 __cil_tmp10 = (unsigned long )led;
1818#line 140
1819 __cil_tmp11 = __cil_tmp10 + 264;
1820#line 140
1821 *((enum led_brightness *)__cil_tmp11) = value;
1822#line 141
1823 __cil_tmp12 = (unsigned long )led;
1824#line 141
1825 __cil_tmp13 = __cil_tmp12 + 344;
1826#line 141
1827 __cil_tmp14 = (struct work_struct *)__cil_tmp13;
1828#line 141
1829 schedule_work(__cil_tmp14);
1830 }
1831#line 142
1832 return;
1833}
1834}
1835#line 186 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1836static struct lock_class_key __key___2 ;
1837#line 144
1838static int regulator_led_probe(struct platform_device *pdev ) __attribute__((__section__(".devinit.text"),
1839__no_instrument_function__)) ;
1840#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
1841static int regulator_led_probe(struct platform_device *pdev )
1842{ struct led_regulator_platform_data *pdata ;
1843 struct regulator_led *led ;
1844 struct regulator *vcc ;
1845 int ret ;
1846 long tmp ;
1847 long tmp___0 ;
1848 void *tmp___1 ;
1849 int tmp___2 ;
1850 atomic_long_t __constr_expr_0 ;
1851 unsigned long __cil_tmp11 ;
1852 unsigned long __cil_tmp12 ;
1853 unsigned long __cil_tmp13 ;
1854 void *__cil_tmp14 ;
1855 void *__cil_tmp15 ;
1856 unsigned long __cil_tmp16 ;
1857 unsigned long __cil_tmp17 ;
1858 unsigned long __cil_tmp18 ;
1859 unsigned long __cil_tmp19 ;
1860 struct device *__cil_tmp20 ;
1861 struct device const *__cil_tmp21 ;
1862 unsigned long __cil_tmp22 ;
1863 unsigned long __cil_tmp23 ;
1864 struct device *__cil_tmp24 ;
1865 void const *__cil_tmp25 ;
1866 unsigned long __cil_tmp26 ;
1867 unsigned long __cil_tmp27 ;
1868 struct device *__cil_tmp28 ;
1869 struct device const *__cil_tmp29 ;
1870 char *__cil_tmp30 ;
1871 void const *__cil_tmp31 ;
1872 void *__cil_tmp32 ;
1873 unsigned long __cil_tmp33 ;
1874 unsigned long __cil_tmp34 ;
1875 unsigned long __cil_tmp35 ;
1876 unsigned long __cil_tmp36 ;
1877 unsigned long __cil_tmp37 ;
1878 unsigned long __cil_tmp38 ;
1879 unsigned long __cil_tmp39 ;
1880 unsigned long __cil_tmp40 ;
1881 int __cil_tmp41 ;
1882 unsigned int __cil_tmp42 ;
1883 unsigned long __cil_tmp43 ;
1884 unsigned long __cil_tmp44 ;
1885 enum led_brightness __cil_tmp45 ;
1886 unsigned int __cil_tmp46 ;
1887 unsigned long __cil_tmp47 ;
1888 unsigned long __cil_tmp48 ;
1889 struct device *__cil_tmp49 ;
1890 struct device const *__cil_tmp50 ;
1891 unsigned long __cil_tmp51 ;
1892 unsigned long __cil_tmp52 ;
1893 enum led_brightness __cil_tmp53 ;
1894 unsigned int __cil_tmp54 ;
1895 unsigned long __cil_tmp55 ;
1896 unsigned long __cil_tmp56 ;
1897 unsigned long __cil_tmp57 ;
1898 unsigned long __cil_tmp58 ;
1899 unsigned long __cil_tmp59 ;
1900 unsigned long __cil_tmp60 ;
1901 unsigned long __cil_tmp61 ;
1902 char *__cil_tmp62 ;
1903 unsigned long __cil_tmp63 ;
1904 unsigned long __cil_tmp64 ;
1905 unsigned long __cil_tmp65 ;
1906 int __cil_tmp66 ;
1907 unsigned long __cil_tmp67 ;
1908 unsigned long __cil_tmp68 ;
1909 unsigned long __cil_tmp69 ;
1910 int __cil_tmp70 ;
1911 unsigned long __cil_tmp71 ;
1912 unsigned long __cil_tmp72 ;
1913 unsigned long __cil_tmp73 ;
1914 unsigned long __cil_tmp74 ;
1915 struct regulator *__cil_tmp75 ;
1916 unsigned long __cil_tmp76 ;
1917 unsigned long __cil_tmp77 ;
1918 unsigned long __cil_tmp78 ;
1919 unsigned long __cil_tmp79 ;
1920 struct mutex *__cil_tmp80 ;
1921 unsigned long __cil_tmp81 ;
1922 unsigned long __cil_tmp82 ;
1923 struct work_struct *__cil_tmp83 ;
1924 unsigned long __cil_tmp84 ;
1925 unsigned long __cil_tmp85 ;
1926 unsigned long __cil_tmp86 ;
1927 unsigned long __cil_tmp87 ;
1928 unsigned long __cil_tmp88 ;
1929 struct list_head *__cil_tmp89 ;
1930 unsigned long __cil_tmp90 ;
1931 unsigned long __cil_tmp91 ;
1932 unsigned long __cil_tmp92 ;
1933 void *__cil_tmp93 ;
1934 unsigned long __cil_tmp94 ;
1935 unsigned long __cil_tmp95 ;
1936 struct device *__cil_tmp96 ;
1937 struct led_classdev *__cil_tmp97 ;
1938 unsigned long __cil_tmp98 ;
1939 unsigned long __cil_tmp99 ;
1940 struct work_struct *__cil_tmp100 ;
1941 unsigned long __cil_tmp101 ;
1942 unsigned long __cil_tmp102 ;
1943 unsigned long __cil_tmp103 ;
1944 unsigned long __cil_tmp104 ;
1945 unsigned long __cil_tmp105 ;
1946 enum led_brightness __cil_tmp106 ;
1947 void const *__cil_tmp107 ;
1948 long __constr_expr_0_counter108 ;
1949
1950 {
1951#line 146
1952 __cil_tmp11 = 16 + 184;
1953#line 146
1954 __cil_tmp12 = (unsigned long )pdev;
1955#line 146
1956 __cil_tmp13 = __cil_tmp12 + __cil_tmp11;
1957#line 146
1958 __cil_tmp14 = *((void **)__cil_tmp13);
1959#line 146
1960 pdata = (struct led_regulator_platform_data *)__cil_tmp14;
1961#line 149
1962 ret = 0;
1963 {
1964#line 151
1965 __cil_tmp15 = (void *)0;
1966#line 151
1967 __cil_tmp16 = (unsigned long )__cil_tmp15;
1968#line 151
1969 __cil_tmp17 = (unsigned long )pdata;
1970#line 151
1971 if (__cil_tmp17 == __cil_tmp16) {
1972 {
1973#line 152
1974 __cil_tmp18 = (unsigned long )pdev;
1975#line 152
1976 __cil_tmp19 = __cil_tmp18 + 16;
1977#line 152
1978 __cil_tmp20 = (struct device *)__cil_tmp19;
1979#line 152
1980 __cil_tmp21 = (struct device const *)__cil_tmp20;
1981#line 152
1982 dev_err(__cil_tmp21, "no platform data\n");
1983 }
1984#line 153
1985 return (-19);
1986 } else {
1987
1988 }
1989 }
1990 {
1991#line 156
1992 __cil_tmp22 = (unsigned long )pdev;
1993#line 156
1994 __cil_tmp23 = __cil_tmp22 + 16;
1995#line 156
1996 __cil_tmp24 = (struct device *)__cil_tmp23;
1997#line 156
1998 vcc = (struct regulator *)regulator_get_exclusive(__cil_tmp24, "vled");
1999#line 157
2000 __cil_tmp25 = (void const *)vcc;
2001#line 157
2002 tmp___0 = (long )IS_ERR(__cil_tmp25);
2003 }
2004#line 157
2005 if (tmp___0) {
2006 {
2007#line 158
2008 __cil_tmp26 = (unsigned long )pdev;
2009#line 158
2010 __cil_tmp27 = __cil_tmp26 + 16;
2011#line 158
2012 __cil_tmp28 = (struct device *)__cil_tmp27;
2013#line 158
2014 __cil_tmp29 = (struct device const *)__cil_tmp28;
2015#line 158
2016 __cil_tmp30 = *((char **)pdata);
2017#line 158
2018 dev_err(__cil_tmp29, "Cannot get vcc for %s\n", __cil_tmp30);
2019#line 159
2020 __cil_tmp31 = (void const *)vcc;
2021#line 159
2022 tmp = (long )PTR_ERR(__cil_tmp31);
2023 }
2024#line 159
2025 return ((int )tmp);
2026 } else {
2027
2028 }
2029 {
2030#line 162
2031 tmp___1 = kzalloc(384UL, 208U);
2032#line 162
2033 led = (struct regulator_led *)tmp___1;
2034 }
2035 {
2036#line 163
2037 __cil_tmp32 = (void *)0;
2038#line 163
2039 __cil_tmp33 = (unsigned long )__cil_tmp32;
2040#line 163
2041 __cil_tmp34 = (unsigned long )led;
2042#line 163
2043 if (__cil_tmp34 == __cil_tmp33) {
2044#line 164
2045 ret = -12;
2046#line 165
2047 goto err_vcc;
2048 } else {
2049
2050 }
2051 }
2052 {
2053#line 168
2054 __cil_tmp35 = 0 + 12;
2055#line 168
2056 __cil_tmp36 = (unsigned long )led;
2057#line 168
2058 __cil_tmp37 = __cil_tmp36 + __cil_tmp35;
2059#line 168
2060 *((int *)__cil_tmp37) = led_regulator_get_max_brightness(vcc);
2061 }
2062 {
2063#line 169
2064 __cil_tmp38 = 0 + 12;
2065#line 169
2066 __cil_tmp39 = (unsigned long )led;
2067#line 169
2068 __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
2069#line 169
2070 __cil_tmp41 = *((int *)__cil_tmp40);
2071#line 169
2072 __cil_tmp42 = (unsigned int )__cil_tmp41;
2073#line 169
2074 __cil_tmp43 = (unsigned long )pdata;
2075#line 169
2076 __cil_tmp44 = __cil_tmp43 + 8;
2077#line 169
2078 __cil_tmp45 = *((enum led_brightness *)__cil_tmp44);
2079#line 169
2080 __cil_tmp46 = (unsigned int )__cil_tmp45;
2081#line 169
2082 if (__cil_tmp46 > __cil_tmp42) {
2083 {
2084#line 170
2085 __cil_tmp47 = (unsigned long )pdev;
2086#line 170
2087 __cil_tmp48 = __cil_tmp47 + 16;
2088#line 170
2089 __cil_tmp49 = (struct device *)__cil_tmp48;
2090#line 170
2091 __cil_tmp50 = (struct device const *)__cil_tmp49;
2092#line 170
2093 __cil_tmp51 = (unsigned long )pdata;
2094#line 170
2095 __cil_tmp52 = __cil_tmp51 + 8;
2096#line 170
2097 __cil_tmp53 = *((enum led_brightness *)__cil_tmp52);
2098#line 170
2099 __cil_tmp54 = (unsigned int )__cil_tmp53;
2100#line 170
2101 dev_err(__cil_tmp50, "Invalid default brightness %d\n", __cil_tmp54);
2102#line 172
2103 ret = -22;
2104 }
2105#line 173
2106 goto err_led;
2107 } else {
2108
2109 }
2110 }
2111 {
2112#line 175
2113 __cil_tmp55 = (unsigned long )led;
2114#line 175
2115 __cil_tmp56 = __cil_tmp55 + 264;
2116#line 175
2117 __cil_tmp57 = (unsigned long )pdata;
2118#line 175
2119 __cil_tmp58 = __cil_tmp57 + 8;
2120#line 175
2121 *((enum led_brightness *)__cil_tmp56) = *((enum led_brightness *)__cil_tmp58);
2122#line 177
2123 __cil_tmp59 = 0 + 24;
2124#line 177
2125 __cil_tmp60 = (unsigned long )led;
2126#line 177
2127 __cil_tmp61 = __cil_tmp60 + __cil_tmp59;
2128#line 177
2129 *((void (**)(struct led_classdev *led_cdev , enum led_brightness brightness ))__cil_tmp61) = & regulator_led_brightness_set;
2130#line 178
2131 __cil_tmp62 = *((char **)pdata);
2132#line 178
2133 *((char const **)led) = (char const *)__cil_tmp62;
2134#line 179
2135 __cil_tmp63 = 0 + 16;
2136#line 179
2137 __cil_tmp64 = (unsigned long )led;
2138#line 179
2139 __cil_tmp65 = __cil_tmp64 + __cil_tmp63;
2140#line 179
2141 __cil_tmp66 = 1 << 16;
2142#line 179
2143 __cil_tmp67 = 0 + 16;
2144#line 179
2145 __cil_tmp68 = (unsigned long )led;
2146#line 179
2147 __cil_tmp69 = __cil_tmp68 + __cil_tmp67;
2148#line 179
2149 __cil_tmp70 = *((int *)__cil_tmp69);
2150#line 179
2151 *((int *)__cil_tmp65) = __cil_tmp70 | __cil_tmp66;
2152#line 180
2153 __cil_tmp71 = (unsigned long )led;
2154#line 180
2155 __cil_tmp72 = __cil_tmp71 + 376;
2156#line 180
2157 *((struct regulator **)__cil_tmp72) = vcc;
2158#line 183
2159 __cil_tmp73 = (unsigned long )led;
2160#line 183
2161 __cil_tmp74 = __cil_tmp73 + 376;
2162#line 183
2163 __cil_tmp75 = *((struct regulator **)__cil_tmp74);
2164#line 183
2165 tmp___2 = regulator_is_enabled(__cil_tmp75);
2166 }
2167#line 183
2168 if (tmp___2) {
2169#line 184
2170 __cil_tmp76 = (unsigned long )led;
2171#line 184
2172 __cil_tmp77 = __cil_tmp76 + 268;
2173#line 184
2174 *((int *)__cil_tmp77) = 1;
2175 } else {
2176
2177 }
2178 {
2179#line 186
2180 while (1) {
2181 while_continue: ;
2182 {
2183#line 186
2184 __cil_tmp78 = (unsigned long )led;
2185#line 186
2186 __cil_tmp79 = __cil_tmp78 + 272;
2187#line 186
2188 __cil_tmp80 = (struct mutex *)__cil_tmp79;
2189#line 186
2190 __mutex_init(__cil_tmp80, "&led->mutex", & __key___2);
2191 }
2192#line 186
2193 goto while_break;
2194 }
2195 while_break: ;
2196 }
2197 {
2198#line 187
2199 while (1) {
2200 while_continue___0: ;
2201 {
2202#line 187
2203 while (1) {
2204 while_continue___1: ;
2205 {
2206#line 187
2207 __cil_tmp81 = (unsigned long )led;
2208#line 187
2209 __cil_tmp82 = __cil_tmp81 + 344;
2210#line 187
2211 __cil_tmp83 = (struct work_struct *)__cil_tmp82;
2212#line 187
2213 __init_work(__cil_tmp83, 0);
2214#line 187
2215 __constr_expr_0_counter108 = 2097664L;
2216#line 187
2217 __cil_tmp84 = (unsigned long )led;
2218#line 187
2219 __cil_tmp85 = __cil_tmp84 + 344;
2220#line 187
2221 ((atomic_long_t *)__cil_tmp85)->counter = __constr_expr_0_counter108;
2222#line 187
2223 __cil_tmp86 = 344 + 8;
2224#line 187
2225 __cil_tmp87 = (unsigned long )led;
2226#line 187
2227 __cil_tmp88 = __cil_tmp87 + __cil_tmp86;
2228#line 187
2229 __cil_tmp89 = (struct list_head *)__cil_tmp88;
2230#line 187
2231 INIT_LIST_HEAD(__cil_tmp89);
2232 }
2233 {
2234#line 187
2235 while (1) {
2236 while_continue___2: ;
2237#line 187
2238 __cil_tmp90 = 344 + 24;
2239#line 187
2240 __cil_tmp91 = (unsigned long )led;
2241#line 187
2242 __cil_tmp92 = __cil_tmp91 + __cil_tmp90;
2243#line 187
2244 *((void (**)(struct work_struct *work ))__cil_tmp92) = & led_work;
2245#line 187
2246 goto while_break___2;
2247 }
2248 while_break___2: ;
2249 }
2250#line 187
2251 goto while_break___1;
2252 }
2253 while_break___1: ;
2254 }
2255#line 187
2256 goto while_break___0;
2257 }
2258 while_break___0: ;
2259 }
2260 {
2261#line 189
2262 __cil_tmp93 = (void *)led;
2263#line 189
2264 platform_set_drvdata(pdev, __cil_tmp93);
2265#line 191
2266 __cil_tmp94 = (unsigned long )pdev;
2267#line 191
2268 __cil_tmp95 = __cil_tmp94 + 16;
2269#line 191
2270 __cil_tmp96 = (struct device *)__cil_tmp95;
2271#line 191
2272 __cil_tmp97 = (struct led_classdev *)led;
2273#line 191
2274 ret = led_classdev_register(__cil_tmp96, __cil_tmp97);
2275 }
2276#line 192
2277 if (ret < 0) {
2278 {
2279#line 193
2280 __cil_tmp98 = (unsigned long )led;
2281#line 193
2282 __cil_tmp99 = __cil_tmp98 + 344;
2283#line 193
2284 __cil_tmp100 = (struct work_struct *)__cil_tmp99;
2285#line 193
2286 cancel_work_sync(__cil_tmp100);
2287 }
2288#line 194
2289 goto err_led;
2290 } else {
2291
2292 }
2293 {
2294#line 198
2295 __cil_tmp101 = 0 + 8;
2296#line 198
2297 __cil_tmp102 = (unsigned long )led;
2298#line 198
2299 __cil_tmp103 = __cil_tmp102 + __cil_tmp101;
2300#line 198
2301 __cil_tmp104 = (unsigned long )led;
2302#line 198
2303 __cil_tmp105 = __cil_tmp104 + 264;
2304#line 198
2305 __cil_tmp106 = *((enum led_brightness *)__cil_tmp105);
2306#line 198
2307 *((int *)__cil_tmp103) = (int )__cil_tmp106;
2308#line 201
2309 regulator_led_set_value(led);
2310 }
2311#line 203
2312 return (0);
2313 err_led:
2314 {
2315#line 206
2316 __cil_tmp107 = (void const *)led;
2317#line 206
2318 kfree(__cil_tmp107);
2319 }
2320 err_vcc:
2321 {
2322#line 208
2323 regulator_put(vcc);
2324 }
2325#line 209
2326 return (ret);
2327}
2328}
2329#line 212
2330static int regulator_led_remove(struct platform_device *pdev ) __attribute__((__section__(".devexit.text"),
2331__no_instrument_function__)) ;
2332#line 212 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2333static int regulator_led_remove(struct platform_device *pdev )
2334{ struct regulator_led *led ;
2335 void *tmp ;
2336 struct platform_device const *__cil_tmp4 ;
2337 struct led_classdev *__cil_tmp5 ;
2338 unsigned long __cil_tmp6 ;
2339 unsigned long __cil_tmp7 ;
2340 struct work_struct *__cil_tmp8 ;
2341 unsigned long __cil_tmp9 ;
2342 unsigned long __cil_tmp10 ;
2343 struct regulator *__cil_tmp11 ;
2344 void const *__cil_tmp12 ;
2345
2346 {
2347 {
2348#line 214
2349 __cil_tmp4 = (struct platform_device const *)pdev;
2350#line 214
2351 tmp = platform_get_drvdata(__cil_tmp4);
2352#line 214
2353 led = (struct regulator_led *)tmp;
2354#line 216
2355 __cil_tmp5 = (struct led_classdev *)led;
2356#line 216
2357 led_classdev_unregister(__cil_tmp5);
2358#line 217
2359 __cil_tmp6 = (unsigned long )led;
2360#line 217
2361 __cil_tmp7 = __cil_tmp6 + 344;
2362#line 217
2363 __cil_tmp8 = (struct work_struct *)__cil_tmp7;
2364#line 217
2365 cancel_work_sync(__cil_tmp8);
2366#line 218
2367 regulator_led_disable(led);
2368#line 219
2369 __cil_tmp9 = (unsigned long )led;
2370#line 219
2371 __cil_tmp10 = __cil_tmp9 + 376;
2372#line 219
2373 __cil_tmp11 = *((struct regulator **)__cil_tmp10);
2374#line 219
2375 regulator_put(__cil_tmp11);
2376#line 220
2377 __cil_tmp12 = (void const *)led;
2378#line 220
2379 kfree(__cil_tmp12);
2380 }
2381#line 221
2382 return (0);
2383}
2384}
2385#line 224 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2386static struct platform_driver regulator_led_driver = {& regulator_led_probe, & regulator_led_remove, (void (*)(struct platform_device * ))0,
2387 (int (*)(struct platform_device * , pm_message_t state ))0, (int (*)(struct platform_device * ))0,
2388 {"leds-regulator", (struct bus_type *)0, & __this_module, (char const *)0, (_Bool)0,
2389 (struct of_device_id const *)0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
2390 (void (*)(struct device *dev ))0, (int (*)(struct device *dev , pm_message_t state ))0,
2391 (int (*)(struct device *dev ))0, (struct attribute_group const **)0, (struct dev_pm_ops const *)0,
2392 (struct driver_private *)0}, (struct platform_device_id const *)0};
2393#line 233
2394static int regulator_led_driver_init(void) __attribute__((__section__(".init.text"),
2395__no_instrument_function__)) ;
2396#line 233 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2397static int regulator_led_driver_init(void)
2398{ int tmp ;
2399
2400 {
2401 {
2402#line 233
2403 tmp = platform_driver_register(& regulator_led_driver);
2404 }
2405#line 233
2406 return (tmp);
2407}
2408}
2409#line 233 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2410int init_module(void)
2411{ int tmp ;
2412
2413 {
2414 {
2415#line 233
2416 tmp = regulator_led_driver_init();
2417 }
2418#line 233
2419 return (tmp);
2420}
2421}
2422#line 233
2423static void regulator_led_driver_exit(void) __attribute__((__section__(".exit.text"),
2424__no_instrument_function__)) ;
2425#line 233 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2426static void regulator_led_driver_exit(void)
2427{
2428
2429 {
2430 {
2431#line 233
2432 platform_driver_unregister(& regulator_led_driver);
2433 }
2434#line 233
2435 return;
2436}
2437}
2438#line 233 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2439void cleanup_module(void)
2440{
2441
2442 {
2443 {
2444#line 233
2445 regulator_led_driver_exit();
2446 }
2447#line 233
2448 return;
2449}
2450}
2451#line 235 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2452static char const __mod_author235[49] __attribute__((__used__, __unused__, __section__(".modinfo"),
2453__aligned__(1))) =
2454#line 235
2455 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
2456 (char const )'o', (char const )'r', (char const )'=', (char const )'A',
2457 (char const )'n', (char const )'t', (char const )'o', (char const )'n',
2458 (char const )'i', (char const )'o', (char const )' ', (char const )'O',
2459 (char const )'s', (char const )'p', (char const )'i', (char const )'t',
2460 (char const )'e', (char const )' ', (char const )'<', (char const )'o',
2461 (char const )'s', (char const )'p', (char const )'i', (char const )'t',
2462 (char const )'e', (char const )'@', (char const )'s', (char const )'t',
2463 (char const )'u', (char const )'d', (char const )'e', (char const )'n',
2464 (char const )'t', (char const )'i', (char const )'.', (char const )'u',
2465 (char const )'n', (char const )'i', (char const )'n', (char const )'a',
2466 (char const )'.', (char const )'i', (char const )'t', (char const )'>',
2467 (char const )'\000'};
2468#line 236 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2469static char const __mod_description236[40] __attribute__((__used__, __unused__,
2470__section__(".modinfo"), __aligned__(1))) =
2471#line 236
2472 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
2473 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
2474 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
2475 (char const )'R', (char const )'e', (char const )'g', (char const )'u',
2476 (char const )'l', (char const )'a', (char const )'t', (char const )'o',
2477 (char const )'r', (char const )' ', (char const )'d', (char const )'r',
2478 (char const )'i', (char const )'v', (char const )'e', (char const )'n',
2479 (char const )' ', (char const )'L', (char const )'E', (char const )'D',
2480 (char const )' ', (char const )'d', (char const )'r', (char const )'i',
2481 (char const )'v', (char const )'e', (char const )'r', (char const )'\000'};
2482#line 237 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2483static char const __mod_license237[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
2484__aligned__(1))) =
2485#line 237
2486 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
2487 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
2488 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
2489#line 238 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2490static char const __mod_alias238[30] __attribute__((__used__, __unused__, __section__(".modinfo"),
2491__aligned__(1))) =
2492#line 238
2493 { (char const )'a', (char const )'l', (char const )'i', (char const )'a',
2494 (char const )'s', (char const )'=', (char const )'p', (char const )'l',
2495 (char const )'a', (char const )'t', (char const )'f', (char const )'o',
2496 (char const )'r', (char const )'m', (char const )':', (char const )'l',
2497 (char const )'e', (char const )'d', (char const )'s', (char const )'-',
2498 (char const )'r', (char const )'e', (char const )'g', (char const )'u',
2499 (char const )'l', (char const )'a', (char const )'t', (char const )'o',
2500 (char const )'r', (char const )'\000'};
2501#line 256
2502void ldv_check_final_state(void) ;
2503#line 259
2504extern void ldv_check_return_value(int res ) ;
2505#line 262
2506extern void ldv_initialize(void) ;
2507#line 265
2508extern int __VERIFIER_nondet_int(void) ;
2509#line 268 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2510int LDV_IN_INTERRUPT ;
2511#line 286 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2512static int res_regulator_led_probe_7 ;
2513#line 271 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2514void main(void)
2515{ struct platform_device *var_group1 ;
2516 int ldv_s_regulator_led_driver_platform_driver ;
2517 int tmp ;
2518 int tmp___0 ;
2519 int __cil_tmp5 ;
2520
2521 {
2522 {
2523#line 294
2524 LDV_IN_INTERRUPT = 1;
2525#line 303
2526 ldv_initialize();
2527#line 304
2528 ldv_s_regulator_led_driver_platform_driver = 0;
2529 }
2530 {
2531#line 307
2532 while (1) {
2533 while_continue: ;
2534 {
2535#line 307
2536 tmp___0 = __VERIFIER_nondet_int();
2537 }
2538#line 307
2539 if (tmp___0) {
2540
2541 } else {
2542 {
2543#line 307
2544 __cil_tmp5 = ldv_s_regulator_led_driver_platform_driver == 0;
2545#line 307
2546 if (! __cil_tmp5) {
2547
2548 } else {
2549#line 307
2550 goto while_break;
2551 }
2552 }
2553 }
2554 {
2555#line 311
2556 tmp = __VERIFIER_nondet_int();
2557 }
2558#line 313
2559 if (tmp == 0) {
2560#line 313
2561 goto case_0;
2562 } else {
2563 {
2564#line 335
2565 goto switch_default;
2566#line 311
2567 if (0) {
2568 case_0:
2569#line 316
2570 if (ldv_s_regulator_led_driver_platform_driver == 0) {
2571 {
2572#line 324
2573 res_regulator_led_probe_7 = regulator_led_probe(var_group1);
2574#line 325
2575 ldv_check_return_value(res_regulator_led_probe_7);
2576 }
2577#line 326
2578 if (res_regulator_led_probe_7) {
2579#line 327
2580 goto ldv_module_exit;
2581 } else {
2582
2583 }
2584#line 328
2585 ldv_s_regulator_led_driver_platform_driver = 0;
2586 } else {
2587
2588 }
2589#line 334
2590 goto switch_break;
2591 switch_default:
2592#line 335
2593 goto switch_break;
2594 } else {
2595 switch_break: ;
2596 }
2597 }
2598 }
2599 }
2600 while_break: ;
2601 }
2602 ldv_module_exit:
2603 {
2604#line 344
2605 ldv_check_final_state();
2606 }
2607#line 347
2608 return;
2609}
2610}
2611#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2612void ldv_blast_assert(void)
2613{
2614
2615 {
2616 ERROR:
2617#line 6
2618 goto ERROR;
2619}
2620}
2621#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2622extern int __VERIFIER_nondet_int(void) ;
2623#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2624int ldv_mutex = 1;
2625#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2626int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
2627{ int nondetermined ;
2628
2629 {
2630#line 29
2631 if (ldv_mutex == 1) {
2632
2633 } else {
2634 {
2635#line 29
2636 ldv_blast_assert();
2637 }
2638 }
2639 {
2640#line 32
2641 nondetermined = __VERIFIER_nondet_int();
2642 }
2643#line 35
2644 if (nondetermined) {
2645#line 38
2646 ldv_mutex = 2;
2647#line 40
2648 return (0);
2649 } else {
2650#line 45
2651 return (-4);
2652 }
2653}
2654}
2655#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2656int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
2657{ int nondetermined ;
2658
2659 {
2660#line 57
2661 if (ldv_mutex == 1) {
2662
2663 } else {
2664 {
2665#line 57
2666 ldv_blast_assert();
2667 }
2668 }
2669 {
2670#line 60
2671 nondetermined = __VERIFIER_nondet_int();
2672 }
2673#line 63
2674 if (nondetermined) {
2675#line 66
2676 ldv_mutex = 2;
2677#line 68
2678 return (0);
2679 } else {
2680#line 73
2681 return (-4);
2682 }
2683}
2684}
2685#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2686int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
2687{ int atomic_value_after_dec ;
2688
2689 {
2690#line 83
2691 if (ldv_mutex == 1) {
2692
2693 } else {
2694 {
2695#line 83
2696 ldv_blast_assert();
2697 }
2698 }
2699 {
2700#line 86
2701 atomic_value_after_dec = __VERIFIER_nondet_int();
2702 }
2703#line 89
2704 if (atomic_value_after_dec == 0) {
2705#line 92
2706 ldv_mutex = 2;
2707#line 94
2708 return (1);
2709 } else {
2710
2711 }
2712#line 98
2713 return (0);
2714}
2715}
2716#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2717void mutex_lock(struct mutex *lock )
2718{
2719
2720 {
2721#line 108
2722 if (ldv_mutex == 1) {
2723
2724 } else {
2725 {
2726#line 108
2727 ldv_blast_assert();
2728 }
2729 }
2730#line 110
2731 ldv_mutex = 2;
2732#line 111
2733 return;
2734}
2735}
2736#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2737int mutex_trylock(struct mutex *lock )
2738{ int nondetermined ;
2739
2740 {
2741#line 121
2742 if (ldv_mutex == 1) {
2743
2744 } else {
2745 {
2746#line 121
2747 ldv_blast_assert();
2748 }
2749 }
2750 {
2751#line 124
2752 nondetermined = __VERIFIER_nondet_int();
2753 }
2754#line 127
2755 if (nondetermined) {
2756#line 130
2757 ldv_mutex = 2;
2758#line 132
2759 return (1);
2760 } else {
2761#line 137
2762 return (0);
2763 }
2764}
2765}
2766#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2767void mutex_unlock(struct mutex *lock )
2768{
2769
2770 {
2771#line 147
2772 if (ldv_mutex == 2) {
2773
2774 } else {
2775 {
2776#line 147
2777 ldv_blast_assert();
2778 }
2779 }
2780#line 149
2781 ldv_mutex = 1;
2782#line 150
2783 return;
2784}
2785}
2786#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2787void ldv_check_final_state(void)
2788{
2789
2790 {
2791#line 156
2792 if (ldv_mutex == 1) {
2793
2794 } else {
2795 {
2796#line 156
2797 ldv_blast_assert();
2798 }
2799 }
2800#line 157
2801 return;
2802}
2803}
2804#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-regulator.c.common.c"
2805long s__builtin_expect(long val , long res )
2806{
2807
2808 {
2809#line 357
2810 return (val);
2811}
2812}