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 46 "include/linux/dynamic_debug.h"
120struct device;
121#line 46
122struct device;
123#line 348 "include/linux/kernel.h"
124struct pid;
125#line 348
126struct pid;
127#line 112 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/stat.h"
128struct timespec;
129#line 112
130struct timespec;
131#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
132struct page;
133#line 58
134struct page;
135#line 26 "include/asm-generic/getorder.h"
136struct task_struct;
137#line 26
138struct task_struct;
139#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
140struct file;
141#line 290
142struct file;
143#line 305
144struct seq_file;
145#line 305
146struct seq_file;
147#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
148struct arch_spinlock;
149#line 327
150struct arch_spinlock;
151#line 306 "include/linux/bitmap.h"
152struct bug_entry {
153 int bug_addr_disp ;
154 int file_disp ;
155 unsigned short line ;
156 unsigned short flags ;
157};
158#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
159struct static_key;
160#line 234
161struct static_key;
162#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
163struct kmem_cache;
164#line 23 "include/asm-generic/atomic-long.h"
165typedef atomic64_t atomic_long_t;
166#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
167typedef u16 __ticket_t;
168#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
169typedef u32 __ticketpair_t;
170#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
171struct __raw_tickets {
172 __ticket_t head ;
173 __ticket_t tail ;
174};
175#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
176union __anonunion_ldv_5907_29 {
177 __ticketpair_t head_tail ;
178 struct __raw_tickets tickets ;
179};
180#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
181struct arch_spinlock {
182 union __anonunion_ldv_5907_29 ldv_5907 ;
183};
184#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
185typedef struct arch_spinlock arch_spinlock_t;
186#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
187struct __anonstruct_ldv_5914_31 {
188 u32 read ;
189 s32 write ;
190};
191#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
192union __anonunion_arch_rwlock_t_30 {
193 s64 lock ;
194 struct __anonstruct_ldv_5914_31 ldv_5914 ;
195};
196#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
197typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
198#line 34
199struct lockdep_map;
200#line 34
201struct lockdep_map;
202#line 55 "include/linux/debug_locks.h"
203struct stack_trace {
204 unsigned int nr_entries ;
205 unsigned int max_entries ;
206 unsigned long *entries ;
207 int skip ;
208};
209#line 26 "include/linux/stacktrace.h"
210struct lockdep_subclass_key {
211 char __one_byte ;
212};
213#line 53 "include/linux/lockdep.h"
214struct lock_class_key {
215 struct lockdep_subclass_key subkeys[8U] ;
216};
217#line 59 "include/linux/lockdep.h"
218struct lock_class {
219 struct list_head hash_entry ;
220 struct list_head lock_entry ;
221 struct lockdep_subclass_key *key ;
222 unsigned int subclass ;
223 unsigned int dep_gen_id ;
224 unsigned long usage_mask ;
225 struct stack_trace usage_traces[13U] ;
226 struct list_head locks_after ;
227 struct list_head locks_before ;
228 unsigned int version ;
229 unsigned long ops ;
230 char const *name ;
231 int name_version ;
232 unsigned long contention_point[4U] ;
233 unsigned long contending_point[4U] ;
234};
235#line 144 "include/linux/lockdep.h"
236struct lockdep_map {
237 struct lock_class_key *key ;
238 struct lock_class *class_cache[2U] ;
239 char const *name ;
240 int cpu ;
241 unsigned long ip ;
242};
243#line 556 "include/linux/lockdep.h"
244struct raw_spinlock {
245 arch_spinlock_t raw_lock ;
246 unsigned int magic ;
247 unsigned int owner_cpu ;
248 void *owner ;
249 struct lockdep_map dep_map ;
250};
251#line 32 "include/linux/spinlock_types.h"
252typedef struct raw_spinlock raw_spinlock_t;
253#line 33 "include/linux/spinlock_types.h"
254struct __anonstruct_ldv_6122_33 {
255 u8 __padding[24U] ;
256 struct lockdep_map dep_map ;
257};
258#line 33 "include/linux/spinlock_types.h"
259union __anonunion_ldv_6123_32 {
260 struct raw_spinlock rlock ;
261 struct __anonstruct_ldv_6122_33 ldv_6122 ;
262};
263#line 33 "include/linux/spinlock_types.h"
264struct spinlock {
265 union __anonunion_ldv_6123_32 ldv_6123 ;
266};
267#line 76 "include/linux/spinlock_types.h"
268typedef struct spinlock spinlock_t;
269#line 23 "include/linux/rwlock_types.h"
270struct __anonstruct_rwlock_t_34 {
271 arch_rwlock_t raw_lock ;
272 unsigned int magic ;
273 unsigned int owner_cpu ;
274 void *owner ;
275 struct lockdep_map dep_map ;
276};
277#line 23 "include/linux/rwlock_types.h"
278typedef struct __anonstruct_rwlock_t_34 rwlock_t;
279#line 110 "include/linux/seqlock.h"
280struct seqcount {
281 unsigned int sequence ;
282};
283#line 121 "include/linux/seqlock.h"
284typedef struct seqcount seqcount_t;
285#line 254 "include/linux/seqlock.h"
286struct timespec {
287 __kernel_time_t tv_sec ;
288 long tv_nsec ;
289};
290#line 286 "include/linux/time.h"
291struct kstat {
292 u64 ino ;
293 dev_t dev ;
294 umode_t mode ;
295 unsigned int nlink ;
296 uid_t uid ;
297 gid_t gid ;
298 dev_t rdev ;
299 loff_t size ;
300 struct timespec atime ;
301 struct timespec mtime ;
302 struct timespec ctime ;
303 unsigned long blksize ;
304 unsigned long long blocks ;
305};
306#line 48 "include/linux/wait.h"
307struct __wait_queue_head {
308 spinlock_t lock ;
309 struct list_head task_list ;
310};
311#line 53 "include/linux/wait.h"
312typedef struct __wait_queue_head wait_queue_head_t;
313#line 670 "include/linux/mmzone.h"
314struct mutex {
315 atomic_t count ;
316 spinlock_t wait_lock ;
317 struct list_head wait_list ;
318 struct task_struct *owner ;
319 char const *name ;
320 void *magic ;
321 struct lockdep_map dep_map ;
322};
323#line 171 "include/linux/mutex.h"
324struct rw_semaphore;
325#line 171
326struct rw_semaphore;
327#line 172 "include/linux/mutex.h"
328struct rw_semaphore {
329 long count ;
330 raw_spinlock_t wait_lock ;
331 struct list_head wait_list ;
332 struct lockdep_map dep_map ;
333};
334#line 188 "include/linux/rcupdate.h"
335struct notifier_block;
336#line 188
337struct notifier_block;
338#line 239 "include/linux/srcu.h"
339struct notifier_block {
340 int (*notifier_call)(struct notifier_block * , unsigned long , void * ) ;
341 struct notifier_block *next ;
342 int priority ;
343};
344#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
345struct resource {
346 resource_size_t start ;
347 resource_size_t end ;
348 char const *name ;
349 unsigned long flags ;
350 struct resource *parent ;
351 struct resource *sibling ;
352 struct resource *child ;
353};
354#line 18 "include/asm-generic/pci_iomap.h"
355struct vm_area_struct;
356#line 18
357struct vm_area_struct;
358#line 37 "include/linux/kmod.h"
359struct cred;
360#line 37
361struct cred;
362#line 18 "include/linux/elf.h"
363typedef __u64 Elf64_Addr;
364#line 19 "include/linux/elf.h"
365typedef __u16 Elf64_Half;
366#line 23 "include/linux/elf.h"
367typedef __u32 Elf64_Word;
368#line 24 "include/linux/elf.h"
369typedef __u64 Elf64_Xword;
370#line 193 "include/linux/elf.h"
371struct elf64_sym {
372 Elf64_Word st_name ;
373 unsigned char st_info ;
374 unsigned char st_other ;
375 Elf64_Half st_shndx ;
376 Elf64_Addr st_value ;
377 Elf64_Xword st_size ;
378};
379#line 201 "include/linux/elf.h"
380typedef struct elf64_sym Elf64_Sym;
381#line 445
382struct sock;
383#line 445
384struct sock;
385#line 446
386struct kobject;
387#line 446
388struct kobject;
389#line 447
390enum kobj_ns_type {
391 KOBJ_NS_TYPE_NONE = 0,
392 KOBJ_NS_TYPE_NET = 1,
393 KOBJ_NS_TYPES = 2
394} ;
395#line 453 "include/linux/elf.h"
396struct kobj_ns_type_operations {
397 enum kobj_ns_type type ;
398 void *(*grab_current_ns)(void) ;
399 void const *(*netlink_ns)(struct sock * ) ;
400 void const *(*initial_ns)(void) ;
401 void (*drop_ns)(void * ) ;
402};
403#line 57 "include/linux/kobject_ns.h"
404struct attribute {
405 char const *name ;
406 umode_t mode ;
407 struct lock_class_key *key ;
408 struct lock_class_key skey ;
409};
410#line 98 "include/linux/sysfs.h"
411struct sysfs_ops {
412 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
413 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
414 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
415};
416#line 117
417struct sysfs_dirent;
418#line 117
419struct sysfs_dirent;
420#line 182 "include/linux/sysfs.h"
421struct kref {
422 atomic_t refcount ;
423};
424#line 49 "include/linux/kobject.h"
425struct kset;
426#line 49
427struct kobj_type;
428#line 49 "include/linux/kobject.h"
429struct kobject {
430 char const *name ;
431 struct list_head entry ;
432 struct kobject *parent ;
433 struct kset *kset ;
434 struct kobj_type *ktype ;
435 struct sysfs_dirent *sd ;
436 struct kref kref ;
437 unsigned char state_initialized : 1 ;
438 unsigned char state_in_sysfs : 1 ;
439 unsigned char state_add_uevent_sent : 1 ;
440 unsigned char state_remove_uevent_sent : 1 ;
441 unsigned char uevent_suppress : 1 ;
442};
443#line 107 "include/linux/kobject.h"
444struct kobj_type {
445 void (*release)(struct kobject * ) ;
446 struct sysfs_ops const *sysfs_ops ;
447 struct attribute **default_attrs ;
448 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
449 void const *(*namespace)(struct kobject * ) ;
450};
451#line 115 "include/linux/kobject.h"
452struct kobj_uevent_env {
453 char *envp[32U] ;
454 int envp_idx ;
455 char buf[2048U] ;
456 int buflen ;
457};
458#line 122 "include/linux/kobject.h"
459struct kset_uevent_ops {
460 int (* const filter)(struct kset * , struct kobject * ) ;
461 char const *(* const name)(struct kset * , struct kobject * ) ;
462 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
463};
464#line 139 "include/linux/kobject.h"
465struct kset {
466 struct list_head list ;
467 spinlock_t list_lock ;
468 struct kobject kobj ;
469 struct kset_uevent_ops const *uevent_ops ;
470};
471#line 215
472struct kernel_param;
473#line 215
474struct kernel_param;
475#line 216 "include/linux/kobject.h"
476struct kernel_param_ops {
477 int (*set)(char const * , struct kernel_param const * ) ;
478 int (*get)(char * , struct kernel_param const * ) ;
479 void (*free)(void * ) ;
480};
481#line 49 "include/linux/moduleparam.h"
482struct kparam_string;
483#line 49
484struct kparam_array;
485#line 49 "include/linux/moduleparam.h"
486union __anonunion_ldv_13363_134 {
487 void *arg ;
488 struct kparam_string const *str ;
489 struct kparam_array const *arr ;
490};
491#line 49 "include/linux/moduleparam.h"
492struct kernel_param {
493 char const *name ;
494 struct kernel_param_ops const *ops ;
495 u16 perm ;
496 s16 level ;
497 union __anonunion_ldv_13363_134 ldv_13363 ;
498};
499#line 61 "include/linux/moduleparam.h"
500struct kparam_string {
501 unsigned int maxlen ;
502 char *string ;
503};
504#line 67 "include/linux/moduleparam.h"
505struct kparam_array {
506 unsigned int max ;
507 unsigned int elemsize ;
508 unsigned int *num ;
509 struct kernel_param_ops const *ops ;
510 void *elem ;
511};
512#line 458 "include/linux/moduleparam.h"
513struct static_key {
514 atomic_t enabled ;
515};
516#line 225 "include/linux/jump_label.h"
517struct tracepoint;
518#line 225
519struct tracepoint;
520#line 226 "include/linux/jump_label.h"
521struct tracepoint_func {
522 void *func ;
523 void *data ;
524};
525#line 29 "include/linux/tracepoint.h"
526struct tracepoint {
527 char const *name ;
528 struct static_key key ;
529 void (*regfunc)(void) ;
530 void (*unregfunc)(void) ;
531 struct tracepoint_func *funcs ;
532};
533#line 86 "include/linux/tracepoint.h"
534struct kernel_symbol {
535 unsigned long value ;
536 char const *name ;
537};
538#line 27 "include/linux/export.h"
539struct mod_arch_specific {
540
541};
542#line 34 "include/linux/module.h"
543struct module_param_attrs;
544#line 34 "include/linux/module.h"
545struct module_kobject {
546 struct kobject kobj ;
547 struct module *mod ;
548 struct kobject *drivers_dir ;
549 struct module_param_attrs *mp ;
550};
551#line 43 "include/linux/module.h"
552struct module_attribute {
553 struct attribute attr ;
554 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
555 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
556 size_t ) ;
557 void (*setup)(struct module * , char const * ) ;
558 int (*test)(struct module * ) ;
559 void (*free)(struct module * ) ;
560};
561#line 69
562struct exception_table_entry;
563#line 69
564struct exception_table_entry;
565#line 198
566enum module_state {
567 MODULE_STATE_LIVE = 0,
568 MODULE_STATE_COMING = 1,
569 MODULE_STATE_GOING = 2
570} ;
571#line 204 "include/linux/module.h"
572struct module_ref {
573 unsigned long incs ;
574 unsigned long decs ;
575};
576#line 219
577struct module_sect_attrs;
578#line 219
579struct module_notes_attrs;
580#line 219
581struct ftrace_event_call;
582#line 219 "include/linux/module.h"
583struct module {
584 enum module_state state ;
585 struct list_head list ;
586 char name[56U] ;
587 struct module_kobject mkobj ;
588 struct module_attribute *modinfo_attrs ;
589 char const *version ;
590 char const *srcversion ;
591 struct kobject *holders_dir ;
592 struct kernel_symbol const *syms ;
593 unsigned long const *crcs ;
594 unsigned int num_syms ;
595 struct kernel_param *kp ;
596 unsigned int num_kp ;
597 unsigned int num_gpl_syms ;
598 struct kernel_symbol const *gpl_syms ;
599 unsigned long const *gpl_crcs ;
600 struct kernel_symbol const *unused_syms ;
601 unsigned long const *unused_crcs ;
602 unsigned int num_unused_syms ;
603 unsigned int num_unused_gpl_syms ;
604 struct kernel_symbol const *unused_gpl_syms ;
605 unsigned long const *unused_gpl_crcs ;
606 struct kernel_symbol const *gpl_future_syms ;
607 unsigned long const *gpl_future_crcs ;
608 unsigned int num_gpl_future_syms ;
609 unsigned int num_exentries ;
610 struct exception_table_entry *extable ;
611 int (*init)(void) ;
612 void *module_init ;
613 void *module_core ;
614 unsigned int init_size ;
615 unsigned int core_size ;
616 unsigned int init_text_size ;
617 unsigned int core_text_size ;
618 unsigned int init_ro_size ;
619 unsigned int core_ro_size ;
620 struct mod_arch_specific arch ;
621 unsigned int taints ;
622 unsigned int num_bugs ;
623 struct list_head bug_list ;
624 struct bug_entry *bug_table ;
625 Elf64_Sym *symtab ;
626 Elf64_Sym *core_symtab ;
627 unsigned int num_symtab ;
628 unsigned int core_num_syms ;
629 char *strtab ;
630 char *core_strtab ;
631 struct module_sect_attrs *sect_attrs ;
632 struct module_notes_attrs *notes_attrs ;
633 char *args ;
634 void *percpu ;
635 unsigned int percpu_size ;
636 unsigned int num_tracepoints ;
637 struct tracepoint * const *tracepoints_ptrs ;
638 unsigned int num_trace_bprintk_fmt ;
639 char const **trace_bprintk_fmt_start ;
640 struct ftrace_event_call **trace_events ;
641 unsigned int num_trace_events ;
642 struct list_head source_list ;
643 struct list_head target_list ;
644 struct task_struct *waiter ;
645 void (*exit)(void) ;
646 struct module_ref *refptr ;
647 ctor_fn_t (**ctors)(void) ;
648 unsigned int num_ctors ;
649};
650#line 88 "include/linux/kmemleak.h"
651struct kmem_cache_cpu {
652 void **freelist ;
653 unsigned long tid ;
654 struct page *page ;
655 struct page *partial ;
656 int node ;
657 unsigned int stat[26U] ;
658};
659#line 55 "include/linux/slub_def.h"
660struct kmem_cache_node {
661 spinlock_t list_lock ;
662 unsigned long nr_partial ;
663 struct list_head partial ;
664 atomic_long_t nr_slabs ;
665 atomic_long_t total_objects ;
666 struct list_head full ;
667};
668#line 66 "include/linux/slub_def.h"
669struct kmem_cache_order_objects {
670 unsigned long x ;
671};
672#line 76 "include/linux/slub_def.h"
673struct kmem_cache {
674 struct kmem_cache_cpu *cpu_slab ;
675 unsigned long flags ;
676 unsigned long min_partial ;
677 int size ;
678 int objsize ;
679 int offset ;
680 int cpu_partial ;
681 struct kmem_cache_order_objects oo ;
682 struct kmem_cache_order_objects max ;
683 struct kmem_cache_order_objects min ;
684 gfp_t allocflags ;
685 int refcount ;
686 void (*ctor)(void * ) ;
687 int inuse ;
688 int align ;
689 int reserved ;
690 char const *name ;
691 struct list_head list ;
692 struct kobject kobj ;
693 int remote_node_defrag_ratio ;
694 struct kmem_cache_node *node[1024U] ;
695};
696#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
697struct file_operations;
698#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
699struct miscdevice {
700 int minor ;
701 char const *name ;
702 struct file_operations const *fops ;
703 struct list_head list ;
704 struct device *parent ;
705 struct device *this_device ;
706 char const *nodename ;
707 umode_t mode ;
708};
709#line 63 "include/linux/miscdevice.h"
710struct watchdog_info {
711 __u32 options ;
712 __u32 firmware_version ;
713 __u8 identity[32U] ;
714};
715#line 57 "include/linux/delay.h"
716struct block_device;
717#line 57
718struct block_device;
719#line 93 "include/linux/bit_spinlock.h"
720struct hlist_bl_node;
721#line 93 "include/linux/bit_spinlock.h"
722struct hlist_bl_head {
723 struct hlist_bl_node *first ;
724};
725#line 36 "include/linux/list_bl.h"
726struct hlist_bl_node {
727 struct hlist_bl_node *next ;
728 struct hlist_bl_node **pprev ;
729};
730#line 114 "include/linux/rculist_bl.h"
731struct nameidata;
732#line 114
733struct nameidata;
734#line 115
735struct path;
736#line 115
737struct path;
738#line 116
739struct vfsmount;
740#line 116
741struct vfsmount;
742#line 117 "include/linux/rculist_bl.h"
743struct qstr {
744 unsigned int hash ;
745 unsigned int len ;
746 unsigned char const *name ;
747};
748#line 72 "include/linux/dcache.h"
749struct inode;
750#line 72
751struct dentry_operations;
752#line 72
753struct super_block;
754#line 72 "include/linux/dcache.h"
755union __anonunion_d_u_135 {
756 struct list_head d_child ;
757 struct rcu_head d_rcu ;
758};
759#line 72 "include/linux/dcache.h"
760struct dentry {
761 unsigned int d_flags ;
762 seqcount_t d_seq ;
763 struct hlist_bl_node d_hash ;
764 struct dentry *d_parent ;
765 struct qstr d_name ;
766 struct inode *d_inode ;
767 unsigned char d_iname[32U] ;
768 unsigned int d_count ;
769 spinlock_t d_lock ;
770 struct dentry_operations const *d_op ;
771 struct super_block *d_sb ;
772 unsigned long d_time ;
773 void *d_fsdata ;
774 struct list_head d_lru ;
775 union __anonunion_d_u_135 d_u ;
776 struct list_head d_subdirs ;
777 struct list_head d_alias ;
778};
779#line 123 "include/linux/dcache.h"
780struct dentry_operations {
781 int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
782 int (*d_hash)(struct dentry const * , struct inode const * , struct qstr * ) ;
783 int (*d_compare)(struct dentry const * , struct inode const * , struct dentry const * ,
784 struct inode const * , unsigned int , char const * , struct qstr const * ) ;
785 int (*d_delete)(struct dentry const * ) ;
786 void (*d_release)(struct dentry * ) ;
787 void (*d_prune)(struct dentry * ) ;
788 void (*d_iput)(struct dentry * , struct inode * ) ;
789 char *(*d_dname)(struct dentry * , char * , int ) ;
790 struct vfsmount *(*d_automount)(struct path * ) ;
791 int (*d_manage)(struct dentry * , bool ) ;
792};
793#line 402 "include/linux/dcache.h"
794struct path {
795 struct vfsmount *mnt ;
796 struct dentry *dentry ;
797};
798#line 58 "include/linux/radix-tree.h"
799struct radix_tree_node;
800#line 58 "include/linux/radix-tree.h"
801struct radix_tree_root {
802 unsigned int height ;
803 gfp_t gfp_mask ;
804 struct radix_tree_node *rnode ;
805};
806#line 377
807struct prio_tree_node;
808#line 19 "include/linux/prio_tree.h"
809struct prio_tree_node {
810 struct prio_tree_node *left ;
811 struct prio_tree_node *right ;
812 struct prio_tree_node *parent ;
813 unsigned long start ;
814 unsigned long last ;
815};
816#line 27 "include/linux/prio_tree.h"
817struct prio_tree_root {
818 struct prio_tree_node *prio_tree_node ;
819 unsigned short index_bits ;
820 unsigned short raw ;
821};
822#line 111
823enum pid_type {
824 PIDTYPE_PID = 0,
825 PIDTYPE_PGID = 1,
826 PIDTYPE_SID = 2,
827 PIDTYPE_MAX = 3
828} ;
829#line 118
830struct pid_namespace;
831#line 118 "include/linux/prio_tree.h"
832struct upid {
833 int nr ;
834 struct pid_namespace *ns ;
835 struct hlist_node pid_chain ;
836};
837#line 56 "include/linux/pid.h"
838struct pid {
839 atomic_t count ;
840 unsigned int level ;
841 struct hlist_head tasks[3U] ;
842 struct rcu_head rcu ;
843 struct upid numbers[1U] ;
844};
845#line 45 "include/linux/semaphore.h"
846struct fiemap_extent {
847 __u64 fe_logical ;
848 __u64 fe_physical ;
849 __u64 fe_length ;
850 __u64 fe_reserved64[2U] ;
851 __u32 fe_flags ;
852 __u32 fe_reserved[3U] ;
853};
854#line 38 "include/linux/fiemap.h"
855struct shrink_control {
856 gfp_t gfp_mask ;
857 unsigned long nr_to_scan ;
858};
859#line 14 "include/linux/shrinker.h"
860struct shrinker {
861 int (*shrink)(struct shrinker * , struct shrink_control * ) ;
862 int seeks ;
863 long batch ;
864 struct list_head list ;
865 atomic_long_t nr_in_batch ;
866};
867#line 43
868enum migrate_mode {
869 MIGRATE_ASYNC = 0,
870 MIGRATE_SYNC_LIGHT = 1,
871 MIGRATE_SYNC = 2
872} ;
873#line 49
874struct export_operations;
875#line 49
876struct export_operations;
877#line 51
878struct iovec;
879#line 51
880struct iovec;
881#line 52
882struct kiocb;
883#line 52
884struct kiocb;
885#line 53
886struct pipe_inode_info;
887#line 53
888struct pipe_inode_info;
889#line 54
890struct poll_table_struct;
891#line 54
892struct poll_table_struct;
893#line 55
894struct kstatfs;
895#line 55
896struct kstatfs;
897#line 435 "include/linux/fs.h"
898struct iattr {
899 unsigned int ia_valid ;
900 umode_t ia_mode ;
901 uid_t ia_uid ;
902 gid_t ia_gid ;
903 loff_t ia_size ;
904 struct timespec ia_atime ;
905 struct timespec ia_mtime ;
906 struct timespec ia_ctime ;
907 struct file *ia_file ;
908};
909#line 119 "include/linux/quota.h"
910struct if_dqinfo {
911 __u64 dqi_bgrace ;
912 __u64 dqi_igrace ;
913 __u32 dqi_flags ;
914 __u32 dqi_valid ;
915};
916#line 176 "include/linux/percpu_counter.h"
917struct fs_disk_quota {
918 __s8 d_version ;
919 __s8 d_flags ;
920 __u16 d_fieldmask ;
921 __u32 d_id ;
922 __u64 d_blk_hardlimit ;
923 __u64 d_blk_softlimit ;
924 __u64 d_ino_hardlimit ;
925 __u64 d_ino_softlimit ;
926 __u64 d_bcount ;
927 __u64 d_icount ;
928 __s32 d_itimer ;
929 __s32 d_btimer ;
930 __u16 d_iwarns ;
931 __u16 d_bwarns ;
932 __s32 d_padding2 ;
933 __u64 d_rtb_hardlimit ;
934 __u64 d_rtb_softlimit ;
935 __u64 d_rtbcount ;
936 __s32 d_rtbtimer ;
937 __u16 d_rtbwarns ;
938 __s16 d_padding3 ;
939 char d_padding4[8U] ;
940};
941#line 75 "include/linux/dqblk_xfs.h"
942struct fs_qfilestat {
943 __u64 qfs_ino ;
944 __u64 qfs_nblks ;
945 __u32 qfs_nextents ;
946};
947#line 150 "include/linux/dqblk_xfs.h"
948typedef struct fs_qfilestat fs_qfilestat_t;
949#line 151 "include/linux/dqblk_xfs.h"
950struct fs_quota_stat {
951 __s8 qs_version ;
952 __u16 qs_flags ;
953 __s8 qs_pad ;
954 fs_qfilestat_t qs_uquota ;
955 fs_qfilestat_t qs_gquota ;
956 __u32 qs_incoredqs ;
957 __s32 qs_btimelimit ;
958 __s32 qs_itimelimit ;
959 __s32 qs_rtbtimelimit ;
960 __u16 qs_bwarnlimit ;
961 __u16 qs_iwarnlimit ;
962};
963#line 165
964struct dquot;
965#line 165
966struct dquot;
967#line 185 "include/linux/quota.h"
968typedef __kernel_uid32_t qid_t;
969#line 186 "include/linux/quota.h"
970typedef long long qsize_t;
971#line 189 "include/linux/quota.h"
972struct mem_dqblk {
973 qsize_t dqb_bhardlimit ;
974 qsize_t dqb_bsoftlimit ;
975 qsize_t dqb_curspace ;
976 qsize_t dqb_rsvspace ;
977 qsize_t dqb_ihardlimit ;
978 qsize_t dqb_isoftlimit ;
979 qsize_t dqb_curinodes ;
980 time_t dqb_btime ;
981 time_t dqb_itime ;
982};
983#line 211
984struct quota_format_type;
985#line 211
986struct quota_format_type;
987#line 212 "include/linux/quota.h"
988struct mem_dqinfo {
989 struct quota_format_type *dqi_format ;
990 int dqi_fmt_id ;
991 struct list_head dqi_dirty_list ;
992 unsigned long dqi_flags ;
993 unsigned int dqi_bgrace ;
994 unsigned int dqi_igrace ;
995 qsize_t dqi_maxblimit ;
996 qsize_t dqi_maxilimit ;
997 void *dqi_priv ;
998};
999#line 275 "include/linux/quota.h"
1000struct dquot {
1001 struct hlist_node dq_hash ;
1002 struct list_head dq_inuse ;
1003 struct list_head dq_free ;
1004 struct list_head dq_dirty ;
1005 struct mutex dq_lock ;
1006 atomic_t dq_count ;
1007 wait_queue_head_t dq_wait_unused ;
1008 struct super_block *dq_sb ;
1009 unsigned int dq_id ;
1010 loff_t dq_off ;
1011 unsigned long dq_flags ;
1012 short dq_type ;
1013 struct mem_dqblk dq_dqb ;
1014};
1015#line 303 "include/linux/quota.h"
1016struct quota_format_ops {
1017 int (*check_quota_file)(struct super_block * , int ) ;
1018 int (*read_file_info)(struct super_block * , int ) ;
1019 int (*write_file_info)(struct super_block * , int ) ;
1020 int (*free_file_info)(struct super_block * , int ) ;
1021 int (*read_dqblk)(struct dquot * ) ;
1022 int (*commit_dqblk)(struct dquot * ) ;
1023 int (*release_dqblk)(struct dquot * ) ;
1024};
1025#line 314 "include/linux/quota.h"
1026struct dquot_operations {
1027 int (*write_dquot)(struct dquot * ) ;
1028 struct dquot *(*alloc_dquot)(struct super_block * , int ) ;
1029 void (*destroy_dquot)(struct dquot * ) ;
1030 int (*acquire_dquot)(struct dquot * ) ;
1031 int (*release_dquot)(struct dquot * ) ;
1032 int (*mark_dirty)(struct dquot * ) ;
1033 int (*write_info)(struct super_block * , int ) ;
1034 qsize_t *(*get_reserved_space)(struct inode * ) ;
1035};
1036#line 328 "include/linux/quota.h"
1037struct quotactl_ops {
1038 int (*quota_on)(struct super_block * , int , int , struct path * ) ;
1039 int (*quota_on_meta)(struct super_block * , int , int ) ;
1040 int (*quota_off)(struct super_block * , int ) ;
1041 int (*quota_sync)(struct super_block * , int , int ) ;
1042 int (*get_info)(struct super_block * , int , struct if_dqinfo * ) ;
1043 int (*set_info)(struct super_block * , int , struct if_dqinfo * ) ;
1044 int (*get_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1045 int (*set_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1046 int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1047 int (*set_xstate)(struct super_block * , unsigned int , int ) ;
1048};
1049#line 344 "include/linux/quota.h"
1050struct quota_format_type {
1051 int qf_fmt_id ;
1052 struct quota_format_ops const *qf_ops ;
1053 struct module *qf_owner ;
1054 struct quota_format_type *qf_next ;
1055};
1056#line 390 "include/linux/quota.h"
1057struct quota_info {
1058 unsigned int flags ;
1059 struct mutex dqio_mutex ;
1060 struct mutex dqonoff_mutex ;
1061 struct rw_semaphore dqptr_sem ;
1062 struct inode *files[2U] ;
1063 struct mem_dqinfo info[2U] ;
1064 struct quota_format_ops const *ops[2U] ;
1065};
1066#line 421
1067struct address_space;
1068#line 421
1069struct address_space;
1070#line 422
1071struct writeback_control;
1072#line 422
1073struct writeback_control;
1074#line 585 "include/linux/fs.h"
1075union __anonunion_arg_138 {
1076 char *buf ;
1077 void *data ;
1078};
1079#line 585 "include/linux/fs.h"
1080struct __anonstruct_read_descriptor_t_137 {
1081 size_t written ;
1082 size_t count ;
1083 union __anonunion_arg_138 arg ;
1084 int error ;
1085};
1086#line 585 "include/linux/fs.h"
1087typedef struct __anonstruct_read_descriptor_t_137 read_descriptor_t;
1088#line 588 "include/linux/fs.h"
1089struct address_space_operations {
1090 int (*writepage)(struct page * , struct writeback_control * ) ;
1091 int (*readpage)(struct file * , struct page * ) ;
1092 int (*writepages)(struct address_space * , struct writeback_control * ) ;
1093 int (*set_page_dirty)(struct page * ) ;
1094 int (*readpages)(struct file * , struct address_space * , struct list_head * ,
1095 unsigned int ) ;
1096 int (*write_begin)(struct file * , struct address_space * , loff_t , unsigned int ,
1097 unsigned int , struct page ** , void ** ) ;
1098 int (*write_end)(struct file * , struct address_space * , loff_t , unsigned int ,
1099 unsigned int , struct page * , void * ) ;
1100 sector_t (*bmap)(struct address_space * , sector_t ) ;
1101 void (*invalidatepage)(struct page * , unsigned long ) ;
1102 int (*releasepage)(struct page * , gfp_t ) ;
1103 void (*freepage)(struct page * ) ;
1104 ssize_t (*direct_IO)(int , struct kiocb * , struct iovec const * , loff_t ,
1105 unsigned long ) ;
1106 int (*get_xip_mem)(struct address_space * , unsigned long , int , void ** , unsigned long * ) ;
1107 int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode ) ;
1108 int (*launder_page)(struct page * ) ;
1109 int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long ) ;
1110 int (*error_remove_page)(struct address_space * , struct page * ) ;
1111};
1112#line 642
1113struct backing_dev_info;
1114#line 642
1115struct backing_dev_info;
1116#line 643 "include/linux/fs.h"
1117struct address_space {
1118 struct inode *host ;
1119 struct radix_tree_root page_tree ;
1120 spinlock_t tree_lock ;
1121 unsigned int i_mmap_writable ;
1122 struct prio_tree_root i_mmap ;
1123 struct list_head i_mmap_nonlinear ;
1124 struct mutex i_mmap_mutex ;
1125 unsigned long nrpages ;
1126 unsigned long writeback_index ;
1127 struct address_space_operations const *a_ops ;
1128 unsigned long flags ;
1129 struct backing_dev_info *backing_dev_info ;
1130 spinlock_t private_lock ;
1131 struct list_head private_list ;
1132 struct address_space *assoc_mapping ;
1133};
1134#line 664
1135struct request_queue;
1136#line 664
1137struct request_queue;
1138#line 665
1139struct hd_struct;
1140#line 665
1141struct gendisk;
1142#line 665 "include/linux/fs.h"
1143struct block_device {
1144 dev_t bd_dev ;
1145 int bd_openers ;
1146 struct inode *bd_inode ;
1147 struct super_block *bd_super ;
1148 struct mutex bd_mutex ;
1149 struct list_head bd_inodes ;
1150 void *bd_claiming ;
1151 void *bd_holder ;
1152 int bd_holders ;
1153 bool bd_write_holder ;
1154 struct list_head bd_holder_disks ;
1155 struct block_device *bd_contains ;
1156 unsigned int bd_block_size ;
1157 struct hd_struct *bd_part ;
1158 unsigned int bd_part_count ;
1159 int bd_invalidated ;
1160 struct gendisk *bd_disk ;
1161 struct request_queue *bd_queue ;
1162 struct list_head bd_list ;
1163 unsigned long bd_private ;
1164 int bd_fsfreeze_count ;
1165 struct mutex bd_fsfreeze_mutex ;
1166};
1167#line 737
1168struct posix_acl;
1169#line 737
1170struct posix_acl;
1171#line 738
1172struct inode_operations;
1173#line 738 "include/linux/fs.h"
1174union __anonunion_ldv_15837_139 {
1175 unsigned int const i_nlink ;
1176 unsigned int __i_nlink ;
1177};
1178#line 738 "include/linux/fs.h"
1179union __anonunion_ldv_15856_140 {
1180 struct list_head i_dentry ;
1181 struct rcu_head i_rcu ;
1182};
1183#line 738
1184struct file_lock;
1185#line 738
1186struct cdev;
1187#line 738 "include/linux/fs.h"
1188union __anonunion_ldv_15873_141 {
1189 struct pipe_inode_info *i_pipe ;
1190 struct block_device *i_bdev ;
1191 struct cdev *i_cdev ;
1192};
1193#line 738 "include/linux/fs.h"
1194struct inode {
1195 umode_t i_mode ;
1196 unsigned short i_opflags ;
1197 uid_t i_uid ;
1198 gid_t i_gid ;
1199 unsigned int i_flags ;
1200 struct posix_acl *i_acl ;
1201 struct posix_acl *i_default_acl ;
1202 struct inode_operations const *i_op ;
1203 struct super_block *i_sb ;
1204 struct address_space *i_mapping ;
1205 void *i_security ;
1206 unsigned long i_ino ;
1207 union __anonunion_ldv_15837_139 ldv_15837 ;
1208 dev_t i_rdev ;
1209 struct timespec i_atime ;
1210 struct timespec i_mtime ;
1211 struct timespec i_ctime ;
1212 spinlock_t i_lock ;
1213 unsigned short i_bytes ;
1214 blkcnt_t i_blocks ;
1215 loff_t i_size ;
1216 unsigned long i_state ;
1217 struct mutex i_mutex ;
1218 unsigned long dirtied_when ;
1219 struct hlist_node i_hash ;
1220 struct list_head i_wb_list ;
1221 struct list_head i_lru ;
1222 struct list_head i_sb_list ;
1223 union __anonunion_ldv_15856_140 ldv_15856 ;
1224 atomic_t i_count ;
1225 unsigned int i_blkbits ;
1226 u64 i_version ;
1227 atomic_t i_dio_count ;
1228 atomic_t i_writecount ;
1229 struct file_operations const *i_fop ;
1230 struct file_lock *i_flock ;
1231 struct address_space i_data ;
1232 struct dquot *i_dquot[2U] ;
1233 struct list_head i_devices ;
1234 union __anonunion_ldv_15873_141 ldv_15873 ;
1235 __u32 i_generation ;
1236 __u32 i_fsnotify_mask ;
1237 struct hlist_head i_fsnotify_marks ;
1238 atomic_t i_readcount ;
1239 void *i_private ;
1240};
1241#line 941 "include/linux/fs.h"
1242struct fown_struct {
1243 rwlock_t lock ;
1244 struct pid *pid ;
1245 enum pid_type pid_type ;
1246 uid_t uid ;
1247 uid_t euid ;
1248 int signum ;
1249};
1250#line 949 "include/linux/fs.h"
1251struct file_ra_state {
1252 unsigned long start ;
1253 unsigned int size ;
1254 unsigned int async_size ;
1255 unsigned int ra_pages ;
1256 unsigned int mmap_miss ;
1257 loff_t prev_pos ;
1258};
1259#line 972 "include/linux/fs.h"
1260union __anonunion_f_u_142 {
1261 struct list_head fu_list ;
1262 struct rcu_head fu_rcuhead ;
1263};
1264#line 972 "include/linux/fs.h"
1265struct file {
1266 union __anonunion_f_u_142 f_u ;
1267 struct path f_path ;
1268 struct file_operations const *f_op ;
1269 spinlock_t f_lock ;
1270 int f_sb_list_cpu ;
1271 atomic_long_t f_count ;
1272 unsigned int f_flags ;
1273 fmode_t f_mode ;
1274 loff_t f_pos ;
1275 struct fown_struct f_owner ;
1276 struct cred const *f_cred ;
1277 struct file_ra_state f_ra ;
1278 u64 f_version ;
1279 void *f_security ;
1280 void *private_data ;
1281 struct list_head f_ep_links ;
1282 struct list_head f_tfile_llink ;
1283 struct address_space *f_mapping ;
1284 unsigned long f_mnt_write_state ;
1285};
1286#line 1111
1287struct files_struct;
1288#line 1111 "include/linux/fs.h"
1289typedef struct files_struct *fl_owner_t;
1290#line 1112 "include/linux/fs.h"
1291struct file_lock_operations {
1292 void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1293 void (*fl_release_private)(struct file_lock * ) ;
1294};
1295#line 1117 "include/linux/fs.h"
1296struct lock_manager_operations {
1297 int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1298 void (*lm_notify)(struct file_lock * ) ;
1299 int (*lm_grant)(struct file_lock * , struct file_lock * , int ) ;
1300 void (*lm_release_private)(struct file_lock * ) ;
1301 void (*lm_break)(struct file_lock * ) ;
1302 int (*lm_change)(struct file_lock ** , int ) ;
1303};
1304#line 1134
1305struct nlm_lockowner;
1306#line 1134
1307struct nlm_lockowner;
1308#line 1135 "include/linux/fs.h"
1309struct nfs_lock_info {
1310 u32 state ;
1311 struct nlm_lockowner *owner ;
1312 struct list_head list ;
1313};
1314#line 14 "include/linux/nfs_fs_i.h"
1315struct nfs4_lock_state;
1316#line 14
1317struct nfs4_lock_state;
1318#line 15 "include/linux/nfs_fs_i.h"
1319struct nfs4_lock_info {
1320 struct nfs4_lock_state *owner ;
1321};
1322#line 19
1323struct fasync_struct;
1324#line 19 "include/linux/nfs_fs_i.h"
1325struct __anonstruct_afs_144 {
1326 struct list_head link ;
1327 int state ;
1328};
1329#line 19 "include/linux/nfs_fs_i.h"
1330union __anonunion_fl_u_143 {
1331 struct nfs_lock_info nfs_fl ;
1332 struct nfs4_lock_info nfs4_fl ;
1333 struct __anonstruct_afs_144 afs ;
1334};
1335#line 19 "include/linux/nfs_fs_i.h"
1336struct file_lock {
1337 struct file_lock *fl_next ;
1338 struct list_head fl_link ;
1339 struct list_head fl_block ;
1340 fl_owner_t fl_owner ;
1341 unsigned int fl_flags ;
1342 unsigned char fl_type ;
1343 unsigned int fl_pid ;
1344 struct pid *fl_nspid ;
1345 wait_queue_head_t fl_wait ;
1346 struct file *fl_file ;
1347 loff_t fl_start ;
1348 loff_t fl_end ;
1349 struct fasync_struct *fl_fasync ;
1350 unsigned long fl_break_time ;
1351 unsigned long fl_downgrade_time ;
1352 struct file_lock_operations const *fl_ops ;
1353 struct lock_manager_operations const *fl_lmops ;
1354 union __anonunion_fl_u_143 fl_u ;
1355};
1356#line 1221 "include/linux/fs.h"
1357struct fasync_struct {
1358 spinlock_t fa_lock ;
1359 int magic ;
1360 int fa_fd ;
1361 struct fasync_struct *fa_next ;
1362 struct file *fa_file ;
1363 struct rcu_head fa_rcu ;
1364};
1365#line 1417
1366struct file_system_type;
1367#line 1417
1368struct super_operations;
1369#line 1417
1370struct xattr_handler;
1371#line 1417
1372struct mtd_info;
1373#line 1417 "include/linux/fs.h"
1374struct super_block {
1375 struct list_head s_list ;
1376 dev_t s_dev ;
1377 unsigned char s_dirt ;
1378 unsigned char s_blocksize_bits ;
1379 unsigned long s_blocksize ;
1380 loff_t s_maxbytes ;
1381 struct file_system_type *s_type ;
1382 struct super_operations const *s_op ;
1383 struct dquot_operations const *dq_op ;
1384 struct quotactl_ops const *s_qcop ;
1385 struct export_operations const *s_export_op ;
1386 unsigned long s_flags ;
1387 unsigned long s_magic ;
1388 struct dentry *s_root ;
1389 struct rw_semaphore s_umount ;
1390 struct mutex s_lock ;
1391 int s_count ;
1392 atomic_t s_active ;
1393 void *s_security ;
1394 struct xattr_handler const **s_xattr ;
1395 struct list_head s_inodes ;
1396 struct hlist_bl_head s_anon ;
1397 struct list_head *s_files ;
1398 struct list_head s_mounts ;
1399 struct list_head s_dentry_lru ;
1400 int s_nr_dentry_unused ;
1401 spinlock_t s_inode_lru_lock ;
1402 struct list_head s_inode_lru ;
1403 int s_nr_inodes_unused ;
1404 struct block_device *s_bdev ;
1405 struct backing_dev_info *s_bdi ;
1406 struct mtd_info *s_mtd ;
1407 struct hlist_node s_instances ;
1408 struct quota_info s_dquot ;
1409 int s_frozen ;
1410 wait_queue_head_t s_wait_unfrozen ;
1411 char s_id[32U] ;
1412 u8 s_uuid[16U] ;
1413 void *s_fs_info ;
1414 unsigned int s_max_links ;
1415 fmode_t s_mode ;
1416 u32 s_time_gran ;
1417 struct mutex s_vfs_rename_mutex ;
1418 char *s_subtype ;
1419 char *s_options ;
1420 struct dentry_operations const *s_d_op ;
1421 int cleancache_poolid ;
1422 struct shrinker s_shrink ;
1423 atomic_long_t s_remove_count ;
1424 int s_readonly_remount ;
1425};
1426#line 1563 "include/linux/fs.h"
1427struct fiemap_extent_info {
1428 unsigned int fi_flags ;
1429 unsigned int fi_extents_mapped ;
1430 unsigned int fi_extents_max ;
1431 struct fiemap_extent *fi_extents_start ;
1432};
1433#line 1602 "include/linux/fs.h"
1434struct file_operations {
1435 struct module *owner ;
1436 loff_t (*llseek)(struct file * , loff_t , int ) ;
1437 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ;
1438 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ;
1439 ssize_t (*aio_read)(struct kiocb * , struct iovec const * , unsigned long ,
1440 loff_t ) ;
1441 ssize_t (*aio_write)(struct kiocb * , struct iovec const * , unsigned long ,
1442 loff_t ) ;
1443 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int ,
1444 loff_t , u64 , unsigned int ) ) ;
1445 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1446 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
1447 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
1448 int (*mmap)(struct file * , struct vm_area_struct * ) ;
1449 int (*open)(struct inode * , struct file * ) ;
1450 int (*flush)(struct file * , fl_owner_t ) ;
1451 int (*release)(struct inode * , struct file * ) ;
1452 int (*fsync)(struct file * , loff_t , loff_t , int ) ;
1453 int (*aio_fsync)(struct kiocb * , int ) ;
1454 int (*fasync)(int , struct file * , int ) ;
1455 int (*lock)(struct file * , int , struct file_lock * ) ;
1456 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * ,
1457 int ) ;
1458 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
1459 unsigned long , unsigned long ) ;
1460 int (*check_flags)(int ) ;
1461 int (*flock)(struct file * , int , struct file_lock * ) ;
1462 ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t ,
1463 unsigned int ) ;
1464 ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t ,
1465 unsigned int ) ;
1466 int (*setlease)(struct file * , long , struct file_lock ** ) ;
1467 long (*fallocate)(struct file * , int , loff_t , loff_t ) ;
1468};
1469#line 1637 "include/linux/fs.h"
1470struct inode_operations {
1471 struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1472 void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1473 int (*permission)(struct inode * , int ) ;
1474 struct posix_acl *(*get_acl)(struct inode * , int ) ;
1475 int (*readlink)(struct dentry * , char * , int ) ;
1476 void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
1477 int (*create)(struct inode * , struct dentry * , umode_t , struct nameidata * ) ;
1478 int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
1479 int (*unlink)(struct inode * , struct dentry * ) ;
1480 int (*symlink)(struct inode * , struct dentry * , char const * ) ;
1481 int (*mkdir)(struct inode * , struct dentry * , umode_t ) ;
1482 int (*rmdir)(struct inode * , struct dentry * ) ;
1483 int (*mknod)(struct inode * , struct dentry * , umode_t , dev_t ) ;
1484 int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
1485 void (*truncate)(struct inode * ) ;
1486 int (*setattr)(struct dentry * , struct iattr * ) ;
1487 int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
1488 int (*setxattr)(struct dentry * , char const * , void const * , size_t , int ) ;
1489 ssize_t (*getxattr)(struct dentry * , char const * , void * , size_t ) ;
1490 ssize_t (*listxattr)(struct dentry * , char * , size_t ) ;
1491 int (*removexattr)(struct dentry * , char const * ) ;
1492 void (*truncate_range)(struct inode * , loff_t , loff_t ) ;
1493 int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 , u64 ) ;
1494};
1495#line 1682 "include/linux/fs.h"
1496struct super_operations {
1497 struct inode *(*alloc_inode)(struct super_block * ) ;
1498 void (*destroy_inode)(struct inode * ) ;
1499 void (*dirty_inode)(struct inode * , int ) ;
1500 int (*write_inode)(struct inode * , struct writeback_control * ) ;
1501 int (*drop_inode)(struct inode * ) ;
1502 void (*evict_inode)(struct inode * ) ;
1503 void (*put_super)(struct super_block * ) ;
1504 void (*write_super)(struct super_block * ) ;
1505 int (*sync_fs)(struct super_block * , int ) ;
1506 int (*freeze_fs)(struct super_block * ) ;
1507 int (*unfreeze_fs)(struct super_block * ) ;
1508 int (*statfs)(struct dentry * , struct kstatfs * ) ;
1509 int (*remount_fs)(struct super_block * , int * , char * ) ;
1510 void (*umount_begin)(struct super_block * ) ;
1511 int (*show_options)(struct seq_file * , struct dentry * ) ;
1512 int (*show_devname)(struct seq_file * , struct dentry * ) ;
1513 int (*show_path)(struct seq_file * , struct dentry * ) ;
1514 int (*show_stats)(struct seq_file * , struct dentry * ) ;
1515 ssize_t (*quota_read)(struct super_block * , int , char * , size_t , loff_t ) ;
1516 ssize_t (*quota_write)(struct super_block * , int , char const * , size_t ,
1517 loff_t ) ;
1518 int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t ) ;
1519 int (*nr_cached_objects)(struct super_block * ) ;
1520 void (*free_cached_objects)(struct super_block * , int ) ;
1521};
1522#line 1834 "include/linux/fs.h"
1523struct file_system_type {
1524 char const *name ;
1525 int fs_flags ;
1526 struct dentry *(*mount)(struct file_system_type * , int , char const * , void * ) ;
1527 void (*kill_sb)(struct super_block * ) ;
1528 struct module *owner ;
1529 struct file_system_type *next ;
1530 struct hlist_head fs_supers ;
1531 struct lock_class_key s_lock_key ;
1532 struct lock_class_key s_umount_key ;
1533 struct lock_class_key s_vfs_rename_key ;
1534 struct lock_class_key i_lock_key ;
1535 struct lock_class_key i_mutex_key ;
1536 struct lock_class_key i_mutex_dir_key ;
1537};
1538#line 69 "include/linux/io.h"
1539struct exception_table_entry {
1540 unsigned long insn ;
1541 unsigned long fixup ;
1542};
1543#line 446 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1544union __anonunion_uarg_146 {
1545 struct watchdog_info *ident ;
1546 int *i ;
1547};
1548#line 2
1549void ldv_spin_lock(void) ;
1550#line 3
1551void ldv_spin_unlock(void) ;
1552#line 4
1553int ldv_spin_trylock(void) ;
1554#line 98 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
1555__inline static void clear_bit(int nr , unsigned long volatile *addr )
1556{ long volatile *__cil_tmp3 ;
1557
1558 {
1559#line 105
1560 __cil_tmp3 = (long volatile *)addr;
1561#line 105
1562 __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));
1563#line 107
1564 return;
1565}
1566}
1567#line 195 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
1568__inline static int test_and_set_bit(int nr , unsigned long volatile *addr )
1569{ int oldbit ;
1570 long volatile *__cil_tmp4 ;
1571
1572 {
1573#line 199
1574 __cil_tmp4 = (long volatile *)addr;
1575#line 199
1576 __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),
1577 "+m" (*__cil_tmp4): "Ir" (nr): "memory");
1578#line 202
1579 return (oldbit);
1580}
1581}
1582#line 101 "include/linux/printk.h"
1583extern int printk(char const * , ...) ;
1584#line 192 "include/linux/kernel.h"
1585extern void might_fault(void) ;
1586#line 22 "include/linux/spinlock_api_smp.h"
1587extern void _raw_spin_lock(raw_spinlock_t * ) ;
1588#line 39
1589extern void _raw_spin_unlock(raw_spinlock_t * ) ;
1590#line 283 "include/linux/spinlock.h"
1591__inline static void ldv_spin_lock_1(spinlock_t *lock )
1592{ struct raw_spinlock *__cil_tmp2 ;
1593
1594 {
1595 {
1596#line 285
1597 __cil_tmp2 = (struct raw_spinlock *)lock;
1598#line 285
1599 _raw_spin_lock(__cil_tmp2);
1600 }
1601#line 286
1602 return;
1603}
1604}
1605#line 283
1606__inline static void spin_lock(spinlock_t *lock ) ;
1607#line 323 "include/linux/spinlock.h"
1608__inline static void ldv_spin_unlock_5(spinlock_t *lock )
1609{ struct raw_spinlock *__cil_tmp2 ;
1610
1611 {
1612 {
1613#line 325
1614 __cil_tmp2 = (struct raw_spinlock *)lock;
1615#line 325
1616 _raw_spin_unlock(__cil_tmp2);
1617 }
1618#line 326
1619 return;
1620}
1621}
1622#line 323
1623__inline static void spin_unlock(spinlock_t *lock ) ;
1624#line 137 "include/linux/ioport.h"
1625extern struct resource ioport_resource ;
1626#line 181
1627extern struct resource *__request_region(struct resource * , resource_size_t , resource_size_t ,
1628 char const * , int ) ;
1629#line 192
1630extern void __release_region(struct resource * , resource_size_t , resource_size_t ) ;
1631#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1632__inline static void outb(unsigned char value , int port )
1633{
1634
1635 {
1636#line 308
1637 __asm__ volatile ("outb %b0, %w1": : "a" (value), "Nd" (port));
1638#line 309
1639 return;
1640}
1641}
1642#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1643__inline static unsigned char inb(int port )
1644{ unsigned char value ;
1645
1646 {
1647#line 308
1648 __asm__ volatile ("inb %w1, %b0": "=a" (value): "Nd" (port));
1649#line 308
1650 return (value);
1651}
1652}
1653#line 26 "include/linux/export.h"
1654extern struct module __this_module ;
1655#line 453 "include/linux/module.h"
1656extern void __module_get(struct module * ) ;
1657#line 220 "include/linux/slub_def.h"
1658extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1659#line 223
1660void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1661#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1662void ldv_check_alloc_flags(gfp_t flags ) ;
1663#line 12
1664void ldv_check_alloc_nonatomic(void) ;
1665#line 14
1666struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1667#line 61 "include/linux/miscdevice.h"
1668extern int misc_register(struct miscdevice * ) ;
1669#line 62
1670extern int misc_deregister(struct miscdevice * ) ;
1671#line 10 "include/asm-generic/delay.h"
1672extern void __const_udelay(unsigned long ) ;
1673#line 2402 "include/linux/fs.h"
1674extern loff_t no_llseek(struct file * , loff_t , int ) ;
1675#line 2407
1676extern int nonseekable_open(struct inode * , struct file * ) ;
1677#line 47 "include/linux/reboot.h"
1678extern int register_reboot_notifier(struct notifier_block * ) ;
1679#line 48
1680extern int unregister_reboot_notifier(struct notifier_block * ) ;
1681#line 40 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess_64.h"
1682extern unsigned long _copy_to_user(void * , void const * , unsigned int ) ;
1683#line 63 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess_64.h"
1684__inline static int copy_to_user(void *dst , void const *src , unsigned int size )
1685{ unsigned long tmp ;
1686
1687 {
1688 {
1689#line 65
1690 might_fault();
1691#line 67
1692 tmp = _copy_to_user(dst, src, size);
1693 }
1694#line 67
1695 return ((int )tmp);
1696}
1697}
1698#line 95 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1699static int unit = 0;
1700#line 96 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1701static int timeout = 60;
1702#line 97 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1703static unsigned long timer_enabled ;
1704#line 99 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1705static char expect_close ;
1706#line 101 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1707static spinlock_t io_lock = {{{{{0U}}, 3735899821U, 4294967295U, (void *)0xffffffffffffffffUL, {(struct lock_class_key *)0,
1708 {(struct lock_class *)0,
1709 (struct lock_class *)0},
1710 "io_lock",
1711 0, 0UL}}}};
1712#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1713static bool nowayout = (bool )1;
1714#line 109 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1715__inline static void open_io_config(void)
1716{ unsigned long __ms ;
1717 unsigned long tmp ;
1718
1719 {
1720 {
1721#line 111
1722 outb((unsigned char)85, 1008);
1723 }
1724#line 112
1725 if (1) {
1726 {
1727#line 112
1728 __const_udelay(4295000UL);
1729 }
1730 } else {
1731#line 112
1732 __ms = 1UL;
1733#line 112
1734 goto ldv_18031;
1735 ldv_18030:
1736 {
1737#line 112
1738 __const_udelay(4295000UL);
1739 }
1740 ldv_18031:
1741#line 112
1742 tmp = __ms;
1743#line 112
1744 __ms = __ms - 1UL;
1745#line 112
1746 if (tmp != 0UL) {
1747#line 113
1748 goto ldv_18030;
1749 } else {
1750#line 115
1751 goto ldv_18032;
1752 }
1753 ldv_18032: ;
1754 }
1755 {
1756#line 113
1757 outb((unsigned char)85, 1008);
1758 }
1759#line 114
1760 return;
1761}
1762}
1763#line 117 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1764__inline static void close_io_config(void)
1765{
1766
1767 {
1768 {
1769#line 119
1770 outb((unsigned char)170, 1008);
1771 }
1772#line 120
1773 return;
1774}
1775}
1776#line 123 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1777__inline static void select_io_device(unsigned char devno )
1778{ int __cil_tmp2 ;
1779 unsigned char __cil_tmp3 ;
1780
1781 {
1782 {
1783#line 125
1784 outb((unsigned char)7, 1008);
1785#line 126
1786 __cil_tmp2 = (int )devno;
1787#line 126
1788 __cil_tmp3 = (unsigned char )__cil_tmp2;
1789#line 126
1790 outb(__cil_tmp3, 1009);
1791 }
1792#line 127
1793 return;
1794}
1795}
1796#line 130 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1797__inline static void write_io_cr(unsigned char reg , unsigned char data )
1798{ int __cil_tmp3 ;
1799 unsigned char __cil_tmp4 ;
1800 int __cil_tmp5 ;
1801 unsigned char __cil_tmp6 ;
1802
1803 {
1804 {
1805#line 132
1806 __cil_tmp3 = (int )reg;
1807#line 132
1808 __cil_tmp4 = (unsigned char )__cil_tmp3;
1809#line 132
1810 outb(__cil_tmp4, 1008);
1811#line 133
1812 __cil_tmp5 = (int )data;
1813#line 133
1814 __cil_tmp6 = (unsigned char )__cil_tmp5;
1815#line 133
1816 outb(__cil_tmp6, 1009);
1817 }
1818#line 134
1819 return;
1820}
1821}
1822#line 137 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1823__inline static char read_io_cr(unsigned char reg )
1824{ unsigned char tmp ;
1825 int __cil_tmp3 ;
1826 unsigned char __cil_tmp4 ;
1827
1828 {
1829 {
1830#line 139
1831 __cil_tmp3 = (int )reg;
1832#line 139
1833 __cil_tmp4 = (unsigned char )__cil_tmp3;
1834#line 139
1835 outb(__cil_tmp4, 1008);
1836#line 140
1837 tmp = inb(1009);
1838 }
1839#line 140
1840 return ((char )tmp);
1841}
1842}
1843#line 145 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1844__inline static void gpio_bit12(unsigned char reg )
1845{ int __cil_tmp2 ;
1846 unsigned char __cil_tmp3 ;
1847
1848 {
1849 {
1850#line 156
1851 __cil_tmp2 = (int )reg;
1852#line 156
1853 __cil_tmp3 = (unsigned char )__cil_tmp2;
1854#line 156
1855 write_io_cr((unsigned char)226, __cil_tmp3);
1856 }
1857#line 157
1858 return;
1859}
1860}
1861#line 159 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1862__inline static void gpio_bit13(unsigned char reg )
1863{ int __cil_tmp2 ;
1864 unsigned char __cil_tmp3 ;
1865
1866 {
1867 {
1868#line 169
1869 __cil_tmp2 = (int )reg;
1870#line 169
1871 __cil_tmp3 = (unsigned char )__cil_tmp2;
1872#line 169
1873 write_io_cr((unsigned char)227, __cil_tmp3);
1874 }
1875#line 170
1876 return;
1877}
1878}
1879#line 172 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1880__inline static void wdt_timer_units(unsigned char new_units )
1881{ int __cil_tmp2 ;
1882 unsigned char __cil_tmp3 ;
1883
1884 {
1885 {
1886#line 179
1887 __cil_tmp2 = (int )new_units;
1888#line 179
1889 __cil_tmp3 = (unsigned char )__cil_tmp2;
1890#line 179
1891 write_io_cr((unsigned char)241, __cil_tmp3);
1892 }
1893#line 180
1894 return;
1895}
1896}
1897#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1898__inline static void wdt_timeout_value(unsigned char new_timeout )
1899{ int __cil_tmp2 ;
1900 unsigned char __cil_tmp3 ;
1901
1902 {
1903 {
1904#line 187
1905 __cil_tmp2 = (int )new_timeout;
1906#line 187
1907 __cil_tmp3 = (unsigned char )__cil_tmp2;
1908#line 187
1909 write_io_cr((unsigned char)242, __cil_tmp3);
1910 }
1911#line 188
1912 return;
1913}
1914}
1915#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1916__inline static void wdt_timer_conf(unsigned char conf )
1917{ int __cil_tmp2 ;
1918 unsigned char __cil_tmp3 ;
1919
1920 {
1921 {
1922#line 203
1923 __cil_tmp2 = (int )conf;
1924#line 203
1925 __cil_tmp3 = (unsigned char )__cil_tmp2;
1926#line 203
1927 write_io_cr((unsigned char)243, __cil_tmp3);
1928 }
1929#line 204
1930 return;
1931}
1932}
1933#line 206 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1934__inline static void wdt_timer_ctrl(unsigned char reg )
1935{ int __cil_tmp2 ;
1936 unsigned char __cil_tmp3 ;
1937
1938 {
1939 {
1940#line 225
1941 __cil_tmp2 = (int )reg;
1942#line 225
1943 __cil_tmp3 = (unsigned char )__cil_tmp2;
1944#line 225
1945 write_io_cr((unsigned char)244, __cil_tmp3);
1946 }
1947#line 226
1948 return;
1949}
1950}
1951#line 232 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
1952static void wb_smsc_wdt_initialize(void)
1953{ unsigned char old ;
1954 char tmp ;
1955 unsigned char __cil_tmp3 ;
1956 unsigned int __cil_tmp4 ;
1957 unsigned int __cil_tmp5 ;
1958 unsigned int __cil_tmp6 ;
1959 unsigned int __cil_tmp7 ;
1960 int __cil_tmp8 ;
1961 unsigned char __cil_tmp9 ;
1962
1963 {
1964 {
1965#line 236
1966 spin_lock(& io_lock);
1967#line 237
1968 open_io_config();
1969#line 238
1970 select_io_device((unsigned char)8);
1971#line 241
1972 gpio_bit13((unsigned char)8);
1973#line 242
1974 gpio_bit12((unsigned char)10);
1975#line 245
1976 wdt_timeout_value((unsigned char)0);
1977#line 248
1978 wdt_timer_ctrl((unsigned char)0);
1979#line 251
1980 wdt_timer_conf((unsigned char)0);
1981#line 254
1982 tmp = read_io_cr((unsigned char)241);
1983#line 254
1984 __cil_tmp3 = (unsigned char )tmp;
1985#line 254
1986 __cil_tmp4 = (unsigned int )__cil_tmp3;
1987#line 254
1988 __cil_tmp5 = __cil_tmp4 & 127U;
1989#line 254
1990 old = (unsigned char )__cil_tmp5;
1991 }
1992#line 255
1993 if (unit == 0) {
1994#line 256
1995 __cil_tmp6 = (unsigned int )old;
1996#line 256
1997 __cil_tmp7 = __cil_tmp6 | 128U;
1998#line 256
1999 old = (unsigned char )__cil_tmp7;
2000 } else {
2001
2002 }
2003 {
2004#line 259
2005 __cil_tmp8 = (int )old;
2006#line 259
2007 __cil_tmp9 = (unsigned char )__cil_tmp8;
2008#line 259
2009 wdt_timer_units(__cil_tmp9);
2010#line 261
2011 close_io_config();
2012#line 262
2013 spin_unlock(& io_lock);
2014 }
2015#line 263
2016 return;
2017}
2018}
2019#line 267 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
2020static void wb_smsc_wdt_shutdown(void)
2021{
2022
2023 {
2024 {
2025#line 269
2026 spin_lock(& io_lock);
2027#line 270
2028 open_io_config();
2029#line 271
2030 select_io_device((unsigned char)8);
2031#line 274
2032 gpio_bit13((unsigned char)9);
2033#line 275
2034 gpio_bit12((unsigned char)9);
2035#line 278
2036 wdt_timer_conf((unsigned char)0);
2037#line 281
2038 wdt_timer_ctrl((unsigned char)0);
2039#line 284
2040 wdt_timeout_value((unsigned char)0);
2041#line 286
2042 close_io_config();
2043#line 287
2044 spin_unlock(& io_lock);
2045 }
2046#line 288
2047 return;
2048}
2049}
2050#line 292 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
2051static void wb_smsc_wdt_set_timeout(unsigned char new_timeout )
2052{ int tmp ;
2053 unsigned int __cil_tmp3 ;
2054 unsigned char __cil_tmp4 ;
2055 int __cil_tmp5 ;
2056 unsigned char __cil_tmp6 ;
2057
2058 {
2059 {
2060#line 294
2061 spin_lock(& io_lock);
2062#line 295
2063 open_io_config();
2064#line 296
2065 select_io_device((unsigned char)8);
2066 }
2067 {
2068#line 299
2069 __cil_tmp3 = (unsigned int )new_timeout;
2070#line 299
2071 if (__cil_tmp3 == 0U) {
2072#line 299
2073 tmp = 0;
2074 } else {
2075#line 299
2076 tmp = 2;
2077 }
2078 }
2079 {
2080#line 299
2081 __cil_tmp4 = (unsigned char )tmp;
2082#line 299
2083 wdt_timer_ctrl(__cil_tmp4);
2084#line 302
2085 __cil_tmp5 = (int )new_timeout;
2086#line 302
2087 __cil_tmp6 = (unsigned char )__cil_tmp5;
2088#line 302
2089 wdt_timeout_value(__cil_tmp6);
2090#line 304
2091 close_io_config();
2092#line 305
2093 spin_unlock(& io_lock);
2094 }
2095#line 306
2096 return;
2097}
2098}
2099#line 310 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
2100static unsigned char wb_smsc_wdt_get_timeout(void)
2101{ unsigned char set_timeout ;
2102 char tmp ;
2103
2104 {
2105 {
2106#line 314
2107 spin_lock(& io_lock);
2108#line 315
2109 open_io_config();
2110#line 316
2111 select_io_device((unsigned char)8);
2112#line 317
2113 tmp = read_io_cr((unsigned char)242);
2114#line 317
2115 set_timeout = (unsigned char )tmp;
2116#line 318
2117 close_io_config();
2118#line 319
2119 spin_unlock(& io_lock);
2120 }
2121#line 321
2122 return (set_timeout);
2123}
2124}
2125#line 326 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
2126static void wb_smsc_wdt_disable(void)
2127{
2128
2129 {
2130 {
2131#line 329
2132 wb_smsc_wdt_set_timeout((unsigned char)0);
2133 }
2134#line 330
2135 return;
2136}
2137}
2138#line 334 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
2139static void wb_smsc_wdt_enable(void)
2140{ int *__cil_tmp1 ;
2141 int __cil_tmp2 ;
2142 unsigned char __cil_tmp3 ;
2143 int __cil_tmp4 ;
2144 unsigned char __cil_tmp5 ;
2145
2146 {
2147 {
2148#line 337
2149 __cil_tmp1 = & timeout;
2150#line 337
2151 __cil_tmp2 = *__cil_tmp1;
2152#line 337
2153 __cil_tmp3 = (unsigned char )__cil_tmp2;
2154#line 337
2155 __cil_tmp4 = (int )__cil_tmp3;
2156#line 337
2157 __cil_tmp5 = (unsigned char )__cil_tmp4;
2158#line 337
2159 wb_smsc_wdt_set_timeout(__cil_tmp5);
2160 }
2161#line 338
2162 return;
2163}
2164}
2165#line 342 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
2166static void wb_smsc_wdt_reset_timer(void)
2167{ int *__cil_tmp1 ;
2168 int __cil_tmp2 ;
2169 unsigned char __cil_tmp3 ;
2170 int __cil_tmp4 ;
2171 unsigned char __cil_tmp5 ;
2172
2173 {
2174 {
2175#line 344
2176 spin_lock(& io_lock);
2177#line 345
2178 open_io_config();
2179#line 346
2180 select_io_device((unsigned char)8);
2181#line 349
2182 __cil_tmp1 = & timeout;
2183#line 349
2184 __cil_tmp2 = *__cil_tmp1;
2185#line 349
2186 __cil_tmp3 = (unsigned char )__cil_tmp2;
2187#line 349
2188 __cil_tmp4 = (int )__cil_tmp3;
2189#line 349
2190 __cil_tmp5 = (unsigned char )__cil_tmp4;
2191#line 349
2192 wdt_timeout_value(__cil_tmp5);
2193#line 350
2194 wdt_timer_conf((unsigned char)8);
2195#line 352
2196 close_io_config();
2197#line 353
2198 spin_unlock(& io_lock);
2199 }
2200#line 354
2201 return;
2202}
2203}
2204#line 358 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
2205static int wb_smsc_wdt_status(void)
2206{ int tmp___0 ;
2207 unsigned char tmp___1 ;
2208 unsigned int __cil_tmp4 ;
2209
2210 {
2211 {
2212#line 360
2213 tmp___1 = wb_smsc_wdt_get_timeout();
2214 }
2215 {
2216#line 360
2217 __cil_tmp4 = (unsigned int )tmp___1;
2218#line 360
2219 if (__cil_tmp4 == 0U) {
2220#line 360
2221 tmp___0 = 0;
2222 } else {
2223#line 360
2224 tmp___0 = 32768;
2225 }
2226 }
2227#line 360
2228 return (tmp___0);
2229}
2230}
2231#line 368 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
2232static int wb_smsc_wdt_open(struct inode *inode , struct file *file )
2233{ int tmp ;
2234 char *tmp___0 ;
2235 int tmp___1 ;
2236 unsigned long volatile *__cil_tmp6 ;
2237 bool *__cil_tmp7 ;
2238 bool __cil_tmp8 ;
2239 int *__cil_tmp9 ;
2240 int __cil_tmp10 ;
2241
2242 {
2243 {
2244#line 372
2245 __cil_tmp6 = (unsigned long volatile *)(& timer_enabled);
2246#line 372
2247 tmp = test_and_set_bit(0, __cil_tmp6);
2248 }
2249#line 372
2250 if (tmp != 0) {
2251#line 373
2252 return (-16);
2253 } else {
2254
2255 }
2256 {
2257#line 375
2258 __cil_tmp7 = & nowayout;
2259#line 375
2260 __cil_tmp8 = *__cil_tmp7;
2261#line 375
2262 if ((int )__cil_tmp8) {
2263 {
2264#line 376
2265 __module_get(& __this_module);
2266 }
2267 } else {
2268
2269 }
2270 }
2271 {
2272#line 379
2273 wb_smsc_wdt_enable();
2274 }
2275#line 381
2276 if (unit == 0) {
2277#line 381
2278 tmp___0 = (char *)"second(s)";
2279 } else {
2280#line 381
2281 tmp___0 = (char *)"minute(s)";
2282 }
2283 {
2284#line 381
2285 __cil_tmp9 = & timeout;
2286#line 381
2287 __cil_tmp10 = *__cil_tmp9;
2288#line 381
2289 printk("<6>smsc37b787_wdt: Watchdog enabled. Timeout set to %d %s\n", __cil_tmp10,
2290 tmp___0);
2291#line 384
2292 tmp___1 = nonseekable_open(inode, file);
2293 }
2294#line 384
2295 return (tmp___1);
2296}
2297}
2298#line 389 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
2299static int wb_smsc_wdt_release(struct inode *inode , struct file *file )
2300{ signed char __cil_tmp3 ;
2301 int __cil_tmp4 ;
2302 unsigned long volatile *__cil_tmp5 ;
2303
2304 {
2305 {
2306#line 393
2307 __cil_tmp3 = (signed char )expect_close;
2308#line 393
2309 __cil_tmp4 = (int )__cil_tmp3;
2310#line 393
2311 if (__cil_tmp4 == 42) {
2312 {
2313#line 394
2314 wb_smsc_wdt_disable();
2315#line 395
2316 printk("<6>smsc37b787_wdt: Watchdog disabled, sleeping again...\n");
2317 }
2318 } else {
2319 {
2320#line 397
2321 printk("<2>smsc37b787_wdt: Unexpected close, not stopping watchdog!\n");
2322#line 398
2323 wb_smsc_wdt_reset_timer();
2324 }
2325 }
2326 }
2327 {
2328#line 401
2329 __cil_tmp5 = (unsigned long volatile *)(& timer_enabled);
2330#line 401
2331 clear_bit(0, __cil_tmp5);
2332#line 402
2333 expect_close = (char)0;
2334 }
2335#line 403
2336 return (0);
2337}
2338}
2339#line 408 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
2340static ssize_t wb_smsc_wdt_write(struct file *file , char const *data , size_t len ,
2341 loff_t *ppos )
2342{ size_t i ;
2343 char c ;
2344 int __ret_gu ;
2345 unsigned long __val_gu ;
2346 bool *__cil_tmp9 ;
2347 bool __cil_tmp10 ;
2348 signed char __cil_tmp11 ;
2349 int __cil_tmp12 ;
2350
2351 {
2352#line 412
2353 if (len != 0UL) {
2354 {
2355#line 413
2356 __cil_tmp9 = & nowayout;
2357#line 413
2358 __cil_tmp10 = *__cil_tmp9;
2359#line 413
2360 if (! __cil_tmp10) {
2361#line 417
2362 expect_close = (char)0;
2363#line 421
2364 i = 0UL;
2365#line 421
2366 goto ldv_18116;
2367 ldv_18115:
2368 {
2369#line 423
2370 might_fault();
2371 }
2372#line 423
2373 if (1 == 1) {
2374#line 423
2375 goto case_1;
2376 } else
2377#line 423
2378 if (1 == 2) {
2379#line 423
2380 goto case_2;
2381 } else
2382#line 423
2383 if (1 == 4) {
2384#line 423
2385 goto case_4;
2386 } else
2387#line 423
2388 if (1 == 8) {
2389#line 423
2390 goto case_8;
2391 } else {
2392 {
2393#line 423
2394 goto switch_default;
2395#line 423
2396 if (0) {
2397 case_1:
2398#line 423
2399 __asm__ volatile ("call __get_user_1": "=a" (__ret_gu), "=d" (__val_gu): "0" (data + i));
2400#line 423
2401 goto ldv_18109;
2402 case_2:
2403#line 423
2404 __asm__ volatile ("call __get_user_2": "=a" (__ret_gu), "=d" (__val_gu): "0" (data + i));
2405#line 423
2406 goto ldv_18109;
2407 case_4:
2408#line 423
2409 __asm__ volatile ("call __get_user_4": "=a" (__ret_gu), "=d" (__val_gu): "0" (data + i));
2410#line 423
2411 goto ldv_18109;
2412 case_8:
2413#line 423
2414 __asm__ volatile ("call __get_user_8": "=a" (__ret_gu), "=d" (__val_gu): "0" (data + i));
2415#line 423
2416 goto ldv_18109;
2417 switch_default:
2418#line 423
2419 __asm__ volatile ("call __get_user_X": "=a" (__ret_gu), "=d" (__val_gu): "0" (data + i));
2420#line 423
2421 goto ldv_18109;
2422 } else {
2423 switch_break: ;
2424 }
2425 }
2426 }
2427 ldv_18109:
2428#line 423
2429 c = (char )__val_gu;
2430#line 423
2431 if (__ret_gu != 0) {
2432#line 424
2433 return (-14L);
2434 } else {
2435
2436 }
2437 {
2438#line 425
2439 __cil_tmp11 = (signed char )c;
2440#line 425
2441 __cil_tmp12 = (int )__cil_tmp11;
2442#line 425
2443 if (__cil_tmp12 == 86) {
2444#line 426
2445 expect_close = (char)42;
2446 } else {
2447
2448 }
2449 }
2450#line 421
2451 i = i + 1UL;
2452 ldv_18116: ;
2453#line 421
2454 if (i != len) {
2455#line 422
2456 goto ldv_18115;
2457 } else {
2458#line 424
2459 goto ldv_18117;
2460 }
2461 ldv_18117: ;
2462 } else {
2463
2464 }
2465 }
2466 {
2467#line 431
2468 wb_smsc_wdt_reset_timer();
2469 }
2470 } else {
2471
2472 }
2473#line 433
2474 return ((ssize_t )len);
2475}
2476}
2477#line 438 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
2478static long wb_smsc_wdt_ioctl(struct file *file , unsigned int cmd , unsigned long arg )
2479{ int new_timeout ;
2480 union __anonunion_uarg_146 uarg ;
2481 struct watchdog_info ident ;
2482 long tmp___0 ;
2483 int tmp___1 ;
2484 int __ret_pu ;
2485 int __pu_val ;
2486 int __ret_pu___0 ;
2487 int __pu_val___0 ;
2488 int options ;
2489 int retval ;
2490 int __ret_gu ;
2491 unsigned long __val_gu ;
2492 int __ret_gu___0 ;
2493 unsigned long __val_gu___0 ;
2494 int __ret_pu___1 ;
2495 int __pu_val___1 ;
2496 struct watchdog_info *__cil_tmp22 ;
2497 unsigned long __cil_tmp23 ;
2498 unsigned long __cil_tmp24 ;
2499 unsigned long __cil_tmp25 ;
2500 unsigned long __cil_tmp26 ;
2501 unsigned long __cil_tmp27 ;
2502 unsigned long __cil_tmp28 ;
2503 unsigned long __cil_tmp29 ;
2504 unsigned long __cil_tmp30 ;
2505 unsigned long __cil_tmp31 ;
2506 unsigned long __cil_tmp32 ;
2507 unsigned long __cil_tmp33 ;
2508 unsigned long __cil_tmp34 ;
2509 unsigned long __cil_tmp35 ;
2510 unsigned long __cil_tmp36 ;
2511 unsigned long __cil_tmp37 ;
2512 unsigned long __cil_tmp38 ;
2513 unsigned long __cil_tmp39 ;
2514 unsigned long __cil_tmp40 ;
2515 unsigned long __cil_tmp41 ;
2516 unsigned long __cil_tmp42 ;
2517 unsigned long __cil_tmp43 ;
2518 unsigned long __cil_tmp44 ;
2519 unsigned long __cil_tmp45 ;
2520 unsigned long __cil_tmp46 ;
2521 unsigned long __cil_tmp47 ;
2522 unsigned long __cil_tmp48 ;
2523 unsigned long __cil_tmp49 ;
2524 unsigned long __cil_tmp50 ;
2525 unsigned long __cil_tmp51 ;
2526 unsigned long __cil_tmp52 ;
2527 unsigned long __cil_tmp53 ;
2528 unsigned long __cil_tmp54 ;
2529 unsigned long __cil_tmp55 ;
2530 unsigned long __cil_tmp56 ;
2531 unsigned long __cil_tmp57 ;
2532 unsigned long __cil_tmp58 ;
2533 unsigned long __cil_tmp59 ;
2534 unsigned long __cil_tmp60 ;
2535 unsigned long __cil_tmp61 ;
2536 unsigned long __cil_tmp62 ;
2537 unsigned long __cil_tmp63 ;
2538 unsigned long __cil_tmp64 ;
2539 unsigned long __cil_tmp65 ;
2540 unsigned long __cil_tmp66 ;
2541 unsigned long __cil_tmp67 ;
2542 unsigned long __cil_tmp68 ;
2543 unsigned long __cil_tmp69 ;
2544 unsigned long __cil_tmp70 ;
2545 unsigned long __cil_tmp71 ;
2546 unsigned long __cil_tmp72 ;
2547 unsigned long __cil_tmp73 ;
2548 unsigned long __cil_tmp74 ;
2549 unsigned long __cil_tmp75 ;
2550 unsigned long __cil_tmp76 ;
2551 unsigned long __cil_tmp77 ;
2552 unsigned long __cil_tmp78 ;
2553 unsigned long __cil_tmp79 ;
2554 unsigned long __cil_tmp80 ;
2555 unsigned long __cil_tmp81 ;
2556 unsigned long __cil_tmp82 ;
2557 unsigned long __cil_tmp83 ;
2558 unsigned long __cil_tmp84 ;
2559 unsigned long __cil_tmp85 ;
2560 unsigned long __cil_tmp86 ;
2561 unsigned long __cil_tmp87 ;
2562 unsigned long __cil_tmp88 ;
2563 unsigned long __cil_tmp89 ;
2564 unsigned long __cil_tmp90 ;
2565 unsigned long __cil_tmp91 ;
2566 unsigned long __cil_tmp92 ;
2567 unsigned long __cil_tmp93 ;
2568 unsigned long __cil_tmp94 ;
2569 unsigned long __cil_tmp95 ;
2570 unsigned long __cil_tmp96 ;
2571 unsigned long __cil_tmp97 ;
2572 unsigned long __cil_tmp98 ;
2573 unsigned long __cil_tmp99 ;
2574 unsigned long __cil_tmp100 ;
2575 unsigned long __cil_tmp101 ;
2576 unsigned long __cil_tmp102 ;
2577 unsigned long __cil_tmp103 ;
2578 unsigned long __cil_tmp104 ;
2579 unsigned long __cil_tmp105 ;
2580 unsigned long __cil_tmp106 ;
2581 unsigned long __cil_tmp107 ;
2582 unsigned long __cil_tmp108 ;
2583 unsigned long __cil_tmp109 ;
2584 unsigned long __cil_tmp110 ;
2585 unsigned long __cil_tmp111 ;
2586 unsigned long __cil_tmp112 ;
2587 unsigned long __cil_tmp113 ;
2588 unsigned long __cil_tmp114 ;
2589 unsigned long __cil_tmp115 ;
2590 unsigned long __cil_tmp116 ;
2591 unsigned long __cil_tmp117 ;
2592 unsigned long __cil_tmp118 ;
2593 unsigned long __cil_tmp119 ;
2594 void *__cil_tmp120 ;
2595 void const *__cil_tmp121 ;
2596 int __cil_tmp122 ;
2597 int *__cil_tmp123 ;
2598 int *__cil_tmp124 ;
2599 int __cil_tmp125 ;
2600 unsigned char __cil_tmp126 ;
2601 int __cil_tmp127 ;
2602 unsigned char __cil_tmp128 ;
2603 int *__cil_tmp129 ;
2604
2605 {
2606#line 448
2607 __cil_tmp22 = & ident;
2608#line 448
2609 *((__u32 *)__cil_tmp22) = 33152U;
2610#line 448
2611 __cil_tmp23 = (unsigned long )(& ident) + 4;
2612#line 448
2613 *((__u32 *)__cil_tmp23) = 0U;
2614#line 448
2615 __cil_tmp24 = 0 * 1UL;
2616#line 448
2617 __cil_tmp25 = 8 + __cil_tmp24;
2618#line 448
2619 __cil_tmp26 = (unsigned long )(& ident) + __cil_tmp25;
2620#line 448
2621 *((__u8 *)__cil_tmp26) = (__u8 )'S';
2622#line 448
2623 __cil_tmp27 = 1 * 1UL;
2624#line 448
2625 __cil_tmp28 = 8 + __cil_tmp27;
2626#line 448
2627 __cil_tmp29 = (unsigned long )(& ident) + __cil_tmp28;
2628#line 448
2629 *((__u8 *)__cil_tmp29) = (__u8 )'M';
2630#line 448
2631 __cil_tmp30 = 2 * 1UL;
2632#line 448
2633 __cil_tmp31 = 8 + __cil_tmp30;
2634#line 448
2635 __cil_tmp32 = (unsigned long )(& ident) + __cil_tmp31;
2636#line 448
2637 *((__u8 *)__cil_tmp32) = (__u8 )'s';
2638#line 448
2639 __cil_tmp33 = 3 * 1UL;
2640#line 448
2641 __cil_tmp34 = 8 + __cil_tmp33;
2642#line 448
2643 __cil_tmp35 = (unsigned long )(& ident) + __cil_tmp34;
2644#line 448
2645 *((__u8 *)__cil_tmp35) = (__u8 )'C';
2646#line 448
2647 __cil_tmp36 = 4 * 1UL;
2648#line 448
2649 __cil_tmp37 = 8 + __cil_tmp36;
2650#line 448
2651 __cil_tmp38 = (unsigned long )(& ident) + __cil_tmp37;
2652#line 448
2653 *((__u8 *)__cil_tmp38) = (__u8 )' ';
2654#line 448
2655 __cil_tmp39 = 5 * 1UL;
2656#line 448
2657 __cil_tmp40 = 8 + __cil_tmp39;
2658#line 448
2659 __cil_tmp41 = (unsigned long )(& ident) + __cil_tmp40;
2660#line 448
2661 *((__u8 *)__cil_tmp41) = (__u8 )'3';
2662#line 448
2663 __cil_tmp42 = 6 * 1UL;
2664#line 448
2665 __cil_tmp43 = 8 + __cil_tmp42;
2666#line 448
2667 __cil_tmp44 = (unsigned long )(& ident) + __cil_tmp43;
2668#line 448
2669 *((__u8 *)__cil_tmp44) = (__u8 )'7';
2670#line 448
2671 __cil_tmp45 = 7 * 1UL;
2672#line 448
2673 __cil_tmp46 = 8 + __cil_tmp45;
2674#line 448
2675 __cil_tmp47 = (unsigned long )(& ident) + __cil_tmp46;
2676#line 448
2677 *((__u8 *)__cil_tmp47) = (__u8 )'B';
2678#line 448
2679 __cil_tmp48 = 8 * 1UL;
2680#line 448
2681 __cil_tmp49 = 8 + __cil_tmp48;
2682#line 448
2683 __cil_tmp50 = (unsigned long )(& ident) + __cil_tmp49;
2684#line 448
2685 *((__u8 *)__cil_tmp50) = (__u8 )'7';
2686#line 448
2687 __cil_tmp51 = 9 * 1UL;
2688#line 448
2689 __cil_tmp52 = 8 + __cil_tmp51;
2690#line 448
2691 __cil_tmp53 = (unsigned long )(& ident) + __cil_tmp52;
2692#line 448
2693 *((__u8 *)__cil_tmp53) = (__u8 )'8';
2694#line 448
2695 __cil_tmp54 = 10 * 1UL;
2696#line 448
2697 __cil_tmp55 = 8 + __cil_tmp54;
2698#line 448
2699 __cil_tmp56 = (unsigned long )(& ident) + __cil_tmp55;
2700#line 448
2701 *((__u8 *)__cil_tmp56) = (__u8 )'7';
2702#line 448
2703 __cil_tmp57 = 11 * 1UL;
2704#line 448
2705 __cil_tmp58 = 8 + __cil_tmp57;
2706#line 448
2707 __cil_tmp59 = (unsigned long )(& ident) + __cil_tmp58;
2708#line 448
2709 *((__u8 *)__cil_tmp59) = (__u8 )' ';
2710#line 448
2711 __cil_tmp60 = 12 * 1UL;
2712#line 448
2713 __cil_tmp61 = 8 + __cil_tmp60;
2714#line 448
2715 __cil_tmp62 = (unsigned long )(& ident) + __cil_tmp61;
2716#line 448
2717 *((__u8 *)__cil_tmp62) = (__u8 )'W';
2718#line 448
2719 __cil_tmp63 = 13 * 1UL;
2720#line 448
2721 __cil_tmp64 = 8 + __cil_tmp63;
2722#line 448
2723 __cil_tmp65 = (unsigned long )(& ident) + __cil_tmp64;
2724#line 448
2725 *((__u8 *)__cil_tmp65) = (__u8 )'a';
2726#line 448
2727 __cil_tmp66 = 14 * 1UL;
2728#line 448
2729 __cil_tmp67 = 8 + __cil_tmp66;
2730#line 448
2731 __cil_tmp68 = (unsigned long )(& ident) + __cil_tmp67;
2732#line 448
2733 *((__u8 *)__cil_tmp68) = (__u8 )'t';
2734#line 448
2735 __cil_tmp69 = 15 * 1UL;
2736#line 448
2737 __cil_tmp70 = 8 + __cil_tmp69;
2738#line 448
2739 __cil_tmp71 = (unsigned long )(& ident) + __cil_tmp70;
2740#line 448
2741 *((__u8 *)__cil_tmp71) = (__u8 )'c';
2742#line 448
2743 __cil_tmp72 = 16 * 1UL;
2744#line 448
2745 __cil_tmp73 = 8 + __cil_tmp72;
2746#line 448
2747 __cil_tmp74 = (unsigned long )(& ident) + __cil_tmp73;
2748#line 448
2749 *((__u8 *)__cil_tmp74) = (__u8 )'h';
2750#line 448
2751 __cil_tmp75 = 17 * 1UL;
2752#line 448
2753 __cil_tmp76 = 8 + __cil_tmp75;
2754#line 448
2755 __cil_tmp77 = (unsigned long )(& ident) + __cil_tmp76;
2756#line 448
2757 *((__u8 *)__cil_tmp77) = (__u8 )'d';
2758#line 448
2759 __cil_tmp78 = 18 * 1UL;
2760#line 448
2761 __cil_tmp79 = 8 + __cil_tmp78;
2762#line 448
2763 __cil_tmp80 = (unsigned long )(& ident) + __cil_tmp79;
2764#line 448
2765 *((__u8 *)__cil_tmp80) = (__u8 )'o';
2766#line 448
2767 __cil_tmp81 = 19 * 1UL;
2768#line 448
2769 __cil_tmp82 = 8 + __cil_tmp81;
2770#line 448
2771 __cil_tmp83 = (unsigned long )(& ident) + __cil_tmp82;
2772#line 448
2773 *((__u8 *)__cil_tmp83) = (__u8 )'g';
2774#line 448
2775 __cil_tmp84 = 20 * 1UL;
2776#line 448
2777 __cil_tmp85 = 8 + __cil_tmp84;
2778#line 448
2779 __cil_tmp86 = (unsigned long )(& ident) + __cil_tmp85;
2780#line 448
2781 *((__u8 *)__cil_tmp86) = (__u8 )'\000';
2782#line 448
2783 __cil_tmp87 = 21 * 1UL;
2784#line 448
2785 __cil_tmp88 = 8 + __cil_tmp87;
2786#line 448
2787 __cil_tmp89 = (unsigned long )(& ident) + __cil_tmp88;
2788#line 448
2789 *((__u8 *)__cil_tmp89) = (unsigned char)0;
2790#line 448
2791 __cil_tmp90 = 22 * 1UL;
2792#line 448
2793 __cil_tmp91 = 8 + __cil_tmp90;
2794#line 448
2795 __cil_tmp92 = (unsigned long )(& ident) + __cil_tmp91;
2796#line 448
2797 *((__u8 *)__cil_tmp92) = (unsigned char)0;
2798#line 448
2799 __cil_tmp93 = 23 * 1UL;
2800#line 448
2801 __cil_tmp94 = 8 + __cil_tmp93;
2802#line 448
2803 __cil_tmp95 = (unsigned long )(& ident) + __cil_tmp94;
2804#line 448
2805 *((__u8 *)__cil_tmp95) = (unsigned char)0;
2806#line 448
2807 __cil_tmp96 = 24 * 1UL;
2808#line 448
2809 __cil_tmp97 = 8 + __cil_tmp96;
2810#line 448
2811 __cil_tmp98 = (unsigned long )(& ident) + __cil_tmp97;
2812#line 448
2813 *((__u8 *)__cil_tmp98) = (unsigned char)0;
2814#line 448
2815 __cil_tmp99 = 25 * 1UL;
2816#line 448
2817 __cil_tmp100 = 8 + __cil_tmp99;
2818#line 448
2819 __cil_tmp101 = (unsigned long )(& ident) + __cil_tmp100;
2820#line 448
2821 *((__u8 *)__cil_tmp101) = (unsigned char)0;
2822#line 448
2823 __cil_tmp102 = 26 * 1UL;
2824#line 448
2825 __cil_tmp103 = 8 + __cil_tmp102;
2826#line 448
2827 __cil_tmp104 = (unsigned long )(& ident) + __cil_tmp103;
2828#line 448
2829 *((__u8 *)__cil_tmp104) = (unsigned char)0;
2830#line 448
2831 __cil_tmp105 = 27 * 1UL;
2832#line 448
2833 __cil_tmp106 = 8 + __cil_tmp105;
2834#line 448
2835 __cil_tmp107 = (unsigned long )(& ident) + __cil_tmp106;
2836#line 448
2837 *((__u8 *)__cil_tmp107) = (unsigned char)0;
2838#line 448
2839 __cil_tmp108 = 28 * 1UL;
2840#line 448
2841 __cil_tmp109 = 8 + __cil_tmp108;
2842#line 448
2843 __cil_tmp110 = (unsigned long )(& ident) + __cil_tmp109;
2844#line 448
2845 *((__u8 *)__cil_tmp110) = (unsigned char)0;
2846#line 448
2847 __cil_tmp111 = 29 * 1UL;
2848#line 448
2849 __cil_tmp112 = 8 + __cil_tmp111;
2850#line 448
2851 __cil_tmp113 = (unsigned long )(& ident) + __cil_tmp112;
2852#line 448
2853 *((__u8 *)__cil_tmp113) = (unsigned char)0;
2854#line 448
2855 __cil_tmp114 = 30 * 1UL;
2856#line 448
2857 __cil_tmp115 = 8 + __cil_tmp114;
2858#line 448
2859 __cil_tmp116 = (unsigned long )(& ident) + __cil_tmp115;
2860#line 448
2861 *((__u8 *)__cil_tmp116) = (unsigned char)0;
2862#line 448
2863 __cil_tmp117 = 31 * 1UL;
2864#line 448
2865 __cil_tmp118 = 8 + __cil_tmp117;
2866#line 448
2867 __cil_tmp119 = (unsigned long )(& ident) + __cil_tmp118;
2868#line 448
2869 *((__u8 *)__cil_tmp119) = (unsigned char)0;
2870#line 456
2871 uarg.i = (int *)arg;
2872#line 459
2873 if ((int )cmd == -2144839936) {
2874#line 459
2875 goto case_neg_2144839936;
2876 } else
2877#line 462
2878 if ((int )cmd == -2147199231) {
2879#line 462
2880 goto case_neg_2147199231;
2881 } else
2882#line 464
2883 if ((int )cmd == -2147199230) {
2884#line 464
2885 goto case_neg_2147199230;
2886 } else
2887#line 466
2888 if ((int )cmd == -2147199228) {
2889#line 466
2890 goto case_neg_2147199228;
2891 } else
2892#line 483
2893 if ((int )cmd == -2147199227) {
2894#line 483
2895 goto case_neg_2147199227;
2896 } else
2897#line 486
2898 if ((int )cmd == -1073457402) {
2899#line 486
2900 goto case_neg_1073457402;
2901 } else
2902#line 497
2903 if ((int )cmd == -2147199225) {
2904#line 497
2905 goto case_neg_2147199225;
2906 } else {
2907 {
2908#line 502
2909 goto switch_default___4;
2910#line 458
2911 if (0) {
2912 case_neg_2144839936:
2913 {
2914#line 460
2915 __cil_tmp120 = (void *)uarg.ident;
2916#line 460
2917 __cil_tmp121 = (void const *)(& ident);
2918#line 460
2919 tmp___1 = copy_to_user(__cil_tmp120, __cil_tmp121, 40U);
2920 }
2921#line 460
2922 if (tmp___1 != 0) {
2923#line 460
2924 tmp___0 = -14L;
2925 } else {
2926#line 460
2927 tmp___0 = 0L;
2928 }
2929#line 460
2930 return (tmp___0);
2931 case_neg_2147199231:
2932 {
2933#line 463
2934 might_fault();
2935#line 463
2936 __pu_val = wb_smsc_wdt_status();
2937 }
2938#line 463
2939 if (4 == 1) {
2940#line 463
2941 goto case_1;
2942 } else
2943#line 463
2944 if (4 == 2) {
2945#line 463
2946 goto case_2;
2947 } else
2948#line 463
2949 if (4 == 4) {
2950#line 463
2951 goto case_4;
2952 } else
2953#line 463
2954 if (4 == 8) {
2955#line 463
2956 goto case_8;
2957 } else {
2958 {
2959#line 463
2960 goto switch_default;
2961#line 463
2962 if (0) {
2963 case_1:
2964#line 463
2965 __asm__ volatile ("call __put_user_1": "=a" (__ret_pu): "0" (__pu_val),
2966 "c" (uarg.i): "ebx");
2967#line 463
2968 goto ldv_18134;
2969 case_2:
2970#line 463
2971 __asm__ volatile ("call __put_user_2": "=a" (__ret_pu): "0" (__pu_val),
2972 "c" (uarg.i): "ebx");
2973#line 463
2974 goto ldv_18134;
2975 case_4:
2976#line 463
2977 __asm__ volatile ("call __put_user_4": "=a" (__ret_pu): "0" (__pu_val),
2978 "c" (uarg.i): "ebx");
2979#line 463
2980 goto ldv_18134;
2981 case_8:
2982#line 463
2983 __asm__ volatile ("call __put_user_8": "=a" (__ret_pu): "0" (__pu_val),
2984 "c" (uarg.i): "ebx");
2985#line 463
2986 goto ldv_18134;
2987 switch_default:
2988#line 463
2989 __asm__ volatile ("call __put_user_X": "=a" (__ret_pu): "0" (__pu_val),
2990 "c" (uarg.i): "ebx");
2991#line 463
2992 goto ldv_18134;
2993 } else {
2994 switch_break___0: ;
2995 }
2996 }
2997 }
2998 ldv_18134: ;
2999#line 463
3000 return ((long )__ret_pu);
3001 case_neg_2147199230:
3002 {
3003#line 465
3004 might_fault();
3005#line 465
3006 __pu_val___0 = 0;
3007 }
3008#line 465
3009 if (4 == 1) {
3010#line 465
3011 goto case_1___0;
3012 } else
3013#line 465
3014 if (4 == 2) {
3015#line 465
3016 goto case_2___0;
3017 } else
3018#line 465
3019 if (4 == 4) {
3020#line 465
3021 goto case_4___0;
3022 } else
3023#line 465
3024 if (4 == 8) {
3025#line 465
3026 goto case_8___0;
3027 } else {
3028 {
3029#line 465
3030 goto switch_default___0;
3031#line 465
3032 if (0) {
3033 case_1___0:
3034#line 465
3035 __asm__ volatile ("call __put_user_1": "=a" (__ret_pu___0): "0" (__pu_val___0),
3036 "c" (uarg.i): "ebx");
3037#line 465
3038 goto ldv_18144;
3039 case_2___0:
3040#line 465
3041 __asm__ volatile ("call __put_user_2": "=a" (__ret_pu___0): "0" (__pu_val___0),
3042 "c" (uarg.i): "ebx");
3043#line 465
3044 goto ldv_18144;
3045 case_4___0:
3046#line 465
3047 __asm__ volatile ("call __put_user_4": "=a" (__ret_pu___0): "0" (__pu_val___0),
3048 "c" (uarg.i): "ebx");
3049#line 465
3050 goto ldv_18144;
3051 case_8___0:
3052#line 465
3053 __asm__ volatile ("call __put_user_8": "=a" (__ret_pu___0): "0" (__pu_val___0),
3054 "c" (uarg.i): "ebx");
3055#line 465
3056 goto ldv_18144;
3057 switch_default___0:
3058#line 465
3059 __asm__ volatile ("call __put_user_X": "=a" (__ret_pu___0): "0" (__pu_val___0),
3060 "c" (uarg.i): "ebx");
3061#line 465
3062 goto ldv_18144;
3063 } else {
3064 switch_break___1: ;
3065 }
3066 }
3067 }
3068 ldv_18144: ;
3069#line 465
3070 return ((long )__ret_pu___0);
3071 case_neg_2147199228:
3072 {
3073#line 468
3074 retval = -22;
3075#line 470
3076 might_fault();
3077 }
3078#line 470
3079 if (4 == 1) {
3080#line 470
3081 goto case_1___1;
3082 } else
3083#line 470
3084 if (4 == 2) {
3085#line 470
3086 goto case_2___1;
3087 } else
3088#line 470
3089 if (4 == 4) {
3090#line 470
3091 goto case_4___1;
3092 } else
3093#line 470
3094 if (4 == 8) {
3095#line 470
3096 goto case_8___1;
3097 } else {
3098 {
3099#line 470
3100 goto switch_default___1;
3101#line 470
3102 if (0) {
3103 case_1___1:
3104#line 470
3105 __asm__ volatile ("call __get_user_1": "=a" (__ret_gu), "=d" (__val_gu): "0" (uarg.i));
3106#line 470
3107 goto ldv_18156;
3108 case_2___1:
3109#line 470
3110 __asm__ volatile ("call __get_user_2": "=a" (__ret_gu), "=d" (__val_gu): "0" (uarg.i));
3111#line 470
3112 goto ldv_18156;
3113 case_4___1:
3114#line 470
3115 __asm__ volatile ("call __get_user_4": "=a" (__ret_gu), "=d" (__val_gu): "0" (uarg.i));
3116#line 470
3117 goto ldv_18156;
3118 case_8___1:
3119#line 470
3120 __asm__ volatile ("call __get_user_8": "=a" (__ret_gu), "=d" (__val_gu): "0" (uarg.i));
3121#line 470
3122 goto ldv_18156;
3123 switch_default___1:
3124#line 470
3125 __asm__ volatile ("call __get_user_X": "=a" (__ret_gu), "=d" (__val_gu): "0" (uarg.i));
3126#line 470
3127 goto ldv_18156;
3128 } else {
3129 switch_break___2: ;
3130 }
3131 }
3132 }
3133 ldv_18156:
3134#line 470
3135 options = (int )__val_gu;
3136#line 470
3137 if (__ret_gu != 0) {
3138#line 471
3139 return (-14L);
3140 } else {
3141
3142 }
3143#line 473
3144 if (options & 1) {
3145 {
3146#line 474
3147 wb_smsc_wdt_disable();
3148#line 475
3149 retval = 0;
3150 }
3151 } else {
3152
3153 }
3154 {
3155#line 477
3156 __cil_tmp122 = options & 2;
3157#line 477
3158 if (__cil_tmp122 != 0) {
3159 {
3160#line 478
3161 wb_smsc_wdt_enable();
3162#line 479
3163 retval = 0;
3164 }
3165 } else {
3166
3167 }
3168 }
3169#line 481
3170 return ((long )retval);
3171 case_neg_2147199227:
3172 {
3173#line 484
3174 wb_smsc_wdt_reset_timer();
3175 }
3176#line 485
3177 return (0L);
3178 case_neg_1073457402:
3179 {
3180#line 487
3181 might_fault();
3182 }
3183#line 487
3184 if (4 == 1) {
3185#line 487
3186 goto case_1___2;
3187 } else
3188#line 487
3189 if (4 == 2) {
3190#line 487
3191 goto case_2___2;
3192 } else
3193#line 487
3194 if (4 == 4) {
3195#line 487
3196 goto case_4___2;
3197 } else
3198#line 487
3199 if (4 == 8) {
3200#line 487
3201 goto case_8___2;
3202 } else {
3203 {
3204#line 487
3205 goto switch_default___2;
3206#line 487
3207 if (0) {
3208 case_1___2:
3209#line 487
3210 __asm__ volatile ("call __get_user_1": "=a" (__ret_gu___0), "=d" (__val_gu___0): "0" (uarg.i));
3211#line 487
3212 goto ldv_18167;
3213 case_2___2:
3214#line 487
3215 __asm__ volatile ("call __get_user_2": "=a" (__ret_gu___0), "=d" (__val_gu___0): "0" (uarg.i));
3216#line 487
3217 goto ldv_18167;
3218 case_4___2:
3219#line 487
3220 __asm__ volatile ("call __get_user_4": "=a" (__ret_gu___0), "=d" (__val_gu___0): "0" (uarg.i));
3221#line 487
3222 goto ldv_18167;
3223 case_8___2:
3224#line 487
3225 __asm__ volatile ("call __get_user_8": "=a" (__ret_gu___0), "=d" (__val_gu___0): "0" (uarg.i));
3226#line 487
3227 goto ldv_18167;
3228 switch_default___2:
3229#line 487
3230 __asm__ volatile ("call __get_user_X": "=a" (__ret_gu___0), "=d" (__val_gu___0): "0" (uarg.i));
3231#line 487
3232 goto ldv_18167;
3233 } else {
3234 switch_break___3: ;
3235 }
3236 }
3237 }
3238 ldv_18167:
3239#line 487
3240 new_timeout = (int )__val_gu___0;
3241#line 487
3242 if (__ret_gu___0 != 0) {
3243#line 488
3244 return (-14L);
3245 } else {
3246
3247 }
3248#line 490
3249 if (unit == 1) {
3250#line 491
3251 new_timeout = new_timeout / 60;
3252 } else {
3253
3254 }
3255#line 492
3256 if (new_timeout < 0) {
3257#line 493
3258 return (-22L);
3259 } else
3260#line 492
3261 if (new_timeout > 255) {
3262#line 493
3263 return (-22L);
3264 } else {
3265
3266 }
3267 {
3268#line 494
3269 __cil_tmp123 = & timeout;
3270#line 494
3271 *__cil_tmp123 = new_timeout;
3272#line 495
3273 __cil_tmp124 = & timeout;
3274#line 495
3275 __cil_tmp125 = *__cil_tmp124;
3276#line 495
3277 __cil_tmp126 = (unsigned char )__cil_tmp125;
3278#line 495
3279 __cil_tmp127 = (int )__cil_tmp126;
3280#line 495
3281 __cil_tmp128 = (unsigned char )__cil_tmp127;
3282#line 495
3283 wb_smsc_wdt_set_timeout(__cil_tmp128);
3284 }
3285 case_neg_2147199225:
3286#line 498
3287 __cil_tmp129 = & timeout;
3288#line 498
3289 new_timeout = *__cil_tmp129;
3290#line 499
3291 if (unit == 1) {
3292#line 500
3293 new_timeout = new_timeout * 60;
3294 } else {
3295
3296 }
3297 {
3298#line 501
3299 might_fault();
3300#line 501
3301 __pu_val___1 = new_timeout;
3302 }
3303#line 501
3304 if (4 == 1) {
3305#line 501
3306 goto case_1___3;
3307 } else
3308#line 501
3309 if (4 == 2) {
3310#line 501
3311 goto case_2___3;
3312 } else
3313#line 501
3314 if (4 == 4) {
3315#line 501
3316 goto case_4___3;
3317 } else
3318#line 501
3319 if (4 == 8) {
3320#line 501
3321 goto case_8___3;
3322 } else {
3323 {
3324#line 501
3325 goto switch_default___3;
3326#line 501
3327 if (0) {
3328 case_1___3:
3329#line 501
3330 __asm__ volatile ("call __put_user_1": "=a" (__ret_pu___1): "0" (__pu_val___1),
3331 "c" (uarg.i): "ebx");
3332#line 501
3333 goto ldv_18177;
3334 case_2___3:
3335#line 501
3336 __asm__ volatile ("call __put_user_2": "=a" (__ret_pu___1): "0" (__pu_val___1),
3337 "c" (uarg.i): "ebx");
3338#line 501
3339 goto ldv_18177;
3340 case_4___3:
3341#line 501
3342 __asm__ volatile ("call __put_user_4": "=a" (__ret_pu___1): "0" (__pu_val___1),
3343 "c" (uarg.i): "ebx");
3344#line 501
3345 goto ldv_18177;
3346 case_8___3:
3347#line 501
3348 __asm__ volatile ("call __put_user_8": "=a" (__ret_pu___1): "0" (__pu_val___1),
3349 "c" (uarg.i): "ebx");
3350#line 501
3351 goto ldv_18177;
3352 switch_default___3:
3353#line 501
3354 __asm__ volatile ("call __put_user_X": "=a" (__ret_pu___1): "0" (__pu_val___1),
3355 "c" (uarg.i): "ebx");
3356#line 501
3357 goto ldv_18177;
3358 } else {
3359 switch_break___4: ;
3360 }
3361 }
3362 }
3363 ldv_18177: ;
3364#line 501
3365 return ((long )__ret_pu___1);
3366 switch_default___4: ;
3367#line 503
3368 return (-25L);
3369 } else {
3370 switch_break: ;
3371 }
3372 }
3373 }
3374}
3375}
3376#line 509 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3377static int wb_smsc_wdt_notify_sys(struct notifier_block *this , unsigned long code ,
3378 void *unused )
3379{ int *__cil_tmp4 ;
3380 int *__cil_tmp5 ;
3381
3382 {
3383#line 512
3384 if (code == 1UL) {
3385 {
3386#line 514
3387 __cil_tmp4 = & timeout;
3388#line 514
3389 *__cil_tmp4 = 0;
3390#line 515
3391 wb_smsc_wdt_disable();
3392 }
3393 } else
3394#line 512
3395 if (code == 2UL) {
3396 {
3397#line 514
3398 __cil_tmp5 = & timeout;
3399#line 514
3400 *__cil_tmp5 = 0;
3401#line 515
3402 wb_smsc_wdt_disable();
3403 }
3404 } else {
3405
3406 }
3407#line 517
3408 return (0);
3409}
3410}
3411#line 522 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3412static struct file_operations const wb_smsc_wdt_fops =
3413#line 522
3414 {& __this_module, & no_llseek, (ssize_t (*)(struct file * , char * , size_t ,
3415 loff_t * ))0, & wb_smsc_wdt_write,
3416 (ssize_t (*)(struct kiocb * , struct iovec const * , unsigned long , loff_t ))0,
3417 (ssize_t (*)(struct kiocb * , struct iovec const * , unsigned long , loff_t ))0,
3418 (int (*)(struct file * , void * , int (*)(void * , char const * , int , loff_t ,
3419 u64 , unsigned int ) ))0, (unsigned int (*)(struct file * ,
3420 struct poll_table_struct * ))0,
3421 & wb_smsc_wdt_ioctl, (long (*)(struct file * , unsigned int , unsigned long ))0,
3422 (int (*)(struct file * , struct vm_area_struct * ))0, & wb_smsc_wdt_open, (int (*)(struct file * ,
3423 fl_owner_t ))0,
3424 & wb_smsc_wdt_release, (int (*)(struct file * , loff_t , loff_t , int ))0,
3425 (int (*)(struct kiocb * , int ))0, (int (*)(int , struct file * , int ))0,
3426 (int (*)(struct file * , int , struct file_lock * ))0, (ssize_t (*)(struct file * ,
3427 struct page * ,
3428 int , size_t ,
3429 loff_t * ,
3430 int ))0,
3431 (unsigned long (*)(struct file * , unsigned long , unsigned long , unsigned long ,
3432 unsigned long ))0, (int (*)(int ))0, (int (*)(struct file * ,
3433 int , struct file_lock * ))0,
3434 (ssize_t (*)(struct pipe_inode_info * , struct file * , loff_t * , size_t , unsigned int ))0,
3435 (ssize_t (*)(struct file * , loff_t * , struct pipe_inode_info * , size_t , unsigned int ))0,
3436 (int (*)(struct file * , long , struct file_lock ** ))0, (long (*)(struct file * ,
3437 int , loff_t ,
3438 loff_t ))0};
3439#line 531 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3440static struct notifier_block wb_smsc_wdt_notifier = {& wb_smsc_wdt_notify_sys, (struct notifier_block *)0, 0};
3441#line 535 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3442static struct miscdevice wb_smsc_wdt_miscdev =
3443#line 535
3444 {130, "watchdog", & wb_smsc_wdt_fops, {(struct list_head *)0, (struct list_head *)0},
3445 (struct device *)0, (struct device *)0, (char const *)0, (unsigned short)0};
3446#line 545 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3447static int wb_smsc_wdt_init(void)
3448{ int ret ;
3449 struct resource *tmp ;
3450 char *tmp___0 ;
3451 struct resource *__cil_tmp4 ;
3452 unsigned long __cil_tmp5 ;
3453 unsigned long __cil_tmp6 ;
3454 int *__cil_tmp7 ;
3455 int __cil_tmp8 ;
3456 int *__cil_tmp9 ;
3457 int *__cil_tmp10 ;
3458 int __cil_tmp11 ;
3459 bool *__cil_tmp12 ;
3460 bool __cil_tmp13 ;
3461 int __cil_tmp14 ;
3462
3463 {
3464 {
3465#line 549
3466 printk("<6>smsc37b787_wdt: SMsC 37B787 watchdog component driver 1.1 initialising...\n");
3467#line 552
3468 tmp = __request_region(& ioport_resource, 1008ULL, 2ULL, "SMsC 37B787 watchdog",
3469 0);
3470 }
3471 {
3472#line 552
3473 __cil_tmp4 = (struct resource *)0;
3474#line 552
3475 __cil_tmp5 = (unsigned long )__cil_tmp4;
3476#line 552
3477 __cil_tmp6 = (unsigned long )tmp;
3478#line 552
3479 if (__cil_tmp6 == __cil_tmp5) {
3480 {
3481#line 553
3482 printk("<3>smsc37b787_wdt: Unable to register IO port %#x\n", 1008);
3483#line 554
3484 ret = -16;
3485 }
3486#line 555
3487 goto out_pnp;
3488 } else {
3489
3490 }
3491 }
3492 {
3493#line 559
3494 __cil_tmp7 = & timeout;
3495#line 559
3496 __cil_tmp8 = *__cil_tmp7;
3497#line 559
3498 if (__cil_tmp8 > 255) {
3499#line 560
3500 __cil_tmp9 = & timeout;
3501#line 560
3502 *__cil_tmp9 = 255;
3503 } else {
3504
3505 }
3506 }
3507 {
3508#line 563
3509 wb_smsc_wdt_initialize();
3510#line 565
3511 ret = register_reboot_notifier(& wb_smsc_wdt_notifier);
3512 }
3513#line 566
3514 if (ret != 0) {
3515 {
3516#line 567
3517 printk("<3>smsc37b787_wdt: Unable to register reboot notifier err = %d\n", ret);
3518 }
3519#line 568
3520 goto out_io;
3521 } else {
3522
3523 }
3524 {
3525#line 571
3526 ret = misc_register(& wb_smsc_wdt_miscdev);
3527 }
3528#line 572
3529 if (ret != 0) {
3530 {
3531#line 573
3532 printk("<3>smsc37b787_wdt: Unable to register miscdev on minor %d\n", 130);
3533 }
3534#line 575
3535 goto out_rbt;
3536 } else {
3537
3538 }
3539#line 579
3540 if (unit == 0) {
3541#line 579
3542 tmp___0 = (char *)"second(s)";
3543 } else {
3544#line 579
3545 tmp___0 = (char *)"minute(s)";
3546 }
3547 {
3548#line 579
3549 __cil_tmp10 = & timeout;
3550#line 579
3551 __cil_tmp11 = *__cil_tmp10;
3552#line 579
3553 printk("<6>smsc37b787_wdt: Timeout set to %d %s\n", __cil_tmp11, tmp___0);
3554#line 581
3555 __cil_tmp12 = & nowayout;
3556#line 581
3557 __cil_tmp13 = *__cil_tmp12;
3558#line 581
3559 __cil_tmp14 = (int )__cil_tmp13;
3560#line 581
3561 printk("<6>smsc37b787_wdt: Watchdog initialized and sleeping (nowayout=%d)...\n",
3562 __cil_tmp14);
3563 }
3564 out_clean: ;
3565#line 584
3566 return (ret);
3567 out_rbt:
3568 {
3569#line 587
3570 unregister_reboot_notifier(& wb_smsc_wdt_notifier);
3571 }
3572 out_io:
3573 {
3574#line 590
3575 __release_region(& ioport_resource, 1008ULL, 2ULL);
3576 }
3577 out_pnp: ;
3578#line 593
3579 goto out_clean;
3580}
3581}
3582#line 598 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3583static void wb_smsc_wdt_exit(void)
3584{ bool *__cil_tmp1 ;
3585 bool __cil_tmp2 ;
3586
3587 {
3588 {
3589#line 601
3590 __cil_tmp1 = & nowayout;
3591#line 601
3592 __cil_tmp2 = *__cil_tmp1;
3593#line 601
3594 if (! __cil_tmp2) {
3595 {
3596#line 602
3597 wb_smsc_wdt_shutdown();
3598#line 603
3599 printk("<6>smsc37b787_wdt: Watchdog disabled\n");
3600 }
3601 } else {
3602
3603 }
3604 }
3605 {
3606#line 606
3607 misc_deregister(& wb_smsc_wdt_miscdev);
3608#line 607
3609 unregister_reboot_notifier(& wb_smsc_wdt_notifier);
3610#line 608
3611 __release_region(& ioport_resource, 1008ULL, 2ULL);
3612#line 610
3613 printk("<6>smsc37b787_wdt: SMsC 37B787 watchdog component driver removed\n");
3614 }
3615#line 611
3616 return;
3617}
3618}
3619#line 653
3620extern void ldv_check_final_state(void) ;
3621#line 656
3622extern void ldv_check_return_value(int ) ;
3623#line 659
3624extern void ldv_initialize(void) ;
3625#line 662
3626extern int __VERIFIER_nondet_int(void) ;
3627#line 665 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3628int LDV_IN_INTERRUPT ;
3629#line 668 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3630void main(void)
3631{ struct file *var_group1 ;
3632 char const *var_wb_smsc_wdt_write_21_p1 ;
3633 size_t var_wb_smsc_wdt_write_21_p2 ;
3634 loff_t *var_wb_smsc_wdt_write_21_p3 ;
3635 ssize_t res_wb_smsc_wdt_write_21 ;
3636 unsigned int var_wb_smsc_wdt_ioctl_22_p1 ;
3637 unsigned long var_wb_smsc_wdt_ioctl_22_p2 ;
3638 struct inode *var_group2 ;
3639 int res_wb_smsc_wdt_open_19 ;
3640 struct notifier_block *var_group3 ;
3641 unsigned long var_wb_smsc_wdt_notify_sys_23_p1 ;
3642 void *var_wb_smsc_wdt_notify_sys_23_p2 ;
3643 int ldv_s_wb_smsc_wdt_fops_file_operations ;
3644 int tmp ;
3645 int tmp___0 ;
3646 int tmp___1 ;
3647 int __cil_tmp17 ;
3648
3649 {
3650 {
3651#line 825
3652 ldv_s_wb_smsc_wdt_fops_file_operations = 0;
3653#line 793
3654 LDV_IN_INTERRUPT = 1;
3655#line 802
3656 ldv_initialize();
3657#line 819
3658 tmp = wb_smsc_wdt_init();
3659 }
3660#line 819
3661 if (tmp != 0) {
3662#line 820
3663 goto ldv_final;
3664 } else {
3665
3666 }
3667#line 831
3668 goto ldv_18276;
3669 ldv_18275:
3670 {
3671#line 835
3672 tmp___0 = __VERIFIER_nondet_int();
3673 }
3674#line 837
3675 if (tmp___0 == 0) {
3676#line 837
3677 goto case_0;
3678 } else
3679#line 871
3680 if (tmp___0 == 1) {
3681#line 871
3682 goto case_1;
3683 } else
3684#line 905
3685 if (tmp___0 == 2) {
3686#line 905
3687 goto case_2;
3688 } else
3689#line 936
3690 if (tmp___0 == 3) {
3691#line 936
3692 goto case_3;
3693 } else
3694#line 967
3695 if (tmp___0 == 4) {
3696#line 967
3697 goto case_4;
3698 } else {
3699 {
3700#line 998
3701 goto switch_default;
3702#line 835
3703 if (0) {
3704 case_0: ;
3705#line 840
3706 if (ldv_s_wb_smsc_wdt_fops_file_operations == 0) {
3707 {
3708#line 856
3709 res_wb_smsc_wdt_open_19 = wb_smsc_wdt_open(var_group2, var_group1);
3710#line 857
3711 ldv_check_return_value(res_wb_smsc_wdt_open_19);
3712 }
3713#line 858
3714 if (res_wb_smsc_wdt_open_19 != 0) {
3715#line 859
3716 goto ldv_module_exit;
3717 } else {
3718
3719 }
3720#line 864
3721 ldv_s_wb_smsc_wdt_fops_file_operations = ldv_s_wb_smsc_wdt_fops_file_operations + 1;
3722 } else {
3723
3724 }
3725#line 870
3726 goto ldv_18269;
3727 case_1: ;
3728#line 874
3729 if (ldv_s_wb_smsc_wdt_fops_file_operations == 1) {
3730 {
3731#line 890
3732 res_wb_smsc_wdt_write_21 = wb_smsc_wdt_write(var_group1, var_wb_smsc_wdt_write_21_p1,
3733 var_wb_smsc_wdt_write_21_p2,
3734 var_wb_smsc_wdt_write_21_p3);
3735#line 891
3736 __cil_tmp17 = (int )res_wb_smsc_wdt_write_21;
3737#line 891
3738 ldv_check_return_value(__cil_tmp17);
3739 }
3740#line 892
3741 if (res_wb_smsc_wdt_write_21 < 0L) {
3742#line 893
3743 goto ldv_module_exit;
3744 } else {
3745
3746 }
3747#line 898
3748 ldv_s_wb_smsc_wdt_fops_file_operations = ldv_s_wb_smsc_wdt_fops_file_operations + 1;
3749 } else {
3750
3751 }
3752#line 904
3753 goto ldv_18269;
3754 case_2: ;
3755#line 908
3756 if (ldv_s_wb_smsc_wdt_fops_file_operations == 2) {
3757 {
3758#line 924
3759 wb_smsc_wdt_release(var_group2, var_group1);
3760#line 929
3761 ldv_s_wb_smsc_wdt_fops_file_operations = 0;
3762 }
3763 } else {
3764
3765 }
3766#line 935
3767 goto ldv_18269;
3768 case_3:
3769 {
3770#line 955
3771 wb_smsc_wdt_ioctl(var_group1, var_wb_smsc_wdt_ioctl_22_p1, var_wb_smsc_wdt_ioctl_22_p2);
3772 }
3773#line 966
3774 goto ldv_18269;
3775 case_4:
3776 {
3777#line 986
3778 wb_smsc_wdt_notify_sys(var_group3, var_wb_smsc_wdt_notify_sys_23_p1, var_wb_smsc_wdt_notify_sys_23_p2);
3779 }
3780#line 997
3781 goto ldv_18269;
3782 switch_default: ;
3783#line 998
3784 goto ldv_18269;
3785 } else {
3786 switch_break: ;
3787 }
3788 }
3789 }
3790 ldv_18269: ;
3791 ldv_18276:
3792 {
3793#line 831
3794 tmp___1 = __VERIFIER_nondet_int();
3795 }
3796#line 831
3797 if (tmp___1 != 0) {
3798#line 833
3799 goto ldv_18275;
3800 } else
3801#line 831
3802 if (ldv_s_wb_smsc_wdt_fops_file_operations != 0) {
3803#line 833
3804 goto ldv_18275;
3805 } else {
3806#line 835
3807 goto ldv_18277;
3808 }
3809 ldv_18277: ;
3810 ldv_module_exit:
3811 {
3812#line 1021
3813 wb_smsc_wdt_exit();
3814 }
3815 ldv_final:
3816 {
3817#line 1028
3818 ldv_check_final_state();
3819 }
3820#line 1031
3821 return;
3822}
3823}
3824#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3825void ldv_blast_assert(void)
3826{
3827
3828 {
3829 ERROR: ;
3830#line 6
3831 goto ERROR;
3832}
3833}
3834#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3835extern int __VERIFIER_nondet_int(void) ;
3836#line 1052 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3837int ldv_spin = 0;
3838#line 1056 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3839void ldv_check_alloc_flags(gfp_t flags )
3840{
3841
3842 {
3843#line 1059
3844 if (ldv_spin != 0) {
3845#line 1059
3846 if (flags != 32U) {
3847 {
3848#line 1059
3849 ldv_blast_assert();
3850 }
3851 } else {
3852
3853 }
3854 } else {
3855
3856 }
3857#line 1062
3858 return;
3859}
3860}
3861#line 1062
3862extern struct page *ldv_some_page(void) ;
3863#line 1065 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3864struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
3865{ struct page *tmp ;
3866
3867 {
3868#line 1068
3869 if (ldv_spin != 0) {
3870#line 1068
3871 if (flags != 32U) {
3872 {
3873#line 1068
3874 ldv_blast_assert();
3875 }
3876 } else {
3877
3878 }
3879 } else {
3880
3881 }
3882 {
3883#line 1070
3884 tmp = ldv_some_page();
3885 }
3886#line 1070
3887 return (tmp);
3888}
3889}
3890#line 1074 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3891void ldv_check_alloc_nonatomic(void)
3892{
3893
3894 {
3895#line 1077
3896 if (ldv_spin != 0) {
3897 {
3898#line 1077
3899 ldv_blast_assert();
3900 }
3901 } else {
3902
3903 }
3904#line 1080
3905 return;
3906}
3907}
3908#line 1081 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3909void ldv_spin_lock(void)
3910{
3911
3912 {
3913#line 1084
3914 ldv_spin = 1;
3915#line 1085
3916 return;
3917}
3918}
3919#line 1088 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3920void ldv_spin_unlock(void)
3921{
3922
3923 {
3924#line 1091
3925 ldv_spin = 0;
3926#line 1092
3927 return;
3928}
3929}
3930#line 1095 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3931int ldv_spin_trylock(void)
3932{ int is_lock ;
3933
3934 {
3935 {
3936#line 1100
3937 is_lock = __VERIFIER_nondet_int();
3938 }
3939#line 1102
3940 if (is_lock != 0) {
3941#line 1105
3942 return (0);
3943 } else {
3944#line 1110
3945 ldv_spin = 1;
3946#line 1112
3947 return (1);
3948 }
3949}
3950}
3951#line 1116 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3952__inline static void spin_lock(spinlock_t *lock )
3953{
3954
3955 {
3956 {
3957#line 1121
3958 ldv_spin_lock();
3959#line 1123
3960 ldv_spin_lock_1(lock);
3961 }
3962#line 1124
3963 return;
3964}
3965}
3966#line 1158 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3967__inline static void spin_unlock(spinlock_t *lock )
3968{
3969
3970 {
3971 {
3972#line 1163
3973 ldv_spin_unlock();
3974#line 1165
3975 ldv_spin_unlock_5(lock);
3976 }
3977#line 1166
3978 return;
3979}
3980}
3981#line 1279 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3982void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
3983{
3984
3985 {
3986 {
3987#line 1285
3988 ldv_check_alloc_flags(ldv_func_arg2);
3989#line 1287
3990 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
3991 }
3992#line 1288
3993 return ((void *)0);
3994}
3995}