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