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