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