1
2
3
4#line 19 "include/asm-generic/int-ll64.h"
5typedef signed char __s8;
6#line 20 "include/asm-generic/int-ll64.h"
7typedef unsigned char __u8;
8#line 22 "include/asm-generic/int-ll64.h"
9typedef short __s16;
10#line 23 "include/asm-generic/int-ll64.h"
11typedef unsigned short __u16;
12#line 25 "include/asm-generic/int-ll64.h"
13typedef int __s32;
14#line 26 "include/asm-generic/int-ll64.h"
15typedef unsigned int __u32;
16#line 30 "include/asm-generic/int-ll64.h"
17typedef unsigned long long __u64;
18#line 43 "include/asm-generic/int-ll64.h"
19typedef unsigned char u8;
20#line 45 "include/asm-generic/int-ll64.h"
21typedef short s16;
22#line 46 "include/asm-generic/int-ll64.h"
23typedef unsigned short u16;
24#line 48 "include/asm-generic/int-ll64.h"
25typedef int s32;
26#line 49 "include/asm-generic/int-ll64.h"
27typedef unsigned int u32;
28#line 51 "include/asm-generic/int-ll64.h"
29typedef long long s64;
30#line 52 "include/asm-generic/int-ll64.h"
31typedef unsigned long long u64;
32#line 14 "include/asm-generic/posix_types.h"
33typedef long __kernel_long_t;
34#line 15 "include/asm-generic/posix_types.h"
35typedef unsigned long __kernel_ulong_t;
36#line 52 "include/asm-generic/posix_types.h"
37typedef unsigned int __kernel_uid32_t;
38#line 53 "include/asm-generic/posix_types.h"
39typedef unsigned int __kernel_gid32_t;
40#line 75 "include/asm-generic/posix_types.h"
41typedef __kernel_ulong_t __kernel_size_t;
42#line 76 "include/asm-generic/posix_types.h"
43typedef __kernel_long_t __kernel_ssize_t;
44#line 91 "include/asm-generic/posix_types.h"
45typedef long long __kernel_loff_t;
46#line 92 "include/asm-generic/posix_types.h"
47typedef __kernel_long_t __kernel_time_t;
48#line 21 "include/linux/types.h"
49typedef __u32 __kernel_dev_t;
50#line 24 "include/linux/types.h"
51typedef __kernel_dev_t dev_t;
52#line 27 "include/linux/types.h"
53typedef unsigned short umode_t;
54#line 38 "include/linux/types.h"
55typedef _Bool bool;
56#line 40 "include/linux/types.h"
57typedef __kernel_uid32_t uid_t;
58#line 41 "include/linux/types.h"
59typedef __kernel_gid32_t gid_t;
60#line 54 "include/linux/types.h"
61typedef __kernel_loff_t loff_t;
62#line 63 "include/linux/types.h"
63typedef __kernel_size_t size_t;
64#line 68 "include/linux/types.h"
65typedef __kernel_ssize_t ssize_t;
66#line 78 "include/linux/types.h"
67typedef __kernel_time_t time_t;
68#line 142 "include/linux/types.h"
69typedef unsigned long sector_t;
70#line 143 "include/linux/types.h"
71typedef unsigned long blkcnt_t;
72#line 155 "include/linux/types.h"
73typedef u64 dma_addr_t;
74#line 202 "include/linux/types.h"
75typedef unsigned int gfp_t;
76#line 203 "include/linux/types.h"
77typedef unsigned int fmode_t;
78#line 206 "include/linux/types.h"
79typedef u64 phys_addr_t;
80#line 211 "include/linux/types.h"
81typedef phys_addr_t resource_size_t;
82#line 221 "include/linux/types.h"
83struct __anonstruct_atomic_t_6 {
84 int counter ;
85};
86#line 221 "include/linux/types.h"
87typedef struct __anonstruct_atomic_t_6 atomic_t;
88#line 226 "include/linux/types.h"
89struct __anonstruct_atomic64_t_7 {
90 long counter ;
91};
92#line 226 "include/linux/types.h"
93typedef struct __anonstruct_atomic64_t_7 atomic64_t;
94#line 227 "include/linux/types.h"
95struct list_head {
96 struct list_head *next ;
97 struct list_head *prev ;
98};
99#line 232
100struct hlist_node;
101#line 232 "include/linux/types.h"
102struct hlist_head {
103 struct hlist_node *first ;
104};
105#line 236 "include/linux/types.h"
106struct hlist_node {
107 struct hlist_node *next ;
108 struct hlist_node **pprev ;
109};
110#line 247 "include/linux/types.h"
111struct rcu_head {
112 struct rcu_head *next ;
113 void (*func)(struct rcu_head * ) ;
114};
115#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
116struct module;
117#line 55
118struct module;
119#line 146 "include/linux/init.h"
120typedef void (*ctor_fn_t)(void);
121#line 46 "include/linux/dynamic_debug.h"
122struct device;
123#line 46
124struct device;
125#line 57
126struct completion;
127#line 57
128struct completion;
129#line 348 "include/linux/kernel.h"
130struct pid;
131#line 348
132struct pid;
133#line 112 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/stat.h"
134struct timespec;
135#line 112
136struct timespec;
137#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
138struct page;
139#line 58
140struct page;
141#line 26 "include/asm-generic/getorder.h"
142struct task_struct;
143#line 26
144struct task_struct;
145#line 28
146struct mm_struct;
147#line 28
148struct mm_struct;
149#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
150typedef unsigned long pgdval_t;
151#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
152typedef unsigned long pgprotval_t;
153#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
154struct pgprot {
155 pgprotval_t pgprot ;
156};
157#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
158typedef struct pgprot pgprot_t;
159#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
160struct __anonstruct_pgd_t_16 {
161 pgdval_t pgd ;
162};
163#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
164typedef struct __anonstruct_pgd_t_16 pgd_t;
165#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
166typedef struct page *pgtable_t;
167#line 290
168struct file;
169#line 290
170struct file;
171#line 305
172struct seq_file;
173#line 305
174struct seq_file;
175#line 339
176struct cpumask;
177#line 339
178struct cpumask;
179#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
180struct arch_spinlock;
181#line 327
182struct arch_spinlock;
183#line 306 "include/linux/bitmap.h"
184struct bug_entry {
185 int bug_addr_disp ;
186 int file_disp ;
187 unsigned short line ;
188 unsigned short flags ;
189};
190#line 89 "include/linux/bug.h"
191struct cpumask {
192 unsigned long bits[64U] ;
193};
194#line 637 "include/linux/cpumask.h"
195typedef struct cpumask *cpumask_var_t;
196#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
197struct static_key;
198#line 234
199struct static_key;
200#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
201struct kmem_cache;
202#line 23 "include/asm-generic/atomic-long.h"
203typedef atomic64_t atomic_long_t;
204#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
205typedef u16 __ticket_t;
206#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
207typedef u32 __ticketpair_t;
208#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
209struct __raw_tickets {
210 __ticket_t head ;
211 __ticket_t tail ;
212};
213#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
214union __anonunion_ldv_5907_29 {
215 __ticketpair_t head_tail ;
216 struct __raw_tickets tickets ;
217};
218#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
219struct arch_spinlock {
220 union __anonunion_ldv_5907_29 ldv_5907 ;
221};
222#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
223typedef struct arch_spinlock arch_spinlock_t;
224#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
225struct __anonstruct_ldv_5914_31 {
226 u32 read ;
227 s32 write ;
228};
229#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
230union __anonunion_arch_rwlock_t_30 {
231 s64 lock ;
232 struct __anonstruct_ldv_5914_31 ldv_5914 ;
233};
234#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
235typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
236#line 34
237struct lockdep_map;
238#line 34
239struct lockdep_map;
240#line 55 "include/linux/debug_locks.h"
241struct stack_trace {
242 unsigned int nr_entries ;
243 unsigned int max_entries ;
244 unsigned long *entries ;
245 int skip ;
246};
247#line 26 "include/linux/stacktrace.h"
248struct lockdep_subclass_key {
249 char __one_byte ;
250};
251#line 53 "include/linux/lockdep.h"
252struct lock_class_key {
253 struct lockdep_subclass_key subkeys[8U] ;
254};
255#line 59 "include/linux/lockdep.h"
256struct lock_class {
257 struct list_head hash_entry ;
258 struct list_head lock_entry ;
259 struct lockdep_subclass_key *key ;
260 unsigned int subclass ;
261 unsigned int dep_gen_id ;
262 unsigned long usage_mask ;
263 struct stack_trace usage_traces[13U] ;
264 struct list_head locks_after ;
265 struct list_head locks_before ;
266 unsigned int version ;
267 unsigned long ops ;
268 char const *name ;
269 int name_version ;
270 unsigned long contention_point[4U] ;
271 unsigned long contending_point[4U] ;
272};
273#line 144 "include/linux/lockdep.h"
274struct lockdep_map {
275 struct lock_class_key *key ;
276 struct lock_class *class_cache[2U] ;
277 char const *name ;
278 int cpu ;
279 unsigned long ip ;
280};
281#line 556 "include/linux/lockdep.h"
282struct raw_spinlock {
283 arch_spinlock_t raw_lock ;
284 unsigned int magic ;
285 unsigned int owner_cpu ;
286 void *owner ;
287 struct lockdep_map dep_map ;
288};
289#line 32 "include/linux/spinlock_types.h"
290typedef struct raw_spinlock raw_spinlock_t;
291#line 33 "include/linux/spinlock_types.h"
292struct __anonstruct_ldv_6122_33 {
293 u8 __padding[24U] ;
294 struct lockdep_map dep_map ;
295};
296#line 33 "include/linux/spinlock_types.h"
297union __anonunion_ldv_6123_32 {
298 struct raw_spinlock rlock ;
299 struct __anonstruct_ldv_6122_33 ldv_6122 ;
300};
301#line 33 "include/linux/spinlock_types.h"
302struct spinlock {
303 union __anonunion_ldv_6123_32 ldv_6123 ;
304};
305#line 76 "include/linux/spinlock_types.h"
306typedef struct spinlock spinlock_t;
307#line 23 "include/linux/rwlock_types.h"
308struct __anonstruct_rwlock_t_34 {
309 arch_rwlock_t raw_lock ;
310 unsigned int magic ;
311 unsigned int owner_cpu ;
312 void *owner ;
313 struct lockdep_map dep_map ;
314};
315#line 23 "include/linux/rwlock_types.h"
316typedef struct __anonstruct_rwlock_t_34 rwlock_t;
317#line 110 "include/linux/seqlock.h"
318struct seqcount {
319 unsigned int sequence ;
320};
321#line 121 "include/linux/seqlock.h"
322typedef struct seqcount seqcount_t;
323#line 254 "include/linux/seqlock.h"
324struct timespec {
325 __kernel_time_t tv_sec ;
326 long tv_nsec ;
327};
328#line 286 "include/linux/time.h"
329struct kstat {
330 u64 ino ;
331 dev_t dev ;
332 umode_t mode ;
333 unsigned int nlink ;
334 uid_t uid ;
335 gid_t gid ;
336 dev_t rdev ;
337 loff_t size ;
338 struct timespec atime ;
339 struct timespec mtime ;
340 struct timespec ctime ;
341 unsigned long blksize ;
342 unsigned long long blocks ;
343};
344#line 48 "include/linux/wait.h"
345struct __wait_queue_head {
346 spinlock_t lock ;
347 struct list_head task_list ;
348};
349#line 53 "include/linux/wait.h"
350typedef struct __wait_queue_head wait_queue_head_t;
351#line 98 "include/linux/nodemask.h"
352struct __anonstruct_nodemask_t_36 {
353 unsigned long bits[16U] ;
354};
355#line 98 "include/linux/nodemask.h"
356typedef struct __anonstruct_nodemask_t_36 nodemask_t;
357#line 670 "include/linux/mmzone.h"
358struct mutex {
359 atomic_t count ;
360 spinlock_t wait_lock ;
361 struct list_head wait_list ;
362 struct task_struct *owner ;
363 char const *name ;
364 void *magic ;
365 struct lockdep_map dep_map ;
366};
367#line 171 "include/linux/mutex.h"
368struct rw_semaphore;
369#line 171
370struct rw_semaphore;
371#line 172 "include/linux/mutex.h"
372struct rw_semaphore {
373 long count ;
374 raw_spinlock_t wait_lock ;
375 struct list_head wait_list ;
376 struct lockdep_map dep_map ;
377};
378#line 128 "include/linux/rwsem.h"
379struct completion {
380 unsigned int done ;
381 wait_queue_head_t wait ;
382};
383#line 188 "include/linux/rcupdate.h"
384struct notifier_block;
385#line 188
386struct notifier_block;
387#line 239 "include/linux/srcu.h"
388struct notifier_block {
389 int (*notifier_call)(struct notifier_block * , unsigned long , void * ) ;
390 struct notifier_block *next ;
391 int priority ;
392};
393#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
394struct resource {
395 resource_size_t start ;
396 resource_size_t end ;
397 char const *name ;
398 unsigned long flags ;
399 struct resource *parent ;
400 struct resource *sibling ;
401 struct resource *child ;
402};
403#line 181 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/x86_init.h"
404struct pci_dev;
405#line 181
406struct pci_dev;
407#line 312 "include/linux/jiffies.h"
408union ktime {
409 s64 tv64 ;
410};
411#line 59 "include/linux/ktime.h"
412typedef union ktime ktime_t;
413#line 341
414struct tvec_base;
415#line 341
416struct tvec_base;
417#line 342 "include/linux/ktime.h"
418struct timer_list {
419 struct list_head entry ;
420 unsigned long expires ;
421 struct tvec_base *base ;
422 void (*function)(unsigned long ) ;
423 unsigned long data ;
424 int slack ;
425 int start_pid ;
426 void *start_site ;
427 char start_comm[16U] ;
428 struct lockdep_map lockdep_map ;
429};
430#line 302 "include/linux/timer.h"
431struct work_struct;
432#line 302
433struct work_struct;
434#line 45 "include/linux/workqueue.h"
435struct work_struct {
436 atomic_long_t data ;
437 struct list_head entry ;
438 void (*func)(struct work_struct * ) ;
439 struct lockdep_map lockdep_map ;
440};
441#line 46 "include/linux/pm.h"
442struct pm_message {
443 int event ;
444};
445#line 52 "include/linux/pm.h"
446typedef struct pm_message pm_message_t;
447#line 53 "include/linux/pm.h"
448struct dev_pm_ops {
449 int (*prepare)(struct device * ) ;
450 void (*complete)(struct device * ) ;
451 int (*suspend)(struct device * ) ;
452 int (*resume)(struct device * ) ;
453 int (*freeze)(struct device * ) ;
454 int (*thaw)(struct device * ) ;
455 int (*poweroff)(struct device * ) ;
456 int (*restore)(struct device * ) ;
457 int (*suspend_late)(struct device * ) ;
458 int (*resume_early)(struct device * ) ;
459 int (*freeze_late)(struct device * ) ;
460 int (*thaw_early)(struct device * ) ;
461 int (*poweroff_late)(struct device * ) ;
462 int (*restore_early)(struct device * ) ;
463 int (*suspend_noirq)(struct device * ) ;
464 int (*resume_noirq)(struct device * ) ;
465 int (*freeze_noirq)(struct device * ) ;
466 int (*thaw_noirq)(struct device * ) ;
467 int (*poweroff_noirq)(struct device * ) ;
468 int (*restore_noirq)(struct device * ) ;
469 int (*runtime_suspend)(struct device * ) ;
470 int (*runtime_resume)(struct device * ) ;
471 int (*runtime_idle)(struct device * ) ;
472};
473#line 289
474enum rpm_status {
475 RPM_ACTIVE = 0,
476 RPM_RESUMING = 1,
477 RPM_SUSPENDED = 2,
478 RPM_SUSPENDING = 3
479} ;
480#line 296
481enum rpm_request {
482 RPM_REQ_NONE = 0,
483 RPM_REQ_IDLE = 1,
484 RPM_REQ_SUSPEND = 2,
485 RPM_REQ_AUTOSUSPEND = 3,
486 RPM_REQ_RESUME = 4
487} ;
488#line 304
489struct wakeup_source;
490#line 304
491struct wakeup_source;
492#line 494 "include/linux/pm.h"
493struct pm_subsys_data {
494 spinlock_t lock ;
495 unsigned int refcount ;
496};
497#line 499
498struct dev_pm_qos_request;
499#line 499
500struct pm_qos_constraints;
501#line 499 "include/linux/pm.h"
502struct dev_pm_info {
503 pm_message_t power_state ;
504 unsigned char can_wakeup : 1 ;
505 unsigned char async_suspend : 1 ;
506 bool is_prepared ;
507 bool is_suspended ;
508 bool ignore_children ;
509 spinlock_t lock ;
510 struct list_head entry ;
511 struct completion completion ;
512 struct wakeup_source *wakeup ;
513 bool wakeup_path ;
514 struct timer_list suspend_timer ;
515 unsigned long timer_expires ;
516 struct work_struct work ;
517 wait_queue_head_t wait_queue ;
518 atomic_t usage_count ;
519 atomic_t child_count ;
520 unsigned char disable_depth : 3 ;
521 unsigned char idle_notification : 1 ;
522 unsigned char request_pending : 1 ;
523 unsigned char deferred_resume : 1 ;
524 unsigned char run_wake : 1 ;
525 unsigned char runtime_auto : 1 ;
526 unsigned char no_callbacks : 1 ;
527 unsigned char irq_safe : 1 ;
528 unsigned char use_autosuspend : 1 ;
529 unsigned char timer_autosuspends : 1 ;
530 enum rpm_request request ;
531 enum rpm_status runtime_status ;
532 int runtime_error ;
533 int autosuspend_delay ;
534 unsigned long last_busy ;
535 unsigned long active_jiffies ;
536 unsigned long suspended_jiffies ;
537 unsigned long accounting_timestamp ;
538 ktime_t suspend_time ;
539 s64 max_time_suspended_ns ;
540 struct dev_pm_qos_request *pq_req ;
541 struct pm_subsys_data *subsys_data ;
542 struct pm_qos_constraints *constraints ;
543};
544#line 558 "include/linux/pm.h"
545struct dev_pm_domain {
546 struct dev_pm_ops ops ;
547};
548#line 173 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/topology.h"
549struct pci_bus;
550#line 173
551struct pci_bus;
552#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
553struct __anonstruct_mm_context_t_101 {
554 void *ldt ;
555 int size ;
556 unsigned short ia32_compat ;
557 struct mutex lock ;
558 void *vdso ;
559};
560#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
561typedef struct __anonstruct_mm_context_t_101 mm_context_t;
562#line 18 "include/asm-generic/pci_iomap.h"
563struct vm_area_struct;
564#line 18
565struct vm_area_struct;
566#line 835 "include/linux/sysctl.h"
567struct rb_node {
568 unsigned long rb_parent_color ;
569 struct rb_node *rb_right ;
570 struct rb_node *rb_left ;
571};
572#line 108 "include/linux/rbtree.h"
573struct rb_root {
574 struct rb_node *rb_node ;
575};
576#line 37 "include/linux/kmod.h"
577struct cred;
578#line 37
579struct cred;
580#line 18 "include/linux/elf.h"
581typedef __u64 Elf64_Addr;
582#line 19 "include/linux/elf.h"
583typedef __u16 Elf64_Half;
584#line 23 "include/linux/elf.h"
585typedef __u32 Elf64_Word;
586#line 24 "include/linux/elf.h"
587typedef __u64 Elf64_Xword;
588#line 193 "include/linux/elf.h"
589struct elf64_sym {
590 Elf64_Word st_name ;
591 unsigned char st_info ;
592 unsigned char st_other ;
593 Elf64_Half st_shndx ;
594 Elf64_Addr st_value ;
595 Elf64_Xword st_size ;
596};
597#line 201 "include/linux/elf.h"
598typedef struct elf64_sym Elf64_Sym;
599#line 445
600struct sock;
601#line 445
602struct sock;
603#line 446
604struct kobject;
605#line 446
606struct kobject;
607#line 447
608enum kobj_ns_type {
609 KOBJ_NS_TYPE_NONE = 0,
610 KOBJ_NS_TYPE_NET = 1,
611 KOBJ_NS_TYPES = 2
612} ;
613#line 453 "include/linux/elf.h"
614struct kobj_ns_type_operations {
615 enum kobj_ns_type type ;
616 void *(*grab_current_ns)(void) ;
617 void const *(*netlink_ns)(struct sock * ) ;
618 void const *(*initial_ns)(void) ;
619 void (*drop_ns)(void * ) ;
620};
621#line 57 "include/linux/kobject_ns.h"
622struct attribute {
623 char const *name ;
624 umode_t mode ;
625 struct lock_class_key *key ;
626 struct lock_class_key skey ;
627};
628#line 33 "include/linux/sysfs.h"
629struct attribute_group {
630 char const *name ;
631 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
632 struct attribute **attrs ;
633};
634#line 62 "include/linux/sysfs.h"
635struct bin_attribute {
636 struct attribute attr ;
637 size_t size ;
638 void *private ;
639 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
640 loff_t , size_t ) ;
641 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
642 loff_t , size_t ) ;
643 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
644};
645#line 98 "include/linux/sysfs.h"
646struct sysfs_ops {
647 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
648 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
649 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
650};
651#line 117
652struct sysfs_dirent;
653#line 117
654struct sysfs_dirent;
655#line 182 "include/linux/sysfs.h"
656struct kref {
657 atomic_t refcount ;
658};
659#line 49 "include/linux/kobject.h"
660struct kset;
661#line 49
662struct kobj_type;
663#line 49 "include/linux/kobject.h"
664struct kobject {
665 char const *name ;
666 struct list_head entry ;
667 struct kobject *parent ;
668 struct kset *kset ;
669 struct kobj_type *ktype ;
670 struct sysfs_dirent *sd ;
671 struct kref kref ;
672 unsigned char state_initialized : 1 ;
673 unsigned char state_in_sysfs : 1 ;
674 unsigned char state_add_uevent_sent : 1 ;
675 unsigned char state_remove_uevent_sent : 1 ;
676 unsigned char uevent_suppress : 1 ;
677};
678#line 107 "include/linux/kobject.h"
679struct kobj_type {
680 void (*release)(struct kobject * ) ;
681 struct sysfs_ops const *sysfs_ops ;
682 struct attribute **default_attrs ;
683 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
684 void const *(*namespace)(struct kobject * ) ;
685};
686#line 115 "include/linux/kobject.h"
687struct kobj_uevent_env {
688 char *envp[32U] ;
689 int envp_idx ;
690 char buf[2048U] ;
691 int buflen ;
692};
693#line 122 "include/linux/kobject.h"
694struct kset_uevent_ops {
695 int (* const filter)(struct kset * , struct kobject * ) ;
696 char const *(* const name)(struct kset * , struct kobject * ) ;
697 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
698};
699#line 139 "include/linux/kobject.h"
700struct kset {
701 struct list_head list ;
702 spinlock_t list_lock ;
703 struct kobject kobj ;
704 struct kset_uevent_ops const *uevent_ops ;
705};
706#line 215
707struct kernel_param;
708#line 215
709struct kernel_param;
710#line 216 "include/linux/kobject.h"
711struct kernel_param_ops {
712 int (*set)(char const * , struct kernel_param const * ) ;
713 int (*get)(char * , struct kernel_param const * ) ;
714 void (*free)(void * ) ;
715};
716#line 49 "include/linux/moduleparam.h"
717struct kparam_string;
718#line 49
719struct kparam_array;
720#line 49 "include/linux/moduleparam.h"
721union __anonunion_ldv_13363_134 {
722 void *arg ;
723 struct kparam_string const *str ;
724 struct kparam_array const *arr ;
725};
726#line 49 "include/linux/moduleparam.h"
727struct kernel_param {
728 char const *name ;
729 struct kernel_param_ops const *ops ;
730 u16 perm ;
731 s16 level ;
732 union __anonunion_ldv_13363_134 ldv_13363 ;
733};
734#line 61 "include/linux/moduleparam.h"
735struct kparam_string {
736 unsigned int maxlen ;
737 char *string ;
738};
739#line 67 "include/linux/moduleparam.h"
740struct kparam_array {
741 unsigned int max ;
742 unsigned int elemsize ;
743 unsigned int *num ;
744 struct kernel_param_ops const *ops ;
745 void *elem ;
746};
747#line 458 "include/linux/moduleparam.h"
748struct static_key {
749 atomic_t enabled ;
750};
751#line 225 "include/linux/jump_label.h"
752struct tracepoint;
753#line 225
754struct tracepoint;
755#line 226 "include/linux/jump_label.h"
756struct tracepoint_func {
757 void *func ;
758 void *data ;
759};
760#line 29 "include/linux/tracepoint.h"
761struct tracepoint {
762 char const *name ;
763 struct static_key key ;
764 void (*regfunc)(void) ;
765 void (*unregfunc)(void) ;
766 struct tracepoint_func *funcs ;
767};
768#line 86 "include/linux/tracepoint.h"
769struct kernel_symbol {
770 unsigned long value ;
771 char const *name ;
772};
773#line 27 "include/linux/export.h"
774struct mod_arch_specific {
775
776};
777#line 34 "include/linux/module.h"
778struct module_param_attrs;
779#line 34 "include/linux/module.h"
780struct module_kobject {
781 struct kobject kobj ;
782 struct module *mod ;
783 struct kobject *drivers_dir ;
784 struct module_param_attrs *mp ;
785};
786#line 43 "include/linux/module.h"
787struct module_attribute {
788 struct attribute attr ;
789 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
790 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
791 size_t ) ;
792 void (*setup)(struct module * , char const * ) ;
793 int (*test)(struct module * ) ;
794 void (*free)(struct module * ) ;
795};
796#line 69
797struct exception_table_entry;
798#line 69
799struct exception_table_entry;
800#line 198
801enum module_state {
802 MODULE_STATE_LIVE = 0,
803 MODULE_STATE_COMING = 1,
804 MODULE_STATE_GOING = 2
805} ;
806#line 204 "include/linux/module.h"
807struct module_ref {
808 unsigned long incs ;
809 unsigned long decs ;
810};
811#line 219
812struct module_sect_attrs;
813#line 219
814struct module_notes_attrs;
815#line 219
816struct ftrace_event_call;
817#line 219 "include/linux/module.h"
818struct module {
819 enum module_state state ;
820 struct list_head list ;
821 char name[56U] ;
822 struct module_kobject mkobj ;
823 struct module_attribute *modinfo_attrs ;
824 char const *version ;
825 char const *srcversion ;
826 struct kobject *holders_dir ;
827 struct kernel_symbol const *syms ;
828 unsigned long const *crcs ;
829 unsigned int num_syms ;
830 struct kernel_param *kp ;
831 unsigned int num_kp ;
832 unsigned int num_gpl_syms ;
833 struct kernel_symbol const *gpl_syms ;
834 unsigned long const *gpl_crcs ;
835 struct kernel_symbol const *unused_syms ;
836 unsigned long const *unused_crcs ;
837 unsigned int num_unused_syms ;
838 unsigned int num_unused_gpl_syms ;
839 struct kernel_symbol const *unused_gpl_syms ;
840 unsigned long const *unused_gpl_crcs ;
841 struct kernel_symbol const *gpl_future_syms ;
842 unsigned long const *gpl_future_crcs ;
843 unsigned int num_gpl_future_syms ;
844 unsigned int num_exentries ;
845 struct exception_table_entry *extable ;
846 int (*init)(void) ;
847 void *module_init ;
848 void *module_core ;
849 unsigned int init_size ;
850 unsigned int core_size ;
851 unsigned int init_text_size ;
852 unsigned int core_text_size ;
853 unsigned int init_ro_size ;
854 unsigned int core_ro_size ;
855 struct mod_arch_specific arch ;
856 unsigned int taints ;
857 unsigned int num_bugs ;
858 struct list_head bug_list ;
859 struct bug_entry *bug_table ;
860 Elf64_Sym *symtab ;
861 Elf64_Sym *core_symtab ;
862 unsigned int num_symtab ;
863 unsigned int core_num_syms ;
864 char *strtab ;
865 char *core_strtab ;
866 struct module_sect_attrs *sect_attrs ;
867 struct module_notes_attrs *notes_attrs ;
868 char *args ;
869 void *percpu ;
870 unsigned int percpu_size ;
871 unsigned int num_tracepoints ;
872 struct tracepoint * const *tracepoints_ptrs ;
873 unsigned int num_trace_bprintk_fmt ;
874 char const **trace_bprintk_fmt_start ;
875 struct ftrace_event_call **trace_events ;
876 unsigned int num_trace_events ;
877 struct list_head source_list ;
878 struct list_head target_list ;
879 struct task_struct *waiter ;
880 void (*exit)(void) ;
881 struct module_ref *refptr ;
882 ctor_fn_t (**ctors)(void) ;
883 unsigned int num_ctors ;
884};
885#line 88 "include/linux/kmemleak.h"
886struct kmem_cache_cpu {
887 void **freelist ;
888 unsigned long tid ;
889 struct page *page ;
890 struct page *partial ;
891 int node ;
892 unsigned int stat[26U] ;
893};
894#line 55 "include/linux/slub_def.h"
895struct kmem_cache_node {
896 spinlock_t list_lock ;
897 unsigned long nr_partial ;
898 struct list_head partial ;
899 atomic_long_t nr_slabs ;
900 atomic_long_t total_objects ;
901 struct list_head full ;
902};
903#line 66 "include/linux/slub_def.h"
904struct kmem_cache_order_objects {
905 unsigned long x ;
906};
907#line 76 "include/linux/slub_def.h"
908struct kmem_cache {
909 struct kmem_cache_cpu *cpu_slab ;
910 unsigned long flags ;
911 unsigned long min_partial ;
912 int size ;
913 int objsize ;
914 int offset ;
915 int cpu_partial ;
916 struct kmem_cache_order_objects oo ;
917 struct kmem_cache_order_objects max ;
918 struct kmem_cache_order_objects min ;
919 gfp_t allocflags ;
920 int refcount ;
921 void (*ctor)(void * ) ;
922 int inuse ;
923 int align ;
924 int reserved ;
925 char const *name ;
926 struct list_head list ;
927 struct kobject kobj ;
928 int remote_node_defrag_ratio ;
929 struct kmem_cache_node *node[1024U] ;
930};
931#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
932enum irqreturn {
933 IRQ_NONE = 0,
934 IRQ_HANDLED = 1,
935 IRQ_WAKE_THREAD = 2
936} ;
937#line 16 "include/linux/irqreturn.h"
938typedef enum irqreturn irqreturn_t;
939#line 348 "include/linux/irq.h"
940struct proc_dir_entry;
941#line 348
942struct proc_dir_entry;
943#line 41 "include/asm-generic/sections.h"
944struct exception_table_entry {
945 unsigned long insn ;
946 unsigned long fixup ;
947};
948#line 702 "include/linux/interrupt.h"
949struct file_operations;
950#line 702 "include/linux/interrupt.h"
951struct miscdevice {
952 int minor ;
953 char const *name ;
954 struct file_operations const *fops ;
955 struct list_head list ;
956 struct device *parent ;
957 struct device *this_device ;
958 char const *nodename ;
959 umode_t mode ;
960};
961#line 63 "include/linux/miscdevice.h"
962struct watchdog_info {
963 __u32 options ;
964 __u32 firmware_version ;
965 __u8 identity[32U] ;
966};
967#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/emergency-restart.h"
968struct block_device;
969#line 22
970struct block_device;
971#line 93 "include/linux/bit_spinlock.h"
972struct hlist_bl_node;
973#line 93 "include/linux/bit_spinlock.h"
974struct hlist_bl_head {
975 struct hlist_bl_node *first ;
976};
977#line 36 "include/linux/list_bl.h"
978struct hlist_bl_node {
979 struct hlist_bl_node *next ;
980 struct hlist_bl_node **pprev ;
981};
982#line 114 "include/linux/rculist_bl.h"
983struct nameidata;
984#line 114
985struct nameidata;
986#line 115
987struct path;
988#line 115
989struct path;
990#line 116
991struct vfsmount;
992#line 116
993struct vfsmount;
994#line 117 "include/linux/rculist_bl.h"
995struct qstr {
996 unsigned int hash ;
997 unsigned int len ;
998 unsigned char const *name ;
999};
1000#line 72 "include/linux/dcache.h"
1001struct inode;
1002#line 72
1003struct dentry_operations;
1004#line 72
1005struct super_block;
1006#line 72 "include/linux/dcache.h"
1007union __anonunion_d_u_136 {
1008 struct list_head d_child ;
1009 struct rcu_head d_rcu ;
1010};
1011#line 72 "include/linux/dcache.h"
1012struct dentry {
1013 unsigned int d_flags ;
1014 seqcount_t d_seq ;
1015 struct hlist_bl_node d_hash ;
1016 struct dentry *d_parent ;
1017 struct qstr d_name ;
1018 struct inode *d_inode ;
1019 unsigned char d_iname[32U] ;
1020 unsigned int d_count ;
1021 spinlock_t d_lock ;
1022 struct dentry_operations const *d_op ;
1023 struct super_block *d_sb ;
1024 unsigned long d_time ;
1025 void *d_fsdata ;
1026 struct list_head d_lru ;
1027 union __anonunion_d_u_136 d_u ;
1028 struct list_head d_subdirs ;
1029 struct list_head d_alias ;
1030};
1031#line 123 "include/linux/dcache.h"
1032struct dentry_operations {
1033 int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1034 int (*d_hash)(struct dentry const * , struct inode const * , struct qstr * ) ;
1035 int (*d_compare)(struct dentry const * , struct inode const * , struct dentry const * ,
1036 struct inode const * , unsigned int , char const * , struct qstr const * ) ;
1037 int (*d_delete)(struct dentry const * ) ;
1038 void (*d_release)(struct dentry * ) ;
1039 void (*d_prune)(struct dentry * ) ;
1040 void (*d_iput)(struct dentry * , struct inode * ) ;
1041 char *(*d_dname)(struct dentry * , char * , int ) ;
1042 struct vfsmount *(*d_automount)(struct path * ) ;
1043 int (*d_manage)(struct dentry * , bool ) ;
1044};
1045#line 402 "include/linux/dcache.h"
1046struct path {
1047 struct vfsmount *mnt ;
1048 struct dentry *dentry ;
1049};
1050#line 58 "include/linux/radix-tree.h"
1051struct radix_tree_node;
1052#line 58 "include/linux/radix-tree.h"
1053struct radix_tree_root {
1054 unsigned int height ;
1055 gfp_t gfp_mask ;
1056 struct radix_tree_node *rnode ;
1057};
1058#line 377
1059struct prio_tree_node;
1060#line 377 "include/linux/radix-tree.h"
1061struct raw_prio_tree_node {
1062 struct prio_tree_node *left ;
1063 struct prio_tree_node *right ;
1064 struct prio_tree_node *parent ;
1065};
1066#line 19 "include/linux/prio_tree.h"
1067struct prio_tree_node {
1068 struct prio_tree_node *left ;
1069 struct prio_tree_node *right ;
1070 struct prio_tree_node *parent ;
1071 unsigned long start ;
1072 unsigned long last ;
1073};
1074#line 27 "include/linux/prio_tree.h"
1075struct prio_tree_root {
1076 struct prio_tree_node *prio_tree_node ;
1077 unsigned short index_bits ;
1078 unsigned short raw ;
1079};
1080#line 111
1081enum pid_type {
1082 PIDTYPE_PID = 0,
1083 PIDTYPE_PGID = 1,
1084 PIDTYPE_SID = 2,
1085 PIDTYPE_MAX = 3
1086} ;
1087#line 118
1088struct pid_namespace;
1089#line 118 "include/linux/prio_tree.h"
1090struct upid {
1091 int nr ;
1092 struct pid_namespace *ns ;
1093 struct hlist_node pid_chain ;
1094};
1095#line 56 "include/linux/pid.h"
1096struct pid {
1097 atomic_t count ;
1098 unsigned int level ;
1099 struct hlist_head tasks[3U] ;
1100 struct rcu_head rcu ;
1101 struct upid numbers[1U] ;
1102};
1103#line 45 "include/linux/semaphore.h"
1104struct fiemap_extent {
1105 __u64 fe_logical ;
1106 __u64 fe_physical ;
1107 __u64 fe_length ;
1108 __u64 fe_reserved64[2U] ;
1109 __u32 fe_flags ;
1110 __u32 fe_reserved[3U] ;
1111};
1112#line 38 "include/linux/fiemap.h"
1113struct shrink_control {
1114 gfp_t gfp_mask ;
1115 unsigned long nr_to_scan ;
1116};
1117#line 14 "include/linux/shrinker.h"
1118struct shrinker {
1119 int (*shrink)(struct shrinker * , struct shrink_control * ) ;
1120 int seeks ;
1121 long batch ;
1122 struct list_head list ;
1123 atomic_long_t nr_in_batch ;
1124};
1125#line 43
1126enum migrate_mode {
1127 MIGRATE_ASYNC = 0,
1128 MIGRATE_SYNC_LIGHT = 1,
1129 MIGRATE_SYNC = 2
1130} ;
1131#line 49
1132struct export_operations;
1133#line 49
1134struct export_operations;
1135#line 51
1136struct iovec;
1137#line 51
1138struct iovec;
1139#line 52
1140struct kiocb;
1141#line 52
1142struct kiocb;
1143#line 53
1144struct pipe_inode_info;
1145#line 53
1146struct pipe_inode_info;
1147#line 54
1148struct poll_table_struct;
1149#line 54
1150struct poll_table_struct;
1151#line 55
1152struct kstatfs;
1153#line 55
1154struct kstatfs;
1155#line 435 "include/linux/fs.h"
1156struct iattr {
1157 unsigned int ia_valid ;
1158 umode_t ia_mode ;
1159 uid_t ia_uid ;
1160 gid_t ia_gid ;
1161 loff_t ia_size ;
1162 struct timespec ia_atime ;
1163 struct timespec ia_mtime ;
1164 struct timespec ia_ctime ;
1165 struct file *ia_file ;
1166};
1167#line 119 "include/linux/quota.h"
1168struct if_dqinfo {
1169 __u64 dqi_bgrace ;
1170 __u64 dqi_igrace ;
1171 __u32 dqi_flags ;
1172 __u32 dqi_valid ;
1173};
1174#line 176 "include/linux/percpu_counter.h"
1175struct fs_disk_quota {
1176 __s8 d_version ;
1177 __s8 d_flags ;
1178 __u16 d_fieldmask ;
1179 __u32 d_id ;
1180 __u64 d_blk_hardlimit ;
1181 __u64 d_blk_softlimit ;
1182 __u64 d_ino_hardlimit ;
1183 __u64 d_ino_softlimit ;
1184 __u64 d_bcount ;
1185 __u64 d_icount ;
1186 __s32 d_itimer ;
1187 __s32 d_btimer ;
1188 __u16 d_iwarns ;
1189 __u16 d_bwarns ;
1190 __s32 d_padding2 ;
1191 __u64 d_rtb_hardlimit ;
1192 __u64 d_rtb_softlimit ;
1193 __u64 d_rtbcount ;
1194 __s32 d_rtbtimer ;
1195 __u16 d_rtbwarns ;
1196 __s16 d_padding3 ;
1197 char d_padding4[8U] ;
1198};
1199#line 75 "include/linux/dqblk_xfs.h"
1200struct fs_qfilestat {
1201 __u64 qfs_ino ;
1202 __u64 qfs_nblks ;
1203 __u32 qfs_nextents ;
1204};
1205#line 150 "include/linux/dqblk_xfs.h"
1206typedef struct fs_qfilestat fs_qfilestat_t;
1207#line 151 "include/linux/dqblk_xfs.h"
1208struct fs_quota_stat {
1209 __s8 qs_version ;
1210 __u16 qs_flags ;
1211 __s8 qs_pad ;
1212 fs_qfilestat_t qs_uquota ;
1213 fs_qfilestat_t qs_gquota ;
1214 __u32 qs_incoredqs ;
1215 __s32 qs_btimelimit ;
1216 __s32 qs_itimelimit ;
1217 __s32 qs_rtbtimelimit ;
1218 __u16 qs_bwarnlimit ;
1219 __u16 qs_iwarnlimit ;
1220};
1221#line 165
1222struct dquot;
1223#line 165
1224struct dquot;
1225#line 185 "include/linux/quota.h"
1226typedef __kernel_uid32_t qid_t;
1227#line 186 "include/linux/quota.h"
1228typedef long long qsize_t;
1229#line 189 "include/linux/quota.h"
1230struct mem_dqblk {
1231 qsize_t dqb_bhardlimit ;
1232 qsize_t dqb_bsoftlimit ;
1233 qsize_t dqb_curspace ;
1234 qsize_t dqb_rsvspace ;
1235 qsize_t dqb_ihardlimit ;
1236 qsize_t dqb_isoftlimit ;
1237 qsize_t dqb_curinodes ;
1238 time_t dqb_btime ;
1239 time_t dqb_itime ;
1240};
1241#line 211
1242struct quota_format_type;
1243#line 211
1244struct quota_format_type;
1245#line 212 "include/linux/quota.h"
1246struct mem_dqinfo {
1247 struct quota_format_type *dqi_format ;
1248 int dqi_fmt_id ;
1249 struct list_head dqi_dirty_list ;
1250 unsigned long dqi_flags ;
1251 unsigned int dqi_bgrace ;
1252 unsigned int dqi_igrace ;
1253 qsize_t dqi_maxblimit ;
1254 qsize_t dqi_maxilimit ;
1255 void *dqi_priv ;
1256};
1257#line 275 "include/linux/quota.h"
1258struct dquot {
1259 struct hlist_node dq_hash ;
1260 struct list_head dq_inuse ;
1261 struct list_head dq_free ;
1262 struct list_head dq_dirty ;
1263 struct mutex dq_lock ;
1264 atomic_t dq_count ;
1265 wait_queue_head_t dq_wait_unused ;
1266 struct super_block *dq_sb ;
1267 unsigned int dq_id ;
1268 loff_t dq_off ;
1269 unsigned long dq_flags ;
1270 short dq_type ;
1271 struct mem_dqblk dq_dqb ;
1272};
1273#line 303 "include/linux/quota.h"
1274struct quota_format_ops {
1275 int (*check_quota_file)(struct super_block * , int ) ;
1276 int (*read_file_info)(struct super_block * , int ) ;
1277 int (*write_file_info)(struct super_block * , int ) ;
1278 int (*free_file_info)(struct super_block * , int ) ;
1279 int (*read_dqblk)(struct dquot * ) ;
1280 int (*commit_dqblk)(struct dquot * ) ;
1281 int (*release_dqblk)(struct dquot * ) ;
1282};
1283#line 314 "include/linux/quota.h"
1284struct dquot_operations {
1285 int (*write_dquot)(struct dquot * ) ;
1286 struct dquot *(*alloc_dquot)(struct super_block * , int ) ;
1287 void (*destroy_dquot)(struct dquot * ) ;
1288 int (*acquire_dquot)(struct dquot * ) ;
1289 int (*release_dquot)(struct dquot * ) ;
1290 int (*mark_dirty)(struct dquot * ) ;
1291 int (*write_info)(struct super_block * , int ) ;
1292 qsize_t *(*get_reserved_space)(struct inode * ) ;
1293};
1294#line 328 "include/linux/quota.h"
1295struct quotactl_ops {
1296 int (*quota_on)(struct super_block * , int , int , struct path * ) ;
1297 int (*quota_on_meta)(struct super_block * , int , int ) ;
1298 int (*quota_off)(struct super_block * , int ) ;
1299 int (*quota_sync)(struct super_block * , int , int ) ;
1300 int (*get_info)(struct super_block * , int , struct if_dqinfo * ) ;
1301 int (*set_info)(struct super_block * , int , struct if_dqinfo * ) ;
1302 int (*get_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1303 int (*set_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1304 int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1305 int (*set_xstate)(struct super_block * , unsigned int , int ) ;
1306};
1307#line 344 "include/linux/quota.h"
1308struct quota_format_type {
1309 int qf_fmt_id ;
1310 struct quota_format_ops const *qf_ops ;
1311 struct module *qf_owner ;
1312 struct quota_format_type *qf_next ;
1313};
1314#line 390 "include/linux/quota.h"
1315struct quota_info {
1316 unsigned int flags ;
1317 struct mutex dqio_mutex ;
1318 struct mutex dqonoff_mutex ;
1319 struct rw_semaphore dqptr_sem ;
1320 struct inode *files[2U] ;
1321 struct mem_dqinfo info[2U] ;
1322 struct quota_format_ops const *ops[2U] ;
1323};
1324#line 421
1325struct address_space;
1326#line 421
1327struct address_space;
1328#line 422
1329struct writeback_control;
1330#line 422
1331struct writeback_control;
1332#line 585 "include/linux/fs.h"
1333union __anonunion_arg_139 {
1334 char *buf ;
1335 void *data ;
1336};
1337#line 585 "include/linux/fs.h"
1338struct __anonstruct_read_descriptor_t_138 {
1339 size_t written ;
1340 size_t count ;
1341 union __anonunion_arg_139 arg ;
1342 int error ;
1343};
1344#line 585 "include/linux/fs.h"
1345typedef struct __anonstruct_read_descriptor_t_138 read_descriptor_t;
1346#line 588 "include/linux/fs.h"
1347struct address_space_operations {
1348 int (*writepage)(struct page * , struct writeback_control * ) ;
1349 int (*readpage)(struct file * , struct page * ) ;
1350 int (*writepages)(struct address_space * , struct writeback_control * ) ;
1351 int (*set_page_dirty)(struct page * ) ;
1352 int (*readpages)(struct file * , struct address_space * , struct list_head * ,
1353 unsigned int ) ;
1354 int (*write_begin)(struct file * , struct address_space * , loff_t , unsigned int ,
1355 unsigned int , struct page ** , void ** ) ;
1356 int (*write_end)(struct file * , struct address_space * , loff_t , unsigned int ,
1357 unsigned int , struct page * , void * ) ;
1358 sector_t (*bmap)(struct address_space * , sector_t ) ;
1359 void (*invalidatepage)(struct page * , unsigned long ) ;
1360 int (*releasepage)(struct page * , gfp_t ) ;
1361 void (*freepage)(struct page * ) ;
1362 ssize_t (*direct_IO)(int , struct kiocb * , struct iovec const * , loff_t ,
1363 unsigned long ) ;
1364 int (*get_xip_mem)(struct address_space * , unsigned long , int , void ** , unsigned long * ) ;
1365 int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode ) ;
1366 int (*launder_page)(struct page * ) ;
1367 int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long ) ;
1368 int (*error_remove_page)(struct address_space * , struct page * ) ;
1369};
1370#line 642
1371struct backing_dev_info;
1372#line 642
1373struct backing_dev_info;
1374#line 643 "include/linux/fs.h"
1375struct address_space {
1376 struct inode *host ;
1377 struct radix_tree_root page_tree ;
1378 spinlock_t tree_lock ;
1379 unsigned int i_mmap_writable ;
1380 struct prio_tree_root i_mmap ;
1381 struct list_head i_mmap_nonlinear ;
1382 struct mutex i_mmap_mutex ;
1383 unsigned long nrpages ;
1384 unsigned long writeback_index ;
1385 struct address_space_operations const *a_ops ;
1386 unsigned long flags ;
1387 struct backing_dev_info *backing_dev_info ;
1388 spinlock_t private_lock ;
1389 struct list_head private_list ;
1390 struct address_space *assoc_mapping ;
1391};
1392#line 664
1393struct request_queue;
1394#line 664
1395struct request_queue;
1396#line 665
1397struct hd_struct;
1398#line 665
1399struct gendisk;
1400#line 665 "include/linux/fs.h"
1401struct block_device {
1402 dev_t bd_dev ;
1403 int bd_openers ;
1404 struct inode *bd_inode ;
1405 struct super_block *bd_super ;
1406 struct mutex bd_mutex ;
1407 struct list_head bd_inodes ;
1408 void *bd_claiming ;
1409 void *bd_holder ;
1410 int bd_holders ;
1411 bool bd_write_holder ;
1412 struct list_head bd_holder_disks ;
1413 struct block_device *bd_contains ;
1414 unsigned int bd_block_size ;
1415 struct hd_struct *bd_part ;
1416 unsigned int bd_part_count ;
1417 int bd_invalidated ;
1418 struct gendisk *bd_disk ;
1419 struct request_queue *bd_queue ;
1420 struct list_head bd_list ;
1421 unsigned long bd_private ;
1422 int bd_fsfreeze_count ;
1423 struct mutex bd_fsfreeze_mutex ;
1424};
1425#line 737
1426struct posix_acl;
1427#line 737
1428struct posix_acl;
1429#line 738
1430struct inode_operations;
1431#line 738 "include/linux/fs.h"
1432union __anonunion_ldv_17477_140 {
1433 unsigned int const i_nlink ;
1434 unsigned int __i_nlink ;
1435};
1436#line 738 "include/linux/fs.h"
1437union __anonunion_ldv_17496_141 {
1438 struct list_head i_dentry ;
1439 struct rcu_head i_rcu ;
1440};
1441#line 738
1442struct file_lock;
1443#line 738
1444struct cdev;
1445#line 738 "include/linux/fs.h"
1446union __anonunion_ldv_17513_142 {
1447 struct pipe_inode_info *i_pipe ;
1448 struct block_device *i_bdev ;
1449 struct cdev *i_cdev ;
1450};
1451#line 738 "include/linux/fs.h"
1452struct inode {
1453 umode_t i_mode ;
1454 unsigned short i_opflags ;
1455 uid_t i_uid ;
1456 gid_t i_gid ;
1457 unsigned int i_flags ;
1458 struct posix_acl *i_acl ;
1459 struct posix_acl *i_default_acl ;
1460 struct inode_operations const *i_op ;
1461 struct super_block *i_sb ;
1462 struct address_space *i_mapping ;
1463 void *i_security ;
1464 unsigned long i_ino ;
1465 union __anonunion_ldv_17477_140 ldv_17477 ;
1466 dev_t i_rdev ;
1467 struct timespec i_atime ;
1468 struct timespec i_mtime ;
1469 struct timespec i_ctime ;
1470 spinlock_t i_lock ;
1471 unsigned short i_bytes ;
1472 blkcnt_t i_blocks ;
1473 loff_t i_size ;
1474 unsigned long i_state ;
1475 struct mutex i_mutex ;
1476 unsigned long dirtied_when ;
1477 struct hlist_node i_hash ;
1478 struct list_head i_wb_list ;
1479 struct list_head i_lru ;
1480 struct list_head i_sb_list ;
1481 union __anonunion_ldv_17496_141 ldv_17496 ;
1482 atomic_t i_count ;
1483 unsigned int i_blkbits ;
1484 u64 i_version ;
1485 atomic_t i_dio_count ;
1486 atomic_t i_writecount ;
1487 struct file_operations const *i_fop ;
1488 struct file_lock *i_flock ;
1489 struct address_space i_data ;
1490 struct dquot *i_dquot[2U] ;
1491 struct list_head i_devices ;
1492 union __anonunion_ldv_17513_142 ldv_17513 ;
1493 __u32 i_generation ;
1494 __u32 i_fsnotify_mask ;
1495 struct hlist_head i_fsnotify_marks ;
1496 atomic_t i_readcount ;
1497 void *i_private ;
1498};
1499#line 941 "include/linux/fs.h"
1500struct fown_struct {
1501 rwlock_t lock ;
1502 struct pid *pid ;
1503 enum pid_type pid_type ;
1504 uid_t uid ;
1505 uid_t euid ;
1506 int signum ;
1507};
1508#line 949 "include/linux/fs.h"
1509struct file_ra_state {
1510 unsigned long start ;
1511 unsigned int size ;
1512 unsigned int async_size ;
1513 unsigned int ra_pages ;
1514 unsigned int mmap_miss ;
1515 loff_t prev_pos ;
1516};
1517#line 972 "include/linux/fs.h"
1518union __anonunion_f_u_143 {
1519 struct list_head fu_list ;
1520 struct rcu_head fu_rcuhead ;
1521};
1522#line 972 "include/linux/fs.h"
1523struct file {
1524 union __anonunion_f_u_143 f_u ;
1525 struct path f_path ;
1526 struct file_operations const *f_op ;
1527 spinlock_t f_lock ;
1528 int f_sb_list_cpu ;
1529 atomic_long_t f_count ;
1530 unsigned int f_flags ;
1531 fmode_t f_mode ;
1532 loff_t f_pos ;
1533 struct fown_struct f_owner ;
1534 struct cred const *f_cred ;
1535 struct file_ra_state f_ra ;
1536 u64 f_version ;
1537 void *f_security ;
1538 void *private_data ;
1539 struct list_head f_ep_links ;
1540 struct list_head f_tfile_llink ;
1541 struct address_space *f_mapping ;
1542 unsigned long f_mnt_write_state ;
1543};
1544#line 1111
1545struct files_struct;
1546#line 1111 "include/linux/fs.h"
1547typedef struct files_struct *fl_owner_t;
1548#line 1112 "include/linux/fs.h"
1549struct file_lock_operations {
1550 void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1551 void (*fl_release_private)(struct file_lock * ) ;
1552};
1553#line 1117 "include/linux/fs.h"
1554struct lock_manager_operations {
1555 int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1556 void (*lm_notify)(struct file_lock * ) ;
1557 int (*lm_grant)(struct file_lock * , struct file_lock * , int ) ;
1558 void (*lm_release_private)(struct file_lock * ) ;
1559 void (*lm_break)(struct file_lock * ) ;
1560 int (*lm_change)(struct file_lock ** , int ) ;
1561};
1562#line 1134
1563struct nlm_lockowner;
1564#line 1134
1565struct nlm_lockowner;
1566#line 1135 "include/linux/fs.h"
1567struct nfs_lock_info {
1568 u32 state ;
1569 struct nlm_lockowner *owner ;
1570 struct list_head list ;
1571};
1572#line 14 "include/linux/nfs_fs_i.h"
1573struct nfs4_lock_state;
1574#line 14
1575struct nfs4_lock_state;
1576#line 15 "include/linux/nfs_fs_i.h"
1577struct nfs4_lock_info {
1578 struct nfs4_lock_state *owner ;
1579};
1580#line 19
1581struct fasync_struct;
1582#line 19 "include/linux/nfs_fs_i.h"
1583struct __anonstruct_afs_145 {
1584 struct list_head link ;
1585 int state ;
1586};
1587#line 19 "include/linux/nfs_fs_i.h"
1588union __anonunion_fl_u_144 {
1589 struct nfs_lock_info nfs_fl ;
1590 struct nfs4_lock_info nfs4_fl ;
1591 struct __anonstruct_afs_145 afs ;
1592};
1593#line 19 "include/linux/nfs_fs_i.h"
1594struct file_lock {
1595 struct file_lock *fl_next ;
1596 struct list_head fl_link ;
1597 struct list_head fl_block ;
1598 fl_owner_t fl_owner ;
1599 unsigned int fl_flags ;
1600 unsigned char fl_type ;
1601 unsigned int fl_pid ;
1602 struct pid *fl_nspid ;
1603 wait_queue_head_t fl_wait ;
1604 struct file *fl_file ;
1605 loff_t fl_start ;
1606 loff_t fl_end ;
1607 struct fasync_struct *fl_fasync ;
1608 unsigned long fl_break_time ;
1609 unsigned long fl_downgrade_time ;
1610 struct file_lock_operations const *fl_ops ;
1611 struct lock_manager_operations const *fl_lmops ;
1612 union __anonunion_fl_u_144 fl_u ;
1613};
1614#line 1221 "include/linux/fs.h"
1615struct fasync_struct {
1616 spinlock_t fa_lock ;
1617 int magic ;
1618 int fa_fd ;
1619 struct fasync_struct *fa_next ;
1620 struct file *fa_file ;
1621 struct rcu_head fa_rcu ;
1622};
1623#line 1417
1624struct file_system_type;
1625#line 1417
1626struct super_operations;
1627#line 1417
1628struct xattr_handler;
1629#line 1417
1630struct mtd_info;
1631#line 1417 "include/linux/fs.h"
1632struct super_block {
1633 struct list_head s_list ;
1634 dev_t s_dev ;
1635 unsigned char s_dirt ;
1636 unsigned char s_blocksize_bits ;
1637 unsigned long s_blocksize ;
1638 loff_t s_maxbytes ;
1639 struct file_system_type *s_type ;
1640 struct super_operations const *s_op ;
1641 struct dquot_operations const *dq_op ;
1642 struct quotactl_ops const *s_qcop ;
1643 struct export_operations const *s_export_op ;
1644 unsigned long s_flags ;
1645 unsigned long s_magic ;
1646 struct dentry *s_root ;
1647 struct rw_semaphore s_umount ;
1648 struct mutex s_lock ;
1649 int s_count ;
1650 atomic_t s_active ;
1651 void *s_security ;
1652 struct xattr_handler const **s_xattr ;
1653 struct list_head s_inodes ;
1654 struct hlist_bl_head s_anon ;
1655 struct list_head *s_files ;
1656 struct list_head s_mounts ;
1657 struct list_head s_dentry_lru ;
1658 int s_nr_dentry_unused ;
1659 spinlock_t s_inode_lru_lock ;
1660 struct list_head s_inode_lru ;
1661 int s_nr_inodes_unused ;
1662 struct block_device *s_bdev ;
1663 struct backing_dev_info *s_bdi ;
1664 struct mtd_info *s_mtd ;
1665 struct hlist_node s_instances ;
1666 struct quota_info s_dquot ;
1667 int s_frozen ;
1668 wait_queue_head_t s_wait_unfrozen ;
1669 char s_id[32U] ;
1670 u8 s_uuid[16U] ;
1671 void *s_fs_info ;
1672 unsigned int s_max_links ;
1673 fmode_t s_mode ;
1674 u32 s_time_gran ;
1675 struct mutex s_vfs_rename_mutex ;
1676 char *s_subtype ;
1677 char *s_options ;
1678 struct dentry_operations const *s_d_op ;
1679 int cleancache_poolid ;
1680 struct shrinker s_shrink ;
1681 atomic_long_t s_remove_count ;
1682 int s_readonly_remount ;
1683};
1684#line 1563 "include/linux/fs.h"
1685struct fiemap_extent_info {
1686 unsigned int fi_flags ;
1687 unsigned int fi_extents_mapped ;
1688 unsigned int fi_extents_max ;
1689 struct fiemap_extent *fi_extents_start ;
1690};
1691#line 1602 "include/linux/fs.h"
1692struct file_operations {
1693 struct module *owner ;
1694 loff_t (*llseek)(struct file * , loff_t , int ) ;
1695 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ;
1696 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ;
1697 ssize_t (*aio_read)(struct kiocb * , struct iovec const * , unsigned long ,
1698 loff_t ) ;
1699 ssize_t (*aio_write)(struct kiocb * , struct iovec const * , unsigned long ,
1700 loff_t ) ;
1701 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int ,
1702 loff_t , u64 , unsigned int ) ) ;
1703 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1704 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
1705 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
1706 int (*mmap)(struct file * , struct vm_area_struct * ) ;
1707 int (*open)(struct inode * , struct file * ) ;
1708 int (*flush)(struct file * , fl_owner_t ) ;
1709 int (*release)(struct inode * , struct file * ) ;
1710 int (*fsync)(struct file * , loff_t , loff_t , int ) ;
1711 int (*aio_fsync)(struct kiocb * , int ) ;
1712 int (*fasync)(int , struct file * , int ) ;
1713 int (*lock)(struct file * , int , struct file_lock * ) ;
1714 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * ,
1715 int ) ;
1716 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
1717 unsigned long , unsigned long ) ;
1718 int (*check_flags)(int ) ;
1719 int (*flock)(struct file * , int , struct file_lock * ) ;
1720 ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t ,
1721 unsigned int ) ;
1722 ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t ,
1723 unsigned int ) ;
1724 int (*setlease)(struct file * , long , struct file_lock ** ) ;
1725 long (*fallocate)(struct file * , int , loff_t , loff_t ) ;
1726};
1727#line 1637 "include/linux/fs.h"
1728struct inode_operations {
1729 struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1730 void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1731 int (*permission)(struct inode * , int ) ;
1732 struct posix_acl *(*get_acl)(struct inode * , int ) ;
1733 int (*readlink)(struct dentry * , char * , int ) ;
1734 void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
1735 int (*create)(struct inode * , struct dentry * , umode_t , struct nameidata * ) ;
1736 int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
1737 int (*unlink)(struct inode * , struct dentry * ) ;
1738 int (*symlink)(struct inode * , struct dentry * , char const * ) ;
1739 int (*mkdir)(struct inode * , struct dentry * , umode_t ) ;
1740 int (*rmdir)(struct inode * , struct dentry * ) ;
1741 int (*mknod)(struct inode * , struct dentry * , umode_t , dev_t ) ;
1742 int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
1743 void (*truncate)(struct inode * ) ;
1744 int (*setattr)(struct dentry * , struct iattr * ) ;
1745 int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
1746 int (*setxattr)(struct dentry * , char const * , void const * , size_t , int ) ;
1747 ssize_t (*getxattr)(struct dentry * , char const * , void * , size_t ) ;
1748 ssize_t (*listxattr)(struct dentry * , char * , size_t ) ;
1749 int (*removexattr)(struct dentry * , char const * ) ;
1750 void (*truncate_range)(struct inode * , loff_t , loff_t ) ;
1751 int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 , u64 ) ;
1752};
1753#line 1682 "include/linux/fs.h"
1754struct super_operations {
1755 struct inode *(*alloc_inode)(struct super_block * ) ;
1756 void (*destroy_inode)(struct inode * ) ;
1757 void (*dirty_inode)(struct inode * , int ) ;
1758 int (*write_inode)(struct inode * , struct writeback_control * ) ;
1759 int (*drop_inode)(struct inode * ) ;
1760 void (*evict_inode)(struct inode * ) ;
1761 void (*put_super)(struct super_block * ) ;
1762 void (*write_super)(struct super_block * ) ;
1763 int (*sync_fs)(struct super_block * , int ) ;
1764 int (*freeze_fs)(struct super_block * ) ;
1765 int (*unfreeze_fs)(struct super_block * ) ;
1766 int (*statfs)(struct dentry * , struct kstatfs * ) ;
1767 int (*remount_fs)(struct super_block * , int * , char * ) ;
1768 void (*umount_begin)(struct super_block * ) ;
1769 int (*show_options)(struct seq_file * , struct dentry * ) ;
1770 int (*show_devname)(struct seq_file * , struct dentry * ) ;
1771 int (*show_path)(struct seq_file * , struct dentry * ) ;
1772 int (*show_stats)(struct seq_file * , struct dentry * ) ;
1773 ssize_t (*quota_read)(struct super_block * , int , char * , size_t , loff_t ) ;
1774 ssize_t (*quota_write)(struct super_block * , int , char const * , size_t ,
1775 loff_t ) ;
1776 int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t ) ;
1777 int (*nr_cached_objects)(struct super_block * ) ;
1778 void (*free_cached_objects)(struct super_block * , int ) ;
1779};
1780#line 1834 "include/linux/fs.h"
1781struct file_system_type {
1782 char const *name ;
1783 int fs_flags ;
1784 struct dentry *(*mount)(struct file_system_type * , int , char const * , void * ) ;
1785 void (*kill_sb)(struct super_block * ) ;
1786 struct module *owner ;
1787 struct file_system_type *next ;
1788 struct hlist_head fs_supers ;
1789 struct lock_class_key s_lock_key ;
1790 struct lock_class_key s_umount_key ;
1791 struct lock_class_key s_vfs_rename_key ;
1792 struct lock_class_key i_lock_key ;
1793 struct lock_class_key i_mutex_key ;
1794 struct lock_class_key i_mutex_dir_key ;
1795};
1796#line 12 "include/linux/mod_devicetable.h"
1797typedef unsigned long kernel_ulong_t;
1798#line 13 "include/linux/mod_devicetable.h"
1799struct pci_device_id {
1800 __u32 vendor ;
1801 __u32 device ;
1802 __u32 subvendor ;
1803 __u32 subdevice ;
1804 __u32 class ;
1805 __u32 class_mask ;
1806 kernel_ulong_t driver_data ;
1807};
1808#line 215 "include/linux/mod_devicetable.h"
1809struct of_device_id {
1810 char name[32U] ;
1811 char type[32U] ;
1812 char compatible[128U] ;
1813 void *data ;
1814};
1815#line 584
1816struct klist_node;
1817#line 584
1818struct klist_node;
1819#line 37 "include/linux/klist.h"
1820struct klist_node {
1821 void *n_klist ;
1822 struct list_head n_node ;
1823 struct kref n_ref ;
1824};
1825#line 67
1826struct dma_map_ops;
1827#line 67 "include/linux/klist.h"
1828struct dev_archdata {
1829 void *acpi_handle ;
1830 struct dma_map_ops *dma_ops ;
1831 void *iommu ;
1832};
1833#line 17 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1834struct device_private;
1835#line 17
1836struct device_private;
1837#line 18
1838struct device_driver;
1839#line 18
1840struct device_driver;
1841#line 19
1842struct driver_private;
1843#line 19
1844struct driver_private;
1845#line 20
1846struct class;
1847#line 20
1848struct class;
1849#line 21
1850struct subsys_private;
1851#line 21
1852struct subsys_private;
1853#line 22
1854struct bus_type;
1855#line 22
1856struct bus_type;
1857#line 23
1858struct device_node;
1859#line 23
1860struct device_node;
1861#line 24
1862struct iommu_ops;
1863#line 24
1864struct iommu_ops;
1865#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1866struct bus_attribute {
1867 struct attribute attr ;
1868 ssize_t (*show)(struct bus_type * , char * ) ;
1869 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
1870};
1871#line 51 "include/linux/device.h"
1872struct device_attribute;
1873#line 51
1874struct driver_attribute;
1875#line 51 "include/linux/device.h"
1876struct bus_type {
1877 char const *name ;
1878 char const *dev_name ;
1879 struct device *dev_root ;
1880 struct bus_attribute *bus_attrs ;
1881 struct device_attribute *dev_attrs ;
1882 struct driver_attribute *drv_attrs ;
1883 int (*match)(struct device * , struct device_driver * ) ;
1884 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
1885 int (*probe)(struct device * ) ;
1886 int (*remove)(struct device * ) ;
1887 void (*shutdown)(struct device * ) ;
1888 int (*suspend)(struct device * , pm_message_t ) ;
1889 int (*resume)(struct device * ) ;
1890 struct dev_pm_ops const *pm ;
1891 struct iommu_ops *iommu_ops ;
1892 struct subsys_private *p ;
1893};
1894#line 125
1895struct device_type;
1896#line 182 "include/linux/device.h"
1897struct device_driver {
1898 char const *name ;
1899 struct bus_type *bus ;
1900 struct module *owner ;
1901 char const *mod_name ;
1902 bool suppress_bind_attrs ;
1903 struct of_device_id const *of_match_table ;
1904 int (*probe)(struct device * ) ;
1905 int (*remove)(struct device * ) ;
1906 void (*shutdown)(struct device * ) ;
1907 int (*suspend)(struct device * , pm_message_t ) ;
1908 int (*resume)(struct device * ) ;
1909 struct attribute_group const **groups ;
1910 struct dev_pm_ops const *pm ;
1911 struct driver_private *p ;
1912};
1913#line 245 "include/linux/device.h"
1914struct driver_attribute {
1915 struct attribute attr ;
1916 ssize_t (*show)(struct device_driver * , char * ) ;
1917 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
1918};
1919#line 299
1920struct class_attribute;
1921#line 299 "include/linux/device.h"
1922struct class {
1923 char const *name ;
1924 struct module *owner ;
1925 struct class_attribute *class_attrs ;
1926 struct device_attribute *dev_attrs ;
1927 struct bin_attribute *dev_bin_attrs ;
1928 struct kobject *dev_kobj ;
1929 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
1930 char *(*devnode)(struct device * , umode_t * ) ;
1931 void (*class_release)(struct class * ) ;
1932 void (*dev_release)(struct device * ) ;
1933 int (*suspend)(struct device * , pm_message_t ) ;
1934 int (*resume)(struct device * ) ;
1935 struct kobj_ns_type_operations const *ns_type ;
1936 void const *(*namespace)(struct device * ) ;
1937 struct dev_pm_ops const *pm ;
1938 struct subsys_private *p ;
1939};
1940#line 394 "include/linux/device.h"
1941struct class_attribute {
1942 struct attribute attr ;
1943 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
1944 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
1945 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
1946};
1947#line 447 "include/linux/device.h"
1948struct device_type {
1949 char const *name ;
1950 struct attribute_group const **groups ;
1951 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
1952 char *(*devnode)(struct device * , umode_t * ) ;
1953 void (*release)(struct device * ) ;
1954 struct dev_pm_ops const *pm ;
1955};
1956#line 474 "include/linux/device.h"
1957struct device_attribute {
1958 struct attribute attr ;
1959 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
1960 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
1961 size_t ) ;
1962};
1963#line 557 "include/linux/device.h"
1964struct device_dma_parameters {
1965 unsigned int max_segment_size ;
1966 unsigned long segment_boundary_mask ;
1967};
1968#line 567
1969struct dma_coherent_mem;
1970#line 567 "include/linux/device.h"
1971struct device {
1972 struct device *parent ;
1973 struct device_private *p ;
1974 struct kobject kobj ;
1975 char const *init_name ;
1976 struct device_type const *type ;
1977 struct mutex mutex ;
1978 struct bus_type *bus ;
1979 struct device_driver *driver ;
1980 void *platform_data ;
1981 struct dev_pm_info power ;
1982 struct dev_pm_domain *pm_domain ;
1983 int numa_node ;
1984 u64 *dma_mask ;
1985 u64 coherent_dma_mask ;
1986 struct device_dma_parameters *dma_parms ;
1987 struct list_head dma_pools ;
1988 struct dma_coherent_mem *dma_mem ;
1989 struct dev_archdata archdata ;
1990 struct device_node *of_node ;
1991 dev_t devt ;
1992 u32 id ;
1993 spinlock_t devres_lock ;
1994 struct list_head devres_head ;
1995 struct klist_node knode_class ;
1996 struct class *class ;
1997 struct attribute_group const **groups ;
1998 void (*release)(struct device * ) ;
1999};
2000#line 681 "include/linux/device.h"
2001struct wakeup_source {
2002 char const *name ;
2003 struct list_head entry ;
2004 spinlock_t lock ;
2005 struct timer_list timer ;
2006 unsigned long timer_expires ;
2007 ktime_t total_time ;
2008 ktime_t max_time ;
2009 ktime_t last_time ;
2010 unsigned long event_count ;
2011 unsigned long active_count ;
2012 unsigned long relax_count ;
2013 unsigned long hit_count ;
2014 unsigned char active : 1 ;
2015};
2016#line 69 "include/linux/io.h"
2017struct hotplug_slot;
2018#line 69 "include/linux/io.h"
2019struct pci_slot {
2020 struct pci_bus *bus ;
2021 struct list_head list ;
2022 struct hotplug_slot *hotplug ;
2023 unsigned char number ;
2024 struct kobject kobj ;
2025};
2026#line 117 "include/linux/pci.h"
2027typedef int pci_power_t;
2028#line 143 "include/linux/pci.h"
2029typedef unsigned int pci_channel_state_t;
2030#line 144
2031enum pci_channel_state {
2032 pci_channel_io_normal = 1,
2033 pci_channel_io_frozen = 2,
2034 pci_channel_io_perm_failure = 3
2035} ;
2036#line 169 "include/linux/pci.h"
2037typedef unsigned short pci_dev_flags_t;
2038#line 186 "include/linux/pci.h"
2039typedef unsigned short pci_bus_flags_t;
2040#line 229
2041struct pcie_link_state;
2042#line 229
2043struct pcie_link_state;
2044#line 230
2045struct pci_vpd;
2046#line 230
2047struct pci_vpd;
2048#line 231
2049struct pci_sriov;
2050#line 231
2051struct pci_sriov;
2052#line 232
2053struct pci_ats;
2054#line 232
2055struct pci_ats;
2056#line 233
2057struct pci_driver;
2058#line 233 "include/linux/pci.h"
2059union __anonunion_ldv_20553_147 {
2060 struct pci_sriov *sriov ;
2061 struct pci_dev *physfn ;
2062};
2063#line 233 "include/linux/pci.h"
2064struct pci_dev {
2065 struct list_head bus_list ;
2066 struct pci_bus *bus ;
2067 struct pci_bus *subordinate ;
2068 void *sysdata ;
2069 struct proc_dir_entry *procent ;
2070 struct pci_slot *slot ;
2071 unsigned int devfn ;
2072 unsigned short vendor ;
2073 unsigned short device ;
2074 unsigned short subsystem_vendor ;
2075 unsigned short subsystem_device ;
2076 unsigned int class ;
2077 u8 revision ;
2078 u8 hdr_type ;
2079 u8 pcie_cap ;
2080 unsigned char pcie_type : 4 ;
2081 unsigned char pcie_mpss : 3 ;
2082 u8 rom_base_reg ;
2083 u8 pin ;
2084 struct pci_driver *driver ;
2085 u64 dma_mask ;
2086 struct device_dma_parameters dma_parms ;
2087 pci_power_t current_state ;
2088 int pm_cap ;
2089 unsigned char pme_support : 5 ;
2090 unsigned char pme_interrupt : 1 ;
2091 unsigned char pme_poll : 1 ;
2092 unsigned char d1_support : 1 ;
2093 unsigned char d2_support : 1 ;
2094 unsigned char no_d1d2 : 1 ;
2095 unsigned char mmio_always_on : 1 ;
2096 unsigned char wakeup_prepared : 1 ;
2097 unsigned int d3_delay ;
2098 struct pcie_link_state *link_state ;
2099 pci_channel_state_t error_state ;
2100 struct device dev ;
2101 int cfg_size ;
2102 unsigned int irq ;
2103 struct resource resource[17U] ;
2104 unsigned char transparent : 1 ;
2105 unsigned char multifunction : 1 ;
2106 unsigned char is_added : 1 ;
2107 unsigned char is_busmaster : 1 ;
2108 unsigned char no_msi : 1 ;
2109 unsigned char block_cfg_access : 1 ;
2110 unsigned char broken_parity_status : 1 ;
2111 unsigned char irq_reroute_variant : 2 ;
2112 unsigned char msi_enabled : 1 ;
2113 unsigned char msix_enabled : 1 ;
2114 unsigned char ari_enabled : 1 ;
2115 unsigned char is_managed : 1 ;
2116 unsigned char is_pcie : 1 ;
2117 unsigned char needs_freset : 1 ;
2118 unsigned char state_saved : 1 ;
2119 unsigned char is_physfn : 1 ;
2120 unsigned char is_virtfn : 1 ;
2121 unsigned char reset_fn : 1 ;
2122 unsigned char is_hotplug_bridge : 1 ;
2123 unsigned char __aer_firmware_first_valid : 1 ;
2124 unsigned char __aer_firmware_first : 1 ;
2125 pci_dev_flags_t dev_flags ;
2126 atomic_t enable_cnt ;
2127 u32 saved_config_space[16U] ;
2128 struct hlist_head saved_cap_space ;
2129 struct bin_attribute *rom_attr ;
2130 int rom_attr_enabled ;
2131 struct bin_attribute *res_attr[17U] ;
2132 struct bin_attribute *res_attr_wc[17U] ;
2133 struct list_head msi_list ;
2134 struct kset *msi_kset ;
2135 struct pci_vpd *vpd ;
2136 union __anonunion_ldv_20553_147 ldv_20553 ;
2137 struct pci_ats *ats ;
2138};
2139#line 403
2140struct pci_ops;
2141#line 403 "include/linux/pci.h"
2142struct pci_bus {
2143 struct list_head node ;
2144 struct pci_bus *parent ;
2145 struct list_head children ;
2146 struct list_head devices ;
2147 struct pci_dev *self ;
2148 struct list_head slots ;
2149 struct resource *resource[4U] ;
2150 struct list_head resources ;
2151 struct pci_ops *ops ;
2152 void *sysdata ;
2153 struct proc_dir_entry *procdir ;
2154 unsigned char number ;
2155 unsigned char primary ;
2156 unsigned char secondary ;
2157 unsigned char subordinate ;
2158 unsigned char max_bus_speed ;
2159 unsigned char cur_bus_speed ;
2160 char name[48U] ;
2161 unsigned short bridge_ctl ;
2162 pci_bus_flags_t bus_flags ;
2163 struct device *bridge ;
2164 struct device dev ;
2165 struct bin_attribute *legacy_io ;
2166 struct bin_attribute *legacy_mem ;
2167 unsigned char is_added : 1 ;
2168};
2169#line 455 "include/linux/pci.h"
2170struct pci_ops {
2171 int (*read)(struct pci_bus * , unsigned int , int , int , u32 * ) ;
2172 int (*write)(struct pci_bus * , unsigned int , int , int , u32 ) ;
2173};
2174#line 490 "include/linux/pci.h"
2175struct pci_dynids {
2176 spinlock_t lock ;
2177 struct list_head list ;
2178};
2179#line 503 "include/linux/pci.h"
2180typedef unsigned int pci_ers_result_t;
2181#line 512 "include/linux/pci.h"
2182struct pci_error_handlers {
2183 pci_ers_result_t (*error_detected)(struct pci_dev * , enum pci_channel_state ) ;
2184 pci_ers_result_t (*mmio_enabled)(struct pci_dev * ) ;
2185 pci_ers_result_t (*link_reset)(struct pci_dev * ) ;
2186 pci_ers_result_t (*slot_reset)(struct pci_dev * ) ;
2187 void (*resume)(struct pci_dev * ) ;
2188};
2189#line 540 "include/linux/pci.h"
2190struct pci_driver {
2191 struct list_head node ;
2192 char const *name ;
2193 struct pci_device_id const *id_table ;
2194 int (*probe)(struct pci_dev * , struct pci_device_id const * ) ;
2195 void (*remove)(struct pci_dev * ) ;
2196 int (*suspend)(struct pci_dev * , pm_message_t ) ;
2197 int (*suspend_late)(struct pci_dev * , pm_message_t ) ;
2198 int (*resume_early)(struct pci_dev * ) ;
2199 int (*resume)(struct pci_dev * ) ;
2200 void (*shutdown)(struct pci_dev * ) ;
2201 struct pci_error_handlers *err_handler ;
2202 struct device_driver driver ;
2203 struct pci_dynids dynids ;
2204};
2205#line 986 "include/linux/pci.h"
2206struct scatterlist {
2207 unsigned long sg_magic ;
2208 unsigned long page_link ;
2209 unsigned int offset ;
2210 unsigned int length ;
2211 dma_addr_t dma_address ;
2212 unsigned int dma_length ;
2213};
2214#line 1139 "include/linux/pci.h"
2215union __anonunion_ldv_21372_149 {
2216 unsigned long index ;
2217 void *freelist ;
2218};
2219#line 1139 "include/linux/pci.h"
2220struct __anonstruct_ldv_21382_153 {
2221 unsigned short inuse ;
2222 unsigned short objects : 15 ;
2223 unsigned char frozen : 1 ;
2224};
2225#line 1139 "include/linux/pci.h"
2226union __anonunion_ldv_21383_152 {
2227 atomic_t _mapcount ;
2228 struct __anonstruct_ldv_21382_153 ldv_21382 ;
2229};
2230#line 1139 "include/linux/pci.h"
2231struct __anonstruct_ldv_21385_151 {
2232 union __anonunion_ldv_21383_152 ldv_21383 ;
2233 atomic_t _count ;
2234};
2235#line 1139 "include/linux/pci.h"
2236union __anonunion_ldv_21386_150 {
2237 unsigned long counters ;
2238 struct __anonstruct_ldv_21385_151 ldv_21385 ;
2239};
2240#line 1139 "include/linux/pci.h"
2241struct __anonstruct_ldv_21387_148 {
2242 union __anonunion_ldv_21372_149 ldv_21372 ;
2243 union __anonunion_ldv_21386_150 ldv_21386 ;
2244};
2245#line 1139 "include/linux/pci.h"
2246struct __anonstruct_ldv_21394_155 {
2247 struct page *next ;
2248 int pages ;
2249 int pobjects ;
2250};
2251#line 1139 "include/linux/pci.h"
2252union __anonunion_ldv_21395_154 {
2253 struct list_head lru ;
2254 struct __anonstruct_ldv_21394_155 ldv_21394 ;
2255};
2256#line 1139 "include/linux/pci.h"
2257union __anonunion_ldv_21400_156 {
2258 unsigned long private ;
2259 struct kmem_cache *slab ;
2260 struct page *first_page ;
2261};
2262#line 1139 "include/linux/pci.h"
2263struct page {
2264 unsigned long flags ;
2265 struct address_space *mapping ;
2266 struct __anonstruct_ldv_21387_148 ldv_21387 ;
2267 union __anonunion_ldv_21395_154 ldv_21395 ;
2268 union __anonunion_ldv_21400_156 ldv_21400 ;
2269 unsigned long debug_flags ;
2270};
2271#line 192 "include/linux/mm_types.h"
2272struct __anonstruct_vm_set_158 {
2273 struct list_head list ;
2274 void *parent ;
2275 struct vm_area_struct *head ;
2276};
2277#line 192 "include/linux/mm_types.h"
2278union __anonunion_shared_157 {
2279 struct __anonstruct_vm_set_158 vm_set ;
2280 struct raw_prio_tree_node prio_tree_node ;
2281};
2282#line 192
2283struct anon_vma;
2284#line 192
2285struct vm_operations_struct;
2286#line 192
2287struct mempolicy;
2288#line 192 "include/linux/mm_types.h"
2289struct vm_area_struct {
2290 struct mm_struct *vm_mm ;
2291 unsigned long vm_start ;
2292 unsigned long vm_end ;
2293 struct vm_area_struct *vm_next ;
2294 struct vm_area_struct *vm_prev ;
2295 pgprot_t vm_page_prot ;
2296 unsigned long vm_flags ;
2297 struct rb_node vm_rb ;
2298 union __anonunion_shared_157 shared ;
2299 struct list_head anon_vma_chain ;
2300 struct anon_vma *anon_vma ;
2301 struct vm_operations_struct const *vm_ops ;
2302 unsigned long vm_pgoff ;
2303 struct file *vm_file ;
2304 void *vm_private_data ;
2305 struct mempolicy *vm_policy ;
2306};
2307#line 255 "include/linux/mm_types.h"
2308struct core_thread {
2309 struct task_struct *task ;
2310 struct core_thread *next ;
2311};
2312#line 261 "include/linux/mm_types.h"
2313struct core_state {
2314 atomic_t nr_threads ;
2315 struct core_thread dumper ;
2316 struct completion startup ;
2317};
2318#line 274 "include/linux/mm_types.h"
2319struct mm_rss_stat {
2320 atomic_long_t count[3U] ;
2321};
2322#line 287
2323struct linux_binfmt;
2324#line 287
2325struct mmu_notifier_mm;
2326#line 287 "include/linux/mm_types.h"
2327struct mm_struct {
2328 struct vm_area_struct *mmap ;
2329 struct rb_root mm_rb ;
2330 struct vm_area_struct *mmap_cache ;
2331 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
2332 unsigned long , unsigned long ) ;
2333 void (*unmap_area)(struct mm_struct * , unsigned long ) ;
2334 unsigned long mmap_base ;
2335 unsigned long task_size ;
2336 unsigned long cached_hole_size ;
2337 unsigned long free_area_cache ;
2338 pgd_t *pgd ;
2339 atomic_t mm_users ;
2340 atomic_t mm_count ;
2341 int map_count ;
2342 spinlock_t page_table_lock ;
2343 struct rw_semaphore mmap_sem ;
2344 struct list_head mmlist ;
2345 unsigned long hiwater_rss ;
2346 unsigned long hiwater_vm ;
2347 unsigned long total_vm ;
2348 unsigned long locked_vm ;
2349 unsigned long pinned_vm ;
2350 unsigned long shared_vm ;
2351 unsigned long exec_vm ;
2352 unsigned long stack_vm ;
2353 unsigned long reserved_vm ;
2354 unsigned long def_flags ;
2355 unsigned long nr_ptes ;
2356 unsigned long start_code ;
2357 unsigned long end_code ;
2358 unsigned long start_data ;
2359 unsigned long end_data ;
2360 unsigned long start_brk ;
2361 unsigned long brk ;
2362 unsigned long start_stack ;
2363 unsigned long arg_start ;
2364 unsigned long arg_end ;
2365 unsigned long env_start ;
2366 unsigned long env_end ;
2367 unsigned long saved_auxv[44U] ;
2368 struct mm_rss_stat rss_stat ;
2369 struct linux_binfmt *binfmt ;
2370 cpumask_var_t cpu_vm_mask_var ;
2371 mm_context_t context ;
2372 unsigned int faultstamp ;
2373 unsigned int token_priority ;
2374 unsigned int last_interval ;
2375 unsigned long flags ;
2376 struct core_state *core_state ;
2377 spinlock_t ioctx_lock ;
2378 struct hlist_head ioctx_list ;
2379 struct task_struct *owner ;
2380 struct file *exe_file ;
2381 unsigned long num_exe_file_vmas ;
2382 struct mmu_notifier_mm *mmu_notifier_mm ;
2383 pgtable_t pmd_huge_pte ;
2384 struct cpumask cpumask_allocation ;
2385};
2386#line 178 "include/linux/mm.h"
2387struct vm_fault {
2388 unsigned int flags ;
2389 unsigned long pgoff ;
2390 void *virtual_address ;
2391 struct page *page ;
2392};
2393#line 195 "include/linux/mm.h"
2394struct vm_operations_struct {
2395 void (*open)(struct vm_area_struct * ) ;
2396 void (*close)(struct vm_area_struct * ) ;
2397 int (*fault)(struct vm_area_struct * , struct vm_fault * ) ;
2398 int (*page_mkwrite)(struct vm_area_struct * , struct vm_fault * ) ;
2399 int (*access)(struct vm_area_struct * , unsigned long , void * , int , int ) ;
2400 int (*set_policy)(struct vm_area_struct * , struct mempolicy * ) ;
2401 struct mempolicy *(*get_policy)(struct vm_area_struct * , unsigned long ) ;
2402 int (*migrate)(struct vm_area_struct * , nodemask_t const * , nodemask_t const * ,
2403 unsigned long ) ;
2404};
2405#line 31 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pci_64.h"
2406struct dma_attrs {
2407 unsigned long flags[1U] ;
2408};
2409#line 67 "include/linux/dma-attrs.h"
2410enum dma_data_direction {
2411 DMA_BIDIRECTIONAL = 0,
2412 DMA_TO_DEVICE = 1,
2413 DMA_FROM_DEVICE = 2,
2414 DMA_NONE = 3
2415} ;
2416#line 268 "include/linux/scatterlist.h"
2417struct dma_map_ops {
2418 void *(*alloc)(struct device * , size_t , dma_addr_t * , gfp_t , struct dma_attrs * ) ;
2419 void (*free)(struct device * , size_t , void * , dma_addr_t , struct dma_attrs * ) ;
2420 int (*mmap)(struct device * , struct vm_area_struct * , void * , dma_addr_t ,
2421 size_t , struct dma_attrs * ) ;
2422 dma_addr_t (*map_page)(struct device * , struct page * , unsigned long , size_t ,
2423 enum dma_data_direction , struct dma_attrs * ) ;
2424 void (*unmap_page)(struct device * , dma_addr_t , size_t , enum dma_data_direction ,
2425 struct dma_attrs * ) ;
2426 int (*map_sg)(struct device * , struct scatterlist * , int , enum dma_data_direction ,
2427 struct dma_attrs * ) ;
2428 void (*unmap_sg)(struct device * , struct scatterlist * , int , enum dma_data_direction ,
2429 struct dma_attrs * ) ;
2430 void (*sync_single_for_cpu)(struct device * , dma_addr_t , size_t , enum dma_data_direction ) ;
2431 void (*sync_single_for_device)(struct device * , dma_addr_t , size_t , enum dma_data_direction ) ;
2432 void (*sync_sg_for_cpu)(struct device * , struct scatterlist * , int , enum dma_data_direction ) ;
2433 void (*sync_sg_for_device)(struct device * , struct scatterlist * , int , enum dma_data_direction ) ;
2434 int (*mapping_error)(struct device * , dma_addr_t ) ;
2435 int (*dma_supported)(struct device * , u64 ) ;
2436 int (*set_dma_mask)(struct device * , u64 ) ;
2437 int is_phys ;
2438};
2439#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2440void ldv_spin_lock(void) ;
2441#line 3
2442void ldv_spin_unlock(void) ;
2443#line 4
2444int ldv_spin_trylock(void) ;
2445#line 98 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
2446__inline static void clear_bit(int nr , unsigned long volatile *addr )
2447{ long volatile *__cil_tmp3 ;
2448
2449 {
2450#line 105
2451 __cil_tmp3 = (long volatile *)addr;
2452#line 105
2453 __asm__ volatile (".section .smp_locks,\"a\"\n.balign 4\n.long 671f - .\n.previous\n671:\n\tlock; btr %1,%0": "+m" (*__cil_tmp3): "Ir" (nr));
2454#line 107
2455 return;
2456}
2457}
2458#line 195 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
2459__inline static int test_and_set_bit(int nr , unsigned long volatile *addr )
2460{ int oldbit ;
2461 long volatile *__cil_tmp4 ;
2462
2463 {
2464#line 199
2465 __cil_tmp4 = (long volatile *)addr;
2466#line 199
2467 __asm__ volatile (".section .smp_locks,\"a\"\n.balign 4\n.long 671f - .\n.previous\n671:\n\tlock; bts %2,%1\n\tsbb %0,%0": "=r" (oldbit),
2468 "+m" (*__cil_tmp4): "Ir" (nr): "memory");
2469#line 202
2470 return (oldbit);
2471}
2472}
2473#line 101 "include/linux/printk.h"
2474extern int printk(char const * , ...) ;
2475#line 192 "include/linux/kernel.h"
2476extern void might_fault(void) ;
2477#line 22 "include/linux/spinlock_api_smp.h"
2478extern void _raw_spin_lock(raw_spinlock_t * ) ;
2479#line 39
2480extern void _raw_spin_unlock(raw_spinlock_t * ) ;
2481#line 43
2482extern void _raw_spin_unlock_irqrestore(raw_spinlock_t * , unsigned long ) ;
2483#line 283 "include/linux/spinlock.h"
2484__inline static void ldv_spin_lock_1(spinlock_t *lock )
2485{ struct raw_spinlock *__cil_tmp2 ;
2486
2487 {
2488 {
2489#line 285
2490 __cil_tmp2 = (struct raw_spinlock *)lock;
2491#line 285
2492 _raw_spin_lock(__cil_tmp2);
2493 }
2494#line 286
2495 return;
2496}
2497}
2498#line 283
2499__inline static void spin_lock(spinlock_t *lock ) ;
2500#line 323 "include/linux/spinlock.h"
2501__inline static void ldv_spin_unlock_5(spinlock_t *lock )
2502{ struct raw_spinlock *__cil_tmp2 ;
2503
2504 {
2505 {
2506#line 325
2507 __cil_tmp2 = (struct raw_spinlock *)lock;
2508#line 325
2509 _raw_spin_unlock(__cil_tmp2);
2510 }
2511#line 326
2512 return;
2513}
2514}
2515#line 323
2516__inline static void spin_unlock(spinlock_t *lock ) ;
2517#line 350 "include/linux/spinlock.h"
2518__inline static void ldv_spin_unlock_irqrestore_8(spinlock_t *lock , unsigned long flags )
2519{ struct raw_spinlock *__cil_tmp5 ;
2520
2521 {
2522 {
2523#line 352
2524 __cil_tmp5 = (struct raw_spinlock *)lock;
2525#line 352
2526 _raw_spin_unlock_irqrestore(__cil_tmp5, flags);
2527 }
2528#line 353
2529 return;
2530}
2531}
2532#line 350
2533__inline static void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags ) ;
2534#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
2535__inline static void outb(unsigned char value , int port )
2536{
2537
2538 {
2539#line 308
2540 __asm__ volatile ("outb %b0, %w1": : "a" (value), "Nd" (port));
2541#line 309
2542 return;
2543}
2544}
2545#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
2546__inline static unsigned char inb(int port )
2547{ unsigned char value ;
2548
2549 {
2550#line 308
2551 __asm__ volatile ("inb %w1, %b0": "=a" (value): "Nd" (port));
2552#line 308
2553 return (value);
2554}
2555}
2556#line 26 "include/linux/export.h"
2557extern struct module __this_module ;
2558#line 453 "include/linux/module.h"
2559extern void __module_get(struct module * ) ;
2560#line 220 "include/linux/slub_def.h"
2561extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
2562#line 223
2563void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
2564#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2565void ldv_check_alloc_flags(gfp_t flags ) ;
2566#line 12
2567void ldv_check_alloc_nonatomic(void) ;
2568#line 14
2569struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
2570#line 40 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess_64.h"
2571extern unsigned long _copy_to_user(void * , void const * , unsigned int ) ;
2572#line 63 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess_64.h"
2573__inline static int copy_to_user(void *dst , void const *src , unsigned int size )
2574{ unsigned long tmp ;
2575
2576 {
2577 {
2578#line 65
2579 might_fault();
2580#line 67
2581 tmp = _copy_to_user(dst, src, size);
2582 }
2583#line 67
2584 return ((int )tmp);
2585}
2586}
2587#line 127 "include/linux/interrupt.h"
2588extern int request_threaded_irq(unsigned int , irqreturn_t (*)(int , void * ) ,
2589 irqreturn_t (*)(int , void * ) , unsigned long ,
2590 char const * , void * ) ;
2591#line 132 "include/linux/interrupt.h"
2592__inline static int request_irq(unsigned int irq , irqreturn_t (*handler)(int , void * ) ,
2593 unsigned long flags , char const *name , void *dev )
2594{ int tmp ;
2595 irqreturn_t (*__cil_tmp7)(int , void * ) ;
2596
2597 {
2598 {
2599#line 135
2600 __cil_tmp7 = (irqreturn_t (*)(int , void * ))0;
2601#line 135
2602 tmp = request_threaded_irq(irq, handler, __cil_tmp7, flags, name, dev);
2603 }
2604#line 135
2605 return (tmp);
2606}
2607}
2608#line 184
2609extern void free_irq(unsigned int , void * ) ;
2610#line 61 "include/linux/miscdevice.h"
2611extern int misc_register(struct miscdevice * ) ;
2612#line 62
2613extern int misc_deregister(struct miscdevice * ) ;
2614#line 10 "include/asm-generic/delay.h"
2615extern void __const_udelay(unsigned long ) ;
2616#line 47 "include/linux/reboot.h"
2617extern int register_reboot_notifier(struct notifier_block * ) ;
2618#line 48
2619extern int unregister_reboot_notifier(struct notifier_block * ) ;
2620#line 2402 "include/linux/fs.h"
2621extern loff_t no_llseek(struct file * , loff_t , int ) ;
2622#line 2407
2623extern int nonseekable_open(struct inode * , struct file * ) ;
2624#line 773 "include/linux/pci.h"
2625extern int pci_enable_device(struct pci_dev * ) ;
2626#line 790
2627extern void pci_disable_device(struct pci_dev * ) ;
2628#line 907
2629extern int pci_request_region(struct pci_dev * , int , char const * ) ;
2630#line 909
2631extern void pci_release_region(struct pci_dev * , int ) ;
2632#line 940
2633extern int __pci_register_driver(struct pci_driver * , struct module * , char const * ) ;
2634#line 949
2635extern void pci_unregister_driver(struct pci_driver * ) ;
2636#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2637static int dev_count ;
2638#line 80 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2639static unsigned long open_lock ;
2640#line 81 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2641static spinlock_t wdtpci_lock = {{{{{0U}}, 3735899821U, 4294967295U, (void *)0xffffffffffffffffUL, {(struct lock_class_key *)0,
2642 {(struct lock_class *)0,
2643 (struct lock_class *)0},
2644 "wdtpci_lock",
2645 0, 0UL}}}};
2646#line 82 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2647static char expect_close ;
2648#line 84 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2649static resource_size_t io ;
2650#line 85 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2651static int irq ;
2652#line 90 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2653static int heartbeat = 60;
2654#line 91 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2655static int wd_heartbeat ;
2656#line 97 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2657static bool nowayout = (bool )1;
2658#line 104 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2659static int tachometer ;
2660#line 109 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2661static int type = 500;
2662#line 118 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2663static void wdtpci_ctr_mode(int ctr , int mode )
2664{ int __cil_tmp3 ;
2665 unsigned char __cil_tmp4 ;
2666 int __cil_tmp5 ;
2667 unsigned char __cil_tmp6 ;
2668 unsigned int __cil_tmp7 ;
2669 unsigned int __cil_tmp8 ;
2670 int __cil_tmp9 ;
2671
2672 {
2673 {
2674#line 120
2675 ctr = ctr << 6;
2676#line 121
2677 ctr = ctr | 48;
2678#line 122
2679 __cil_tmp3 = mode << 1;
2680#line 122
2681 ctr = __cil_tmp3 | ctr;
2682#line 123
2683 __cil_tmp4 = (unsigned char )ctr;
2684#line 123
2685 __cil_tmp5 = (int )__cil_tmp4;
2686#line 123
2687 __cil_tmp6 = (unsigned char )__cil_tmp5;
2688#line 123
2689 __cil_tmp7 = (unsigned int )io;
2690#line 123
2691 __cil_tmp8 = __cil_tmp7 + 3U;
2692#line 123
2693 __cil_tmp9 = (int )__cil_tmp8;
2694#line 123
2695 outb(__cil_tmp6, __cil_tmp9);
2696#line 124
2697 __const_udelay(34360UL);
2698 }
2699#line 126
2700 return;
2701}
2702}
2703#line 127 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2704static void wdtpci_ctr_load(int ctr , int val )
2705{ unsigned char __cil_tmp3 ;
2706 int __cil_tmp4 ;
2707 unsigned char __cil_tmp5 ;
2708 unsigned int __cil_tmp6 ;
2709 unsigned int __cil_tmp7 ;
2710 unsigned int __cil_tmp8 ;
2711 int __cil_tmp9 ;
2712 int __cil_tmp10 ;
2713 unsigned char __cil_tmp11 ;
2714 int __cil_tmp12 ;
2715 unsigned char __cil_tmp13 ;
2716 unsigned int __cil_tmp14 ;
2717 unsigned int __cil_tmp15 ;
2718 unsigned int __cil_tmp16 ;
2719 int __cil_tmp17 ;
2720
2721 {
2722 {
2723#line 129
2724 __cil_tmp3 = (unsigned char )val;
2725#line 129
2726 __cil_tmp4 = (int )__cil_tmp3;
2727#line 129
2728 __cil_tmp5 = (unsigned char )__cil_tmp4;
2729#line 129
2730 __cil_tmp6 = (unsigned int )ctr;
2731#line 129
2732 __cil_tmp7 = (unsigned int )io;
2733#line 129
2734 __cil_tmp8 = __cil_tmp7 + __cil_tmp6;
2735#line 129
2736 __cil_tmp9 = (int )__cil_tmp8;
2737#line 129
2738 outb(__cil_tmp5, __cil_tmp9);
2739#line 130
2740 __const_udelay(34360UL);
2741#line 131
2742 __cil_tmp10 = val >> 8;
2743#line 131
2744 __cil_tmp11 = (unsigned char )__cil_tmp10;
2745#line 131
2746 __cil_tmp12 = (int )__cil_tmp11;
2747#line 131
2748 __cil_tmp13 = (unsigned char )__cil_tmp12;
2749#line 131
2750 __cil_tmp14 = (unsigned int )ctr;
2751#line 131
2752 __cil_tmp15 = (unsigned int )io;
2753#line 131
2754 __cil_tmp16 = __cil_tmp15 + __cil_tmp14;
2755#line 131
2756 __cil_tmp17 = (int )__cil_tmp16;
2757#line 131
2758 outb(__cil_tmp13, __cil_tmp17);
2759#line 132
2760 __const_udelay(34360UL);
2761 }
2762#line 134
2763 return;
2764}
2765}
2766#line 141 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2767static int wdtpci_start(void)
2768{ unsigned long flags ;
2769 unsigned int __cil_tmp2 ;
2770 unsigned int __cil_tmp3 ;
2771 int __cil_tmp4 ;
2772 unsigned int __cil_tmp5 ;
2773 unsigned int __cil_tmp6 ;
2774 int __cil_tmp7 ;
2775 unsigned int __cil_tmp8 ;
2776 unsigned int __cil_tmp9 ;
2777 int __cil_tmp10 ;
2778 unsigned int __cil_tmp11 ;
2779 unsigned int __cil_tmp12 ;
2780 int __cil_tmp13 ;
2781 unsigned int __cil_tmp14 ;
2782 unsigned int __cil_tmp15 ;
2783 int __cil_tmp16 ;
2784 unsigned int __cil_tmp17 ;
2785 unsigned int __cil_tmp18 ;
2786 int __cil_tmp19 ;
2787 unsigned int __cil_tmp20 ;
2788 unsigned int __cil_tmp21 ;
2789 int __cil_tmp22 ;
2790 unsigned int __cil_tmp23 ;
2791 unsigned int __cil_tmp24 ;
2792 int __cil_tmp25 ;
2793 unsigned int __cil_tmp26 ;
2794 unsigned int __cil_tmp27 ;
2795 int __cil_tmp28 ;
2796
2797 {
2798 {
2799#line 145
2800 ldv_spin_lock();
2801#line 151
2802 __cil_tmp2 = (unsigned int )io;
2803#line 151
2804 __cil_tmp3 = __cil_tmp2 + 7U;
2805#line 151
2806 __cil_tmp4 = (int )__cil_tmp3;
2807#line 151
2808 inb(__cil_tmp4);
2809#line 152
2810 __const_udelay(34360UL);
2811#line 153
2812 wdtpci_ctr_mode(2, 0);
2813#line 155
2814 __cil_tmp5 = (unsigned int )io;
2815#line 155
2816 __cil_tmp6 = __cil_tmp5 + 7U;
2817#line 155
2818 __cil_tmp7 = (int )__cil_tmp6;
2819#line 155
2820 outb((unsigned char)0, __cil_tmp7);
2821#line 156
2822 __const_udelay(34360UL);
2823#line 157
2824 __cil_tmp8 = (unsigned int )io;
2825#line 157
2826 __cil_tmp9 = __cil_tmp8 + 7U;
2827#line 157
2828 __cil_tmp10 = (int )__cil_tmp9;
2829#line 157
2830 inb(__cil_tmp10);
2831#line 158
2832 __const_udelay(34360UL);
2833#line 159
2834 __cil_tmp11 = (unsigned int )io;
2835#line 159
2836 __cil_tmp12 = __cil_tmp11 + 12U;
2837#line 159
2838 __cil_tmp13 = (int )__cil_tmp12;
2839#line 159
2840 outb((unsigned char)0, __cil_tmp13);
2841#line 160
2842 __const_udelay(34360UL);
2843#line 161
2844 __cil_tmp14 = (unsigned int )io;
2845#line 161
2846 __cil_tmp15 = __cil_tmp14 + 6U;
2847#line 161
2848 __cil_tmp16 = (int )__cil_tmp15;
2849#line 161
2850 inb(__cil_tmp16);
2851#line 162
2852 __const_udelay(34360UL);
2853#line 163
2854 __cil_tmp17 = (unsigned int )io;
2855#line 163
2856 __cil_tmp18 = __cil_tmp17 + 13U;
2857#line 163
2858 __cil_tmp19 = (int )__cil_tmp18;
2859#line 163
2860 inb(__cil_tmp19);
2861#line 164
2862 __const_udelay(34360UL);
2863#line 165
2864 __cil_tmp20 = (unsigned int )io;
2865#line 165
2866 __cil_tmp21 = __cil_tmp20 + 14U;
2867#line 165
2868 __cil_tmp22 = (int )__cil_tmp21;
2869#line 165
2870 inb(__cil_tmp22);
2871#line 166
2872 __const_udelay(34360UL);
2873#line 167
2874 __cil_tmp23 = (unsigned int )io;
2875#line 167
2876 __cil_tmp24 = __cil_tmp23 + 15U;
2877#line 167
2878 __cil_tmp25 = (int )__cil_tmp24;
2879#line 167
2880 inb(__cil_tmp25);
2881#line 168
2882 __const_udelay(34360UL);
2883#line 169
2884 wdtpci_ctr_mode(0, 3);
2885#line 171
2886 wdtpci_ctr_mode(1, 2);
2887#line 173
2888 wdtpci_ctr_mode(2, 1);
2889#line 175
2890 wdtpci_ctr_load(0, 20833);
2891#line 176
2892 wdtpci_ctr_load(1, wd_heartbeat);
2893#line 178
2894 __cil_tmp26 = (unsigned int )io;
2895#line 178
2896 __cil_tmp27 = __cil_tmp26 + 7U;
2897#line 178
2898 __cil_tmp28 = (int )__cil_tmp27;
2899#line 178
2900 outb((unsigned char)0, __cil_tmp28);
2901#line 179
2902 __const_udelay(34360UL);
2903#line 181
2904 spin_unlock_irqrestore(& wdtpci_lock, flags);
2905 }
2906#line 182
2907 return (0);
2908}
2909}
2910#line 191 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2911static int wdtpci_stop(void)
2912{ unsigned long flags ;
2913 unsigned int __cil_tmp2 ;
2914 unsigned int __cil_tmp3 ;
2915 int __cil_tmp4 ;
2916
2917 {
2918 {
2919#line 196
2920 ldv_spin_lock();
2921#line 197
2922 __cil_tmp2 = (unsigned int )io;
2923#line 197
2924 __cil_tmp3 = __cil_tmp2 + 7U;
2925#line 197
2926 __cil_tmp4 = (int )__cil_tmp3;
2927#line 197
2928 inb(__cil_tmp4);
2929#line 198
2930 __const_udelay(34360UL);
2931#line 199
2932 wdtpci_ctr_load(2, 0);
2933#line 200
2934 spin_unlock_irqrestore(& wdtpci_lock, flags);
2935 }
2936#line 201
2937 return (0);
2938}
2939}
2940#line 211 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2941static int wdtpci_ping(void)
2942{ unsigned long flags ;
2943 unsigned int __cil_tmp2 ;
2944 unsigned int __cil_tmp3 ;
2945 int __cil_tmp4 ;
2946 unsigned int __cil_tmp5 ;
2947 unsigned int __cil_tmp6 ;
2948 int __cil_tmp7 ;
2949
2950 {
2951 {
2952#line 215
2953 ldv_spin_lock();
2954#line 217
2955 __cil_tmp2 = (unsigned int )io;
2956#line 217
2957 __cil_tmp3 = __cil_tmp2 + 7U;
2958#line 217
2959 __cil_tmp4 = (int )__cil_tmp3;
2960#line 217
2961 inb(__cil_tmp4);
2962#line 218
2963 __const_udelay(34360UL);
2964#line 219
2965 wdtpci_ctr_mode(1, 2);
2966#line 221
2967 wdtpci_ctr_load(1, wd_heartbeat);
2968#line 222
2969 __cil_tmp5 = (unsigned int )io;
2970#line 222
2971 __cil_tmp6 = __cil_tmp5 + 7U;
2972#line 222
2973 __cil_tmp7 = (int )__cil_tmp6;
2974#line 222
2975 outb((unsigned char)0, __cil_tmp7);
2976#line 223
2977 __const_udelay(34360UL);
2978#line 224
2979 spin_unlock_irqrestore(& wdtpci_lock, flags);
2980 }
2981#line 225
2982 return (0);
2983}
2984}
2985#line 236 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
2986static int wdtpci_set_heartbeat(int t )
2987{ int *__cil_tmp2 ;
2988
2989 {
2990#line 239
2991 if (t <= 0) {
2992#line 240
2993 return (-22);
2994 } else
2995#line 239
2996 if (t > 65535) {
2997#line 240
2998 return (-22);
2999 } else {
3000
3001 }
3002#line 242
3003 __cil_tmp2 = & heartbeat;
3004#line 242
3005 *__cil_tmp2 = t;
3006#line 243
3007 wd_heartbeat = t * 100;
3008#line 244
3009 return (0);
3010}
3011}
3012#line 258 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
3013static int wdtpci_get_status(int *status )
3014{ unsigned char new_status ;
3015 unsigned long flags ;
3016 unsigned int __cil_tmp4 ;
3017 unsigned int __cil_tmp5 ;
3018 int __cil_tmp6 ;
3019 int __cil_tmp7 ;
3020 int __cil_tmp8 ;
3021 int __cil_tmp9 ;
3022 int __cil_tmp10 ;
3023 int __cil_tmp11 ;
3024 int __cil_tmp12 ;
3025 int *__cil_tmp13 ;
3026 int __cil_tmp14 ;
3027 int __cil_tmp15 ;
3028 int __cil_tmp16 ;
3029 int __cil_tmp17 ;
3030 int __cil_tmp18 ;
3031 int __cil_tmp19 ;
3032 int __cil_tmp20 ;
3033 int __cil_tmp21 ;
3034 int __cil_tmp22 ;
3035 int __cil_tmp23 ;
3036 int *__cil_tmp24 ;
3037 int __cil_tmp25 ;
3038 int __cil_tmp26 ;
3039 int __cil_tmp27 ;
3040 int __cil_tmp28 ;
3041
3042 {
3043 {
3044#line 263
3045 ldv_spin_lock();
3046#line 264
3047 __cil_tmp4 = (unsigned int )io;
3048#line 264
3049 __cil_tmp5 = __cil_tmp4 + 4U;
3050#line 264
3051 __cil_tmp6 = (int )__cil_tmp5;
3052#line 264
3053 new_status = inb(__cil_tmp6);
3054#line 265
3055 spin_unlock_irqrestore(& wdtpci_lock, flags);
3056#line 267
3057 *status = 0;
3058 }
3059 {
3060#line 268
3061 __cil_tmp7 = (int )new_status;
3062#line 268
3063 __cil_tmp8 = __cil_tmp7 & 4;
3064#line 268
3065 if (__cil_tmp8 != 0) {
3066#line 269
3067 __cil_tmp9 = *status;
3068#line 269
3069 *status = __cil_tmp9 | 4;
3070 } else {
3071
3072 }
3073 }
3074 {
3075#line 270
3076 __cil_tmp10 = (int )new_status;
3077#line 270
3078 __cil_tmp11 = __cil_tmp10 & 8;
3079#line 270
3080 if (__cil_tmp11 != 0) {
3081#line 271
3082 __cil_tmp12 = *status;
3083#line 271
3084 *status = __cil_tmp12 | 8;
3085 } else {
3086
3087 }
3088 }
3089 {
3090#line 272
3091 __cil_tmp13 = & type;
3092#line 272
3093 __cil_tmp14 = *__cil_tmp13;
3094#line 272
3095 if (__cil_tmp14 == 501) {
3096 {
3097#line 273
3098 __cil_tmp15 = (int )new_status;
3099#line 273
3100 __cil_tmp16 = __cil_tmp15 & 2;
3101#line 273
3102 if (__cil_tmp16 == 0) {
3103#line 274
3104 __cil_tmp17 = *status;
3105#line 274
3106 *status = __cil_tmp17 | 1;
3107 } else {
3108
3109 }
3110 }
3111 {
3112#line 275
3113 __cil_tmp18 = (int )new_status;
3114#line 275
3115 __cil_tmp19 = __cil_tmp18 & 32;
3116#line 275
3117 if (__cil_tmp19 == 0) {
3118#line 276
3119 __cil_tmp20 = *status;
3120#line 276
3121 *status = __cil_tmp20 | 64;
3122 } else {
3123
3124 }
3125 }
3126 {
3127#line 277
3128 __cil_tmp21 = (int )new_status;
3129#line 277
3130 __cil_tmp22 = __cil_tmp21 & 64;
3131#line 277
3132 if (__cil_tmp22 == 0) {
3133#line 278
3134 __cil_tmp23 = *status;
3135#line 278
3136 *status = __cil_tmp23 | 16;
3137 } else {
3138
3139 }
3140 }
3141 {
3142#line 279
3143 __cil_tmp24 = & tachometer;
3144#line 279
3145 __cil_tmp25 = *__cil_tmp24;
3146#line 279
3147 if (__cil_tmp25 != 0) {
3148 {
3149#line 280
3150 __cil_tmp26 = (int )new_status;
3151#line 280
3152 __cil_tmp27 = __cil_tmp26 & 16;
3153#line 280
3154 if (__cil_tmp27 == 0) {
3155#line 281
3156 __cil_tmp28 = *status;
3157#line 281
3158 *status = __cil_tmp28 | 2;
3159 } else {
3160
3161 }
3162 }
3163 } else {
3164
3165 }
3166 }
3167 } else {
3168
3169 }
3170 }
3171#line 284
3172 return (0);
3173}
3174}
3175#line 294 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
3176static int wdtpci_get_temperature(int *temperature )
3177{ unsigned short c ;
3178 unsigned long flags ;
3179 unsigned char tmp ;
3180 unsigned int __cil_tmp5 ;
3181 unsigned int __cil_tmp6 ;
3182 int __cil_tmp7 ;
3183 int __cil_tmp8 ;
3184 int __cil_tmp9 ;
3185 int __cil_tmp10 ;
3186
3187 {
3188 {
3189#line 298
3190 ldv_spin_lock();
3191#line 299
3192 __cil_tmp5 = (unsigned int )io;
3193#line 299
3194 __cil_tmp6 = __cil_tmp5 + 5U;
3195#line 299
3196 __cil_tmp7 = (int )__cil_tmp6;
3197#line 299
3198 tmp = inb(__cil_tmp7);
3199#line 299
3200 c = (unsigned short )tmp;
3201#line 300
3202 __const_udelay(34360UL);
3203#line 301
3204 spin_unlock_irqrestore(& wdtpci_lock, flags);
3205#line 302
3206 __cil_tmp8 = (int )c;
3207#line 302
3208 __cil_tmp9 = __cil_tmp8 * 11;
3209#line 302
3210 __cil_tmp10 = __cil_tmp9 / 15;
3211#line 302
3212 *temperature = __cil_tmp10 + 7;
3213 }
3214#line 303
3215 return (0);
3216}
3217}
3218#line 316 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
3219static irqreturn_t wdtpci_interrupt(int irq___0 , void *dev_id )
3220{ unsigned char status ;
3221 unsigned char tmp ;
3222 unsigned int __cil_tmp5 ;
3223 unsigned int __cil_tmp6 ;
3224 int __cil_tmp7 ;
3225 int __cil_tmp8 ;
3226 int *__cil_tmp9 ;
3227 int __cil_tmp10 ;
3228 int __cil_tmp11 ;
3229 int __cil_tmp12 ;
3230 unsigned int __cil_tmp13 ;
3231 unsigned int __cil_tmp14 ;
3232 int __cil_tmp15 ;
3233 int __cil_tmp16 ;
3234 int __cil_tmp17 ;
3235 int __cil_tmp18 ;
3236 int __cil_tmp19 ;
3237 int __cil_tmp20 ;
3238 int *__cil_tmp21 ;
3239 int __cil_tmp22 ;
3240 int __cil_tmp23 ;
3241 int __cil_tmp24 ;
3242 int __cil_tmp25 ;
3243 int __cil_tmp26 ;
3244
3245 {
3246 {
3247#line 324
3248 spin_lock(& wdtpci_lock);
3249#line 326
3250 __cil_tmp5 = (unsigned int )io;
3251#line 326
3252 __cil_tmp6 = __cil_tmp5 + 4U;
3253#line 326
3254 __cil_tmp7 = (int )__cil_tmp6;
3255#line 326
3256 status = inb(__cil_tmp7);
3257#line 327
3258 __const_udelay(34360UL);
3259#line 329
3260 __cil_tmp8 = (int )status;
3261#line 329
3262 printk("<2>wdt_pci: status %d\n", __cil_tmp8);
3263 }
3264 {
3265#line 331
3266 __cil_tmp9 = & type;
3267#line 331
3268 __cil_tmp10 = *__cil_tmp9;
3269#line 331
3270 if (__cil_tmp10 == 501) {
3271 {
3272#line 332
3273 __cil_tmp11 = (int )status;
3274#line 332
3275 __cil_tmp12 = __cil_tmp11 & 2;
3276#line 332
3277 if (__cil_tmp12 == 0) {
3278 {
3279#line 333
3280 __cil_tmp13 = (unsigned int )io;
3281#line 333
3282 __cil_tmp14 = __cil_tmp13 + 5U;
3283#line 333
3284 __cil_tmp15 = (int )__cil_tmp14;
3285#line 333
3286 tmp = inb(__cil_tmp15);
3287#line 333
3288 __cil_tmp16 = (int )tmp;
3289#line 333
3290 printk("<2>wdt_pci: Overheat alarm (%d)\n", __cil_tmp16);
3291#line 334
3292 __const_udelay(34360UL);
3293 }
3294 } else {
3295
3296 }
3297 }
3298 {
3299#line 336
3300 __cil_tmp17 = (int )status;
3301#line 336
3302 __cil_tmp18 = __cil_tmp17 & 32;
3303#line 336
3304 if (__cil_tmp18 == 0) {
3305 {
3306#line 337
3307 printk("<2>wdt_pci: PSU over voltage\n");
3308 }
3309 } else {
3310
3311 }
3312 }
3313 {
3314#line 338
3315 __cil_tmp19 = (int )status;
3316#line 338
3317 __cil_tmp20 = __cil_tmp19 & 64;
3318#line 338
3319 if (__cil_tmp20 == 0) {
3320 {
3321#line 339
3322 printk("<2>wdt_pci: PSU under voltage\n");
3323 }
3324 } else {
3325
3326 }
3327 }
3328 {
3329#line 340
3330 __cil_tmp21 = & tachometer;
3331#line 340
3332 __cil_tmp22 = *__cil_tmp21;
3333#line 340
3334 if (__cil_tmp22 != 0) {
3335 {
3336#line 341
3337 __cil_tmp23 = (int )status;
3338#line 341
3339 __cil_tmp24 = __cil_tmp23 & 16;
3340#line 341
3341 if (__cil_tmp24 == 0) {
3342 {
3343#line 342
3344 printk("<2>wdt_pci: Possible fan fault\n");
3345 }
3346 } else {
3347
3348 }
3349 }
3350 } else {
3351
3352 }
3353 }
3354 } else {
3355
3356 }
3357 }
3358 {
3359#line 345
3360 __cil_tmp25 = (int )status;
3361#line 345
3362 __cil_tmp26 = __cil_tmp25 & 1;
3363#line 345
3364 if (__cil_tmp26 == 0) {
3365 {
3366#line 354
3367 printk("<2>wdt_pci: Reset in 5ms\n");
3368 }
3369 } else {
3370
3371 }
3372 }
3373 {
3374#line 357
3375 spin_unlock(& wdtpci_lock);
3376 }
3377#line 358
3378 return ((irqreturn_t )1);
3379}
3380}
3381#line 373 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
3382static ssize_t wdtpci_write(struct file *file , char const *buf , size_t count ,
3383 loff_t *ppos )
3384{ size_t i ;
3385 char c ;
3386 int __ret_gu ;
3387 unsigned long __val_gu ;
3388 bool *__cil_tmp9 ;
3389 bool __cil_tmp10 ;
3390 signed char __cil_tmp11 ;
3391 int __cil_tmp12 ;
3392
3393 {
3394#line 376
3395 if (count != 0UL) {
3396 {
3397#line 377
3398 __cil_tmp9 = & nowayout;
3399#line 377
3400 __cil_tmp10 = *__cil_tmp9;
3401#line 377
3402 if (! __cil_tmp10) {
3403#line 381
3404 expect_close = (char)0;
3405#line 383
3406 i = 0UL;
3407#line 383
3408 goto ldv_25117;
3409 ldv_25116:
3410 {
3411#line 385
3412 might_fault();
3413 }
3414#line 385
3415 if (1 == 1) {
3416#line 385
3417 goto case_1;
3418 } else
3419#line 385
3420 if (1 == 2) {
3421#line 385
3422 goto case_2;
3423 } else
3424#line 385
3425 if (1 == 4) {
3426#line 385
3427 goto case_4;
3428 } else
3429#line 385
3430 if (1 == 8) {
3431#line 385
3432 goto case_8;
3433 } else {
3434 {
3435#line 385
3436 goto switch_default;
3437#line 385
3438 if (0) {
3439 case_1:
3440#line 385
3441 __asm__ volatile ("call __get_user_1": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + i));
3442#line 385
3443 goto ldv_25110;
3444 case_2:
3445#line 385
3446 __asm__ volatile ("call __get_user_2": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + i));
3447#line 385
3448 goto ldv_25110;
3449 case_4:
3450#line 385
3451 __asm__ volatile ("call __get_user_4": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + i));
3452#line 385
3453 goto ldv_25110;
3454 case_8:
3455#line 385
3456 __asm__ volatile ("call __get_user_8": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + i));
3457#line 385
3458 goto ldv_25110;
3459 switch_default:
3460#line 385
3461 __asm__ volatile ("call __get_user_X": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + i));
3462#line 385
3463 goto ldv_25110;
3464 } else {
3465 switch_break: ;
3466 }
3467 }
3468 }
3469 ldv_25110:
3470#line 385
3471 c = (char )__val_gu;
3472#line 385
3473 if (__ret_gu != 0) {
3474#line 386
3475 return (-14L);
3476 } else {
3477
3478 }
3479 {
3480#line 387
3481 __cil_tmp11 = (signed char )c;
3482#line 387
3483 __cil_tmp12 = (int )__cil_tmp11;
3484#line 387
3485 if (__cil_tmp12 == 86) {
3486#line 388
3487 expect_close = (char)42;
3488 } else {
3489
3490 }
3491 }
3492#line 383
3493 i = i + 1UL;
3494 ldv_25117: ;
3495#line 383
3496 if (i != count) {
3497#line 384
3498 goto ldv_25116;
3499 } else {
3500#line 386
3501 goto ldv_25118;
3502 }
3503 ldv_25118: ;
3504 } else {
3505
3506 }
3507 }
3508 {
3509#line 391
3510 wdtpci_ping();
3511 }
3512 } else {
3513
3514 }
3515#line 393
3516 return ((ssize_t )count);
3517}
3518}
3519#line 407 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
3520static long wdtpci_ioctl(struct file *file , unsigned int cmd , unsigned long arg )
3521{ void *argp ;
3522 int *p ;
3523 int new_heartbeat ;
3524 int status ;
3525 struct watchdog_info ident ;
3526 long tmp___0 ;
3527 int tmp___1 ;
3528 int __ret_pu ;
3529 int __pu_val ;
3530 int __ret_pu___0 ;
3531 int __pu_val___0 ;
3532 int __ret_gu ;
3533 unsigned long __val_gu ;
3534 int tmp___2 ;
3535 int __ret_pu___1 ;
3536 int __pu_val___1 ;
3537 struct watchdog_info *__cil_tmp21 ;
3538 unsigned long __cil_tmp22 ;
3539 unsigned long __cil_tmp23 ;
3540 unsigned long __cil_tmp24 ;
3541 unsigned long __cil_tmp25 ;
3542 unsigned long __cil_tmp26 ;
3543 unsigned long __cil_tmp27 ;
3544 unsigned long __cil_tmp28 ;
3545 unsigned long __cil_tmp29 ;
3546 unsigned long __cil_tmp30 ;
3547 unsigned long __cil_tmp31 ;
3548 unsigned long __cil_tmp32 ;
3549 unsigned long __cil_tmp33 ;
3550 unsigned long __cil_tmp34 ;
3551 unsigned long __cil_tmp35 ;
3552 unsigned long __cil_tmp36 ;
3553 unsigned long __cil_tmp37 ;
3554 unsigned long __cil_tmp38 ;
3555 unsigned long __cil_tmp39 ;
3556 unsigned long __cil_tmp40 ;
3557 unsigned long __cil_tmp41 ;
3558 unsigned long __cil_tmp42 ;
3559 unsigned long __cil_tmp43 ;
3560 unsigned long __cil_tmp44 ;
3561 unsigned long __cil_tmp45 ;
3562 unsigned long __cil_tmp46 ;
3563 unsigned long __cil_tmp47 ;
3564 unsigned long __cil_tmp48 ;
3565 unsigned long __cil_tmp49 ;
3566 unsigned long __cil_tmp50 ;
3567 unsigned long __cil_tmp51 ;
3568 unsigned long __cil_tmp52 ;
3569 unsigned long __cil_tmp53 ;
3570 unsigned long __cil_tmp54 ;
3571 unsigned long __cil_tmp55 ;
3572 unsigned long __cil_tmp56 ;
3573 unsigned long __cil_tmp57 ;
3574 unsigned long __cil_tmp58 ;
3575 unsigned long __cil_tmp59 ;
3576 unsigned long __cil_tmp60 ;
3577 unsigned long __cil_tmp61 ;
3578 unsigned long __cil_tmp62 ;
3579 unsigned long __cil_tmp63 ;
3580 unsigned long __cil_tmp64 ;
3581 unsigned long __cil_tmp65 ;
3582 unsigned long __cil_tmp66 ;
3583 unsigned long __cil_tmp67 ;
3584 struct watchdog_info *__cil_tmp68 ;
3585 struct watchdog_info *__cil_tmp69 ;
3586 __u32 __cil_tmp70 ;
3587 int *__cil_tmp71 ;
3588 int __cil_tmp72 ;
3589 struct watchdog_info *__cil_tmp73 ;
3590 struct watchdog_info *__cil_tmp74 ;
3591 __u32 __cil_tmp75 ;
3592 int *__cil_tmp76 ;
3593 int __cil_tmp77 ;
3594 struct watchdog_info *__cil_tmp78 ;
3595 struct watchdog_info *__cil_tmp79 ;
3596 __u32 __cil_tmp80 ;
3597 void const *__cil_tmp81 ;
3598 int *__cil_tmp82 ;
3599 int *__cil_tmp83 ;
3600
3601 {
3602#line 410
3603 argp = (void *)arg;
3604#line 411
3605 p = (int *)argp;
3606#line 415
3607 __cil_tmp21 = & ident;
3608#line 415
3609 *((__u32 *)__cil_tmp21) = 33152U;
3610#line 415
3611 __cil_tmp22 = (unsigned long )(& ident) + 4;
3612#line 415
3613 *((__u32 *)__cil_tmp22) = 1U;
3614#line 415
3615 __cil_tmp23 = 0 * 1UL;
3616#line 415
3617 __cil_tmp24 = 8 + __cil_tmp23;
3618#line 415
3619 __cil_tmp25 = (unsigned long )(& ident) + __cil_tmp24;
3620#line 415
3621 *((__u8 *)__cil_tmp25) = (__u8 )'P';
3622#line 415
3623 __cil_tmp26 = 1 * 1UL;
3624#line 415
3625 __cil_tmp27 = 8 + __cil_tmp26;
3626#line 415
3627 __cil_tmp28 = (unsigned long )(& ident) + __cil_tmp27;
3628#line 415
3629 *((__u8 *)__cil_tmp28) = (__u8 )'C';
3630#line 415
3631 __cil_tmp29 = 2 * 1UL;
3632#line 415
3633 __cil_tmp30 = 8 + __cil_tmp29;
3634#line 415
3635 __cil_tmp31 = (unsigned long )(& ident) + __cil_tmp30;
3636#line 415
3637 *((__u8 *)__cil_tmp31) = (__u8 )'I';
3638#line 415
3639 __cil_tmp32 = 3 * 1UL;
3640#line 415
3641 __cil_tmp33 = 8 + __cil_tmp32;
3642#line 415
3643 __cil_tmp34 = (unsigned long )(& ident) + __cil_tmp33;
3644#line 415
3645 *((__u8 *)__cil_tmp34) = (__u8 )'-';
3646#line 415
3647 __cil_tmp35 = 4 * 1UL;
3648#line 415
3649 __cil_tmp36 = 8 + __cil_tmp35;
3650#line 415
3651 __cil_tmp37 = (unsigned long )(& ident) + __cil_tmp36;
3652#line 415
3653 *((__u8 *)__cil_tmp37) = (__u8 )'W';
3654#line 415
3655 __cil_tmp38 = 5 * 1UL;
3656#line 415
3657 __cil_tmp39 = 8 + __cil_tmp38;
3658#line 415
3659 __cil_tmp40 = (unsigned long )(& ident) + __cil_tmp39;
3660#line 415
3661 *((__u8 *)__cil_tmp40) = (__u8 )'D';
3662#line 415
3663 __cil_tmp41 = 6 * 1UL;
3664#line 415
3665 __cil_tmp42 = 8 + __cil_tmp41;
3666#line 415
3667 __cil_tmp43 = (unsigned long )(& ident) + __cil_tmp42;
3668#line 415
3669 *((__u8 *)__cil_tmp43) = (__u8 )'T';
3670#line 415
3671 __cil_tmp44 = 7 * 1UL;
3672#line 415
3673 __cil_tmp45 = 8 + __cil_tmp44;
3674#line 415
3675 __cil_tmp46 = (unsigned long )(& ident) + __cil_tmp45;
3676#line 415
3677 *((__u8 *)__cil_tmp46) = (__u8 )'5';
3678#line 415
3679 __cil_tmp47 = 8 * 1UL;
3680#line 415
3681 __cil_tmp48 = 8 + __cil_tmp47;
3682#line 415
3683 __cil_tmp49 = (unsigned long )(& ident) + __cil_tmp48;
3684#line 415
3685 *((__u8 *)__cil_tmp49) = (__u8 )'0';
3686#line 415
3687 __cil_tmp50 = 9 * 1UL;
3688#line 415
3689 __cil_tmp51 = 8 + __cil_tmp50;
3690#line 415
3691 __cil_tmp52 = (unsigned long )(& ident) + __cil_tmp51;
3692#line 415
3693 *((__u8 *)__cil_tmp52) = (__u8 )'0';
3694#line 415
3695 __cil_tmp53 = 10 * 1UL;
3696#line 415
3697 __cil_tmp54 = 8 + __cil_tmp53;
3698#line 415
3699 __cil_tmp55 = (unsigned long )(& ident) + __cil_tmp54;
3700#line 415
3701 *((__u8 *)__cil_tmp55) = (__u8 )'/';
3702#line 415
3703 __cil_tmp56 = 11 * 1UL;
3704#line 415
3705 __cil_tmp57 = 8 + __cil_tmp56;
3706#line 415
3707 __cil_tmp58 = (unsigned long )(& ident) + __cil_tmp57;
3708#line 415
3709 *((__u8 *)__cil_tmp58) = (__u8 )'5';
3710#line 415
3711 __cil_tmp59 = 12 * 1UL;
3712#line 415
3713 __cil_tmp60 = 8 + __cil_tmp59;
3714#line 415
3715 __cil_tmp61 = (unsigned long )(& ident) + __cil_tmp60;
3716#line 415
3717 *((__u8 *)__cil_tmp61) = (__u8 )'0';
3718#line 415
3719 __cil_tmp62 = 13 * 1UL;
3720#line 415
3721 __cil_tmp63 = 8 + __cil_tmp62;
3722#line 415
3723 __cil_tmp64 = (unsigned long )(& ident) + __cil_tmp63;
3724#line 415
3725 *((__u8 *)__cil_tmp64) = (__u8 )'1';
3726#line 415
3727 __cil_tmp65 = 14 * 1UL;
3728#line 415
3729 __cil_tmp66 = 8 + __cil_tmp65;
3730#line 415
3731 __cil_tmp67 = (unsigned long )(& ident) + __cil_tmp66;
3732#line 415
3733 *((__u8 *)__cil_tmp67) = (__u8 )'\000';
3734#line 424
3735 __cil_tmp68 = & ident;
3736#line 424
3737 __cil_tmp69 = & ident;
3738#line 424
3739 __cil_tmp70 = *((__u32 *)__cil_tmp69);
3740#line 424
3741 *((__u32 *)__cil_tmp68) = __cil_tmp70 | 12U;
3742 {
3743#line 425
3744 __cil_tmp71 = & type;
3745#line 425
3746 __cil_tmp72 = *__cil_tmp71;
3747#line 425
3748 if (__cil_tmp72 == 501) {
3749#line 426
3750 __cil_tmp73 = & ident;
3751#line 426
3752 __cil_tmp74 = & ident;
3753#line 426
3754 __cil_tmp75 = *((__u32 *)__cil_tmp74);
3755#line 426
3756 *((__u32 *)__cil_tmp73) = __cil_tmp75 | 81U;
3757 {
3758#line 428
3759 __cil_tmp76 = & tachometer;
3760#line 428
3761 __cil_tmp77 = *__cil_tmp76;
3762#line 428
3763 if (__cil_tmp77 != 0) {
3764#line 429
3765 __cil_tmp78 = & ident;
3766#line 429
3767 __cil_tmp79 = & ident;
3768#line 429
3769 __cil_tmp80 = *((__u32 *)__cil_tmp79);
3770#line 429
3771 *((__u32 *)__cil_tmp78) = __cil_tmp80 | 2U;
3772 } else {
3773
3774 }
3775 }
3776 } else {
3777
3778 }
3779 }
3780#line 433
3781 if ((int )cmd == -2144839936) {
3782#line 433
3783 goto case_neg_2144839936;
3784 } else
3785#line 435
3786 if ((int )cmd == -2147199231) {
3787#line 435
3788 goto case_neg_2147199231;
3789 } else
3790#line 438
3791 if ((int )cmd == -2147199230) {
3792#line 438
3793 goto case_neg_2147199230;
3794 } else
3795#line 440
3796 if ((int )cmd == -2147199227) {
3797#line 440
3798 goto case_neg_2147199227;
3799 } else
3800#line 443
3801 if ((int )cmd == -1073457402) {
3802#line 443
3803 goto case_neg_1073457402;
3804 } else
3805#line 450
3806 if ((int )cmd == -2147199225) {
3807#line 450
3808 goto case_neg_2147199225;
3809 } else {
3810 {
3811#line 452
3812 goto switch_default___3;
3813#line 432
3814 if (0) {
3815 case_neg_2144839936:
3816 {
3817#line 434
3818 __cil_tmp81 = (void const *)(& ident);
3819#line 434
3820 tmp___1 = copy_to_user(argp, __cil_tmp81, 40U);
3821 }
3822#line 434
3823 if (tmp___1 != 0) {
3824#line 434
3825 tmp___0 = -14L;
3826 } else {
3827#line 434
3828 tmp___0 = 0L;
3829 }
3830#line 434
3831 return (tmp___0);
3832 case_neg_2147199231:
3833 {
3834#line 436
3835 wdtpci_get_status(& status);
3836#line 437
3837 might_fault();
3838#line 437
3839 __cil_tmp82 = & status;
3840#line 437
3841 __pu_val = *__cil_tmp82;
3842 }
3843#line 437
3844 if (4 == 1) {
3845#line 437
3846 goto case_1;
3847 } else
3848#line 437
3849 if (4 == 2) {
3850#line 437
3851 goto case_2;
3852 } else
3853#line 437
3854 if (4 == 4) {
3855#line 437
3856 goto case_4;
3857 } else
3858#line 437
3859 if (4 == 8) {
3860#line 437
3861 goto case_8;
3862 } else {
3863 {
3864#line 437
3865 goto switch_default;
3866#line 437
3867 if (0) {
3868 case_1:
3869#line 437
3870 __asm__ volatile ("call __put_user_1": "=a" (__ret_pu): "0" (__pu_val),
3871 "c" (p): "ebx");
3872#line 437
3873 goto ldv_25134;
3874 case_2:
3875#line 437
3876 __asm__ volatile ("call __put_user_2": "=a" (__ret_pu): "0" (__pu_val),
3877 "c" (p): "ebx");
3878#line 437
3879 goto ldv_25134;
3880 case_4:
3881#line 437
3882 __asm__ volatile ("call __put_user_4": "=a" (__ret_pu): "0" (__pu_val),
3883 "c" (p): "ebx");
3884#line 437
3885 goto ldv_25134;
3886 case_8:
3887#line 437
3888 __asm__ volatile ("call __put_user_8": "=a" (__ret_pu): "0" (__pu_val),
3889 "c" (p): "ebx");
3890#line 437
3891 goto ldv_25134;
3892 switch_default:
3893#line 437
3894 __asm__ volatile ("call __put_user_X": "=a" (__ret_pu): "0" (__pu_val),
3895 "c" (p): "ebx");
3896#line 437
3897 goto ldv_25134;
3898 } else {
3899 switch_break___0: ;
3900 }
3901 }
3902 }
3903 ldv_25134: ;
3904#line 437
3905 return ((long )__ret_pu);
3906 case_neg_2147199230:
3907 {
3908#line 439
3909 might_fault();
3910#line 439
3911 __pu_val___0 = 0;
3912 }
3913#line 439
3914 if (4 == 1) {
3915#line 439
3916 goto case_1___0;
3917 } else
3918#line 439
3919 if (4 == 2) {
3920#line 439
3921 goto case_2___0;
3922 } else
3923#line 439
3924 if (4 == 4) {
3925#line 439
3926 goto case_4___0;
3927 } else
3928#line 439
3929 if (4 == 8) {
3930#line 439
3931 goto case_8___0;
3932 } else {
3933 {
3934#line 439
3935 goto switch_default___0;
3936#line 439
3937 if (0) {
3938 case_1___0:
3939#line 439
3940 __asm__ volatile ("call __put_user_1": "=a" (__ret_pu___0): "0" (__pu_val___0),
3941 "c" (p): "ebx");
3942#line 439
3943 goto ldv_25144;
3944 case_2___0:
3945#line 439
3946 __asm__ volatile ("call __put_user_2": "=a" (__ret_pu___0): "0" (__pu_val___0),
3947 "c" (p): "ebx");
3948#line 439
3949 goto ldv_25144;
3950 case_4___0:
3951#line 439
3952 __asm__ volatile ("call __put_user_4": "=a" (__ret_pu___0): "0" (__pu_val___0),
3953 "c" (p): "ebx");
3954#line 439
3955 goto ldv_25144;
3956 case_8___0:
3957#line 439
3958 __asm__ volatile ("call __put_user_8": "=a" (__ret_pu___0): "0" (__pu_val___0),
3959 "c" (p): "ebx");
3960#line 439
3961 goto ldv_25144;
3962 switch_default___0:
3963#line 439
3964 __asm__ volatile ("call __put_user_X": "=a" (__ret_pu___0): "0" (__pu_val___0),
3965 "c" (p): "ebx");
3966#line 439
3967 goto ldv_25144;
3968 } else {
3969 switch_break___1: ;
3970 }
3971 }
3972 }
3973 ldv_25144: ;
3974#line 439
3975 return ((long )__ret_pu___0);
3976 case_neg_2147199227:
3977 {
3978#line 441
3979 wdtpci_ping();
3980 }
3981#line 442
3982 return (0L);
3983 case_neg_1073457402:
3984 {
3985#line 444
3986 might_fault();
3987 }
3988#line 444
3989 if (4 == 1) {
3990#line 444
3991 goto case_1___1;
3992 } else
3993#line 444
3994 if (4 == 2) {
3995#line 444
3996 goto case_2___1;
3997 } else
3998#line 444
3999 if (4 == 4) {
4000#line 444
4001 goto case_4___1;
4002 } else
4003#line 444
4004 if (4 == 8) {
4005#line 444
4006 goto case_8___1;
4007 } else {
4008 {
4009#line 444
4010 goto switch_default___1;
4011#line 444
4012 if (0) {
4013 case_1___1:
4014#line 444
4015 __asm__ volatile ("call __get_user_1": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
4016#line 444
4017 goto ldv_25155;
4018 case_2___1:
4019#line 444
4020 __asm__ volatile ("call __get_user_2": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
4021#line 444
4022 goto ldv_25155;
4023 case_4___1:
4024#line 444
4025 __asm__ volatile ("call __get_user_4": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
4026#line 444
4027 goto ldv_25155;
4028 case_8___1:
4029#line 444
4030 __asm__ volatile ("call __get_user_8": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
4031#line 444
4032 goto ldv_25155;
4033 switch_default___1:
4034#line 444
4035 __asm__ volatile ("call __get_user_X": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
4036#line 444
4037 goto ldv_25155;
4038 } else {
4039 switch_break___2: ;
4040 }
4041 }
4042 }
4043 ldv_25155:
4044#line 444
4045 new_heartbeat = (int )__val_gu;
4046#line 444
4047 if (__ret_gu != 0) {
4048#line 445
4049 return (-14L);
4050 } else {
4051
4052 }
4053 {
4054#line 446
4055 tmp___2 = wdtpci_set_heartbeat(new_heartbeat);
4056 }
4057#line 446
4058 if (tmp___2 != 0) {
4059#line 447
4060 return (-22L);
4061 } else {
4062
4063 }
4064 {
4065#line 448
4066 wdtpci_ping();
4067 }
4068 case_neg_2147199225:
4069 {
4070#line 451
4071 might_fault();
4072#line 451
4073 __cil_tmp83 = & heartbeat;
4074#line 451
4075 __pu_val___1 = *__cil_tmp83;
4076 }
4077#line 451
4078 if (4 == 1) {
4079#line 451
4080 goto case_1___2;
4081 } else
4082#line 451
4083 if (4 == 2) {
4084#line 451
4085 goto case_2___2;
4086 } else
4087#line 451
4088 if (4 == 4) {
4089#line 451
4090 goto case_4___2;
4091 } else
4092#line 451
4093 if (4 == 8) {
4094#line 451
4095 goto case_8___2;
4096 } else {
4097 {
4098#line 451
4099 goto switch_default___2;
4100#line 451
4101 if (0) {
4102 case_1___2:
4103#line 451
4104 __asm__ volatile ("call __put_user_1": "=a" (__ret_pu___1): "0" (__pu_val___1),
4105 "c" (p): "ebx");
4106#line 451
4107 goto ldv_25165;
4108 case_2___2:
4109#line 451
4110 __asm__ volatile ("call __put_user_2": "=a" (__ret_pu___1): "0" (__pu_val___1),
4111 "c" (p): "ebx");
4112#line 451
4113 goto ldv_25165;
4114 case_4___2:
4115#line 451
4116 __asm__ volatile ("call __put_user_4": "=a" (__ret_pu___1): "0" (__pu_val___1),
4117 "c" (p): "ebx");
4118#line 451
4119 goto ldv_25165;
4120 case_8___2:
4121#line 451
4122 __asm__ volatile ("call __put_user_8": "=a" (__ret_pu___1): "0" (__pu_val___1),
4123 "c" (p): "ebx");
4124#line 451
4125 goto ldv_25165;
4126 switch_default___2:
4127#line 451
4128 __asm__ volatile ("call __put_user_X": "=a" (__ret_pu___1): "0" (__pu_val___1),
4129 "c" (p): "ebx");
4130#line 451
4131 goto ldv_25165;
4132 } else {
4133 switch_break___3: ;
4134 }
4135 }
4136 }
4137 ldv_25165: ;
4138#line 451
4139 return ((long )__ret_pu___1);
4140 switch_default___3: ;
4141#line 453
4142 return (-25L);
4143 } else {
4144 switch_break: ;
4145 }
4146 }
4147 }
4148}
4149}
4150#line 469 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4151static int wdtpci_open(struct inode *inode , struct file *file )
4152{ int tmp ;
4153 int tmp___0 ;
4154 unsigned long volatile *__cil_tmp5 ;
4155 bool *__cil_tmp6 ;
4156 bool __cil_tmp7 ;
4157
4158 {
4159 {
4160#line 471
4161 __cil_tmp5 = (unsigned long volatile *)(& open_lock);
4162#line 471
4163 tmp = test_and_set_bit(0, __cil_tmp5);
4164 }
4165#line 471
4166 if (tmp != 0) {
4167#line 472
4168 return (-16);
4169 } else {
4170
4171 }
4172 {
4173#line 474
4174 __cil_tmp6 = & nowayout;
4175#line 474
4176 __cil_tmp7 = *__cil_tmp6;
4177#line 474
4178 if ((int )__cil_tmp7) {
4179 {
4180#line 475
4181 __module_get(& __this_module);
4182 }
4183 } else {
4184
4185 }
4186 }
4187 {
4188#line 479
4189 wdtpci_start();
4190#line 480
4191 tmp___0 = nonseekable_open(inode, file);
4192 }
4193#line 480
4194 return (tmp___0);
4195}
4196}
4197#line 495 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4198static int wdtpci_release(struct inode *inode , struct file *file )
4199{ signed char __cil_tmp3 ;
4200 int __cil_tmp4 ;
4201 unsigned long volatile *__cil_tmp5 ;
4202
4203 {
4204 {
4205#line 497
4206 __cil_tmp3 = (signed char )expect_close;
4207#line 497
4208 __cil_tmp4 = (int )__cil_tmp3;
4209#line 497
4210 if (__cil_tmp4 == 42) {
4211 {
4212#line 498
4213 wdtpci_stop();
4214 }
4215 } else {
4216 {
4217#line 500
4218 printk("<2>wdt_pci: Unexpected close, not stopping timer!\n");
4219#line 501
4220 wdtpci_ping();
4221 }
4222 }
4223 }
4224 {
4225#line 503
4226 expect_close = (char)0;
4227#line 504
4228 __cil_tmp5 = (unsigned long volatile *)(& open_lock);
4229#line 504
4230 clear_bit(0, __cil_tmp5);
4231 }
4232#line 505
4233 return (0);
4234}
4235}
4236#line 519 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4237static ssize_t wdtpci_temp_read(struct file *file , char *buf , size_t count , loff_t *ptr )
4238{ int temperature ;
4239 int tmp ;
4240 int tmp___0 ;
4241 void *__cil_tmp8 ;
4242 void const *__cil_tmp9 ;
4243
4244 {
4245 {
4246#line 524
4247 tmp = wdtpci_get_temperature(& temperature);
4248 }
4249#line 524
4250 if (tmp != 0) {
4251#line 525
4252 return (-14L);
4253 } else {
4254
4255 }
4256 {
4257#line 527
4258 __cil_tmp8 = (void *)buf;
4259#line 527
4260 __cil_tmp9 = (void const *)(& temperature);
4261#line 527
4262 tmp___0 = copy_to_user(__cil_tmp8, __cil_tmp9, 1U);
4263 }
4264#line 527
4265 if (tmp___0 != 0) {
4266#line 528
4267 return (-14L);
4268 } else {
4269
4270 }
4271#line 530
4272 return (1L);
4273}
4274}
4275#line 541 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4276static int wdtpci_temp_open(struct inode *inode , struct file *file )
4277{ int tmp ;
4278
4279 {
4280 {
4281#line 543
4282 tmp = nonseekable_open(inode, file);
4283 }
4284#line 543
4285 return (tmp);
4286}
4287}
4288#line 554 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4289static int wdtpci_temp_release(struct inode *inode , struct file *file )
4290{
4291
4292 {
4293#line 556
4294 return (0);
4295}
4296}
4297#line 571 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4298static int wdtpci_notify_sys(struct notifier_block *this , unsigned long code , void *unused )
4299{
4300
4301 {
4302#line 574
4303 if (code == 1UL) {
4304 {
4305#line 575
4306 wdtpci_stop();
4307 }
4308 } else
4309#line 574
4310 if (code == 2UL) {
4311 {
4312#line 575
4313 wdtpci_stop();
4314 }
4315 } else {
4316
4317 }
4318#line 576
4319 return (0);
4320}
4321}
4322#line 584 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4323static struct file_operations const wdtpci_fops =
4324#line 584
4325 {& __this_module, & no_llseek, (ssize_t (*)(struct file * , char * , size_t ,
4326 loff_t * ))0, & wdtpci_write, (ssize_t (*)(struct kiocb * ,
4327 struct iovec const * ,
4328 unsigned long ,
4329 loff_t ))0,
4330 (ssize_t (*)(struct kiocb * , struct iovec const * , unsigned long , loff_t ))0,
4331 (int (*)(struct file * , void * , int (*)(void * , char const * , int , loff_t ,
4332 u64 , unsigned int ) ))0, (unsigned int (*)(struct file * ,
4333 struct poll_table_struct * ))0,
4334 & wdtpci_ioctl, (long (*)(struct file * , unsigned int , unsigned long ))0,
4335 (int (*)(struct file * , struct vm_area_struct * ))0, & wdtpci_open, (int (*)(struct file * ,
4336 fl_owner_t ))0,
4337 & wdtpci_release, (int (*)(struct file * , loff_t , loff_t , int ))0, (int (*)(struct kiocb * ,
4338 int ))0,
4339 (int (*)(int , struct file * , int ))0, (int (*)(struct file * , int , struct file_lock * ))0,
4340 (ssize_t (*)(struct file * , struct page * , int , size_t , loff_t * , int ))0,
4341 (unsigned long (*)(struct file * , unsigned long , unsigned long , unsigned long ,
4342 unsigned long ))0, (int (*)(int ))0, (int (*)(struct file * ,
4343 int , struct file_lock * ))0,
4344 (ssize_t (*)(struct pipe_inode_info * , struct file * , loff_t * , size_t , unsigned int ))0,
4345 (ssize_t (*)(struct file * , loff_t * , struct pipe_inode_info * , size_t , unsigned int ))0,
4346 (int (*)(struct file * , long , struct file_lock ** ))0, (long (*)(struct file * ,
4347 int , loff_t ,
4348 loff_t ))0};
4349#line 593 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4350static struct miscdevice wdtpci_miscdev =
4351#line 593
4352 {130, "watchdog", & wdtpci_fops, {(struct list_head *)0, (struct list_head *)0},
4353 (struct device *)0, (struct device *)0, (char const *)0, (unsigned short)0};
4354#line 599 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4355static struct file_operations const wdtpci_temp_fops =
4356#line 599
4357 {& __this_module, & no_llseek, & wdtpci_temp_read, (ssize_t (*)(struct file * ,
4358 char const * ,
4359 size_t , loff_t * ))0,
4360 (ssize_t (*)(struct kiocb * , struct iovec const * , unsigned long , loff_t ))0,
4361 (ssize_t (*)(struct kiocb * , struct iovec const * , unsigned long , loff_t ))0,
4362 (int (*)(struct file * , void * , int (*)(void * , char const * , int , loff_t ,
4363 u64 , unsigned int ) ))0, (unsigned int (*)(struct file * ,
4364 struct poll_table_struct * ))0,
4365 (long (*)(struct file * , unsigned int , unsigned long ))0, (long (*)(struct file * ,
4366 unsigned int ,
4367 unsigned long ))0,
4368 (int (*)(struct file * , struct vm_area_struct * ))0, & wdtpci_temp_open, (int (*)(struct file * ,
4369 fl_owner_t ))0,
4370 & wdtpci_temp_release, (int (*)(struct file * , loff_t , loff_t , int ))0,
4371 (int (*)(struct kiocb * , int ))0, (int (*)(int , struct file * , int ))0,
4372 (int (*)(struct file * , int , struct file_lock * ))0, (ssize_t (*)(struct file * ,
4373 struct page * ,
4374 int , size_t ,
4375 loff_t * ,
4376 int ))0,
4377 (unsigned long (*)(struct file * , unsigned long , unsigned long , unsigned long ,
4378 unsigned long ))0, (int (*)(int ))0, (int (*)(struct file * ,
4379 int , struct file_lock * ))0,
4380 (ssize_t (*)(struct pipe_inode_info * , struct file * , loff_t * , size_t , unsigned int ))0,
4381 (ssize_t (*)(struct file * , loff_t * , struct pipe_inode_info * , size_t , unsigned int ))0,
4382 (int (*)(struct file * , long , struct file_lock ** ))0, (long (*)(struct file * ,
4383 int , loff_t ,
4384 loff_t ))0};
4385#line 607 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4386static struct miscdevice temp_miscdev =
4387#line 607
4388 {131, "temperature", & wdtpci_temp_fops, {(struct list_head *)0, (struct list_head *)0},
4389 (struct device *)0, (struct device *)0, (char const *)0, (unsigned short)0};
4390#line 618 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4391static struct notifier_block wdtpci_notifier = {& wdtpci_notify_sys, (struct notifier_block *)0, 0};
4392#line 623 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4393static int wdtpci_init_one(struct pci_dev *dev , struct pci_device_id const *ent )
4394{ int ret ;
4395 int tmp ;
4396 int tmp___0 ;
4397 int tmp___1 ;
4398 int tmp___2 ;
4399 char *tmp___3 ;
4400 int *__cil_tmp9 ;
4401 int __cil_tmp10 ;
4402 int *__cil_tmp11 ;
4403 int __cil_tmp12 ;
4404 int *__cil_tmp13 ;
4405 int __cil_tmp14 ;
4406 unsigned long __cil_tmp15 ;
4407 unsigned long __cil_tmp16 ;
4408 unsigned long __cil_tmp17 ;
4409 unsigned long __cil_tmp18 ;
4410 resource_size_t __cil_tmp19 ;
4411 unsigned long __cil_tmp20 ;
4412 unsigned long __cil_tmp21 ;
4413 unsigned long __cil_tmp22 ;
4414 unsigned long __cil_tmp23 ;
4415 resource_size_t __cil_tmp24 ;
4416 unsigned long __cil_tmp25 ;
4417 unsigned long __cil_tmp26 ;
4418 unsigned int __cil_tmp27 ;
4419 unsigned long __cil_tmp28 ;
4420 unsigned long __cil_tmp29 ;
4421 unsigned long __cil_tmp30 ;
4422 unsigned long __cil_tmp31 ;
4423 unsigned int __cil_tmp32 ;
4424 void *__cil_tmp33 ;
4425 int *__cil_tmp34 ;
4426 int __cil_tmp35 ;
4427 int *__cil_tmp36 ;
4428 int __cil_tmp37 ;
4429 int *__cil_tmp38 ;
4430 int __cil_tmp39 ;
4431 bool *__cil_tmp40 ;
4432 bool __cil_tmp41 ;
4433 int __cil_tmp42 ;
4434 int *__cil_tmp43 ;
4435 int __cil_tmp44 ;
4436 int *__cil_tmp45 ;
4437 int __cil_tmp46 ;
4438 int *__cil_tmp47 ;
4439 int __cil_tmp48 ;
4440 unsigned int __cil_tmp49 ;
4441 void *__cil_tmp50 ;
4442
4443 {
4444#line 626
4445 ret = -5;
4446#line 628
4447 dev_count = dev_count + 1;
4448#line 629
4449 if (dev_count > 1) {
4450 {
4451#line 630
4452 printk("<3>wdt_pci: This driver only supports one device\n");
4453 }
4454#line 631
4455 return (-19);
4456 } else {
4457
4458 }
4459 {
4460#line 634
4461 __cil_tmp9 = & type;
4462#line 634
4463 __cil_tmp10 = *__cil_tmp9;
4464#line 634
4465 if (__cil_tmp10 != 500) {
4466 {
4467#line 634
4468 __cil_tmp11 = & type;
4469#line 634
4470 __cil_tmp12 = *__cil_tmp11;
4471#line 634
4472 if (__cil_tmp12 != 501) {
4473 {
4474#line 635
4475 __cil_tmp13 = & type;
4476#line 635
4477 __cil_tmp14 = *__cil_tmp13;
4478#line 635
4479 printk("<3>wdt_pci: unknown card type \'%d\'\n", __cil_tmp14);
4480 }
4481#line 636
4482 return (-19);
4483 } else {
4484
4485 }
4486 }
4487 } else {
4488
4489 }
4490 }
4491 {
4492#line 639
4493 tmp = pci_enable_device(dev);
4494 }
4495#line 639
4496 if (tmp != 0) {
4497 {
4498#line 640
4499 printk("<3>wdt_pci: Not possible to enable PCI Device\n");
4500 }
4501#line 641
4502 return (-19);
4503 } else {
4504
4505 }
4506 {
4507#line 644
4508 __cil_tmp15 = 2 * 56UL;
4509#line 644
4510 __cil_tmp16 = 1304 + __cil_tmp15;
4511#line 644
4512 __cil_tmp17 = (unsigned long )dev;
4513#line 644
4514 __cil_tmp18 = __cil_tmp17 + __cil_tmp16;
4515#line 644
4516 __cil_tmp19 = *((resource_size_t *)__cil_tmp18);
4517#line 644
4518 if (__cil_tmp19 == 0ULL) {
4519 {
4520#line 645
4521 printk("<3>wdt_pci: No I/O-Address for card detected\n");
4522#line 646
4523 ret = -19;
4524 }
4525#line 647
4526 goto out_pci;
4527 } else {
4528
4529 }
4530 }
4531 {
4532#line 650
4533 tmp___0 = pci_request_region(dev, 2, "wdt_pci");
4534 }
4535#line 650
4536 if (tmp___0 != 0) {
4537 {
4538#line 651
4539 __cil_tmp20 = 2 * 56UL;
4540#line 651
4541 __cil_tmp21 = 1304 + __cil_tmp20;
4542#line 651
4543 __cil_tmp22 = (unsigned long )dev;
4544#line 651
4545 __cil_tmp23 = __cil_tmp22 + __cil_tmp21;
4546#line 651
4547 __cil_tmp24 = *((resource_size_t *)__cil_tmp23);
4548#line 651
4549 printk("<3>wdt_pci: I/O address 0x%llx already in use\n", __cil_tmp24);
4550 }
4551#line 653
4552 goto out_pci;
4553 } else {
4554
4555 }
4556 {
4557#line 656
4558 __cil_tmp25 = (unsigned long )dev;
4559#line 656
4560 __cil_tmp26 = __cil_tmp25 + 1300;
4561#line 656
4562 __cil_tmp27 = *((unsigned int *)__cil_tmp26);
4563#line 656
4564 irq = (int )__cil_tmp27;
4565#line 657
4566 __cil_tmp28 = 2 * 56UL;
4567#line 657
4568 __cil_tmp29 = 1304 + __cil_tmp28;
4569#line 657
4570 __cil_tmp30 = (unsigned long )dev;
4571#line 657
4572 __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
4573#line 657
4574 io = *((resource_size_t *)__cil_tmp31);
4575#line 659
4576 __cil_tmp32 = (unsigned int )irq;
4577#line 659
4578 __cil_tmp33 = (void *)(& wdtpci_miscdev);
4579#line 659
4580 tmp___1 = request_irq(__cil_tmp32, & wdtpci_interrupt, 128UL, "wdt_pci", __cil_tmp33);
4581 }
4582#line 659
4583 if (tmp___1 != 0) {
4584 {
4585#line 661
4586 printk("<3>wdt_pci: IRQ %d is not free\n", irq);
4587 }
4588#line 662
4589 goto out_reg;
4590 } else {
4591
4592 }
4593 {
4594#line 665
4595 printk("<6>wdt_pci: PCI-WDT500/501 (PCI-WDG-CSM) driver 0.10 at 0x%llx (Interrupt %d)\n",
4596 io, irq);
4597#line 670
4598 __cil_tmp34 = & heartbeat;
4599#line 670
4600 __cil_tmp35 = *__cil_tmp34;
4601#line 670
4602 tmp___2 = wdtpci_set_heartbeat(__cil_tmp35);
4603 }
4604#line 670
4605 if (tmp___2 != 0) {
4606 {
4607#line 671
4608 wdtpci_set_heartbeat(60);
4609#line 672
4610 printk("<6>wdt_pci: heartbeat value must be 0 < heartbeat < 65536, using %d\n",
4611 60);
4612 }
4613 } else {
4614
4615 }
4616 {
4617#line 676
4618 ret = register_reboot_notifier(& wdtpci_notifier);
4619 }
4620#line 677
4621 if (ret != 0) {
4622 {
4623#line 678
4624 printk("<3>wdt_pci: cannot register reboot notifier (err=%d)\n", ret);
4625 }
4626#line 679
4627 goto out_irq;
4628 } else {
4629
4630 }
4631 {
4632#line 682
4633 __cil_tmp36 = & type;
4634#line 682
4635 __cil_tmp37 = *__cil_tmp36;
4636#line 682
4637 if (__cil_tmp37 == 501) {
4638 {
4639#line 683
4640 ret = misc_register(& temp_miscdev);
4641 }
4642#line 684
4643 if (ret != 0) {
4644 {
4645#line 685
4646 printk("<3>wdt_pci: cannot register miscdev on minor=%d (err=%d)\n", 131, ret);
4647 }
4648#line 687
4649 goto out_rbt;
4650 } else {
4651
4652 }
4653 } else {
4654
4655 }
4656 }
4657 {
4658#line 691
4659 ret = misc_register(& wdtpci_miscdev);
4660 }
4661#line 692
4662 if (ret != 0) {
4663 {
4664#line 693
4665 printk("<3>wdt_pci: cannot register miscdev on minor=%d (err=%d)\n", 130, ret);
4666 }
4667#line 695
4668 goto out_misc;
4669 } else {
4670
4671 }
4672 {
4673#line 698
4674 __cil_tmp38 = & heartbeat;
4675#line 698
4676 __cil_tmp39 = *__cil_tmp38;
4677#line 698
4678 __cil_tmp40 = & nowayout;
4679#line 698
4680 __cil_tmp41 = *__cil_tmp40;
4681#line 698
4682 __cil_tmp42 = (int )__cil_tmp41;
4683#line 698
4684 printk("<6>wdt_pci: initialized. heartbeat=%d sec (nowayout=%d)\n", __cil_tmp39,
4685 __cil_tmp42);
4686 }
4687 {
4688#line 700
4689 __cil_tmp43 = & type;
4690#line 700
4691 __cil_tmp44 = *__cil_tmp43;
4692#line 700
4693 if (__cil_tmp44 == 501) {
4694 {
4695#line 701
4696 __cil_tmp45 = & tachometer;
4697#line 701
4698 __cil_tmp46 = *__cil_tmp45;
4699#line 701
4700 if (__cil_tmp46 != 0) {
4701#line 701
4702 tmp___3 = (char *)"Enabled";
4703 } else {
4704#line 701
4705 tmp___3 = (char *)"Disabled";
4706 }
4707 }
4708 {
4709#line 701
4710 printk("<6>wdt_pci: Fan Tachometer is %s\n", tmp___3);
4711 }
4712 } else {
4713
4714 }
4715 }
4716#line 704
4717 ret = 0;
4718 out: ;
4719#line 706
4720 return (ret);
4721 out_misc: ;
4722 {
4723#line 709
4724 __cil_tmp47 = & type;
4725#line 709
4726 __cil_tmp48 = *__cil_tmp47;
4727#line 709
4728 if (__cil_tmp48 == 501) {
4729 {
4730#line 710
4731 misc_deregister(& temp_miscdev);
4732 }
4733 } else {
4734
4735 }
4736 }
4737 out_rbt:
4738 {
4739#line 712
4740 unregister_reboot_notifier(& wdtpci_notifier);
4741 }
4742 out_irq:
4743 {
4744#line 714
4745 __cil_tmp49 = (unsigned int )irq;
4746#line 714
4747 __cil_tmp50 = (void *)(& wdtpci_miscdev);
4748#line 714
4749 free_irq(__cil_tmp49, __cil_tmp50);
4750 }
4751 out_reg:
4752 {
4753#line 716
4754 pci_release_region(dev, 2);
4755 }
4756 out_pci:
4757 {
4758#line 718
4759 pci_disable_device(dev);
4760 }
4761#line 719
4762 goto out;
4763}
4764}
4765#line 723 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4766static void wdtpci_remove_one(struct pci_dev *pdev )
4767{ int *__cil_tmp2 ;
4768 int __cil_tmp3 ;
4769 unsigned int __cil_tmp4 ;
4770 void *__cil_tmp5 ;
4771
4772 {
4773 {
4774#line 727
4775 misc_deregister(& wdtpci_miscdev);
4776 }
4777 {
4778#line 728
4779 __cil_tmp2 = & type;
4780#line 728
4781 __cil_tmp3 = *__cil_tmp2;
4782#line 728
4783 if (__cil_tmp3 == 501) {
4784 {
4785#line 729
4786 misc_deregister(& temp_miscdev);
4787 }
4788 } else {
4789
4790 }
4791 }
4792 {
4793#line 730
4794 unregister_reboot_notifier(& wdtpci_notifier);
4795#line 731
4796 __cil_tmp4 = (unsigned int )irq;
4797#line 731
4798 __cil_tmp5 = (void *)(& wdtpci_miscdev);
4799#line 731
4800 free_irq(__cil_tmp4, __cil_tmp5);
4801#line 732
4802 pci_release_region(pdev, 2);
4803#line 733
4804 pci_disable_device(pdev);
4805#line 734
4806 dev_count = dev_count - 1;
4807 }
4808#line 735
4809 return;
4810}
4811}
4812#line 738 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4813static struct pci_device_id const wdtpci_pci_tbl[2U] = { {18767U, 8896U, 4294967295U, 4294967295U, 0U, 0U, 0UL},
4814 {0U, 0U, 0U, 0U, 0U, 0U, 0UL}};
4815#line 747 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4816struct pci_device_id const __mod_pci_device_table ;
4817#line 750 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4818static struct pci_driver wdtpci_driver =
4819#line 750
4820 {{(struct list_head *)0, (struct list_head *)0}, "wdt_pci", (struct pci_device_id const *)(& wdtpci_pci_tbl),
4821 & wdtpci_init_one, & wdtpci_remove_one, (int (*)(struct pci_dev * , pm_message_t ))0,
4822 (int (*)(struct pci_dev * , pm_message_t ))0, (int (*)(struct pci_dev * ))0,
4823 (int (*)(struct pci_dev * ))0, (void (*)(struct pci_dev * ))0, (struct pci_error_handlers *)0,
4824 {(char const *)0, (struct bus_type *)0, (struct module *)0, (char const *)0,
4825 (_Bool)0, (struct of_device_id const *)0, (int (*)(struct device * ))0, (int (*)(struct device * ))0,
4826 (void (*)(struct device * ))0, (int (*)(struct device * , pm_message_t ))0,
4827 (int (*)(struct device * ))0, (struct attribute_group const **)0, (struct dev_pm_ops const *)0,
4828 (struct driver_private *)0}, {{{{{{0U}}, 0U, 0U, (void *)0, {(struct lock_class_key *)0,
4829 {(struct lock_class *)0,
4830 (struct lock_class *)0},
4831 (char const *)0,
4832 0, 0UL}}}}, {(struct list_head *)0,
4833 (struct list_head *)0}}};
4834#line 768 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4835static void wdtpci_cleanup(void)
4836{
4837
4838 {
4839 {
4840#line 770
4841 pci_unregister_driver(& wdtpci_driver);
4842 }
4843#line 771
4844 return;
4845}
4846}
4847#line 782 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4848static int wdtpci_init(void)
4849{ int tmp ;
4850
4851 {
4852 {
4853#line 784
4854 tmp = __pci_register_driver(& wdtpci_driver, & __this_module, "wdt_pci");
4855 }
4856#line 784
4857 return (tmp);
4858}
4859}
4860#line 813
4861extern void ldv_check_final_state(void) ;
4862#line 816
4863extern void ldv_check_return_value(int ) ;
4864#line 819
4865extern void ldv_initialize(void) ;
4866#line 822
4867extern int __VERIFIER_nondet_int(void) ;
4868#line 825 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4869int LDV_IN_INTERRUPT ;
4870#line 828 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
4871void main(void)
4872{ struct file *var_group1 ;
4873 char const *var_wdtpci_write_9_p1 ;
4874 size_t var_wdtpci_write_9_p2 ;
4875 loff_t *var_wdtpci_write_9_p3 ;
4876 ssize_t res_wdtpci_write_9 ;
4877 unsigned int var_wdtpci_ioctl_10_p1 ;
4878 unsigned long var_wdtpci_ioctl_10_p2 ;
4879 struct inode *var_group2 ;
4880 int res_wdtpci_open_11 ;
4881 char *var_wdtpci_temp_read_13_p1 ;
4882 size_t var_wdtpci_temp_read_13_p2 ;
4883 loff_t *var_wdtpci_temp_read_13_p3 ;
4884 ssize_t res_wdtpci_temp_read_13 ;
4885 int res_wdtpci_temp_open_14 ;
4886 struct notifier_block *var_group3 ;
4887 unsigned long var_wdtpci_notify_sys_16_p1 ;
4888 void *var_wdtpci_notify_sys_16_p2 ;
4889 struct pci_dev *var_group4 ;
4890 struct pci_device_id const *var_wdtpci_init_one_17_p1 ;
4891 int res_wdtpci_init_one_17 ;
4892 int var_wdtpci_interrupt_8_p0 ;
4893 void *var_wdtpci_interrupt_8_p1 ;
4894 int ldv_s_wdtpci_fops_file_operations ;
4895 int ldv_s_wdtpci_temp_fops_file_operations ;
4896 int ldv_s_wdtpci_driver_pci_driver ;
4897 int tmp ;
4898 int tmp___0 ;
4899 int tmp___1 ;
4900 int __cil_tmp29 ;
4901 int __cil_tmp30 ;
4902
4903 {
4904 {
4905#line 1035
4906 ldv_s_wdtpci_fops_file_operations = 0;
4907#line 1038
4908 ldv_s_wdtpci_temp_fops_file_operations = 0;
4909#line 1042
4910 ldv_s_wdtpci_driver_pci_driver = 0;
4911#line 1008
4912 LDV_IN_INTERRUPT = 1;
4913#line 1017
4914 ldv_initialize();
4915#line 1033
4916 tmp = wdtpci_init();
4917 }
4918#line 1033
4919 if (tmp != 0) {
4920#line 1034
4921 goto ldv_final;
4922 } else {
4923
4924 }
4925#line 1047
4926 goto ldv_25295;
4927 ldv_25294:
4928 {
4929#line 1053
4930 tmp___0 = __VERIFIER_nondet_int();
4931 }
4932#line 1055
4933 if (tmp___0 == 0) {
4934#line 1055
4935 goto case_0;
4936 } else
4937#line 1084
4938 if (tmp___0 == 1) {
4939#line 1084
4940 goto case_1;
4941 } else
4942#line 1113
4943 if (tmp___0 == 2) {
4944#line 1113
4945 goto case_2;
4946 } else
4947#line 1139
4948 if (tmp___0 == 3) {
4949#line 1139
4950 goto case_3;
4951 } else
4952#line 1165
4953 if (tmp___0 == 4) {
4954#line 1165
4955 goto case_4;
4956 } else
4957#line 1194
4958 if (tmp___0 == 5) {
4959#line 1194
4960 goto case_5;
4961 } else
4962#line 1223
4963 if (tmp___0 == 6) {
4964#line 1223
4965 goto case_6;
4966 } else
4967#line 1249
4968 if (tmp___0 == 7) {
4969#line 1249
4970 goto case_7;
4971 } else
4972#line 1275
4973 if (tmp___0 == 8) {
4974#line 1275
4975 goto case_8;
4976 } else
4977#line 1304
4978 if (tmp___0 == 9) {
4979#line 1304
4980 goto case_9;
4981 } else {
4982 {
4983#line 1324
4984 goto switch_default;
4985#line 1053
4986 if (0) {
4987 case_0: ;
4988#line 1058
4989 if (ldv_s_wdtpci_fops_file_operations == 0) {
4990 {
4991#line 1073
4992 res_wdtpci_open_11 = wdtpci_open(var_group2, var_group1);
4993#line 1074
4994 ldv_check_return_value(res_wdtpci_open_11);
4995 }
4996#line 1075
4997 if (res_wdtpci_open_11 != 0) {
4998#line 1076
4999 goto ldv_module_exit;
5000 } else {
5001
5002 }
5003#line 1077
5004 ldv_s_wdtpci_fops_file_operations = ldv_s_wdtpci_fops_file_operations + 1;
5005 } else {
5006
5007 }
5008#line 1083
5009 goto ldv_25283;
5010 case_1: ;
5011#line 1087
5012 if (ldv_s_wdtpci_fops_file_operations == 1) {
5013 {
5014#line 1102
5015 res_wdtpci_write_9 = wdtpci_write(var_group1, var_wdtpci_write_9_p1, var_wdtpci_write_9_p2,
5016 var_wdtpci_write_9_p3);
5017#line 1103
5018 __cil_tmp29 = (int )res_wdtpci_write_9;
5019#line 1103
5020 ldv_check_return_value(__cil_tmp29);
5021 }
5022#line 1104
5023 if (res_wdtpci_write_9 < 0L) {
5024#line 1105
5025 goto ldv_module_exit;
5026 } else {
5027
5028 }
5029#line 1106
5030 ldv_s_wdtpci_fops_file_operations = ldv_s_wdtpci_fops_file_operations + 1;
5031 } else {
5032
5033 }
5034#line 1112
5035 goto ldv_25283;
5036 case_2: ;
5037#line 1116
5038 if (ldv_s_wdtpci_fops_file_operations == 2) {
5039 {
5040#line 1131
5041 wdtpci_release(var_group2, var_group1);
5042#line 1132
5043 ldv_s_wdtpci_fops_file_operations = 0;
5044 }
5045 } else {
5046
5047 }
5048#line 1138
5049 goto ldv_25283;
5050 case_3:
5051 {
5052#line 1157
5053 wdtpci_ioctl(var_group1, var_wdtpci_ioctl_10_p1, var_wdtpci_ioctl_10_p2);
5054 }
5055#line 1164
5056 goto ldv_25283;
5057 case_4: ;
5058#line 1168
5059 if (ldv_s_wdtpci_temp_fops_file_operations == 0) {
5060 {
5061#line 1183
5062 res_wdtpci_temp_open_14 = wdtpci_temp_open(var_group2, var_group1);
5063#line 1184
5064 ldv_check_return_value(res_wdtpci_temp_open_14);
5065 }
5066#line 1185
5067 if (res_wdtpci_temp_open_14 != 0) {
5068#line 1186
5069 goto ldv_module_exit;
5070 } else {
5071
5072 }
5073#line 1187
5074 ldv_s_wdtpci_temp_fops_file_operations = ldv_s_wdtpci_temp_fops_file_operations + 1;
5075 } else {
5076
5077 }
5078#line 1193
5079 goto ldv_25283;
5080 case_5: ;
5081#line 1197
5082 if (ldv_s_wdtpci_temp_fops_file_operations == 1) {
5083 {
5084#line 1212
5085 res_wdtpci_temp_read_13 = wdtpci_temp_read(var_group1, var_wdtpci_temp_read_13_p1,
5086 var_wdtpci_temp_read_13_p2, var_wdtpci_temp_read_13_p3);
5087#line 1213
5088 __cil_tmp30 = (int )res_wdtpci_temp_read_13;
5089#line 1213
5090 ldv_check_return_value(__cil_tmp30);
5091 }
5092#line 1214
5093 if (res_wdtpci_temp_read_13 < 0L) {
5094#line 1215
5095 goto ldv_module_exit;
5096 } else {
5097
5098 }
5099#line 1216
5100 ldv_s_wdtpci_temp_fops_file_operations = ldv_s_wdtpci_temp_fops_file_operations + 1;
5101 } else {
5102
5103 }
5104#line 1222
5105 goto ldv_25283;
5106 case_6: ;
5107#line 1226
5108 if (ldv_s_wdtpci_temp_fops_file_operations == 2) {
5109 {
5110#line 1241
5111 wdtpci_temp_release(var_group2, var_group1);
5112#line 1242
5113 ldv_s_wdtpci_temp_fops_file_operations = 0;
5114 }
5115 } else {
5116
5117 }
5118#line 1248
5119 goto ldv_25283;
5120 case_7:
5121 {
5122#line 1267
5123 wdtpci_notify_sys(var_group3, var_wdtpci_notify_sys_16_p1, var_wdtpci_notify_sys_16_p2);
5124 }
5125#line 1274
5126 goto ldv_25283;
5127 case_8: ;
5128#line 1278
5129 if (ldv_s_wdtpci_driver_pci_driver == 0) {
5130 {
5131#line 1293
5132 res_wdtpci_init_one_17 = wdtpci_init_one(var_group4, var_wdtpci_init_one_17_p1);
5133#line 1294
5134 ldv_check_return_value(res_wdtpci_init_one_17);
5135 }
5136#line 1295
5137 if (res_wdtpci_init_one_17 != 0) {
5138#line 1296
5139 goto ldv_module_exit;
5140 } else {
5141
5142 }
5143#line 1297
5144 ldv_s_wdtpci_driver_pci_driver = 0;
5145 } else {
5146
5147 }
5148#line 1303
5149 goto ldv_25283;
5150 case_9:
5151 {
5152#line 1307
5153 LDV_IN_INTERRUPT = 2;
5154#line 1316
5155 wdtpci_interrupt(var_wdtpci_interrupt_8_p0, var_wdtpci_interrupt_8_p1);
5156#line 1317
5157 LDV_IN_INTERRUPT = 1;
5158 }
5159#line 1323
5160 goto ldv_25283;
5161 switch_default: ;
5162#line 1324
5163 goto ldv_25283;
5164 } else {
5165 switch_break: ;
5166 }
5167 }
5168 }
5169 ldv_25283: ;
5170 ldv_25295:
5171 {
5172#line 1047
5173 tmp___1 = __VERIFIER_nondet_int();
5174 }
5175#line 1047
5176 if (tmp___1 != 0) {
5177#line 1051
5178 goto ldv_25294;
5179 } else
5180#line 1047
5181 if (ldv_s_wdtpci_fops_file_operations != 0) {
5182#line 1051
5183 goto ldv_25294;
5184 } else
5185#line 1047
5186 if (ldv_s_wdtpci_temp_fops_file_operations != 0) {
5187#line 1051
5188 goto ldv_25294;
5189 } else
5190#line 1047
5191 if (ldv_s_wdtpci_driver_pci_driver != 0) {
5192#line 1051
5193 goto ldv_25294;
5194 } else {
5195#line 1053
5196 goto ldv_25296;
5197 }
5198 ldv_25296: ;
5199 ldv_module_exit:
5200 {
5201#line 1346
5202 wdtpci_cleanup();
5203 }
5204 ldv_final:
5205 {
5206#line 1349
5207 ldv_check_final_state();
5208 }
5209#line 1352
5210 return;
5211}
5212}
5213#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5214void ldv_blast_assert(void)
5215{
5216
5217 {
5218 ERROR: ;
5219#line 6
5220 goto ERROR;
5221}
5222}
5223#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5224extern int __VERIFIER_nondet_int(void) ;
5225#line 1373 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5226int ldv_spin = 0;
5227#line 1377 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5228void ldv_check_alloc_flags(gfp_t flags )
5229{
5230
5231 {
5232#line 1380
5233 if (ldv_spin != 0) {
5234#line 1380
5235 if (flags != 32U) {
5236 {
5237#line 1380
5238 ldv_blast_assert();
5239 }
5240 } else {
5241
5242 }
5243 } else {
5244
5245 }
5246#line 1383
5247 return;
5248}
5249}
5250#line 1383
5251extern struct page *ldv_some_page(void) ;
5252#line 1386 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5253struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
5254{ struct page *tmp ;
5255
5256 {
5257#line 1389
5258 if (ldv_spin != 0) {
5259#line 1389
5260 if (flags != 32U) {
5261 {
5262#line 1389
5263 ldv_blast_assert();
5264 }
5265 } else {
5266
5267 }
5268 } else {
5269
5270 }
5271 {
5272#line 1391
5273 tmp = ldv_some_page();
5274 }
5275#line 1391
5276 return (tmp);
5277}
5278}
5279#line 1395 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5280void ldv_check_alloc_nonatomic(void)
5281{
5282
5283 {
5284#line 1398
5285 if (ldv_spin != 0) {
5286 {
5287#line 1398
5288 ldv_blast_assert();
5289 }
5290 } else {
5291
5292 }
5293#line 1401
5294 return;
5295}
5296}
5297#line 1402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5298void ldv_spin_lock(void)
5299{
5300
5301 {
5302#line 1405
5303 ldv_spin = 1;
5304#line 1406
5305 return;
5306}
5307}
5308#line 1409 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5309void ldv_spin_unlock(void)
5310{
5311
5312 {
5313#line 1412
5314 ldv_spin = 0;
5315#line 1413
5316 return;
5317}
5318}
5319#line 1416 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5320int ldv_spin_trylock(void)
5321{ int is_lock ;
5322
5323 {
5324 {
5325#line 1421
5326 is_lock = __VERIFIER_nondet_int();
5327 }
5328#line 1423
5329 if (is_lock != 0) {
5330#line 1426
5331 return (0);
5332 } else {
5333#line 1431
5334 ldv_spin = 1;
5335#line 1433
5336 return (1);
5337 }
5338}
5339}
5340#line 1437 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5341__inline static void spin_lock(spinlock_t *lock )
5342{
5343
5344 {
5345 {
5346#line 1442
5347 ldv_spin_lock();
5348#line 1444
5349 ldv_spin_lock_1(lock);
5350 }
5351#line 1445
5352 return;
5353}
5354}
5355#line 1479 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5356__inline static void spin_unlock(spinlock_t *lock )
5357{
5358
5359 {
5360 {
5361#line 1484
5362 ldv_spin_unlock();
5363#line 1486
5364 ldv_spin_unlock_5(lock);
5365 }
5366#line 1487
5367 return;
5368}
5369}
5370#line 1509 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5371__inline static void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags )
5372{
5373
5374 {
5375 {
5376#line 1515
5377 ldv_spin_unlock();
5378#line 1517
5379 ldv_spin_unlock_irqrestore_8(lock, flags);
5380 }
5381#line 1518
5382 return;
5383}
5384}
5385#line 1600 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17373/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wdt_pci.c.p"
5386void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
5387{
5388
5389 {
5390 {
5391#line 1606
5392 ldv_check_alloc_flags(ldv_func_arg2);
5393#line 1608
5394 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
5395 }
5396#line 1609
5397 return ((void *)0);
5398}
5399}