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