1
2
3
4#line 19 "include/asm-generic/int-ll64.h"
5typedef signed char __s8;
6#line 22 "include/asm-generic/int-ll64.h"
7typedef short __s16;
8#line 23 "include/asm-generic/int-ll64.h"
9typedef unsigned short __u16;
10#line 25 "include/asm-generic/int-ll64.h"
11typedef int __s32;
12#line 26 "include/asm-generic/int-ll64.h"
13typedef unsigned int __u32;
14#line 30 "include/asm-generic/int-ll64.h"
15typedef unsigned long long __u64;
16#line 43 "include/asm-generic/int-ll64.h"
17typedef unsigned char u8;
18#line 45 "include/asm-generic/int-ll64.h"
19typedef short s16;
20#line 46 "include/asm-generic/int-ll64.h"
21typedef unsigned short u16;
22#line 48 "include/asm-generic/int-ll64.h"
23typedef int s32;
24#line 49 "include/asm-generic/int-ll64.h"
25typedef unsigned int u32;
26#line 51 "include/asm-generic/int-ll64.h"
27typedef long long s64;
28#line 52 "include/asm-generic/int-ll64.h"
29typedef unsigned long long u64;
30#line 14 "include/asm-generic/posix_types.h"
31typedef long __kernel_long_t;
32#line 15 "include/asm-generic/posix_types.h"
33typedef unsigned long __kernel_ulong_t;
34#line 52 "include/asm-generic/posix_types.h"
35typedef unsigned int __kernel_uid32_t;
36#line 53 "include/asm-generic/posix_types.h"
37typedef unsigned int __kernel_gid32_t;
38#line 75 "include/asm-generic/posix_types.h"
39typedef __kernel_ulong_t __kernel_size_t;
40#line 76 "include/asm-generic/posix_types.h"
41typedef __kernel_long_t __kernel_ssize_t;
42#line 91 "include/asm-generic/posix_types.h"
43typedef long long __kernel_loff_t;
44#line 92 "include/asm-generic/posix_types.h"
45typedef __kernel_long_t __kernel_time_t;
46#line 21 "include/linux/types.h"
47typedef __u32 __kernel_dev_t;
48#line 24 "include/linux/types.h"
49typedef __kernel_dev_t dev_t;
50#line 27 "include/linux/types.h"
51typedef unsigned short umode_t;
52#line 38 "include/linux/types.h"
53typedef _Bool bool;
54#line 40 "include/linux/types.h"
55typedef __kernel_uid32_t uid_t;
56#line 41 "include/linux/types.h"
57typedef __kernel_gid32_t gid_t;
58#line 54 "include/linux/types.h"
59typedef __kernel_loff_t loff_t;
60#line 63 "include/linux/types.h"
61typedef __kernel_size_t size_t;
62#line 68 "include/linux/types.h"
63typedef __kernel_ssize_t ssize_t;
64#line 78 "include/linux/types.h"
65typedef __kernel_time_t time_t;
66#line 142 "include/linux/types.h"
67typedef unsigned long sector_t;
68#line 143 "include/linux/types.h"
69typedef unsigned long blkcnt_t;
70#line 202 "include/linux/types.h"
71typedef unsigned int gfp_t;
72#line 203 "include/linux/types.h"
73typedef unsigned int fmode_t;
74#line 206 "include/linux/types.h"
75typedef u64 phys_addr_t;
76#line 211 "include/linux/types.h"
77typedef phys_addr_t resource_size_t;
78#line 221 "include/linux/types.h"
79struct __anonstruct_atomic_t_6 {
80 int counter ;
81};
82#line 221 "include/linux/types.h"
83typedef struct __anonstruct_atomic_t_6 atomic_t;
84#line 226 "include/linux/types.h"
85struct __anonstruct_atomic64_t_7 {
86 long counter ;
87};
88#line 226 "include/linux/types.h"
89typedef struct __anonstruct_atomic64_t_7 atomic64_t;
90#line 227 "include/linux/types.h"
91struct list_head {
92 struct list_head *next ;
93 struct list_head *prev ;
94};
95#line 232
96struct hlist_node;
97#line 232 "include/linux/types.h"
98struct hlist_head {
99 struct hlist_node *first ;
100};
101#line 236 "include/linux/types.h"
102struct hlist_node {
103 struct hlist_node *next ;
104 struct hlist_node **pprev ;
105};
106#line 247 "include/linux/types.h"
107struct rcu_head {
108 struct rcu_head *next ;
109 void (*func)(struct rcu_head * ) ;
110};
111#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
112struct module;
113#line 55
114struct module;
115#line 146 "include/linux/init.h"
116typedef void (*ctor_fn_t)(void);
117#line 46 "include/linux/dynamic_debug.h"
118struct device;
119#line 46
120struct device;
121#line 348 "include/linux/kernel.h"
122struct pid;
123#line 348
124struct pid;
125#line 112 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/stat.h"
126struct timespec;
127#line 112
128struct timespec;
129#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
130struct page;
131#line 58
132struct page;
133#line 26 "include/asm-generic/getorder.h"
134struct task_struct;
135#line 26
136struct task_struct;
137#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
138struct file;
139#line 290
140struct file;
141#line 305
142struct seq_file;
143#line 305
144struct seq_file;
145#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
146struct arch_spinlock;
147#line 327
148struct arch_spinlock;
149#line 306 "include/linux/bitmap.h"
150struct bug_entry {
151 int bug_addr_disp ;
152 int file_disp ;
153 unsigned short line ;
154 unsigned short flags ;
155};
156#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
157struct static_key;
158#line 234
159struct static_key;
160#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
161struct kmem_cache;
162#line 23 "include/asm-generic/atomic-long.h"
163typedef atomic64_t atomic_long_t;
164#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
165typedef u16 __ticket_t;
166#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
167typedef u32 __ticketpair_t;
168#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
169struct __raw_tickets {
170 __ticket_t head ;
171 __ticket_t tail ;
172};
173#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
174union __anonunion_ldv_5907_29 {
175 __ticketpair_t head_tail ;
176 struct __raw_tickets tickets ;
177};
178#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
179struct arch_spinlock {
180 union __anonunion_ldv_5907_29 ldv_5907 ;
181};
182#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
183typedef struct arch_spinlock arch_spinlock_t;
184#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
185struct __anonstruct_ldv_5914_31 {
186 u32 read ;
187 s32 write ;
188};
189#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
190union __anonunion_arch_rwlock_t_30 {
191 s64 lock ;
192 struct __anonstruct_ldv_5914_31 ldv_5914 ;
193};
194#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
195typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
196#line 34
197struct lockdep_map;
198#line 34
199struct lockdep_map;
200#line 55 "include/linux/debug_locks.h"
201struct stack_trace {
202 unsigned int nr_entries ;
203 unsigned int max_entries ;
204 unsigned long *entries ;
205 int skip ;
206};
207#line 26 "include/linux/stacktrace.h"
208struct lockdep_subclass_key {
209 char __one_byte ;
210};
211#line 53 "include/linux/lockdep.h"
212struct lock_class_key {
213 struct lockdep_subclass_key subkeys[8U] ;
214};
215#line 59 "include/linux/lockdep.h"
216struct lock_class {
217 struct list_head hash_entry ;
218 struct list_head lock_entry ;
219 struct lockdep_subclass_key *key ;
220 unsigned int subclass ;
221 unsigned int dep_gen_id ;
222 unsigned long usage_mask ;
223 struct stack_trace usage_traces[13U] ;
224 struct list_head locks_after ;
225 struct list_head locks_before ;
226 unsigned int version ;
227 unsigned long ops ;
228 char const *name ;
229 int name_version ;
230 unsigned long contention_point[4U] ;
231 unsigned long contending_point[4U] ;
232};
233#line 144 "include/linux/lockdep.h"
234struct lockdep_map {
235 struct lock_class_key *key ;
236 struct lock_class *class_cache[2U] ;
237 char const *name ;
238 int cpu ;
239 unsigned long ip ;
240};
241#line 556 "include/linux/lockdep.h"
242struct raw_spinlock {
243 arch_spinlock_t raw_lock ;
244 unsigned int magic ;
245 unsigned int owner_cpu ;
246 void *owner ;
247 struct lockdep_map dep_map ;
248};
249#line 32 "include/linux/spinlock_types.h"
250typedef struct raw_spinlock raw_spinlock_t;
251#line 33 "include/linux/spinlock_types.h"
252struct __anonstruct_ldv_6122_33 {
253 u8 __padding[24U] ;
254 struct lockdep_map dep_map ;
255};
256#line 33 "include/linux/spinlock_types.h"
257union __anonunion_ldv_6123_32 {
258 struct raw_spinlock rlock ;
259 struct __anonstruct_ldv_6122_33 ldv_6122 ;
260};
261#line 33 "include/linux/spinlock_types.h"
262struct spinlock {
263 union __anonunion_ldv_6123_32 ldv_6123 ;
264};
265#line 76 "include/linux/spinlock_types.h"
266typedef struct spinlock spinlock_t;
267#line 23 "include/linux/rwlock_types.h"
268struct __anonstruct_rwlock_t_34 {
269 arch_rwlock_t raw_lock ;
270 unsigned int magic ;
271 unsigned int owner_cpu ;
272 void *owner ;
273 struct lockdep_map dep_map ;
274};
275#line 23 "include/linux/rwlock_types.h"
276typedef struct __anonstruct_rwlock_t_34 rwlock_t;
277#line 110 "include/linux/seqlock.h"
278struct seqcount {
279 unsigned int sequence ;
280};
281#line 121 "include/linux/seqlock.h"
282typedef struct seqcount seqcount_t;
283#line 254 "include/linux/seqlock.h"
284struct timespec {
285 __kernel_time_t tv_sec ;
286 long tv_nsec ;
287};
288#line 286 "include/linux/time.h"
289struct kstat {
290 u64 ino ;
291 dev_t dev ;
292 umode_t mode ;
293 unsigned int nlink ;
294 uid_t uid ;
295 gid_t gid ;
296 dev_t rdev ;
297 loff_t size ;
298 struct timespec atime ;
299 struct timespec mtime ;
300 struct timespec ctime ;
301 unsigned long blksize ;
302 unsigned long long blocks ;
303};
304#line 48 "include/linux/wait.h"
305struct __wait_queue_head {
306 spinlock_t lock ;
307 struct list_head task_list ;
308};
309#line 53 "include/linux/wait.h"
310typedef struct __wait_queue_head wait_queue_head_t;
311#line 670 "include/linux/mmzone.h"
312struct mutex {
313 atomic_t count ;
314 spinlock_t wait_lock ;
315 struct list_head wait_list ;
316 struct task_struct *owner ;
317 char const *name ;
318 void *magic ;
319 struct lockdep_map dep_map ;
320};
321#line 171 "include/linux/mutex.h"
322struct rw_semaphore;
323#line 171
324struct rw_semaphore;
325#line 172 "include/linux/mutex.h"
326struct rw_semaphore {
327 long count ;
328 raw_spinlock_t wait_lock ;
329 struct list_head wait_list ;
330 struct lockdep_map dep_map ;
331};
332#line 188 "include/linux/rcupdate.h"
333struct notifier_block;
334#line 188
335struct notifier_block;
336#line 239 "include/linux/srcu.h"
337struct notifier_block {
338 int (*notifier_call)(struct notifier_block * , unsigned long , void * ) ;
339 struct notifier_block *next ;
340 int priority ;
341};
342#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
343struct resource {
344 resource_size_t start ;
345 resource_size_t end ;
346 char const *name ;
347 unsigned long flags ;
348 struct resource *parent ;
349 struct resource *sibling ;
350 struct resource *child ;
351};
352#line 18 "include/asm-generic/pci_iomap.h"
353struct vm_area_struct;
354#line 18
355struct vm_area_struct;
356#line 37 "include/linux/kmod.h"
357struct cred;
358#line 37
359struct cred;
360#line 18 "include/linux/elf.h"
361typedef __u64 Elf64_Addr;
362#line 19 "include/linux/elf.h"
363typedef __u16 Elf64_Half;
364#line 23 "include/linux/elf.h"
365typedef __u32 Elf64_Word;
366#line 24 "include/linux/elf.h"
367typedef __u64 Elf64_Xword;
368#line 193 "include/linux/elf.h"
369struct elf64_sym {
370 Elf64_Word st_name ;
371 unsigned char st_info ;
372 unsigned char st_other ;
373 Elf64_Half st_shndx ;
374 Elf64_Addr st_value ;
375 Elf64_Xword st_size ;
376};
377#line 201 "include/linux/elf.h"
378typedef struct elf64_sym Elf64_Sym;
379#line 445
380struct sock;
381#line 445
382struct sock;
383#line 446
384struct kobject;
385#line 446
386struct kobject;
387#line 447
388enum kobj_ns_type {
389 KOBJ_NS_TYPE_NONE = 0,
390 KOBJ_NS_TYPE_NET = 1,
391 KOBJ_NS_TYPES = 2
392} ;
393#line 453 "include/linux/elf.h"
394struct kobj_ns_type_operations {
395 enum kobj_ns_type type ;
396 void *(*grab_current_ns)(void) ;
397 void const *(*netlink_ns)(struct sock * ) ;
398 void const *(*initial_ns)(void) ;
399 void (*drop_ns)(void * ) ;
400};
401#line 57 "include/linux/kobject_ns.h"
402struct attribute {
403 char const *name ;
404 umode_t mode ;
405 struct lock_class_key *key ;
406 struct lock_class_key skey ;
407};
408#line 98 "include/linux/sysfs.h"
409struct sysfs_ops {
410 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
411 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
412 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
413};
414#line 117
415struct sysfs_dirent;
416#line 117
417struct sysfs_dirent;
418#line 182 "include/linux/sysfs.h"
419struct kref {
420 atomic_t refcount ;
421};
422#line 49 "include/linux/kobject.h"
423struct kset;
424#line 49
425struct kobj_type;
426#line 49 "include/linux/kobject.h"
427struct kobject {
428 char const *name ;
429 struct list_head entry ;
430 struct kobject *parent ;
431 struct kset *kset ;
432 struct kobj_type *ktype ;
433 struct sysfs_dirent *sd ;
434 struct kref kref ;
435 unsigned char state_initialized : 1 ;
436 unsigned char state_in_sysfs : 1 ;
437 unsigned char state_add_uevent_sent : 1 ;
438 unsigned char state_remove_uevent_sent : 1 ;
439 unsigned char uevent_suppress : 1 ;
440};
441#line 107 "include/linux/kobject.h"
442struct kobj_type {
443 void (*release)(struct kobject * ) ;
444 struct sysfs_ops const *sysfs_ops ;
445 struct attribute **default_attrs ;
446 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
447 void const *(*namespace)(struct kobject * ) ;
448};
449#line 115 "include/linux/kobject.h"
450struct kobj_uevent_env {
451 char *envp[32U] ;
452 int envp_idx ;
453 char buf[2048U] ;
454 int buflen ;
455};
456#line 122 "include/linux/kobject.h"
457struct kset_uevent_ops {
458 int (* const filter)(struct kset * , struct kobject * ) ;
459 char const *(* const name)(struct kset * , struct kobject * ) ;
460 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
461};
462#line 139 "include/linux/kobject.h"
463struct kset {
464 struct list_head list ;
465 spinlock_t list_lock ;
466 struct kobject kobj ;
467 struct kset_uevent_ops const *uevent_ops ;
468};
469#line 215
470struct kernel_param;
471#line 215
472struct kernel_param;
473#line 216 "include/linux/kobject.h"
474struct kernel_param_ops {
475 int (*set)(char const * , struct kernel_param const * ) ;
476 int (*get)(char * , struct kernel_param const * ) ;
477 void (*free)(void * ) ;
478};
479#line 49 "include/linux/moduleparam.h"
480struct kparam_string;
481#line 49
482struct kparam_array;
483#line 49 "include/linux/moduleparam.h"
484union __anonunion_ldv_13363_134 {
485 void *arg ;
486 struct kparam_string const *str ;
487 struct kparam_array const *arr ;
488};
489#line 49 "include/linux/moduleparam.h"
490struct kernel_param {
491 char const *name ;
492 struct kernel_param_ops const *ops ;
493 u16 perm ;
494 s16 level ;
495 union __anonunion_ldv_13363_134 ldv_13363 ;
496};
497#line 61 "include/linux/moduleparam.h"
498struct kparam_string {
499 unsigned int maxlen ;
500 char *string ;
501};
502#line 67 "include/linux/moduleparam.h"
503struct kparam_array {
504 unsigned int max ;
505 unsigned int elemsize ;
506 unsigned int *num ;
507 struct kernel_param_ops const *ops ;
508 void *elem ;
509};
510#line 458 "include/linux/moduleparam.h"
511struct static_key {
512 atomic_t enabled ;
513};
514#line 225 "include/linux/jump_label.h"
515struct tracepoint;
516#line 225
517struct tracepoint;
518#line 226 "include/linux/jump_label.h"
519struct tracepoint_func {
520 void *func ;
521 void *data ;
522};
523#line 29 "include/linux/tracepoint.h"
524struct tracepoint {
525 char const *name ;
526 struct static_key key ;
527 void (*regfunc)(void) ;
528 void (*unregfunc)(void) ;
529 struct tracepoint_func *funcs ;
530};
531#line 86 "include/linux/tracepoint.h"
532struct kernel_symbol {
533 unsigned long value ;
534 char const *name ;
535};
536#line 27 "include/linux/export.h"
537struct mod_arch_specific {
538
539};
540#line 34 "include/linux/module.h"
541struct module_param_attrs;
542#line 34 "include/linux/module.h"
543struct module_kobject {
544 struct kobject kobj ;
545 struct module *mod ;
546 struct kobject *drivers_dir ;
547 struct module_param_attrs *mp ;
548};
549#line 43 "include/linux/module.h"
550struct module_attribute {
551 struct attribute attr ;
552 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
553 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
554 size_t ) ;
555 void (*setup)(struct module * , char const * ) ;
556 int (*test)(struct module * ) ;
557 void (*free)(struct module * ) ;
558};
559#line 69
560struct exception_table_entry;
561#line 69
562struct exception_table_entry;
563#line 198
564enum module_state {
565 MODULE_STATE_LIVE = 0,
566 MODULE_STATE_COMING = 1,
567 MODULE_STATE_GOING = 2
568} ;
569#line 204 "include/linux/module.h"
570struct module_ref {
571 unsigned long incs ;
572 unsigned long decs ;
573};
574#line 219
575struct module_sect_attrs;
576#line 219
577struct module_notes_attrs;
578#line 219
579struct ftrace_event_call;
580#line 219 "include/linux/module.h"
581struct module {
582 enum module_state state ;
583 struct list_head list ;
584 char name[56U] ;
585 struct module_kobject mkobj ;
586 struct module_attribute *modinfo_attrs ;
587 char const *version ;
588 char const *srcversion ;
589 struct kobject *holders_dir ;
590 struct kernel_symbol const *syms ;
591 unsigned long const *crcs ;
592 unsigned int num_syms ;
593 struct kernel_param *kp ;
594 unsigned int num_kp ;
595 unsigned int num_gpl_syms ;
596 struct kernel_symbol const *gpl_syms ;
597 unsigned long const *gpl_crcs ;
598 struct kernel_symbol const *unused_syms ;
599 unsigned long const *unused_crcs ;
600 unsigned int num_unused_syms ;
601 unsigned int num_unused_gpl_syms ;
602 struct kernel_symbol const *unused_gpl_syms ;
603 unsigned long const *unused_gpl_crcs ;
604 struct kernel_symbol const *gpl_future_syms ;
605 unsigned long const *gpl_future_crcs ;
606 unsigned int num_gpl_future_syms ;
607 unsigned int num_exentries ;
608 struct exception_table_entry *extable ;
609 int (*init)(void) ;
610 void *module_init ;
611 void *module_core ;
612 unsigned int init_size ;
613 unsigned int core_size ;
614 unsigned int init_text_size ;
615 unsigned int core_text_size ;
616 unsigned int init_ro_size ;
617 unsigned int core_ro_size ;
618 struct mod_arch_specific arch ;
619 unsigned int taints ;
620 unsigned int num_bugs ;
621 struct list_head bug_list ;
622 struct bug_entry *bug_table ;
623 Elf64_Sym *symtab ;
624 Elf64_Sym *core_symtab ;
625 unsigned int num_symtab ;
626 unsigned int core_num_syms ;
627 char *strtab ;
628 char *core_strtab ;
629 struct module_sect_attrs *sect_attrs ;
630 struct module_notes_attrs *notes_attrs ;
631 char *args ;
632 void *percpu ;
633 unsigned int percpu_size ;
634 unsigned int num_tracepoints ;
635 struct tracepoint * const *tracepoints_ptrs ;
636 unsigned int num_trace_bprintk_fmt ;
637 char const **trace_bprintk_fmt_start ;
638 struct ftrace_event_call **trace_events ;
639 unsigned int num_trace_events ;
640 struct list_head source_list ;
641 struct list_head target_list ;
642 struct task_struct *waiter ;
643 void (*exit)(void) ;
644 struct module_ref *refptr ;
645 ctor_fn_t (**ctors)(void) ;
646 unsigned int num_ctors ;
647};
648#line 88 "include/linux/kmemleak.h"
649struct kmem_cache_cpu {
650 void **freelist ;
651 unsigned long tid ;
652 struct page *page ;
653 struct page *partial ;
654 int node ;
655 unsigned int stat[26U] ;
656};
657#line 55 "include/linux/slub_def.h"
658struct kmem_cache_node {
659 spinlock_t list_lock ;
660 unsigned long nr_partial ;
661 struct list_head partial ;
662 atomic_long_t nr_slabs ;
663 atomic_long_t total_objects ;
664 struct list_head full ;
665};
666#line 66 "include/linux/slub_def.h"
667struct kmem_cache_order_objects {
668 unsigned long x ;
669};
670#line 76 "include/linux/slub_def.h"
671struct kmem_cache {
672 struct kmem_cache_cpu *cpu_slab ;
673 unsigned long flags ;
674 unsigned long min_partial ;
675 int size ;
676 int objsize ;
677 int offset ;
678 int cpu_partial ;
679 struct kmem_cache_order_objects oo ;
680 struct kmem_cache_order_objects max ;
681 struct kmem_cache_order_objects min ;
682 gfp_t allocflags ;
683 int refcount ;
684 void (*ctor)(void * ) ;
685 int inuse ;
686 int align ;
687 int reserved ;
688 char const *name ;
689 struct list_head list ;
690 struct kobject kobj ;
691 int remote_node_defrag_ratio ;
692 struct kmem_cache_node *node[1024U] ;
693};
694#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
695struct file_operations;
696#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
697struct miscdevice {
698 int minor ;
699 char const *name ;
700 struct file_operations const *fops ;
701 struct list_head list ;
702 struct device *parent ;
703 struct device *this_device ;
704 char const *nodename ;
705 umode_t mode ;
706};
707#line 57 "include/linux/delay.h"
708struct block_device;
709#line 57
710struct block_device;
711#line 93 "include/linux/bit_spinlock.h"
712struct hlist_bl_node;
713#line 93 "include/linux/bit_spinlock.h"
714struct hlist_bl_head {
715 struct hlist_bl_node *first ;
716};
717#line 36 "include/linux/list_bl.h"
718struct hlist_bl_node {
719 struct hlist_bl_node *next ;
720 struct hlist_bl_node **pprev ;
721};
722#line 114 "include/linux/rculist_bl.h"
723struct nameidata;
724#line 114
725struct nameidata;
726#line 115
727struct path;
728#line 115
729struct path;
730#line 116
731struct vfsmount;
732#line 116
733struct vfsmount;
734#line 117 "include/linux/rculist_bl.h"
735struct qstr {
736 unsigned int hash ;
737 unsigned int len ;
738 unsigned char const *name ;
739};
740#line 72 "include/linux/dcache.h"
741struct inode;
742#line 72
743struct dentry_operations;
744#line 72
745struct super_block;
746#line 72 "include/linux/dcache.h"
747union __anonunion_d_u_135 {
748 struct list_head d_child ;
749 struct rcu_head d_rcu ;
750};
751#line 72 "include/linux/dcache.h"
752struct dentry {
753 unsigned int d_flags ;
754 seqcount_t d_seq ;
755 struct hlist_bl_node d_hash ;
756 struct dentry *d_parent ;
757 struct qstr d_name ;
758 struct inode *d_inode ;
759 unsigned char d_iname[32U] ;
760 unsigned int d_count ;
761 spinlock_t d_lock ;
762 struct dentry_operations const *d_op ;
763 struct super_block *d_sb ;
764 unsigned long d_time ;
765 void *d_fsdata ;
766 struct list_head d_lru ;
767 union __anonunion_d_u_135 d_u ;
768 struct list_head d_subdirs ;
769 struct list_head d_alias ;
770};
771#line 123 "include/linux/dcache.h"
772struct dentry_operations {
773 int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
774 int (*d_hash)(struct dentry const * , struct inode const * , struct qstr * ) ;
775 int (*d_compare)(struct dentry const * , struct inode const * , struct dentry const * ,
776 struct inode const * , unsigned int , char const * , struct qstr const * ) ;
777 int (*d_delete)(struct dentry const * ) ;
778 void (*d_release)(struct dentry * ) ;
779 void (*d_prune)(struct dentry * ) ;
780 void (*d_iput)(struct dentry * , struct inode * ) ;
781 char *(*d_dname)(struct dentry * , char * , int ) ;
782 struct vfsmount *(*d_automount)(struct path * ) ;
783 int (*d_manage)(struct dentry * , bool ) ;
784};
785#line 402 "include/linux/dcache.h"
786struct path {
787 struct vfsmount *mnt ;
788 struct dentry *dentry ;
789};
790#line 58 "include/linux/radix-tree.h"
791struct radix_tree_node;
792#line 58 "include/linux/radix-tree.h"
793struct radix_tree_root {
794 unsigned int height ;
795 gfp_t gfp_mask ;
796 struct radix_tree_node *rnode ;
797};
798#line 377
799struct prio_tree_node;
800#line 19 "include/linux/prio_tree.h"
801struct prio_tree_node {
802 struct prio_tree_node *left ;
803 struct prio_tree_node *right ;
804 struct prio_tree_node *parent ;
805 unsigned long start ;
806 unsigned long last ;
807};
808#line 27 "include/linux/prio_tree.h"
809struct prio_tree_root {
810 struct prio_tree_node *prio_tree_node ;
811 unsigned short index_bits ;
812 unsigned short raw ;
813};
814#line 111
815enum pid_type {
816 PIDTYPE_PID = 0,
817 PIDTYPE_PGID = 1,
818 PIDTYPE_SID = 2,
819 PIDTYPE_MAX = 3
820} ;
821#line 118
822struct pid_namespace;
823#line 118 "include/linux/prio_tree.h"
824struct upid {
825 int nr ;
826 struct pid_namespace *ns ;
827 struct hlist_node pid_chain ;
828};
829#line 56 "include/linux/pid.h"
830struct pid {
831 atomic_t count ;
832 unsigned int level ;
833 struct hlist_head tasks[3U] ;
834 struct rcu_head rcu ;
835 struct upid numbers[1U] ;
836};
837#line 45 "include/linux/semaphore.h"
838struct fiemap_extent {
839 __u64 fe_logical ;
840 __u64 fe_physical ;
841 __u64 fe_length ;
842 __u64 fe_reserved64[2U] ;
843 __u32 fe_flags ;
844 __u32 fe_reserved[3U] ;
845};
846#line 38 "include/linux/fiemap.h"
847struct shrink_control {
848 gfp_t gfp_mask ;
849 unsigned long nr_to_scan ;
850};
851#line 14 "include/linux/shrinker.h"
852struct shrinker {
853 int (*shrink)(struct shrinker * , struct shrink_control * ) ;
854 int seeks ;
855 long batch ;
856 struct list_head list ;
857 atomic_long_t nr_in_batch ;
858};
859#line 43
860enum migrate_mode {
861 MIGRATE_ASYNC = 0,
862 MIGRATE_SYNC_LIGHT = 1,
863 MIGRATE_SYNC = 2
864} ;
865#line 49
866struct export_operations;
867#line 49
868struct export_operations;
869#line 51
870struct iovec;
871#line 51
872struct iovec;
873#line 52
874struct kiocb;
875#line 52
876struct kiocb;
877#line 53
878struct pipe_inode_info;
879#line 53
880struct pipe_inode_info;
881#line 54
882struct poll_table_struct;
883#line 54
884struct poll_table_struct;
885#line 55
886struct kstatfs;
887#line 55
888struct kstatfs;
889#line 435 "include/linux/fs.h"
890struct iattr {
891 unsigned int ia_valid ;
892 umode_t ia_mode ;
893 uid_t ia_uid ;
894 gid_t ia_gid ;
895 loff_t ia_size ;
896 struct timespec ia_atime ;
897 struct timespec ia_mtime ;
898 struct timespec ia_ctime ;
899 struct file *ia_file ;
900};
901#line 119 "include/linux/quota.h"
902struct if_dqinfo {
903 __u64 dqi_bgrace ;
904 __u64 dqi_igrace ;
905 __u32 dqi_flags ;
906 __u32 dqi_valid ;
907};
908#line 176 "include/linux/percpu_counter.h"
909struct fs_disk_quota {
910 __s8 d_version ;
911 __s8 d_flags ;
912 __u16 d_fieldmask ;
913 __u32 d_id ;
914 __u64 d_blk_hardlimit ;
915 __u64 d_blk_softlimit ;
916 __u64 d_ino_hardlimit ;
917 __u64 d_ino_softlimit ;
918 __u64 d_bcount ;
919 __u64 d_icount ;
920 __s32 d_itimer ;
921 __s32 d_btimer ;
922 __u16 d_iwarns ;
923 __u16 d_bwarns ;
924 __s32 d_padding2 ;
925 __u64 d_rtb_hardlimit ;
926 __u64 d_rtb_softlimit ;
927 __u64 d_rtbcount ;
928 __s32 d_rtbtimer ;
929 __u16 d_rtbwarns ;
930 __s16 d_padding3 ;
931 char d_padding4[8U] ;
932};
933#line 75 "include/linux/dqblk_xfs.h"
934struct fs_qfilestat {
935 __u64 qfs_ino ;
936 __u64 qfs_nblks ;
937 __u32 qfs_nextents ;
938};
939#line 150 "include/linux/dqblk_xfs.h"
940typedef struct fs_qfilestat fs_qfilestat_t;
941#line 151 "include/linux/dqblk_xfs.h"
942struct fs_quota_stat {
943 __s8 qs_version ;
944 __u16 qs_flags ;
945 __s8 qs_pad ;
946 fs_qfilestat_t qs_uquota ;
947 fs_qfilestat_t qs_gquota ;
948 __u32 qs_incoredqs ;
949 __s32 qs_btimelimit ;
950 __s32 qs_itimelimit ;
951 __s32 qs_rtbtimelimit ;
952 __u16 qs_bwarnlimit ;
953 __u16 qs_iwarnlimit ;
954};
955#line 165
956struct dquot;
957#line 165
958struct dquot;
959#line 185 "include/linux/quota.h"
960typedef __kernel_uid32_t qid_t;
961#line 186 "include/linux/quota.h"
962typedef long long qsize_t;
963#line 189 "include/linux/quota.h"
964struct mem_dqblk {
965 qsize_t dqb_bhardlimit ;
966 qsize_t dqb_bsoftlimit ;
967 qsize_t dqb_curspace ;
968 qsize_t dqb_rsvspace ;
969 qsize_t dqb_ihardlimit ;
970 qsize_t dqb_isoftlimit ;
971 qsize_t dqb_curinodes ;
972 time_t dqb_btime ;
973 time_t dqb_itime ;
974};
975#line 211
976struct quota_format_type;
977#line 211
978struct quota_format_type;
979#line 212 "include/linux/quota.h"
980struct mem_dqinfo {
981 struct quota_format_type *dqi_format ;
982 int dqi_fmt_id ;
983 struct list_head dqi_dirty_list ;
984 unsigned long dqi_flags ;
985 unsigned int dqi_bgrace ;
986 unsigned int dqi_igrace ;
987 qsize_t dqi_maxblimit ;
988 qsize_t dqi_maxilimit ;
989 void *dqi_priv ;
990};
991#line 275 "include/linux/quota.h"
992struct dquot {
993 struct hlist_node dq_hash ;
994 struct list_head dq_inuse ;
995 struct list_head dq_free ;
996 struct list_head dq_dirty ;
997 struct mutex dq_lock ;
998 atomic_t dq_count ;
999 wait_queue_head_t dq_wait_unused ;
1000 struct super_block *dq_sb ;
1001 unsigned int dq_id ;
1002 loff_t dq_off ;
1003 unsigned long dq_flags ;
1004 short dq_type ;
1005 struct mem_dqblk dq_dqb ;
1006};
1007#line 303 "include/linux/quota.h"
1008struct quota_format_ops {
1009 int (*check_quota_file)(struct super_block * , int ) ;
1010 int (*read_file_info)(struct super_block * , int ) ;
1011 int (*write_file_info)(struct super_block * , int ) ;
1012 int (*free_file_info)(struct super_block * , int ) ;
1013 int (*read_dqblk)(struct dquot * ) ;
1014 int (*commit_dqblk)(struct dquot * ) ;
1015 int (*release_dqblk)(struct dquot * ) ;
1016};
1017#line 314 "include/linux/quota.h"
1018struct dquot_operations {
1019 int (*write_dquot)(struct dquot * ) ;
1020 struct dquot *(*alloc_dquot)(struct super_block * , int ) ;
1021 void (*destroy_dquot)(struct dquot * ) ;
1022 int (*acquire_dquot)(struct dquot * ) ;
1023 int (*release_dquot)(struct dquot * ) ;
1024 int (*mark_dirty)(struct dquot * ) ;
1025 int (*write_info)(struct super_block * , int ) ;
1026 qsize_t *(*get_reserved_space)(struct inode * ) ;
1027};
1028#line 328 "include/linux/quota.h"
1029struct quotactl_ops {
1030 int (*quota_on)(struct super_block * , int , int , struct path * ) ;
1031 int (*quota_on_meta)(struct super_block * , int , int ) ;
1032 int (*quota_off)(struct super_block * , int ) ;
1033 int (*quota_sync)(struct super_block * , int , int ) ;
1034 int (*get_info)(struct super_block * , int , struct if_dqinfo * ) ;
1035 int (*set_info)(struct super_block * , int , struct if_dqinfo * ) ;
1036 int (*get_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1037 int (*set_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1038 int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1039 int (*set_xstate)(struct super_block * , unsigned int , int ) ;
1040};
1041#line 344 "include/linux/quota.h"
1042struct quota_format_type {
1043 int qf_fmt_id ;
1044 struct quota_format_ops const *qf_ops ;
1045 struct module *qf_owner ;
1046 struct quota_format_type *qf_next ;
1047};
1048#line 390 "include/linux/quota.h"
1049struct quota_info {
1050 unsigned int flags ;
1051 struct mutex dqio_mutex ;
1052 struct mutex dqonoff_mutex ;
1053 struct rw_semaphore dqptr_sem ;
1054 struct inode *files[2U] ;
1055 struct mem_dqinfo info[2U] ;
1056 struct quota_format_ops const *ops[2U] ;
1057};
1058#line 421
1059struct address_space;
1060#line 421
1061struct address_space;
1062#line 422
1063struct writeback_control;
1064#line 422
1065struct writeback_control;
1066#line 585 "include/linux/fs.h"
1067union __anonunion_arg_138 {
1068 char *buf ;
1069 void *data ;
1070};
1071#line 585 "include/linux/fs.h"
1072struct __anonstruct_read_descriptor_t_137 {
1073 size_t written ;
1074 size_t count ;
1075 union __anonunion_arg_138 arg ;
1076 int error ;
1077};
1078#line 585 "include/linux/fs.h"
1079typedef struct __anonstruct_read_descriptor_t_137 read_descriptor_t;
1080#line 588 "include/linux/fs.h"
1081struct address_space_operations {
1082 int (*writepage)(struct page * , struct writeback_control * ) ;
1083 int (*readpage)(struct file * , struct page * ) ;
1084 int (*writepages)(struct address_space * , struct writeback_control * ) ;
1085 int (*set_page_dirty)(struct page * ) ;
1086 int (*readpages)(struct file * , struct address_space * , struct list_head * ,
1087 unsigned int ) ;
1088 int (*write_begin)(struct file * , struct address_space * , loff_t , unsigned int ,
1089 unsigned int , struct page ** , void ** ) ;
1090 int (*write_end)(struct file * , struct address_space * , loff_t , unsigned int ,
1091 unsigned int , struct page * , void * ) ;
1092 sector_t (*bmap)(struct address_space * , sector_t ) ;
1093 void (*invalidatepage)(struct page * , unsigned long ) ;
1094 int (*releasepage)(struct page * , gfp_t ) ;
1095 void (*freepage)(struct page * ) ;
1096 ssize_t (*direct_IO)(int , struct kiocb * , struct iovec const * , loff_t ,
1097 unsigned long ) ;
1098 int (*get_xip_mem)(struct address_space * , unsigned long , int , void ** , unsigned long * ) ;
1099 int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode ) ;
1100 int (*launder_page)(struct page * ) ;
1101 int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long ) ;
1102 int (*error_remove_page)(struct address_space * , struct page * ) ;
1103};
1104#line 642
1105struct backing_dev_info;
1106#line 642
1107struct backing_dev_info;
1108#line 643 "include/linux/fs.h"
1109struct address_space {
1110 struct inode *host ;
1111 struct radix_tree_root page_tree ;
1112 spinlock_t tree_lock ;
1113 unsigned int i_mmap_writable ;
1114 struct prio_tree_root i_mmap ;
1115 struct list_head i_mmap_nonlinear ;
1116 struct mutex i_mmap_mutex ;
1117 unsigned long nrpages ;
1118 unsigned long writeback_index ;
1119 struct address_space_operations const *a_ops ;
1120 unsigned long flags ;
1121 struct backing_dev_info *backing_dev_info ;
1122 spinlock_t private_lock ;
1123 struct list_head private_list ;
1124 struct address_space *assoc_mapping ;
1125};
1126#line 664
1127struct request_queue;
1128#line 664
1129struct request_queue;
1130#line 665
1131struct hd_struct;
1132#line 665
1133struct gendisk;
1134#line 665 "include/linux/fs.h"
1135struct block_device {
1136 dev_t bd_dev ;
1137 int bd_openers ;
1138 struct inode *bd_inode ;
1139 struct super_block *bd_super ;
1140 struct mutex bd_mutex ;
1141 struct list_head bd_inodes ;
1142 void *bd_claiming ;
1143 void *bd_holder ;
1144 int bd_holders ;
1145 bool bd_write_holder ;
1146 struct list_head bd_holder_disks ;
1147 struct block_device *bd_contains ;
1148 unsigned int bd_block_size ;
1149 struct hd_struct *bd_part ;
1150 unsigned int bd_part_count ;
1151 int bd_invalidated ;
1152 struct gendisk *bd_disk ;
1153 struct request_queue *bd_queue ;
1154 struct list_head bd_list ;
1155 unsigned long bd_private ;
1156 int bd_fsfreeze_count ;
1157 struct mutex bd_fsfreeze_mutex ;
1158};
1159#line 737
1160struct posix_acl;
1161#line 737
1162struct posix_acl;
1163#line 738
1164struct inode_operations;
1165#line 738 "include/linux/fs.h"
1166union __anonunion_ldv_15837_139 {
1167 unsigned int const i_nlink ;
1168 unsigned int __i_nlink ;
1169};
1170#line 738 "include/linux/fs.h"
1171union __anonunion_ldv_15856_140 {
1172 struct list_head i_dentry ;
1173 struct rcu_head i_rcu ;
1174};
1175#line 738
1176struct file_lock;
1177#line 738
1178struct cdev;
1179#line 738 "include/linux/fs.h"
1180union __anonunion_ldv_15873_141 {
1181 struct pipe_inode_info *i_pipe ;
1182 struct block_device *i_bdev ;
1183 struct cdev *i_cdev ;
1184};
1185#line 738 "include/linux/fs.h"
1186struct inode {
1187 umode_t i_mode ;
1188 unsigned short i_opflags ;
1189 uid_t i_uid ;
1190 gid_t i_gid ;
1191 unsigned int i_flags ;
1192 struct posix_acl *i_acl ;
1193 struct posix_acl *i_default_acl ;
1194 struct inode_operations const *i_op ;
1195 struct super_block *i_sb ;
1196 struct address_space *i_mapping ;
1197 void *i_security ;
1198 unsigned long i_ino ;
1199 union __anonunion_ldv_15837_139 ldv_15837 ;
1200 dev_t i_rdev ;
1201 struct timespec i_atime ;
1202 struct timespec i_mtime ;
1203 struct timespec i_ctime ;
1204 spinlock_t i_lock ;
1205 unsigned short i_bytes ;
1206 blkcnt_t i_blocks ;
1207 loff_t i_size ;
1208 unsigned long i_state ;
1209 struct mutex i_mutex ;
1210 unsigned long dirtied_when ;
1211 struct hlist_node i_hash ;
1212 struct list_head i_wb_list ;
1213 struct list_head i_lru ;
1214 struct list_head i_sb_list ;
1215 union __anonunion_ldv_15856_140 ldv_15856 ;
1216 atomic_t i_count ;
1217 unsigned int i_blkbits ;
1218 u64 i_version ;
1219 atomic_t i_dio_count ;
1220 atomic_t i_writecount ;
1221 struct file_operations const *i_fop ;
1222 struct file_lock *i_flock ;
1223 struct address_space i_data ;
1224 struct dquot *i_dquot[2U] ;
1225 struct list_head i_devices ;
1226 union __anonunion_ldv_15873_141 ldv_15873 ;
1227 __u32 i_generation ;
1228 __u32 i_fsnotify_mask ;
1229 struct hlist_head i_fsnotify_marks ;
1230 atomic_t i_readcount ;
1231 void *i_private ;
1232};
1233#line 941 "include/linux/fs.h"
1234struct fown_struct {
1235 rwlock_t lock ;
1236 struct pid *pid ;
1237 enum pid_type pid_type ;
1238 uid_t uid ;
1239 uid_t euid ;
1240 int signum ;
1241};
1242#line 949 "include/linux/fs.h"
1243struct file_ra_state {
1244 unsigned long start ;
1245 unsigned int size ;
1246 unsigned int async_size ;
1247 unsigned int ra_pages ;
1248 unsigned int mmap_miss ;
1249 loff_t prev_pos ;
1250};
1251#line 972 "include/linux/fs.h"
1252union __anonunion_f_u_142 {
1253 struct list_head fu_list ;
1254 struct rcu_head fu_rcuhead ;
1255};
1256#line 972 "include/linux/fs.h"
1257struct file {
1258 union __anonunion_f_u_142 f_u ;
1259 struct path f_path ;
1260 struct file_operations const *f_op ;
1261 spinlock_t f_lock ;
1262 int f_sb_list_cpu ;
1263 atomic_long_t f_count ;
1264 unsigned int f_flags ;
1265 fmode_t f_mode ;
1266 loff_t f_pos ;
1267 struct fown_struct f_owner ;
1268 struct cred const *f_cred ;
1269 struct file_ra_state f_ra ;
1270 u64 f_version ;
1271 void *f_security ;
1272 void *private_data ;
1273 struct list_head f_ep_links ;
1274 struct list_head f_tfile_llink ;
1275 struct address_space *f_mapping ;
1276 unsigned long f_mnt_write_state ;
1277};
1278#line 1111
1279struct files_struct;
1280#line 1111 "include/linux/fs.h"
1281typedef struct files_struct *fl_owner_t;
1282#line 1112 "include/linux/fs.h"
1283struct file_lock_operations {
1284 void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1285 void (*fl_release_private)(struct file_lock * ) ;
1286};
1287#line 1117 "include/linux/fs.h"
1288struct lock_manager_operations {
1289 int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1290 void (*lm_notify)(struct file_lock * ) ;
1291 int (*lm_grant)(struct file_lock * , struct file_lock * , int ) ;
1292 void (*lm_release_private)(struct file_lock * ) ;
1293 void (*lm_break)(struct file_lock * ) ;
1294 int (*lm_change)(struct file_lock ** , int ) ;
1295};
1296#line 1134
1297struct nlm_lockowner;
1298#line 1134
1299struct nlm_lockowner;
1300#line 1135 "include/linux/fs.h"
1301struct nfs_lock_info {
1302 u32 state ;
1303 struct nlm_lockowner *owner ;
1304 struct list_head list ;
1305};
1306#line 14 "include/linux/nfs_fs_i.h"
1307struct nfs4_lock_state;
1308#line 14
1309struct nfs4_lock_state;
1310#line 15 "include/linux/nfs_fs_i.h"
1311struct nfs4_lock_info {
1312 struct nfs4_lock_state *owner ;
1313};
1314#line 19
1315struct fasync_struct;
1316#line 19 "include/linux/nfs_fs_i.h"
1317struct __anonstruct_afs_144 {
1318 struct list_head link ;
1319 int state ;
1320};
1321#line 19 "include/linux/nfs_fs_i.h"
1322union __anonunion_fl_u_143 {
1323 struct nfs_lock_info nfs_fl ;
1324 struct nfs4_lock_info nfs4_fl ;
1325 struct __anonstruct_afs_144 afs ;
1326};
1327#line 19 "include/linux/nfs_fs_i.h"
1328struct file_lock {
1329 struct file_lock *fl_next ;
1330 struct list_head fl_link ;
1331 struct list_head fl_block ;
1332 fl_owner_t fl_owner ;
1333 unsigned int fl_flags ;
1334 unsigned char fl_type ;
1335 unsigned int fl_pid ;
1336 struct pid *fl_nspid ;
1337 wait_queue_head_t fl_wait ;
1338 struct file *fl_file ;
1339 loff_t fl_start ;
1340 loff_t fl_end ;
1341 struct fasync_struct *fl_fasync ;
1342 unsigned long fl_break_time ;
1343 unsigned long fl_downgrade_time ;
1344 struct file_lock_operations const *fl_ops ;
1345 struct lock_manager_operations const *fl_lmops ;
1346 union __anonunion_fl_u_143 fl_u ;
1347};
1348#line 1221 "include/linux/fs.h"
1349struct fasync_struct {
1350 spinlock_t fa_lock ;
1351 int magic ;
1352 int fa_fd ;
1353 struct fasync_struct *fa_next ;
1354 struct file *fa_file ;
1355 struct rcu_head fa_rcu ;
1356};
1357#line 1417
1358struct file_system_type;
1359#line 1417
1360struct super_operations;
1361#line 1417
1362struct xattr_handler;
1363#line 1417
1364struct mtd_info;
1365#line 1417 "include/linux/fs.h"
1366struct super_block {
1367 struct list_head s_list ;
1368 dev_t s_dev ;
1369 unsigned char s_dirt ;
1370 unsigned char s_blocksize_bits ;
1371 unsigned long s_blocksize ;
1372 loff_t s_maxbytes ;
1373 struct file_system_type *s_type ;
1374 struct super_operations const *s_op ;
1375 struct dquot_operations const *dq_op ;
1376 struct quotactl_ops const *s_qcop ;
1377 struct export_operations const *s_export_op ;
1378 unsigned long s_flags ;
1379 unsigned long s_magic ;
1380 struct dentry *s_root ;
1381 struct rw_semaphore s_umount ;
1382 struct mutex s_lock ;
1383 int s_count ;
1384 atomic_t s_active ;
1385 void *s_security ;
1386 struct xattr_handler const **s_xattr ;
1387 struct list_head s_inodes ;
1388 struct hlist_bl_head s_anon ;
1389 struct list_head *s_files ;
1390 struct list_head s_mounts ;
1391 struct list_head s_dentry_lru ;
1392 int s_nr_dentry_unused ;
1393 spinlock_t s_inode_lru_lock ;
1394 struct list_head s_inode_lru ;
1395 int s_nr_inodes_unused ;
1396 struct block_device *s_bdev ;
1397 struct backing_dev_info *s_bdi ;
1398 struct mtd_info *s_mtd ;
1399 struct hlist_node s_instances ;
1400 struct quota_info s_dquot ;
1401 int s_frozen ;
1402 wait_queue_head_t s_wait_unfrozen ;
1403 char s_id[32U] ;
1404 u8 s_uuid[16U] ;
1405 void *s_fs_info ;
1406 unsigned int s_max_links ;
1407 fmode_t s_mode ;
1408 u32 s_time_gran ;
1409 struct mutex s_vfs_rename_mutex ;
1410 char *s_subtype ;
1411 char *s_options ;
1412 struct dentry_operations const *s_d_op ;
1413 int cleancache_poolid ;
1414 struct shrinker s_shrink ;
1415 atomic_long_t s_remove_count ;
1416 int s_readonly_remount ;
1417};
1418#line 1563 "include/linux/fs.h"
1419struct fiemap_extent_info {
1420 unsigned int fi_flags ;
1421 unsigned int fi_extents_mapped ;
1422 unsigned int fi_extents_max ;
1423 struct fiemap_extent *fi_extents_start ;
1424};
1425#line 1602 "include/linux/fs.h"
1426struct file_operations {
1427 struct module *owner ;
1428 loff_t (*llseek)(struct file * , loff_t , int ) ;
1429 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ;
1430 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ;
1431 ssize_t (*aio_read)(struct kiocb * , struct iovec const * , unsigned long ,
1432 loff_t ) ;
1433 ssize_t (*aio_write)(struct kiocb * , struct iovec const * , unsigned long ,
1434 loff_t ) ;
1435 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int ,
1436 loff_t , u64 , unsigned int ) ) ;
1437 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1438 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
1439 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
1440 int (*mmap)(struct file * , struct vm_area_struct * ) ;
1441 int (*open)(struct inode * , struct file * ) ;
1442 int (*flush)(struct file * , fl_owner_t ) ;
1443 int (*release)(struct inode * , struct file * ) ;
1444 int (*fsync)(struct file * , loff_t , loff_t , int ) ;
1445 int (*aio_fsync)(struct kiocb * , int ) ;
1446 int (*fasync)(int , struct file * , int ) ;
1447 int (*lock)(struct file * , int , struct file_lock * ) ;
1448 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * ,
1449 int ) ;
1450 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
1451 unsigned long , unsigned long ) ;
1452 int (*check_flags)(int ) ;
1453 int (*flock)(struct file * , int , struct file_lock * ) ;
1454 ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t ,
1455 unsigned int ) ;
1456 ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t ,
1457 unsigned int ) ;
1458 int (*setlease)(struct file * , long , struct file_lock ** ) ;
1459 long (*fallocate)(struct file * , int , loff_t , loff_t ) ;
1460};
1461#line 1637 "include/linux/fs.h"
1462struct inode_operations {
1463 struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1464 void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1465 int (*permission)(struct inode * , int ) ;
1466 struct posix_acl *(*get_acl)(struct inode * , int ) ;
1467 int (*readlink)(struct dentry * , char * , int ) ;
1468 void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
1469 int (*create)(struct inode * , struct dentry * , umode_t , struct nameidata * ) ;
1470 int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
1471 int (*unlink)(struct inode * , struct dentry * ) ;
1472 int (*symlink)(struct inode * , struct dentry * , char const * ) ;
1473 int (*mkdir)(struct inode * , struct dentry * , umode_t ) ;
1474 int (*rmdir)(struct inode * , struct dentry * ) ;
1475 int (*mknod)(struct inode * , struct dentry * , umode_t , dev_t ) ;
1476 int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
1477 void (*truncate)(struct inode * ) ;
1478 int (*setattr)(struct dentry * , struct iattr * ) ;
1479 int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
1480 int (*setxattr)(struct dentry * , char const * , void const * , size_t , int ) ;
1481 ssize_t (*getxattr)(struct dentry * , char const * , void * , size_t ) ;
1482 ssize_t (*listxattr)(struct dentry * , char * , size_t ) ;
1483 int (*removexattr)(struct dentry * , char const * ) ;
1484 void (*truncate_range)(struct inode * , loff_t , loff_t ) ;
1485 int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 , u64 ) ;
1486};
1487#line 1682 "include/linux/fs.h"
1488struct super_operations {
1489 struct inode *(*alloc_inode)(struct super_block * ) ;
1490 void (*destroy_inode)(struct inode * ) ;
1491 void (*dirty_inode)(struct inode * , int ) ;
1492 int (*write_inode)(struct inode * , struct writeback_control * ) ;
1493 int (*drop_inode)(struct inode * ) ;
1494 void (*evict_inode)(struct inode * ) ;
1495 void (*put_super)(struct super_block * ) ;
1496 void (*write_super)(struct super_block * ) ;
1497 int (*sync_fs)(struct super_block * , int ) ;
1498 int (*freeze_fs)(struct super_block * ) ;
1499 int (*unfreeze_fs)(struct super_block * ) ;
1500 int (*statfs)(struct dentry * , struct kstatfs * ) ;
1501 int (*remount_fs)(struct super_block * , int * , char * ) ;
1502 void (*umount_begin)(struct super_block * ) ;
1503 int (*show_options)(struct seq_file * , struct dentry * ) ;
1504 int (*show_devname)(struct seq_file * , struct dentry * ) ;
1505 int (*show_path)(struct seq_file * , struct dentry * ) ;
1506 int (*show_stats)(struct seq_file * , struct dentry * ) ;
1507 ssize_t (*quota_read)(struct super_block * , int , char * , size_t , loff_t ) ;
1508 ssize_t (*quota_write)(struct super_block * , int , char const * , size_t ,
1509 loff_t ) ;
1510 int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t ) ;
1511 int (*nr_cached_objects)(struct super_block * ) ;
1512 void (*free_cached_objects)(struct super_block * , int ) ;
1513};
1514#line 1834 "include/linux/fs.h"
1515struct file_system_type {
1516 char const *name ;
1517 int fs_flags ;
1518 struct dentry *(*mount)(struct file_system_type * , int , char const * , void * ) ;
1519 void (*kill_sb)(struct super_block * ) ;
1520 struct module *owner ;
1521 struct file_system_type *next ;
1522 struct hlist_head fs_supers ;
1523 struct lock_class_key s_lock_key ;
1524 struct lock_class_key s_umount_key ;
1525 struct lock_class_key s_vfs_rename_key ;
1526 struct lock_class_key i_lock_key ;
1527 struct lock_class_key i_mutex_key ;
1528 struct lock_class_key i_mutex_dir_key ;
1529};
1530#line 69 "include/linux/io.h"
1531struct exception_table_entry {
1532 unsigned long insn ;
1533 unsigned long fixup ;
1534};
1535#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1536void ldv_spin_lock(void) ;
1537#line 3
1538void ldv_spin_unlock(void) ;
1539#line 4
1540int ldv_spin_trylock(void) ;
1541#line 98 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
1542__inline static void clear_bit(int nr , unsigned long volatile *addr )
1543{ long volatile *__cil_tmp3 ;
1544
1545 {
1546#line 105
1547 __cil_tmp3 = (long volatile *)addr;
1548#line 105
1549 __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));
1550#line 107
1551 return;
1552}
1553}
1554#line 195 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
1555__inline static int test_and_set_bit(int nr , unsigned long volatile *addr )
1556{ int oldbit ;
1557 long volatile *__cil_tmp4 ;
1558
1559 {
1560#line 199
1561 __cil_tmp4 = (long volatile *)addr;
1562#line 199
1563 __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),
1564 "+m" (*__cil_tmp4): "Ir" (nr): "memory");
1565#line 202
1566 return (oldbit);
1567}
1568}
1569#line 101 "include/linux/printk.h"
1570extern int printk(char const * , ...) ;
1571#line 192 "include/linux/kernel.h"
1572extern void might_fault(void) ;
1573#line 137 "include/linux/ioport.h"
1574extern struct resource ioport_resource ;
1575#line 181
1576extern struct resource *__request_region(struct resource * , resource_size_t , resource_size_t ,
1577 char const * , int ) ;
1578#line 192
1579extern void __release_region(struct resource * , resource_size_t , resource_size_t ) ;
1580#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1581__inline static void outb(unsigned char value , int port )
1582{
1583
1584 {
1585#line 308
1586 __asm__ volatile ("outb %b0, %w1": : "a" (value), "Nd" (port));
1587#line 309
1588 return;
1589}
1590}
1591#line 26 "include/linux/export.h"
1592extern struct module __this_module ;
1593#line 453 "include/linux/module.h"
1594extern void __module_get(struct module * ) ;
1595#line 220 "include/linux/slub_def.h"
1596extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1597#line 223
1598void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1599#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1600void ldv_check_alloc_flags(gfp_t flags ) ;
1601#line 12
1602void ldv_check_alloc_nonatomic(void) ;
1603#line 14
1604struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1605#line 61 "include/linux/miscdevice.h"
1606extern int misc_register(struct miscdevice * ) ;
1607#line 62
1608extern int misc_deregister(struct miscdevice * ) ;
1609#line 47 "include/linux/delay.h"
1610extern unsigned long msleep_interruptible(unsigned int ) ;
1611#line 2402 "include/linux/fs.h"
1612extern loff_t no_llseek(struct file * , loff_t , int ) ;
1613#line 2407
1614extern int nonseekable_open(struct inode * , struct file * ) ;
1615#line 47 "include/linux/reboot.h"
1616extern int register_reboot_notifier(struct notifier_block * ) ;
1617#line 48
1618extern int unregister_reboot_notifier(struct notifier_block * ) ;
1619#line 72 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1620static unsigned long sbc8360_is_open ;
1621#line 73 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1622static char expect_close ;
1623#line 141 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1624static int wd_times[64U][2U] =
1625#line 141
1626 { { 0, 1},
1627 { 1, 1},
1628 { 2, 1},
1629 { 3, 1},
1630 { 4, 1},
1631 { 5, 1},
1632 { 6, 1},
1633 { 7, 1},
1634 { 8, 1},
1635 { 9, 1},
1636 { 10, 1},
1637 { 11, 1},
1638 { 12, 1},
1639 { 13, 1},
1640 { 14, 1},
1641 { 15, 1},
1642 { 0, 2},
1643 { 1, 2},
1644 { 2, 2},
1645 { 3, 2},
1646 { 4, 2},
1647 { 5, 2},
1648 { 6, 2},
1649 { 7, 2},
1650 { 8, 2},
1651 { 9, 2},
1652 { 10, 2},
1653 { 11, 2},
1654 { 12, 2},
1655 { 13, 2},
1656 { 14, 2},
1657 { 15, 2},
1658 { 0, 3},
1659 { 1, 3},
1660 { 2, 3},
1661 { 3, 3},
1662 { 4, 3},
1663 { 5, 3},
1664 { 6, 3},
1665 { 7, 3},
1666 { 8, 3},
1667 { 9, 3},
1668 { 10, 3},
1669 { 11, 3},
1670 { 12, 3},
1671 { 13, 3},
1672 { 14, 3},
1673 { 15, 3},
1674 { 0, 4},
1675 { 1, 4},
1676 { 2, 4},
1677 { 3, 4},
1678 { 4, 4},
1679 { 5, 4},
1680 { 6, 4},
1681 { 7, 4},
1682 { 8, 4},
1683 { 9, 4},
1684 { 10, 4},
1685 { 11, 4},
1686 { 12, 4},
1687 { 13, 4},
1688 { 14, 4},
1689 { 15, 4}};
1690#line 211 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1691static int timeout = 27;
1692#line 212 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1693static int wd_margin = 11;
1694#line 213 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1695static int wd_multiplier = 2;
1696#line 214 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1697static bool nowayout = (bool )1;
1698#line 228 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1699static void sbc8360_activate(void)
1700{ unsigned char __cil_tmp1 ;
1701 int __cil_tmp2 ;
1702 unsigned char __cil_tmp3 ;
1703
1704 {
1705 {
1706#line 231
1707 outb((unsigned char)10, 288);
1708#line 232
1709 msleep_interruptible(100U);
1710#line 233
1711 outb((unsigned char)11, 288);
1712#line 234
1713 msleep_interruptible(100U);
1714#line 236
1715 __cil_tmp1 = (unsigned char )wd_multiplier;
1716#line 236
1717 __cil_tmp2 = (int )__cil_tmp1;
1718#line 236
1719 __cil_tmp3 = (unsigned char )__cil_tmp2;
1720#line 236
1721 outb(__cil_tmp3, 288);
1722#line 237
1723 msleep_interruptible(100U);
1724 }
1725#line 238
1726 return;
1727}
1728}
1729#line 242 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1730static void sbc8360_ping(void)
1731{ unsigned char __cil_tmp1 ;
1732 int __cil_tmp2 ;
1733 unsigned char __cil_tmp3 ;
1734
1735 {
1736 {
1737#line 245
1738 __cil_tmp1 = (unsigned char )wd_margin;
1739#line 245
1740 __cil_tmp2 = (int )__cil_tmp1;
1741#line 245
1742 __cil_tmp3 = (unsigned char )__cil_tmp2;
1743#line 245
1744 outb(__cil_tmp3, 289);
1745 }
1746#line 246
1747 return;
1748}
1749}
1750#line 249 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1751static void sbc8360_stop(void)
1752{
1753
1754 {
1755 {
1756#line 252
1757 outb((unsigned char)0, 288);
1758 }
1759#line 253
1760 return;
1761}
1762}
1763#line 256 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1764static ssize_t sbc8360_write(struct file *file , char const *buf , size_t count ,
1765 loff_t *ppos )
1766{ size_t i ;
1767 char c ;
1768 int __ret_gu ;
1769 unsigned long __val_gu ;
1770 bool *__cil_tmp9 ;
1771 bool __cil_tmp10 ;
1772 signed char __cil_tmp11 ;
1773 int __cil_tmp12 ;
1774
1775 {
1776#line 259
1777 if (count != 0UL) {
1778 {
1779#line 260
1780 __cil_tmp9 = & nowayout;
1781#line 260
1782 __cil_tmp10 = *__cil_tmp9;
1783#line 260
1784 if (! __cil_tmp10) {
1785#line 264
1786 expect_close = (char)0;
1787#line 266
1788 i = 0UL;
1789#line 266
1790 goto ldv_18077;
1791 ldv_18076:
1792 {
1793#line 268
1794 might_fault();
1795 }
1796#line 268
1797 if (1 == 1) {
1798#line 268
1799 goto case_1;
1800 } else
1801#line 268
1802 if (1 == 2) {
1803#line 268
1804 goto case_2;
1805 } else
1806#line 268
1807 if (1 == 4) {
1808#line 268
1809 goto case_4;
1810 } else
1811#line 268
1812 if (1 == 8) {
1813#line 268
1814 goto case_8;
1815 } else {
1816 {
1817#line 268
1818 goto switch_default;
1819#line 268
1820 if (0) {
1821 case_1:
1822#line 268
1823 __asm__ volatile ("call __get_user_1": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + i));
1824#line 268
1825 goto ldv_18070;
1826 case_2:
1827#line 268
1828 __asm__ volatile ("call __get_user_2": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + i));
1829#line 268
1830 goto ldv_18070;
1831 case_4:
1832#line 268
1833 __asm__ volatile ("call __get_user_4": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + i));
1834#line 268
1835 goto ldv_18070;
1836 case_8:
1837#line 268
1838 __asm__ volatile ("call __get_user_8": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + i));
1839#line 268
1840 goto ldv_18070;
1841 switch_default:
1842#line 268
1843 __asm__ volatile ("call __get_user_X": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + i));
1844#line 268
1845 goto ldv_18070;
1846 } else {
1847 switch_break: ;
1848 }
1849 }
1850 }
1851 ldv_18070:
1852#line 268
1853 c = (char )__val_gu;
1854#line 268
1855 if (__ret_gu != 0) {
1856#line 269
1857 return (-14L);
1858 } else {
1859
1860 }
1861 {
1862#line 270
1863 __cil_tmp11 = (signed char )c;
1864#line 270
1865 __cil_tmp12 = (int )__cil_tmp11;
1866#line 270
1867 if (__cil_tmp12 == 86) {
1868#line 271
1869 expect_close = (char)42;
1870 } else {
1871
1872 }
1873 }
1874#line 266
1875 i = i + 1UL;
1876 ldv_18077: ;
1877#line 266
1878 if (i != count) {
1879#line 267
1880 goto ldv_18076;
1881 } else {
1882#line 269
1883 goto ldv_18078;
1884 }
1885 ldv_18078: ;
1886 } else {
1887
1888 }
1889 }
1890 {
1891#line 274
1892 sbc8360_ping();
1893 }
1894 } else {
1895
1896 }
1897#line 276
1898 return ((ssize_t )count);
1899}
1900}
1901#line 279 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1902static int sbc8360_open(struct inode *inode , struct file *file )
1903{ int tmp ;
1904 int tmp___0 ;
1905 unsigned long volatile *__cil_tmp5 ;
1906 bool *__cil_tmp6 ;
1907 bool __cil_tmp7 ;
1908
1909 {
1910 {
1911#line 281
1912 __cil_tmp5 = (unsigned long volatile *)(& sbc8360_is_open);
1913#line 281
1914 tmp = test_and_set_bit(0, __cil_tmp5);
1915 }
1916#line 281
1917 if (tmp != 0) {
1918#line 282
1919 return (-16);
1920 } else {
1921
1922 }
1923 {
1924#line 283
1925 __cil_tmp6 = & nowayout;
1926#line 283
1927 __cil_tmp7 = *__cil_tmp6;
1928#line 283
1929 if ((int )__cil_tmp7) {
1930 {
1931#line 284
1932 __module_get(& __this_module);
1933 }
1934 } else {
1935
1936 }
1937 }
1938 {
1939#line 287
1940 sbc8360_activate();
1941#line 288
1942 sbc8360_ping();
1943#line 289
1944 tmp___0 = nonseekable_open(inode, file);
1945 }
1946#line 289
1947 return (tmp___0);
1948}
1949}
1950#line 292 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1951static int sbc8360_close(struct inode *inode , struct file *file )
1952{ signed char __cil_tmp3 ;
1953 int __cil_tmp4 ;
1954 unsigned long volatile *__cil_tmp5 ;
1955
1956 {
1957 {
1958#line 294
1959 __cil_tmp3 = (signed char )expect_close;
1960#line 294
1961 __cil_tmp4 = (int )__cil_tmp3;
1962#line 294
1963 if (__cil_tmp4 == 42) {
1964 {
1965#line 295
1966 sbc8360_stop();
1967 }
1968 } else {
1969 {
1970#line 297
1971 printk("<2>sbc8360: SBC8360 device closed unexpectedly. SBC8360 will not stop!\n");
1972 }
1973 }
1974 }
1975 {
1976#line 299
1977 __cil_tmp5 = (unsigned long volatile *)(& sbc8360_is_open);
1978#line 299
1979 clear_bit(0, __cil_tmp5);
1980#line 300
1981 expect_close = (char)0;
1982 }
1983#line 301
1984 return (0);
1985}
1986}
1987#line 308 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
1988static int sbc8360_notify_sys(struct notifier_block *this , unsigned long code , void *unused )
1989{
1990
1991 {
1992#line 311
1993 if (code == 1UL) {
1994 {
1995#line 312
1996 sbc8360_stop();
1997 }
1998 } else
1999#line 311
2000 if (code == 2UL) {
2001 {
2002#line 312
2003 sbc8360_stop();
2004 }
2005 } else {
2006
2007 }
2008#line 314
2009 return (0);
2010}
2011}
2012#line 321 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2013static struct file_operations const sbc8360_fops =
2014#line 321
2015 {& __this_module, & no_llseek, (ssize_t (*)(struct file * , char * , size_t ,
2016 loff_t * ))0, & sbc8360_write, (ssize_t (*)(struct kiocb * ,
2017 struct iovec const * ,
2018 unsigned long ,
2019 loff_t ))0,
2020 (ssize_t (*)(struct kiocb * , struct iovec const * , unsigned long , loff_t ))0,
2021 (int (*)(struct file * , void * , int (*)(void * , char const * , int , loff_t ,
2022 u64 , unsigned int ) ))0, (unsigned int (*)(struct file * ,
2023 struct poll_table_struct * ))0,
2024 (long (*)(struct file * , unsigned int , unsigned long ))0, (long (*)(struct file * ,
2025 unsigned int ,
2026 unsigned long ))0,
2027 (int (*)(struct file * , struct vm_area_struct * ))0, & sbc8360_open, (int (*)(struct file * ,
2028 fl_owner_t ))0,
2029 & sbc8360_close, (int (*)(struct file * , loff_t , loff_t , int ))0, (int (*)(struct kiocb * ,
2030 int ))0,
2031 (int (*)(int , struct file * , int ))0, (int (*)(struct file * , int , struct file_lock * ))0,
2032 (ssize_t (*)(struct file * , struct page * , int , size_t , loff_t * , int ))0,
2033 (unsigned long (*)(struct file * , unsigned long , unsigned long , unsigned long ,
2034 unsigned long ))0, (int (*)(int ))0, (int (*)(struct file * ,
2035 int , struct file_lock * ))0,
2036 (ssize_t (*)(struct pipe_inode_info * , struct file * , loff_t * , size_t , unsigned int ))0,
2037 (ssize_t (*)(struct file * , loff_t * , struct pipe_inode_info * , size_t , unsigned int ))0,
2038 (int (*)(struct file * , long , struct file_lock ** ))0, (long (*)(struct file * ,
2039 int , loff_t ,
2040 loff_t ))0};
2041#line 329 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2042static struct miscdevice sbc8360_miscdev =
2043#line 329
2044 {130, "watchdog", & sbc8360_fops, {(struct list_head *)0, (struct list_head *)0},
2045 (struct device *)0, (struct device *)0, (char const *)0, (unsigned short)0};
2046#line 340 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2047static struct notifier_block sbc8360_notifier = {& sbc8360_notify_sys, (struct notifier_block *)0, 0};
2048#line 344 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2049static int sbc8360_init(void)
2050{ int res ;
2051 unsigned long mseconds ;
2052 struct resource *tmp ;
2053 struct resource *tmp___0 ;
2054 int *__cil_tmp5 ;
2055 int __cil_tmp6 ;
2056 int *__cil_tmp7 ;
2057 int __cil_tmp8 ;
2058 struct resource *__cil_tmp9 ;
2059 unsigned long __cil_tmp10 ;
2060 unsigned long __cil_tmp11 ;
2061 struct resource *__cil_tmp12 ;
2062 unsigned long __cil_tmp13 ;
2063 unsigned long __cil_tmp14 ;
2064 unsigned long __cil_tmp15 ;
2065 int *__cil_tmp16 ;
2066 int __cil_tmp17 ;
2067 unsigned long __cil_tmp18 ;
2068 unsigned long __cil_tmp19 ;
2069 unsigned long __cil_tmp20 ;
2070 unsigned long __cil_tmp21 ;
2071 int *__cil_tmp22 ;
2072 int __cil_tmp23 ;
2073 unsigned long __cil_tmp24 ;
2074 unsigned long __cil_tmp25 ;
2075 unsigned long __cil_tmp26 ;
2076 int __cil_tmp27 ;
2077 int __cil_tmp28 ;
2078 int __cil_tmp29 ;
2079 int __cil_tmp30 ;
2080 int __cil_tmp31 ;
2081 int __cil_tmp32 ;
2082 int __cil_tmp33 ;
2083 int __cil_tmp34 ;
2084
2085 {
2086#line 347
2087 mseconds = 60000UL;
2088 {
2089#line 349
2090 __cil_tmp5 = & timeout;
2091#line 349
2092 __cil_tmp6 = *__cil_tmp5;
2093#line 349
2094 if (__cil_tmp6 < 0) {
2095 {
2096#line 350
2097 printk("<3>sbc8360: Invalid timeout index (must be 0-63)\n");
2098#line 351
2099 res = -22;
2100 }
2101#line 352
2102 goto out;
2103 } else {
2104 {
2105#line 349
2106 __cil_tmp7 = & timeout;
2107#line 349
2108 __cil_tmp8 = *__cil_tmp7;
2109#line 349
2110 if (__cil_tmp8 > 63) {
2111 {
2112#line 350
2113 printk("<3>sbc8360: Invalid timeout index (must be 0-63)\n");
2114#line 351
2115 res = -22;
2116 }
2117#line 352
2118 goto out;
2119 } else {
2120
2121 }
2122 }
2123 }
2124 }
2125 {
2126#line 355
2127 tmp = __request_region(& ioport_resource, 288ULL, 1ULL, "SBC8360", 0);
2128 }
2129 {
2130#line 355
2131 __cil_tmp9 = (struct resource *)0;
2132#line 355
2133 __cil_tmp10 = (unsigned long )__cil_tmp9;
2134#line 355
2135 __cil_tmp11 = (unsigned long )tmp;
2136#line 355
2137 if (__cil_tmp11 == __cil_tmp10) {
2138 {
2139#line 356
2140 printk("<3>sbc8360: ENABLE method I/O %X is not available\n", 288);
2141#line 358
2142 res = -5;
2143 }
2144#line 359
2145 goto out;
2146 } else {
2147
2148 }
2149 }
2150 {
2151#line 361
2152 tmp___0 = __request_region(& ioport_resource, 289ULL, 1ULL, "SBC8360", 0);
2153 }
2154 {
2155#line 361
2156 __cil_tmp12 = (struct resource *)0;
2157#line 361
2158 __cil_tmp13 = (unsigned long )__cil_tmp12;
2159#line 361
2160 __cil_tmp14 = (unsigned long )tmp___0;
2161#line 361
2162 if (__cil_tmp14 == __cil_tmp13) {
2163 {
2164#line 362
2165 printk("<3>sbc8360: BASETIME method I/O %X is not available\n", 289);
2166#line 364
2167 res = -5;
2168 }
2169#line 365
2170 goto out_nobasetimereg;
2171 } else {
2172
2173 }
2174 }
2175 {
2176#line 368
2177 res = register_reboot_notifier(& sbc8360_notifier);
2178 }
2179#line 369
2180 if (res != 0) {
2181 {
2182#line 370
2183 printk("<3>sbc8360: Failed to register reboot notifier\n");
2184 }
2185#line 371
2186 goto out_noreboot;
2187 } else {
2188
2189 }
2190 {
2191#line 374
2192 res = misc_register(& sbc8360_miscdev);
2193 }
2194#line 375
2195 if (res != 0) {
2196 {
2197#line 376
2198 printk("<3>sbc8360: failed to register misc device\n");
2199 }
2200#line 377
2201 goto out_nomisc;
2202 } else {
2203
2204 }
2205#line 380
2206 __cil_tmp15 = 0 * 4UL;
2207#line 380
2208 __cil_tmp16 = & timeout;
2209#line 380
2210 __cil_tmp17 = *__cil_tmp16;
2211#line 380
2212 __cil_tmp18 = __cil_tmp17 * 8UL;
2213#line 380
2214 __cil_tmp19 = __cil_tmp18 + __cil_tmp15;
2215#line 380
2216 __cil_tmp20 = (unsigned long )(wd_times) + __cil_tmp19;
2217#line 380
2218 wd_margin = *((int *)__cil_tmp20);
2219#line 381
2220 __cil_tmp21 = 1 * 4UL;
2221#line 381
2222 __cil_tmp22 = & timeout;
2223#line 381
2224 __cil_tmp23 = *__cil_tmp22;
2225#line 381
2226 __cil_tmp24 = __cil_tmp23 * 8UL;
2227#line 381
2228 __cil_tmp25 = __cil_tmp24 + __cil_tmp21;
2229#line 381
2230 __cil_tmp26 = (unsigned long )(wd_times) + __cil_tmp25;
2231#line 381
2232 wd_multiplier = *((int *)__cil_tmp26);
2233#line 383
2234 if (wd_multiplier == 1) {
2235#line 384
2236 __cil_tmp27 = wd_margin + 1;
2237#line 384
2238 __cil_tmp28 = __cil_tmp27 * 500;
2239#line 384
2240 mseconds = (unsigned long )__cil_tmp28;
2241 } else
2242#line 385
2243 if (wd_multiplier == 2) {
2244#line 386
2245 __cil_tmp29 = wd_margin + 1;
2246#line 386
2247 __cil_tmp30 = __cil_tmp29 * 5000;
2248#line 386
2249 mseconds = (unsigned long )__cil_tmp30;
2250 } else
2251#line 387
2252 if (wd_multiplier == 3) {
2253#line 388
2254 __cil_tmp31 = wd_margin + 1;
2255#line 388
2256 __cil_tmp32 = __cil_tmp31 * 50000;
2257#line 388
2258 mseconds = (unsigned long )__cil_tmp32;
2259 } else
2260#line 389
2261 if (wd_multiplier == 4) {
2262#line 390
2263 __cil_tmp33 = wd_margin + 1;
2264#line 390
2265 __cil_tmp34 = __cil_tmp33 * 100000;
2266#line 390
2267 mseconds = (unsigned long )__cil_tmp34;
2268 } else {
2269
2270 }
2271 {
2272#line 393
2273 printk("<6>sbc8360: Timeout set at %ld ms\n", mseconds);
2274 }
2275#line 395
2276 return (0);
2277 out_nomisc:
2278 {
2279#line 398
2280 unregister_reboot_notifier(& sbc8360_notifier);
2281 }
2282 out_noreboot:
2283 {
2284#line 400
2285 __release_region(& ioport_resource, 289ULL, 1ULL);
2286 }
2287 out_nobasetimereg:
2288 {
2289#line 402
2290 __release_region(& ioport_resource, 288ULL, 1ULL);
2291 }
2292 out: ;
2293#line 404
2294 return (res);
2295}
2296}
2297#line 407 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2298static void sbc8360_exit(void)
2299{
2300
2301 {
2302 {
2303#line 409
2304 misc_deregister(& sbc8360_miscdev);
2305#line 410
2306 unregister_reboot_notifier(& sbc8360_notifier);
2307#line 411
2308 __release_region(& ioport_resource, 288ULL, 1ULL);
2309#line 412
2310 __release_region(& ioport_resource, 289ULL, 1ULL);
2311 }
2312#line 413
2313 return;
2314}
2315}
2316#line 442
2317extern void ldv_check_final_state(void) ;
2318#line 445
2319extern void ldv_check_return_value(int ) ;
2320#line 448
2321extern void ldv_initialize(void) ;
2322#line 451
2323extern int __VERIFIER_nondet_int(void) ;
2324#line 454 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2325int LDV_IN_INTERRUPT ;
2326#line 457 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2327void main(void)
2328{ struct file *var_group1 ;
2329 char const *var_sbc8360_write_3_p1 ;
2330 size_t var_sbc8360_write_3_p2 ;
2331 loff_t *var_sbc8360_write_3_p3 ;
2332 ssize_t res_sbc8360_write_3 ;
2333 struct inode *var_group2 ;
2334 int res_sbc8360_open_4 ;
2335 struct notifier_block *var_group3 ;
2336 unsigned long var_sbc8360_notify_sys_6_p1 ;
2337 void *var_sbc8360_notify_sys_6_p2 ;
2338 int ldv_s_sbc8360_fops_file_operations ;
2339 int tmp ;
2340 int tmp___0 ;
2341 int tmp___1 ;
2342 int __cil_tmp15 ;
2343
2344 {
2345 {
2346#line 538
2347 ldv_s_sbc8360_fops_file_operations = 0;
2348#line 517
2349 LDV_IN_INTERRUPT = 1;
2350#line 526
2351 ldv_initialize();
2352#line 536
2353 tmp = sbc8360_init();
2354 }
2355#line 536
2356 if (tmp != 0) {
2357#line 537
2358 goto ldv_final;
2359 } else {
2360
2361 }
2362#line 543
2363 goto ldv_18154;
2364 ldv_18153:
2365 {
2366#line 547
2367 tmp___0 = __VERIFIER_nondet_int();
2368 }
2369#line 549
2370 if (tmp___0 == 0) {
2371#line 549
2372 goto case_0;
2373 } else
2374#line 572
2375 if (tmp___0 == 1) {
2376#line 572
2377 goto case_1;
2378 } else
2379#line 595
2380 if (tmp___0 == 2) {
2381#line 595
2382 goto case_2;
2383 } else
2384#line 615
2385 if (tmp___0 == 3) {
2386#line 615
2387 goto case_3;
2388 } else {
2389 {
2390#line 635
2391 goto switch_default;
2392#line 547
2393 if (0) {
2394 case_0: ;
2395#line 552
2396 if (ldv_s_sbc8360_fops_file_operations == 0) {
2397 {
2398#line 561
2399 res_sbc8360_open_4 = sbc8360_open(var_group2, var_group1);
2400#line 562
2401 ldv_check_return_value(res_sbc8360_open_4);
2402 }
2403#line 563
2404 if (res_sbc8360_open_4 != 0) {
2405#line 564
2406 goto ldv_module_exit;
2407 } else {
2408
2409 }
2410#line 565
2411 ldv_s_sbc8360_fops_file_operations = ldv_s_sbc8360_fops_file_operations + 1;
2412 } else {
2413
2414 }
2415#line 571
2416 goto ldv_18148;
2417 case_1: ;
2418#line 575
2419 if (ldv_s_sbc8360_fops_file_operations == 1) {
2420 {
2421#line 584
2422 res_sbc8360_write_3 = sbc8360_write(var_group1, var_sbc8360_write_3_p1, var_sbc8360_write_3_p2,
2423 var_sbc8360_write_3_p3);
2424#line 585
2425 __cil_tmp15 = (int )res_sbc8360_write_3;
2426#line 585
2427 ldv_check_return_value(__cil_tmp15);
2428 }
2429#line 586
2430 if (res_sbc8360_write_3 < 0L) {
2431#line 587
2432 goto ldv_module_exit;
2433 } else {
2434
2435 }
2436#line 588
2437 ldv_s_sbc8360_fops_file_operations = ldv_s_sbc8360_fops_file_operations + 1;
2438 } else {
2439
2440 }
2441#line 594
2442 goto ldv_18148;
2443 case_2: ;
2444#line 598
2445 if (ldv_s_sbc8360_fops_file_operations == 2) {
2446 {
2447#line 607
2448 sbc8360_close(var_group2, var_group1);
2449#line 608
2450 ldv_s_sbc8360_fops_file_operations = 0;
2451 }
2452 } else {
2453
2454 }
2455#line 614
2456 goto ldv_18148;
2457 case_3:
2458 {
2459#line 627
2460 sbc8360_notify_sys(var_group3, var_sbc8360_notify_sys_6_p1, var_sbc8360_notify_sys_6_p2);
2461 }
2462#line 634
2463 goto ldv_18148;
2464 switch_default: ;
2465#line 635
2466 goto ldv_18148;
2467 } else {
2468 switch_break: ;
2469 }
2470 }
2471 }
2472 ldv_18148: ;
2473 ldv_18154:
2474 {
2475#line 543
2476 tmp___1 = __VERIFIER_nondet_int();
2477 }
2478#line 543
2479 if (tmp___1 != 0) {
2480#line 545
2481 goto ldv_18153;
2482 } else
2483#line 543
2484 if (ldv_s_sbc8360_fops_file_operations != 0) {
2485#line 545
2486 goto ldv_18153;
2487 } else {
2488#line 547
2489 goto ldv_18155;
2490 }
2491 ldv_18155: ;
2492 ldv_module_exit:
2493 {
2494#line 651
2495 sbc8360_exit();
2496 }
2497 ldv_final:
2498 {
2499#line 654
2500 ldv_check_final_state();
2501 }
2502#line 657
2503 return;
2504}
2505}
2506#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2507void ldv_blast_assert(void)
2508{
2509
2510 {
2511 ERROR: ;
2512#line 6
2513 goto ERROR;
2514}
2515}
2516#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2517extern int __VERIFIER_nondet_int(void) ;
2518#line 678 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2519int ldv_spin = 0;
2520#line 682 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2521void ldv_check_alloc_flags(gfp_t flags )
2522{
2523
2524 {
2525#line 685
2526 if (ldv_spin != 0) {
2527#line 685
2528 if (flags != 32U) {
2529 {
2530#line 685
2531 ldv_blast_assert();
2532 }
2533 } else {
2534
2535 }
2536 } else {
2537
2538 }
2539#line 688
2540 return;
2541}
2542}
2543#line 688
2544extern struct page *ldv_some_page(void) ;
2545#line 691 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2546struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
2547{ struct page *tmp ;
2548
2549 {
2550#line 694
2551 if (ldv_spin != 0) {
2552#line 694
2553 if (flags != 32U) {
2554 {
2555#line 694
2556 ldv_blast_assert();
2557 }
2558 } else {
2559
2560 }
2561 } else {
2562
2563 }
2564 {
2565#line 696
2566 tmp = ldv_some_page();
2567 }
2568#line 696
2569 return (tmp);
2570}
2571}
2572#line 700 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2573void ldv_check_alloc_nonatomic(void)
2574{
2575
2576 {
2577#line 703
2578 if (ldv_spin != 0) {
2579 {
2580#line 703
2581 ldv_blast_assert();
2582 }
2583 } else {
2584
2585 }
2586#line 706
2587 return;
2588}
2589}
2590#line 707 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2591void ldv_spin_lock(void)
2592{
2593
2594 {
2595#line 710
2596 ldv_spin = 1;
2597#line 711
2598 return;
2599}
2600}
2601#line 714 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2602void ldv_spin_unlock(void)
2603{
2604
2605 {
2606#line 717
2607 ldv_spin = 0;
2608#line 718
2609 return;
2610}
2611}
2612#line 721 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2613int ldv_spin_trylock(void)
2614{ int is_lock ;
2615
2616 {
2617 {
2618#line 726
2619 is_lock = __VERIFIER_nondet_int();
2620 }
2621#line 728
2622 if (is_lock != 0) {
2623#line 731
2624 return (0);
2625 } else {
2626#line 736
2627 ldv_spin = 1;
2628#line 738
2629 return (1);
2630 }
2631}
2632}
2633#line 905 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17357/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc8360.c.p"
2634void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
2635{
2636
2637 {
2638 {
2639#line 911
2640 ldv_check_alloc_flags(ldv_func_arg2);
2641#line 913
2642 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2643 }
2644#line 914
2645 return ((void *)0);
2646}
2647}