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