Showing error 1085

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