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