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/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
732enum irqreturn {
733 IRQ_NONE = 0,
734 IRQ_HANDLED = 1,
735 IRQ_WAKE_THREAD = 2
736} ;
737#line 16 "include/linux/irqreturn.h"
738typedef enum irqreturn irqreturn_t;
739#line 348 "include/linux/irq.h"
740struct proc_dir_entry;
741#line 348
742struct proc_dir_entry;
743#line 41 "include/asm-generic/sections.h"
744struct exception_table_entry {
745 unsigned long insn ;
746 unsigned long fixup ;
747};
748#line 702 "include/linux/interrupt.h"
749struct klist_node;
750#line 702
751struct klist_node;
752#line 37 "include/linux/klist.h"
753struct klist_node {
754 void *n_klist ;
755 struct list_head n_node ;
756 struct kref n_ref ;
757};
758#line 67
759struct dma_map_ops;
760#line 67 "include/linux/klist.h"
761struct dev_archdata {
762 void *acpi_handle ;
763 struct dma_map_ops *dma_ops ;
764 void *iommu ;
765};
766#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
767struct pdev_archdata {
768
769};
770#line 17
771struct device_private;
772#line 17
773struct device_private;
774#line 18
775struct device_driver;
776#line 18
777struct device_driver;
778#line 19
779struct driver_private;
780#line 19
781struct driver_private;
782#line 20
783struct class;
784#line 20
785struct class;
786#line 21
787struct subsys_private;
788#line 21
789struct subsys_private;
790#line 22
791struct bus_type;
792#line 22
793struct bus_type;
794#line 23
795struct device_node;
796#line 23
797struct device_node;
798#line 24
799struct iommu_ops;
800#line 24
801struct iommu_ops;
802#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
803struct bus_attribute {
804 struct attribute attr ;
805 ssize_t (*show)(struct bus_type * , char * ) ;
806 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
807};
808#line 51 "include/linux/device.h"
809struct device_attribute;
810#line 51
811struct driver_attribute;
812#line 51 "include/linux/device.h"
813struct bus_type {
814 char const *name ;
815 char const *dev_name ;
816 struct device *dev_root ;
817 struct bus_attribute *bus_attrs ;
818 struct device_attribute *dev_attrs ;
819 struct driver_attribute *drv_attrs ;
820 int (*match)(struct device * , struct device_driver * ) ;
821 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
822 int (*probe)(struct device * ) ;
823 int (*remove)(struct device * ) ;
824 void (*shutdown)(struct device * ) ;
825 int (*suspend)(struct device * , pm_message_t ) ;
826 int (*resume)(struct device * ) ;
827 struct dev_pm_ops const *pm ;
828 struct iommu_ops *iommu_ops ;
829 struct subsys_private *p ;
830};
831#line 125
832struct device_type;
833#line 182
834struct of_device_id;
835#line 182 "include/linux/device.h"
836struct device_driver {
837 char const *name ;
838 struct bus_type *bus ;
839 struct module *owner ;
840 char const *mod_name ;
841 bool suppress_bind_attrs ;
842 struct of_device_id const *of_match_table ;
843 int (*probe)(struct device * ) ;
844 int (*remove)(struct device * ) ;
845 void (*shutdown)(struct device * ) ;
846 int (*suspend)(struct device * , pm_message_t ) ;
847 int (*resume)(struct device * ) ;
848 struct attribute_group const **groups ;
849 struct dev_pm_ops const *pm ;
850 struct driver_private *p ;
851};
852#line 245 "include/linux/device.h"
853struct driver_attribute {
854 struct attribute attr ;
855 ssize_t (*show)(struct device_driver * , char * ) ;
856 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
857};
858#line 299
859struct class_attribute;
860#line 299 "include/linux/device.h"
861struct class {
862 char const *name ;
863 struct module *owner ;
864 struct class_attribute *class_attrs ;
865 struct device_attribute *dev_attrs ;
866 struct bin_attribute *dev_bin_attrs ;
867 struct kobject *dev_kobj ;
868 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
869 char *(*devnode)(struct device * , umode_t * ) ;
870 void (*class_release)(struct class * ) ;
871 void (*dev_release)(struct device * ) ;
872 int (*suspend)(struct device * , pm_message_t ) ;
873 int (*resume)(struct device * ) ;
874 struct kobj_ns_type_operations const *ns_type ;
875 void const *(*namespace)(struct device * ) ;
876 struct dev_pm_ops const *pm ;
877 struct subsys_private *p ;
878};
879#line 394 "include/linux/device.h"
880struct class_attribute {
881 struct attribute attr ;
882 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
883 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
884 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
885};
886#line 447 "include/linux/device.h"
887struct device_type {
888 char const *name ;
889 struct attribute_group const **groups ;
890 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
891 char *(*devnode)(struct device * , umode_t * ) ;
892 void (*release)(struct device * ) ;
893 struct dev_pm_ops const *pm ;
894};
895#line 474 "include/linux/device.h"
896struct device_attribute {
897 struct attribute attr ;
898 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
899 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
900 size_t ) ;
901};
902#line 557 "include/linux/device.h"
903struct device_dma_parameters {
904 unsigned int max_segment_size ;
905 unsigned long segment_boundary_mask ;
906};
907#line 567
908struct dma_coherent_mem;
909#line 567 "include/linux/device.h"
910struct device {
911 struct device *parent ;
912 struct device_private *p ;
913 struct kobject kobj ;
914 char const *init_name ;
915 struct device_type const *type ;
916 struct mutex mutex ;
917 struct bus_type *bus ;
918 struct device_driver *driver ;
919 void *platform_data ;
920 struct dev_pm_info power ;
921 struct dev_pm_domain *pm_domain ;
922 int numa_node ;
923 u64 *dma_mask ;
924 u64 coherent_dma_mask ;
925 struct device_dma_parameters *dma_parms ;
926 struct list_head dma_pools ;
927 struct dma_coherent_mem *dma_mem ;
928 struct dev_archdata archdata ;
929 struct device_node *of_node ;
930 dev_t devt ;
931 u32 id ;
932 spinlock_t devres_lock ;
933 struct list_head devres_head ;
934 struct klist_node knode_class ;
935 struct class *class ;
936 struct attribute_group const **groups ;
937 void (*release)(struct device * ) ;
938};
939#line 681 "include/linux/device.h"
940struct wakeup_source {
941 char const *name ;
942 struct list_head entry ;
943 spinlock_t lock ;
944 struct timer_list timer ;
945 unsigned long timer_expires ;
946 ktime_t total_time ;
947 ktime_t max_time ;
948 ktime_t last_time ;
949 unsigned long event_count ;
950 unsigned long active_count ;
951 unsigned long relax_count ;
952 unsigned long hit_count ;
953 unsigned char active : 1 ;
954};
955#line 12 "include/linux/mod_devicetable.h"
956typedef unsigned long kernel_ulong_t;
957#line 215 "include/linux/mod_devicetable.h"
958struct of_device_id {
959 char name[32U] ;
960 char type[32U] ;
961 char compatible[128U] ;
962 void *data ;
963};
964#line 492 "include/linux/mod_devicetable.h"
965struct platform_device_id {
966 char name[20U] ;
967 kernel_ulong_t driver_data ;
968};
969#line 584
970struct mfd_cell;
971#line 584
972struct mfd_cell;
973#line 585 "include/linux/mod_devicetable.h"
974struct platform_device {
975 char const *name ;
976 int id ;
977 struct device dev ;
978 u32 num_resources ;
979 struct resource *resource ;
980 struct platform_device_id const *id_entry ;
981 struct mfd_cell *mfd_cell ;
982 struct pdev_archdata archdata ;
983};
984#line 163 "include/linux/platform_device.h"
985struct platform_driver {
986 int (*probe)(struct platform_device * ) ;
987 int (*remove)(struct platform_device * ) ;
988 void (*shutdown)(struct platform_device * ) ;
989 int (*suspend)(struct platform_device * , pm_message_t ) ;
990 int (*resume)(struct platform_device * ) ;
991 struct device_driver driver ;
992 struct platform_device_id const *id_table ;
993};
994#line 28 "include/linux/of.h"
995typedef u32 phandle;
996#line 30 "include/linux/of.h"
997struct property {
998 char *name ;
999 int length ;
1000 void *value ;
1001 struct property *next ;
1002 unsigned long _flags ;
1003 unsigned int unique_id ;
1004};
1005#line 39 "include/linux/of.h"
1006struct device_node {
1007 char const *name ;
1008 char const *type ;
1009 phandle phandle ;
1010 char *full_name ;
1011 struct property *properties ;
1012 struct property *deadprops ;
1013 struct device_node *parent ;
1014 struct device_node *child ;
1015 struct device_node *sibling ;
1016 struct device_node *next ;
1017 struct device_node *allnext ;
1018 struct proc_dir_entry *pde ;
1019 struct kref kref ;
1020 unsigned long _flags ;
1021 void *data ;
1022};
1023#line 50 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
1024struct switch_dev {
1025 char const *name ;
1026 struct device *dev ;
1027 int index ;
1028 int state ;
1029 ssize_t (*print_name)(struct switch_dev * , char * ) ;
1030 ssize_t (*print_state)(struct switch_dev * , char * ) ;
1031};
1032#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/android/switch/switch.h"
1033struct gpio_switch_platform_data {
1034 char const *name ;
1035 unsigned int gpio ;
1036 char const *name_on ;
1037 char const *name_off ;
1038 char const *state_on ;
1039 char const *state_off ;
1040};
1041#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/android/switch/switch.h"
1042struct gpio_switch_data {
1043 struct switch_dev sdev ;
1044 unsigned int gpio ;
1045 char const *name_on ;
1046 char const *name_off ;
1047 char const *state_on ;
1048 char const *state_off ;
1049 int irq ;
1050 struct work_struct work ;
1051};
1052#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1053void ldv_spin_lock(void) ;
1054#line 3
1055void ldv_spin_unlock(void) ;
1056#line 4
1057int ldv_spin_trylock(void) ;
1058#line 320 "include/linux/kernel.h"
1059extern int sprintf(char * , char const * , ...) ;
1060#line 24 "include/linux/list.h"
1061__inline static void INIT_LIST_HEAD(struct list_head *list )
1062{ unsigned long __cil_tmp2 ;
1063 unsigned long __cil_tmp3 ;
1064
1065 {
1066#line 26
1067 *((struct list_head **)list) = list;
1068#line 27
1069 __cil_tmp2 = (unsigned long )list;
1070#line 27
1071 __cil_tmp3 = __cil_tmp2 + 8;
1072#line 27
1073 *((struct list_head **)__cil_tmp3) = list;
1074#line 28
1075 return;
1076}
1077}
1078#line 261 "include/linux/lockdep.h"
1079extern void lockdep_init_map(struct lockdep_map * , char const * , struct lock_class_key * ,
1080 int ) ;
1081#line 156 "include/linux/workqueue.h"
1082extern void __init_work(struct work_struct * , int ) ;
1083#line 380
1084extern int schedule_work(struct work_struct * ) ;
1085#line 392
1086extern bool cancel_work_sync(struct work_struct * ) ;
1087#line 26 "include/linux/export.h"
1088extern struct module __this_module ;
1089#line 161 "include/linux/slab.h"
1090extern void kfree(void const * ) ;
1091#line 220 "include/linux/slub_def.h"
1092extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1093#line 223
1094void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1095#line 353 "include/linux/slab.h"
1096__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1097#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1098extern void *__VERIFIER_nondet_pointer(void) ;
1099#line 11
1100void ldv_check_alloc_flags(gfp_t flags ) ;
1101#line 12
1102void ldv_check_alloc_nonatomic(void) ;
1103#line 14
1104struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1105#line 127 "include/linux/interrupt.h"
1106extern int request_threaded_irq(unsigned int , irqreturn_t (*)(int , void * ) ,
1107 irqreturn_t (*)(int , void * ) , unsigned long ,
1108 char const * , void * ) ;
1109#line 132 "include/linux/interrupt.h"
1110__inline static int request_irq(unsigned int irq , irqreturn_t (*handler)(int , void * ) ,
1111 unsigned long flags , char const *name , void *dev )
1112{ int tmp ;
1113 irqreturn_t (*__cil_tmp7)(int , void * ) ;
1114
1115 {
1116 {
1117#line 135
1118 __cil_tmp7 = (irqreturn_t (*)(int , void * ))0;
1119#line 135
1120 tmp = request_threaded_irq(irq, handler, __cil_tmp7, flags, name, dev);
1121 }
1122#line 135
1123 return (tmp);
1124}
1125}
1126#line 792 "include/linux/device.h"
1127extern void *dev_get_drvdata(struct device const * ) ;
1128#line 174 "include/linux/platform_device.h"
1129extern int platform_driver_register(struct platform_driver * ) ;
1130#line 175
1131extern void platform_driver_unregister(struct platform_driver * ) ;
1132#line 183 "include/linux/platform_device.h"
1133__inline static void *platform_get_drvdata(struct platform_device const *pdev )
1134{ void *tmp ;
1135 unsigned long __cil_tmp3 ;
1136 unsigned long __cil_tmp4 ;
1137 struct device const *__cil_tmp5 ;
1138
1139 {
1140 {
1141#line 185
1142 __cil_tmp3 = (unsigned long )pdev;
1143#line 185
1144 __cil_tmp4 = __cil_tmp3 + 16;
1145#line 185
1146 __cil_tmp5 = (struct device const *)__cil_tmp4;
1147#line 185
1148 tmp = dev_get_drvdata(__cil_tmp5);
1149 }
1150#line 185
1151 return (tmp);
1152}
1153}
1154#line 153 "include/asm-generic/gpio.h"
1155extern int gpio_request(unsigned int , char const * ) ;
1156#line 154
1157extern void gpio_free(unsigned int ) ;
1158#line 156
1159extern int gpio_direction_input(unsigned int ) ;
1160#line 169
1161extern int __gpio_get_value(unsigned int ) ;
1162#line 174
1163extern int __gpio_to_irq(unsigned int ) ;
1164#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
1165__inline static int gpio_get_value(unsigned int gpio )
1166{ int tmp ;
1167
1168 {
1169 {
1170#line 28
1171 tmp = __gpio_get_value(gpio);
1172 }
1173#line 28
1174 return (tmp);
1175}
1176}
1177#line 41 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
1178__inline static int gpio_to_irq(unsigned int gpio )
1179{ int tmp ;
1180
1181 {
1182 {
1183#line 43
1184 tmp = __gpio_to_irq(gpio);
1185 }
1186#line 43
1187 return (tmp);
1188}
1189}
1190#line 43 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/android/switch/switch.h"
1191extern int switch_dev_register(struct switch_dev * ) ;
1192#line 44
1193extern void switch_dev_unregister(struct switch_dev * ) ;
1194#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/android/switch/switch.h"
1195__inline static int switch_get_state(struct switch_dev *sdev )
1196{ unsigned long __cil_tmp2 ;
1197 unsigned long __cil_tmp3 ;
1198
1199 {
1200 {
1201#line 48
1202 __cil_tmp2 = (unsigned long )sdev;
1203#line 48
1204 __cil_tmp3 = __cil_tmp2 + 20;
1205#line 48
1206 return (*((int *)__cil_tmp3));
1207 }
1208}
1209}
1210#line 51
1211extern void switch_set_state(struct switch_dev * , int ) ;
1212#line 54 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1213static void gpio_switch_work(struct work_struct *work )
1214{ int state ;
1215 struct gpio_switch_data *data ;
1216 struct work_struct const *__mptr ;
1217 struct gpio_switch_data *__cil_tmp5 ;
1218 unsigned long __cil_tmp6 ;
1219 unsigned long __cil_tmp7 ;
1220 unsigned int __cil_tmp8 ;
1221 struct switch_dev *__cil_tmp9 ;
1222
1223 {
1224 {
1225#line 58
1226 __mptr = (struct work_struct const *)work;
1227#line 58
1228 __cil_tmp5 = (struct gpio_switch_data *)__mptr;
1229#line 58
1230 data = __cil_tmp5 + 0xffffffffffffffa8UL;
1231#line 60
1232 __cil_tmp6 = (unsigned long )data;
1233#line 60
1234 __cil_tmp7 = __cil_tmp6 + 40;
1235#line 60
1236 __cil_tmp8 = *((unsigned int *)__cil_tmp7);
1237#line 60
1238 state = gpio_get_value(__cil_tmp8);
1239#line 61
1240 __cil_tmp9 = (struct switch_dev *)data;
1241#line 61
1242 switch_set_state(__cil_tmp9, state);
1243 }
1244#line 62
1245 return;
1246}
1247}
1248#line 64 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1249static irqreturn_t gpio_irq_handler(int irq , void *dev_id )
1250{ struct gpio_switch_data *switch_data ;
1251 unsigned long __cil_tmp4 ;
1252 unsigned long __cil_tmp5 ;
1253 struct work_struct *__cil_tmp6 ;
1254
1255 {
1256 {
1257#line 66
1258 switch_data = (struct gpio_switch_data *)dev_id;
1259#line 69
1260 __cil_tmp4 = (unsigned long )switch_data;
1261#line 69
1262 __cil_tmp5 = __cil_tmp4 + 88;
1263#line 69
1264 __cil_tmp6 = (struct work_struct *)__cil_tmp5;
1265#line 69
1266 schedule_work(__cil_tmp6);
1267 }
1268#line 70
1269 return ((irqreturn_t )1);
1270}
1271}
1272#line 73 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1273static ssize_t switch_gpio_print_state(struct switch_dev *sdev , char *buf )
1274{ struct gpio_switch_data *switch_data ;
1275 struct switch_dev const *__mptr ;
1276 char const *state ;
1277 int tmp ;
1278 int tmp___0 ;
1279 unsigned long __cil_tmp8 ;
1280 unsigned long __cil_tmp9 ;
1281 unsigned long __cil_tmp10 ;
1282 unsigned long __cil_tmp11 ;
1283 char const *__cil_tmp12 ;
1284 unsigned long __cil_tmp13 ;
1285 unsigned long __cil_tmp14 ;
1286
1287 {
1288 {
1289#line 76
1290 __mptr = (struct switch_dev const *)sdev;
1291#line 76
1292 switch_data = (struct gpio_switch_data *)__mptr;
1293#line 78
1294 tmp = switch_get_state(sdev);
1295 }
1296#line 78
1297 if (tmp != 0) {
1298#line 79
1299 __cil_tmp8 = (unsigned long )switch_data;
1300#line 79
1301 __cil_tmp9 = __cil_tmp8 + 64;
1302#line 79
1303 state = *((char const **)__cil_tmp9);
1304 } else {
1305#line 81
1306 __cil_tmp10 = (unsigned long )switch_data;
1307#line 81
1308 __cil_tmp11 = __cil_tmp10 + 72;
1309#line 81
1310 state = *((char const **)__cil_tmp11);
1311 }
1312 {
1313#line 83
1314 __cil_tmp12 = (char const *)0;
1315#line 83
1316 __cil_tmp13 = (unsigned long )__cil_tmp12;
1317#line 83
1318 __cil_tmp14 = (unsigned long )state;
1319#line 83
1320 if (__cil_tmp14 != __cil_tmp13) {
1321 {
1322#line 84
1323 tmp___0 = sprintf(buf, "%s\n", state);
1324 }
1325#line 84
1326 return ((ssize_t )tmp___0);
1327 } else {
1328
1329 }
1330 }
1331#line 85
1332 return (-1L);
1333}
1334}
1335#line 88 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1336static int gpio_switch_probe(struct platform_device *pdev )
1337{ struct gpio_switch_platform_data *pdata ;
1338 struct gpio_switch_data *switch_data ;
1339 int ret ;
1340 void *tmp ;
1341 struct lock_class_key __key ;
1342 atomic_long_t __constr_expr_0 ;
1343 unsigned long __cil_tmp8 ;
1344 unsigned long __cil_tmp9 ;
1345 unsigned long __cil_tmp10 ;
1346 void *__cil_tmp11 ;
1347 struct gpio_switch_platform_data *__cil_tmp12 ;
1348 unsigned long __cil_tmp13 ;
1349 unsigned long __cil_tmp14 ;
1350 struct gpio_switch_data *__cil_tmp15 ;
1351 unsigned long __cil_tmp16 ;
1352 unsigned long __cil_tmp17 ;
1353 unsigned long __cil_tmp18 ;
1354 unsigned long __cil_tmp19 ;
1355 unsigned long __cil_tmp20 ;
1356 unsigned long __cil_tmp21 ;
1357 unsigned long __cil_tmp22 ;
1358 unsigned long __cil_tmp23 ;
1359 unsigned long __cil_tmp24 ;
1360 unsigned long __cil_tmp25 ;
1361 unsigned long __cil_tmp26 ;
1362 unsigned long __cil_tmp27 ;
1363 unsigned long __cil_tmp28 ;
1364 unsigned long __cil_tmp29 ;
1365 unsigned long __cil_tmp30 ;
1366 unsigned long __cil_tmp31 ;
1367 unsigned long __cil_tmp32 ;
1368 unsigned long __cil_tmp33 ;
1369 unsigned long __cil_tmp34 ;
1370 unsigned long __cil_tmp35 ;
1371 unsigned long __cil_tmp36 ;
1372 unsigned long __cil_tmp37 ;
1373 unsigned long __cil_tmp38 ;
1374 unsigned long __cil_tmp39 ;
1375 unsigned long __cil_tmp40 ;
1376 struct switch_dev *__cil_tmp41 ;
1377 unsigned long __cil_tmp42 ;
1378 unsigned long __cil_tmp43 ;
1379 unsigned int __cil_tmp44 ;
1380 char const *__cil_tmp45 ;
1381 unsigned long __cil_tmp46 ;
1382 unsigned long __cil_tmp47 ;
1383 unsigned int __cil_tmp48 ;
1384 unsigned long __cil_tmp49 ;
1385 unsigned long __cil_tmp50 ;
1386 struct work_struct *__cil_tmp51 ;
1387 unsigned long __cil_tmp52 ;
1388 unsigned long __cil_tmp53 ;
1389 unsigned long __cil_tmp54 ;
1390 unsigned long __cil_tmp55 ;
1391 unsigned long __cil_tmp56 ;
1392 struct lockdep_map *__cil_tmp57 ;
1393 unsigned long __cil_tmp58 ;
1394 unsigned long __cil_tmp59 ;
1395 unsigned long __cil_tmp60 ;
1396 struct list_head *__cil_tmp61 ;
1397 unsigned long __cil_tmp62 ;
1398 unsigned long __cil_tmp63 ;
1399 unsigned long __cil_tmp64 ;
1400 unsigned long __cil_tmp65 ;
1401 unsigned long __cil_tmp66 ;
1402 unsigned long __cil_tmp67 ;
1403 unsigned long __cil_tmp68 ;
1404 unsigned int __cil_tmp69 ;
1405 unsigned long __cil_tmp70 ;
1406 unsigned long __cil_tmp71 ;
1407 int __cil_tmp72 ;
1408 unsigned long __cil_tmp73 ;
1409 unsigned long __cil_tmp74 ;
1410 unsigned long __cil_tmp75 ;
1411 unsigned long __cil_tmp76 ;
1412 int __cil_tmp77 ;
1413 unsigned int __cil_tmp78 ;
1414 char const *__cil_tmp79 ;
1415 void *__cil_tmp80 ;
1416 unsigned long __cil_tmp81 ;
1417 unsigned long __cil_tmp82 ;
1418 struct work_struct *__cil_tmp83 ;
1419 unsigned long __cil_tmp84 ;
1420 unsigned long __cil_tmp85 ;
1421 unsigned int __cil_tmp86 ;
1422 struct switch_dev *__cil_tmp87 ;
1423 void const *__cil_tmp88 ;
1424 long __constr_expr_0_counter89 ;
1425
1426 {
1427#line 90
1428 __cil_tmp8 = 16 + 280;
1429#line 90
1430 __cil_tmp9 = (unsigned long )pdev;
1431#line 90
1432 __cil_tmp10 = __cil_tmp9 + __cil_tmp8;
1433#line 90
1434 __cil_tmp11 = *((void **)__cil_tmp10);
1435#line 90
1436 pdata = (struct gpio_switch_platform_data *)__cil_tmp11;
1437#line 92
1438 ret = 0;
1439 {
1440#line 94
1441 __cil_tmp12 = (struct gpio_switch_platform_data *)0;
1442#line 94
1443 __cil_tmp13 = (unsigned long )__cil_tmp12;
1444#line 94
1445 __cil_tmp14 = (unsigned long )pdata;
1446#line 94
1447 if (__cil_tmp14 == __cil_tmp13) {
1448#line 95
1449 return (-16);
1450 } else {
1451
1452 }
1453 }
1454 {
1455#line 97
1456 tmp = kzalloc(168UL, 208U);
1457#line 97
1458 switch_data = (struct gpio_switch_data *)tmp;
1459 }
1460 {
1461#line 98
1462 __cil_tmp15 = (struct gpio_switch_data *)0;
1463#line 98
1464 __cil_tmp16 = (unsigned long )__cil_tmp15;
1465#line 98
1466 __cil_tmp17 = (unsigned long )switch_data;
1467#line 98
1468 if (__cil_tmp17 == __cil_tmp16) {
1469#line 99
1470 return (-12);
1471 } else {
1472
1473 }
1474 }
1475 {
1476#line 101
1477 *((char const **)switch_data) = *((char const **)pdata);
1478#line 102
1479 __cil_tmp18 = (unsigned long )switch_data;
1480#line 102
1481 __cil_tmp19 = __cil_tmp18 + 40;
1482#line 102
1483 __cil_tmp20 = (unsigned long )pdata;
1484#line 102
1485 __cil_tmp21 = __cil_tmp20 + 8;
1486#line 102
1487 *((unsigned int *)__cil_tmp19) = *((unsigned int *)__cil_tmp21);
1488#line 103
1489 __cil_tmp22 = (unsigned long )switch_data;
1490#line 103
1491 __cil_tmp23 = __cil_tmp22 + 48;
1492#line 103
1493 __cil_tmp24 = (unsigned long )pdata;
1494#line 103
1495 __cil_tmp25 = __cil_tmp24 + 16;
1496#line 103
1497 *((char const **)__cil_tmp23) = *((char const **)__cil_tmp25);
1498#line 104
1499 __cil_tmp26 = (unsigned long )switch_data;
1500#line 104
1501 __cil_tmp27 = __cil_tmp26 + 56;
1502#line 104
1503 __cil_tmp28 = (unsigned long )pdata;
1504#line 104
1505 __cil_tmp29 = __cil_tmp28 + 24;
1506#line 104
1507 *((char const **)__cil_tmp27) = *((char const **)__cil_tmp29);
1508#line 105
1509 __cil_tmp30 = (unsigned long )switch_data;
1510#line 105
1511 __cil_tmp31 = __cil_tmp30 + 64;
1512#line 105
1513 __cil_tmp32 = (unsigned long )pdata;
1514#line 105
1515 __cil_tmp33 = __cil_tmp32 + 32;
1516#line 105
1517 *((char const **)__cil_tmp31) = *((char const **)__cil_tmp33);
1518#line 106
1519 __cil_tmp34 = (unsigned long )switch_data;
1520#line 106
1521 __cil_tmp35 = __cil_tmp34 + 72;
1522#line 106
1523 __cil_tmp36 = (unsigned long )pdata;
1524#line 106
1525 __cil_tmp37 = __cil_tmp36 + 40;
1526#line 106
1527 *((char const **)__cil_tmp35) = *((char const **)__cil_tmp37);
1528#line 107
1529 __cil_tmp38 = 0 + 32;
1530#line 107
1531 __cil_tmp39 = (unsigned long )switch_data;
1532#line 107
1533 __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
1534#line 107
1535 *((ssize_t (**)(struct switch_dev * , char * ))__cil_tmp40) = & switch_gpio_print_state;
1536#line 109
1537 __cil_tmp41 = (struct switch_dev *)switch_data;
1538#line 109
1539 ret = switch_dev_register(__cil_tmp41);
1540 }
1541#line 110
1542 if (ret < 0) {
1543#line 111
1544 goto err_switch_dev_register;
1545 } else {
1546
1547 }
1548 {
1549#line 113
1550 __cil_tmp42 = (unsigned long )switch_data;
1551#line 113
1552 __cil_tmp43 = __cil_tmp42 + 40;
1553#line 113
1554 __cil_tmp44 = *((unsigned int *)__cil_tmp43);
1555#line 113
1556 __cil_tmp45 = *((char const **)pdev);
1557#line 113
1558 ret = gpio_request(__cil_tmp44, __cil_tmp45);
1559 }
1560#line 114
1561 if (ret < 0) {
1562#line 115
1563 goto err_request_gpio;
1564 } else {
1565
1566 }
1567 {
1568#line 117
1569 __cil_tmp46 = (unsigned long )switch_data;
1570#line 117
1571 __cil_tmp47 = __cil_tmp46 + 40;
1572#line 117
1573 __cil_tmp48 = *((unsigned int *)__cil_tmp47);
1574#line 117
1575 ret = gpio_direction_input(__cil_tmp48);
1576 }
1577#line 118
1578 if (ret < 0) {
1579#line 119
1580 goto err_set_gpio_input;
1581 } else {
1582
1583 }
1584 {
1585#line 121
1586 __cil_tmp49 = (unsigned long )switch_data;
1587#line 121
1588 __cil_tmp50 = __cil_tmp49 + 88;
1589#line 121
1590 __cil_tmp51 = (struct work_struct *)__cil_tmp50;
1591#line 121
1592 __init_work(__cil_tmp51, 0);
1593#line 121
1594 __constr_expr_0_counter89 = 2097664L;
1595#line 121
1596 __cil_tmp52 = (unsigned long )switch_data;
1597#line 121
1598 __cil_tmp53 = __cil_tmp52 + 88;
1599#line 121
1600 ((atomic_long_t *)__cil_tmp53)->counter = __constr_expr_0_counter89;
1601#line 121
1602 __cil_tmp54 = 88 + 32;
1603#line 121
1604 __cil_tmp55 = (unsigned long )switch_data;
1605#line 121
1606 __cil_tmp56 = __cil_tmp55 + __cil_tmp54;
1607#line 121
1608 __cil_tmp57 = (struct lockdep_map *)__cil_tmp56;
1609#line 121
1610 lockdep_init_map(__cil_tmp57, "(&switch_data->work)", & __key, 0);
1611#line 121
1612 __cil_tmp58 = 88 + 8;
1613#line 121
1614 __cil_tmp59 = (unsigned long )switch_data;
1615#line 121
1616 __cil_tmp60 = __cil_tmp59 + __cil_tmp58;
1617#line 121
1618 __cil_tmp61 = (struct list_head *)__cil_tmp60;
1619#line 121
1620 INIT_LIST_HEAD(__cil_tmp61);
1621#line 121
1622 __cil_tmp62 = 88 + 24;
1623#line 121
1624 __cil_tmp63 = (unsigned long )switch_data;
1625#line 121
1626 __cil_tmp64 = __cil_tmp63 + __cil_tmp62;
1627#line 121
1628 *((void (**)(struct work_struct * ))__cil_tmp64) = & gpio_switch_work;
1629#line 123
1630 __cil_tmp65 = (unsigned long )switch_data;
1631#line 123
1632 __cil_tmp66 = __cil_tmp65 + 80;
1633#line 123
1634 __cil_tmp67 = (unsigned long )switch_data;
1635#line 123
1636 __cil_tmp68 = __cil_tmp67 + 40;
1637#line 123
1638 __cil_tmp69 = *((unsigned int *)__cil_tmp68);
1639#line 123
1640 *((int *)__cil_tmp66) = gpio_to_irq(__cil_tmp69);
1641 }
1642 {
1643#line 124
1644 __cil_tmp70 = (unsigned long )switch_data;
1645#line 124
1646 __cil_tmp71 = __cil_tmp70 + 80;
1647#line 124
1648 __cil_tmp72 = *((int *)__cil_tmp71);
1649#line 124
1650 if (__cil_tmp72 < 0) {
1651#line 125
1652 __cil_tmp73 = (unsigned long )switch_data;
1653#line 125
1654 __cil_tmp74 = __cil_tmp73 + 80;
1655#line 125
1656 ret = *((int *)__cil_tmp74);
1657#line 126
1658 goto err_detect_irq_num_failed;
1659 } else {
1660
1661 }
1662 }
1663 {
1664#line 129
1665 __cil_tmp75 = (unsigned long )switch_data;
1666#line 129
1667 __cil_tmp76 = __cil_tmp75 + 80;
1668#line 129
1669 __cil_tmp77 = *((int *)__cil_tmp76);
1670#line 129
1671 __cil_tmp78 = (unsigned int )__cil_tmp77;
1672#line 129
1673 __cil_tmp79 = *((char const **)pdev);
1674#line 129
1675 __cil_tmp80 = (void *)switch_data;
1676#line 129
1677 ret = request_irq(__cil_tmp78, & gpio_irq_handler, 8UL, __cil_tmp79, __cil_tmp80);
1678 }
1679#line 131
1680 if (ret < 0) {
1681#line 132
1682 goto err_request_irq;
1683 } else {
1684
1685 }
1686 {
1687#line 135
1688 __cil_tmp81 = (unsigned long )switch_data;
1689#line 135
1690 __cil_tmp82 = __cil_tmp81 + 88;
1691#line 135
1692 __cil_tmp83 = (struct work_struct *)__cil_tmp82;
1693#line 135
1694 gpio_switch_work(__cil_tmp83);
1695 }
1696#line 137
1697 return (0);
1698 err_request_irq: ;
1699 err_detect_irq_num_failed: ;
1700 err_set_gpio_input:
1701 {
1702#line 142
1703 __cil_tmp84 = (unsigned long )switch_data;
1704#line 142
1705 __cil_tmp85 = __cil_tmp84 + 40;
1706#line 142
1707 __cil_tmp86 = *((unsigned int *)__cil_tmp85);
1708#line 142
1709 gpio_free(__cil_tmp86);
1710 }
1711 err_request_gpio:
1712 {
1713#line 144
1714 __cil_tmp87 = (struct switch_dev *)switch_data;
1715#line 144
1716 switch_dev_unregister(__cil_tmp87);
1717 }
1718 err_switch_dev_register:
1719 {
1720#line 146
1721 __cil_tmp88 = (void const *)switch_data;
1722#line 146
1723 kfree(__cil_tmp88);
1724 }
1725#line 148
1726 return (ret);
1727}
1728}
1729#line 151 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1730static int gpio_switch_remove(struct platform_device *pdev )
1731{ struct gpio_switch_data *switch_data ;
1732 void *tmp ;
1733 struct platform_device const *__cil_tmp4 ;
1734 unsigned long __cil_tmp5 ;
1735 unsigned long __cil_tmp6 ;
1736 struct work_struct *__cil_tmp7 ;
1737 unsigned long __cil_tmp8 ;
1738 unsigned long __cil_tmp9 ;
1739 unsigned int __cil_tmp10 ;
1740 struct switch_dev *__cil_tmp11 ;
1741 void const *__cil_tmp12 ;
1742
1743 {
1744 {
1745#line 153
1746 __cil_tmp4 = (struct platform_device const *)pdev;
1747#line 153
1748 tmp = platform_get_drvdata(__cil_tmp4);
1749#line 153
1750 switch_data = (struct gpio_switch_data *)tmp;
1751#line 155
1752 __cil_tmp5 = (unsigned long )switch_data;
1753#line 155
1754 __cil_tmp6 = __cil_tmp5 + 88;
1755#line 155
1756 __cil_tmp7 = (struct work_struct *)__cil_tmp6;
1757#line 155
1758 cancel_work_sync(__cil_tmp7);
1759#line 156
1760 __cil_tmp8 = (unsigned long )switch_data;
1761#line 156
1762 __cil_tmp9 = __cil_tmp8 + 40;
1763#line 156
1764 __cil_tmp10 = *((unsigned int *)__cil_tmp9);
1765#line 156
1766 gpio_free(__cil_tmp10);
1767#line 157
1768 __cil_tmp11 = (struct switch_dev *)switch_data;
1769#line 157
1770 switch_dev_unregister(__cil_tmp11);
1771#line 158
1772 __cil_tmp12 = (void const *)switch_data;
1773#line 158
1774 kfree(__cil_tmp12);
1775 }
1776#line 160
1777 return (0);
1778}
1779}
1780#line 163 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1781static struct platform_driver gpio_switch_driver = {& gpio_switch_probe, & gpio_switch_remove, (void (*)(struct platform_device * ))0,
1782 (int (*)(struct platform_device * , pm_message_t ))0, (int (*)(struct platform_device * ))0,
1783 {"switch-gpio", (struct bus_type *)0, & __this_module, (char const *)0, (_Bool)0,
1784 (struct of_device_id const *)0, (int (*)(struct device * ))0, (int (*)(struct device * ))0,
1785 (void (*)(struct device * ))0, (int (*)(struct device * , pm_message_t ))0,
1786 (int (*)(struct device * ))0, (struct attribute_group const **)0, (struct dev_pm_ops const *)0,
1787 (struct driver_private *)0}, (struct platform_device_id const *)0};
1788#line 172 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1789static int gpio_switch_init(void)
1790{ int tmp ;
1791
1792 {
1793 {
1794#line 174
1795 tmp = platform_driver_register(& gpio_switch_driver);
1796 }
1797#line 174
1798 return (tmp);
1799}
1800}
1801#line 177 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1802static void gpio_switch_exit(void)
1803{
1804
1805 {
1806 {
1807#line 179
1808 platform_driver_unregister(& gpio_switch_driver);
1809 }
1810#line 180
1811 return;
1812}
1813}
1814#line 205
1815extern void ldv_check_final_state(void) ;
1816#line 208
1817extern void ldv_check_return_value(int ) ;
1818#line 211
1819extern void ldv_initialize(void) ;
1820#line 214
1821extern int __VERIFIER_nondet_int(void) ;
1822#line 217 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1823int LDV_IN_INTERRUPT ;
1824#line 220 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1825void main(void)
1826{ struct platform_device *var_group1 ;
1827 int res_gpio_switch_probe_3 ;
1828 int var_gpio_irq_handler_1_p0 ;
1829 void *var_gpio_irq_handler_1_p1 ;
1830 int ldv_s_gpio_switch_driver_platform_driver ;
1831 int tmp ;
1832 int tmp___0 ;
1833 int tmp___1 ;
1834
1835 {
1836 {
1837#line 265
1838 ldv_s_gpio_switch_driver_platform_driver = 0;
1839#line 248
1840 LDV_IN_INTERRUPT = 1;
1841#line 257
1842 ldv_initialize();
1843#line 263
1844 tmp = gpio_switch_init();
1845 }
1846#line 263
1847 if (tmp != 0) {
1848#line 264
1849 goto ldv_final;
1850 } else {
1851
1852 }
1853#line 270
1854 goto ldv_17224;
1855 ldv_17223:
1856 {
1857#line 274
1858 tmp___0 = __VERIFIER_nondet_int();
1859 }
1860#line 276
1861 if (tmp___0 == 0) {
1862#line 276
1863 goto case_0;
1864 } else
1865#line 295
1866 if (tmp___0 == 1) {
1867#line 295
1868 goto case_1;
1869 } else {
1870 {
1871#line 311
1872 goto switch_default;
1873#line 274
1874 if (0) {
1875 case_0: ;
1876#line 279
1877 if (ldv_s_gpio_switch_driver_platform_driver == 0) {
1878 {
1879#line 284
1880 res_gpio_switch_probe_3 = gpio_switch_probe(var_group1);
1881#line 285
1882 ldv_check_return_value(res_gpio_switch_probe_3);
1883 }
1884#line 286
1885 if (res_gpio_switch_probe_3 != 0) {
1886#line 287
1887 goto ldv_module_exit;
1888 } else {
1889
1890 }
1891#line 288
1892 ldv_s_gpio_switch_driver_platform_driver = 0;
1893 } else {
1894
1895 }
1896#line 294
1897 goto ldv_17220;
1898 case_1:
1899 {
1900#line 298
1901 LDV_IN_INTERRUPT = 2;
1902#line 303
1903 gpio_irq_handler(var_gpio_irq_handler_1_p0, var_gpio_irq_handler_1_p1);
1904#line 304
1905 LDV_IN_INTERRUPT = 1;
1906 }
1907#line 310
1908 goto ldv_17220;
1909 switch_default: ;
1910#line 311
1911 goto ldv_17220;
1912 } else {
1913 switch_break: ;
1914 }
1915 }
1916 }
1917 ldv_17220: ;
1918 ldv_17224:
1919 {
1920#line 270
1921 tmp___1 = __VERIFIER_nondet_int();
1922 }
1923#line 270
1924 if (tmp___1 != 0) {
1925#line 272
1926 goto ldv_17223;
1927 } else
1928#line 270
1929 if (ldv_s_gpio_switch_driver_platform_driver != 0) {
1930#line 272
1931 goto ldv_17223;
1932 } else {
1933#line 274
1934 goto ldv_17225;
1935 }
1936 ldv_17225: ;
1937 ldv_module_exit:
1938 {
1939#line 323
1940 gpio_switch_exit();
1941 }
1942 ldv_final:
1943 {
1944#line 326
1945 ldv_check_final_state();
1946 }
1947#line 329
1948 return;
1949}
1950}
1951#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1952void ldv_blast_assert(void)
1953{
1954
1955 {
1956 ERROR: ;
1957#line 6
1958 goto ERROR;
1959}
1960}
1961#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1962extern int __VERIFIER_nondet_int(void) ;
1963#line 350 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1964int ldv_spin = 0;
1965#line 354 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1966void ldv_check_alloc_flags(gfp_t flags )
1967{
1968
1969 {
1970#line 357
1971 if (ldv_spin != 0) {
1972#line 357
1973 if (flags != 32U) {
1974 {
1975#line 357
1976 ldv_blast_assert();
1977 }
1978 } else {
1979
1980 }
1981 } else {
1982
1983 }
1984#line 360
1985 return;
1986}
1987}
1988#line 360
1989extern struct page *ldv_some_page(void) ;
1990#line 363 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
1991struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
1992{ struct page *tmp ;
1993
1994 {
1995#line 366
1996 if (ldv_spin != 0) {
1997#line 366
1998 if (flags != 32U) {
1999 {
2000#line 366
2001 ldv_blast_assert();
2002 }
2003 } else {
2004
2005 }
2006 } else {
2007
2008 }
2009 {
2010#line 368
2011 tmp = ldv_some_page();
2012 }
2013#line 368
2014 return (tmp);
2015}
2016}
2017#line 372 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
2018void ldv_check_alloc_nonatomic(void)
2019{
2020
2021 {
2022#line 375
2023 if (ldv_spin != 0) {
2024 {
2025#line 375
2026 ldv_blast_assert();
2027 }
2028 } else {
2029
2030 }
2031#line 378
2032 return;
2033}
2034}
2035#line 379 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
2036void ldv_spin_lock(void)
2037{
2038
2039 {
2040#line 382
2041 ldv_spin = 1;
2042#line 383
2043 return;
2044}
2045}
2046#line 386 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
2047void ldv_spin_unlock(void)
2048{
2049
2050 {
2051#line 389
2052 ldv_spin = 0;
2053#line 390
2054 return;
2055}
2056}
2057#line 393 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
2058int ldv_spin_trylock(void)
2059{ int is_lock ;
2060
2061 {
2062 {
2063#line 398
2064 is_lock = __VERIFIER_nondet_int();
2065 }
2066#line 400
2067 if (is_lock != 0) {
2068#line 403
2069 return (0);
2070 } else {
2071#line 408
2072 ldv_spin = 1;
2073#line 410
2074 return (1);
2075 }
2076}
2077}
2078#line 577 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
2079void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
2080{
2081
2082 {
2083 {
2084#line 583
2085 ldv_check_alloc_flags(ldv_func_arg2);
2086#line 585
2087 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2088 }
2089#line 586
2090 return ((void *)0);
2091}
2092}
2093#line 588 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5575/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_gpio.c.p"
2094__inline static void *kzalloc(size_t size , gfp_t flags )
2095{ void *tmp ;
2096
2097 {
2098 {
2099#line 594
2100 ldv_check_alloc_flags(flags);
2101#line 595
2102 tmp = __VERIFIER_nondet_pointer();
2103 }
2104#line 595
2105 return (tmp);
2106}
2107}