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