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