1
2
3
4#line 19 "include/asm-generic/int-ll64.h"
5typedef signed char __s8;
6#line 20 "include/asm-generic/int-ll64.h"
7typedef unsigned char __u8;
8#line 22 "include/asm-generic/int-ll64.h"
9typedef short __s16;
10#line 23 "include/asm-generic/int-ll64.h"
11typedef unsigned short __u16;
12#line 25 "include/asm-generic/int-ll64.h"
13typedef int __s32;
14#line 26 "include/asm-generic/int-ll64.h"
15typedef unsigned int __u32;
16#line 29 "include/asm-generic/int-ll64.h"
17typedef long long __s64;
18#line 30 "include/asm-generic/int-ll64.h"
19typedef unsigned long long __u64;
20#line 43 "include/asm-generic/int-ll64.h"
21typedef unsigned char u8;
22#line 45 "include/asm-generic/int-ll64.h"
23typedef short s16;
24#line 46 "include/asm-generic/int-ll64.h"
25typedef unsigned short u16;
26#line 48 "include/asm-generic/int-ll64.h"
27typedef int s32;
28#line 49 "include/asm-generic/int-ll64.h"
29typedef unsigned int u32;
30#line 51 "include/asm-generic/int-ll64.h"
31typedef long long s64;
32#line 52 "include/asm-generic/int-ll64.h"
33typedef unsigned long long u64;
34#line 14 "include/asm-generic/posix_types.h"
35typedef long __kernel_long_t;
36#line 15 "include/asm-generic/posix_types.h"
37typedef unsigned long __kernel_ulong_t;
38#line 31 "include/asm-generic/posix_types.h"
39typedef int __kernel_pid_t;
40#line 52 "include/asm-generic/posix_types.h"
41typedef unsigned int __kernel_uid32_t;
42#line 53 "include/asm-generic/posix_types.h"
43typedef unsigned int __kernel_gid32_t;
44#line 75 "include/asm-generic/posix_types.h"
45typedef __kernel_ulong_t __kernel_size_t;
46#line 76 "include/asm-generic/posix_types.h"
47typedef __kernel_long_t __kernel_ssize_t;
48#line 91 "include/asm-generic/posix_types.h"
49typedef long long __kernel_loff_t;
50#line 92 "include/asm-generic/posix_types.h"
51typedef __kernel_long_t __kernel_time_t;
52#line 93 "include/asm-generic/posix_types.h"
53typedef __kernel_long_t __kernel_clock_t;
54#line 94 "include/asm-generic/posix_types.h"
55typedef int __kernel_timer_t;
56#line 95 "include/asm-generic/posix_types.h"
57typedef int __kernel_clockid_t;
58#line 21 "include/linux/types.h"
59typedef __u32 __kernel_dev_t;
60#line 24 "include/linux/types.h"
61typedef __kernel_dev_t dev_t;
62#line 27 "include/linux/types.h"
63typedef unsigned short umode_t;
64#line 30 "include/linux/types.h"
65typedef __kernel_pid_t pid_t;
66#line 35 "include/linux/types.h"
67typedef __kernel_clockid_t clockid_t;
68#line 38 "include/linux/types.h"
69typedef _Bool bool;
70#line 40 "include/linux/types.h"
71typedef __kernel_uid32_t uid_t;
72#line 41 "include/linux/types.h"
73typedef __kernel_gid32_t gid_t;
74#line 54 "include/linux/types.h"
75typedef __kernel_loff_t loff_t;
76#line 63 "include/linux/types.h"
77typedef __kernel_size_t size_t;
78#line 68 "include/linux/types.h"
79typedef __kernel_ssize_t ssize_t;
80#line 78 "include/linux/types.h"
81typedef __kernel_time_t time_t;
82#line 111 "include/linux/types.h"
83typedef __s32 int32_t;
84#line 117 "include/linux/types.h"
85typedef __u32 uint32_t;
86#line 142 "include/linux/types.h"
87typedef unsigned long sector_t;
88#line 143 "include/linux/types.h"
89typedef unsigned long blkcnt_t;
90#line 202 "include/linux/types.h"
91typedef unsigned int gfp_t;
92#line 203 "include/linux/types.h"
93typedef unsigned int fmode_t;
94#line 219 "include/linux/types.h"
95struct __anonstruct_atomic_t_7 {
96 int counter ;
97};
98#line 219 "include/linux/types.h"
99typedef struct __anonstruct_atomic_t_7 atomic_t;
100#line 224 "include/linux/types.h"
101struct __anonstruct_atomic64_t_8 {
102 long counter ;
103};
104#line 224 "include/linux/types.h"
105typedef struct __anonstruct_atomic64_t_8 atomic64_t;
106#line 229 "include/linux/types.h"
107struct list_head {
108 struct list_head *next ;
109 struct list_head *prev ;
110};
111#line 233
112struct hlist_node;
113#line 233 "include/linux/types.h"
114struct hlist_head {
115 struct hlist_node *first ;
116};
117#line 237 "include/linux/types.h"
118struct hlist_node {
119 struct hlist_node *next ;
120 struct hlist_node **pprev ;
121};
122#line 253 "include/linux/types.h"
123struct rcu_head {
124 struct rcu_head *next ;
125 void (*func)(struct rcu_head *head ) ;
126};
127#line 7 "include/linux/sysinfo.h"
128struct sysinfo {
129 __kernel_long_t uptime ;
130 __kernel_ulong_t loads[3] ;
131 __kernel_ulong_t totalram ;
132 __kernel_ulong_t freeram ;
133 __kernel_ulong_t sharedram ;
134 __kernel_ulong_t bufferram ;
135 __kernel_ulong_t totalswap ;
136 __kernel_ulong_t freeswap ;
137 __u16 procs ;
138 __u16 pad ;
139 __kernel_ulong_t totalhigh ;
140 __kernel_ulong_t freehigh ;
141 __u32 mem_unit ;
142 char _f[(20UL - 2UL * sizeof(__kernel_ulong_t )) - sizeof(__u32 )] ;
143};
144#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
145struct module;
146#line 56
147struct module;
148#line 146 "include/linux/init.h"
149typedef void (*ctor_fn_t)(void);
150#line 9 "include/linux/dynamic_debug.h"
151struct _ddebug {
152 char const *modname ;
153 char const *function ;
154 char const *filename ;
155 char const *format ;
156 unsigned int lineno : 18 ;
157 unsigned int flags : 8 ;
158} __attribute__((__aligned__(8))) ;
159#line 135 "include/linux/kernel.h"
160struct completion;
161#line 135
162struct completion;
163#line 136
164struct pt_regs;
165#line 136
166struct pt_regs;
167#line 349
168struct pid;
169#line 349
170struct pid;
171#line 12 "include/linux/thread_info.h"
172struct timespec;
173#line 12
174struct timespec;
175#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
176struct page;
177#line 18
178struct page;
179#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
180struct task_struct;
181#line 20
182struct task_struct;
183#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
184struct task_struct;
185#line 8
186struct mm_struct;
187#line 8
188struct mm_struct;
189#line 99 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
190struct pt_regs {
191 unsigned long r15 ;
192 unsigned long r14 ;
193 unsigned long r13 ;
194 unsigned long r12 ;
195 unsigned long bp ;
196 unsigned long bx ;
197 unsigned long r11 ;
198 unsigned long r10 ;
199 unsigned long r9 ;
200 unsigned long r8 ;
201 unsigned long ax ;
202 unsigned long cx ;
203 unsigned long dx ;
204 unsigned long si ;
205 unsigned long di ;
206 unsigned long orig_ax ;
207 unsigned long ip ;
208 unsigned long cs ;
209 unsigned long flags ;
210 unsigned long sp ;
211 unsigned long ss ;
212};
213#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
214struct __anonstruct____missing_field_name_15 {
215 unsigned int a ;
216 unsigned int b ;
217};
218#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
219struct __anonstruct____missing_field_name_16 {
220 u16 limit0 ;
221 u16 base0 ;
222 unsigned int base1 : 8 ;
223 unsigned int type : 4 ;
224 unsigned int s : 1 ;
225 unsigned int dpl : 2 ;
226 unsigned int p : 1 ;
227 unsigned int limit : 4 ;
228 unsigned int avl : 1 ;
229 unsigned int l : 1 ;
230 unsigned int d : 1 ;
231 unsigned int g : 1 ;
232 unsigned int base2 : 8 ;
233};
234#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
235union __anonunion____missing_field_name_14 {
236 struct __anonstruct____missing_field_name_15 __annonCompField5 ;
237 struct __anonstruct____missing_field_name_16 __annonCompField6 ;
238};
239#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
240struct desc_struct {
241 union __anonunion____missing_field_name_14 __annonCompField7 ;
242} __attribute__((__packed__)) ;
243#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
244typedef unsigned long pgdval_t;
245#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
246typedef unsigned long pgprotval_t;
247#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
248struct pgprot {
249 pgprotval_t pgprot ;
250};
251#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
252typedef struct pgprot pgprot_t;
253#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
254struct __anonstruct_pgd_t_20 {
255 pgdval_t pgd ;
256};
257#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
258typedef struct __anonstruct_pgd_t_20 pgd_t;
259#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
260typedef struct page *pgtable_t;
261#line 295
262struct file;
263#line 295
264struct file;
265#line 313
266struct seq_file;
267#line 313
268struct seq_file;
269#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
270struct page;
271#line 47
272struct thread_struct;
273#line 47
274struct thread_struct;
275#line 50
276struct mm_struct;
277#line 51
278struct desc_struct;
279#line 52
280struct task_struct;
281#line 53
282struct cpumask;
283#line 53
284struct cpumask;
285#line 329
286struct arch_spinlock;
287#line 329
288struct arch_spinlock;
289#line 138 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
290struct cpuinfo_x86;
291#line 138
292struct cpuinfo_x86;
293#line 139
294struct task_struct;
295#line 141 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
296struct kernel_vm86_regs {
297 struct pt_regs pt ;
298 unsigned short es ;
299 unsigned short __esh ;
300 unsigned short ds ;
301 unsigned short __dsh ;
302 unsigned short fs ;
303 unsigned short __fsh ;
304 unsigned short gs ;
305 unsigned short __gsh ;
306};
307#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
308union __anonunion____missing_field_name_24 {
309 struct pt_regs *regs ;
310 struct kernel_vm86_regs *vm86 ;
311};
312#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
313struct math_emu_info {
314 long ___orig_eip ;
315 union __anonunion____missing_field_name_24 __annonCompField8 ;
316};
317#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
318struct task_struct;
319#line 10 "include/asm-generic/bug.h"
320struct bug_entry {
321 int bug_addr_disp ;
322 int file_disp ;
323 unsigned short line ;
324 unsigned short flags ;
325};
326#line 12 "include/linux/bug.h"
327struct pt_regs;
328#line 14 "include/linux/cpumask.h"
329struct cpumask {
330 unsigned long bits[((4096UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
331};
332#line 14 "include/linux/cpumask.h"
333typedef struct cpumask cpumask_t;
334#line 637 "include/linux/cpumask.h"
335typedef struct cpumask *cpumask_var_t;
336#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
337struct static_key;
338#line 234
339struct static_key;
340#line 11 "include/linux/personality.h"
341struct pt_regs;
342#line 70 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
343struct cpuinfo_x86 {
344 __u8 x86 ;
345 __u8 x86_vendor ;
346 __u8 x86_model ;
347 __u8 x86_mask ;
348 int x86_tlbsize ;
349 __u8 x86_virt_bits ;
350 __u8 x86_phys_bits ;
351 __u8 x86_coreid_bits ;
352 __u32 extended_cpuid_level ;
353 int cpuid_level ;
354 __u32 x86_capability[10] ;
355 char x86_vendor_id[16] ;
356 char x86_model_id[64] ;
357 int x86_cache_size ;
358 int x86_cache_alignment ;
359 int x86_power ;
360 unsigned long loops_per_jiffy ;
361 u16 x86_max_cores ;
362 u16 apicid ;
363 u16 initial_apicid ;
364 u16 x86_clflush_size ;
365 u16 booted_cores ;
366 u16 phys_proc_id ;
367 u16 cpu_core_id ;
368 u8 compute_unit_id ;
369 u16 cpu_index ;
370 u32 microcode ;
371} __attribute__((__aligned__((1) << (6) ))) ;
372#line 153
373struct seq_operations;
374#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
375struct i387_fsave_struct {
376 u32 cwd ;
377 u32 swd ;
378 u32 twd ;
379 u32 fip ;
380 u32 fcs ;
381 u32 foo ;
382 u32 fos ;
383 u32 st_space[20] ;
384 u32 status ;
385};
386#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
387struct __anonstruct____missing_field_name_31 {
388 u64 rip ;
389 u64 rdp ;
390};
391#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
392struct __anonstruct____missing_field_name_32 {
393 u32 fip ;
394 u32 fcs ;
395 u32 foo ;
396 u32 fos ;
397};
398#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
399union __anonunion____missing_field_name_30 {
400 struct __anonstruct____missing_field_name_31 __annonCompField12 ;
401 struct __anonstruct____missing_field_name_32 __annonCompField13 ;
402};
403#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
404union __anonunion____missing_field_name_33 {
405 u32 padding1[12] ;
406 u32 sw_reserved[12] ;
407};
408#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
409struct i387_fxsave_struct {
410 u16 cwd ;
411 u16 swd ;
412 u16 twd ;
413 u16 fop ;
414 union __anonunion____missing_field_name_30 __annonCompField14 ;
415 u32 mxcsr ;
416 u32 mxcsr_mask ;
417 u32 st_space[32] ;
418 u32 xmm_space[64] ;
419 u32 padding[12] ;
420 union __anonunion____missing_field_name_33 __annonCompField15 ;
421} __attribute__((__aligned__(16))) ;
422#line 341 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
423struct i387_soft_struct {
424 u32 cwd ;
425 u32 swd ;
426 u32 twd ;
427 u32 fip ;
428 u32 fcs ;
429 u32 foo ;
430 u32 fos ;
431 u32 st_space[20] ;
432 u8 ftop ;
433 u8 changed ;
434 u8 lookahead ;
435 u8 no_update ;
436 u8 rm ;
437 u8 alimit ;
438 struct math_emu_info *info ;
439 u32 entry_eip ;
440};
441#line 361 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
442struct ymmh_struct {
443 u32 ymmh_space[64] ;
444};
445#line 366 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
446struct xsave_hdr_struct {
447 u64 xstate_bv ;
448 u64 reserved1[2] ;
449 u64 reserved2[5] ;
450} __attribute__((__packed__)) ;
451#line 372 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
452struct xsave_struct {
453 struct i387_fxsave_struct i387 ;
454 struct xsave_hdr_struct xsave_hdr ;
455 struct ymmh_struct ymmh ;
456} __attribute__((__packed__, __aligned__(64))) ;
457#line 379 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
458union thread_xstate {
459 struct i387_fsave_struct fsave ;
460 struct i387_fxsave_struct fxsave ;
461 struct i387_soft_struct soft ;
462 struct xsave_struct xsave ;
463};
464#line 386 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
465struct fpu {
466 unsigned int last_cpu ;
467 unsigned int has_fpu ;
468 union thread_xstate *state ;
469};
470#line 433
471struct kmem_cache;
472#line 435
473struct perf_event;
474#line 435
475struct perf_event;
476#line 437 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
477struct thread_struct {
478 struct desc_struct tls_array[3] ;
479 unsigned long sp0 ;
480 unsigned long sp ;
481 unsigned long usersp ;
482 unsigned short es ;
483 unsigned short ds ;
484 unsigned short fsindex ;
485 unsigned short gsindex ;
486 unsigned long fs ;
487 unsigned long gs ;
488 struct perf_event *ptrace_bps[4] ;
489 unsigned long debugreg6 ;
490 unsigned long ptrace_dr7 ;
491 unsigned long cr2 ;
492 unsigned long trap_nr ;
493 unsigned long error_code ;
494 struct fpu fpu ;
495 unsigned long *io_bitmap_ptr ;
496 unsigned long iopl ;
497 unsigned int io_bitmap_max ;
498};
499#line 23 "include/asm-generic/atomic-long.h"
500typedef atomic64_t atomic_long_t;
501#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
502typedef u16 __ticket_t;
503#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
504typedef u32 __ticketpair_t;
505#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
506struct __raw_tickets {
507 __ticket_t head ;
508 __ticket_t tail ;
509};
510#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
511union __anonunion____missing_field_name_36 {
512 __ticketpair_t head_tail ;
513 struct __raw_tickets tickets ;
514};
515#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
516struct arch_spinlock {
517 union __anonunion____missing_field_name_36 __annonCompField17 ;
518};
519#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
520typedef struct arch_spinlock arch_spinlock_t;
521#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
522struct __anonstruct____missing_field_name_38 {
523 u32 read ;
524 s32 write ;
525};
526#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
527union __anonunion_arch_rwlock_t_37 {
528 s64 lock ;
529 struct __anonstruct____missing_field_name_38 __annonCompField18 ;
530};
531#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
532typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_t;
533#line 12 "include/linux/lockdep.h"
534struct task_struct;
535#line 391 "include/linux/lockdep.h"
536struct lock_class_key {
537
538};
539#line 20 "include/linux/spinlock_types.h"
540struct raw_spinlock {
541 arch_spinlock_t raw_lock ;
542 unsigned int magic ;
543 unsigned int owner_cpu ;
544 void *owner ;
545};
546#line 20 "include/linux/spinlock_types.h"
547typedef struct raw_spinlock raw_spinlock_t;
548#line 64 "include/linux/spinlock_types.h"
549union __anonunion____missing_field_name_39 {
550 struct raw_spinlock rlock ;
551};
552#line 64 "include/linux/spinlock_types.h"
553struct spinlock {
554 union __anonunion____missing_field_name_39 __annonCompField19 ;
555};
556#line 64 "include/linux/spinlock_types.h"
557typedef struct spinlock spinlock_t;
558#line 11 "include/linux/rwlock_types.h"
559struct __anonstruct_rwlock_t_40 {
560 arch_rwlock_t raw_lock ;
561 unsigned int magic ;
562 unsigned int owner_cpu ;
563 void *owner ;
564};
565#line 11 "include/linux/rwlock_types.h"
566typedef struct __anonstruct_rwlock_t_40 rwlock_t;
567#line 49 "include/linux/wait.h"
568struct __wait_queue_head {
569 spinlock_t lock ;
570 struct list_head task_list ;
571};
572#line 53 "include/linux/wait.h"
573typedef struct __wait_queue_head wait_queue_head_t;
574#line 55
575struct task_struct;
576#line 119 "include/linux/seqlock.h"
577struct seqcount {
578 unsigned int sequence ;
579};
580#line 119 "include/linux/seqlock.h"
581typedef struct seqcount seqcount_t;
582#line 98 "include/linux/nodemask.h"
583struct __anonstruct_nodemask_t_42 {
584 unsigned long bits[(((unsigned long )(1 << 10) + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
585};
586#line 98 "include/linux/nodemask.h"
587typedef struct __anonstruct_nodemask_t_42 nodemask_t;
588#line 60 "include/linux/pageblock-flags.h"
589struct page;
590#line 48 "include/linux/mutex.h"
591struct mutex {
592 atomic_t count ;
593 spinlock_t wait_lock ;
594 struct list_head wait_list ;
595 struct task_struct *owner ;
596 char const *name ;
597 void *magic ;
598};
599#line 69 "include/linux/mutex.h"
600struct mutex_waiter {
601 struct list_head list ;
602 struct task_struct *task ;
603 void *magic ;
604};
605#line 19 "include/linux/rwsem.h"
606struct rw_semaphore;
607#line 19
608struct rw_semaphore;
609#line 25 "include/linux/rwsem.h"
610struct rw_semaphore {
611 long count ;
612 raw_spinlock_t wait_lock ;
613 struct list_head wait_list ;
614};
615#line 25 "include/linux/completion.h"
616struct completion {
617 unsigned int done ;
618 wait_queue_head_t wait ;
619};
620#line 9 "include/linux/memory_hotplug.h"
621struct page;
622#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/x86_init.h"
623struct cpuinfo_x86;
624#line 14 "include/linux/time.h"
625struct timespec {
626 __kernel_time_t tv_sec ;
627 long tv_nsec ;
628};
629#line 46 "include/linux/ktime.h"
630union ktime {
631 s64 tv64 ;
632};
633#line 59 "include/linux/ktime.h"
634typedef union ktime ktime_t;
635#line 10 "include/linux/timer.h"
636struct tvec_base;
637#line 10
638struct tvec_base;
639#line 12 "include/linux/timer.h"
640struct timer_list {
641 struct list_head entry ;
642 unsigned long expires ;
643 struct tvec_base *base ;
644 void (*function)(unsigned long ) ;
645 unsigned long data ;
646 int slack ;
647 int start_pid ;
648 void *start_site ;
649 char start_comm[16] ;
650};
651#line 289
652struct hrtimer;
653#line 289
654struct hrtimer;
655#line 290
656enum hrtimer_restart;
657#line 15 "include/linux/workqueue.h"
658struct workqueue_struct;
659#line 15
660struct workqueue_struct;
661#line 17
662struct work_struct;
663#line 17
664struct work_struct;
665#line 79 "include/linux/workqueue.h"
666struct work_struct {
667 atomic_long_t data ;
668 struct list_head entry ;
669 void (*func)(struct work_struct *work ) ;
670};
671#line 92 "include/linux/workqueue.h"
672struct delayed_work {
673 struct work_struct work ;
674 struct timer_list timer ;
675};
676#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
677struct __anonstruct_mm_context_t_112 {
678 void *ldt ;
679 int size ;
680 unsigned short ia32_compat ;
681 struct mutex lock ;
682 void *vdso ;
683};
684#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
685typedef struct __anonstruct_mm_context_t_112 mm_context_t;
686#line 8 "include/linux/vmalloc.h"
687struct vm_area_struct;
688#line 8
689struct vm_area_struct;
690#line 994 "include/linux/mmzone.h"
691struct page;
692#line 10 "include/linux/gfp.h"
693struct vm_area_struct;
694#line 100 "include/linux/rbtree.h"
695struct rb_node {
696 unsigned long rb_parent_color ;
697 struct rb_node *rb_right ;
698 struct rb_node *rb_left ;
699} __attribute__((__aligned__(sizeof(long )))) ;
700#line 110 "include/linux/rbtree.h"
701struct rb_root {
702 struct rb_node *rb_node ;
703};
704#line 14 "include/linux/prio_tree.h"
705struct prio_tree_node;
706#line 14 "include/linux/prio_tree.h"
707struct raw_prio_tree_node {
708 struct prio_tree_node *left ;
709 struct prio_tree_node *right ;
710 struct prio_tree_node *parent ;
711};
712#line 20 "include/linux/prio_tree.h"
713struct prio_tree_node {
714 struct prio_tree_node *left ;
715 struct prio_tree_node *right ;
716 struct prio_tree_node *parent ;
717 unsigned long start ;
718 unsigned long last ;
719};
720#line 28 "include/linux/prio_tree.h"
721struct prio_tree_root {
722 struct prio_tree_node *prio_tree_node ;
723 unsigned short index_bits ;
724 unsigned short raw ;
725};
726#line 8 "include/linux/debug_locks.h"
727struct task_struct;
728#line 48
729struct task_struct;
730#line 23 "include/linux/mm_types.h"
731struct address_space;
732#line 23
733struct address_space;
734#line 40 "include/linux/mm_types.h"
735union __anonunion____missing_field_name_140 {
736 unsigned long index ;
737 void *freelist ;
738};
739#line 40 "include/linux/mm_types.h"
740struct __anonstruct____missing_field_name_144 {
741 unsigned int inuse : 16 ;
742 unsigned int objects : 15 ;
743 unsigned int frozen : 1 ;
744};
745#line 40 "include/linux/mm_types.h"
746union __anonunion____missing_field_name_143 {
747 atomic_t _mapcount ;
748 struct __anonstruct____missing_field_name_144 __annonCompField31 ;
749};
750#line 40 "include/linux/mm_types.h"
751struct __anonstruct____missing_field_name_142 {
752 union __anonunion____missing_field_name_143 __annonCompField32 ;
753 atomic_t _count ;
754};
755#line 40 "include/linux/mm_types.h"
756union __anonunion____missing_field_name_141 {
757 unsigned long counters ;
758 struct __anonstruct____missing_field_name_142 __annonCompField33 ;
759};
760#line 40 "include/linux/mm_types.h"
761struct __anonstruct____missing_field_name_139 {
762 union __anonunion____missing_field_name_140 __annonCompField30 ;
763 union __anonunion____missing_field_name_141 __annonCompField34 ;
764};
765#line 40 "include/linux/mm_types.h"
766struct __anonstruct____missing_field_name_146 {
767 struct page *next ;
768 int pages ;
769 int pobjects ;
770};
771#line 40 "include/linux/mm_types.h"
772union __anonunion____missing_field_name_145 {
773 struct list_head lru ;
774 struct __anonstruct____missing_field_name_146 __annonCompField36 ;
775};
776#line 40 "include/linux/mm_types.h"
777union __anonunion____missing_field_name_147 {
778 unsigned long private ;
779 struct kmem_cache *slab ;
780 struct page *first_page ;
781};
782#line 40 "include/linux/mm_types.h"
783struct page {
784 unsigned long flags ;
785 struct address_space *mapping ;
786 struct __anonstruct____missing_field_name_139 __annonCompField35 ;
787 union __anonunion____missing_field_name_145 __annonCompField37 ;
788 union __anonunion____missing_field_name_147 __annonCompField38 ;
789 unsigned long debug_flags ;
790} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ;
791#line 200 "include/linux/mm_types.h"
792struct __anonstruct_vm_set_149 {
793 struct list_head list ;
794 void *parent ;
795 struct vm_area_struct *head ;
796};
797#line 200 "include/linux/mm_types.h"
798union __anonunion_shared_148 {
799 struct __anonstruct_vm_set_149 vm_set ;
800 struct raw_prio_tree_node prio_tree_node ;
801};
802#line 200
803struct anon_vma;
804#line 200
805struct vm_operations_struct;
806#line 200
807struct mempolicy;
808#line 200 "include/linux/mm_types.h"
809struct vm_area_struct {
810 struct mm_struct *vm_mm ;
811 unsigned long vm_start ;
812 unsigned long vm_end ;
813 struct vm_area_struct *vm_next ;
814 struct vm_area_struct *vm_prev ;
815 pgprot_t vm_page_prot ;
816 unsigned long vm_flags ;
817 struct rb_node vm_rb ;
818 union __anonunion_shared_148 shared ;
819 struct list_head anon_vma_chain ;
820 struct anon_vma *anon_vma ;
821 struct vm_operations_struct const *vm_ops ;
822 unsigned long vm_pgoff ;
823 struct file *vm_file ;
824 void *vm_private_data ;
825 struct mempolicy *vm_policy ;
826};
827#line 257 "include/linux/mm_types.h"
828struct core_thread {
829 struct task_struct *task ;
830 struct core_thread *next ;
831};
832#line 262 "include/linux/mm_types.h"
833struct core_state {
834 atomic_t nr_threads ;
835 struct core_thread dumper ;
836 struct completion startup ;
837};
838#line 284 "include/linux/mm_types.h"
839struct mm_rss_stat {
840 atomic_long_t count[3] ;
841};
842#line 288
843struct linux_binfmt;
844#line 288
845struct mmu_notifier_mm;
846#line 288 "include/linux/mm_types.h"
847struct mm_struct {
848 struct vm_area_struct *mmap ;
849 struct rb_root mm_rb ;
850 struct vm_area_struct *mmap_cache ;
851 unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
852 unsigned long pgoff , unsigned long flags ) ;
853 void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
854 unsigned long mmap_base ;
855 unsigned long task_size ;
856 unsigned long cached_hole_size ;
857 unsigned long free_area_cache ;
858 pgd_t *pgd ;
859 atomic_t mm_users ;
860 atomic_t mm_count ;
861 int map_count ;
862 spinlock_t page_table_lock ;
863 struct rw_semaphore mmap_sem ;
864 struct list_head mmlist ;
865 unsigned long hiwater_rss ;
866 unsigned long hiwater_vm ;
867 unsigned long total_vm ;
868 unsigned long locked_vm ;
869 unsigned long pinned_vm ;
870 unsigned long shared_vm ;
871 unsigned long exec_vm ;
872 unsigned long stack_vm ;
873 unsigned long reserved_vm ;
874 unsigned long def_flags ;
875 unsigned long nr_ptes ;
876 unsigned long start_code ;
877 unsigned long end_code ;
878 unsigned long start_data ;
879 unsigned long end_data ;
880 unsigned long start_brk ;
881 unsigned long brk ;
882 unsigned long start_stack ;
883 unsigned long arg_start ;
884 unsigned long arg_end ;
885 unsigned long env_start ;
886 unsigned long env_end ;
887 unsigned long saved_auxv[44] ;
888 struct mm_rss_stat rss_stat ;
889 struct linux_binfmt *binfmt ;
890 cpumask_var_t cpu_vm_mask_var ;
891 mm_context_t context ;
892 unsigned int faultstamp ;
893 unsigned int token_priority ;
894 unsigned int last_interval ;
895 unsigned long flags ;
896 struct core_state *core_state ;
897 spinlock_t ioctx_lock ;
898 struct hlist_head ioctx_list ;
899 struct task_struct *owner ;
900 struct file *exe_file ;
901 unsigned long num_exe_file_vmas ;
902 struct mmu_notifier_mm *mmu_notifier_mm ;
903 pgtable_t pmd_huge_pte ;
904 struct cpumask cpumask_allocation ;
905};
906#line 8 "include/linux/shrinker.h"
907struct shrink_control {
908 gfp_t gfp_mask ;
909 unsigned long nr_to_scan ;
910};
911#line 31 "include/linux/shrinker.h"
912struct shrinker {
913 int (*shrink)(struct shrinker * , struct shrink_control *sc ) ;
914 int seeks ;
915 long batch ;
916 struct list_head list ;
917 atomic_long_t nr_in_batch ;
918};
919#line 22 "include/linux/mm.h"
920struct mempolicy;
921#line 23
922struct anon_vma;
923#line 24
924struct file_ra_state;
925#line 24
926struct file_ra_state;
927#line 25
928struct user_struct;
929#line 25
930struct user_struct;
931#line 26
932struct writeback_control;
933#line 26
934struct writeback_control;
935#line 41 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64.h"
936struct mm_struct;
937#line 656 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable.h"
938struct vm_area_struct;
939#line 188 "include/linux/mm.h"
940struct vm_fault {
941 unsigned int flags ;
942 unsigned long pgoff ;
943 void *virtual_address ;
944 struct page *page ;
945};
946#line 205 "include/linux/mm.h"
947struct vm_operations_struct {
948 void (*open)(struct vm_area_struct *area ) ;
949 void (*close)(struct vm_area_struct *area ) ;
950 int (*fault)(struct vm_area_struct *vma , struct vm_fault *vmf ) ;
951 int (*page_mkwrite)(struct vm_area_struct *vma , struct vm_fault *vmf ) ;
952 int (*access)(struct vm_area_struct *vma , unsigned long addr , void *buf , int len ,
953 int write ) ;
954 int (*set_policy)(struct vm_area_struct *vma , struct mempolicy *new ) ;
955 struct mempolicy *(*get_policy)(struct vm_area_struct *vma , unsigned long addr ) ;
956 int (*migrate)(struct vm_area_struct *vma , nodemask_t const *from , nodemask_t const *to ,
957 unsigned long flags ) ;
958};
959#line 247
960struct inode;
961#line 247
962struct inode;
963#line 195 "include/linux/page-flags.h"
964struct page;
965#line 18 "include/linux/capability.h"
966struct task_struct;
967#line 94 "include/linux/capability.h"
968struct kernel_cap_struct {
969 __u32 cap[2] ;
970};
971#line 94 "include/linux/capability.h"
972typedef struct kernel_cap_struct kernel_cap_t;
973#line 377
974struct dentry;
975#line 377
976struct dentry;
977#line 378
978struct user_namespace;
979#line 378
980struct user_namespace;
981#line 7 "include/asm-generic/cputime.h"
982typedef unsigned long cputime_t;
983#line 84 "include/linux/sem.h"
984struct task_struct;
985#line 101
986struct sem_undo_list;
987#line 101 "include/linux/sem.h"
988struct sysv_sem {
989 struct sem_undo_list *undo_list ;
990};
991#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
992struct siginfo;
993#line 10
994struct siginfo;
995#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
996struct __anonstruct_sigset_t_152 {
997 unsigned long sig[1] ;
998};
999#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1000typedef struct __anonstruct_sigset_t_152 sigset_t;
1001#line 17 "include/asm-generic/signal-defs.h"
1002typedef void __signalfn_t(int );
1003#line 18 "include/asm-generic/signal-defs.h"
1004typedef __signalfn_t *__sighandler_t;
1005#line 20 "include/asm-generic/signal-defs.h"
1006typedef void __restorefn_t(void);
1007#line 21 "include/asm-generic/signal-defs.h"
1008typedef __restorefn_t *__sigrestore_t;
1009#line 167 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1010struct sigaction {
1011 __sighandler_t sa_handler ;
1012 unsigned long sa_flags ;
1013 __sigrestore_t sa_restorer ;
1014 sigset_t sa_mask ;
1015};
1016#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1017struct k_sigaction {
1018 struct sigaction sa ;
1019};
1020#line 7 "include/asm-generic/siginfo.h"
1021union sigval {
1022 int sival_int ;
1023 void *sival_ptr ;
1024};
1025#line 7 "include/asm-generic/siginfo.h"
1026typedef union sigval sigval_t;
1027#line 48 "include/asm-generic/siginfo.h"
1028struct __anonstruct__kill_154 {
1029 __kernel_pid_t _pid ;
1030 __kernel_uid32_t _uid ;
1031};
1032#line 48 "include/asm-generic/siginfo.h"
1033struct __anonstruct__timer_155 {
1034 __kernel_timer_t _tid ;
1035 int _overrun ;
1036 char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ;
1037 sigval_t _sigval ;
1038 int _sys_private ;
1039};
1040#line 48 "include/asm-generic/siginfo.h"
1041struct __anonstruct__rt_156 {
1042 __kernel_pid_t _pid ;
1043 __kernel_uid32_t _uid ;
1044 sigval_t _sigval ;
1045};
1046#line 48 "include/asm-generic/siginfo.h"
1047struct __anonstruct__sigchld_157 {
1048 __kernel_pid_t _pid ;
1049 __kernel_uid32_t _uid ;
1050 int _status ;
1051 __kernel_clock_t _utime ;
1052 __kernel_clock_t _stime ;
1053};
1054#line 48 "include/asm-generic/siginfo.h"
1055struct __anonstruct__sigfault_158 {
1056 void *_addr ;
1057 short _addr_lsb ;
1058};
1059#line 48 "include/asm-generic/siginfo.h"
1060struct __anonstruct__sigpoll_159 {
1061 long _band ;
1062 int _fd ;
1063};
1064#line 48 "include/asm-generic/siginfo.h"
1065union __anonunion__sifields_153 {
1066 int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ;
1067 struct __anonstruct__kill_154 _kill ;
1068 struct __anonstruct__timer_155 _timer ;
1069 struct __anonstruct__rt_156 _rt ;
1070 struct __anonstruct__sigchld_157 _sigchld ;
1071 struct __anonstruct__sigfault_158 _sigfault ;
1072 struct __anonstruct__sigpoll_159 _sigpoll ;
1073};
1074#line 48 "include/asm-generic/siginfo.h"
1075struct siginfo {
1076 int si_signo ;
1077 int si_errno ;
1078 int si_code ;
1079 union __anonunion__sifields_153 _sifields ;
1080};
1081#line 48 "include/asm-generic/siginfo.h"
1082typedef struct siginfo siginfo_t;
1083#line 288
1084struct siginfo;
1085#line 10 "include/linux/signal.h"
1086struct task_struct;
1087#line 28 "include/linux/signal.h"
1088struct sigpending {
1089 struct list_head list ;
1090 sigset_t signal ;
1091};
1092#line 239
1093struct timespec;
1094#line 240
1095struct pt_regs;
1096#line 6 "include/linux/pid.h"
1097enum pid_type {
1098 PIDTYPE_PID = 0,
1099 PIDTYPE_PGID = 1,
1100 PIDTYPE_SID = 2,
1101 PIDTYPE_MAX = 3
1102} ;
1103#line 50
1104struct pid_namespace;
1105#line 50 "include/linux/pid.h"
1106struct upid {
1107 int nr ;
1108 struct pid_namespace *ns ;
1109 struct hlist_node pid_chain ;
1110};
1111#line 57 "include/linux/pid.h"
1112struct pid {
1113 atomic_t count ;
1114 unsigned int level ;
1115 struct hlist_head tasks[3] ;
1116 struct rcu_head rcu ;
1117 struct upid numbers[1] ;
1118};
1119#line 69 "include/linux/pid.h"
1120struct pid_link {
1121 struct hlist_node node ;
1122 struct pid *pid ;
1123};
1124#line 100
1125struct pid_namespace;
1126#line 10 "include/linux/seccomp.h"
1127struct __anonstruct_seccomp_t_162 {
1128 int mode ;
1129};
1130#line 10 "include/linux/seccomp.h"
1131typedef struct __anonstruct_seccomp_t_162 seccomp_t;
1132#line 81 "include/linux/plist.h"
1133struct plist_head {
1134 struct list_head node_list ;
1135};
1136#line 85 "include/linux/plist.h"
1137struct plist_node {
1138 int prio ;
1139 struct list_head prio_list ;
1140 struct list_head node_list ;
1141};
1142#line 40 "include/linux/rtmutex.h"
1143struct rt_mutex_waiter;
1144#line 40
1145struct rt_mutex_waiter;
1146#line 42 "include/linux/resource.h"
1147struct rlimit {
1148 unsigned long rlim_cur ;
1149 unsigned long rlim_max ;
1150};
1151#line 81
1152struct task_struct;
1153#line 8 "include/linux/timerqueue.h"
1154struct timerqueue_node {
1155 struct rb_node node ;
1156 ktime_t expires ;
1157};
1158#line 13 "include/linux/timerqueue.h"
1159struct timerqueue_head {
1160 struct rb_root head ;
1161 struct timerqueue_node *next ;
1162};
1163#line 27 "include/linux/hrtimer.h"
1164struct hrtimer_clock_base;
1165#line 27
1166struct hrtimer_clock_base;
1167#line 28
1168struct hrtimer_cpu_base;
1169#line 28
1170struct hrtimer_cpu_base;
1171#line 44
1172enum hrtimer_restart {
1173 HRTIMER_NORESTART = 0,
1174 HRTIMER_RESTART = 1
1175} ;
1176#line 108 "include/linux/hrtimer.h"
1177struct hrtimer {
1178 struct timerqueue_node node ;
1179 ktime_t _softexpires ;
1180 enum hrtimer_restart (*function)(struct hrtimer * ) ;
1181 struct hrtimer_clock_base *base ;
1182 unsigned long state ;
1183 int start_pid ;
1184 void *start_site ;
1185 char start_comm[16] ;
1186};
1187#line 145 "include/linux/hrtimer.h"
1188struct hrtimer_clock_base {
1189 struct hrtimer_cpu_base *cpu_base ;
1190 int index ;
1191 clockid_t clockid ;
1192 struct timerqueue_head active ;
1193 ktime_t resolution ;
1194 ktime_t (*get_time)(void) ;
1195 ktime_t softirq_time ;
1196 ktime_t offset ;
1197};
1198#line 178 "include/linux/hrtimer.h"
1199struct hrtimer_cpu_base {
1200 raw_spinlock_t lock ;
1201 unsigned long active_bases ;
1202 ktime_t expires_next ;
1203 int hres_active ;
1204 int hang_detected ;
1205 unsigned long nr_events ;
1206 unsigned long nr_retries ;
1207 unsigned long nr_hangs ;
1208 ktime_t max_hang_time ;
1209 struct hrtimer_clock_base clock_base[3] ;
1210};
1211#line 11 "include/linux/task_io_accounting.h"
1212struct task_io_accounting {
1213 u64 rchar ;
1214 u64 wchar ;
1215 u64 syscr ;
1216 u64 syscw ;
1217 u64 read_bytes ;
1218 u64 write_bytes ;
1219 u64 cancelled_write_bytes ;
1220};
1221#line 13 "include/linux/latencytop.h"
1222struct task_struct;
1223#line 20 "include/linux/latencytop.h"
1224struct latency_record {
1225 unsigned long backtrace[12] ;
1226 unsigned int count ;
1227 unsigned long time ;
1228 unsigned long max ;
1229};
1230#line 29 "include/linux/sysctl.h"
1231struct completion;
1232#line 939
1233struct nsproxy;
1234#line 939
1235struct nsproxy;
1236#line 29 "include/linux/key.h"
1237typedef int32_t key_serial_t;
1238#line 32 "include/linux/key.h"
1239typedef uint32_t key_perm_t;
1240#line 34
1241struct key;
1242#line 34
1243struct key;
1244#line 74
1245struct seq_file;
1246#line 75
1247struct user_struct;
1248#line 76
1249struct signal_struct;
1250#line 76
1251struct signal_struct;
1252#line 77
1253struct cred;
1254#line 77
1255struct cred;
1256#line 79
1257struct key_type;
1258#line 79
1259struct key_type;
1260#line 81
1261struct keyring_list;
1262#line 81
1263struct keyring_list;
1264#line 124
1265struct key_user;
1266#line 124 "include/linux/key.h"
1267union __anonunion____missing_field_name_219 {
1268 time_t expiry ;
1269 time_t revoked_at ;
1270};
1271#line 124 "include/linux/key.h"
1272union __anonunion_type_data_220 {
1273 struct list_head link ;
1274 unsigned long x[2] ;
1275 void *p[2] ;
1276 int reject_error ;
1277};
1278#line 124 "include/linux/key.h"
1279union __anonunion_payload_221 {
1280 unsigned long value ;
1281 void *rcudata ;
1282 void *data ;
1283 struct keyring_list *subscriptions ;
1284};
1285#line 124 "include/linux/key.h"
1286struct key {
1287 atomic_t usage ;
1288 key_serial_t serial ;
1289 struct rb_node serial_node ;
1290 struct key_type *type ;
1291 struct rw_semaphore sem ;
1292 struct key_user *user ;
1293 void *security ;
1294 union __anonunion____missing_field_name_219 __annonCompField41 ;
1295 uid_t uid ;
1296 gid_t gid ;
1297 key_perm_t perm ;
1298 unsigned short quotalen ;
1299 unsigned short datalen ;
1300 unsigned long flags ;
1301 char *description ;
1302 union __anonunion_type_data_220 type_data ;
1303 union __anonunion_payload_221 payload ;
1304};
1305#line 18 "include/linux/selinux.h"
1306struct audit_context;
1307#line 18
1308struct audit_context;
1309#line 21 "include/linux/cred.h"
1310struct user_struct;
1311#line 22
1312struct cred;
1313#line 23
1314struct inode;
1315#line 31 "include/linux/cred.h"
1316struct group_info {
1317 atomic_t usage ;
1318 int ngroups ;
1319 int nblocks ;
1320 gid_t small_block[32] ;
1321 gid_t *blocks[0] ;
1322};
1323#line 83 "include/linux/cred.h"
1324struct thread_group_cred {
1325 atomic_t usage ;
1326 pid_t tgid ;
1327 spinlock_t lock ;
1328 struct key *session_keyring ;
1329 struct key *process_keyring ;
1330 struct rcu_head rcu ;
1331};
1332#line 116 "include/linux/cred.h"
1333struct cred {
1334 atomic_t usage ;
1335 atomic_t subscribers ;
1336 void *put_addr ;
1337 unsigned int magic ;
1338 uid_t uid ;
1339 gid_t gid ;
1340 uid_t suid ;
1341 gid_t sgid ;
1342 uid_t euid ;
1343 gid_t egid ;
1344 uid_t fsuid ;
1345 gid_t fsgid ;
1346 unsigned int securebits ;
1347 kernel_cap_t cap_inheritable ;
1348 kernel_cap_t cap_permitted ;
1349 kernel_cap_t cap_effective ;
1350 kernel_cap_t cap_bset ;
1351 unsigned char jit_keyring ;
1352 struct key *thread_keyring ;
1353 struct key *request_key_auth ;
1354 struct thread_group_cred *tgcred ;
1355 void *security ;
1356 struct user_struct *user ;
1357 struct user_namespace *user_ns ;
1358 struct group_info *group_info ;
1359 struct rcu_head rcu ;
1360};
1361#line 61 "include/linux/llist.h"
1362struct llist_node;
1363#line 65 "include/linux/llist.h"
1364struct llist_node {
1365 struct llist_node *next ;
1366};
1367#line 97 "include/linux/sched.h"
1368struct futex_pi_state;
1369#line 97
1370struct futex_pi_state;
1371#line 98
1372struct robust_list_head;
1373#line 98
1374struct robust_list_head;
1375#line 99
1376struct bio_list;
1377#line 99
1378struct bio_list;
1379#line 100
1380struct fs_struct;
1381#line 100
1382struct fs_struct;
1383#line 101
1384struct perf_event_context;
1385#line 101
1386struct perf_event_context;
1387#line 102
1388struct blk_plug;
1389#line 102
1390struct blk_plug;
1391#line 150
1392struct seq_file;
1393#line 151
1394struct cfs_rq;
1395#line 151
1396struct cfs_rq;
1397#line 259
1398struct task_struct;
1399#line 366
1400struct nsproxy;
1401#line 367
1402struct user_namespace;
1403#line 58 "include/linux/aio_abi.h"
1404struct io_event {
1405 __u64 data ;
1406 __u64 obj ;
1407 __s64 res ;
1408 __s64 res2 ;
1409};
1410#line 16 "include/linux/uio.h"
1411struct iovec {
1412 void *iov_base ;
1413 __kernel_size_t iov_len ;
1414};
1415#line 15 "include/linux/aio.h"
1416struct kioctx;
1417#line 15
1418struct kioctx;
1419#line 87 "include/linux/aio.h"
1420union __anonunion_ki_obj_223 {
1421 void *user ;
1422 struct task_struct *tsk ;
1423};
1424#line 87
1425struct eventfd_ctx;
1426#line 87 "include/linux/aio.h"
1427struct kiocb {
1428 struct list_head ki_run_list ;
1429 unsigned long ki_flags ;
1430 int ki_users ;
1431 unsigned int ki_key ;
1432 struct file *ki_filp ;
1433 struct kioctx *ki_ctx ;
1434 int (*ki_cancel)(struct kiocb * , struct io_event * ) ;
1435 ssize_t (*ki_retry)(struct kiocb * ) ;
1436 void (*ki_dtor)(struct kiocb * ) ;
1437 union __anonunion_ki_obj_223 ki_obj ;
1438 __u64 ki_user_data ;
1439 loff_t ki_pos ;
1440 void *private ;
1441 unsigned short ki_opcode ;
1442 size_t ki_nbytes ;
1443 char *ki_buf ;
1444 size_t ki_left ;
1445 struct iovec ki_inline_vec ;
1446 struct iovec *ki_iovec ;
1447 unsigned long ki_nr_segs ;
1448 unsigned long ki_cur_seg ;
1449 struct list_head ki_list ;
1450 struct list_head ki_batch ;
1451 struct eventfd_ctx *ki_eventfd ;
1452};
1453#line 166 "include/linux/aio.h"
1454struct aio_ring_info {
1455 unsigned long mmap_base ;
1456 unsigned long mmap_size ;
1457 struct page **ring_pages ;
1458 spinlock_t ring_lock ;
1459 long nr_pages ;
1460 unsigned int nr ;
1461 unsigned int tail ;
1462 struct page *internal_pages[8] ;
1463};
1464#line 179 "include/linux/aio.h"
1465struct kioctx {
1466 atomic_t users ;
1467 int dead ;
1468 struct mm_struct *mm ;
1469 unsigned long user_id ;
1470 struct hlist_node list ;
1471 wait_queue_head_t wait ;
1472 spinlock_t ctx_lock ;
1473 int reqs_active ;
1474 struct list_head active_reqs ;
1475 struct list_head run_list ;
1476 unsigned int max_reqs ;
1477 struct aio_ring_info ring_info ;
1478 struct delayed_work wq ;
1479 struct rcu_head rcu_head ;
1480};
1481#line 214
1482struct mm_struct;
1483#line 443 "include/linux/sched.h"
1484struct sighand_struct {
1485 atomic_t count ;
1486 struct k_sigaction action[64] ;
1487 spinlock_t siglock ;
1488 wait_queue_head_t signalfd_wqh ;
1489};
1490#line 450 "include/linux/sched.h"
1491struct pacct_struct {
1492 int ac_flag ;
1493 long ac_exitcode ;
1494 unsigned long ac_mem ;
1495 cputime_t ac_utime ;
1496 cputime_t ac_stime ;
1497 unsigned long ac_minflt ;
1498 unsigned long ac_majflt ;
1499};
1500#line 458 "include/linux/sched.h"
1501struct cpu_itimer {
1502 cputime_t expires ;
1503 cputime_t incr ;
1504 u32 error ;
1505 u32 incr_error ;
1506};
1507#line 476 "include/linux/sched.h"
1508struct task_cputime {
1509 cputime_t utime ;
1510 cputime_t stime ;
1511 unsigned long long sum_exec_runtime ;
1512};
1513#line 512 "include/linux/sched.h"
1514struct thread_group_cputimer {
1515 struct task_cputime cputime ;
1516 int running ;
1517 raw_spinlock_t lock ;
1518};
1519#line 519
1520struct autogroup;
1521#line 519
1522struct autogroup;
1523#line 528
1524struct tty_struct;
1525#line 528
1526struct taskstats;
1527#line 528
1528struct tty_audit_buf;
1529#line 528 "include/linux/sched.h"
1530struct signal_struct {
1531 atomic_t sigcnt ;
1532 atomic_t live ;
1533 int nr_threads ;
1534 wait_queue_head_t wait_chldexit ;
1535 struct task_struct *curr_target ;
1536 struct sigpending shared_pending ;
1537 int group_exit_code ;
1538 int notify_count ;
1539 struct task_struct *group_exit_task ;
1540 int group_stop_count ;
1541 unsigned int flags ;
1542 unsigned int is_child_subreaper : 1 ;
1543 unsigned int has_child_subreaper : 1 ;
1544 struct list_head posix_timers ;
1545 struct hrtimer real_timer ;
1546 struct pid *leader_pid ;
1547 ktime_t it_real_incr ;
1548 struct cpu_itimer it[2] ;
1549 struct thread_group_cputimer cputimer ;
1550 struct task_cputime cputime_expires ;
1551 struct list_head cpu_timers[3] ;
1552 struct pid *tty_old_pgrp ;
1553 int leader ;
1554 struct tty_struct *tty ;
1555 struct autogroup *autogroup ;
1556 cputime_t utime ;
1557 cputime_t stime ;
1558 cputime_t cutime ;
1559 cputime_t cstime ;
1560 cputime_t gtime ;
1561 cputime_t cgtime ;
1562 cputime_t prev_utime ;
1563 cputime_t prev_stime ;
1564 unsigned long nvcsw ;
1565 unsigned long nivcsw ;
1566 unsigned long cnvcsw ;
1567 unsigned long cnivcsw ;
1568 unsigned long min_flt ;
1569 unsigned long maj_flt ;
1570 unsigned long cmin_flt ;
1571 unsigned long cmaj_flt ;
1572 unsigned long inblock ;
1573 unsigned long oublock ;
1574 unsigned long cinblock ;
1575 unsigned long coublock ;
1576 unsigned long maxrss ;
1577 unsigned long cmaxrss ;
1578 struct task_io_accounting ioac ;
1579 unsigned long long sum_sched_runtime ;
1580 struct rlimit rlim[16] ;
1581 struct pacct_struct pacct ;
1582 struct taskstats *stats ;
1583 unsigned int audit_tty ;
1584 struct tty_audit_buf *tty_audit_buf ;
1585 struct rw_semaphore group_rwsem ;
1586 int oom_adj ;
1587 int oom_score_adj ;
1588 int oom_score_adj_min ;
1589 struct mutex cred_guard_mutex ;
1590};
1591#line 703 "include/linux/sched.h"
1592struct user_struct {
1593 atomic_t __count ;
1594 atomic_t processes ;
1595 atomic_t files ;
1596 atomic_t sigpending ;
1597 atomic_t inotify_watches ;
1598 atomic_t inotify_devs ;
1599 atomic_t fanotify_listeners ;
1600 atomic_long_t epoll_watches ;
1601 unsigned long mq_bytes ;
1602 unsigned long locked_shm ;
1603 struct key *uid_keyring ;
1604 struct key *session_keyring ;
1605 struct hlist_node uidhash_node ;
1606 uid_t uid ;
1607 struct user_namespace *user_ns ;
1608 atomic_long_t locked_vm ;
1609};
1610#line 747
1611struct backing_dev_info;
1612#line 747
1613struct backing_dev_info;
1614#line 748
1615struct reclaim_state;
1616#line 748
1617struct reclaim_state;
1618#line 751 "include/linux/sched.h"
1619struct sched_info {
1620 unsigned long pcount ;
1621 unsigned long long run_delay ;
1622 unsigned long long last_arrival ;
1623 unsigned long long last_queued ;
1624};
1625#line 763 "include/linux/sched.h"
1626struct task_delay_info {
1627 spinlock_t lock ;
1628 unsigned int flags ;
1629 struct timespec blkio_start ;
1630 struct timespec blkio_end ;
1631 u64 blkio_delay ;
1632 u64 swapin_delay ;
1633 u32 blkio_count ;
1634 u32 swapin_count ;
1635 struct timespec freepages_start ;
1636 struct timespec freepages_end ;
1637 u64 freepages_delay ;
1638 u32 freepages_count ;
1639};
1640#line 1088
1641struct io_context;
1642#line 1088
1643struct io_context;
1644#line 1097
1645struct audit_context;
1646#line 1098
1647struct mempolicy;
1648#line 1099
1649struct pipe_inode_info;
1650#line 1099
1651struct pipe_inode_info;
1652#line 1102
1653struct rq;
1654#line 1102
1655struct rq;
1656#line 1122 "include/linux/sched.h"
1657struct sched_class {
1658 struct sched_class const *next ;
1659 void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
1660 void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
1661 void (*yield_task)(struct rq *rq ) ;
1662 bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ;
1663 void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ;
1664 struct task_struct *(*pick_next_task)(struct rq *rq ) ;
1665 void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ;
1666 int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ;
1667 void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ;
1668 void (*post_schedule)(struct rq *this_rq ) ;
1669 void (*task_waking)(struct task_struct *task ) ;
1670 void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ;
1671 void (*set_cpus_allowed)(struct task_struct *p , struct cpumask const *newmask ) ;
1672 void (*rq_online)(struct rq *rq ) ;
1673 void (*rq_offline)(struct rq *rq ) ;
1674 void (*set_curr_task)(struct rq *rq ) ;
1675 void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ;
1676 void (*task_fork)(struct task_struct *p ) ;
1677 void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ;
1678 void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ;
1679 void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ;
1680 unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ;
1681 void (*task_move_group)(struct task_struct *p , int on_rq ) ;
1682};
1683#line 1167 "include/linux/sched.h"
1684struct load_weight {
1685 unsigned long weight ;
1686 unsigned long inv_weight ;
1687};
1688#line 1172 "include/linux/sched.h"
1689struct sched_statistics {
1690 u64 wait_start ;
1691 u64 wait_max ;
1692 u64 wait_count ;
1693 u64 wait_sum ;
1694 u64 iowait_count ;
1695 u64 iowait_sum ;
1696 u64 sleep_start ;
1697 u64 sleep_max ;
1698 s64 sum_sleep_runtime ;
1699 u64 block_start ;
1700 u64 block_max ;
1701 u64 exec_max ;
1702 u64 slice_max ;
1703 u64 nr_migrations_cold ;
1704 u64 nr_failed_migrations_affine ;
1705 u64 nr_failed_migrations_running ;
1706 u64 nr_failed_migrations_hot ;
1707 u64 nr_forced_migrations ;
1708 u64 nr_wakeups ;
1709 u64 nr_wakeups_sync ;
1710 u64 nr_wakeups_migrate ;
1711 u64 nr_wakeups_local ;
1712 u64 nr_wakeups_remote ;
1713 u64 nr_wakeups_affine ;
1714 u64 nr_wakeups_affine_attempts ;
1715 u64 nr_wakeups_passive ;
1716 u64 nr_wakeups_idle ;
1717};
1718#line 1207 "include/linux/sched.h"
1719struct sched_entity {
1720 struct load_weight load ;
1721 struct rb_node run_node ;
1722 struct list_head group_node ;
1723 unsigned int on_rq ;
1724 u64 exec_start ;
1725 u64 sum_exec_runtime ;
1726 u64 vruntime ;
1727 u64 prev_sum_exec_runtime ;
1728 u64 nr_migrations ;
1729 struct sched_statistics statistics ;
1730 struct sched_entity *parent ;
1731 struct cfs_rq *cfs_rq ;
1732 struct cfs_rq *my_q ;
1733};
1734#line 1233
1735struct rt_rq;
1736#line 1233 "include/linux/sched.h"
1737struct sched_rt_entity {
1738 struct list_head run_list ;
1739 unsigned long timeout ;
1740 unsigned int time_slice ;
1741 int nr_cpus_allowed ;
1742 struct sched_rt_entity *back ;
1743 struct sched_rt_entity *parent ;
1744 struct rt_rq *rt_rq ;
1745 struct rt_rq *my_q ;
1746};
1747#line 1264
1748struct files_struct;
1749#line 1264
1750struct css_set;
1751#line 1264
1752struct compat_robust_list_head;
1753#line 1264
1754struct mem_cgroup;
1755#line 1264 "include/linux/sched.h"
1756struct memcg_batch_info {
1757 int do_batch ;
1758 struct mem_cgroup *memcg ;
1759 unsigned long nr_pages ;
1760 unsigned long memsw_nr_pages ;
1761};
1762#line 1264 "include/linux/sched.h"
1763struct task_struct {
1764 long volatile state ;
1765 void *stack ;
1766 atomic_t usage ;
1767 unsigned int flags ;
1768 unsigned int ptrace ;
1769 struct llist_node wake_entry ;
1770 int on_cpu ;
1771 int on_rq ;
1772 int prio ;
1773 int static_prio ;
1774 int normal_prio ;
1775 unsigned int rt_priority ;
1776 struct sched_class const *sched_class ;
1777 struct sched_entity se ;
1778 struct sched_rt_entity rt ;
1779 struct hlist_head preempt_notifiers ;
1780 unsigned char fpu_counter ;
1781 unsigned int policy ;
1782 cpumask_t cpus_allowed ;
1783 struct sched_info sched_info ;
1784 struct list_head tasks ;
1785 struct plist_node pushable_tasks ;
1786 struct mm_struct *mm ;
1787 struct mm_struct *active_mm ;
1788 unsigned int brk_randomized : 1 ;
1789 int exit_state ;
1790 int exit_code ;
1791 int exit_signal ;
1792 int pdeath_signal ;
1793 unsigned int jobctl ;
1794 unsigned int personality ;
1795 unsigned int did_exec : 1 ;
1796 unsigned int in_execve : 1 ;
1797 unsigned int in_iowait : 1 ;
1798 unsigned int sched_reset_on_fork : 1 ;
1799 unsigned int sched_contributes_to_load : 1 ;
1800 unsigned int irq_thread : 1 ;
1801 pid_t pid ;
1802 pid_t tgid ;
1803 unsigned long stack_canary ;
1804 struct task_struct *real_parent ;
1805 struct task_struct *parent ;
1806 struct list_head children ;
1807 struct list_head sibling ;
1808 struct task_struct *group_leader ;
1809 struct list_head ptraced ;
1810 struct list_head ptrace_entry ;
1811 struct pid_link pids[3] ;
1812 struct list_head thread_group ;
1813 struct completion *vfork_done ;
1814 int *set_child_tid ;
1815 int *clear_child_tid ;
1816 cputime_t utime ;
1817 cputime_t stime ;
1818 cputime_t utimescaled ;
1819 cputime_t stimescaled ;
1820 cputime_t gtime ;
1821 cputime_t prev_utime ;
1822 cputime_t prev_stime ;
1823 unsigned long nvcsw ;
1824 unsigned long nivcsw ;
1825 struct timespec start_time ;
1826 struct timespec real_start_time ;
1827 unsigned long min_flt ;
1828 unsigned long maj_flt ;
1829 struct task_cputime cputime_expires ;
1830 struct list_head cpu_timers[3] ;
1831 struct cred const *real_cred ;
1832 struct cred const *cred ;
1833 struct cred *replacement_session_keyring ;
1834 char comm[16] ;
1835 int link_count ;
1836 int total_link_count ;
1837 struct sysv_sem sysvsem ;
1838 unsigned long last_switch_count ;
1839 struct thread_struct thread ;
1840 struct fs_struct *fs ;
1841 struct files_struct *files ;
1842 struct nsproxy *nsproxy ;
1843 struct signal_struct *signal ;
1844 struct sighand_struct *sighand ;
1845 sigset_t blocked ;
1846 sigset_t real_blocked ;
1847 sigset_t saved_sigmask ;
1848 struct sigpending pending ;
1849 unsigned long sas_ss_sp ;
1850 size_t sas_ss_size ;
1851 int (*notifier)(void *priv ) ;
1852 void *notifier_data ;
1853 sigset_t *notifier_mask ;
1854 struct audit_context *audit_context ;
1855 uid_t loginuid ;
1856 unsigned int sessionid ;
1857 seccomp_t seccomp ;
1858 u32 parent_exec_id ;
1859 u32 self_exec_id ;
1860 spinlock_t alloc_lock ;
1861 raw_spinlock_t pi_lock ;
1862 struct plist_head pi_waiters ;
1863 struct rt_mutex_waiter *pi_blocked_on ;
1864 struct mutex_waiter *blocked_on ;
1865 unsigned int irq_events ;
1866 unsigned long hardirq_enable_ip ;
1867 unsigned long hardirq_disable_ip ;
1868 unsigned int hardirq_enable_event ;
1869 unsigned int hardirq_disable_event ;
1870 int hardirqs_enabled ;
1871 int hardirq_context ;
1872 unsigned long softirq_disable_ip ;
1873 unsigned long softirq_enable_ip ;
1874 unsigned int softirq_disable_event ;
1875 unsigned int softirq_enable_event ;
1876 int softirqs_enabled ;
1877 int softirq_context ;
1878 void *journal_info ;
1879 struct bio_list *bio_list ;
1880 struct blk_plug *plug ;
1881 struct reclaim_state *reclaim_state ;
1882 struct backing_dev_info *backing_dev_info ;
1883 struct io_context *io_context ;
1884 unsigned long ptrace_message ;
1885 siginfo_t *last_siginfo ;
1886 struct task_io_accounting ioac ;
1887 u64 acct_rss_mem1 ;
1888 u64 acct_vm_mem1 ;
1889 cputime_t acct_timexpd ;
1890 nodemask_t mems_allowed ;
1891 seqcount_t mems_allowed_seq ;
1892 int cpuset_mem_spread_rotor ;
1893 int cpuset_slab_spread_rotor ;
1894 struct css_set *cgroups ;
1895 struct list_head cg_list ;
1896 struct robust_list_head *robust_list ;
1897 struct compat_robust_list_head *compat_robust_list ;
1898 struct list_head pi_state_list ;
1899 struct futex_pi_state *pi_state_cache ;
1900 struct perf_event_context *perf_event_ctxp[2] ;
1901 struct mutex perf_event_mutex ;
1902 struct list_head perf_event_list ;
1903 struct mempolicy *mempolicy ;
1904 short il_next ;
1905 short pref_node_fork ;
1906 struct rcu_head rcu ;
1907 struct pipe_inode_info *splice_pipe ;
1908 struct task_delay_info *delays ;
1909 int make_it_fail ;
1910 int nr_dirtied ;
1911 int nr_dirtied_pause ;
1912 unsigned long dirty_paused_when ;
1913 int latency_record_count ;
1914 struct latency_record latency_record[32] ;
1915 unsigned long timer_slack_ns ;
1916 unsigned long default_timer_slack_ns ;
1917 struct list_head *scm_work_list ;
1918 unsigned long trace ;
1919 unsigned long trace_recursion ;
1920 struct memcg_batch_info memcg_batch ;
1921 atomic_t ptrace_bp_refcnt ;
1922};
1923#line 1681
1924struct pid_namespace;
1925#line 62 "include/linux/stat.h"
1926struct kstat {
1927 u64 ino ;
1928 dev_t dev ;
1929 umode_t mode ;
1930 unsigned int nlink ;
1931 uid_t uid ;
1932 gid_t gid ;
1933 dev_t rdev ;
1934 loff_t size ;
1935 struct timespec atime ;
1936 struct timespec mtime ;
1937 struct timespec ctime ;
1938 unsigned long blksize ;
1939 unsigned long long blocks ;
1940};
1941#line 48 "include/linux/kmod.h"
1942struct cred;
1943#line 49
1944struct file;
1945#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
1946struct task_struct;
1947#line 18 "include/linux/elf.h"
1948typedef __u64 Elf64_Addr;
1949#line 19 "include/linux/elf.h"
1950typedef __u16 Elf64_Half;
1951#line 23 "include/linux/elf.h"
1952typedef __u32 Elf64_Word;
1953#line 24 "include/linux/elf.h"
1954typedef __u64 Elf64_Xword;
1955#line 194 "include/linux/elf.h"
1956struct elf64_sym {
1957 Elf64_Word st_name ;
1958 unsigned char st_info ;
1959 unsigned char st_other ;
1960 Elf64_Half st_shndx ;
1961 Elf64_Addr st_value ;
1962 Elf64_Xword st_size ;
1963};
1964#line 194 "include/linux/elf.h"
1965typedef struct elf64_sym Elf64_Sym;
1966#line 438
1967struct file;
1968#line 20 "include/linux/kobject_ns.h"
1969struct sock;
1970#line 20
1971struct sock;
1972#line 21
1973struct kobject;
1974#line 21
1975struct kobject;
1976#line 27
1977enum kobj_ns_type {
1978 KOBJ_NS_TYPE_NONE = 0,
1979 KOBJ_NS_TYPE_NET = 1,
1980 KOBJ_NS_TYPES = 2
1981} ;
1982#line 40 "include/linux/kobject_ns.h"
1983struct kobj_ns_type_operations {
1984 enum kobj_ns_type type ;
1985 void *(*grab_current_ns)(void) ;
1986 void const *(*netlink_ns)(struct sock *sk ) ;
1987 void const *(*initial_ns)(void) ;
1988 void (*drop_ns)(void * ) ;
1989};
1990#line 22 "include/linux/sysfs.h"
1991struct kobject;
1992#line 23
1993struct module;
1994#line 24
1995enum kobj_ns_type;
1996#line 26 "include/linux/sysfs.h"
1997struct attribute {
1998 char const *name ;
1999 umode_t mode ;
2000};
2001#line 85
2002struct file;
2003#line 86
2004struct vm_area_struct;
2005#line 112 "include/linux/sysfs.h"
2006struct sysfs_ops {
2007 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
2008 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
2009 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
2010};
2011#line 118
2012struct sysfs_dirent;
2013#line 118
2014struct sysfs_dirent;
2015#line 22 "include/linux/kref.h"
2016struct kref {
2017 atomic_t refcount ;
2018};
2019#line 60 "include/linux/kobject.h"
2020struct kset;
2021#line 60
2022struct kobj_type;
2023#line 60 "include/linux/kobject.h"
2024struct kobject {
2025 char const *name ;
2026 struct list_head entry ;
2027 struct kobject *parent ;
2028 struct kset *kset ;
2029 struct kobj_type *ktype ;
2030 struct sysfs_dirent *sd ;
2031 struct kref kref ;
2032 unsigned int state_initialized : 1 ;
2033 unsigned int state_in_sysfs : 1 ;
2034 unsigned int state_add_uevent_sent : 1 ;
2035 unsigned int state_remove_uevent_sent : 1 ;
2036 unsigned int uevent_suppress : 1 ;
2037};
2038#line 108 "include/linux/kobject.h"
2039struct kobj_type {
2040 void (*release)(struct kobject *kobj ) ;
2041 struct sysfs_ops const *sysfs_ops ;
2042 struct attribute **default_attrs ;
2043 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
2044 void const *(*namespace)(struct kobject *kobj ) ;
2045};
2046#line 116 "include/linux/kobject.h"
2047struct kobj_uevent_env {
2048 char *envp[32] ;
2049 int envp_idx ;
2050 char buf[2048] ;
2051 int buflen ;
2052};
2053#line 123 "include/linux/kobject.h"
2054struct kset_uevent_ops {
2055 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
2056 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
2057 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
2058};
2059#line 140
2060struct sock;
2061#line 159 "include/linux/kobject.h"
2062struct kset {
2063 struct list_head list ;
2064 spinlock_t list_lock ;
2065 struct kobject kobj ;
2066 struct kset_uevent_ops const *uevent_ops ;
2067};
2068#line 39 "include/linux/moduleparam.h"
2069struct kernel_param;
2070#line 39
2071struct kernel_param;
2072#line 41 "include/linux/moduleparam.h"
2073struct kernel_param_ops {
2074 int (*set)(char const *val , struct kernel_param const *kp ) ;
2075 int (*get)(char *buffer , struct kernel_param const *kp ) ;
2076 void (*free)(void *arg ) ;
2077};
2078#line 50
2079struct kparam_string;
2080#line 50
2081struct kparam_array;
2082#line 50 "include/linux/moduleparam.h"
2083union __anonunion____missing_field_name_229 {
2084 void *arg ;
2085 struct kparam_string const *str ;
2086 struct kparam_array const *arr ;
2087};
2088#line 50 "include/linux/moduleparam.h"
2089struct kernel_param {
2090 char const *name ;
2091 struct kernel_param_ops const *ops ;
2092 u16 perm ;
2093 s16 level ;
2094 union __anonunion____missing_field_name_229 __annonCompField43 ;
2095};
2096#line 63 "include/linux/moduleparam.h"
2097struct kparam_string {
2098 unsigned int maxlen ;
2099 char *string ;
2100};
2101#line 69 "include/linux/moduleparam.h"
2102struct kparam_array {
2103 unsigned int max ;
2104 unsigned int elemsize ;
2105 unsigned int *num ;
2106 struct kernel_param_ops const *ops ;
2107 void *elem ;
2108};
2109#line 445
2110struct module;
2111#line 80 "include/linux/jump_label.h"
2112struct module;
2113#line 143 "include/linux/jump_label.h"
2114struct static_key {
2115 atomic_t enabled ;
2116};
2117#line 22 "include/linux/tracepoint.h"
2118struct module;
2119#line 23
2120struct tracepoint;
2121#line 23
2122struct tracepoint;
2123#line 25 "include/linux/tracepoint.h"
2124struct tracepoint_func {
2125 void *func ;
2126 void *data ;
2127};
2128#line 30 "include/linux/tracepoint.h"
2129struct tracepoint {
2130 char const *name ;
2131 struct static_key key ;
2132 void (*regfunc)(void) ;
2133 void (*unregfunc)(void) ;
2134 struct tracepoint_func *funcs ;
2135};
2136#line 19 "include/linux/export.h"
2137struct kernel_symbol {
2138 unsigned long value ;
2139 char const *name ;
2140};
2141#line 8 "include/asm-generic/module.h"
2142struct mod_arch_specific {
2143
2144};
2145#line 35 "include/linux/module.h"
2146struct module;
2147#line 37
2148struct module_param_attrs;
2149#line 37 "include/linux/module.h"
2150struct module_kobject {
2151 struct kobject kobj ;
2152 struct module *mod ;
2153 struct kobject *drivers_dir ;
2154 struct module_param_attrs *mp ;
2155};
2156#line 44 "include/linux/module.h"
2157struct module_attribute {
2158 struct attribute attr ;
2159 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
2160 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
2161 size_t count ) ;
2162 void (*setup)(struct module * , char const * ) ;
2163 int (*test)(struct module * ) ;
2164 void (*free)(struct module * ) ;
2165};
2166#line 71
2167struct exception_table_entry;
2168#line 71
2169struct exception_table_entry;
2170#line 199
2171enum module_state {
2172 MODULE_STATE_LIVE = 0,
2173 MODULE_STATE_COMING = 1,
2174 MODULE_STATE_GOING = 2
2175} ;
2176#line 215 "include/linux/module.h"
2177struct module_ref {
2178 unsigned long incs ;
2179 unsigned long decs ;
2180} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ;
2181#line 220
2182struct module_sect_attrs;
2183#line 220
2184struct module_notes_attrs;
2185#line 220
2186struct ftrace_event_call;
2187#line 220 "include/linux/module.h"
2188struct module {
2189 enum module_state state ;
2190 struct list_head list ;
2191 char name[64UL - sizeof(unsigned long )] ;
2192 struct module_kobject mkobj ;
2193 struct module_attribute *modinfo_attrs ;
2194 char const *version ;
2195 char const *srcversion ;
2196 struct kobject *holders_dir ;
2197 struct kernel_symbol const *syms ;
2198 unsigned long const *crcs ;
2199 unsigned int num_syms ;
2200 struct kernel_param *kp ;
2201 unsigned int num_kp ;
2202 unsigned int num_gpl_syms ;
2203 struct kernel_symbol const *gpl_syms ;
2204 unsigned long const *gpl_crcs ;
2205 struct kernel_symbol const *unused_syms ;
2206 unsigned long const *unused_crcs ;
2207 unsigned int num_unused_syms ;
2208 unsigned int num_unused_gpl_syms ;
2209 struct kernel_symbol const *unused_gpl_syms ;
2210 unsigned long const *unused_gpl_crcs ;
2211 struct kernel_symbol const *gpl_future_syms ;
2212 unsigned long const *gpl_future_crcs ;
2213 unsigned int num_gpl_future_syms ;
2214 unsigned int num_exentries ;
2215 struct exception_table_entry *extable ;
2216 int (*init)(void) ;
2217 void *module_init ;
2218 void *module_core ;
2219 unsigned int init_size ;
2220 unsigned int core_size ;
2221 unsigned int init_text_size ;
2222 unsigned int core_text_size ;
2223 unsigned int init_ro_size ;
2224 unsigned int core_ro_size ;
2225 struct mod_arch_specific arch ;
2226 unsigned int taints ;
2227 unsigned int num_bugs ;
2228 struct list_head bug_list ;
2229 struct bug_entry *bug_table ;
2230 Elf64_Sym *symtab ;
2231 Elf64_Sym *core_symtab ;
2232 unsigned int num_symtab ;
2233 unsigned int core_num_syms ;
2234 char *strtab ;
2235 char *core_strtab ;
2236 struct module_sect_attrs *sect_attrs ;
2237 struct module_notes_attrs *notes_attrs ;
2238 char *args ;
2239 void *percpu ;
2240 unsigned int percpu_size ;
2241 unsigned int num_tracepoints ;
2242 struct tracepoint * const *tracepoints_ptrs ;
2243 unsigned int num_trace_bprintk_fmt ;
2244 char const **trace_bprintk_fmt_start ;
2245 struct ftrace_event_call **trace_events ;
2246 unsigned int num_trace_events ;
2247 struct list_head source_list ;
2248 struct list_head target_list ;
2249 struct task_struct *waiter ;
2250 void (*exit)(void) ;
2251 struct module_ref *refptr ;
2252 ctor_fn_t *ctors ;
2253 unsigned int num_ctors ;
2254};
2255#line 15 "include/linux/blk_types.h"
2256struct page;
2257#line 16
2258struct block_device;
2259#line 16
2260struct block_device;
2261#line 33 "include/linux/list_bl.h"
2262struct hlist_bl_node;
2263#line 33 "include/linux/list_bl.h"
2264struct hlist_bl_head {
2265 struct hlist_bl_node *first ;
2266};
2267#line 37 "include/linux/list_bl.h"
2268struct hlist_bl_node {
2269 struct hlist_bl_node *next ;
2270 struct hlist_bl_node **pprev ;
2271};
2272#line 13 "include/linux/dcache.h"
2273struct nameidata;
2274#line 13
2275struct nameidata;
2276#line 14
2277struct path;
2278#line 14
2279struct path;
2280#line 15
2281struct vfsmount;
2282#line 15
2283struct vfsmount;
2284#line 35 "include/linux/dcache.h"
2285struct qstr {
2286 unsigned int hash ;
2287 unsigned int len ;
2288 unsigned char const *name ;
2289};
2290#line 88
2291struct dentry_operations;
2292#line 88
2293struct super_block;
2294#line 88 "include/linux/dcache.h"
2295union __anonunion_d_u_231 {
2296 struct list_head d_child ;
2297 struct rcu_head d_rcu ;
2298};
2299#line 88 "include/linux/dcache.h"
2300struct dentry {
2301 unsigned int d_flags ;
2302 seqcount_t d_seq ;
2303 struct hlist_bl_node d_hash ;
2304 struct dentry *d_parent ;
2305 struct qstr d_name ;
2306 struct inode *d_inode ;
2307 unsigned char d_iname[32] ;
2308 unsigned int d_count ;
2309 spinlock_t d_lock ;
2310 struct dentry_operations const *d_op ;
2311 struct super_block *d_sb ;
2312 unsigned long d_time ;
2313 void *d_fsdata ;
2314 struct list_head d_lru ;
2315 union __anonunion_d_u_231 d_u ;
2316 struct list_head d_subdirs ;
2317 struct list_head d_alias ;
2318};
2319#line 131 "include/linux/dcache.h"
2320struct dentry_operations {
2321 int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
2322 int (*d_hash)(struct dentry const * , struct inode const * , struct qstr * ) ;
2323 int (*d_compare)(struct dentry const * , struct inode const * , struct dentry const * ,
2324 struct inode const * , unsigned int , char const * , struct qstr const * ) ;
2325 int (*d_delete)(struct dentry const * ) ;
2326 void (*d_release)(struct dentry * ) ;
2327 void (*d_prune)(struct dentry * ) ;
2328 void (*d_iput)(struct dentry * , struct inode * ) ;
2329 char *(*d_dname)(struct dentry * , char * , int ) ;
2330 struct vfsmount *(*d_automount)(struct path * ) ;
2331 int (*d_manage)(struct dentry * , bool ) ;
2332} __attribute__((__aligned__((1) << (6) ))) ;
2333#line 4 "include/linux/path.h"
2334struct dentry;
2335#line 5
2336struct vfsmount;
2337#line 7 "include/linux/path.h"
2338struct path {
2339 struct vfsmount *mnt ;
2340 struct dentry *dentry ;
2341};
2342#line 64 "include/linux/radix-tree.h"
2343struct radix_tree_node;
2344#line 64 "include/linux/radix-tree.h"
2345struct radix_tree_root {
2346 unsigned int height ;
2347 gfp_t gfp_mask ;
2348 struct radix_tree_node *rnode ;
2349};
2350#line 16 "include/linux/fiemap.h"
2351struct fiemap_extent {
2352 __u64 fe_logical ;
2353 __u64 fe_physical ;
2354 __u64 fe_length ;
2355 __u64 fe_reserved64[2] ;
2356 __u32 fe_flags ;
2357 __u32 fe_reserved[3] ;
2358};
2359#line 10 "include/linux/migrate_mode.h"
2360enum migrate_mode {
2361 MIGRATE_ASYNC = 0,
2362 MIGRATE_SYNC_LIGHT = 1,
2363 MIGRATE_SYNC = 2
2364} ;
2365#line 408 "include/linux/fs.h"
2366struct export_operations;
2367#line 408
2368struct export_operations;
2369#line 410
2370struct iovec;
2371#line 411
2372struct nameidata;
2373#line 412
2374struct kiocb;
2375#line 413
2376struct kobject;
2377#line 414
2378struct pipe_inode_info;
2379#line 415
2380struct poll_table_struct;
2381#line 415
2382struct poll_table_struct;
2383#line 416
2384struct kstatfs;
2385#line 416
2386struct kstatfs;
2387#line 417
2388struct vm_area_struct;
2389#line 418
2390struct vfsmount;
2391#line 419
2392struct cred;
2393#line 469 "include/linux/fs.h"
2394struct iattr {
2395 unsigned int ia_valid ;
2396 umode_t ia_mode ;
2397 uid_t ia_uid ;
2398 gid_t ia_gid ;
2399 loff_t ia_size ;
2400 struct timespec ia_atime ;
2401 struct timespec ia_mtime ;
2402 struct timespec ia_ctime ;
2403 struct file *ia_file ;
2404};
2405#line 129 "include/linux/quota.h"
2406struct if_dqinfo {
2407 __u64 dqi_bgrace ;
2408 __u64 dqi_igrace ;
2409 __u32 dqi_flags ;
2410 __u32 dqi_valid ;
2411};
2412#line 50 "include/linux/dqblk_xfs.h"
2413struct fs_disk_quota {
2414 __s8 d_version ;
2415 __s8 d_flags ;
2416 __u16 d_fieldmask ;
2417 __u32 d_id ;
2418 __u64 d_blk_hardlimit ;
2419 __u64 d_blk_softlimit ;
2420 __u64 d_ino_hardlimit ;
2421 __u64 d_ino_softlimit ;
2422 __u64 d_bcount ;
2423 __u64 d_icount ;
2424 __s32 d_itimer ;
2425 __s32 d_btimer ;
2426 __u16 d_iwarns ;
2427 __u16 d_bwarns ;
2428 __s32 d_padding2 ;
2429 __u64 d_rtb_hardlimit ;
2430 __u64 d_rtb_softlimit ;
2431 __u64 d_rtbcount ;
2432 __s32 d_rtbtimer ;
2433 __u16 d_rtbwarns ;
2434 __s16 d_padding3 ;
2435 char d_padding4[8] ;
2436};
2437#line 146 "include/linux/dqblk_xfs.h"
2438struct fs_qfilestat {
2439 __u64 qfs_ino ;
2440 __u64 qfs_nblks ;
2441 __u32 qfs_nextents ;
2442};
2443#line 146 "include/linux/dqblk_xfs.h"
2444typedef struct fs_qfilestat fs_qfilestat_t;
2445#line 152 "include/linux/dqblk_xfs.h"
2446struct fs_quota_stat {
2447 __s8 qs_version ;
2448 __u16 qs_flags ;
2449 __s8 qs_pad ;
2450 fs_qfilestat_t qs_uquota ;
2451 fs_qfilestat_t qs_gquota ;
2452 __u32 qs_incoredqs ;
2453 __s32 qs_btimelimit ;
2454 __s32 qs_itimelimit ;
2455 __s32 qs_rtbtimelimit ;
2456 __u16 qs_bwarnlimit ;
2457 __u16 qs_iwarnlimit ;
2458};
2459#line 17 "include/linux/dqblk_qtree.h"
2460struct dquot;
2461#line 17
2462struct dquot;
2463#line 185 "include/linux/quota.h"
2464typedef __kernel_uid32_t qid_t;
2465#line 186 "include/linux/quota.h"
2466typedef long long qsize_t;
2467#line 200 "include/linux/quota.h"
2468struct mem_dqblk {
2469 qsize_t dqb_bhardlimit ;
2470 qsize_t dqb_bsoftlimit ;
2471 qsize_t dqb_curspace ;
2472 qsize_t dqb_rsvspace ;
2473 qsize_t dqb_ihardlimit ;
2474 qsize_t dqb_isoftlimit ;
2475 qsize_t dqb_curinodes ;
2476 time_t dqb_btime ;
2477 time_t dqb_itime ;
2478};
2479#line 215
2480struct quota_format_type;
2481#line 215
2482struct quota_format_type;
2483#line 217 "include/linux/quota.h"
2484struct mem_dqinfo {
2485 struct quota_format_type *dqi_format ;
2486 int dqi_fmt_id ;
2487 struct list_head dqi_dirty_list ;
2488 unsigned long dqi_flags ;
2489 unsigned int dqi_bgrace ;
2490 unsigned int dqi_igrace ;
2491 qsize_t dqi_maxblimit ;
2492 qsize_t dqi_maxilimit ;
2493 void *dqi_priv ;
2494};
2495#line 230
2496struct super_block;
2497#line 288 "include/linux/quota.h"
2498struct dquot {
2499 struct hlist_node dq_hash ;
2500 struct list_head dq_inuse ;
2501 struct list_head dq_free ;
2502 struct list_head dq_dirty ;
2503 struct mutex dq_lock ;
2504 atomic_t dq_count ;
2505 wait_queue_head_t dq_wait_unused ;
2506 struct super_block *dq_sb ;
2507 unsigned int dq_id ;
2508 loff_t dq_off ;
2509 unsigned long dq_flags ;
2510 short dq_type ;
2511 struct mem_dqblk dq_dqb ;
2512};
2513#line 305 "include/linux/quota.h"
2514struct quota_format_ops {
2515 int (*check_quota_file)(struct super_block *sb , int type ) ;
2516 int (*read_file_info)(struct super_block *sb , int type ) ;
2517 int (*write_file_info)(struct super_block *sb , int type ) ;
2518 int (*free_file_info)(struct super_block *sb , int type ) ;
2519 int (*read_dqblk)(struct dquot *dquot ) ;
2520 int (*commit_dqblk)(struct dquot *dquot ) ;
2521 int (*release_dqblk)(struct dquot *dquot ) ;
2522};
2523#line 316 "include/linux/quota.h"
2524struct dquot_operations {
2525 int (*write_dquot)(struct dquot * ) ;
2526 struct dquot *(*alloc_dquot)(struct super_block * , int ) ;
2527 void (*destroy_dquot)(struct dquot * ) ;
2528 int (*acquire_dquot)(struct dquot * ) ;
2529 int (*release_dquot)(struct dquot * ) ;
2530 int (*mark_dirty)(struct dquot * ) ;
2531 int (*write_info)(struct super_block * , int ) ;
2532 qsize_t *(*get_reserved_space)(struct inode * ) ;
2533};
2534#line 329
2535struct path;
2536#line 332 "include/linux/quota.h"
2537struct quotactl_ops {
2538 int (*quota_on)(struct super_block * , int , int , struct path * ) ;
2539 int (*quota_on_meta)(struct super_block * , int , int ) ;
2540 int (*quota_off)(struct super_block * , int ) ;
2541 int (*quota_sync)(struct super_block * , int , int ) ;
2542 int (*get_info)(struct super_block * , int , struct if_dqinfo * ) ;
2543 int (*set_info)(struct super_block * , int , struct if_dqinfo * ) ;
2544 int (*get_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
2545 int (*set_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
2546 int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
2547 int (*set_xstate)(struct super_block * , unsigned int , int ) ;
2548};
2549#line 345 "include/linux/quota.h"
2550struct quota_format_type {
2551 int qf_fmt_id ;
2552 struct quota_format_ops const *qf_ops ;
2553 struct module *qf_owner ;
2554 struct quota_format_type *qf_next ;
2555};
2556#line 399 "include/linux/quota.h"
2557struct quota_info {
2558 unsigned int flags ;
2559 struct mutex dqio_mutex ;
2560 struct mutex dqonoff_mutex ;
2561 struct rw_semaphore dqptr_sem ;
2562 struct inode *files[2] ;
2563 struct mem_dqinfo info[2] ;
2564 struct quota_format_ops const *ops[2] ;
2565};
2566#line 532 "include/linux/fs.h"
2567struct page;
2568#line 533
2569struct address_space;
2570#line 534
2571struct writeback_control;
2572#line 577 "include/linux/fs.h"
2573union __anonunion_arg_238 {
2574 char *buf ;
2575 void *data ;
2576};
2577#line 577 "include/linux/fs.h"
2578struct __anonstruct_read_descriptor_t_237 {
2579 size_t written ;
2580 size_t count ;
2581 union __anonunion_arg_238 arg ;
2582 int error ;
2583};
2584#line 577 "include/linux/fs.h"
2585typedef struct __anonstruct_read_descriptor_t_237 read_descriptor_t;
2586#line 590 "include/linux/fs.h"
2587struct address_space_operations {
2588 int (*writepage)(struct page *page , struct writeback_control *wbc ) ;
2589 int (*readpage)(struct file * , struct page * ) ;
2590 int (*writepages)(struct address_space * , struct writeback_control * ) ;
2591 int (*set_page_dirty)(struct page *page ) ;
2592 int (*readpages)(struct file *filp , struct address_space *mapping , struct list_head *pages ,
2593 unsigned int nr_pages ) ;
2594 int (*write_begin)(struct file * , struct address_space *mapping , loff_t pos ,
2595 unsigned int len , unsigned int flags , struct page **pagep ,
2596 void **fsdata ) ;
2597 int (*write_end)(struct file * , struct address_space *mapping , loff_t pos , unsigned int len ,
2598 unsigned int copied , struct page *page , void *fsdata ) ;
2599 sector_t (*bmap)(struct address_space * , sector_t ) ;
2600 void (*invalidatepage)(struct page * , unsigned long ) ;
2601 int (*releasepage)(struct page * , gfp_t ) ;
2602 void (*freepage)(struct page * ) ;
2603 ssize_t (*direct_IO)(int , struct kiocb * , struct iovec const *iov , loff_t offset ,
2604 unsigned long nr_segs ) ;
2605 int (*get_xip_mem)(struct address_space * , unsigned long , int , void ** , unsigned long * ) ;
2606 int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode ) ;
2607 int (*launder_page)(struct page * ) ;
2608 int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long ) ;
2609 int (*error_remove_page)(struct address_space * , struct page * ) ;
2610};
2611#line 645
2612struct backing_dev_info;
2613#line 646 "include/linux/fs.h"
2614struct address_space {
2615 struct inode *host ;
2616 struct radix_tree_root page_tree ;
2617 spinlock_t tree_lock ;
2618 unsigned int i_mmap_writable ;
2619 struct prio_tree_root i_mmap ;
2620 struct list_head i_mmap_nonlinear ;
2621 struct mutex i_mmap_mutex ;
2622 unsigned long nrpages ;
2623 unsigned long writeback_index ;
2624 struct address_space_operations const *a_ops ;
2625 unsigned long flags ;
2626 struct backing_dev_info *backing_dev_info ;
2627 spinlock_t private_lock ;
2628 struct list_head private_list ;
2629 struct address_space *assoc_mapping ;
2630} __attribute__((__aligned__(sizeof(long )))) ;
2631#line 669
2632struct request_queue;
2633#line 669
2634struct request_queue;
2635#line 671
2636struct hd_struct;
2637#line 671
2638struct gendisk;
2639#line 671 "include/linux/fs.h"
2640struct block_device {
2641 dev_t bd_dev ;
2642 int bd_openers ;
2643 struct inode *bd_inode ;
2644 struct super_block *bd_super ;
2645 struct mutex bd_mutex ;
2646 struct list_head bd_inodes ;
2647 void *bd_claiming ;
2648 void *bd_holder ;
2649 int bd_holders ;
2650 bool bd_write_holder ;
2651 struct list_head bd_holder_disks ;
2652 struct block_device *bd_contains ;
2653 unsigned int bd_block_size ;
2654 struct hd_struct *bd_part ;
2655 unsigned int bd_part_count ;
2656 int bd_invalidated ;
2657 struct gendisk *bd_disk ;
2658 struct request_queue *bd_queue ;
2659 struct list_head bd_list ;
2660 unsigned long bd_private ;
2661 int bd_fsfreeze_count ;
2662 struct mutex bd_fsfreeze_mutex ;
2663};
2664#line 749
2665struct posix_acl;
2666#line 749
2667struct posix_acl;
2668#line 761
2669struct inode_operations;
2670#line 761 "include/linux/fs.h"
2671union __anonunion____missing_field_name_239 {
2672 unsigned int const i_nlink ;
2673 unsigned int __i_nlink ;
2674};
2675#line 761 "include/linux/fs.h"
2676union __anonunion____missing_field_name_240 {
2677 struct list_head i_dentry ;
2678 struct rcu_head i_rcu ;
2679};
2680#line 761
2681struct file_operations;
2682#line 761
2683struct file_lock;
2684#line 761
2685struct cdev;
2686#line 761 "include/linux/fs.h"
2687union __anonunion____missing_field_name_241 {
2688 struct pipe_inode_info *i_pipe ;
2689 struct block_device *i_bdev ;
2690 struct cdev *i_cdev ;
2691};
2692#line 761 "include/linux/fs.h"
2693struct inode {
2694 umode_t i_mode ;
2695 unsigned short i_opflags ;
2696 uid_t i_uid ;
2697 gid_t i_gid ;
2698 unsigned int i_flags ;
2699 struct posix_acl *i_acl ;
2700 struct posix_acl *i_default_acl ;
2701 struct inode_operations const *i_op ;
2702 struct super_block *i_sb ;
2703 struct address_space *i_mapping ;
2704 void *i_security ;
2705 unsigned long i_ino ;
2706 union __anonunion____missing_field_name_239 __annonCompField44 ;
2707 dev_t i_rdev ;
2708 struct timespec i_atime ;
2709 struct timespec i_mtime ;
2710 struct timespec i_ctime ;
2711 spinlock_t i_lock ;
2712 unsigned short i_bytes ;
2713 blkcnt_t i_blocks ;
2714 loff_t i_size ;
2715 unsigned long i_state ;
2716 struct mutex i_mutex ;
2717 unsigned long dirtied_when ;
2718 struct hlist_node i_hash ;
2719 struct list_head i_wb_list ;
2720 struct list_head i_lru ;
2721 struct list_head i_sb_list ;
2722 union __anonunion____missing_field_name_240 __annonCompField45 ;
2723 atomic_t i_count ;
2724 unsigned int i_blkbits ;
2725 u64 i_version ;
2726 atomic_t i_dio_count ;
2727 atomic_t i_writecount ;
2728 struct file_operations const *i_fop ;
2729 struct file_lock *i_flock ;
2730 struct address_space i_data ;
2731 struct dquot *i_dquot[2] ;
2732 struct list_head i_devices ;
2733 union __anonunion____missing_field_name_241 __annonCompField46 ;
2734 __u32 i_generation ;
2735 __u32 i_fsnotify_mask ;
2736 struct hlist_head i_fsnotify_marks ;
2737 atomic_t i_readcount ;
2738 void *i_private ;
2739};
2740#line 942 "include/linux/fs.h"
2741struct fown_struct {
2742 rwlock_t lock ;
2743 struct pid *pid ;
2744 enum pid_type pid_type ;
2745 uid_t uid ;
2746 uid_t euid ;
2747 int signum ;
2748};
2749#line 953 "include/linux/fs.h"
2750struct file_ra_state {
2751 unsigned long start ;
2752 unsigned int size ;
2753 unsigned int async_size ;
2754 unsigned int ra_pages ;
2755 unsigned int mmap_miss ;
2756 loff_t prev_pos ;
2757};
2758#line 976 "include/linux/fs.h"
2759union __anonunion_f_u_242 {
2760 struct list_head fu_list ;
2761 struct rcu_head fu_rcuhead ;
2762};
2763#line 976 "include/linux/fs.h"
2764struct file {
2765 union __anonunion_f_u_242 f_u ;
2766 struct path f_path ;
2767 struct file_operations const *f_op ;
2768 spinlock_t f_lock ;
2769 int f_sb_list_cpu ;
2770 atomic_long_t f_count ;
2771 unsigned int f_flags ;
2772 fmode_t f_mode ;
2773 loff_t f_pos ;
2774 struct fown_struct f_owner ;
2775 struct cred const *f_cred ;
2776 struct file_ra_state f_ra ;
2777 u64 f_version ;
2778 void *f_security ;
2779 void *private_data ;
2780 struct list_head f_ep_links ;
2781 struct list_head f_tfile_llink ;
2782 struct address_space *f_mapping ;
2783 unsigned long f_mnt_write_state ;
2784};
2785#line 1111 "include/linux/fs.h"
2786typedef struct files_struct *fl_owner_t;
2787#line 1113 "include/linux/fs.h"
2788struct file_lock_operations {
2789 void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
2790 void (*fl_release_private)(struct file_lock * ) ;
2791};
2792#line 1118 "include/linux/fs.h"
2793struct lock_manager_operations {
2794 int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
2795 void (*lm_notify)(struct file_lock * ) ;
2796 int (*lm_grant)(struct file_lock * , struct file_lock * , int ) ;
2797 void (*lm_release_private)(struct file_lock * ) ;
2798 void (*lm_break)(struct file_lock * ) ;
2799 int (*lm_change)(struct file_lock ** , int ) ;
2800};
2801#line 4 "include/linux/nfs_fs_i.h"
2802struct nlm_lockowner;
2803#line 4
2804struct nlm_lockowner;
2805#line 9 "include/linux/nfs_fs_i.h"
2806struct nfs_lock_info {
2807 u32 state ;
2808 struct nlm_lockowner *owner ;
2809 struct list_head list ;
2810};
2811#line 15
2812struct nfs4_lock_state;
2813#line 15
2814struct nfs4_lock_state;
2815#line 16 "include/linux/nfs_fs_i.h"
2816struct nfs4_lock_info {
2817 struct nfs4_lock_state *owner ;
2818};
2819#line 1138 "include/linux/fs.h"
2820struct fasync_struct;
2821#line 1138 "include/linux/fs.h"
2822struct __anonstruct_afs_244 {
2823 struct list_head link ;
2824 int state ;
2825};
2826#line 1138 "include/linux/fs.h"
2827union __anonunion_fl_u_243 {
2828 struct nfs_lock_info nfs_fl ;
2829 struct nfs4_lock_info nfs4_fl ;
2830 struct __anonstruct_afs_244 afs ;
2831};
2832#line 1138 "include/linux/fs.h"
2833struct file_lock {
2834 struct file_lock *fl_next ;
2835 struct list_head fl_link ;
2836 struct list_head fl_block ;
2837 fl_owner_t fl_owner ;
2838 unsigned int fl_flags ;
2839 unsigned char fl_type ;
2840 unsigned int fl_pid ;
2841 struct pid *fl_nspid ;
2842 wait_queue_head_t fl_wait ;
2843 struct file *fl_file ;
2844 loff_t fl_start ;
2845 loff_t fl_end ;
2846 struct fasync_struct *fl_fasync ;
2847 unsigned long fl_break_time ;
2848 unsigned long fl_downgrade_time ;
2849 struct file_lock_operations const *fl_ops ;
2850 struct lock_manager_operations const *fl_lmops ;
2851 union __anonunion_fl_u_243 fl_u ;
2852};
2853#line 1378 "include/linux/fs.h"
2854struct fasync_struct {
2855 spinlock_t fa_lock ;
2856 int magic ;
2857 int fa_fd ;
2858 struct fasync_struct *fa_next ;
2859 struct file *fa_file ;
2860 struct rcu_head fa_rcu ;
2861};
2862#line 1418
2863struct file_system_type;
2864#line 1418
2865struct super_operations;
2866#line 1418
2867struct xattr_handler;
2868#line 1418
2869struct mtd_info;
2870#line 1418 "include/linux/fs.h"
2871struct super_block {
2872 struct list_head s_list ;
2873 dev_t s_dev ;
2874 unsigned char s_dirt ;
2875 unsigned char s_blocksize_bits ;
2876 unsigned long s_blocksize ;
2877 loff_t s_maxbytes ;
2878 struct file_system_type *s_type ;
2879 struct super_operations const *s_op ;
2880 struct dquot_operations const *dq_op ;
2881 struct quotactl_ops const *s_qcop ;
2882 struct export_operations const *s_export_op ;
2883 unsigned long s_flags ;
2884 unsigned long s_magic ;
2885 struct dentry *s_root ;
2886 struct rw_semaphore s_umount ;
2887 struct mutex s_lock ;
2888 int s_count ;
2889 atomic_t s_active ;
2890 void *s_security ;
2891 struct xattr_handler const **s_xattr ;
2892 struct list_head s_inodes ;
2893 struct hlist_bl_head s_anon ;
2894 struct list_head *s_files ;
2895 struct list_head s_mounts ;
2896 struct list_head s_dentry_lru ;
2897 int s_nr_dentry_unused ;
2898 spinlock_t s_inode_lru_lock __attribute__((__aligned__((1) << (6) ))) ;
2899 struct list_head s_inode_lru ;
2900 int s_nr_inodes_unused ;
2901 struct block_device *s_bdev ;
2902 struct backing_dev_info *s_bdi ;
2903 struct mtd_info *s_mtd ;
2904 struct hlist_node s_instances ;
2905 struct quota_info s_dquot ;
2906 int s_frozen ;
2907 wait_queue_head_t s_wait_unfrozen ;
2908 char s_id[32] ;
2909 u8 s_uuid[16] ;
2910 void *s_fs_info ;
2911 unsigned int s_max_links ;
2912 fmode_t s_mode ;
2913 u32 s_time_gran ;
2914 struct mutex s_vfs_rename_mutex ;
2915 char *s_subtype ;
2916 char *s_options ;
2917 struct dentry_operations const *s_d_op ;
2918 int cleancache_poolid ;
2919 struct shrinker s_shrink ;
2920 atomic_long_t s_remove_count ;
2921 int s_readonly_remount ;
2922};
2923#line 1567 "include/linux/fs.h"
2924struct fiemap_extent_info {
2925 unsigned int fi_flags ;
2926 unsigned int fi_extents_mapped ;
2927 unsigned int fi_extents_max ;
2928 struct fiemap_extent *fi_extents_start ;
2929};
2930#line 1609 "include/linux/fs.h"
2931struct file_operations {
2932 struct module *owner ;
2933 loff_t (*llseek)(struct file * , loff_t , int ) ;
2934 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ;
2935 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ;
2936 ssize_t (*aio_read)(struct kiocb * , struct iovec const * , unsigned long ,
2937 loff_t ) ;
2938 ssize_t (*aio_write)(struct kiocb * , struct iovec const * , unsigned long ,
2939 loff_t ) ;
2940 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int ,
2941 loff_t , u64 , unsigned int ) ) ;
2942 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
2943 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
2944 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
2945 int (*mmap)(struct file * , struct vm_area_struct * ) ;
2946 int (*open)(struct inode * , struct file * ) ;
2947 int (*flush)(struct file * , fl_owner_t id ) ;
2948 int (*release)(struct inode * , struct file * ) ;
2949 int (*fsync)(struct file * , loff_t , loff_t , int datasync ) ;
2950 int (*aio_fsync)(struct kiocb * , int datasync ) ;
2951 int (*fasync)(int , struct file * , int ) ;
2952 int (*lock)(struct file * , int , struct file_lock * ) ;
2953 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * ,
2954 int ) ;
2955 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
2956 unsigned long , unsigned long ) ;
2957 int (*check_flags)(int ) ;
2958 int (*flock)(struct file * , int , struct file_lock * ) ;
2959 ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t ,
2960 unsigned int ) ;
2961 ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t ,
2962 unsigned int ) ;
2963 int (*setlease)(struct file * , long , struct file_lock ** ) ;
2964 long (*fallocate)(struct file *file , int mode , loff_t offset , loff_t len ) ;
2965};
2966#line 1639 "include/linux/fs.h"
2967struct inode_operations {
2968 struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
2969 void *(*follow_link)(struct dentry * , struct nameidata * ) ;
2970 int (*permission)(struct inode * , int ) ;
2971 struct posix_acl *(*get_acl)(struct inode * , int ) ;
2972 int (*readlink)(struct dentry * , char * , int ) ;
2973 void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
2974 int (*create)(struct inode * , struct dentry * , umode_t , struct nameidata * ) ;
2975 int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
2976 int (*unlink)(struct inode * , struct dentry * ) ;
2977 int (*symlink)(struct inode * , struct dentry * , char const * ) ;
2978 int (*mkdir)(struct inode * , struct dentry * , umode_t ) ;
2979 int (*rmdir)(struct inode * , struct dentry * ) ;
2980 int (*mknod)(struct inode * , struct dentry * , umode_t , dev_t ) ;
2981 int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
2982 void (*truncate)(struct inode * ) ;
2983 int (*setattr)(struct dentry * , struct iattr * ) ;
2984 int (*getattr)(struct vfsmount *mnt , struct dentry * , struct kstat * ) ;
2985 int (*setxattr)(struct dentry * , char const * , void const * , size_t , int ) ;
2986 ssize_t (*getxattr)(struct dentry * , char const * , void * , size_t ) ;
2987 ssize_t (*listxattr)(struct dentry * , char * , size_t ) ;
2988 int (*removexattr)(struct dentry * , char const * ) ;
2989 void (*truncate_range)(struct inode * , loff_t , loff_t ) ;
2990 int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 start , u64 len ) ;
2991} __attribute__((__aligned__((1) << (6) ))) ;
2992#line 1669
2993struct seq_file;
2994#line 1684 "include/linux/fs.h"
2995struct super_operations {
2996 struct inode *(*alloc_inode)(struct super_block *sb ) ;
2997 void (*destroy_inode)(struct inode * ) ;
2998 void (*dirty_inode)(struct inode * , int flags ) ;
2999 int (*write_inode)(struct inode * , struct writeback_control *wbc ) ;
3000 int (*drop_inode)(struct inode * ) ;
3001 void (*evict_inode)(struct inode * ) ;
3002 void (*put_super)(struct super_block * ) ;
3003 void (*write_super)(struct super_block * ) ;
3004 int (*sync_fs)(struct super_block *sb , int wait ) ;
3005 int (*freeze_fs)(struct super_block * ) ;
3006 int (*unfreeze_fs)(struct super_block * ) ;
3007 int (*statfs)(struct dentry * , struct kstatfs * ) ;
3008 int (*remount_fs)(struct super_block * , int * , char * ) ;
3009 void (*umount_begin)(struct super_block * ) ;
3010 int (*show_options)(struct seq_file * , struct dentry * ) ;
3011 int (*show_devname)(struct seq_file * , struct dentry * ) ;
3012 int (*show_path)(struct seq_file * , struct dentry * ) ;
3013 int (*show_stats)(struct seq_file * , struct dentry * ) ;
3014 ssize_t (*quota_read)(struct super_block * , int , char * , size_t , loff_t ) ;
3015 ssize_t (*quota_write)(struct super_block * , int , char const * , size_t ,
3016 loff_t ) ;
3017 int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t ) ;
3018 int (*nr_cached_objects)(struct super_block * ) ;
3019 void (*free_cached_objects)(struct super_block * , int ) ;
3020};
3021#line 1835 "include/linux/fs.h"
3022struct file_system_type {
3023 char const *name ;
3024 int fs_flags ;
3025 struct dentry *(*mount)(struct file_system_type * , int , char const * , void * ) ;
3026 void (*kill_sb)(struct super_block * ) ;
3027 struct module *owner ;
3028 struct file_system_type *next ;
3029 struct hlist_head fs_supers ;
3030 struct lock_class_key s_lock_key ;
3031 struct lock_class_key s_umount_key ;
3032 struct lock_class_key s_vfs_rename_key ;
3033 struct lock_class_key i_lock_key ;
3034 struct lock_class_key i_mutex_key ;
3035 struct lock_class_key i_mutex_dir_key ;
3036};
3037#line 11 "include/linux/seq_file.h"
3038struct seq_operations;
3039#line 12
3040struct file;
3041#line 13
3042struct path;
3043#line 14
3044struct inode;
3045#line 15
3046struct dentry;
3047#line 17 "include/linux/seq_file.h"
3048struct seq_file {
3049 char *buf ;
3050 size_t size ;
3051 size_t from ;
3052 size_t count ;
3053 loff_t index ;
3054 loff_t read_pos ;
3055 u64 version ;
3056 struct mutex lock ;
3057 struct seq_operations const *op ;
3058 int poll_event ;
3059 void *private ;
3060};
3061#line 31 "include/linux/seq_file.h"
3062struct seq_operations {
3063 void *(*start)(struct seq_file *m , loff_t *pos ) ;
3064 void (*stop)(struct seq_file *m , void *v ) ;
3065 void *(*next)(struct seq_file *m , void *v , loff_t *pos ) ;
3066 int (*show)(struct seq_file *m , void *v ) ;
3067};
3068#line 23 "include/linux/debugfs.h"
3069struct file_operations;
3070#line 32 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/hypervisor.h"
3071struct hypervisor_x86 {
3072 char const *name ;
3073 bool (*detect)(void) ;
3074 void (*set_cpu_features)(struct cpuinfo_x86 * ) ;
3075 void (*init_platform)(void) ;
3076};
3077#line 152 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3078struct vmballoon_stats {
3079 unsigned int timer ;
3080 unsigned int alloc ;
3081 unsigned int alloc_fail ;
3082 unsigned int sleep_alloc ;
3083 unsigned int sleep_alloc_fail ;
3084 unsigned int refused_alloc ;
3085 unsigned int refused_free ;
3086 unsigned int free ;
3087 unsigned int lock ;
3088 unsigned int lock_fail ;
3089 unsigned int unlock ;
3090 unsigned int unlock_fail ;
3091 unsigned int target ;
3092 unsigned int target_fail ;
3093 unsigned int start ;
3094 unsigned int start_fail ;
3095 unsigned int guest_type ;
3096 unsigned int guest_type_fail ;
3097};
3098#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3099struct vmballoon {
3100 struct list_head pages ;
3101 struct list_head refused_pages ;
3102 unsigned int n_refused_pages ;
3103 unsigned int size ;
3104 unsigned int target ;
3105 bool reset_required ;
3106 unsigned int rate_alloc ;
3107 unsigned int rate_free ;
3108 unsigned int slow_allocation_cycles ;
3109 struct vmballoon_stats stats ;
3110 struct dentry *dbg_entry ;
3111 struct sysinfo sysinfo ;
3112 struct delayed_work dwork ;
3113};
3114#line 1 "<compiler builtins>"
3115long __builtin_expect(long val , long res ) ;
3116#line 100 "include/linux/printk.h"
3117extern int ( printk)(char const *fmt , ...) ;
3118#line 44 "include/linux/dynamic_debug.h"
3119extern int ( __dynamic_pr_debug)(struct _ddebug *descriptor ,
3120 char const *fmt , ...) ;
3121#line 147 "include/linux/kernel.h"
3122extern void __might_sleep(char const *file , int line , int preempt_offset ) ;
3123#line 27 "include/linux/err.h"
3124__inline static long __attribute__((__warn_unused_result__)) PTR_ERR(void const *ptr ) __attribute__((__no_instrument_function__)) ;
3125#line 27 "include/linux/err.h"
3126__inline static long __attribute__((__warn_unused_result__)) PTR_ERR(void const *ptr )
3127{
3128
3129 {
3130#line 29
3131 return ((long )ptr);
3132}
3133}
3134#line 32
3135__inline static long __attribute__((__warn_unused_result__)) IS_ERR(void const *ptr ) __attribute__((__no_instrument_function__)) ;
3136#line 32 "include/linux/err.h"
3137__inline static long __attribute__((__warn_unused_result__)) IS_ERR(void const *ptr )
3138{ long tmp ;
3139 unsigned long __cil_tmp3 ;
3140 int __cil_tmp4 ;
3141 int __cil_tmp5 ;
3142 int __cil_tmp6 ;
3143 long __cil_tmp7 ;
3144
3145 {
3146 {
3147#line 34
3148 __cil_tmp3 = (unsigned long )ptr;
3149#line 34
3150 __cil_tmp4 = __cil_tmp3 >= 0xfffffffffffff001UL;
3151#line 34
3152 __cil_tmp5 = ! __cil_tmp4;
3153#line 34
3154 __cil_tmp6 = ! __cil_tmp5;
3155#line 34
3156 __cil_tmp7 = (long )__cil_tmp6;
3157#line 34
3158 tmp = __builtin_expect(__cil_tmp7, 0L);
3159 }
3160#line 34
3161 return (tmp);
3162}
3163}
3164#line 24 "include/linux/list.h"
3165__inline static void INIT_LIST_HEAD(struct list_head *list ) __attribute__((__no_instrument_function__)) ;
3166#line 24 "include/linux/list.h"
3167__inline static void INIT_LIST_HEAD(struct list_head *list )
3168{ unsigned long __cil_tmp2 ;
3169 unsigned long __cil_tmp3 ;
3170
3171 {
3172#line 26
3173 *((struct list_head **)list) = list;
3174#line 27
3175 __cil_tmp2 = (unsigned long )list;
3176#line 27
3177 __cil_tmp3 = __cil_tmp2 + 8;
3178#line 27
3179 *((struct list_head **)__cil_tmp3) = list;
3180#line 28
3181 return;
3182}
3183}
3184#line 47
3185extern void __list_add(struct list_head *new , struct list_head *prev , struct list_head *next ) ;
3186#line 60
3187__inline static void list_add(struct list_head *new , struct list_head *head ) __attribute__((__no_instrument_function__)) ;
3188#line 60 "include/linux/list.h"
3189__inline static void list_add(struct list_head *new , struct list_head *head )
3190{ struct list_head *__cil_tmp3 ;
3191
3192 {
3193 {
3194#line 62
3195 __cil_tmp3 = *((struct list_head **)head);
3196#line 62
3197 __list_add(new, head, __cil_tmp3);
3198 }
3199#line 63
3200 return;
3201}
3202}
3203#line 112
3204extern void list_del(struct list_head *entry ) ;
3205#line 152 "include/linux/mutex.h"
3206void mutex_lock(struct mutex *lock ) ;
3207#line 153
3208int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
3209#line 154
3210int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
3211#line 168
3212int mutex_trylock(struct mutex *lock ) ;
3213#line 169
3214void mutex_unlock(struct mutex *lock ) ;
3215#line 170
3216int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
3217#line 91 "include/linux/timer.h"
3218extern void init_timer_key(struct timer_list *timer , char const *name , struct lock_class_key *key ) ;
3219#line 295
3220extern unsigned long round_jiffies_relative(unsigned long j ) ;
3221#line 97 "include/linux/workqueue.h"
3222__inline static struct delayed_work *to_delayed_work(struct work_struct *work ) __attribute__((__no_instrument_function__)) ;
3223#line 97 "include/linux/workqueue.h"
3224__inline static struct delayed_work *to_delayed_work(struct work_struct *work )
3225{ struct work_struct const *__mptr ;
3226 struct delayed_work *__cil_tmp3 ;
3227 struct work_struct *__cil_tmp4 ;
3228 unsigned int __cil_tmp5 ;
3229 char *__cil_tmp6 ;
3230 char *__cil_tmp7 ;
3231
3232 {
3233#line 99
3234 __mptr = (struct work_struct const *)work;
3235 {
3236#line 99
3237 __cil_tmp3 = (struct delayed_work *)0;
3238#line 99
3239 __cil_tmp4 = (struct work_struct *)__cil_tmp3;
3240#line 99
3241 __cil_tmp5 = (unsigned int )__cil_tmp4;
3242#line 99
3243 __cil_tmp6 = (char *)__mptr;
3244#line 99
3245 __cil_tmp7 = __cil_tmp6 - __cil_tmp5;
3246#line 99
3247 return ((struct delayed_work *)__cil_tmp7);
3248 }
3249}
3250}
3251#line 156
3252extern void __init_work(struct work_struct *work , int onstack ) ;
3253#line 300
3254extern struct workqueue_struct *system_freezable_wq ;
3255#line 371
3256extern int queue_delayed_work(struct workqueue_struct *wq , struct delayed_work *work ,
3257 unsigned long delay ) ;
3258#line 396
3259extern bool cancel_delayed_work_sync(struct delayed_work *dwork ) ;
3260#line 324 "include/linux/gfp.h"
3261extern struct page *alloc_pages_current(gfp_t gfp_mask , unsigned int order ) ;
3262#line 326
3263__inline static struct page *alloc_pages(gfp_t gfp_mask , unsigned int order ) __attribute__((__no_instrument_function__)) ;
3264#line 326 "include/linux/gfp.h"
3265__inline static struct page *alloc_pages(gfp_t gfp_mask , unsigned int order )
3266{ struct page *tmp ;
3267
3268 {
3269 {
3270#line 329
3271 tmp = alloc_pages_current(gfp_mask, order);
3272 }
3273#line 329
3274 return (tmp);
3275}
3276}
3277#line 360
3278extern void __free_pages(struct page *page , unsigned int order ) ;
3279#line 1328 "include/linux/mm.h"
3280extern void si_meminfo(struct sysinfo *val ) ;
3281#line 2626 "include/linux/sched.h"
3282extern int _cond_resched(void) ;
3283#line 26 "include/linux/export.h"
3284extern struct module __this_module ;
3285#line 67 "include/linux/module.h"
3286int init_module(void) ;
3287#line 68
3288void cleanup_module(void) ;
3289#line 80 "include/linux/seq_file.h"
3290extern ssize_t seq_read(struct file * , char * , size_t , loff_t * ) ;
3291#line 81
3292extern loff_t seq_lseek(struct file * , loff_t , int ) ;
3293#line 88
3294extern int ( seq_printf)(struct seq_file * , char const *
3295 , ...) ;
3296#line 120
3297extern int single_open(struct file * , int (*)(struct seq_file * , void * ) , void * ) ;
3298#line 121
3299extern int single_release(struct inode * , struct file * ) ;
3300#line 49 "include/linux/debugfs.h"
3301extern struct dentry *debugfs_create_file(char const *name , umode_t mode , struct dentry *parent ,
3302 void *data , struct file_operations const *fops ) ;
3303#line 58
3304extern void debugfs_remove(struct dentry *dentry ) ;
3305#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/hypervisor.h"
3306extern struct hypervisor_x86 const *x86_hyper ;
3307#line 49
3308extern struct hypervisor_x86 const x86_hyper_vmware ;
3309#line 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3310static char const __mod_author47[20] __attribute__((__used__, __unused__, __section__(".modinfo"),
3311__aligned__(1))) =
3312#line 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3313 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
3314 (char const )'o', (char const )'r', (char const )'=', (char const )'V',
3315 (char const )'M', (char const )'w', (char const )'a', (char const )'r',
3316 (char const )'e', (char const )',', (char const )' ', (char const )'I',
3317 (char const )'n', (char const )'c', (char const )'.', (char const )'\000'};
3318#line 48 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3319static char const __mod_description48[51] __attribute__((__used__, __unused__,
3320__section__(".modinfo"), __aligned__(1))) =
3321#line 48
3322 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
3323 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
3324 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
3325 (char const )'V', (char const )'M', (char const )'w', (char const )'a',
3326 (char const )'r', (char const )'e', (char const )' ', (char const )'M',
3327 (char const )'e', (char const )'m', (char const )'o', (char const )'r',
3328 (char const )'y', (char const )' ', (char const )'C', (char const )'o',
3329 (char const )'n', (char const )'t', (char const )'r', (char const )'o',
3330 (char const )'l', (char const )' ', (char const )'(', (char const )'B',
3331 (char const )'a', (char const )'l', (char const )'l', (char const )'o',
3332 (char const )'o', (char const )'n', (char const )')', (char const )' ',
3333 (char const )'D', (char const )'r', (char const )'i', (char const )'v',
3334 (char const )'e', (char const )'r', (char const )'\000'};
3335#line 49 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3336static char const __mod_version49[18] __attribute__((__used__, __unused__, __section__(".modinfo"),
3337__aligned__(1))) =
3338#line 49
3339 { (char const )'v', (char const )'e', (char const )'r', (char const )'s',
3340 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
3341 (char const )'1', (char const )'.', (char const )'2', (char const )'.',
3342 (char const )'1', (char const )'.', (char const )'3', (char const )'-',
3343 (char const )'k', (char const )'\000'};
3344#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3345static char const __mod_alias50[25] __attribute__((__used__, __unused__, __section__(".modinfo"),
3346__aligned__(1))) =
3347#line 50
3348 { (char const )'a', (char const )'l', (char const )'i', (char const )'a',
3349 (char const )'s', (char const )'=', (char const )'d', (char const )'m',
3350 (char const )'i', (char const )':', (char const )'*', (char const )':',
3351 (char const )'s', (char const )'v', (char const )'n', (char const )'V',
3352 (char const )'M', (char const )'w', (char const )'a', (char const )'r',
3353 (char const )'e', (char const )'*', (char const )':', (char const )'*',
3354 (char const )'\000'};
3355#line 51 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3356static char const __mod_alias51[22] __attribute__((__used__, __unused__, __section__(".modinfo"),
3357__aligned__(1))) =
3358#line 51
3359 { (char const )'a', (char const )'l', (char const )'i', (char const )'a',
3360 (char const )'s', (char const )'=', (char const )'v', (char const )'m',
3361 (char const )'w', (char const )'a', (char const )'r', (char const )'e',
3362 (char const )'_', (char const )'v', (char const )'m', (char const )'m',
3363 (char const )'e', (char const )'m', (char const )'c', (char const )'t',
3364 (char const )'l', (char const )'\000'};
3365#line 52 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3366static char const __mod_license52[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
3367__aligned__(1))) =
3368#line 52
3369 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
3370 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
3371 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
3372#line 218 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3373static struct vmballoon balloon ;
3374#line 234
3375static bool vmballoon_send_start(struct vmballoon *b ) ;
3376#line 234 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3377static struct _ddebug __attribute__((__aligned__(8))) descriptor __attribute__((__used__,
3378__section__("__verbose"))) = {"vmw_balloon", "vmballoon_send_start", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c",
3379 "%s - failed, hv returns %ld\n", 234U, 0U};
3380#line 224 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3381static bool vmballoon_send_start(struct vmballoon *b )
3382{ unsigned long status ;
3383 unsigned long dummy ;
3384 unsigned long __stat ;
3385 unsigned long __dummy1 ;
3386 unsigned long __dummy2 ;
3387 long tmp___7 ;
3388 unsigned long __cil_tmp8 ;
3389 unsigned long __cil_tmp9 ;
3390 unsigned long __cil_tmp10 ;
3391 unsigned long __cil_tmp11 ;
3392 unsigned long __cil_tmp12 ;
3393 unsigned long __cil_tmp13 ;
3394 unsigned int __cil_tmp14 ;
3395 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp15 ;
3396 unsigned int __cil_tmp16 ;
3397 unsigned int __cil_tmp17 ;
3398 int __cil_tmp18 ;
3399 int __cil_tmp19 ;
3400 long __cil_tmp20 ;
3401 unsigned long __cil_tmp21 ;
3402 unsigned long __cil_tmp22 ;
3403 unsigned long __cil_tmp23 ;
3404 unsigned long __cil_tmp24 ;
3405 unsigned long __cil_tmp25 ;
3406 unsigned long __cil_tmp26 ;
3407 unsigned int __cil_tmp27 ;
3408
3409 {
3410#line 228
3411 __cil_tmp8 = 60 + 56;
3412#line 228
3413 __cil_tmp9 = (unsigned long )b;
3414#line 228
3415 __cil_tmp10 = __cil_tmp9 + __cil_tmp8;
3416#line 228
3417 __cil_tmp11 = 60 + 56;
3418#line 228
3419 __cil_tmp12 = (unsigned long )b;
3420#line 228
3421 __cil_tmp13 = __cil_tmp12 + __cil_tmp11;
3422#line 228
3423 __cil_tmp14 = *((unsigned int *)__cil_tmp13);
3424#line 228
3425 *((unsigned int *)__cil_tmp10) = __cil_tmp14 + 1U;
3426#line 230
3427 __asm__ volatile ("inl (%%dx)": "=a" (__stat), "=c" (__dummy1), "=d" (__dummy2),
3428 "=b" (dummy): "0" (1164733807), "1" (0), "2" (22128), "3" (2): "memory");
3429#line 230
3430 dummy = dummy & 0xffffffffffffffffUL;
3431#line 230
3432 status = __stat & 0xffffffffffffffffUL;
3433#line 231
3434 if (status == 0UL) {
3435#line 232
3436 return ((bool )1);
3437 } else {
3438
3439 }
3440 {
3441#line 234
3442 while (1) {
3443 while_continue: ;
3444 {
3445#line 234
3446 __cil_tmp15 = & descriptor;
3447#line 234
3448 __cil_tmp16 = __cil_tmp15->flags;
3449#line 234
3450 __cil_tmp17 = __cil_tmp16 & 1U;
3451#line 234
3452 __cil_tmp18 = ! __cil_tmp17;
3453#line 234
3454 __cil_tmp19 = ! __cil_tmp18;
3455#line 234
3456 __cil_tmp20 = (long )__cil_tmp19;
3457#line 234
3458 tmp___7 = __builtin_expect(__cil_tmp20, 0L);
3459 }
3460#line 234
3461 if (tmp___7) {
3462 {
3463#line 234
3464 __dynamic_pr_debug(& descriptor, "vmw_balloon: %s - failed, hv returns %ld\n",
3465 "vmballoon_send_start", status);
3466 }
3467 } else {
3468
3469 }
3470#line 234
3471 goto while_break;
3472 }
3473 while_break: ;
3474 }
3475#line 235
3476 __cil_tmp21 = 60 + 60;
3477#line 235
3478 __cil_tmp22 = (unsigned long )b;
3479#line 235
3480 __cil_tmp23 = __cil_tmp22 + __cil_tmp21;
3481#line 235
3482 __cil_tmp24 = 60 + 60;
3483#line 235
3484 __cil_tmp25 = (unsigned long )b;
3485#line 235
3486 __cil_tmp26 = __cil_tmp25 + __cil_tmp24;
3487#line 235
3488 __cil_tmp27 = *((unsigned int *)__cil_tmp26);
3489#line 235
3490 *((unsigned int *)__cil_tmp23) = __cil_tmp27 + 1U;
3491#line 236
3492 return ((bool )0);
3493}
3494}
3495#line 239 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3496static bool vmballoon_check_status(struct vmballoon *b , unsigned long status )
3497{ unsigned long __cil_tmp3 ;
3498 unsigned long __cil_tmp4 ;
3499
3500 {
3501#line 242
3502 if ((int )status == 0) {
3503#line 242
3504 goto case_0;
3505 } else
3506#line 245
3507 if ((int )status == 7) {
3508#line 245
3509 goto case_7;
3510 } else {
3511 {
3512#line 249
3513 goto switch_default;
3514#line 241
3515 if (0) {
3516 case_0:
3517#line 243
3518 return ((bool )1);
3519 case_7:
3520#line 246
3521 __cil_tmp3 = (unsigned long )b;
3522#line 246
3523 __cil_tmp4 = __cil_tmp3 + 44;
3524#line 246
3525 *((bool *)__cil_tmp4) = (bool )1;
3526 switch_default:
3527#line 250
3528 return ((bool )0);
3529 } else {
3530 switch_break: ;
3531 }
3532 }
3533 }
3534}
3535}
3536#line 271
3537static bool vmballoon_send_guest_id(struct vmballoon *b ) ;
3538#line 271 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3539static struct _ddebug __attribute__((__aligned__(8))) descriptor___0 __attribute__((__used__,
3540__section__("__verbose"))) = {"vmw_balloon", "vmballoon_send_guest_id", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c",
3541 "%s - failed, hv returns %ld\n", 271U, 0U};
3542#line 260 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3543static bool vmballoon_send_guest_id(struct vmballoon *b )
3544{ unsigned long status ;
3545 unsigned long dummy ;
3546 unsigned long __stat ;
3547 unsigned long __dummy1 ;
3548 unsigned long __dummy2 ;
3549 bool tmp___7 ;
3550 long tmp___8 ;
3551 unsigned long __cil_tmp9 ;
3552 unsigned long __cil_tmp10 ;
3553 unsigned long __cil_tmp11 ;
3554 unsigned long __cil_tmp12 ;
3555 unsigned long __cil_tmp13 ;
3556 unsigned long __cil_tmp14 ;
3557 unsigned int __cil_tmp15 ;
3558 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp16 ;
3559 unsigned int __cil_tmp17 ;
3560 unsigned int __cil_tmp18 ;
3561 int __cil_tmp19 ;
3562 int __cil_tmp20 ;
3563 long __cil_tmp21 ;
3564 unsigned long __cil_tmp22 ;
3565 unsigned long __cil_tmp23 ;
3566 unsigned long __cil_tmp24 ;
3567 unsigned long __cil_tmp25 ;
3568 unsigned long __cil_tmp26 ;
3569 unsigned long __cil_tmp27 ;
3570 unsigned int __cil_tmp28 ;
3571
3572 {
3573 {
3574#line 264
3575 __asm__ volatile ("inl (%%dx)": "=a" (__stat), "=c" (__dummy1), "=d" (__dummy2),
3576 "=b" (dummy): "0" (1164733807), "1" (4), "2" (22128), "3" (1): "memory");
3577#line 264
3578 dummy = dummy & 0xffffffffffffffffUL;
3579#line 264
3580 status = __stat & 0xffffffffffffffffUL;
3581#line 266
3582 __cil_tmp9 = 60 + 64;
3583#line 266
3584 __cil_tmp10 = (unsigned long )b;
3585#line 266
3586 __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
3587#line 266
3588 __cil_tmp12 = 60 + 64;
3589#line 266
3590 __cil_tmp13 = (unsigned long )b;
3591#line 266
3592 __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
3593#line 266
3594 __cil_tmp15 = *((unsigned int *)__cil_tmp14);
3595#line 266
3596 *((unsigned int *)__cil_tmp11) = __cil_tmp15 + 1U;
3597#line 268
3598 tmp___7 = vmballoon_check_status(b, status);
3599 }
3600#line 268
3601 if (tmp___7) {
3602#line 269
3603 return ((bool )1);
3604 } else {
3605
3606 }
3607 {
3608#line 271
3609 while (1) {
3610 while_continue: ;
3611 {
3612#line 271
3613 __cil_tmp16 = & descriptor___0;
3614#line 271
3615 __cil_tmp17 = __cil_tmp16->flags;
3616#line 271
3617 __cil_tmp18 = __cil_tmp17 & 1U;
3618#line 271
3619 __cil_tmp19 = ! __cil_tmp18;
3620#line 271
3621 __cil_tmp20 = ! __cil_tmp19;
3622#line 271
3623 __cil_tmp21 = (long )__cil_tmp20;
3624#line 271
3625 tmp___8 = __builtin_expect(__cil_tmp21, 0L);
3626 }
3627#line 271
3628 if (tmp___8) {
3629 {
3630#line 271
3631 __dynamic_pr_debug(& descriptor___0, "vmw_balloon: %s - failed, hv returns %ld\n",
3632 "vmballoon_send_guest_id", status);
3633 }
3634 } else {
3635
3636 }
3637#line 271
3638 goto while_break;
3639 }
3640 while_break: ;
3641 }
3642#line 272
3643 __cil_tmp22 = 60 + 68;
3644#line 272
3645 __cil_tmp23 = (unsigned long )b;
3646#line 272
3647 __cil_tmp24 = __cil_tmp23 + __cil_tmp22;
3648#line 272
3649 __cil_tmp25 = 60 + 68;
3650#line 272
3651 __cil_tmp26 = (unsigned long )b;
3652#line 272
3653 __cil_tmp27 = __cil_tmp26 + __cil_tmp25;
3654#line 272
3655 __cil_tmp28 = *((unsigned int *)__cil_tmp27);
3656#line 272
3657 *((unsigned int *)__cil_tmp24) = __cil_tmp28 + 1U;
3658#line 273
3659 return ((bool )0);
3660}
3661}
3662#line 308
3663static bool vmballoon_send_get_target(struct vmballoon *b , u32 *new_target ) ;
3664#line 308 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3665static struct _ddebug __attribute__((__aligned__(8))) descriptor___1 __attribute__((__used__,
3666__section__("__verbose"))) = {"vmw_balloon", "vmballoon_send_get_target", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c",
3667 "%s - failed, hv returns %ld\n", 308U, 0U};
3668#line 279 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3669static bool vmballoon_send_get_target(struct vmballoon *b , u32 *new_target )
3670{ unsigned long status ;
3671 unsigned long target ;
3672 unsigned long limit ;
3673 u32 limit32 ;
3674 unsigned long __stat ;
3675 unsigned long __dummy1 ;
3676 unsigned long __dummy2 ;
3677 bool tmp___7 ;
3678 long tmp___8 ;
3679 unsigned long __cil_tmp12 ;
3680 unsigned long __cil_tmp13 ;
3681 struct sysinfo *__cil_tmp14 ;
3682 unsigned long __cil_tmp15 ;
3683 unsigned long __cil_tmp16 ;
3684 unsigned long __cil_tmp17 ;
3685 unsigned long __cil_tmp18 ;
3686 unsigned long __cil_tmp19 ;
3687 unsigned long __cil_tmp20 ;
3688 unsigned long __cil_tmp21 ;
3689 unsigned long __cil_tmp22 ;
3690 unsigned long __cil_tmp23 ;
3691 unsigned long __cil_tmp24 ;
3692 unsigned int __cil_tmp25 ;
3693 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp26 ;
3694 unsigned int __cil_tmp27 ;
3695 unsigned int __cil_tmp28 ;
3696 int __cil_tmp29 ;
3697 int __cil_tmp30 ;
3698 long __cil_tmp31 ;
3699 unsigned long __cil_tmp32 ;
3700 unsigned long __cil_tmp33 ;
3701 unsigned long __cil_tmp34 ;
3702 unsigned long __cil_tmp35 ;
3703 unsigned long __cil_tmp36 ;
3704 unsigned long __cil_tmp37 ;
3705 unsigned int __cil_tmp38 ;
3706
3707 {
3708 {
3709#line 291
3710 __cil_tmp12 = (unsigned long )b;
3711#line 291
3712 __cil_tmp13 = __cil_tmp12 + 144;
3713#line 291
3714 __cil_tmp14 = (struct sysinfo *)__cil_tmp13;
3715#line 291
3716 si_meminfo(__cil_tmp14);
3717#line 292
3718 __cil_tmp15 = 144 + 32;
3719#line 292
3720 __cil_tmp16 = (unsigned long )b;
3721#line 292
3722 __cil_tmp17 = __cil_tmp16 + __cil_tmp15;
3723#line 292
3724 limit = *((__kernel_ulong_t *)__cil_tmp17);
3725#line 295
3726 limit32 = (u32 )limit;
3727 }
3728 {
3729#line 296
3730 __cil_tmp18 = (unsigned long )limit32;
3731#line 296
3732 if (limit != __cil_tmp18) {
3733#line 297
3734 return ((bool )0);
3735 } else {
3736
3737 }
3738 }
3739 {
3740#line 300
3741 __cil_tmp19 = 60 + 48;
3742#line 300
3743 __cil_tmp20 = (unsigned long )b;
3744#line 300
3745 __cil_tmp21 = __cil_tmp20 + __cil_tmp19;
3746#line 300
3747 __cil_tmp22 = 60 + 48;
3748#line 300
3749 __cil_tmp23 = (unsigned long )b;
3750#line 300
3751 __cil_tmp24 = __cil_tmp23 + __cil_tmp22;
3752#line 300
3753 __cil_tmp25 = *((unsigned int *)__cil_tmp24);
3754#line 300
3755 *((unsigned int *)__cil_tmp21) = __cil_tmp25 + 1U;
3756#line 302
3757 __asm__ volatile ("inl (%%dx)": "=a" (__stat), "=c" (__dummy1), "=d" (__dummy2),
3758 "=b" (target): "0" (1164733807), "1" (1), "2" (22128), "3" (limit): "memory");
3759#line 302
3760 target = target & 0xffffffffffffffffUL;
3761#line 302
3762 status = __stat & 0xffffffffffffffffUL;
3763#line 303
3764 tmp___7 = vmballoon_check_status(b, status);
3765 }
3766#line 303
3767 if (tmp___7) {
3768#line 304
3769 *new_target = (u32 )target;
3770#line 305
3771 return ((bool )1);
3772 } else {
3773
3774 }
3775 {
3776#line 308
3777 while (1) {
3778 while_continue: ;
3779 {
3780#line 308
3781 __cil_tmp26 = & descriptor___1;
3782#line 308
3783 __cil_tmp27 = __cil_tmp26->flags;
3784#line 308
3785 __cil_tmp28 = __cil_tmp27 & 1U;
3786#line 308
3787 __cil_tmp29 = ! __cil_tmp28;
3788#line 308
3789 __cil_tmp30 = ! __cil_tmp29;
3790#line 308
3791 __cil_tmp31 = (long )__cil_tmp30;
3792#line 308
3793 tmp___8 = __builtin_expect(__cil_tmp31, 0L);
3794 }
3795#line 308
3796 if (tmp___8) {
3797 {
3798#line 308
3799 __dynamic_pr_debug(& descriptor___1, "vmw_balloon: %s - failed, hv returns %ld\n",
3800 "vmballoon_send_get_target", status);
3801 }
3802 } else {
3803
3804 }
3805#line 308
3806 goto while_break;
3807 }
3808 while_break: ;
3809 }
3810#line 309
3811 __cil_tmp32 = 60 + 52;
3812#line 309
3813 __cil_tmp33 = (unsigned long )b;
3814#line 309
3815 __cil_tmp34 = __cil_tmp33 + __cil_tmp32;
3816#line 309
3817 __cil_tmp35 = 60 + 52;
3818#line 309
3819 __cil_tmp36 = (unsigned long )b;
3820#line 309
3821 __cil_tmp37 = __cil_tmp36 + __cil_tmp35;
3822#line 309
3823 __cil_tmp38 = *((unsigned int *)__cil_tmp37);
3824#line 309
3825 *((unsigned int *)__cil_tmp34) = __cil_tmp38 + 1U;
3826#line 310
3827 return ((bool )0);
3828}
3829}
3830#line 334
3831static int vmballoon_send_lock_page(struct vmballoon *b , unsigned long pfn , unsigned int *hv_status ) ;
3832#line 334 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3833static struct _ddebug __attribute__((__aligned__(8))) descriptor___2 __attribute__((__used__,
3834__section__("__verbose"))) = {"vmw_balloon", "vmballoon_send_lock_page", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c",
3835 "%s - ppn %lx, hv returns %ld\n", 334U, 0U};
3836#line 318 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3837static int vmballoon_send_lock_page(struct vmballoon *b , unsigned long pfn , unsigned int *hv_status )
3838{ unsigned long status ;
3839 unsigned long dummy ;
3840 u32 pfn32 ;
3841 unsigned long __stat ;
3842 unsigned long __dummy1 ;
3843 unsigned long __dummy2 ;
3844 bool tmp___7 ;
3845 long tmp___8 ;
3846 unsigned long __cil_tmp12 ;
3847 unsigned long __cil_tmp13 ;
3848 unsigned long __cil_tmp14 ;
3849 unsigned long __cil_tmp15 ;
3850 unsigned long __cil_tmp16 ;
3851 unsigned long __cil_tmp17 ;
3852 unsigned long __cil_tmp18 ;
3853 unsigned int __cil_tmp19 ;
3854 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp20 ;
3855 unsigned int __cil_tmp21 ;
3856 unsigned int __cil_tmp22 ;
3857 int __cil_tmp23 ;
3858 int __cil_tmp24 ;
3859 long __cil_tmp25 ;
3860 unsigned long __cil_tmp26 ;
3861 unsigned long __cil_tmp27 ;
3862 unsigned long __cil_tmp28 ;
3863 unsigned long __cil_tmp29 ;
3864 unsigned long __cil_tmp30 ;
3865 unsigned long __cil_tmp31 ;
3866 unsigned int __cil_tmp32 ;
3867
3868 {
3869#line 324
3870 pfn32 = (u32 )pfn;
3871 {
3872#line 325
3873 __cil_tmp12 = (unsigned long )pfn32;
3874#line 325
3875 if (__cil_tmp12 != pfn) {
3876#line 326
3877 return (-1);
3878 } else {
3879
3880 }
3881 }
3882 {
3883#line 328
3884 __cil_tmp13 = 60 + 32;
3885#line 328
3886 __cil_tmp14 = (unsigned long )b;
3887#line 328
3888 __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
3889#line 328
3890 __cil_tmp16 = 60 + 32;
3891#line 328
3892 __cil_tmp17 = (unsigned long )b;
3893#line 328
3894 __cil_tmp18 = __cil_tmp17 + __cil_tmp16;
3895#line 328
3896 __cil_tmp19 = *((unsigned int *)__cil_tmp18);
3897#line 328
3898 *((unsigned int *)__cil_tmp15) = __cil_tmp19 + 1U;
3899#line 330
3900 __asm__ volatile ("inl (%%dx)": "=a" (__stat), "=c" (__dummy1), "=d" (__dummy2),
3901 "=b" (dummy): "0" (1164733807), "1" (2), "2" (22128), "3" (pfn): "memory");
3902#line 330
3903 dummy = dummy & 0xffffffffffffffffUL;
3904#line 330
3905 status = __stat & 0xffffffffffffffffUL;
3906#line 330
3907 *hv_status = (unsigned int )status;
3908#line 331
3909 tmp___7 = vmballoon_check_status(b, status);
3910 }
3911#line 331
3912 if (tmp___7) {
3913#line 332
3914 return (0);
3915 } else {
3916
3917 }
3918 {
3919#line 334
3920 while (1) {
3921 while_continue: ;
3922 {
3923#line 334
3924 __cil_tmp20 = & descriptor___2;
3925#line 334
3926 __cil_tmp21 = __cil_tmp20->flags;
3927#line 334
3928 __cil_tmp22 = __cil_tmp21 & 1U;
3929#line 334
3930 __cil_tmp23 = ! __cil_tmp22;
3931#line 334
3932 __cil_tmp24 = ! __cil_tmp23;
3933#line 334
3934 __cil_tmp25 = (long )__cil_tmp24;
3935#line 334
3936 tmp___8 = __builtin_expect(__cil_tmp25, 0L);
3937 }
3938#line 334
3939 if (tmp___8) {
3940 {
3941#line 334
3942 __dynamic_pr_debug(& descriptor___2, "vmw_balloon: %s - ppn %lx, hv returns %ld\n",
3943 "vmballoon_send_lock_page", pfn, status);
3944 }
3945 } else {
3946
3947 }
3948#line 334
3949 goto while_break;
3950 }
3951 while_break: ;
3952 }
3953#line 335
3954 __cil_tmp26 = 60 + 36;
3955#line 335
3956 __cil_tmp27 = (unsigned long )b;
3957#line 335
3958 __cil_tmp28 = __cil_tmp27 + __cil_tmp26;
3959#line 335
3960 __cil_tmp29 = 60 + 36;
3961#line 335
3962 __cil_tmp30 = (unsigned long )b;
3963#line 335
3964 __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
3965#line 335
3966 __cil_tmp32 = *((unsigned int *)__cil_tmp31);
3967#line 335
3968 *((unsigned int *)__cil_tmp28) = __cil_tmp32 + 1U;
3969#line 336
3970 return (1);
3971}
3972}
3973#line 358
3974static bool vmballoon_send_unlock_page(struct vmballoon *b , unsigned long pfn ) ;
3975#line 358 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3976static struct _ddebug __attribute__((__aligned__(8))) descriptor___3 __attribute__((__used__,
3977__section__("__verbose"))) = {"vmw_balloon", "vmballoon_send_unlock_page", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c",
3978 "%s - ppn %lx, hv returns %ld\n", 358U, 0U};
3979#line 343 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
3980static bool vmballoon_send_unlock_page(struct vmballoon *b , unsigned long pfn )
3981{ unsigned long status ;
3982 unsigned long dummy ;
3983 u32 pfn32 ;
3984 unsigned long __stat ;
3985 unsigned long __dummy1 ;
3986 unsigned long __dummy2 ;
3987 bool tmp___7 ;
3988 long tmp___8 ;
3989 unsigned long __cil_tmp11 ;
3990 unsigned long __cil_tmp12 ;
3991 unsigned long __cil_tmp13 ;
3992 unsigned long __cil_tmp14 ;
3993 unsigned long __cil_tmp15 ;
3994 unsigned long __cil_tmp16 ;
3995 unsigned long __cil_tmp17 ;
3996 unsigned int __cil_tmp18 ;
3997 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp19 ;
3998 unsigned int __cil_tmp20 ;
3999 unsigned int __cil_tmp21 ;
4000 int __cil_tmp22 ;
4001 int __cil_tmp23 ;
4002 long __cil_tmp24 ;
4003 unsigned long __cil_tmp25 ;
4004 unsigned long __cil_tmp26 ;
4005 unsigned long __cil_tmp27 ;
4006 unsigned long __cil_tmp28 ;
4007 unsigned long __cil_tmp29 ;
4008 unsigned long __cil_tmp30 ;
4009 unsigned int __cil_tmp31 ;
4010
4011 {
4012#line 348
4013 pfn32 = (u32 )pfn;
4014 {
4015#line 349
4016 __cil_tmp11 = (unsigned long )pfn32;
4017#line 349
4018 if (__cil_tmp11 != pfn) {
4019#line 350
4020 return ((bool )0);
4021 } else {
4022
4023 }
4024 }
4025 {
4026#line 352
4027 __cil_tmp12 = 60 + 40;
4028#line 352
4029 __cil_tmp13 = (unsigned long )b;
4030#line 352
4031 __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
4032#line 352
4033 __cil_tmp15 = 60 + 40;
4034#line 352
4035 __cil_tmp16 = (unsigned long )b;
4036#line 352
4037 __cil_tmp17 = __cil_tmp16 + __cil_tmp15;
4038#line 352
4039 __cil_tmp18 = *((unsigned int *)__cil_tmp17);
4040#line 352
4041 *((unsigned int *)__cil_tmp14) = __cil_tmp18 + 1U;
4042#line 354
4043 __asm__ volatile ("inl (%%dx)": "=a" (__stat), "=c" (__dummy1), "=d" (__dummy2),
4044 "=b" (dummy): "0" (1164733807), "1" (3), "2" (22128), "3" (pfn): "memory");
4045#line 354
4046 dummy = dummy & 0xffffffffffffffffUL;
4047#line 354
4048 status = __stat & 0xffffffffffffffffUL;
4049#line 355
4050 tmp___7 = vmballoon_check_status(b, status);
4051 }
4052#line 355
4053 if (tmp___7) {
4054#line 356
4055 return ((bool )1);
4056 } else {
4057
4058 }
4059 {
4060#line 358
4061 while (1) {
4062 while_continue: ;
4063 {
4064#line 358
4065 __cil_tmp19 = & descriptor___3;
4066#line 358
4067 __cil_tmp20 = __cil_tmp19->flags;
4068#line 358
4069 __cil_tmp21 = __cil_tmp20 & 1U;
4070#line 358
4071 __cil_tmp22 = ! __cil_tmp21;
4072#line 358
4073 __cil_tmp23 = ! __cil_tmp22;
4074#line 358
4075 __cil_tmp24 = (long )__cil_tmp23;
4076#line 358
4077 tmp___8 = __builtin_expect(__cil_tmp24, 0L);
4078 }
4079#line 358
4080 if (tmp___8) {
4081 {
4082#line 358
4083 __dynamic_pr_debug(& descriptor___3, "vmw_balloon: %s - ppn %lx, hv returns %ld\n",
4084 "vmballoon_send_unlock_page", pfn, status);
4085 }
4086 } else {
4087
4088 }
4089#line 358
4090 goto while_break;
4091 }
4092 while_break: ;
4093 }
4094#line 359
4095 __cil_tmp25 = 60 + 44;
4096#line 359
4097 __cil_tmp26 = (unsigned long )b;
4098#line 359
4099 __cil_tmp27 = __cil_tmp26 + __cil_tmp25;
4100#line 359
4101 __cil_tmp28 = 60 + 44;
4102#line 359
4103 __cil_tmp29 = (unsigned long )b;
4104#line 359
4105 __cil_tmp30 = __cil_tmp29 + __cil_tmp28;
4106#line 359
4107 __cil_tmp31 = *((unsigned int *)__cil_tmp30);
4108#line 359
4109 *((unsigned int *)__cil_tmp27) = __cil_tmp31 + 1U;
4110#line 360
4111 return ((bool )0);
4112}
4113}
4114#line 369 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
4115static void vmballoon_pop(struct vmballoon *b )
4116{ struct page *page ;
4117 struct page *next ;
4118 unsigned int count ;
4119 struct list_head const *__mptr ;
4120 struct list_head const *__mptr___0 ;
4121 struct list_head const *__mptr___1 ;
4122 struct list_head *__cil_tmp8 ;
4123 struct page *__cil_tmp9 ;
4124 unsigned long __cil_tmp10 ;
4125 unsigned long __cil_tmp11 ;
4126 struct list_head *__cil_tmp12 ;
4127 unsigned int __cil_tmp13 ;
4128 char *__cil_tmp14 ;
4129 char *__cil_tmp15 ;
4130 unsigned long __cil_tmp16 ;
4131 unsigned long __cil_tmp17 ;
4132 struct list_head *__cil_tmp18 ;
4133 struct page *__cil_tmp19 ;
4134 unsigned long __cil_tmp20 ;
4135 unsigned long __cil_tmp21 ;
4136 struct list_head *__cil_tmp22 ;
4137 unsigned int __cil_tmp23 ;
4138 char *__cil_tmp24 ;
4139 char *__cil_tmp25 ;
4140 struct list_head *__cil_tmp26 ;
4141 unsigned long __cil_tmp27 ;
4142 unsigned long __cil_tmp28 ;
4143 unsigned long __cil_tmp29 ;
4144 struct list_head *__cil_tmp30 ;
4145 unsigned long __cil_tmp31 ;
4146 unsigned long __cil_tmp32 ;
4147 unsigned long __cil_tmp33 ;
4148 struct list_head *__cil_tmp34 ;
4149 unsigned long __cil_tmp35 ;
4150 unsigned long __cil_tmp36 ;
4151 unsigned long __cil_tmp37 ;
4152 unsigned long __cil_tmp38 ;
4153 unsigned long __cil_tmp39 ;
4154 unsigned long __cil_tmp40 ;
4155 unsigned int __cil_tmp41 ;
4156 unsigned long __cil_tmp42 ;
4157 unsigned long __cil_tmp43 ;
4158 unsigned long __cil_tmp44 ;
4159 unsigned long __cil_tmp45 ;
4160 unsigned int __cil_tmp46 ;
4161 unsigned long __cil_tmp47 ;
4162 unsigned long __cil_tmp48 ;
4163 unsigned int __cil_tmp49 ;
4164 unsigned long __cil_tmp50 ;
4165 unsigned long __cil_tmp51 ;
4166 struct list_head *__cil_tmp52 ;
4167 struct page *__cil_tmp53 ;
4168 unsigned long __cil_tmp54 ;
4169 unsigned long __cil_tmp55 ;
4170 struct list_head *__cil_tmp56 ;
4171 unsigned int __cil_tmp57 ;
4172 char *__cil_tmp58 ;
4173 char *__cil_tmp59 ;
4174
4175 {
4176#line 372
4177 count = 0U;
4178#line 374
4179 __cil_tmp8 = *((struct list_head **)b);
4180#line 374
4181 __mptr = (struct list_head const *)__cil_tmp8;
4182#line 374
4183 __cil_tmp9 = (struct page *)0;
4184#line 374
4185 __cil_tmp10 = (unsigned long )__cil_tmp9;
4186#line 374
4187 __cil_tmp11 = __cil_tmp10 + 32;
4188#line 374
4189 __cil_tmp12 = (struct list_head *)__cil_tmp11;
4190#line 374
4191 __cil_tmp13 = (unsigned int )__cil_tmp12;
4192#line 374
4193 __cil_tmp14 = (char *)__mptr;
4194#line 374
4195 __cil_tmp15 = __cil_tmp14 - __cil_tmp13;
4196#line 374
4197 page = (struct page *)__cil_tmp15;
4198#line 374
4199 __cil_tmp16 = (unsigned long )page;
4200#line 374
4201 __cil_tmp17 = __cil_tmp16 + 32;
4202#line 374
4203 __cil_tmp18 = *((struct list_head **)__cil_tmp17);
4204#line 374
4205 __mptr___0 = (struct list_head const *)__cil_tmp18;
4206#line 374
4207 __cil_tmp19 = (struct page *)0;
4208#line 374
4209 __cil_tmp20 = (unsigned long )__cil_tmp19;
4210#line 374
4211 __cil_tmp21 = __cil_tmp20 + 32;
4212#line 374
4213 __cil_tmp22 = (struct list_head *)__cil_tmp21;
4214#line 374
4215 __cil_tmp23 = (unsigned int )__cil_tmp22;
4216#line 374
4217 __cil_tmp24 = (char *)__mptr___0;
4218#line 374
4219 __cil_tmp25 = __cil_tmp24 - __cil_tmp23;
4220#line 374
4221 next = (struct page *)__cil_tmp25;
4222 {
4223#line 374
4224 while (1) {
4225 while_continue: ;
4226 {
4227#line 374
4228 __cil_tmp26 = (struct list_head *)b;
4229#line 374
4230 __cil_tmp27 = (unsigned long )__cil_tmp26;
4231#line 374
4232 __cil_tmp28 = (unsigned long )page;
4233#line 374
4234 __cil_tmp29 = __cil_tmp28 + 32;
4235#line 374
4236 __cil_tmp30 = (struct list_head *)__cil_tmp29;
4237#line 374
4238 __cil_tmp31 = (unsigned long )__cil_tmp30;
4239#line 374
4240 if (__cil_tmp31 != __cil_tmp27) {
4241
4242 } else {
4243#line 374
4244 goto while_break;
4245 }
4246 }
4247 {
4248#line 375
4249 __cil_tmp32 = (unsigned long )page;
4250#line 375
4251 __cil_tmp33 = __cil_tmp32 + 32;
4252#line 375
4253 __cil_tmp34 = (struct list_head *)__cil_tmp33;
4254#line 375
4255 list_del(__cil_tmp34);
4256#line 376
4257 __free_pages(page, 0U);
4258#line 377
4259 __cil_tmp35 = 60 + 28;
4260#line 377
4261 __cil_tmp36 = (unsigned long )b;
4262#line 377
4263 __cil_tmp37 = __cil_tmp36 + __cil_tmp35;
4264#line 377
4265 __cil_tmp38 = 60 + 28;
4266#line 377
4267 __cil_tmp39 = (unsigned long )b;
4268#line 377
4269 __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
4270#line 377
4271 __cil_tmp41 = *((unsigned int *)__cil_tmp40);
4272#line 377
4273 *((unsigned int *)__cil_tmp37) = __cil_tmp41 + 1U;
4274#line 378
4275 __cil_tmp42 = (unsigned long )b;
4276#line 378
4277 __cil_tmp43 = __cil_tmp42 + 36;
4278#line 378
4279 __cil_tmp44 = (unsigned long )b;
4280#line 378
4281 __cil_tmp45 = __cil_tmp44 + 36;
4282#line 378
4283 __cil_tmp46 = *((unsigned int *)__cil_tmp45);
4284#line 378
4285 *((unsigned int *)__cil_tmp43) = __cil_tmp46 - 1U;
4286#line 380
4287 count = count + 1U;
4288 }
4289 {
4290#line 380
4291 __cil_tmp47 = (unsigned long )b;
4292#line 380
4293 __cil_tmp48 = __cil_tmp47 + 52;
4294#line 380
4295 __cil_tmp49 = *((unsigned int *)__cil_tmp48);
4296#line 380
4297 if (count >= __cil_tmp49) {
4298 {
4299#line 381
4300 count = 0U;
4301#line 382
4302 __might_sleep("/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c",
4303 382, 0);
4304#line 382
4305 _cond_resched();
4306 }
4307 } else {
4308
4309 }
4310 }
4311#line 374
4312 page = next;
4313#line 374
4314 __cil_tmp50 = (unsigned long )next;
4315#line 374
4316 __cil_tmp51 = __cil_tmp50 + 32;
4317#line 374
4318 __cil_tmp52 = *((struct list_head **)__cil_tmp51);
4319#line 374
4320 __mptr___1 = (struct list_head const *)__cil_tmp52;
4321#line 374
4322 __cil_tmp53 = (struct page *)0;
4323#line 374
4324 __cil_tmp54 = (unsigned long )__cil_tmp53;
4325#line 374
4326 __cil_tmp55 = __cil_tmp54 + 32;
4327#line 374
4328 __cil_tmp56 = (struct list_head *)__cil_tmp55;
4329#line 374
4330 __cil_tmp57 = (unsigned int )__cil_tmp56;
4331#line 374
4332 __cil_tmp58 = (char *)__mptr___1;
4333#line 374
4334 __cil_tmp59 = __cil_tmp58 - __cil_tmp57;
4335#line 374
4336 next = (struct page *)__cil_tmp59;
4337 }
4338 while_break: ;
4339 }
4340#line 385
4341 return;
4342}
4343}
4344#line 392 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
4345static void vmballoon_reset(struct vmballoon *b )
4346{ bool tmp___7 ;
4347 bool tmp___8 ;
4348 unsigned long __cil_tmp4 ;
4349 unsigned long __cil_tmp5 ;
4350
4351 {
4352 {
4353#line 395
4354 vmballoon_pop(b);
4355#line 397
4356 tmp___8 = vmballoon_send_start(b);
4357 }
4358#line 397
4359 if (tmp___8) {
4360 {
4361#line 398
4362 __cil_tmp4 = (unsigned long )b;
4363#line 398
4364 __cil_tmp5 = __cil_tmp4 + 44;
4365#line 398
4366 *((bool *)__cil_tmp5) = (bool )0;
4367#line 399
4368 tmp___7 = vmballoon_send_guest_id(b);
4369 }
4370#line 399
4371 if (tmp___7) {
4372
4373 } else {
4374 {
4375#line 400
4376 printk("<3>vmw_balloon: failed to send guest ID to the host\n");
4377 }
4378 }
4379 } else {
4380
4381 }
4382#line 402
4383 return;
4384}
4385}
4386#line 410 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
4387static int vmballoon_reserve_page(struct vmballoon *b , bool can_sleep )
4388{ struct page *page ;
4389 gfp_t flags ;
4390 unsigned int hv_status ;
4391 int locked ;
4392 unsigned long __cil_tmp7 ;
4393 unsigned long __cil_tmp8 ;
4394 unsigned long __cil_tmp9 ;
4395 unsigned long __cil_tmp10 ;
4396 unsigned long __cil_tmp11 ;
4397 unsigned long __cil_tmp12 ;
4398 unsigned int __cil_tmp13 ;
4399 unsigned long __cil_tmp14 ;
4400 unsigned long __cil_tmp15 ;
4401 unsigned long __cil_tmp16 ;
4402 unsigned long __cil_tmp17 ;
4403 unsigned long __cil_tmp18 ;
4404 unsigned long __cil_tmp19 ;
4405 unsigned int __cil_tmp20 ;
4406 unsigned long __cil_tmp21 ;
4407 unsigned long __cil_tmp22 ;
4408 unsigned long __cil_tmp23 ;
4409 unsigned long __cil_tmp24 ;
4410 unsigned long __cil_tmp25 ;
4411 unsigned long __cil_tmp26 ;
4412 unsigned int __cil_tmp27 ;
4413 unsigned long __cil_tmp28 ;
4414 unsigned long __cil_tmp29 ;
4415 unsigned long __cil_tmp30 ;
4416 unsigned long __cil_tmp31 ;
4417 unsigned long __cil_tmp32 ;
4418 unsigned long __cil_tmp33 ;
4419 unsigned int __cil_tmp34 ;
4420 struct page *__cil_tmp35 ;
4421 int __cil_tmp36 ;
4422 unsigned long __cil_tmp37 ;
4423 unsigned long __cil_tmp38 ;
4424 unsigned long __cil_tmp39 ;
4425 unsigned long __cil_tmp40 ;
4426 unsigned long __cil_tmp41 ;
4427 unsigned long __cil_tmp42 ;
4428 unsigned long __cil_tmp43 ;
4429 unsigned int __cil_tmp44 ;
4430 unsigned int *__cil_tmp45 ;
4431 unsigned int __cil_tmp46 ;
4432 unsigned int *__cil_tmp47 ;
4433 unsigned int __cil_tmp48 ;
4434 unsigned long __cil_tmp49 ;
4435 unsigned long __cil_tmp50 ;
4436 struct list_head *__cil_tmp51 ;
4437 unsigned long __cil_tmp52 ;
4438 unsigned long __cil_tmp53 ;
4439 struct list_head *__cil_tmp54 ;
4440 unsigned long __cil_tmp55 ;
4441 unsigned long __cil_tmp56 ;
4442 unsigned long __cil_tmp57 ;
4443 unsigned long __cil_tmp58 ;
4444 unsigned int __cil_tmp59 ;
4445 unsigned long __cil_tmp60 ;
4446 unsigned long __cil_tmp61 ;
4447 unsigned int __cil_tmp62 ;
4448 unsigned long __cil_tmp63 ;
4449 unsigned long __cil_tmp64 ;
4450 struct list_head *__cil_tmp65 ;
4451 struct list_head *__cil_tmp66 ;
4452 unsigned long __cil_tmp67 ;
4453 unsigned long __cil_tmp68 ;
4454 unsigned long __cil_tmp69 ;
4455 unsigned long __cil_tmp70 ;
4456 unsigned int __cil_tmp71 ;
4457
4458 {
4459#line 416
4460 if (can_sleep) {
4461#line 416
4462 flags = 131282U;
4463 } else {
4464#line 416
4465 flags = 514U;
4466 }
4467 {
4468#line 418
4469 while (1) {
4470 while_continue: ;
4471#line 419
4472 if (! can_sleep) {
4473#line 420
4474 __cil_tmp7 = 60 + 4;
4475#line 420
4476 __cil_tmp8 = (unsigned long )b;
4477#line 420
4478 __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
4479#line 420
4480 __cil_tmp10 = 60 + 4;
4481#line 420
4482 __cil_tmp11 = (unsigned long )b;
4483#line 420
4484 __cil_tmp12 = __cil_tmp11 + __cil_tmp10;
4485#line 420
4486 __cil_tmp13 = *((unsigned int *)__cil_tmp12);
4487#line 420
4488 *((unsigned int *)__cil_tmp9) = __cil_tmp13 + 1U;
4489 } else {
4490#line 422
4491 __cil_tmp14 = 60 + 12;
4492#line 422
4493 __cil_tmp15 = (unsigned long )b;
4494#line 422
4495 __cil_tmp16 = __cil_tmp15 + __cil_tmp14;
4496#line 422
4497 __cil_tmp17 = 60 + 12;
4498#line 422
4499 __cil_tmp18 = (unsigned long )b;
4500#line 422
4501 __cil_tmp19 = __cil_tmp18 + __cil_tmp17;
4502#line 422
4503 __cil_tmp20 = *((unsigned int *)__cil_tmp19);
4504#line 422
4505 *((unsigned int *)__cil_tmp16) = __cil_tmp20 + 1U;
4506 }
4507 {
4508#line 424
4509 page = alloc_pages(flags, 0U);
4510 }
4511#line 425
4512 if (! page) {
4513#line 426
4514 if (! can_sleep) {
4515#line 427
4516 __cil_tmp21 = 60 + 8;
4517#line 427
4518 __cil_tmp22 = (unsigned long )b;
4519#line 427
4520 __cil_tmp23 = __cil_tmp22 + __cil_tmp21;
4521#line 427
4522 __cil_tmp24 = 60 + 8;
4523#line 427
4524 __cil_tmp25 = (unsigned long )b;
4525#line 427
4526 __cil_tmp26 = __cil_tmp25 + __cil_tmp24;
4527#line 427
4528 __cil_tmp27 = *((unsigned int *)__cil_tmp26);
4529#line 427
4530 *((unsigned int *)__cil_tmp23) = __cil_tmp27 + 1U;
4531 } else {
4532#line 429
4533 __cil_tmp28 = 60 + 16;
4534#line 429
4535 __cil_tmp29 = (unsigned long )b;
4536#line 429
4537 __cil_tmp30 = __cil_tmp29 + __cil_tmp28;
4538#line 429
4539 __cil_tmp31 = 60 + 16;
4540#line 429
4541 __cil_tmp32 = (unsigned long )b;
4542#line 429
4543 __cil_tmp33 = __cil_tmp32 + __cil_tmp31;
4544#line 429
4545 __cil_tmp34 = *((unsigned int *)__cil_tmp33);
4546#line 429
4547 *((unsigned int *)__cil_tmp30) = __cil_tmp34 + 1U;
4548 }
4549#line 430
4550 return (-12);
4551 } else {
4552
4553 }
4554 {
4555#line 434
4556 __cil_tmp35 = (struct page *)0xffffea0000000000UL;
4557#line 434
4558 __cil_tmp36 = page - __cil_tmp35;
4559#line 434
4560 __cil_tmp37 = (unsigned long )__cil_tmp36;
4561#line 434
4562 locked = vmballoon_send_lock_page(b, __cil_tmp37, & hv_status);
4563 }
4564#line 435
4565 if (locked > 0) {
4566#line 436
4567 __cil_tmp38 = 60 + 20;
4568#line 436
4569 __cil_tmp39 = (unsigned long )b;
4570#line 436
4571 __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
4572#line 436
4573 __cil_tmp41 = 60 + 20;
4574#line 436
4575 __cil_tmp42 = (unsigned long )b;
4576#line 436
4577 __cil_tmp43 = __cil_tmp42 + __cil_tmp41;
4578#line 436
4579 __cil_tmp44 = *((unsigned int *)__cil_tmp43);
4580#line 436
4581 *((unsigned int *)__cil_tmp40) = __cil_tmp44 + 1U;
4582 {
4583#line 438
4584 __cil_tmp45 = & hv_status;
4585#line 438
4586 __cil_tmp46 = *__cil_tmp45;
4587#line 438
4588 if (__cil_tmp46 == 7U) {
4589 {
4590#line 440
4591 __free_pages(page, 0U);
4592 }
4593#line 441
4594 return (-5);
4595 } else {
4596 {
4597#line 438
4598 __cil_tmp47 = & hv_status;
4599#line 438
4600 __cil_tmp48 = *__cil_tmp47;
4601#line 438
4602 if (__cil_tmp48 == 6U) {
4603 {
4604#line 440
4605 __free_pages(page, 0U);
4606 }
4607#line 441
4608 return (-5);
4609 } else {
4610
4611 }
4612 }
4613 }
4614 }
4615 {
4616#line 449
4617 __cil_tmp49 = (unsigned long )page;
4618#line 449
4619 __cil_tmp50 = __cil_tmp49 + 32;
4620#line 449
4621 __cil_tmp51 = (struct list_head *)__cil_tmp50;
4622#line 449
4623 __cil_tmp52 = (unsigned long )b;
4624#line 449
4625 __cil_tmp53 = __cil_tmp52 + 16;
4626#line 449
4627 __cil_tmp54 = (struct list_head *)__cil_tmp53;
4628#line 449
4629 list_add(__cil_tmp51, __cil_tmp54);
4630#line 450
4631 __cil_tmp55 = (unsigned long )b;
4632#line 450
4633 __cil_tmp56 = __cil_tmp55 + 32;
4634#line 450
4635 __cil_tmp57 = (unsigned long )b;
4636#line 450
4637 __cil_tmp58 = __cil_tmp57 + 32;
4638#line 450
4639 __cil_tmp59 = *((unsigned int *)__cil_tmp58);
4640#line 450
4641 *((unsigned int *)__cil_tmp56) = __cil_tmp59 + 1U;
4642 }
4643 {
4644#line 450
4645 __cil_tmp60 = (unsigned long )b;
4646#line 450
4647 __cil_tmp61 = __cil_tmp60 + 32;
4648#line 450
4649 __cil_tmp62 = *((unsigned int *)__cil_tmp61);
4650#line 450
4651 if (__cil_tmp62 >= 16U) {
4652#line 451
4653 return (-5);
4654 } else {
4655
4656 }
4657 }
4658 } else {
4659
4660 }
4661#line 418
4662 if (locked != 0) {
4663
4664 } else {
4665#line 418
4666 goto while_break;
4667 }
4668 }
4669 while_break: ;
4670 }
4671 {
4672#line 456
4673 __cil_tmp63 = (unsigned long )page;
4674#line 456
4675 __cil_tmp64 = __cil_tmp63 + 32;
4676#line 456
4677 __cil_tmp65 = (struct list_head *)__cil_tmp64;
4678#line 456
4679 __cil_tmp66 = (struct list_head *)b;
4680#line 456
4681 list_add(__cil_tmp65, __cil_tmp66);
4682#line 459
4683 __cil_tmp67 = (unsigned long )b;
4684#line 459
4685 __cil_tmp68 = __cil_tmp67 + 36;
4686#line 459
4687 __cil_tmp69 = (unsigned long )b;
4688#line 459
4689 __cil_tmp70 = __cil_tmp69 + 36;
4690#line 459
4691 __cil_tmp71 = *((unsigned int *)__cil_tmp70);
4692#line 459
4693 *((unsigned int *)__cil_tmp68) = __cil_tmp71 + 1U;
4694 }
4695#line 461
4696 return (0);
4697}
4698}
4699#line 469 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
4700static int vmballoon_release_page(struct vmballoon *b , struct page *page )
4701{ bool tmp___7 ;
4702 struct page *__cil_tmp4 ;
4703 int __cil_tmp5 ;
4704 unsigned long __cil_tmp6 ;
4705 unsigned long __cil_tmp7 ;
4706 unsigned long __cil_tmp8 ;
4707 struct list_head *__cil_tmp9 ;
4708 unsigned long __cil_tmp10 ;
4709 unsigned long __cil_tmp11 ;
4710 unsigned long __cil_tmp12 ;
4711 unsigned long __cil_tmp13 ;
4712 unsigned long __cil_tmp14 ;
4713 unsigned long __cil_tmp15 ;
4714 unsigned int __cil_tmp16 ;
4715 unsigned long __cil_tmp17 ;
4716 unsigned long __cil_tmp18 ;
4717 unsigned long __cil_tmp19 ;
4718 unsigned long __cil_tmp20 ;
4719 unsigned int __cil_tmp21 ;
4720
4721 {
4722 {
4723#line 471
4724 __cil_tmp4 = (struct page *)0xffffea0000000000UL;
4725#line 471
4726 __cil_tmp5 = page - __cil_tmp4;
4727#line 471
4728 __cil_tmp6 = (unsigned long )__cil_tmp5;
4729#line 471
4730 tmp___7 = vmballoon_send_unlock_page(b, __cil_tmp6);
4731 }
4732#line 471
4733 if (tmp___7) {
4734
4735 } else {
4736#line 472
4737 return (-5);
4738 }
4739 {
4740#line 474
4741 __cil_tmp7 = (unsigned long )page;
4742#line 474
4743 __cil_tmp8 = __cil_tmp7 + 32;
4744#line 474
4745 __cil_tmp9 = (struct list_head *)__cil_tmp8;
4746#line 474
4747 list_del(__cil_tmp9);
4748#line 477
4749 __free_pages(page, 0U);
4750#line 478
4751 __cil_tmp10 = 60 + 28;
4752#line 478
4753 __cil_tmp11 = (unsigned long )b;
4754#line 478
4755 __cil_tmp12 = __cil_tmp11 + __cil_tmp10;
4756#line 478
4757 __cil_tmp13 = 60 + 28;
4758#line 478
4759 __cil_tmp14 = (unsigned long )b;
4760#line 478
4761 __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
4762#line 478
4763 __cil_tmp16 = *((unsigned int *)__cil_tmp15);
4764#line 478
4765 *((unsigned int *)__cil_tmp12) = __cil_tmp16 + 1U;
4766#line 481
4767 __cil_tmp17 = (unsigned long )b;
4768#line 481
4769 __cil_tmp18 = __cil_tmp17 + 36;
4770#line 481
4771 __cil_tmp19 = (unsigned long )b;
4772#line 481
4773 __cil_tmp20 = __cil_tmp19 + 36;
4774#line 481
4775 __cil_tmp21 = *((unsigned int *)__cil_tmp20);
4776#line 481
4777 *((unsigned int *)__cil_tmp18) = __cil_tmp21 - 1U;
4778 }
4779#line 483
4780 return (0);
4781}
4782}
4783#line 490 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
4784static void vmballoon_release_refused_pages(struct vmballoon *b )
4785{ struct page *page ;
4786 struct page *next ;
4787 struct list_head const *__mptr ;
4788 struct list_head const *__mptr___0 ;
4789 struct list_head const *__mptr___1 ;
4790 unsigned long __cil_tmp7 ;
4791 unsigned long __cil_tmp8 ;
4792 struct list_head *__cil_tmp9 ;
4793 struct page *__cil_tmp10 ;
4794 unsigned long __cil_tmp11 ;
4795 unsigned long __cil_tmp12 ;
4796 struct list_head *__cil_tmp13 ;
4797 unsigned int __cil_tmp14 ;
4798 char *__cil_tmp15 ;
4799 char *__cil_tmp16 ;
4800 unsigned long __cil_tmp17 ;
4801 unsigned long __cil_tmp18 ;
4802 struct list_head *__cil_tmp19 ;
4803 struct page *__cil_tmp20 ;
4804 unsigned long __cil_tmp21 ;
4805 unsigned long __cil_tmp22 ;
4806 struct list_head *__cil_tmp23 ;
4807 unsigned int __cil_tmp24 ;
4808 char *__cil_tmp25 ;
4809 char *__cil_tmp26 ;
4810 unsigned long __cil_tmp27 ;
4811 unsigned long __cil_tmp28 ;
4812 struct list_head *__cil_tmp29 ;
4813 unsigned long __cil_tmp30 ;
4814 unsigned long __cil_tmp31 ;
4815 unsigned long __cil_tmp32 ;
4816 struct list_head *__cil_tmp33 ;
4817 unsigned long __cil_tmp34 ;
4818 unsigned long __cil_tmp35 ;
4819 unsigned long __cil_tmp36 ;
4820 struct list_head *__cil_tmp37 ;
4821 unsigned long __cil_tmp38 ;
4822 unsigned long __cil_tmp39 ;
4823 unsigned long __cil_tmp40 ;
4824 unsigned long __cil_tmp41 ;
4825 unsigned long __cil_tmp42 ;
4826 unsigned long __cil_tmp43 ;
4827 unsigned int __cil_tmp44 ;
4828 unsigned long __cil_tmp45 ;
4829 unsigned long __cil_tmp46 ;
4830 struct list_head *__cil_tmp47 ;
4831 struct page *__cil_tmp48 ;
4832 unsigned long __cil_tmp49 ;
4833 unsigned long __cil_tmp50 ;
4834 struct list_head *__cil_tmp51 ;
4835 unsigned int __cil_tmp52 ;
4836 char *__cil_tmp53 ;
4837 char *__cil_tmp54 ;
4838 unsigned long __cil_tmp55 ;
4839 unsigned long __cil_tmp56 ;
4840
4841 {
4842#line 494
4843 __cil_tmp7 = (unsigned long )b;
4844#line 494
4845 __cil_tmp8 = __cil_tmp7 + 16;
4846#line 494
4847 __cil_tmp9 = *((struct list_head **)__cil_tmp8);
4848#line 494
4849 __mptr = (struct list_head const *)__cil_tmp9;
4850#line 494
4851 __cil_tmp10 = (struct page *)0;
4852#line 494
4853 __cil_tmp11 = (unsigned long )__cil_tmp10;
4854#line 494
4855 __cil_tmp12 = __cil_tmp11 + 32;
4856#line 494
4857 __cil_tmp13 = (struct list_head *)__cil_tmp12;
4858#line 494
4859 __cil_tmp14 = (unsigned int )__cil_tmp13;
4860#line 494
4861 __cil_tmp15 = (char *)__mptr;
4862#line 494
4863 __cil_tmp16 = __cil_tmp15 - __cil_tmp14;
4864#line 494
4865 page = (struct page *)__cil_tmp16;
4866#line 494
4867 __cil_tmp17 = (unsigned long )page;
4868#line 494
4869 __cil_tmp18 = __cil_tmp17 + 32;
4870#line 494
4871 __cil_tmp19 = *((struct list_head **)__cil_tmp18);
4872#line 494
4873 __mptr___0 = (struct list_head const *)__cil_tmp19;
4874#line 494
4875 __cil_tmp20 = (struct page *)0;
4876#line 494
4877 __cil_tmp21 = (unsigned long )__cil_tmp20;
4878#line 494
4879 __cil_tmp22 = __cil_tmp21 + 32;
4880#line 494
4881 __cil_tmp23 = (struct list_head *)__cil_tmp22;
4882#line 494
4883 __cil_tmp24 = (unsigned int )__cil_tmp23;
4884#line 494
4885 __cil_tmp25 = (char *)__mptr___0;
4886#line 494
4887 __cil_tmp26 = __cil_tmp25 - __cil_tmp24;
4888#line 494
4889 next = (struct page *)__cil_tmp26;
4890 {
4891#line 494
4892 while (1) {
4893 while_continue: ;
4894 {
4895#line 494
4896 __cil_tmp27 = (unsigned long )b;
4897#line 494
4898 __cil_tmp28 = __cil_tmp27 + 16;
4899#line 494
4900 __cil_tmp29 = (struct list_head *)__cil_tmp28;
4901#line 494
4902 __cil_tmp30 = (unsigned long )__cil_tmp29;
4903#line 494
4904 __cil_tmp31 = (unsigned long )page;
4905#line 494
4906 __cil_tmp32 = __cil_tmp31 + 32;
4907#line 494
4908 __cil_tmp33 = (struct list_head *)__cil_tmp32;
4909#line 494
4910 __cil_tmp34 = (unsigned long )__cil_tmp33;
4911#line 494
4912 if (__cil_tmp34 != __cil_tmp30) {
4913
4914 } else {
4915#line 494
4916 goto while_break;
4917 }
4918 }
4919 {
4920#line 495
4921 __cil_tmp35 = (unsigned long )page;
4922#line 495
4923 __cil_tmp36 = __cil_tmp35 + 32;
4924#line 495
4925 __cil_tmp37 = (struct list_head *)__cil_tmp36;
4926#line 495
4927 list_del(__cil_tmp37);
4928#line 496
4929 __free_pages(page, 0U);
4930#line 497
4931 __cil_tmp38 = 60 + 24;
4932#line 497
4933 __cil_tmp39 = (unsigned long )b;
4934#line 497
4935 __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
4936#line 497
4937 __cil_tmp41 = 60 + 24;
4938#line 497
4939 __cil_tmp42 = (unsigned long )b;
4940#line 497
4941 __cil_tmp43 = __cil_tmp42 + __cil_tmp41;
4942#line 497
4943 __cil_tmp44 = *((unsigned int *)__cil_tmp43);
4944#line 497
4945 *((unsigned int *)__cil_tmp40) = __cil_tmp44 + 1U;
4946#line 494
4947 page = next;
4948#line 494
4949 __cil_tmp45 = (unsigned long )next;
4950#line 494
4951 __cil_tmp46 = __cil_tmp45 + 32;
4952#line 494
4953 __cil_tmp47 = *((struct list_head **)__cil_tmp46);
4954#line 494
4955 __mptr___1 = (struct list_head const *)__cil_tmp47;
4956#line 494
4957 __cil_tmp48 = (struct page *)0;
4958#line 494
4959 __cil_tmp49 = (unsigned long )__cil_tmp48;
4960#line 494
4961 __cil_tmp50 = __cil_tmp49 + 32;
4962#line 494
4963 __cil_tmp51 = (struct list_head *)__cil_tmp50;
4964#line 494
4965 __cil_tmp52 = (unsigned int )__cil_tmp51;
4966#line 494
4967 __cil_tmp53 = (char *)__mptr___1;
4968#line 494
4969 __cil_tmp54 = __cil_tmp53 - __cil_tmp52;
4970#line 494
4971 next = (struct page *)__cil_tmp54;
4972 }
4973 }
4974 while_break: ;
4975 }
4976#line 500
4977 __cil_tmp55 = (unsigned long )b;
4978#line 500
4979 __cil_tmp56 = __cil_tmp55 + 32;
4980#line 500
4981 *((unsigned int *)__cil_tmp56) = 0U;
4982#line 501
4983 return;
4984}
4985}
4986#line 517
4987static void vmballoon_inflate(struct vmballoon *b ) ;
4988#line 517 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
4989static struct _ddebug __attribute__((__aligned__(8))) descriptor___4 __attribute__((__used__,
4990__section__("__verbose"))) = {"vmw_balloon", "vmballoon_inflate", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c",
4991 "%s - size: %d, target %d\n", 517U, 0U};
4992#line 542
4993static void vmballoon_inflate(struct vmballoon *b ) ;
4994#line 542 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
4995static struct _ddebug __attribute__((__aligned__(8))) descriptor___5 __attribute__((__used__,
4996__section__("__verbose"))) = {"vmw_balloon", "vmballoon_inflate", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c",
4997 "%s - goal: %d, no-sleep rate: %d, sleep rate: %d\n", 543U, 0U};
4998#line 508 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
4999static void vmballoon_inflate(struct vmballoon *b )
5000{ unsigned int goal ;
5001 unsigned int rate ;
5002 unsigned int i ;
5003 unsigned int allocations ;
5004 int error ;
5005 bool alloc_can_sleep ;
5006 long tmp___7 ;
5007 long tmp___8 ;
5008 unsigned int _max1 ;
5009 unsigned int _max2 ;
5010 unsigned int tmp___9 ;
5011 unsigned int mult ;
5012 unsigned int _min1 ;
5013 unsigned int _min2 ;
5014 unsigned int tmp___10 ;
5015 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp17 ;
5016 unsigned int __cil_tmp18 ;
5017 unsigned int __cil_tmp19 ;
5018 int __cil_tmp20 ;
5019 int __cil_tmp21 ;
5020 long __cil_tmp22 ;
5021 unsigned long __cil_tmp23 ;
5022 unsigned long __cil_tmp24 ;
5023 unsigned int __cil_tmp25 ;
5024 unsigned long __cil_tmp26 ;
5025 unsigned long __cil_tmp27 ;
5026 unsigned int __cil_tmp28 ;
5027 unsigned long __cil_tmp29 ;
5028 unsigned long __cil_tmp30 ;
5029 unsigned int __cil_tmp31 ;
5030 unsigned long __cil_tmp32 ;
5031 unsigned long __cil_tmp33 ;
5032 unsigned int __cil_tmp34 ;
5033 unsigned long __cil_tmp35 ;
5034 unsigned long __cil_tmp36 ;
5035 unsigned long __cil_tmp37 ;
5036 unsigned long __cil_tmp38 ;
5037 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp39 ;
5038 unsigned int __cil_tmp40 ;
5039 unsigned int __cil_tmp41 ;
5040 int __cil_tmp42 ;
5041 int __cil_tmp43 ;
5042 long __cil_tmp44 ;
5043 unsigned long __cil_tmp45 ;
5044 unsigned long __cil_tmp46 ;
5045 unsigned int __cil_tmp47 ;
5046 unsigned int *__cil_tmp48 ;
5047 unsigned long __cil_tmp49 ;
5048 unsigned long __cil_tmp50 ;
5049 unsigned int __cil_tmp51 ;
5050 unsigned int *__cil_tmp52 ;
5051 unsigned int *__cil_tmp53 ;
5052 unsigned int __cil_tmp54 ;
5053 unsigned int *__cil_tmp55 ;
5054 unsigned int __cil_tmp56 ;
5055 unsigned int *__cil_tmp57 ;
5056 unsigned int *__cil_tmp58 ;
5057 unsigned long __cil_tmp59 ;
5058 unsigned long __cil_tmp60 ;
5059 unsigned long __cil_tmp61 ;
5060 unsigned long __cil_tmp62 ;
5061 unsigned long __cil_tmp63 ;
5062 unsigned long __cil_tmp64 ;
5063 unsigned int __cil_tmp65 ;
5064 unsigned long __cil_tmp66 ;
5065 unsigned long __cil_tmp67 ;
5066 unsigned long __cil_tmp68 ;
5067 unsigned long __cil_tmp69 ;
5068 unsigned int __cil_tmp70 ;
5069 unsigned long __cil_tmp71 ;
5070 unsigned long __cil_tmp72 ;
5071 unsigned int __cil_tmp73 ;
5072 unsigned int *__cil_tmp74 ;
5073 unsigned int __cil_tmp75 ;
5074 unsigned long __cil_tmp76 ;
5075 unsigned long __cil_tmp77 ;
5076 unsigned int __cil_tmp78 ;
5077 unsigned int *__cil_tmp79 ;
5078 unsigned int *__cil_tmp80 ;
5079 unsigned int __cil_tmp81 ;
5080 unsigned int *__cil_tmp82 ;
5081 unsigned int __cil_tmp83 ;
5082 unsigned int *__cil_tmp84 ;
5083 unsigned int *__cil_tmp85 ;
5084 unsigned long __cil_tmp86 ;
5085 unsigned long __cil_tmp87 ;
5086
5087 {
5088#line 513
5089 allocations = 0U;
5090#line 514
5091 error = 0;
5092#line 515
5093 alloc_can_sleep = (bool )0;
5094 {
5095#line 517
5096 while (1) {
5097 while_continue: ;
5098 {
5099#line 517
5100 __cil_tmp17 = & descriptor___4;
5101#line 517
5102 __cil_tmp18 = __cil_tmp17->flags;
5103#line 517
5104 __cil_tmp19 = __cil_tmp18 & 1U;
5105#line 517
5106 __cil_tmp20 = ! __cil_tmp19;
5107#line 517
5108 __cil_tmp21 = ! __cil_tmp20;
5109#line 517
5110 __cil_tmp22 = (long )__cil_tmp21;
5111#line 517
5112 tmp___7 = __builtin_expect(__cil_tmp22, 0L);
5113 }
5114#line 517
5115 if (tmp___7) {
5116 {
5117#line 517
5118 __cil_tmp23 = (unsigned long )b;
5119#line 517
5120 __cil_tmp24 = __cil_tmp23 + 36;
5121#line 517
5122 __cil_tmp25 = *((unsigned int *)__cil_tmp24);
5123#line 517
5124 __cil_tmp26 = (unsigned long )b;
5125#line 517
5126 __cil_tmp27 = __cil_tmp26 + 40;
5127#line 517
5128 __cil_tmp28 = *((unsigned int *)__cil_tmp27);
5129#line 517
5130 __dynamic_pr_debug(& descriptor___4, "vmw_balloon: %s - size: %d, target %d\n",
5131 "vmballoon_inflate", __cil_tmp25, __cil_tmp28);
5132 }
5133 } else {
5134
5135 }
5136#line 517
5137 goto while_break;
5138 }
5139 while_break: ;
5140 }
5141#line 534
5142 __cil_tmp29 = (unsigned long )b;
5143#line 534
5144 __cil_tmp30 = __cil_tmp29 + 36;
5145#line 534
5146 __cil_tmp31 = *((unsigned int *)__cil_tmp30);
5147#line 534
5148 __cil_tmp32 = (unsigned long )b;
5149#line 534
5150 __cil_tmp33 = __cil_tmp32 + 40;
5151#line 534
5152 __cil_tmp34 = *((unsigned int *)__cil_tmp33);
5153#line 534
5154 goal = __cil_tmp34 - __cil_tmp31;
5155 {
5156#line 539
5157 __cil_tmp35 = (unsigned long )b;
5158#line 539
5159 __cil_tmp36 = __cil_tmp35 + 56;
5160#line 539
5161 if (*((unsigned int *)__cil_tmp36)) {
5162#line 539
5163 __cil_tmp37 = (unsigned long )b;
5164#line 539
5165 __cil_tmp38 = __cil_tmp37 + 48;
5166#line 539
5167 rate = *((unsigned int *)__cil_tmp38);
5168 } else {
5169#line 539
5170 rate = 16384U;
5171 }
5172 }
5173 {
5174#line 542
5175 while (1) {
5176 while_continue___0: ;
5177 {
5178#line 542
5179 __cil_tmp39 = & descriptor___5;
5180#line 542
5181 __cil_tmp40 = __cil_tmp39->flags;
5182#line 542
5183 __cil_tmp41 = __cil_tmp40 & 1U;
5184#line 542
5185 __cil_tmp42 = ! __cil_tmp41;
5186#line 542
5187 __cil_tmp43 = ! __cil_tmp42;
5188#line 542
5189 __cil_tmp44 = (long )__cil_tmp43;
5190#line 542
5191 tmp___8 = __builtin_expect(__cil_tmp44, 0L);
5192 }
5193#line 542
5194 if (tmp___8) {
5195 {
5196#line 542
5197 __cil_tmp45 = (unsigned long )b;
5198#line 542
5199 __cil_tmp46 = __cil_tmp45 + 48;
5200#line 542
5201 __cil_tmp47 = *((unsigned int *)__cil_tmp46);
5202#line 542
5203 __dynamic_pr_debug(& descriptor___5, "vmw_balloon: %s - goal: %d, no-sleep rate: %d, sleep rate: %d\n",
5204 "vmballoon_inflate", goal, rate, __cil_tmp47);
5205 }
5206 } else {
5207
5208 }
5209#line 542
5210 goto while_break___0;
5211 }
5212 while_break___0: ;
5213 }
5214#line 545
5215 i = 0U;
5216 {
5217#line 545
5218 while (1) {
5219 while_continue___1: ;
5220#line 545
5221 if (i < goal) {
5222
5223 } else {
5224#line 545
5225 goto while_break___1;
5226 }
5227 {
5228#line 547
5229 error = vmballoon_reserve_page(b, alloc_can_sleep);
5230 }
5231#line 548
5232 if (error) {
5233#line 549
5234 if (error != -12) {
5235#line 555
5236 goto while_break___1;
5237 } else {
5238
5239 }
5240#line 558
5241 if (alloc_can_sleep) {
5242#line 564
5243 __cil_tmp48 = & _max1;
5244#line 564
5245 __cil_tmp49 = (unsigned long )b;
5246#line 564
5247 __cil_tmp50 = __cil_tmp49 + 48;
5248#line 564
5249 __cil_tmp51 = *((unsigned int *)__cil_tmp50);
5250#line 564
5251 *__cil_tmp48 = __cil_tmp51 / 2U;
5252#line 564
5253 __cil_tmp52 = & _max2;
5254#line 564
5255 *__cil_tmp52 = 512U;
5256 {
5257#line 564
5258 __cil_tmp53 = & _max2;
5259#line 564
5260 __cil_tmp54 = *__cil_tmp53;
5261#line 564
5262 __cil_tmp55 = & _max1;
5263#line 564
5264 __cil_tmp56 = *__cil_tmp55;
5265#line 564
5266 if (__cil_tmp56 > __cil_tmp54) {
5267#line 564
5268 __cil_tmp57 = & _max1;
5269#line 564
5270 tmp___9 = *__cil_tmp57;
5271 } else {
5272#line 564
5273 __cil_tmp58 = & _max2;
5274#line 564
5275 tmp___9 = *__cil_tmp58;
5276 }
5277 }
5278#line 564
5279 __cil_tmp59 = (unsigned long )b;
5280#line 564
5281 __cil_tmp60 = __cil_tmp59 + 48;
5282#line 564
5283 *((unsigned int *)__cil_tmp60) = tmp___9;
5284#line 566
5285 goto while_break___1;
5286 } else {
5287
5288 }
5289#line 577
5290 __cil_tmp61 = (unsigned long )b;
5291#line 577
5292 __cil_tmp62 = __cil_tmp61 + 56;
5293#line 577
5294 *((unsigned int *)__cil_tmp62) = 4U;
5295 {
5296#line 579
5297 __cil_tmp63 = (unsigned long )b;
5298#line 579
5299 __cil_tmp64 = __cil_tmp63 + 48;
5300#line 579
5301 __cil_tmp65 = *((unsigned int *)__cil_tmp64);
5302#line 579
5303 if (i >= __cil_tmp65) {
5304#line 580
5305 goto while_break___1;
5306 } else {
5307
5308 }
5309 }
5310#line 582
5311 alloc_can_sleep = (bool )1;
5312#line 584
5313 __cil_tmp66 = (unsigned long )b;
5314#line 584
5315 __cil_tmp67 = __cil_tmp66 + 48;
5316#line 584
5317 rate = *((unsigned int *)__cil_tmp67);
5318 } else {
5319
5320 }
5321#line 587
5322 allocations = allocations + 1U;
5323#line 587
5324 if (allocations > 1024U) {
5325 {
5326#line 588
5327 __might_sleep("/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c",
5328 588, 0);
5329#line 588
5330 _cond_resched();
5331#line 589
5332 allocations = 0U;
5333 }
5334 } else {
5335
5336 }
5337#line 592
5338 if (i >= rate) {
5339#line 594
5340 goto while_break___1;
5341 } else {
5342
5343 }
5344#line 545
5345 i = i + 1U;
5346 }
5347 while_break___1: ;
5348 }
5349#line 602
5350 if (error == 0) {
5351 {
5352#line 602
5353 __cil_tmp68 = (unsigned long )b;
5354#line 602
5355 __cil_tmp69 = __cil_tmp68 + 48;
5356#line 602
5357 __cil_tmp70 = *((unsigned int *)__cil_tmp69);
5358#line 602
5359 if (i >= __cil_tmp70) {
5360#line 603
5361 __cil_tmp71 = (unsigned long )b;
5362#line 603
5363 __cil_tmp72 = __cil_tmp71 + 48;
5364#line 603
5365 __cil_tmp73 = *((unsigned int *)__cil_tmp72);
5366#line 603
5367 mult = i / __cil_tmp73;
5368#line 606
5369 __cil_tmp74 = & _min1;
5370#line 606
5371 __cil_tmp75 = mult * 16U;
5372#line 606
5373 __cil_tmp76 = (unsigned long )b;
5374#line 606
5375 __cil_tmp77 = __cil_tmp76 + 48;
5376#line 606
5377 __cil_tmp78 = *((unsigned int *)__cil_tmp77);
5378#line 606
5379 *__cil_tmp74 = __cil_tmp78 + __cil_tmp75;
5380#line 606
5381 __cil_tmp79 = & _min2;
5382#line 606
5383 *__cil_tmp79 = 2048U;
5384 {
5385#line 606
5386 __cil_tmp80 = & _min2;
5387#line 606
5388 __cil_tmp81 = *__cil_tmp80;
5389#line 606
5390 __cil_tmp82 = & _min1;
5391#line 606
5392 __cil_tmp83 = *__cil_tmp82;
5393#line 606
5394 if (__cil_tmp83 < __cil_tmp81) {
5395#line 606
5396 __cil_tmp84 = & _min1;
5397#line 606
5398 tmp___10 = *__cil_tmp84;
5399 } else {
5400#line 606
5401 __cil_tmp85 = & _min2;
5402#line 606
5403 tmp___10 = *__cil_tmp85;
5404 }
5405 }
5406#line 606
5407 __cil_tmp86 = (unsigned long )b;
5408#line 606
5409 __cil_tmp87 = __cil_tmp86 + 48;
5410#line 606
5411 *((unsigned int *)__cil_tmp87) = tmp___10;
5412 } else {
5413
5414 }
5415 }
5416 } else {
5417
5418 }
5419 {
5420#line 610
5421 vmballoon_release_refused_pages(b);
5422 }
5423#line 611
5424 return;
5425}
5426}
5427#line 623
5428static void vmballoon_deflate(struct vmballoon *b ) ;
5429#line 623 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
5430static struct _ddebug __attribute__((__aligned__(8))) descriptor___6 __attribute__((__used__,
5431__section__("__verbose"))) = {"vmw_balloon", "vmballoon_deflate", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c",
5432 "%s - size: %d, target %d\n", 623U, 0U};
5433#line 628
5434static void vmballoon_deflate(struct vmballoon *b ) ;
5435#line 628 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
5436static struct _ddebug __attribute__((__aligned__(8))) descriptor___7 __attribute__((__used__,
5437__section__("__verbose"))) = {"vmw_balloon", "vmballoon_deflate", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c",
5438 "%s - goal: %d, rate: %d\n", 628U, 0U};
5439#line 616 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
5440static void vmballoon_deflate(struct vmballoon *b )
5441{ struct page *page ;
5442 struct page *next ;
5443 unsigned int i ;
5444 unsigned int goal ;
5445 int error ;
5446 long tmp___7 ;
5447 unsigned int _min1 ;
5448 unsigned int _min2 ;
5449 unsigned int tmp___8 ;
5450 long tmp___9 ;
5451 struct list_head const *__mptr ;
5452 struct list_head const *__mptr___0 ;
5453 struct list_head const *__mptr___1 ;
5454 unsigned int _max1 ;
5455 unsigned int _max2 ;
5456 unsigned int tmp___10 ;
5457 unsigned int _min1___0 ;
5458 unsigned int _min2___0 ;
5459 unsigned int tmp___11 ;
5460 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp21 ;
5461 unsigned int __cil_tmp22 ;
5462 unsigned int __cil_tmp23 ;
5463 int __cil_tmp24 ;
5464 int __cil_tmp25 ;
5465 long __cil_tmp26 ;
5466 unsigned long __cil_tmp27 ;
5467 unsigned long __cil_tmp28 ;
5468 unsigned int __cil_tmp29 ;
5469 unsigned long __cil_tmp30 ;
5470 unsigned long __cil_tmp31 ;
5471 unsigned int __cil_tmp32 ;
5472 unsigned int *__cil_tmp33 ;
5473 unsigned long __cil_tmp34 ;
5474 unsigned long __cil_tmp35 ;
5475 unsigned int __cil_tmp36 ;
5476 unsigned long __cil_tmp37 ;
5477 unsigned long __cil_tmp38 ;
5478 unsigned int __cil_tmp39 ;
5479 unsigned int *__cil_tmp40 ;
5480 unsigned long __cil_tmp41 ;
5481 unsigned long __cil_tmp42 ;
5482 unsigned int *__cil_tmp43 ;
5483 unsigned int __cil_tmp44 ;
5484 unsigned int *__cil_tmp45 ;
5485 unsigned int __cil_tmp46 ;
5486 unsigned int *__cil_tmp47 ;
5487 unsigned int *__cil_tmp48 ;
5488 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp49 ;
5489 unsigned int __cil_tmp50 ;
5490 unsigned int __cil_tmp51 ;
5491 int __cil_tmp52 ;
5492 int __cil_tmp53 ;
5493 long __cil_tmp54 ;
5494 unsigned long __cil_tmp55 ;
5495 unsigned long __cil_tmp56 ;
5496 unsigned int __cil_tmp57 ;
5497 struct list_head *__cil_tmp58 ;
5498 struct page *__cil_tmp59 ;
5499 unsigned long __cil_tmp60 ;
5500 unsigned long __cil_tmp61 ;
5501 struct list_head *__cil_tmp62 ;
5502 unsigned int __cil_tmp63 ;
5503 char *__cil_tmp64 ;
5504 char *__cil_tmp65 ;
5505 unsigned long __cil_tmp66 ;
5506 unsigned long __cil_tmp67 ;
5507 struct list_head *__cil_tmp68 ;
5508 struct page *__cil_tmp69 ;
5509 unsigned long __cil_tmp70 ;
5510 unsigned long __cil_tmp71 ;
5511 struct list_head *__cil_tmp72 ;
5512 unsigned int __cil_tmp73 ;
5513 char *__cil_tmp74 ;
5514 char *__cil_tmp75 ;
5515 struct list_head *__cil_tmp76 ;
5516 unsigned long __cil_tmp77 ;
5517 unsigned long __cil_tmp78 ;
5518 unsigned long __cil_tmp79 ;
5519 struct list_head *__cil_tmp80 ;
5520 unsigned long __cil_tmp81 ;
5521 unsigned int *__cil_tmp82 ;
5522 unsigned long __cil_tmp83 ;
5523 unsigned long __cil_tmp84 ;
5524 unsigned int __cil_tmp85 ;
5525 unsigned int *__cil_tmp86 ;
5526 unsigned int *__cil_tmp87 ;
5527 unsigned int __cil_tmp88 ;
5528 unsigned int *__cil_tmp89 ;
5529 unsigned int __cil_tmp90 ;
5530 unsigned int *__cil_tmp91 ;
5531 unsigned int *__cil_tmp92 ;
5532 unsigned long __cil_tmp93 ;
5533 unsigned long __cil_tmp94 ;
5534 unsigned long __cil_tmp95 ;
5535 unsigned long __cil_tmp96 ;
5536 struct list_head *__cil_tmp97 ;
5537 struct page *__cil_tmp98 ;
5538 unsigned long __cil_tmp99 ;
5539 unsigned long __cil_tmp100 ;
5540 struct list_head *__cil_tmp101 ;
5541 unsigned int __cil_tmp102 ;
5542 char *__cil_tmp103 ;
5543 char *__cil_tmp104 ;
5544 unsigned int *__cil_tmp105 ;
5545 unsigned long __cil_tmp106 ;
5546 unsigned long __cil_tmp107 ;
5547 unsigned int __cil_tmp108 ;
5548 unsigned int *__cil_tmp109 ;
5549 unsigned int *__cil_tmp110 ;
5550 unsigned int __cil_tmp111 ;
5551 unsigned int *__cil_tmp112 ;
5552 unsigned int __cil_tmp113 ;
5553 unsigned int *__cil_tmp114 ;
5554 unsigned int *__cil_tmp115 ;
5555 unsigned long __cil_tmp116 ;
5556 unsigned long __cil_tmp117 ;
5557
5558 {
5559#line 619
5560 i = 0U;
5561 {
5562#line 623
5563 while (1) {
5564 while_continue: ;
5565 {
5566#line 623
5567 __cil_tmp21 = & descriptor___6;
5568#line 623
5569 __cil_tmp22 = __cil_tmp21->flags;
5570#line 623
5571 __cil_tmp23 = __cil_tmp22 & 1U;
5572#line 623
5573 __cil_tmp24 = ! __cil_tmp23;
5574#line 623
5575 __cil_tmp25 = ! __cil_tmp24;
5576#line 623
5577 __cil_tmp26 = (long )__cil_tmp25;
5578#line 623
5579 tmp___7 = __builtin_expect(__cil_tmp26, 0L);
5580 }
5581#line 623
5582 if (tmp___7) {
5583 {
5584#line 623
5585 __cil_tmp27 = (unsigned long )b;
5586#line 623
5587 __cil_tmp28 = __cil_tmp27 + 36;
5588#line 623
5589 __cil_tmp29 = *((unsigned int *)__cil_tmp28);
5590#line 623
5591 __cil_tmp30 = (unsigned long )b;
5592#line 623
5593 __cil_tmp31 = __cil_tmp30 + 40;
5594#line 623
5595 __cil_tmp32 = *((unsigned int *)__cil_tmp31);
5596#line 623
5597 __dynamic_pr_debug(& descriptor___6, "vmw_balloon: %s - size: %d, target %d\n",
5598 "vmballoon_deflate", __cil_tmp29, __cil_tmp32);
5599 }
5600 } else {
5601
5602 }
5603#line 623
5604 goto while_break;
5605 }
5606 while_break: ;
5607 }
5608#line 626
5609 __cil_tmp33 = & _min1;
5610#line 626
5611 __cil_tmp34 = (unsigned long )b;
5612#line 626
5613 __cil_tmp35 = __cil_tmp34 + 40;
5614#line 626
5615 __cil_tmp36 = *((unsigned int *)__cil_tmp35);
5616#line 626
5617 __cil_tmp37 = (unsigned long )b;
5618#line 626
5619 __cil_tmp38 = __cil_tmp37 + 36;
5620#line 626
5621 __cil_tmp39 = *((unsigned int *)__cil_tmp38);
5622#line 626
5623 *__cil_tmp33 = __cil_tmp39 - __cil_tmp36;
5624#line 626
5625 __cil_tmp40 = & _min2;
5626#line 626
5627 __cil_tmp41 = (unsigned long )b;
5628#line 626
5629 __cil_tmp42 = __cil_tmp41 + 52;
5630#line 626
5631 *__cil_tmp40 = *((unsigned int *)__cil_tmp42);
5632 {
5633#line 626
5634 __cil_tmp43 = & _min2;
5635#line 626
5636 __cil_tmp44 = *__cil_tmp43;
5637#line 626
5638 __cil_tmp45 = & _min1;
5639#line 626
5640 __cil_tmp46 = *__cil_tmp45;
5641#line 626
5642 if (__cil_tmp46 < __cil_tmp44) {
5643#line 626
5644 __cil_tmp47 = & _min1;
5645#line 626
5646 tmp___8 = *__cil_tmp47;
5647 } else {
5648#line 626
5649 __cil_tmp48 = & _min2;
5650#line 626
5651 tmp___8 = *__cil_tmp48;
5652 }
5653 }
5654#line 626
5655 goal = tmp___8;
5656 {
5657#line 628
5658 while (1) {
5659 while_continue___0: ;
5660 {
5661#line 628
5662 __cil_tmp49 = & descriptor___7;
5663#line 628
5664 __cil_tmp50 = __cil_tmp49->flags;
5665#line 628
5666 __cil_tmp51 = __cil_tmp50 & 1U;
5667#line 628
5668 __cil_tmp52 = ! __cil_tmp51;
5669#line 628
5670 __cil_tmp53 = ! __cil_tmp52;
5671#line 628
5672 __cil_tmp54 = (long )__cil_tmp53;
5673#line 628
5674 tmp___9 = __builtin_expect(__cil_tmp54, 0L);
5675 }
5676#line 628
5677 if (tmp___9) {
5678 {
5679#line 628
5680 __cil_tmp55 = (unsigned long )b;
5681#line 628
5682 __cil_tmp56 = __cil_tmp55 + 52;
5683#line 628
5684 __cil_tmp57 = *((unsigned int *)__cil_tmp56);
5685#line 628
5686 __dynamic_pr_debug(& descriptor___7, "vmw_balloon: %s - goal: %d, rate: %d\n",
5687 "vmballoon_deflate", goal, __cil_tmp57);
5688 }
5689 } else {
5690
5691 }
5692#line 628
5693 goto while_break___0;
5694 }
5695 while_break___0: ;
5696 }
5697#line 631
5698 __cil_tmp58 = *((struct list_head **)b);
5699#line 631
5700 __mptr = (struct list_head const *)__cil_tmp58;
5701#line 631
5702 __cil_tmp59 = (struct page *)0;
5703#line 631
5704 __cil_tmp60 = (unsigned long )__cil_tmp59;
5705#line 631
5706 __cil_tmp61 = __cil_tmp60 + 32;
5707#line 631
5708 __cil_tmp62 = (struct list_head *)__cil_tmp61;
5709#line 631
5710 __cil_tmp63 = (unsigned int )__cil_tmp62;
5711#line 631
5712 __cil_tmp64 = (char *)__mptr;
5713#line 631
5714 __cil_tmp65 = __cil_tmp64 - __cil_tmp63;
5715#line 631
5716 page = (struct page *)__cil_tmp65;
5717#line 631
5718 __cil_tmp66 = (unsigned long )page;
5719#line 631
5720 __cil_tmp67 = __cil_tmp66 + 32;
5721#line 631
5722 __cil_tmp68 = *((struct list_head **)__cil_tmp67);
5723#line 631
5724 __mptr___0 = (struct list_head const *)__cil_tmp68;
5725#line 631
5726 __cil_tmp69 = (struct page *)0;
5727#line 631
5728 __cil_tmp70 = (unsigned long )__cil_tmp69;
5729#line 631
5730 __cil_tmp71 = __cil_tmp70 + 32;
5731#line 631
5732 __cil_tmp72 = (struct list_head *)__cil_tmp71;
5733#line 631
5734 __cil_tmp73 = (unsigned int )__cil_tmp72;
5735#line 631
5736 __cil_tmp74 = (char *)__mptr___0;
5737#line 631
5738 __cil_tmp75 = __cil_tmp74 - __cil_tmp73;
5739#line 631
5740 next = (struct page *)__cil_tmp75;
5741 {
5742#line 631
5743 while (1) {
5744 while_continue___1: ;
5745 {
5746#line 631
5747 __cil_tmp76 = (struct list_head *)b;
5748#line 631
5749 __cil_tmp77 = (unsigned long )__cil_tmp76;
5750#line 631
5751 __cil_tmp78 = (unsigned long )page;
5752#line 631
5753 __cil_tmp79 = __cil_tmp78 + 32;
5754#line 631
5755 __cil_tmp80 = (struct list_head *)__cil_tmp79;
5756#line 631
5757 __cil_tmp81 = (unsigned long )__cil_tmp80;
5758#line 631
5759 if (__cil_tmp81 != __cil_tmp77) {
5760
5761 } else {
5762#line 631
5763 goto while_break___1;
5764 }
5765 }
5766 {
5767#line 632
5768 error = vmballoon_release_page(b, page);
5769 }
5770#line 633
5771 if (error) {
5772#line 635
5773 __cil_tmp82 = & _max1;
5774#line 635
5775 __cil_tmp83 = (unsigned long )b;
5776#line 635
5777 __cil_tmp84 = __cil_tmp83 + 52;
5778#line 635
5779 __cil_tmp85 = *((unsigned int *)__cil_tmp84);
5780#line 635
5781 *__cil_tmp82 = __cil_tmp85 / 2U;
5782#line 635
5783 __cil_tmp86 = & _max2;
5784#line 635
5785 *__cil_tmp86 = 512U;
5786 {
5787#line 635
5788 __cil_tmp87 = & _max2;
5789#line 635
5790 __cil_tmp88 = *__cil_tmp87;
5791#line 635
5792 __cil_tmp89 = & _max1;
5793#line 635
5794 __cil_tmp90 = *__cil_tmp89;
5795#line 635
5796 if (__cil_tmp90 > __cil_tmp88) {
5797#line 635
5798 __cil_tmp91 = & _max1;
5799#line 635
5800 tmp___10 = *__cil_tmp91;
5801 } else {
5802#line 635
5803 __cil_tmp92 = & _max2;
5804#line 635
5805 tmp___10 = *__cil_tmp92;
5806 }
5807 }
5808#line 635
5809 __cil_tmp93 = (unsigned long )b;
5810#line 635
5811 __cil_tmp94 = __cil_tmp93 + 52;
5812#line 635
5813 *((unsigned int *)__cil_tmp94) = tmp___10;
5814#line 637
5815 return;
5816 } else {
5817
5818 }
5819#line 640
5820 i = i + 1U;
5821#line 640
5822 if (i >= goal) {
5823#line 641
5824 goto while_break___1;
5825 } else {
5826
5827 }
5828#line 631
5829 page = next;
5830#line 631
5831 __cil_tmp95 = (unsigned long )next;
5832#line 631
5833 __cil_tmp96 = __cil_tmp95 + 32;
5834#line 631
5835 __cil_tmp97 = *((struct list_head **)__cil_tmp96);
5836#line 631
5837 __mptr___1 = (struct list_head const *)__cil_tmp97;
5838#line 631
5839 __cil_tmp98 = (struct page *)0;
5840#line 631
5841 __cil_tmp99 = (unsigned long )__cil_tmp98;
5842#line 631
5843 __cil_tmp100 = __cil_tmp99 + 32;
5844#line 631
5845 __cil_tmp101 = (struct list_head *)__cil_tmp100;
5846#line 631
5847 __cil_tmp102 = (unsigned int )__cil_tmp101;
5848#line 631
5849 __cil_tmp103 = (char *)__mptr___1;
5850#line 631
5851 __cil_tmp104 = __cil_tmp103 - __cil_tmp102;
5852#line 631
5853 next = (struct page *)__cil_tmp104;
5854 }
5855 while_break___1: ;
5856 }
5857#line 645
5858 __cil_tmp105 = & _min1___0;
5859#line 645
5860 __cil_tmp106 = (unsigned long )b;
5861#line 645
5862 __cil_tmp107 = __cil_tmp106 + 52;
5863#line 645
5864 __cil_tmp108 = *((unsigned int *)__cil_tmp107);
5865#line 645
5866 *__cil_tmp105 = __cil_tmp108 + 16U;
5867#line 645
5868 __cil_tmp109 = & _min2___0;
5869#line 645
5870 *__cil_tmp109 = 16384U;
5871 {
5872#line 645
5873 __cil_tmp110 = & _min2___0;
5874#line 645
5875 __cil_tmp111 = *__cil_tmp110;
5876#line 645
5877 __cil_tmp112 = & _min1___0;
5878#line 645
5879 __cil_tmp113 = *__cil_tmp112;
5880#line 645
5881 if (__cil_tmp113 < __cil_tmp111) {
5882#line 645
5883 __cil_tmp114 = & _min1___0;
5884#line 645
5885 tmp___11 = *__cil_tmp114;
5886 } else {
5887#line 645
5888 __cil_tmp115 = & _min2___0;
5889#line 645
5890 tmp___11 = *__cil_tmp115;
5891 }
5892 }
5893#line 645
5894 __cil_tmp116 = (unsigned long )b;
5895#line 645
5896 __cil_tmp117 = __cil_tmp116 + 52;
5897#line 645
5898 *((unsigned int *)__cil_tmp117) = tmp___11;
5899#line 647
5900 return;
5901}
5902}
5903#line 653 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
5904static void vmballoon_work(struct work_struct *work )
5905{ struct delayed_work *dwork ;
5906 struct delayed_work *tmp___7 ;
5907 struct vmballoon *b ;
5908 struct delayed_work const *__mptr ;
5909 unsigned int target ;
5910 bool tmp___8 ;
5911 unsigned long tmp___9 ;
5912 struct vmballoon *__cil_tmp9 ;
5913 unsigned long __cil_tmp10 ;
5914 unsigned long __cil_tmp11 ;
5915 struct delayed_work *__cil_tmp12 ;
5916 unsigned int __cil_tmp13 ;
5917 char *__cil_tmp14 ;
5918 char *__cil_tmp15 ;
5919 unsigned long __cil_tmp16 ;
5920 unsigned long __cil_tmp17 ;
5921 unsigned long __cil_tmp18 ;
5922 unsigned long __cil_tmp19 ;
5923 unsigned int __cil_tmp20 ;
5924 unsigned long __cil_tmp21 ;
5925 unsigned long __cil_tmp22 ;
5926 unsigned long __cil_tmp23 ;
5927 unsigned long __cil_tmp24 ;
5928 unsigned int __cil_tmp25 ;
5929 unsigned long __cil_tmp26 ;
5930 unsigned long __cil_tmp27 ;
5931 unsigned long __cil_tmp28 ;
5932 unsigned long __cil_tmp29 ;
5933 unsigned int __cil_tmp30 ;
5934 unsigned long __cil_tmp31 ;
5935 unsigned long __cil_tmp32 ;
5936 unsigned int *__cil_tmp33 ;
5937 unsigned int *__cil_tmp34 ;
5938 unsigned int __cil_tmp35 ;
5939 unsigned long __cil_tmp36 ;
5940 unsigned long __cil_tmp37 ;
5941 unsigned int __cil_tmp38 ;
5942 unsigned int *__cil_tmp39 ;
5943 unsigned int __cil_tmp40 ;
5944 unsigned long __cil_tmp41 ;
5945 unsigned long __cil_tmp42 ;
5946 unsigned int __cil_tmp43 ;
5947
5948 {
5949 {
5950#line 655
5951 tmp___7 = to_delayed_work(work);
5952#line 655
5953 dwork = tmp___7;
5954#line 656
5955 __mptr = (struct delayed_work const *)dwork;
5956#line 656
5957 __cil_tmp9 = (struct vmballoon *)0;
5958#line 656
5959 __cil_tmp10 = (unsigned long )__cil_tmp9;
5960#line 656
5961 __cil_tmp11 = __cil_tmp10 + 256;
5962#line 656
5963 __cil_tmp12 = (struct delayed_work *)__cil_tmp11;
5964#line 656
5965 __cil_tmp13 = (unsigned int )__cil_tmp12;
5966#line 656
5967 __cil_tmp14 = (char *)__mptr;
5968#line 656
5969 __cil_tmp15 = __cil_tmp14 - __cil_tmp13;
5970#line 656
5971 b = (struct vmballoon *)__cil_tmp15;
5972#line 659
5973 __cil_tmp16 = (unsigned long )b;
5974#line 659
5975 __cil_tmp17 = __cil_tmp16 + 60;
5976#line 659
5977 __cil_tmp18 = (unsigned long )b;
5978#line 659
5979 __cil_tmp19 = __cil_tmp18 + 60;
5980#line 659
5981 __cil_tmp20 = *((unsigned int *)__cil_tmp19);
5982#line 659
5983 *((unsigned int *)__cil_tmp17) = __cil_tmp20 + 1U;
5984 }
5985 {
5986#line 661
5987 __cil_tmp21 = (unsigned long )b;
5988#line 661
5989 __cil_tmp22 = __cil_tmp21 + 44;
5990#line 661
5991 if (*((bool *)__cil_tmp22)) {
5992 {
5993#line 662
5994 vmballoon_reset(b);
5995 }
5996 } else {
5997
5998 }
5999 }
6000 {
6001#line 664
6002 __cil_tmp23 = (unsigned long )b;
6003#line 664
6004 __cil_tmp24 = __cil_tmp23 + 56;
6005#line 664
6006 __cil_tmp25 = *((unsigned int *)__cil_tmp24);
6007#line 664
6008 if (__cil_tmp25 > 0U) {
6009#line 665
6010 __cil_tmp26 = (unsigned long )b;
6011#line 665
6012 __cil_tmp27 = __cil_tmp26 + 56;
6013#line 665
6014 __cil_tmp28 = (unsigned long )b;
6015#line 665
6016 __cil_tmp29 = __cil_tmp28 + 56;
6017#line 665
6018 __cil_tmp30 = *((unsigned int *)__cil_tmp29);
6019#line 665
6020 *((unsigned int *)__cil_tmp27) = __cil_tmp30 - 1U;
6021 } else {
6022
6023 }
6024 }
6025 {
6026#line 667
6027 tmp___8 = vmballoon_send_get_target(b, & target);
6028 }
6029#line 667
6030 if (tmp___8) {
6031#line 669
6032 __cil_tmp31 = (unsigned long )b;
6033#line 669
6034 __cil_tmp32 = __cil_tmp31 + 40;
6035#line 669
6036 __cil_tmp33 = & target;
6037#line 669
6038 *((unsigned int *)__cil_tmp32) = *__cil_tmp33;
6039 {
6040#line 671
6041 __cil_tmp34 = & target;
6042#line 671
6043 __cil_tmp35 = *__cil_tmp34;
6044#line 671
6045 __cil_tmp36 = (unsigned long )b;
6046#line 671
6047 __cil_tmp37 = __cil_tmp36 + 36;
6048#line 671
6049 __cil_tmp38 = *((unsigned int *)__cil_tmp37);
6050#line 671
6051 if (__cil_tmp38 < __cil_tmp35) {
6052 {
6053#line 672
6054 vmballoon_inflate(b);
6055 }
6056 } else {
6057 {
6058#line 673
6059 __cil_tmp39 = & target;
6060#line 673
6061 __cil_tmp40 = *__cil_tmp39;
6062#line 673
6063 __cil_tmp41 = (unsigned long )b;
6064#line 673
6065 __cil_tmp42 = __cil_tmp41 + 36;
6066#line 673
6067 __cil_tmp43 = *((unsigned int *)__cil_tmp42);
6068#line 673
6069 if (__cil_tmp43 > __cil_tmp40) {
6070 {
6071#line 674
6072 vmballoon_deflate(b);
6073 }
6074 } else {
6075
6076 }
6077 }
6078 }
6079 }
6080 } else {
6081
6082 }
6083 {
6084#line 681
6085 tmp___9 = round_jiffies_relative(250UL);
6086#line 681
6087 queue_delayed_work(system_freezable_wq, dwork, tmp___9);
6088 }
6089#line 683
6090 return;
6091}
6092}
6093#line 690 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6094static int vmballoon_debug_show(struct seq_file *f , void *offset )
6095{ struct vmballoon *b ;
6096 struct vmballoon_stats *stats ;
6097 unsigned long __cil_tmp5 ;
6098 unsigned long __cil_tmp6 ;
6099 void *__cil_tmp7 ;
6100 unsigned long __cil_tmp8 ;
6101 unsigned long __cil_tmp9 ;
6102 unsigned long __cil_tmp10 ;
6103 unsigned long __cil_tmp11 ;
6104 unsigned int __cil_tmp12 ;
6105 unsigned long __cil_tmp13 ;
6106 unsigned long __cil_tmp14 ;
6107 unsigned int __cil_tmp15 ;
6108 unsigned long __cil_tmp16 ;
6109 unsigned long __cil_tmp17 ;
6110 unsigned int __cil_tmp18 ;
6111 unsigned long __cil_tmp19 ;
6112 unsigned long __cil_tmp20 ;
6113 unsigned int __cil_tmp21 ;
6114 unsigned int __cil_tmp22 ;
6115 unsigned long __cil_tmp23 ;
6116 unsigned long __cil_tmp24 ;
6117 unsigned int __cil_tmp25 ;
6118 unsigned long __cil_tmp26 ;
6119 unsigned long __cil_tmp27 ;
6120 unsigned int __cil_tmp28 ;
6121 unsigned long __cil_tmp29 ;
6122 unsigned long __cil_tmp30 ;
6123 unsigned int __cil_tmp31 ;
6124 unsigned long __cil_tmp32 ;
6125 unsigned long __cil_tmp33 ;
6126 unsigned int __cil_tmp34 ;
6127 unsigned long __cil_tmp35 ;
6128 unsigned long __cil_tmp36 ;
6129 unsigned int __cil_tmp37 ;
6130 unsigned long __cil_tmp38 ;
6131 unsigned long __cil_tmp39 ;
6132 unsigned int __cil_tmp40 ;
6133 unsigned long __cil_tmp41 ;
6134 unsigned long __cil_tmp42 ;
6135 unsigned int __cil_tmp43 ;
6136 unsigned long __cil_tmp44 ;
6137 unsigned long __cil_tmp45 ;
6138 unsigned int __cil_tmp46 ;
6139 unsigned long __cil_tmp47 ;
6140 unsigned long __cil_tmp48 ;
6141 unsigned int __cil_tmp49 ;
6142 unsigned long __cil_tmp50 ;
6143 unsigned long __cil_tmp51 ;
6144 unsigned int __cil_tmp52 ;
6145 unsigned long __cil_tmp53 ;
6146 unsigned long __cil_tmp54 ;
6147 unsigned int __cil_tmp55 ;
6148 unsigned long __cil_tmp56 ;
6149 unsigned long __cil_tmp57 ;
6150 unsigned int __cil_tmp58 ;
6151 unsigned long __cil_tmp59 ;
6152 unsigned long __cil_tmp60 ;
6153 unsigned int __cil_tmp61 ;
6154 unsigned long __cil_tmp62 ;
6155 unsigned long __cil_tmp63 ;
6156 unsigned int __cil_tmp64 ;
6157 unsigned long __cil_tmp65 ;
6158 unsigned long __cil_tmp66 ;
6159 unsigned int __cil_tmp67 ;
6160 unsigned long __cil_tmp68 ;
6161 unsigned long __cil_tmp69 ;
6162 unsigned int __cil_tmp70 ;
6163 unsigned long __cil_tmp71 ;
6164 unsigned long __cil_tmp72 ;
6165 unsigned int __cil_tmp73 ;
6166
6167 {
6168 {
6169#line 692
6170 __cil_tmp5 = (unsigned long )f;
6171#line 692
6172 __cil_tmp6 = __cil_tmp5 + 144;
6173#line 692
6174 __cil_tmp7 = *((void **)__cil_tmp6);
6175#line 692
6176 b = (struct vmballoon *)__cil_tmp7;
6177#line 693
6178 __cil_tmp8 = (unsigned long )b;
6179#line 693
6180 __cil_tmp9 = __cil_tmp8 + 60;
6181#line 693
6182 stats = (struct vmballoon_stats *)__cil_tmp9;
6183#line 696
6184 __cil_tmp10 = (unsigned long )b;
6185#line 696
6186 __cil_tmp11 = __cil_tmp10 + 40;
6187#line 696
6188 __cil_tmp12 = *((unsigned int *)__cil_tmp11);
6189#line 696
6190 __cil_tmp13 = (unsigned long )b;
6191#line 696
6192 __cil_tmp14 = __cil_tmp13 + 36;
6193#line 696
6194 __cil_tmp15 = *((unsigned int *)__cil_tmp14);
6195#line 696
6196 seq_printf(f, "target: %8d pages\ncurrent: %8d pages\n",
6197 __cil_tmp12, __cil_tmp15);
6198#line 702
6199 __cil_tmp16 = (unsigned long )b;
6200#line 702
6201 __cil_tmp17 = __cil_tmp16 + 48;
6202#line 702
6203 __cil_tmp18 = *((unsigned int *)__cil_tmp17);
6204#line 702
6205 __cil_tmp19 = (unsigned long )b;
6206#line 702
6207 __cil_tmp20 = __cil_tmp19 + 52;
6208#line 702
6209 __cil_tmp21 = *((unsigned int *)__cil_tmp20);
6210#line 702
6211 seq_printf(f, "rateNoSleepAlloc: %8d pages/sec\nrateSleepAlloc: %8d pages/sec\nrateFree: %8d pages/sec\n",
6212 16384U, __cil_tmp18, __cil_tmp21);
6213#line 709
6214 __cil_tmp22 = *((unsigned int *)stats);
6215#line 709
6216 __cil_tmp23 = (unsigned long )stats;
6217#line 709
6218 __cil_tmp24 = __cil_tmp23 + 56;
6219#line 709
6220 __cil_tmp25 = *((unsigned int *)__cil_tmp24);
6221#line 709
6222 __cil_tmp26 = (unsigned long )stats;
6223#line 709
6224 __cil_tmp27 = __cil_tmp26 + 60;
6225#line 709
6226 __cil_tmp28 = *((unsigned int *)__cil_tmp27);
6227#line 709
6228 __cil_tmp29 = (unsigned long )stats;
6229#line 709
6230 __cil_tmp30 = __cil_tmp29 + 64;
6231#line 709
6232 __cil_tmp31 = *((unsigned int *)__cil_tmp30);
6233#line 709
6234 __cil_tmp32 = (unsigned long )stats;
6235#line 709
6236 __cil_tmp33 = __cil_tmp32 + 68;
6237#line 709
6238 __cil_tmp34 = *((unsigned int *)__cil_tmp33);
6239#line 709
6240 __cil_tmp35 = (unsigned long )stats;
6241#line 709
6242 __cil_tmp36 = __cil_tmp35 + 32;
6243#line 709
6244 __cil_tmp37 = *((unsigned int *)__cil_tmp36);
6245#line 709
6246 __cil_tmp38 = (unsigned long )stats;
6247#line 709
6248 __cil_tmp39 = __cil_tmp38 + 36;
6249#line 709
6250 __cil_tmp40 = *((unsigned int *)__cil_tmp39);
6251#line 709
6252 __cil_tmp41 = (unsigned long )stats;
6253#line 709
6254 __cil_tmp42 = __cil_tmp41 + 40;
6255#line 709
6256 __cil_tmp43 = *((unsigned int *)__cil_tmp42);
6257#line 709
6258 __cil_tmp44 = (unsigned long )stats;
6259#line 709
6260 __cil_tmp45 = __cil_tmp44 + 44;
6261#line 709
6262 __cil_tmp46 = *((unsigned int *)__cil_tmp45);
6263#line 709
6264 __cil_tmp47 = (unsigned long )stats;
6265#line 709
6266 __cil_tmp48 = __cil_tmp47 + 48;
6267#line 709
6268 __cil_tmp49 = *((unsigned int *)__cil_tmp48);
6269#line 709
6270 __cil_tmp50 = (unsigned long )stats;
6271#line 709
6272 __cil_tmp51 = __cil_tmp50 + 52;
6273#line 709
6274 __cil_tmp52 = *((unsigned int *)__cil_tmp51);
6275#line 709
6276 __cil_tmp53 = (unsigned long )stats;
6277#line 709
6278 __cil_tmp54 = __cil_tmp53 + 4;
6279#line 709
6280 __cil_tmp55 = *((unsigned int *)__cil_tmp54);
6281#line 709
6282 __cil_tmp56 = (unsigned long )stats;
6283#line 709
6284 __cil_tmp57 = __cil_tmp56 + 8;
6285#line 709
6286 __cil_tmp58 = *((unsigned int *)__cil_tmp57);
6287#line 709
6288 __cil_tmp59 = (unsigned long )stats;
6289#line 709
6290 __cil_tmp60 = __cil_tmp59 + 12;
6291#line 709
6292 __cil_tmp61 = *((unsigned int *)__cil_tmp60);
6293#line 709
6294 __cil_tmp62 = (unsigned long )stats;
6295#line 709
6296 __cil_tmp63 = __cil_tmp62 + 16;
6297#line 709
6298 __cil_tmp64 = *((unsigned int *)__cil_tmp63);
6299#line 709
6300 __cil_tmp65 = (unsigned long )stats;
6301#line 709
6302 __cil_tmp66 = __cil_tmp65 + 28;
6303#line 709
6304 __cil_tmp67 = *((unsigned int *)__cil_tmp66);
6305#line 709
6306 __cil_tmp68 = (unsigned long )stats;
6307#line 709
6308 __cil_tmp69 = __cil_tmp68 + 20;
6309#line 709
6310 __cil_tmp70 = *((unsigned int *)__cil_tmp69);
6311#line 709
6312 __cil_tmp71 = (unsigned long )stats;
6313#line 709
6314 __cil_tmp72 = __cil_tmp71 + 24;
6315#line 709
6316 __cil_tmp73 = *((unsigned int *)__cil_tmp72);
6317#line 709
6318 seq_printf(f, "\ntimer: %8u\nstart: %8u (%4u failed)\nguestType: %8u (%4u failed)\nlock: %8u (%4u failed)\nunlock: %8u (%4u failed)\ntarget: %8u (%4u failed)\nprimNoSleepAlloc: %8u (%4u failed)\nprimCanSleepAlloc: %8u (%4u failed)\nprimFree: %8u\nerrAlloc: %8u\nerrFree: %8u\n",
6319 __cil_tmp22, __cil_tmp25, __cil_tmp28, __cil_tmp31, __cil_tmp34, __cil_tmp37,
6320 __cil_tmp40, __cil_tmp43, __cil_tmp46, __cil_tmp49, __cil_tmp52, __cil_tmp55,
6321 __cil_tmp58, __cil_tmp61, __cil_tmp64, __cil_tmp67, __cil_tmp70, __cil_tmp73);
6322 }
6323#line 733
6324 return (0);
6325}
6326}
6327#line 736 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6328static int vmballoon_debug_open(struct inode *inode , struct file *file )
6329{ int tmp___7 ;
6330 unsigned long __cil_tmp4 ;
6331 unsigned long __cil_tmp5 ;
6332 void *__cil_tmp6 ;
6333
6334 {
6335 {
6336#line 738
6337 __cil_tmp4 = (unsigned long )inode;
6338#line 738
6339 __cil_tmp5 = __cil_tmp4 + 696;
6340#line 738
6341 __cil_tmp6 = *((void **)__cil_tmp5);
6342#line 738
6343 tmp___7 = single_open(file, & vmballoon_debug_show, __cil_tmp6);
6344 }
6345#line 738
6346 return (tmp___7);
6347}
6348}
6349#line 741 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6350static struct file_operations const vmballoon_debug_fops =
6351#line 741
6352 {& __this_module, & seq_lseek, & seq_read, (ssize_t (*)(struct file * , char const * ,
6353 size_t , loff_t * ))0,
6354 (ssize_t (*)(struct kiocb * , struct iovec const * , unsigned long , loff_t ))0,
6355 (ssize_t (*)(struct kiocb * , struct iovec const * , unsigned long , loff_t ))0,
6356 (int (*)(struct file * , void * , int (*)(void * , char const * , int , loff_t ,
6357 u64 , unsigned int ) ))0, (unsigned int (*)(struct file * ,
6358 struct poll_table_struct * ))0,
6359 (long (*)(struct file * , unsigned int , unsigned long ))0, (long (*)(struct file * ,
6360 unsigned int ,
6361 unsigned long ))0,
6362 (int (*)(struct file * , struct vm_area_struct * ))0, & vmballoon_debug_open,
6363 (int (*)(struct file * , fl_owner_t id ))0, & single_release, (int (*)(struct file * ,
6364 loff_t ,
6365 loff_t ,
6366 int datasync ))0,
6367 (int (*)(struct kiocb * , int datasync ))0, (int (*)(int , struct file * , int ))0,
6368 (int (*)(struct file * , int , struct file_lock * ))0, (ssize_t (*)(struct file * ,
6369 struct page * ,
6370 int , size_t ,
6371 loff_t * ,
6372 int ))0,
6373 (unsigned long (*)(struct file * , unsigned long , unsigned long , unsigned long ,
6374 unsigned long ))0, (int (*)(int ))0, (int (*)(struct file * ,
6375 int , struct file_lock * ))0,
6376 (ssize_t (*)(struct pipe_inode_info * , struct file * , loff_t * , size_t , unsigned int ))0,
6377 (ssize_t (*)(struct file * , loff_t * , struct pipe_inode_info * , size_t , unsigned int ))0,
6378 (int (*)(struct file * , long , struct file_lock ** ))0, (long (*)(struct file *file ,
6379 int mode ,
6380 loff_t offset ,
6381 loff_t len ))0};
6382#line 749
6383static int vmballoon_debugfs_init(struct vmballoon *b ) __attribute__((__section__(".init.text"),
6384__no_instrument_function__)) ;
6385#line 749 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6386static int vmballoon_debugfs_init(struct vmballoon *b )
6387{ int error ;
6388 long tmp___7 ;
6389 long tmp___8 ;
6390 unsigned long __cil_tmp5 ;
6391 unsigned long __cil_tmp6 ;
6392 umode_t __cil_tmp7 ;
6393 void *__cil_tmp8 ;
6394 struct dentry *__cil_tmp9 ;
6395 void *__cil_tmp10 ;
6396 unsigned long __cil_tmp11 ;
6397 unsigned long __cil_tmp12 ;
6398 struct dentry *__cil_tmp13 ;
6399 void const *__cil_tmp14 ;
6400 unsigned long __cil_tmp15 ;
6401 unsigned long __cil_tmp16 ;
6402 struct dentry *__cil_tmp17 ;
6403 void const *__cil_tmp18 ;
6404
6405 {
6406 {
6407#line 753
6408 __cil_tmp5 = (unsigned long )b;
6409#line 753
6410 __cil_tmp6 = __cil_tmp5 + 136;
6411#line 753
6412 __cil_tmp7 = (umode_t )292;
6413#line 753
6414 __cil_tmp8 = (void *)0;
6415#line 753
6416 __cil_tmp9 = (struct dentry *)__cil_tmp8;
6417#line 753
6418 __cil_tmp10 = (void *)b;
6419#line 753
6420 *((struct dentry **)__cil_tmp6) = debugfs_create_file("vmmemctl", __cil_tmp7, __cil_tmp9,
6421 __cil_tmp10, & vmballoon_debug_fops);
6422#line 755
6423 __cil_tmp11 = (unsigned long )b;
6424#line 755
6425 __cil_tmp12 = __cil_tmp11 + 136;
6426#line 755
6427 __cil_tmp13 = *((struct dentry **)__cil_tmp12);
6428#line 755
6429 __cil_tmp14 = (void const *)__cil_tmp13;
6430#line 755
6431 tmp___8 = (long )IS_ERR(__cil_tmp14);
6432 }
6433#line 755
6434 if (tmp___8) {
6435 {
6436#line 756
6437 __cil_tmp15 = (unsigned long )b;
6438#line 756
6439 __cil_tmp16 = __cil_tmp15 + 136;
6440#line 756
6441 __cil_tmp17 = *((struct dentry **)__cil_tmp16);
6442#line 756
6443 __cil_tmp18 = (void const *)__cil_tmp17;
6444#line 756
6445 tmp___7 = (long )PTR_ERR(__cil_tmp18);
6446#line 756
6447 error = (int )tmp___7;
6448#line 757
6449 printk("<3>vmw_balloon: failed to create debugfs entry, error: %d\n", error);
6450 }
6451#line 758
6452 return (error);
6453 } else {
6454
6455 }
6456#line 761
6457 return (0);
6458}
6459}
6460#line 764
6461static void vmballoon_debugfs_exit(struct vmballoon *b ) __attribute__((__section__(".exit.text"),
6462__no_instrument_function__)) ;
6463#line 764 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6464static void vmballoon_debugfs_exit(struct vmballoon *b )
6465{ unsigned long __cil_tmp2 ;
6466 unsigned long __cil_tmp3 ;
6467 struct dentry *__cil_tmp4 ;
6468
6469 {
6470 {
6471#line 766
6472 __cil_tmp2 = (unsigned long )b;
6473#line 766
6474 __cil_tmp3 = __cil_tmp2 + 136;
6475#line 766
6476 __cil_tmp4 = *((struct dentry **)__cil_tmp3);
6477#line 766
6478 debugfs_remove(__cil_tmp4);
6479 }
6480#line 767
6481 return;
6482}
6483}
6484#line 782
6485static int vmballoon_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
6486#line 782 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6487static int vmballoon_init(void)
6488{ int error ;
6489 atomic_long_t __constr_expr_0 ;
6490 bool tmp___7 ;
6491 bool tmp___8 ;
6492 unsigned long __cil_tmp5 ;
6493 unsigned long __cil_tmp6 ;
6494 struct vmballoon *__cil_tmp7 ;
6495 struct list_head *__cil_tmp8 ;
6496 unsigned long __cil_tmp9 ;
6497 struct list_head *__cil_tmp10 ;
6498 unsigned long __cil_tmp11 ;
6499 unsigned long __cil_tmp12 ;
6500 unsigned long __cil_tmp13 ;
6501 struct work_struct *__cil_tmp14 ;
6502 unsigned long __cil_tmp15 ;
6503 unsigned long __cil_tmp16 ;
6504 unsigned long __cil_tmp17 ;
6505 unsigned long __cil_tmp18 ;
6506 struct list_head *__cil_tmp19 ;
6507 unsigned long __cil_tmp20 ;
6508 unsigned long __cil_tmp21 ;
6509 unsigned long __cil_tmp22 ;
6510 unsigned long __cil_tmp23 ;
6511 unsigned long __cil_tmp24 ;
6512 struct timer_list *__cil_tmp25 ;
6513 void *__cil_tmp26 ;
6514 char const *__cil_tmp27 ;
6515 void *__cil_tmp28 ;
6516 struct lock_class_key *__cil_tmp29 ;
6517 unsigned long __cil_tmp30 ;
6518 struct delayed_work *__cil_tmp31 ;
6519 long __constr_expr_0_counter32 ;
6520
6521 {
6522 {
6523#line 790
6524 __cil_tmp5 = (unsigned long )(& x86_hyper_vmware);
6525#line 790
6526 __cil_tmp6 = (unsigned long )x86_hyper;
6527#line 790
6528 if (__cil_tmp6 != __cil_tmp5) {
6529#line 791
6530 return (-19);
6531 } else {
6532
6533 }
6534 }
6535 {
6536#line 793
6537 __cil_tmp7 = & balloon;
6538#line 793
6539 __cil_tmp8 = (struct list_head *)__cil_tmp7;
6540#line 793
6541 INIT_LIST_HEAD(__cil_tmp8);
6542#line 794
6543 __cil_tmp9 = (unsigned long )(& balloon) + 16;
6544#line 794
6545 __cil_tmp10 = (struct list_head *)__cil_tmp9;
6546#line 794
6547 INIT_LIST_HEAD(__cil_tmp10);
6548#line 797
6549 __cil_tmp11 = (unsigned long )(& balloon) + 48;
6550#line 797
6551 *((unsigned int *)__cil_tmp11) = 2048U;
6552#line 798
6553 __cil_tmp12 = (unsigned long )(& balloon) + 52;
6554#line 798
6555 *((unsigned int *)__cil_tmp12) = 16384U;
6556 }
6557 {
6558#line 800
6559 while (1) {
6560 while_continue: ;
6561 {
6562#line 800
6563 while (1) {
6564 while_continue___0: ;
6565 {
6566#line 800
6567 while (1) {
6568 while_continue___1: ;
6569 {
6570#line 800
6571 __cil_tmp13 = (unsigned long )(& balloon) + 256;
6572#line 800
6573 __cil_tmp14 = (struct work_struct *)__cil_tmp13;
6574#line 800
6575 __init_work(__cil_tmp14, 0);
6576#line 800
6577 __constr_expr_0_counter32 = 2097664L;
6578#line 800
6579 __cil_tmp15 = (unsigned long )(& balloon) + 256;
6580#line 800
6581 ((atomic_long_t *)__cil_tmp15)->counter = __constr_expr_0_counter32;
6582#line 800
6583 __cil_tmp16 = 0 + 8;
6584#line 800
6585 __cil_tmp17 = 256 + __cil_tmp16;
6586#line 800
6587 __cil_tmp18 = (unsigned long )(& balloon) + __cil_tmp17;
6588#line 800
6589 __cil_tmp19 = (struct list_head *)__cil_tmp18;
6590#line 800
6591 INIT_LIST_HEAD(__cil_tmp19);
6592 }
6593 {
6594#line 800
6595 while (1) {
6596 while_continue___2: ;
6597#line 800
6598 __cil_tmp20 = 0 + 24;
6599#line 800
6600 __cil_tmp21 = 256 + __cil_tmp20;
6601#line 800
6602 __cil_tmp22 = (unsigned long )(& balloon) + __cil_tmp21;
6603#line 800
6604 *((void (**)(struct work_struct *work ))__cil_tmp22) = & vmballoon_work;
6605#line 800
6606 goto while_break___2;
6607 }
6608 while_break___2: ;
6609 }
6610#line 800
6611 goto while_break___1;
6612 }
6613 while_break___1: ;
6614 }
6615#line 800
6616 goto while_break___0;
6617 }
6618 while_break___0: ;
6619 }
6620 {
6621#line 800
6622 __cil_tmp23 = 256 + 32;
6623#line 800
6624 __cil_tmp24 = (unsigned long )(& balloon) + __cil_tmp23;
6625#line 800
6626 __cil_tmp25 = (struct timer_list *)__cil_tmp24;
6627#line 800
6628 __cil_tmp26 = (void *)0;
6629#line 800
6630 __cil_tmp27 = (char const *)__cil_tmp26;
6631#line 800
6632 __cil_tmp28 = (void *)0;
6633#line 800
6634 __cil_tmp29 = (struct lock_class_key *)__cil_tmp28;
6635#line 800
6636 init_timer_key(__cil_tmp25, __cil_tmp27, __cil_tmp29);
6637 }
6638#line 800
6639 goto while_break;
6640 }
6641 while_break: ;
6642 }
6643 {
6644#line 805
6645 tmp___7 = vmballoon_send_start(& balloon);
6646 }
6647#line 805
6648 if (tmp___7) {
6649
6650 } else {
6651 {
6652#line 806
6653 printk("<3>vmw_balloon: failed to send start command to the host\n");
6654 }
6655#line 807
6656 return (-5);
6657 }
6658 {
6659#line 810
6660 tmp___8 = vmballoon_send_guest_id(& balloon);
6661 }
6662#line 810
6663 if (tmp___8) {
6664
6665 } else {
6666 {
6667#line 811
6668 printk("<3>vmw_balloon: failed to send guest ID to the host\n");
6669 }
6670#line 812
6671 return (-5);
6672 }
6673 {
6674#line 815
6675 error = vmballoon_debugfs_init(& balloon);
6676 }
6677#line 816
6678 if (error) {
6679#line 817
6680 return (error);
6681 } else {
6682
6683 }
6684 {
6685#line 819
6686 __cil_tmp30 = (unsigned long )(& balloon) + 256;
6687#line 819
6688 __cil_tmp31 = (struct delayed_work *)__cil_tmp30;
6689#line 819
6690 queue_delayed_work(system_freezable_wq, __cil_tmp31, 0UL);
6691 }
6692#line 821
6693 return (0);
6694}
6695}
6696#line 823 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6697int init_module(void)
6698{ int tmp___7 ;
6699
6700 {
6701 {
6702#line 823
6703 tmp___7 = vmballoon_init();
6704 }
6705#line 823
6706 return (tmp___7);
6707}
6708}
6709#line 825
6710static void vmballoon_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
6711#line 825 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6712static void vmballoon_exit(void)
6713{ unsigned long __cil_tmp1 ;
6714 struct delayed_work *__cil_tmp2 ;
6715
6716 {
6717 {
6718#line 827
6719 __cil_tmp1 = (unsigned long )(& balloon) + 256;
6720#line 827
6721 __cil_tmp2 = (struct delayed_work *)__cil_tmp1;
6722#line 827
6723 cancel_delayed_work_sync(__cil_tmp2);
6724#line 829
6725 vmballoon_debugfs_exit(& balloon);
6726#line 836
6727 vmballoon_send_start(& balloon);
6728#line 837
6729 vmballoon_pop(& balloon);
6730 }
6731#line 838
6732 return;
6733}
6734}
6735#line 839 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6736void cleanup_module(void)
6737{
6738
6739 {
6740 {
6741#line 839
6742 vmballoon_exit();
6743 }
6744#line 839
6745 return;
6746}
6747}
6748#line 857
6749void ldv_check_final_state(void) ;
6750#line 860
6751extern void ldv_check_return_value(int res ) ;
6752#line 863
6753extern void ldv_initialize(void) ;
6754#line 866
6755extern int __VERIFIER_nondet_int(void) ;
6756#line 869 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6757int LDV_IN_INTERRUPT ;
6758#line 943 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6759static int res_vmballoon_debug_open_15 ;
6760#line 872 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
6761void main(void)
6762{ struct inode *var_group1 ;
6763 struct file *var_group2 ;
6764 int tmp___7 ;
6765 int ldv_s_vmballoon_debug_fops_file_operations ;
6766 int tmp___8 ;
6767 int tmp___9 ;
6768 int __cil_tmp7 ;
6769
6770 {
6771 {
6772#line 955
6773 LDV_IN_INTERRUPT = 1;
6774#line 964
6775 ldv_initialize();
6776#line 1029
6777 tmp___7 = vmballoon_init();
6778 }
6779#line 1029
6780 if (tmp___7) {
6781#line 1030
6782 goto ldv_final;
6783 } else {
6784
6785 }
6786#line 1031
6787 ldv_s_vmballoon_debug_fops_file_operations = 0;
6788 {
6789#line 1034
6790 while (1) {
6791 while_continue: ;
6792 {
6793#line 1034
6794 tmp___9 = __VERIFIER_nondet_int();
6795 }
6796#line 1034
6797 if (tmp___9) {
6798
6799 } else {
6800 {
6801#line 1034
6802 __cil_tmp7 = ldv_s_vmballoon_debug_fops_file_operations == 0;
6803#line 1034
6804 if (! __cil_tmp7) {
6805
6806 } else {
6807#line 1034
6808 goto while_break;
6809 }
6810 }
6811 }
6812 {
6813#line 1038
6814 tmp___8 = __VERIFIER_nondet_int();
6815 }
6816#line 1040
6817 if (tmp___8 == 0) {
6818#line 1040
6819 goto case_0;
6820 } else {
6821 {
6822#line 1120
6823 goto switch_default;
6824#line 1038
6825 if (0) {
6826 case_0:
6827#line 1043
6828 if (ldv_s_vmballoon_debug_fops_file_operations == 0) {
6829 {
6830#line 1105
6831 res_vmballoon_debug_open_15 = vmballoon_debug_open(var_group1, var_group2);
6832#line 1106
6833 ldv_check_return_value(res_vmballoon_debug_open_15);
6834 }
6835#line 1107
6836 if (res_vmballoon_debug_open_15) {
6837#line 1108
6838 goto ldv_module_exit;
6839 } else {
6840
6841 }
6842#line 1113
6843 ldv_s_vmballoon_debug_fops_file_operations = 0;
6844 } else {
6845
6846 }
6847#line 1119
6848 goto switch_break;
6849 switch_default:
6850#line 1120
6851 goto switch_break;
6852 } else {
6853 switch_break: ;
6854 }
6855 }
6856 }
6857 }
6858 while_break: ;
6859 }
6860 ldv_module_exit:
6861 {
6862#line 1191
6863 vmballoon_exit();
6864 }
6865 ldv_final:
6866 {
6867#line 1194
6868 ldv_check_final_state();
6869 }
6870#line 1197
6871 return;
6872}
6873}
6874#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6875void ldv_blast_assert(void)
6876{
6877
6878 {
6879 ERROR:
6880#line 6
6881 goto ERROR;
6882}
6883}
6884#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6885extern int __VERIFIER_nondet_int(void) ;
6886#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6887int ldv_mutex = 1;
6888#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6889int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
6890{ int nondetermined ;
6891
6892 {
6893#line 29
6894 if (ldv_mutex == 1) {
6895
6896 } else {
6897 {
6898#line 29
6899 ldv_blast_assert();
6900 }
6901 }
6902 {
6903#line 32
6904 nondetermined = __VERIFIER_nondet_int();
6905 }
6906#line 35
6907 if (nondetermined) {
6908#line 38
6909 ldv_mutex = 2;
6910#line 40
6911 return (0);
6912 } else {
6913#line 45
6914 return (-4);
6915 }
6916}
6917}
6918#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6919int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
6920{ int nondetermined ;
6921
6922 {
6923#line 57
6924 if (ldv_mutex == 1) {
6925
6926 } else {
6927 {
6928#line 57
6929 ldv_blast_assert();
6930 }
6931 }
6932 {
6933#line 60
6934 nondetermined = __VERIFIER_nondet_int();
6935 }
6936#line 63
6937 if (nondetermined) {
6938#line 66
6939 ldv_mutex = 2;
6940#line 68
6941 return (0);
6942 } else {
6943#line 73
6944 return (-4);
6945 }
6946}
6947}
6948#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6949int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
6950{ int atomic_value_after_dec ;
6951
6952 {
6953#line 83
6954 if (ldv_mutex == 1) {
6955
6956 } else {
6957 {
6958#line 83
6959 ldv_blast_assert();
6960 }
6961 }
6962 {
6963#line 86
6964 atomic_value_after_dec = __VERIFIER_nondet_int();
6965 }
6966#line 89
6967 if (atomic_value_after_dec == 0) {
6968#line 92
6969 ldv_mutex = 2;
6970#line 94
6971 return (1);
6972 } else {
6973
6974 }
6975#line 98
6976 return (0);
6977}
6978}
6979#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6980void mutex_lock(struct mutex *lock )
6981{
6982
6983 {
6984#line 108
6985 if (ldv_mutex == 1) {
6986
6987 } else {
6988 {
6989#line 108
6990 ldv_blast_assert();
6991 }
6992 }
6993#line 110
6994 ldv_mutex = 2;
6995#line 111
6996 return;
6997}
6998}
6999#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7000int mutex_trylock(struct mutex *lock )
7001{ int nondetermined ;
7002
7003 {
7004#line 121
7005 if (ldv_mutex == 1) {
7006
7007 } else {
7008 {
7009#line 121
7010 ldv_blast_assert();
7011 }
7012 }
7013 {
7014#line 124
7015 nondetermined = __VERIFIER_nondet_int();
7016 }
7017#line 127
7018 if (nondetermined) {
7019#line 130
7020 ldv_mutex = 2;
7021#line 132
7022 return (1);
7023 } else {
7024#line 137
7025 return (0);
7026 }
7027}
7028}
7029#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7030void mutex_unlock(struct mutex *lock )
7031{
7032
7033 {
7034#line 147
7035 if (ldv_mutex == 2) {
7036
7037 } else {
7038 {
7039#line 147
7040 ldv_blast_assert();
7041 }
7042 }
7043#line 149
7044 ldv_mutex = 1;
7045#line 150
7046 return;
7047}
7048}
7049#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7050void ldv_check_final_state(void)
7051{
7052
7053 {
7054#line 156
7055 if (ldv_mutex == 1) {
7056
7057 } else {
7058 {
7059#line 156
7060 ldv_blast_assert();
7061 }
7062 }
7063#line 157
7064 return;
7065}
7066}
7067#line 1206 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4899/dscv_tempdir/dscv/ri/32_1/drivers/misc/vmw_balloon.c.common.c"
7068long s__builtin_expect(long val , long res )
7069{
7070
7071 {
7072#line 1207
7073 return (val);
7074}
7075}