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