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