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