Showing error 499

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--misc--vmw_balloon.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 6879
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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