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