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