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