Showing error 575

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--platform--x86--mxm-wmi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3424
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 22 "include/asm-generic/int-ll64.h"
   7typedef short __s16;
   8#line 23 "include/asm-generic/int-ll64.h"
   9typedef unsigned short __u16;
  10#line 25 "include/asm-generic/int-ll64.h"
  11typedef int __s32;
  12#line 26 "include/asm-generic/int-ll64.h"
  13typedef unsigned int __u32;
  14#line 29 "include/asm-generic/int-ll64.h"
  15typedef long long __s64;
  16#line 30 "include/asm-generic/int-ll64.h"
  17typedef unsigned long long __u64;
  18#line 43 "include/asm-generic/int-ll64.h"
  19typedef unsigned char u8;
  20#line 45 "include/asm-generic/int-ll64.h"
  21typedef short s16;
  22#line 46 "include/asm-generic/int-ll64.h"
  23typedef unsigned short u16;
  24#line 48 "include/asm-generic/int-ll64.h"
  25typedef int s32;
  26#line 49 "include/asm-generic/int-ll64.h"
  27typedef unsigned int u32;
  28#line 51 "include/asm-generic/int-ll64.h"
  29typedef long long s64;
  30#line 52 "include/asm-generic/int-ll64.h"
  31typedef unsigned long long u64;
  32#line 14 "include/asm-generic/posix_types.h"
  33typedef long __kernel_long_t;
  34#line 15 "include/asm-generic/posix_types.h"
  35typedef unsigned long __kernel_ulong_t;
  36#line 31 "include/asm-generic/posix_types.h"
  37typedef int __kernel_pid_t;
  38#line 52 "include/asm-generic/posix_types.h"
  39typedef unsigned int __kernel_uid32_t;
  40#line 53 "include/asm-generic/posix_types.h"
  41typedef unsigned int __kernel_gid32_t;
  42#line 75 "include/asm-generic/posix_types.h"
  43typedef __kernel_ulong_t __kernel_size_t;
  44#line 76 "include/asm-generic/posix_types.h"
  45typedef __kernel_long_t __kernel_ssize_t;
  46#line 91 "include/asm-generic/posix_types.h"
  47typedef long long __kernel_loff_t;
  48#line 92 "include/asm-generic/posix_types.h"
  49typedef __kernel_long_t __kernel_time_t;
  50#line 93 "include/asm-generic/posix_types.h"
  51typedef __kernel_long_t __kernel_clock_t;
  52#line 94 "include/asm-generic/posix_types.h"
  53typedef int __kernel_timer_t;
  54#line 95 "include/asm-generic/posix_types.h"
  55typedef int __kernel_clockid_t;
  56#line 21 "include/linux/types.h"
  57typedef __u32 __kernel_dev_t;
  58#line 24 "include/linux/types.h"
  59typedef __kernel_dev_t dev_t;
  60#line 27 "include/linux/types.h"
  61typedef unsigned short umode_t;
  62#line 30 "include/linux/types.h"
  63typedef __kernel_pid_t pid_t;
  64#line 35 "include/linux/types.h"
  65typedef __kernel_clockid_t clockid_t;
  66#line 38 "include/linux/types.h"
  67typedef _Bool bool;
  68#line 40 "include/linux/types.h"
  69typedef __kernel_uid32_t uid_t;
  70#line 41 "include/linux/types.h"
  71typedef __kernel_gid32_t gid_t;
  72#line 54 "include/linux/types.h"
  73typedef __kernel_loff_t loff_t;
  74#line 63 "include/linux/types.h"
  75typedef __kernel_size_t size_t;
  76#line 68 "include/linux/types.h"
  77typedef __kernel_ssize_t ssize_t;
  78#line 78 "include/linux/types.h"
  79typedef __kernel_time_t time_t;
  80#line 111 "include/linux/types.h"
  81typedef __s32 int32_t;
  82#line 117 "include/linux/types.h"
  83typedef __u32 uint32_t;
  84#line 142 "include/linux/types.h"
  85typedef unsigned long sector_t;
  86#line 143 "include/linux/types.h"
  87typedef unsigned long blkcnt_t;
  88#line 202 "include/linux/types.h"
  89typedef unsigned int gfp_t;
  90#line 203 "include/linux/types.h"
  91typedef unsigned int fmode_t;
  92#line 219 "include/linux/types.h"
  93struct __anonstruct_atomic_t_7 {
  94   int counter ;
  95};
  96#line 219 "include/linux/types.h"
  97typedef struct __anonstruct_atomic_t_7 atomic_t;
  98#line 224 "include/linux/types.h"
  99struct __anonstruct_atomic64_t_8 {
 100   long counter ;
 101};
 102#line 224 "include/linux/types.h"
 103typedef struct __anonstruct_atomic64_t_8 atomic64_t;
 104#line 229 "include/linux/types.h"
 105struct list_head {
 106   struct list_head *next ;
 107   struct list_head *prev ;
 108};
 109#line 233
 110struct hlist_node;
 111#line 233 "include/linux/types.h"
 112struct hlist_head {
 113   struct hlist_node *first ;
 114};
 115#line 237 "include/linux/types.h"
 116struct hlist_node {
 117   struct hlist_node *next ;
 118   struct hlist_node **pprev ;
 119};
 120#line 253 "include/linux/types.h"
 121struct rcu_head {
 122   struct rcu_head *next ;
 123   void (*func)(struct rcu_head *head ) ;
 124};
 125#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 126struct module;
 127#line 56
 128struct module;
 129#line 146 "include/linux/init.h"
 130typedef void (*ctor_fn_t)(void);
 131#line 135 "include/linux/kernel.h"
 132struct completion;
 133#line 135
 134struct completion;
 135#line 136
 136struct pt_regs;
 137#line 136
 138struct pt_regs;
 139#line 349
 140struct pid;
 141#line 349
 142struct pid;
 143#line 12 "include/linux/thread_info.h"
 144struct timespec;
 145#line 12
 146struct timespec;
 147#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
 148struct page;
 149#line 18
 150struct page;
 151#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
 152struct task_struct;
 153#line 20
 154struct task_struct;
 155#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 156struct task_struct;
 157#line 8
 158struct mm_struct;
 159#line 8
 160struct mm_struct;
 161#line 99 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 162struct pt_regs {
 163   unsigned long r15 ;
 164   unsigned long r14 ;
 165   unsigned long r13 ;
 166   unsigned long r12 ;
 167   unsigned long bp ;
 168   unsigned long bx ;
 169   unsigned long r11 ;
 170   unsigned long r10 ;
 171   unsigned long r9 ;
 172   unsigned long r8 ;
 173   unsigned long ax ;
 174   unsigned long cx ;
 175   unsigned long dx ;
 176   unsigned long si ;
 177   unsigned long di ;
 178   unsigned long orig_ax ;
 179   unsigned long ip ;
 180   unsigned long cs ;
 181   unsigned long flags ;
 182   unsigned long sp ;
 183   unsigned long ss ;
 184};
 185#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 186struct __anonstruct____missing_field_name_15 {
 187   unsigned int a ;
 188   unsigned int b ;
 189};
 190#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 191struct __anonstruct____missing_field_name_16 {
 192   u16 limit0 ;
 193   u16 base0 ;
 194   unsigned int base1 : 8 ;
 195   unsigned int type : 4 ;
 196   unsigned int s : 1 ;
 197   unsigned int dpl : 2 ;
 198   unsigned int p : 1 ;
 199   unsigned int limit : 4 ;
 200   unsigned int avl : 1 ;
 201   unsigned int l : 1 ;
 202   unsigned int d : 1 ;
 203   unsigned int g : 1 ;
 204   unsigned int base2 : 8 ;
 205};
 206#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 207union __anonunion____missing_field_name_14 {
 208   struct __anonstruct____missing_field_name_15 __annonCompField5 ;
 209   struct __anonstruct____missing_field_name_16 __annonCompField6 ;
 210};
 211#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 212struct desc_struct {
 213   union __anonunion____missing_field_name_14 __annonCompField7 ;
 214} __attribute__((__packed__)) ;
 215#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 216typedef unsigned long pgdval_t;
 217#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 218typedef unsigned long pgprotval_t;
 219#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 220struct pgprot {
 221   pgprotval_t pgprot ;
 222};
 223#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 224typedef struct pgprot pgprot_t;
 225#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 226struct __anonstruct_pgd_t_20 {
 227   pgdval_t pgd ;
 228};
 229#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 230typedef struct __anonstruct_pgd_t_20 pgd_t;
 231#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 232typedef struct page *pgtable_t;
 233#line 295
 234struct file;
 235#line 295
 236struct file;
 237#line 313
 238struct seq_file;
 239#line 313
 240struct seq_file;
 241#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 242struct page;
 243#line 47
 244struct thread_struct;
 245#line 47
 246struct thread_struct;
 247#line 50
 248struct mm_struct;
 249#line 51
 250struct desc_struct;
 251#line 52
 252struct task_struct;
 253#line 53
 254struct cpumask;
 255#line 53
 256struct cpumask;
 257#line 329
 258struct arch_spinlock;
 259#line 329
 260struct arch_spinlock;
 261#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 262struct task_struct;
 263#line 141 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
 264struct kernel_vm86_regs {
 265   struct pt_regs pt ;
 266   unsigned short es ;
 267   unsigned short __esh ;
 268   unsigned short ds ;
 269   unsigned short __dsh ;
 270   unsigned short fs ;
 271   unsigned short __fsh ;
 272   unsigned short gs ;
 273   unsigned short __gsh ;
 274};
 275#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 276union __anonunion____missing_field_name_24 {
 277   struct pt_regs *regs ;
 278   struct kernel_vm86_regs *vm86 ;
 279};
 280#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 281struct math_emu_info {
 282   long ___orig_eip ;
 283   union __anonunion____missing_field_name_24 __annonCompField8 ;
 284};
 285#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 286struct task_struct;
 287#line 10 "include/asm-generic/bug.h"
 288struct bug_entry {
 289   int bug_addr_disp ;
 290   int file_disp ;
 291   unsigned short line ;
 292   unsigned short flags ;
 293};
 294#line 12 "include/linux/bug.h"
 295struct pt_regs;
 296#line 14 "include/linux/cpumask.h"
 297struct cpumask {
 298   unsigned long bits[((4096UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 299};
 300#line 14 "include/linux/cpumask.h"
 301typedef struct cpumask cpumask_t;
 302#line 637 "include/linux/cpumask.h"
 303typedef struct cpumask *cpumask_var_t;
 304#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 305struct static_key;
 306#line 234
 307struct static_key;
 308#line 11 "include/linux/personality.h"
 309struct pt_regs;
 310#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 311struct i387_fsave_struct {
 312   u32 cwd ;
 313   u32 swd ;
 314   u32 twd ;
 315   u32 fip ;
 316   u32 fcs ;
 317   u32 foo ;
 318   u32 fos ;
 319   u32 st_space[20] ;
 320   u32 status ;
 321};
 322#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 323struct __anonstruct____missing_field_name_31 {
 324   u64 rip ;
 325   u64 rdp ;
 326};
 327#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 328struct __anonstruct____missing_field_name_32 {
 329   u32 fip ;
 330   u32 fcs ;
 331   u32 foo ;
 332   u32 fos ;
 333};
 334#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 335union __anonunion____missing_field_name_30 {
 336   struct __anonstruct____missing_field_name_31 __annonCompField12 ;
 337   struct __anonstruct____missing_field_name_32 __annonCompField13 ;
 338};
 339#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 340union __anonunion____missing_field_name_33 {
 341   u32 padding1[12] ;
 342   u32 sw_reserved[12] ;
 343};
 344#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 345struct i387_fxsave_struct {
 346   u16 cwd ;
 347   u16 swd ;
 348   u16 twd ;
 349   u16 fop ;
 350   union __anonunion____missing_field_name_30 __annonCompField14 ;
 351   u32 mxcsr ;
 352   u32 mxcsr_mask ;
 353   u32 st_space[32] ;
 354   u32 xmm_space[64] ;
 355   u32 padding[12] ;
 356   union __anonunion____missing_field_name_33 __annonCompField15 ;
 357} __attribute__((__aligned__(16))) ;
 358#line 341 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 359struct i387_soft_struct {
 360   u32 cwd ;
 361   u32 swd ;
 362   u32 twd ;
 363   u32 fip ;
 364   u32 fcs ;
 365   u32 foo ;
 366   u32 fos ;
 367   u32 st_space[20] ;
 368   u8 ftop ;
 369   u8 changed ;
 370   u8 lookahead ;
 371   u8 no_update ;
 372   u8 rm ;
 373   u8 alimit ;
 374   struct math_emu_info *info ;
 375   u32 entry_eip ;
 376};
 377#line 361 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 378struct ymmh_struct {
 379   u32 ymmh_space[64] ;
 380};
 381#line 366 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 382struct xsave_hdr_struct {
 383   u64 xstate_bv ;
 384   u64 reserved1[2] ;
 385   u64 reserved2[5] ;
 386} __attribute__((__packed__)) ;
 387#line 372 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 388struct xsave_struct {
 389   struct i387_fxsave_struct i387 ;
 390   struct xsave_hdr_struct xsave_hdr ;
 391   struct ymmh_struct ymmh ;
 392} __attribute__((__packed__, __aligned__(64))) ;
 393#line 379 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 394union thread_xstate {
 395   struct i387_fsave_struct fsave ;
 396   struct i387_fxsave_struct fxsave ;
 397   struct i387_soft_struct soft ;
 398   struct xsave_struct xsave ;
 399};
 400#line 386 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 401struct fpu {
 402   unsigned int last_cpu ;
 403   unsigned int has_fpu ;
 404   union thread_xstate *state ;
 405};
 406#line 433
 407struct kmem_cache;
 408#line 435
 409struct perf_event;
 410#line 435
 411struct perf_event;
 412#line 437 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 413struct thread_struct {
 414   struct desc_struct tls_array[3] ;
 415   unsigned long sp0 ;
 416   unsigned long sp ;
 417   unsigned long usersp ;
 418   unsigned short es ;
 419   unsigned short ds ;
 420   unsigned short fsindex ;
 421   unsigned short gsindex ;
 422   unsigned long fs ;
 423   unsigned long gs ;
 424   struct perf_event *ptrace_bps[4] ;
 425   unsigned long debugreg6 ;
 426   unsigned long ptrace_dr7 ;
 427   unsigned long cr2 ;
 428   unsigned long trap_nr ;
 429   unsigned long error_code ;
 430   struct fpu fpu ;
 431   unsigned long *io_bitmap_ptr ;
 432   unsigned long iopl ;
 433   unsigned int io_bitmap_max ;
 434};
 435#line 23 "include/asm-generic/atomic-long.h"
 436typedef atomic64_t atomic_long_t;
 437#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 438typedef u16 __ticket_t;
 439#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 440typedef u32 __ticketpair_t;
 441#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 442struct __raw_tickets {
 443   __ticket_t head ;
 444   __ticket_t tail ;
 445};
 446#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 447union __anonunion____missing_field_name_36 {
 448   __ticketpair_t head_tail ;
 449   struct __raw_tickets tickets ;
 450};
 451#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 452struct arch_spinlock {
 453   union __anonunion____missing_field_name_36 __annonCompField17 ;
 454};
 455#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 456typedef struct arch_spinlock arch_spinlock_t;
 457#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 458struct __anonstruct____missing_field_name_38 {
 459   u32 read ;
 460   s32 write ;
 461};
 462#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 463union __anonunion_arch_rwlock_t_37 {
 464   s64 lock ;
 465   struct __anonstruct____missing_field_name_38 __annonCompField18 ;
 466};
 467#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 468typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_t;
 469#line 12 "include/linux/lockdep.h"
 470struct task_struct;
 471#line 391 "include/linux/lockdep.h"
 472struct lock_class_key {
 473
 474};
 475#line 20 "include/linux/spinlock_types.h"
 476struct raw_spinlock {
 477   arch_spinlock_t raw_lock ;
 478   unsigned int magic ;
 479   unsigned int owner_cpu ;
 480   void *owner ;
 481};
 482#line 20 "include/linux/spinlock_types.h"
 483typedef struct raw_spinlock raw_spinlock_t;
 484#line 64 "include/linux/spinlock_types.h"
 485union __anonunion____missing_field_name_39 {
 486   struct raw_spinlock rlock ;
 487};
 488#line 64 "include/linux/spinlock_types.h"
 489struct spinlock {
 490   union __anonunion____missing_field_name_39 __annonCompField19 ;
 491};
 492#line 64 "include/linux/spinlock_types.h"
 493typedef struct spinlock spinlock_t;
 494#line 11 "include/linux/rwlock_types.h"
 495struct __anonstruct_rwlock_t_40 {
 496   arch_rwlock_t raw_lock ;
 497   unsigned int magic ;
 498   unsigned int owner_cpu ;
 499   void *owner ;
 500};
 501#line 11 "include/linux/rwlock_types.h"
 502typedef struct __anonstruct_rwlock_t_40 rwlock_t;
 503#line 119 "include/linux/seqlock.h"
 504struct seqcount {
 505   unsigned int sequence ;
 506};
 507#line 119 "include/linux/seqlock.h"
 508typedef struct seqcount seqcount_t;
 509#line 14 "include/linux/time.h"
 510struct timespec {
 511   __kernel_time_t tv_sec ;
 512   long tv_nsec ;
 513};
 514#line 62 "include/linux/stat.h"
 515struct kstat {
 516   u64 ino ;
 517   dev_t dev ;
 518   umode_t mode ;
 519   unsigned int nlink ;
 520   uid_t uid ;
 521   gid_t gid ;
 522   dev_t rdev ;
 523   loff_t size ;
 524   struct timespec atime ;
 525   struct timespec mtime ;
 526   struct timespec ctime ;
 527   unsigned long blksize ;
 528   unsigned long long blocks ;
 529};
 530#line 49 "include/linux/wait.h"
 531struct __wait_queue_head {
 532   spinlock_t lock ;
 533   struct list_head task_list ;
 534};
 535#line 53 "include/linux/wait.h"
 536typedef struct __wait_queue_head wait_queue_head_t;
 537#line 55
 538struct task_struct;
 539#line 98 "include/linux/nodemask.h"
 540struct __anonstruct_nodemask_t_42 {
 541   unsigned long bits[(((unsigned long )(1 << 10) + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 542};
 543#line 98 "include/linux/nodemask.h"
 544typedef struct __anonstruct_nodemask_t_42 nodemask_t;
 545#line 60 "include/linux/pageblock-flags.h"
 546struct page;
 547#line 48 "include/linux/mutex.h"
 548struct mutex {
 549   atomic_t count ;
 550   spinlock_t wait_lock ;
 551   struct list_head wait_list ;
 552   struct task_struct *owner ;
 553   char const   *name ;
 554   void *magic ;
 555};
 556#line 69 "include/linux/mutex.h"
 557struct mutex_waiter {
 558   struct list_head list ;
 559   struct task_struct *task ;
 560   void *magic ;
 561};
 562#line 19 "include/linux/rwsem.h"
 563struct rw_semaphore;
 564#line 19
 565struct rw_semaphore;
 566#line 25 "include/linux/rwsem.h"
 567struct rw_semaphore {
 568   long count ;
 569   raw_spinlock_t wait_lock ;
 570   struct list_head wait_list ;
 571};
 572#line 25 "include/linux/completion.h"
 573struct completion {
 574   unsigned int done ;
 575   wait_queue_head_t wait ;
 576};
 577#line 9 "include/linux/memory_hotplug.h"
 578struct page;
 579#line 46 "include/linux/ktime.h"
 580union ktime {
 581   s64 tv64 ;
 582};
 583#line 59 "include/linux/ktime.h"
 584typedef union ktime ktime_t;
 585#line 10 "include/linux/timer.h"
 586struct tvec_base;
 587#line 10
 588struct tvec_base;
 589#line 12 "include/linux/timer.h"
 590struct timer_list {
 591   struct list_head entry ;
 592   unsigned long expires ;
 593   struct tvec_base *base ;
 594   void (*function)(unsigned long  ) ;
 595   unsigned long data ;
 596   int slack ;
 597   int start_pid ;
 598   void *start_site ;
 599   char start_comm[16] ;
 600};
 601#line 289
 602struct hrtimer;
 603#line 289
 604struct hrtimer;
 605#line 290
 606enum hrtimer_restart;
 607#line 17 "include/linux/workqueue.h"
 608struct work_struct;
 609#line 17
 610struct work_struct;
 611#line 79 "include/linux/workqueue.h"
 612struct work_struct {
 613   atomic_long_t data ;
 614   struct list_head entry ;
 615   void (*func)(struct work_struct *work ) ;
 616};
 617#line 92 "include/linux/workqueue.h"
 618struct delayed_work {
 619   struct work_struct work ;
 620   struct timer_list timer ;
 621};
 622#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 623struct __anonstruct_mm_context_t_112 {
 624   void *ldt ;
 625   int size ;
 626   unsigned short ia32_compat ;
 627   struct mutex lock ;
 628   void *vdso ;
 629};
 630#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 631typedef struct __anonstruct_mm_context_t_112 mm_context_t;
 632#line 8 "include/linux/vmalloc.h"
 633struct vm_area_struct;
 634#line 8
 635struct vm_area_struct;
 636#line 994 "include/linux/mmzone.h"
 637struct page;
 638#line 10 "include/linux/gfp.h"
 639struct vm_area_struct;
 640#line 29 "include/linux/sysctl.h"
 641struct completion;
 642#line 100 "include/linux/rbtree.h"
 643struct rb_node {
 644   unsigned long rb_parent_color ;
 645   struct rb_node *rb_right ;
 646   struct rb_node *rb_left ;
 647} __attribute__((__aligned__(sizeof(long )))) ;
 648#line 110 "include/linux/rbtree.h"
 649struct rb_root {
 650   struct rb_node *rb_node ;
 651};
 652#line 939 "include/linux/sysctl.h"
 653struct nsproxy;
 654#line 939
 655struct nsproxy;
 656#line 48 "include/linux/kmod.h"
 657struct cred;
 658#line 48
 659struct cred;
 660#line 49
 661struct file;
 662#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 663struct task_struct;
 664#line 18 "include/linux/elf.h"
 665typedef __u64 Elf64_Addr;
 666#line 19 "include/linux/elf.h"
 667typedef __u16 Elf64_Half;
 668#line 23 "include/linux/elf.h"
 669typedef __u32 Elf64_Word;
 670#line 24 "include/linux/elf.h"
 671typedef __u64 Elf64_Xword;
 672#line 194 "include/linux/elf.h"
 673struct elf64_sym {
 674   Elf64_Word st_name ;
 675   unsigned char st_info ;
 676   unsigned char st_other ;
 677   Elf64_Half st_shndx ;
 678   Elf64_Addr st_value ;
 679   Elf64_Xword st_size ;
 680};
 681#line 194 "include/linux/elf.h"
 682typedef struct elf64_sym Elf64_Sym;
 683#line 438
 684struct file;
 685#line 20 "include/linux/kobject_ns.h"
 686struct sock;
 687#line 20
 688struct sock;
 689#line 21
 690struct kobject;
 691#line 21
 692struct kobject;
 693#line 27
 694enum kobj_ns_type {
 695    KOBJ_NS_TYPE_NONE = 0,
 696    KOBJ_NS_TYPE_NET = 1,
 697    KOBJ_NS_TYPES = 2
 698} ;
 699#line 40 "include/linux/kobject_ns.h"
 700struct kobj_ns_type_operations {
 701   enum kobj_ns_type type ;
 702   void *(*grab_current_ns)(void) ;
 703   void const   *(*netlink_ns)(struct sock *sk ) ;
 704   void const   *(*initial_ns)(void) ;
 705   void (*drop_ns)(void * ) ;
 706};
 707#line 22 "include/linux/sysfs.h"
 708struct kobject;
 709#line 23
 710struct module;
 711#line 24
 712enum kobj_ns_type;
 713#line 26 "include/linux/sysfs.h"
 714struct attribute {
 715   char const   *name ;
 716   umode_t mode ;
 717};
 718#line 85
 719struct file;
 720#line 86
 721struct vm_area_struct;
 722#line 112 "include/linux/sysfs.h"
 723struct sysfs_ops {
 724   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 725   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 726   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 727};
 728#line 118
 729struct sysfs_dirent;
 730#line 118
 731struct sysfs_dirent;
 732#line 22 "include/linux/kref.h"
 733struct kref {
 734   atomic_t refcount ;
 735};
 736#line 60 "include/linux/kobject.h"
 737struct kset;
 738#line 60
 739struct kobj_type;
 740#line 60 "include/linux/kobject.h"
 741struct kobject {
 742   char const   *name ;
 743   struct list_head entry ;
 744   struct kobject *parent ;
 745   struct kset *kset ;
 746   struct kobj_type *ktype ;
 747   struct sysfs_dirent *sd ;
 748   struct kref kref ;
 749   unsigned int state_initialized : 1 ;
 750   unsigned int state_in_sysfs : 1 ;
 751   unsigned int state_add_uevent_sent : 1 ;
 752   unsigned int state_remove_uevent_sent : 1 ;
 753   unsigned int uevent_suppress : 1 ;
 754};
 755#line 108 "include/linux/kobject.h"
 756struct kobj_type {
 757   void (*release)(struct kobject *kobj ) ;
 758   struct sysfs_ops  const  *sysfs_ops ;
 759   struct attribute **default_attrs ;
 760   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 761   void const   *(*namespace)(struct kobject *kobj ) ;
 762};
 763#line 116 "include/linux/kobject.h"
 764struct kobj_uevent_env {
 765   char *envp[32] ;
 766   int envp_idx ;
 767   char buf[2048] ;
 768   int buflen ;
 769};
 770#line 123 "include/linux/kobject.h"
 771struct kset_uevent_ops {
 772   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 773   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 774   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 775};
 776#line 140
 777struct sock;
 778#line 159 "include/linux/kobject.h"
 779struct kset {
 780   struct list_head list ;
 781   spinlock_t list_lock ;
 782   struct kobject kobj ;
 783   struct kset_uevent_ops  const  *uevent_ops ;
 784};
 785#line 39 "include/linux/moduleparam.h"
 786struct kernel_param;
 787#line 39
 788struct kernel_param;
 789#line 41 "include/linux/moduleparam.h"
 790struct kernel_param_ops {
 791   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
 792   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
 793   void (*free)(void *arg ) ;
 794};
 795#line 50
 796struct kparam_string;
 797#line 50
 798struct kparam_array;
 799#line 50 "include/linux/moduleparam.h"
 800union __anonunion____missing_field_name_199 {
 801   void *arg ;
 802   struct kparam_string  const  *str ;
 803   struct kparam_array  const  *arr ;
 804};
 805#line 50 "include/linux/moduleparam.h"
 806struct kernel_param {
 807   char const   *name ;
 808   struct kernel_param_ops  const  *ops ;
 809   u16 perm ;
 810   s16 level ;
 811   union __anonunion____missing_field_name_199 __annonCompField32 ;
 812};
 813#line 63 "include/linux/moduleparam.h"
 814struct kparam_string {
 815   unsigned int maxlen ;
 816   char *string ;
 817};
 818#line 69 "include/linux/moduleparam.h"
 819struct kparam_array {
 820   unsigned int max ;
 821   unsigned int elemsize ;
 822   unsigned int *num ;
 823   struct kernel_param_ops  const  *ops ;
 824   void *elem ;
 825};
 826#line 445
 827struct module;
 828#line 80 "include/linux/jump_label.h"
 829struct module;
 830#line 143 "include/linux/jump_label.h"
 831struct static_key {
 832   atomic_t enabled ;
 833};
 834#line 22 "include/linux/tracepoint.h"
 835struct module;
 836#line 23
 837struct tracepoint;
 838#line 23
 839struct tracepoint;
 840#line 25 "include/linux/tracepoint.h"
 841struct tracepoint_func {
 842   void *func ;
 843   void *data ;
 844};
 845#line 30 "include/linux/tracepoint.h"
 846struct tracepoint {
 847   char const   *name ;
 848   struct static_key key ;
 849   void (*regfunc)(void) ;
 850   void (*unregfunc)(void) ;
 851   struct tracepoint_func *funcs ;
 852};
 853#line 19 "include/linux/export.h"
 854struct kernel_symbol {
 855   unsigned long value ;
 856   char const   *name ;
 857};
 858#line 8 "include/asm-generic/module.h"
 859struct mod_arch_specific {
 860
 861};
 862#line 35 "include/linux/module.h"
 863struct module;
 864#line 37
 865struct module_param_attrs;
 866#line 37 "include/linux/module.h"
 867struct module_kobject {
 868   struct kobject kobj ;
 869   struct module *mod ;
 870   struct kobject *drivers_dir ;
 871   struct module_param_attrs *mp ;
 872};
 873#line 44 "include/linux/module.h"
 874struct module_attribute {
 875   struct attribute attr ;
 876   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 877   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 878                    size_t count ) ;
 879   void (*setup)(struct module * , char const   * ) ;
 880   int (*test)(struct module * ) ;
 881   void (*free)(struct module * ) ;
 882};
 883#line 71
 884struct exception_table_entry;
 885#line 71
 886struct exception_table_entry;
 887#line 199
 888enum module_state {
 889    MODULE_STATE_LIVE = 0,
 890    MODULE_STATE_COMING = 1,
 891    MODULE_STATE_GOING = 2
 892} ;
 893#line 215 "include/linux/module.h"
 894struct module_ref {
 895   unsigned long incs ;
 896   unsigned long decs ;
 897} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 898#line 220
 899struct module_sect_attrs;
 900#line 220
 901struct module_notes_attrs;
 902#line 220
 903struct ftrace_event_call;
 904#line 220 "include/linux/module.h"
 905struct module {
 906   enum module_state state ;
 907   struct list_head list ;
 908   char name[64UL - sizeof(unsigned long )] ;
 909   struct module_kobject mkobj ;
 910   struct module_attribute *modinfo_attrs ;
 911   char const   *version ;
 912   char const   *srcversion ;
 913   struct kobject *holders_dir ;
 914   struct kernel_symbol  const  *syms ;
 915   unsigned long const   *crcs ;
 916   unsigned int num_syms ;
 917   struct kernel_param *kp ;
 918   unsigned int num_kp ;
 919   unsigned int num_gpl_syms ;
 920   struct kernel_symbol  const  *gpl_syms ;
 921   unsigned long const   *gpl_crcs ;
 922   struct kernel_symbol  const  *unused_syms ;
 923   unsigned long const   *unused_crcs ;
 924   unsigned int num_unused_syms ;
 925   unsigned int num_unused_gpl_syms ;
 926   struct kernel_symbol  const  *unused_gpl_syms ;
 927   unsigned long const   *unused_gpl_crcs ;
 928   struct kernel_symbol  const  *gpl_future_syms ;
 929   unsigned long const   *gpl_future_crcs ;
 930   unsigned int num_gpl_future_syms ;
 931   unsigned int num_exentries ;
 932   struct exception_table_entry *extable ;
 933   int (*init)(void) ;
 934   void *module_init ;
 935   void *module_core ;
 936   unsigned int init_size ;
 937   unsigned int core_size ;
 938   unsigned int init_text_size ;
 939   unsigned int core_text_size ;
 940   unsigned int init_ro_size ;
 941   unsigned int core_ro_size ;
 942   struct mod_arch_specific arch ;
 943   unsigned int taints ;
 944   unsigned int num_bugs ;
 945   struct list_head bug_list ;
 946   struct bug_entry *bug_table ;
 947   Elf64_Sym *symtab ;
 948   Elf64_Sym *core_symtab ;
 949   unsigned int num_symtab ;
 950   unsigned int core_num_syms ;
 951   char *strtab ;
 952   char *core_strtab ;
 953   struct module_sect_attrs *sect_attrs ;
 954   struct module_notes_attrs *notes_attrs ;
 955   char *args ;
 956   void *percpu ;
 957   unsigned int percpu_size ;
 958   unsigned int num_tracepoints ;
 959   struct tracepoint * const  *tracepoints_ptrs ;
 960   unsigned int num_trace_bprintk_fmt ;
 961   char const   **trace_bprintk_fmt_start ;
 962   struct ftrace_event_call **trace_events ;
 963   unsigned int num_trace_events ;
 964   struct list_head source_list ;
 965   struct list_head target_list ;
 966   struct task_struct *waiter ;
 967   void (*exit)(void) ;
 968   struct module_ref *refptr ;
 969   ctor_fn_t *ctors ;
 970   unsigned int num_ctors ;
 971};
 972#line 32 "include/linux/device.h"
 973struct module;
 974#line 18 "include/linux/capability.h"
 975struct task_struct;
 976#line 94 "include/linux/capability.h"
 977struct kernel_cap_struct {
 978   __u32 cap[2] ;
 979};
 980#line 94 "include/linux/capability.h"
 981typedef struct kernel_cap_struct kernel_cap_t;
 982#line 377
 983struct dentry;
 984#line 377
 985struct dentry;
 986#line 378
 987struct user_namespace;
 988#line 378
 989struct user_namespace;
 990#line 14 "include/linux/prio_tree.h"
 991struct prio_tree_node;
 992#line 14 "include/linux/prio_tree.h"
 993struct raw_prio_tree_node {
 994   struct prio_tree_node *left ;
 995   struct prio_tree_node *right ;
 996   struct prio_tree_node *parent ;
 997};
 998#line 20 "include/linux/prio_tree.h"
 999struct prio_tree_node {
1000   struct prio_tree_node *left ;
1001   struct prio_tree_node *right ;
1002   struct prio_tree_node *parent ;
1003   unsigned long start ;
1004   unsigned long last ;
1005};
1006#line 28 "include/linux/prio_tree.h"
1007struct prio_tree_root {
1008   struct prio_tree_node *prio_tree_node ;
1009   unsigned short index_bits ;
1010   unsigned short raw ;
1011};
1012#line 23 "include/linux/mm_types.h"
1013struct address_space;
1014#line 23
1015struct address_space;
1016#line 40 "include/linux/mm_types.h"
1017union __anonunion____missing_field_name_203 {
1018   unsigned long index ;
1019   void *freelist ;
1020};
1021#line 40 "include/linux/mm_types.h"
1022struct __anonstruct____missing_field_name_207 {
1023   unsigned int inuse : 16 ;
1024   unsigned int objects : 15 ;
1025   unsigned int frozen : 1 ;
1026};
1027#line 40 "include/linux/mm_types.h"
1028union __anonunion____missing_field_name_206 {
1029   atomic_t _mapcount ;
1030   struct __anonstruct____missing_field_name_207 __annonCompField34 ;
1031};
1032#line 40 "include/linux/mm_types.h"
1033struct __anonstruct____missing_field_name_205 {
1034   union __anonunion____missing_field_name_206 __annonCompField35 ;
1035   atomic_t _count ;
1036};
1037#line 40 "include/linux/mm_types.h"
1038union __anonunion____missing_field_name_204 {
1039   unsigned long counters ;
1040   struct __anonstruct____missing_field_name_205 __annonCompField36 ;
1041};
1042#line 40 "include/linux/mm_types.h"
1043struct __anonstruct____missing_field_name_202 {
1044   union __anonunion____missing_field_name_203 __annonCompField33 ;
1045   union __anonunion____missing_field_name_204 __annonCompField37 ;
1046};
1047#line 40 "include/linux/mm_types.h"
1048struct __anonstruct____missing_field_name_209 {
1049   struct page *next ;
1050   int pages ;
1051   int pobjects ;
1052};
1053#line 40 "include/linux/mm_types.h"
1054union __anonunion____missing_field_name_208 {
1055   struct list_head lru ;
1056   struct __anonstruct____missing_field_name_209 __annonCompField39 ;
1057};
1058#line 40 "include/linux/mm_types.h"
1059union __anonunion____missing_field_name_210 {
1060   unsigned long private ;
1061   struct kmem_cache *slab ;
1062   struct page *first_page ;
1063};
1064#line 40 "include/linux/mm_types.h"
1065struct page {
1066   unsigned long flags ;
1067   struct address_space *mapping ;
1068   struct __anonstruct____missing_field_name_202 __annonCompField38 ;
1069   union __anonunion____missing_field_name_208 __annonCompField40 ;
1070   union __anonunion____missing_field_name_210 __annonCompField41 ;
1071   unsigned long debug_flags ;
1072} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
1073#line 200 "include/linux/mm_types.h"
1074struct __anonstruct_vm_set_212 {
1075   struct list_head list ;
1076   void *parent ;
1077   struct vm_area_struct *head ;
1078};
1079#line 200 "include/linux/mm_types.h"
1080union __anonunion_shared_211 {
1081   struct __anonstruct_vm_set_212 vm_set ;
1082   struct raw_prio_tree_node prio_tree_node ;
1083};
1084#line 200
1085struct anon_vma;
1086#line 200
1087struct vm_operations_struct;
1088#line 200
1089struct mempolicy;
1090#line 200 "include/linux/mm_types.h"
1091struct vm_area_struct {
1092   struct mm_struct *vm_mm ;
1093   unsigned long vm_start ;
1094   unsigned long vm_end ;
1095   struct vm_area_struct *vm_next ;
1096   struct vm_area_struct *vm_prev ;
1097   pgprot_t vm_page_prot ;
1098   unsigned long vm_flags ;
1099   struct rb_node vm_rb ;
1100   union __anonunion_shared_211 shared ;
1101   struct list_head anon_vma_chain ;
1102   struct anon_vma *anon_vma ;
1103   struct vm_operations_struct  const  *vm_ops ;
1104   unsigned long vm_pgoff ;
1105   struct file *vm_file ;
1106   void *vm_private_data ;
1107   struct mempolicy *vm_policy ;
1108};
1109#line 257 "include/linux/mm_types.h"
1110struct core_thread {
1111   struct task_struct *task ;
1112   struct core_thread *next ;
1113};
1114#line 262 "include/linux/mm_types.h"
1115struct core_state {
1116   atomic_t nr_threads ;
1117   struct core_thread dumper ;
1118   struct completion startup ;
1119};
1120#line 284 "include/linux/mm_types.h"
1121struct mm_rss_stat {
1122   atomic_long_t count[3] ;
1123};
1124#line 288
1125struct linux_binfmt;
1126#line 288
1127struct mmu_notifier_mm;
1128#line 288 "include/linux/mm_types.h"
1129struct mm_struct {
1130   struct vm_area_struct *mmap ;
1131   struct rb_root mm_rb ;
1132   struct vm_area_struct *mmap_cache ;
1133   unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
1134                                      unsigned long pgoff , unsigned long flags ) ;
1135   void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
1136   unsigned long mmap_base ;
1137   unsigned long task_size ;
1138   unsigned long cached_hole_size ;
1139   unsigned long free_area_cache ;
1140   pgd_t *pgd ;
1141   atomic_t mm_users ;
1142   atomic_t mm_count ;
1143   int map_count ;
1144   spinlock_t page_table_lock ;
1145   struct rw_semaphore mmap_sem ;
1146   struct list_head mmlist ;
1147   unsigned long hiwater_rss ;
1148   unsigned long hiwater_vm ;
1149   unsigned long total_vm ;
1150   unsigned long locked_vm ;
1151   unsigned long pinned_vm ;
1152   unsigned long shared_vm ;
1153   unsigned long exec_vm ;
1154   unsigned long stack_vm ;
1155   unsigned long reserved_vm ;
1156   unsigned long def_flags ;
1157   unsigned long nr_ptes ;
1158   unsigned long start_code ;
1159   unsigned long end_code ;
1160   unsigned long start_data ;
1161   unsigned long end_data ;
1162   unsigned long start_brk ;
1163   unsigned long brk ;
1164   unsigned long start_stack ;
1165   unsigned long arg_start ;
1166   unsigned long arg_end ;
1167   unsigned long env_start ;
1168   unsigned long env_end ;
1169   unsigned long saved_auxv[44] ;
1170   struct mm_rss_stat rss_stat ;
1171   struct linux_binfmt *binfmt ;
1172   cpumask_var_t cpu_vm_mask_var ;
1173   mm_context_t context ;
1174   unsigned int faultstamp ;
1175   unsigned int token_priority ;
1176   unsigned int last_interval ;
1177   unsigned long flags ;
1178   struct core_state *core_state ;
1179   spinlock_t ioctx_lock ;
1180   struct hlist_head ioctx_list ;
1181   struct task_struct *owner ;
1182   struct file *exe_file ;
1183   unsigned long num_exe_file_vmas ;
1184   struct mmu_notifier_mm *mmu_notifier_mm ;
1185   pgtable_t pmd_huge_pte ;
1186   struct cpumask cpumask_allocation ;
1187};
1188#line 7 "include/asm-generic/cputime.h"
1189typedef unsigned long cputime_t;
1190#line 84 "include/linux/sem.h"
1191struct task_struct;
1192#line 101
1193struct sem_undo_list;
1194#line 101 "include/linux/sem.h"
1195struct sysv_sem {
1196   struct sem_undo_list *undo_list ;
1197};
1198#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1199struct siginfo;
1200#line 10
1201struct siginfo;
1202#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1203struct __anonstruct_sigset_t_214 {
1204   unsigned long sig[1] ;
1205};
1206#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1207typedef struct __anonstruct_sigset_t_214 sigset_t;
1208#line 17 "include/asm-generic/signal-defs.h"
1209typedef void __signalfn_t(int  );
1210#line 18 "include/asm-generic/signal-defs.h"
1211typedef __signalfn_t *__sighandler_t;
1212#line 20 "include/asm-generic/signal-defs.h"
1213typedef void __restorefn_t(void);
1214#line 21 "include/asm-generic/signal-defs.h"
1215typedef __restorefn_t *__sigrestore_t;
1216#line 167 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1217struct sigaction {
1218   __sighandler_t sa_handler ;
1219   unsigned long sa_flags ;
1220   __sigrestore_t sa_restorer ;
1221   sigset_t sa_mask ;
1222};
1223#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1224struct k_sigaction {
1225   struct sigaction sa ;
1226};
1227#line 7 "include/asm-generic/siginfo.h"
1228union sigval {
1229   int sival_int ;
1230   void *sival_ptr ;
1231};
1232#line 7 "include/asm-generic/siginfo.h"
1233typedef union sigval sigval_t;
1234#line 48 "include/asm-generic/siginfo.h"
1235struct __anonstruct__kill_216 {
1236   __kernel_pid_t _pid ;
1237   __kernel_uid32_t _uid ;
1238};
1239#line 48 "include/asm-generic/siginfo.h"
1240struct __anonstruct__timer_217 {
1241   __kernel_timer_t _tid ;
1242   int _overrun ;
1243   char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ;
1244   sigval_t _sigval ;
1245   int _sys_private ;
1246};
1247#line 48 "include/asm-generic/siginfo.h"
1248struct __anonstruct__rt_218 {
1249   __kernel_pid_t _pid ;
1250   __kernel_uid32_t _uid ;
1251   sigval_t _sigval ;
1252};
1253#line 48 "include/asm-generic/siginfo.h"
1254struct __anonstruct__sigchld_219 {
1255   __kernel_pid_t _pid ;
1256   __kernel_uid32_t _uid ;
1257   int _status ;
1258   __kernel_clock_t _utime ;
1259   __kernel_clock_t _stime ;
1260};
1261#line 48 "include/asm-generic/siginfo.h"
1262struct __anonstruct__sigfault_220 {
1263   void *_addr ;
1264   short _addr_lsb ;
1265};
1266#line 48 "include/asm-generic/siginfo.h"
1267struct __anonstruct__sigpoll_221 {
1268   long _band ;
1269   int _fd ;
1270};
1271#line 48 "include/asm-generic/siginfo.h"
1272union __anonunion__sifields_215 {
1273   int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ;
1274   struct __anonstruct__kill_216 _kill ;
1275   struct __anonstruct__timer_217 _timer ;
1276   struct __anonstruct__rt_218 _rt ;
1277   struct __anonstruct__sigchld_219 _sigchld ;
1278   struct __anonstruct__sigfault_220 _sigfault ;
1279   struct __anonstruct__sigpoll_221 _sigpoll ;
1280};
1281#line 48 "include/asm-generic/siginfo.h"
1282struct siginfo {
1283   int si_signo ;
1284   int si_errno ;
1285   int si_code ;
1286   union __anonunion__sifields_215 _sifields ;
1287};
1288#line 48 "include/asm-generic/siginfo.h"
1289typedef struct siginfo siginfo_t;
1290#line 288
1291struct siginfo;
1292#line 10 "include/linux/signal.h"
1293struct task_struct;
1294#line 18
1295struct user_struct;
1296#line 28 "include/linux/signal.h"
1297struct sigpending {
1298   struct list_head list ;
1299   sigset_t signal ;
1300};
1301#line 239
1302struct timespec;
1303#line 240
1304struct pt_regs;
1305#line 6 "include/linux/pid.h"
1306enum pid_type {
1307    PIDTYPE_PID = 0,
1308    PIDTYPE_PGID = 1,
1309    PIDTYPE_SID = 2,
1310    PIDTYPE_MAX = 3
1311} ;
1312#line 50
1313struct pid_namespace;
1314#line 50 "include/linux/pid.h"
1315struct upid {
1316   int nr ;
1317   struct pid_namespace *ns ;
1318   struct hlist_node pid_chain ;
1319};
1320#line 57 "include/linux/pid.h"
1321struct pid {
1322   atomic_t count ;
1323   unsigned int level ;
1324   struct hlist_head tasks[3] ;
1325   struct rcu_head rcu ;
1326   struct upid numbers[1] ;
1327};
1328#line 69 "include/linux/pid.h"
1329struct pid_link {
1330   struct hlist_node node ;
1331   struct pid *pid ;
1332};
1333#line 100
1334struct pid_namespace;
1335#line 10 "include/linux/seccomp.h"
1336struct __anonstruct_seccomp_t_224 {
1337   int mode ;
1338};
1339#line 10 "include/linux/seccomp.h"
1340typedef struct __anonstruct_seccomp_t_224 seccomp_t;
1341#line 81 "include/linux/plist.h"
1342struct plist_head {
1343   struct list_head node_list ;
1344};
1345#line 85 "include/linux/plist.h"
1346struct plist_node {
1347   int prio ;
1348   struct list_head prio_list ;
1349   struct list_head node_list ;
1350};
1351#line 40 "include/linux/rtmutex.h"
1352struct rt_mutex_waiter;
1353#line 40
1354struct rt_mutex_waiter;
1355#line 42 "include/linux/resource.h"
1356struct rlimit {
1357   unsigned long rlim_cur ;
1358   unsigned long rlim_max ;
1359};
1360#line 81
1361struct task_struct;
1362#line 8 "include/linux/timerqueue.h"
1363struct timerqueue_node {
1364   struct rb_node node ;
1365   ktime_t expires ;
1366};
1367#line 13 "include/linux/timerqueue.h"
1368struct timerqueue_head {
1369   struct rb_root head ;
1370   struct timerqueue_node *next ;
1371};
1372#line 27 "include/linux/hrtimer.h"
1373struct hrtimer_clock_base;
1374#line 27
1375struct hrtimer_clock_base;
1376#line 28
1377struct hrtimer_cpu_base;
1378#line 28
1379struct hrtimer_cpu_base;
1380#line 44
1381enum hrtimer_restart {
1382    HRTIMER_NORESTART = 0,
1383    HRTIMER_RESTART = 1
1384} ;
1385#line 108 "include/linux/hrtimer.h"
1386struct hrtimer {
1387   struct timerqueue_node node ;
1388   ktime_t _softexpires ;
1389   enum hrtimer_restart (*function)(struct hrtimer * ) ;
1390   struct hrtimer_clock_base *base ;
1391   unsigned long state ;
1392   int start_pid ;
1393   void *start_site ;
1394   char start_comm[16] ;
1395};
1396#line 145 "include/linux/hrtimer.h"
1397struct hrtimer_clock_base {
1398   struct hrtimer_cpu_base *cpu_base ;
1399   int index ;
1400   clockid_t clockid ;
1401   struct timerqueue_head active ;
1402   ktime_t resolution ;
1403   ktime_t (*get_time)(void) ;
1404   ktime_t softirq_time ;
1405   ktime_t offset ;
1406};
1407#line 178 "include/linux/hrtimer.h"
1408struct hrtimer_cpu_base {
1409   raw_spinlock_t lock ;
1410   unsigned long active_bases ;
1411   ktime_t expires_next ;
1412   int hres_active ;
1413   int hang_detected ;
1414   unsigned long nr_events ;
1415   unsigned long nr_retries ;
1416   unsigned long nr_hangs ;
1417   ktime_t max_hang_time ;
1418   struct hrtimer_clock_base clock_base[3] ;
1419};
1420#line 11 "include/linux/task_io_accounting.h"
1421struct task_io_accounting {
1422   u64 rchar ;
1423   u64 wchar ;
1424   u64 syscr ;
1425   u64 syscw ;
1426   u64 read_bytes ;
1427   u64 write_bytes ;
1428   u64 cancelled_write_bytes ;
1429};
1430#line 13 "include/linux/latencytop.h"
1431struct task_struct;
1432#line 20 "include/linux/latencytop.h"
1433struct latency_record {
1434   unsigned long backtrace[12] ;
1435   unsigned int count ;
1436   unsigned long time ;
1437   unsigned long max ;
1438};
1439#line 29 "include/linux/key.h"
1440typedef int32_t key_serial_t;
1441#line 32 "include/linux/key.h"
1442typedef uint32_t key_perm_t;
1443#line 34
1444struct key;
1445#line 34
1446struct key;
1447#line 74
1448struct seq_file;
1449#line 75
1450struct user_struct;
1451#line 76
1452struct signal_struct;
1453#line 76
1454struct signal_struct;
1455#line 77
1456struct cred;
1457#line 79
1458struct key_type;
1459#line 79
1460struct key_type;
1461#line 81
1462struct keyring_list;
1463#line 81
1464struct keyring_list;
1465#line 124
1466struct key_user;
1467#line 124 "include/linux/key.h"
1468union __anonunion____missing_field_name_225 {
1469   time_t expiry ;
1470   time_t revoked_at ;
1471};
1472#line 124 "include/linux/key.h"
1473union __anonunion_type_data_226 {
1474   struct list_head link ;
1475   unsigned long x[2] ;
1476   void *p[2] ;
1477   int reject_error ;
1478};
1479#line 124 "include/linux/key.h"
1480union __anonunion_payload_227 {
1481   unsigned long value ;
1482   void *rcudata ;
1483   void *data ;
1484   struct keyring_list *subscriptions ;
1485};
1486#line 124 "include/linux/key.h"
1487struct key {
1488   atomic_t usage ;
1489   key_serial_t serial ;
1490   struct rb_node serial_node ;
1491   struct key_type *type ;
1492   struct rw_semaphore sem ;
1493   struct key_user *user ;
1494   void *security ;
1495   union __anonunion____missing_field_name_225 __annonCompField42 ;
1496   uid_t uid ;
1497   gid_t gid ;
1498   key_perm_t perm ;
1499   unsigned short quotalen ;
1500   unsigned short datalen ;
1501   unsigned long flags ;
1502   char *description ;
1503   union __anonunion_type_data_226 type_data ;
1504   union __anonunion_payload_227 payload ;
1505};
1506#line 18 "include/linux/selinux.h"
1507struct audit_context;
1508#line 18
1509struct audit_context;
1510#line 21 "include/linux/cred.h"
1511struct user_struct;
1512#line 22
1513struct cred;
1514#line 23
1515struct inode;
1516#line 23
1517struct inode;
1518#line 31 "include/linux/cred.h"
1519struct group_info {
1520   atomic_t usage ;
1521   int ngroups ;
1522   int nblocks ;
1523   gid_t small_block[32] ;
1524   gid_t *blocks[0] ;
1525};
1526#line 83 "include/linux/cred.h"
1527struct thread_group_cred {
1528   atomic_t usage ;
1529   pid_t tgid ;
1530   spinlock_t lock ;
1531   struct key *session_keyring ;
1532   struct key *process_keyring ;
1533   struct rcu_head rcu ;
1534};
1535#line 116 "include/linux/cred.h"
1536struct cred {
1537   atomic_t usage ;
1538   atomic_t subscribers ;
1539   void *put_addr ;
1540   unsigned int magic ;
1541   uid_t uid ;
1542   gid_t gid ;
1543   uid_t suid ;
1544   gid_t sgid ;
1545   uid_t euid ;
1546   gid_t egid ;
1547   uid_t fsuid ;
1548   gid_t fsgid ;
1549   unsigned int securebits ;
1550   kernel_cap_t cap_inheritable ;
1551   kernel_cap_t cap_permitted ;
1552   kernel_cap_t cap_effective ;
1553   kernel_cap_t cap_bset ;
1554   unsigned char jit_keyring ;
1555   struct key *thread_keyring ;
1556   struct key *request_key_auth ;
1557   struct thread_group_cred *tgcred ;
1558   void *security ;
1559   struct user_struct *user ;
1560   struct user_namespace *user_ns ;
1561   struct group_info *group_info ;
1562   struct rcu_head rcu ;
1563};
1564#line 61 "include/linux/llist.h"
1565struct llist_node;
1566#line 65 "include/linux/llist.h"
1567struct llist_node {
1568   struct llist_node *next ;
1569};
1570#line 97 "include/linux/sched.h"
1571struct futex_pi_state;
1572#line 97
1573struct futex_pi_state;
1574#line 98
1575struct robust_list_head;
1576#line 98
1577struct robust_list_head;
1578#line 99
1579struct bio_list;
1580#line 99
1581struct bio_list;
1582#line 100
1583struct fs_struct;
1584#line 100
1585struct fs_struct;
1586#line 101
1587struct perf_event_context;
1588#line 101
1589struct perf_event_context;
1590#line 102
1591struct blk_plug;
1592#line 102
1593struct blk_plug;
1594#line 150
1595struct seq_file;
1596#line 151
1597struct cfs_rq;
1598#line 151
1599struct cfs_rq;
1600#line 259
1601struct task_struct;
1602#line 366
1603struct nsproxy;
1604#line 367
1605struct user_namespace;
1606#line 58 "include/linux/aio_abi.h"
1607struct io_event {
1608   __u64 data ;
1609   __u64 obj ;
1610   __s64 res ;
1611   __s64 res2 ;
1612};
1613#line 16 "include/linux/uio.h"
1614struct iovec {
1615   void *iov_base ;
1616   __kernel_size_t iov_len ;
1617};
1618#line 15 "include/linux/aio.h"
1619struct kioctx;
1620#line 15
1621struct kioctx;
1622#line 87 "include/linux/aio.h"
1623union __anonunion_ki_obj_229 {
1624   void *user ;
1625   struct task_struct *tsk ;
1626};
1627#line 87
1628struct eventfd_ctx;
1629#line 87 "include/linux/aio.h"
1630struct kiocb {
1631   struct list_head ki_run_list ;
1632   unsigned long ki_flags ;
1633   int ki_users ;
1634   unsigned int ki_key ;
1635   struct file *ki_filp ;
1636   struct kioctx *ki_ctx ;
1637   int (*ki_cancel)(struct kiocb * , struct io_event * ) ;
1638   ssize_t (*ki_retry)(struct kiocb * ) ;
1639   void (*ki_dtor)(struct kiocb * ) ;
1640   union __anonunion_ki_obj_229 ki_obj ;
1641   __u64 ki_user_data ;
1642   loff_t ki_pos ;
1643   void *private ;
1644   unsigned short ki_opcode ;
1645   size_t ki_nbytes ;
1646   char *ki_buf ;
1647   size_t ki_left ;
1648   struct iovec ki_inline_vec ;
1649   struct iovec *ki_iovec ;
1650   unsigned long ki_nr_segs ;
1651   unsigned long ki_cur_seg ;
1652   struct list_head ki_list ;
1653   struct list_head ki_batch ;
1654   struct eventfd_ctx *ki_eventfd ;
1655};
1656#line 166 "include/linux/aio.h"
1657struct aio_ring_info {
1658   unsigned long mmap_base ;
1659   unsigned long mmap_size ;
1660   struct page **ring_pages ;
1661   spinlock_t ring_lock ;
1662   long nr_pages ;
1663   unsigned int nr ;
1664   unsigned int tail ;
1665   struct page *internal_pages[8] ;
1666};
1667#line 179 "include/linux/aio.h"
1668struct kioctx {
1669   atomic_t users ;
1670   int dead ;
1671   struct mm_struct *mm ;
1672   unsigned long user_id ;
1673   struct hlist_node list ;
1674   wait_queue_head_t wait ;
1675   spinlock_t ctx_lock ;
1676   int reqs_active ;
1677   struct list_head active_reqs ;
1678   struct list_head run_list ;
1679   unsigned int max_reqs ;
1680   struct aio_ring_info ring_info ;
1681   struct delayed_work wq ;
1682   struct rcu_head rcu_head ;
1683};
1684#line 214
1685struct mm_struct;
1686#line 443 "include/linux/sched.h"
1687struct sighand_struct {
1688   atomic_t count ;
1689   struct k_sigaction action[64] ;
1690   spinlock_t siglock ;
1691   wait_queue_head_t signalfd_wqh ;
1692};
1693#line 450 "include/linux/sched.h"
1694struct pacct_struct {
1695   int ac_flag ;
1696   long ac_exitcode ;
1697   unsigned long ac_mem ;
1698   cputime_t ac_utime ;
1699   cputime_t ac_stime ;
1700   unsigned long ac_minflt ;
1701   unsigned long ac_majflt ;
1702};
1703#line 458 "include/linux/sched.h"
1704struct cpu_itimer {
1705   cputime_t expires ;
1706   cputime_t incr ;
1707   u32 error ;
1708   u32 incr_error ;
1709};
1710#line 476 "include/linux/sched.h"
1711struct task_cputime {
1712   cputime_t utime ;
1713   cputime_t stime ;
1714   unsigned long long sum_exec_runtime ;
1715};
1716#line 512 "include/linux/sched.h"
1717struct thread_group_cputimer {
1718   struct task_cputime cputime ;
1719   int running ;
1720   raw_spinlock_t lock ;
1721};
1722#line 519
1723struct autogroup;
1724#line 519
1725struct autogroup;
1726#line 528
1727struct tty_struct;
1728#line 528
1729struct taskstats;
1730#line 528
1731struct tty_audit_buf;
1732#line 528 "include/linux/sched.h"
1733struct signal_struct {
1734   atomic_t sigcnt ;
1735   atomic_t live ;
1736   int nr_threads ;
1737   wait_queue_head_t wait_chldexit ;
1738   struct task_struct *curr_target ;
1739   struct sigpending shared_pending ;
1740   int group_exit_code ;
1741   int notify_count ;
1742   struct task_struct *group_exit_task ;
1743   int group_stop_count ;
1744   unsigned int flags ;
1745   unsigned int is_child_subreaper : 1 ;
1746   unsigned int has_child_subreaper : 1 ;
1747   struct list_head posix_timers ;
1748   struct hrtimer real_timer ;
1749   struct pid *leader_pid ;
1750   ktime_t it_real_incr ;
1751   struct cpu_itimer it[2] ;
1752   struct thread_group_cputimer cputimer ;
1753   struct task_cputime cputime_expires ;
1754   struct list_head cpu_timers[3] ;
1755   struct pid *tty_old_pgrp ;
1756   int leader ;
1757   struct tty_struct *tty ;
1758   struct autogroup *autogroup ;
1759   cputime_t utime ;
1760   cputime_t stime ;
1761   cputime_t cutime ;
1762   cputime_t cstime ;
1763   cputime_t gtime ;
1764   cputime_t cgtime ;
1765   cputime_t prev_utime ;
1766   cputime_t prev_stime ;
1767   unsigned long nvcsw ;
1768   unsigned long nivcsw ;
1769   unsigned long cnvcsw ;
1770   unsigned long cnivcsw ;
1771   unsigned long min_flt ;
1772   unsigned long maj_flt ;
1773   unsigned long cmin_flt ;
1774   unsigned long cmaj_flt ;
1775   unsigned long inblock ;
1776   unsigned long oublock ;
1777   unsigned long cinblock ;
1778   unsigned long coublock ;
1779   unsigned long maxrss ;
1780   unsigned long cmaxrss ;
1781   struct task_io_accounting ioac ;
1782   unsigned long long sum_sched_runtime ;
1783   struct rlimit rlim[16] ;
1784   struct pacct_struct pacct ;
1785   struct taskstats *stats ;
1786   unsigned int audit_tty ;
1787   struct tty_audit_buf *tty_audit_buf ;
1788   struct rw_semaphore group_rwsem ;
1789   int oom_adj ;
1790   int oom_score_adj ;
1791   int oom_score_adj_min ;
1792   struct mutex cred_guard_mutex ;
1793};
1794#line 703 "include/linux/sched.h"
1795struct user_struct {
1796   atomic_t __count ;
1797   atomic_t processes ;
1798   atomic_t files ;
1799   atomic_t sigpending ;
1800   atomic_t inotify_watches ;
1801   atomic_t inotify_devs ;
1802   atomic_t fanotify_listeners ;
1803   atomic_long_t epoll_watches ;
1804   unsigned long mq_bytes ;
1805   unsigned long locked_shm ;
1806   struct key *uid_keyring ;
1807   struct key *session_keyring ;
1808   struct hlist_node uidhash_node ;
1809   uid_t uid ;
1810   struct user_namespace *user_ns ;
1811   atomic_long_t locked_vm ;
1812};
1813#line 747
1814struct backing_dev_info;
1815#line 747
1816struct backing_dev_info;
1817#line 748
1818struct reclaim_state;
1819#line 748
1820struct reclaim_state;
1821#line 751 "include/linux/sched.h"
1822struct sched_info {
1823   unsigned long pcount ;
1824   unsigned long long run_delay ;
1825   unsigned long long last_arrival ;
1826   unsigned long long last_queued ;
1827};
1828#line 763 "include/linux/sched.h"
1829struct task_delay_info {
1830   spinlock_t lock ;
1831   unsigned int flags ;
1832   struct timespec blkio_start ;
1833   struct timespec blkio_end ;
1834   u64 blkio_delay ;
1835   u64 swapin_delay ;
1836   u32 blkio_count ;
1837   u32 swapin_count ;
1838   struct timespec freepages_start ;
1839   struct timespec freepages_end ;
1840   u64 freepages_delay ;
1841   u32 freepages_count ;
1842};
1843#line 1088
1844struct io_context;
1845#line 1088
1846struct io_context;
1847#line 1097
1848struct audit_context;
1849#line 1098
1850struct mempolicy;
1851#line 1099
1852struct pipe_inode_info;
1853#line 1099
1854struct pipe_inode_info;
1855#line 1102
1856struct rq;
1857#line 1102
1858struct rq;
1859#line 1122 "include/linux/sched.h"
1860struct sched_class {
1861   struct sched_class  const  *next ;
1862   void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
1863   void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
1864   void (*yield_task)(struct rq *rq ) ;
1865   bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ;
1866   void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ;
1867   struct task_struct *(*pick_next_task)(struct rq *rq ) ;
1868   void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ;
1869   int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ;
1870   void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ;
1871   void (*post_schedule)(struct rq *this_rq ) ;
1872   void (*task_waking)(struct task_struct *task ) ;
1873   void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ;
1874   void (*set_cpus_allowed)(struct task_struct *p , struct cpumask  const  *newmask ) ;
1875   void (*rq_online)(struct rq *rq ) ;
1876   void (*rq_offline)(struct rq *rq ) ;
1877   void (*set_curr_task)(struct rq *rq ) ;
1878   void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ;
1879   void (*task_fork)(struct task_struct *p ) ;
1880   void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ;
1881   void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ;
1882   void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ;
1883   unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ;
1884   void (*task_move_group)(struct task_struct *p , int on_rq ) ;
1885};
1886#line 1167 "include/linux/sched.h"
1887struct load_weight {
1888   unsigned long weight ;
1889   unsigned long inv_weight ;
1890};
1891#line 1172 "include/linux/sched.h"
1892struct sched_statistics {
1893   u64 wait_start ;
1894   u64 wait_max ;
1895   u64 wait_count ;
1896   u64 wait_sum ;
1897   u64 iowait_count ;
1898   u64 iowait_sum ;
1899   u64 sleep_start ;
1900   u64 sleep_max ;
1901   s64 sum_sleep_runtime ;
1902   u64 block_start ;
1903   u64 block_max ;
1904   u64 exec_max ;
1905   u64 slice_max ;
1906   u64 nr_migrations_cold ;
1907   u64 nr_failed_migrations_affine ;
1908   u64 nr_failed_migrations_running ;
1909   u64 nr_failed_migrations_hot ;
1910   u64 nr_forced_migrations ;
1911   u64 nr_wakeups ;
1912   u64 nr_wakeups_sync ;
1913   u64 nr_wakeups_migrate ;
1914   u64 nr_wakeups_local ;
1915   u64 nr_wakeups_remote ;
1916   u64 nr_wakeups_affine ;
1917   u64 nr_wakeups_affine_attempts ;
1918   u64 nr_wakeups_passive ;
1919   u64 nr_wakeups_idle ;
1920};
1921#line 1207 "include/linux/sched.h"
1922struct sched_entity {
1923   struct load_weight load ;
1924   struct rb_node run_node ;
1925   struct list_head group_node ;
1926   unsigned int on_rq ;
1927   u64 exec_start ;
1928   u64 sum_exec_runtime ;
1929   u64 vruntime ;
1930   u64 prev_sum_exec_runtime ;
1931   u64 nr_migrations ;
1932   struct sched_statistics statistics ;
1933   struct sched_entity *parent ;
1934   struct cfs_rq *cfs_rq ;
1935   struct cfs_rq *my_q ;
1936};
1937#line 1233
1938struct rt_rq;
1939#line 1233 "include/linux/sched.h"
1940struct sched_rt_entity {
1941   struct list_head run_list ;
1942   unsigned long timeout ;
1943   unsigned int time_slice ;
1944   int nr_cpus_allowed ;
1945   struct sched_rt_entity *back ;
1946   struct sched_rt_entity *parent ;
1947   struct rt_rq *rt_rq ;
1948   struct rt_rq *my_q ;
1949};
1950#line 1264
1951struct files_struct;
1952#line 1264
1953struct css_set;
1954#line 1264
1955struct compat_robust_list_head;
1956#line 1264
1957struct mem_cgroup;
1958#line 1264 "include/linux/sched.h"
1959struct memcg_batch_info {
1960   int do_batch ;
1961   struct mem_cgroup *memcg ;
1962   unsigned long nr_pages ;
1963   unsigned long memsw_nr_pages ;
1964};
1965#line 1264 "include/linux/sched.h"
1966struct task_struct {
1967   long volatile   state ;
1968   void *stack ;
1969   atomic_t usage ;
1970   unsigned int flags ;
1971   unsigned int ptrace ;
1972   struct llist_node wake_entry ;
1973   int on_cpu ;
1974   int on_rq ;
1975   int prio ;
1976   int static_prio ;
1977   int normal_prio ;
1978   unsigned int rt_priority ;
1979   struct sched_class  const  *sched_class ;
1980   struct sched_entity se ;
1981   struct sched_rt_entity rt ;
1982   struct hlist_head preempt_notifiers ;
1983   unsigned char fpu_counter ;
1984   unsigned int policy ;
1985   cpumask_t cpus_allowed ;
1986   struct sched_info sched_info ;
1987   struct list_head tasks ;
1988   struct plist_node pushable_tasks ;
1989   struct mm_struct *mm ;
1990   struct mm_struct *active_mm ;
1991   unsigned int brk_randomized : 1 ;
1992   int exit_state ;
1993   int exit_code ;
1994   int exit_signal ;
1995   int pdeath_signal ;
1996   unsigned int jobctl ;
1997   unsigned int personality ;
1998   unsigned int did_exec : 1 ;
1999   unsigned int in_execve : 1 ;
2000   unsigned int in_iowait : 1 ;
2001   unsigned int sched_reset_on_fork : 1 ;
2002   unsigned int sched_contributes_to_load : 1 ;
2003   unsigned int irq_thread : 1 ;
2004   pid_t pid ;
2005   pid_t tgid ;
2006   unsigned long stack_canary ;
2007   struct task_struct *real_parent ;
2008   struct task_struct *parent ;
2009   struct list_head children ;
2010   struct list_head sibling ;
2011   struct task_struct *group_leader ;
2012   struct list_head ptraced ;
2013   struct list_head ptrace_entry ;
2014   struct pid_link pids[3] ;
2015   struct list_head thread_group ;
2016   struct completion *vfork_done ;
2017   int *set_child_tid ;
2018   int *clear_child_tid ;
2019   cputime_t utime ;
2020   cputime_t stime ;
2021   cputime_t utimescaled ;
2022   cputime_t stimescaled ;
2023   cputime_t gtime ;
2024   cputime_t prev_utime ;
2025   cputime_t prev_stime ;
2026   unsigned long nvcsw ;
2027   unsigned long nivcsw ;
2028   struct timespec start_time ;
2029   struct timespec real_start_time ;
2030   unsigned long min_flt ;
2031   unsigned long maj_flt ;
2032   struct task_cputime cputime_expires ;
2033   struct list_head cpu_timers[3] ;
2034   struct cred  const  *real_cred ;
2035   struct cred  const  *cred ;
2036   struct cred *replacement_session_keyring ;
2037   char comm[16] ;
2038   int link_count ;
2039   int total_link_count ;
2040   struct sysv_sem sysvsem ;
2041   unsigned long last_switch_count ;
2042   struct thread_struct thread ;
2043   struct fs_struct *fs ;
2044   struct files_struct *files ;
2045   struct nsproxy *nsproxy ;
2046   struct signal_struct *signal ;
2047   struct sighand_struct *sighand ;
2048   sigset_t blocked ;
2049   sigset_t real_blocked ;
2050   sigset_t saved_sigmask ;
2051   struct sigpending pending ;
2052   unsigned long sas_ss_sp ;
2053   size_t sas_ss_size ;
2054   int (*notifier)(void *priv ) ;
2055   void *notifier_data ;
2056   sigset_t *notifier_mask ;
2057   struct audit_context *audit_context ;
2058   uid_t loginuid ;
2059   unsigned int sessionid ;
2060   seccomp_t seccomp ;
2061   u32 parent_exec_id ;
2062   u32 self_exec_id ;
2063   spinlock_t alloc_lock ;
2064   raw_spinlock_t pi_lock ;
2065   struct plist_head pi_waiters ;
2066   struct rt_mutex_waiter *pi_blocked_on ;
2067   struct mutex_waiter *blocked_on ;
2068   unsigned int irq_events ;
2069   unsigned long hardirq_enable_ip ;
2070   unsigned long hardirq_disable_ip ;
2071   unsigned int hardirq_enable_event ;
2072   unsigned int hardirq_disable_event ;
2073   int hardirqs_enabled ;
2074   int hardirq_context ;
2075   unsigned long softirq_disable_ip ;
2076   unsigned long softirq_enable_ip ;
2077   unsigned int softirq_disable_event ;
2078   unsigned int softirq_enable_event ;
2079   int softirqs_enabled ;
2080   int softirq_context ;
2081   void *journal_info ;
2082   struct bio_list *bio_list ;
2083   struct blk_plug *plug ;
2084   struct reclaim_state *reclaim_state ;
2085   struct backing_dev_info *backing_dev_info ;
2086   struct io_context *io_context ;
2087   unsigned long ptrace_message ;
2088   siginfo_t *last_siginfo ;
2089   struct task_io_accounting ioac ;
2090   u64 acct_rss_mem1 ;
2091   u64 acct_vm_mem1 ;
2092   cputime_t acct_timexpd ;
2093   nodemask_t mems_allowed ;
2094   seqcount_t mems_allowed_seq ;
2095   int cpuset_mem_spread_rotor ;
2096   int cpuset_slab_spread_rotor ;
2097   struct css_set *cgroups ;
2098   struct list_head cg_list ;
2099   struct robust_list_head *robust_list ;
2100   struct compat_robust_list_head *compat_robust_list ;
2101   struct list_head pi_state_list ;
2102   struct futex_pi_state *pi_state_cache ;
2103   struct perf_event_context *perf_event_ctxp[2] ;
2104   struct mutex perf_event_mutex ;
2105   struct list_head perf_event_list ;
2106   struct mempolicy *mempolicy ;
2107   short il_next ;
2108   short pref_node_fork ;
2109   struct rcu_head rcu ;
2110   struct pipe_inode_info *splice_pipe ;
2111   struct task_delay_info *delays ;
2112   int make_it_fail ;
2113   int nr_dirtied ;
2114   int nr_dirtied_pause ;
2115   unsigned long dirty_paused_when ;
2116   int latency_record_count ;
2117   struct latency_record latency_record[32] ;
2118   unsigned long timer_slack_ns ;
2119   unsigned long default_timer_slack_ns ;
2120   struct list_head *scm_work_list ;
2121   unsigned long trace ;
2122   unsigned long trace_recursion ;
2123   struct memcg_batch_info memcg_batch ;
2124   atomic_t ptrace_bp_refcnt ;
2125};
2126#line 1681
2127struct pid_namespace;
2128#line 46 "include/linux/slub_def.h"
2129struct kmem_cache_cpu {
2130   void **freelist ;
2131   unsigned long tid ;
2132   struct page *page ;
2133   struct page *partial ;
2134   int node ;
2135   unsigned int stat[26] ;
2136};
2137#line 57 "include/linux/slub_def.h"
2138struct kmem_cache_node {
2139   spinlock_t list_lock ;
2140   unsigned long nr_partial ;
2141   struct list_head partial ;
2142   atomic_long_t nr_slabs ;
2143   atomic_long_t total_objects ;
2144   struct list_head full ;
2145};
2146#line 73 "include/linux/slub_def.h"
2147struct kmem_cache_order_objects {
2148   unsigned long x ;
2149};
2150#line 80 "include/linux/slub_def.h"
2151struct kmem_cache {
2152   struct kmem_cache_cpu *cpu_slab ;
2153   unsigned long flags ;
2154   unsigned long min_partial ;
2155   int size ;
2156   int objsize ;
2157   int offset ;
2158   int cpu_partial ;
2159   struct kmem_cache_order_objects oo ;
2160   struct kmem_cache_order_objects max ;
2161   struct kmem_cache_order_objects min ;
2162   gfp_t allocflags ;
2163   int refcount ;
2164   void (*ctor)(void * ) ;
2165   int inuse ;
2166   int align ;
2167   int reserved ;
2168   char const   *name ;
2169   struct list_head list ;
2170   struct kobject kobj ;
2171   int remote_node_defrag_ratio ;
2172   struct kmem_cache_node *node[1 << 10] ;
2173};
2174#line 161 "include/acpi/actypes.h"
2175typedef u64 acpi_size;
2176#line 371 "include/acpi/actypes.h"
2177typedef u32 acpi_status;
2178#line 876 "include/acpi/actypes.h"
2179struct acpi_buffer {
2180   acpi_size length ;
2181   void *pointer ;
2182};
2183#line 79 "include/acpi/actbl.h"
2184#pragma pack(1)
2185#line 321
2186#pragma pack()
2187#line 79 "include/acpi/actbl1.h"
2188#pragma pack(1)
2189#line 961
2190#pragma pack()
2191#line 96 "include/acpi/actbl2.h"
2192#pragma pack(1)
2193#line 1046
2194#pragma pack()
2195#line 87 "include/acpi/actbl3.h"
2196#pragma pack(1)
2197#line 550
2198#pragma pack()
2199#line 152 "include/acpi/acrestyp.h"
2200#pragma pack(1)
2201#line 588
2202#pragma pack()
2203#line 15 "include/linux/blk_types.h"
2204struct page;
2205#line 16
2206struct block_device;
2207#line 16
2208struct block_device;
2209#line 33 "include/linux/list_bl.h"
2210struct hlist_bl_node;
2211#line 33 "include/linux/list_bl.h"
2212struct hlist_bl_head {
2213   struct hlist_bl_node *first ;
2214};
2215#line 37 "include/linux/list_bl.h"
2216struct hlist_bl_node {
2217   struct hlist_bl_node *next ;
2218   struct hlist_bl_node **pprev ;
2219};
2220#line 13 "include/linux/dcache.h"
2221struct nameidata;
2222#line 13
2223struct nameidata;
2224#line 14
2225struct path;
2226#line 14
2227struct path;
2228#line 15
2229struct vfsmount;
2230#line 15
2231struct vfsmount;
2232#line 35 "include/linux/dcache.h"
2233struct qstr {
2234   unsigned int hash ;
2235   unsigned int len ;
2236   unsigned char const   *name ;
2237};
2238#line 88
2239struct dentry_operations;
2240#line 88
2241struct super_block;
2242#line 88 "include/linux/dcache.h"
2243union __anonunion_d_u_239 {
2244   struct list_head d_child ;
2245   struct rcu_head d_rcu ;
2246};
2247#line 88 "include/linux/dcache.h"
2248struct dentry {
2249   unsigned int d_flags ;
2250   seqcount_t d_seq ;
2251   struct hlist_bl_node d_hash ;
2252   struct dentry *d_parent ;
2253   struct qstr d_name ;
2254   struct inode *d_inode ;
2255   unsigned char d_iname[32] ;
2256   unsigned int d_count ;
2257   spinlock_t d_lock ;
2258   struct dentry_operations  const  *d_op ;
2259   struct super_block *d_sb ;
2260   unsigned long d_time ;
2261   void *d_fsdata ;
2262   struct list_head d_lru ;
2263   union __anonunion_d_u_239 d_u ;
2264   struct list_head d_subdirs ;
2265   struct list_head d_alias ;
2266};
2267#line 131 "include/linux/dcache.h"
2268struct dentry_operations {
2269   int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
2270   int (*d_hash)(struct dentry  const  * , struct inode  const  * , struct qstr * ) ;
2271   int (*d_compare)(struct dentry  const  * , struct inode  const  * , struct dentry  const  * ,
2272                    struct inode  const  * , unsigned int  , char const   * , struct qstr  const  * ) ;
2273   int (*d_delete)(struct dentry  const  * ) ;
2274   void (*d_release)(struct dentry * ) ;
2275   void (*d_prune)(struct dentry * ) ;
2276   void (*d_iput)(struct dentry * , struct inode * ) ;
2277   char *(*d_dname)(struct dentry * , char * , int  ) ;
2278   struct vfsmount *(*d_automount)(struct path * ) ;
2279   int (*d_manage)(struct dentry * , bool  ) ;
2280} __attribute__((__aligned__((1) <<  (6) ))) ;
2281#line 4 "include/linux/path.h"
2282struct dentry;
2283#line 5
2284struct vfsmount;
2285#line 7 "include/linux/path.h"
2286struct path {
2287   struct vfsmount *mnt ;
2288   struct dentry *dentry ;
2289};
2290#line 64 "include/linux/radix-tree.h"
2291struct radix_tree_node;
2292#line 64 "include/linux/radix-tree.h"
2293struct radix_tree_root {
2294   unsigned int height ;
2295   gfp_t gfp_mask ;
2296   struct radix_tree_node *rnode ;
2297};
2298#line 16 "include/linux/fiemap.h"
2299struct fiemap_extent {
2300   __u64 fe_logical ;
2301   __u64 fe_physical ;
2302   __u64 fe_length ;
2303   __u64 fe_reserved64[2] ;
2304   __u32 fe_flags ;
2305   __u32 fe_reserved[3] ;
2306};
2307#line 8 "include/linux/shrinker.h"
2308struct shrink_control {
2309   gfp_t gfp_mask ;
2310   unsigned long nr_to_scan ;
2311};
2312#line 31 "include/linux/shrinker.h"
2313struct shrinker {
2314   int (*shrink)(struct shrinker * , struct shrink_control *sc ) ;
2315   int seeks ;
2316   long batch ;
2317   struct list_head list ;
2318   atomic_long_t nr_in_batch ;
2319};
2320#line 10 "include/linux/migrate_mode.h"
2321enum migrate_mode {
2322    MIGRATE_ASYNC = 0,
2323    MIGRATE_SYNC_LIGHT = 1,
2324    MIGRATE_SYNC = 2
2325} ;
2326#line 408 "include/linux/fs.h"
2327struct export_operations;
2328#line 408
2329struct export_operations;
2330#line 410
2331struct iovec;
2332#line 411
2333struct nameidata;
2334#line 412
2335struct kiocb;
2336#line 413
2337struct kobject;
2338#line 414
2339struct pipe_inode_info;
2340#line 415
2341struct poll_table_struct;
2342#line 415
2343struct poll_table_struct;
2344#line 416
2345struct kstatfs;
2346#line 416
2347struct kstatfs;
2348#line 417
2349struct vm_area_struct;
2350#line 418
2351struct vfsmount;
2352#line 419
2353struct cred;
2354#line 469 "include/linux/fs.h"
2355struct iattr {
2356   unsigned int ia_valid ;
2357   umode_t ia_mode ;
2358   uid_t ia_uid ;
2359   gid_t ia_gid ;
2360   loff_t ia_size ;
2361   struct timespec ia_atime ;
2362   struct timespec ia_mtime ;
2363   struct timespec ia_ctime ;
2364   struct file *ia_file ;
2365};
2366#line 129 "include/linux/quota.h"
2367struct if_dqinfo {
2368   __u64 dqi_bgrace ;
2369   __u64 dqi_igrace ;
2370   __u32 dqi_flags ;
2371   __u32 dqi_valid ;
2372};
2373#line 50 "include/linux/dqblk_xfs.h"
2374struct fs_disk_quota {
2375   __s8 d_version ;
2376   __s8 d_flags ;
2377   __u16 d_fieldmask ;
2378   __u32 d_id ;
2379   __u64 d_blk_hardlimit ;
2380   __u64 d_blk_softlimit ;
2381   __u64 d_ino_hardlimit ;
2382   __u64 d_ino_softlimit ;
2383   __u64 d_bcount ;
2384   __u64 d_icount ;
2385   __s32 d_itimer ;
2386   __s32 d_btimer ;
2387   __u16 d_iwarns ;
2388   __u16 d_bwarns ;
2389   __s32 d_padding2 ;
2390   __u64 d_rtb_hardlimit ;
2391   __u64 d_rtb_softlimit ;
2392   __u64 d_rtbcount ;
2393   __s32 d_rtbtimer ;
2394   __u16 d_rtbwarns ;
2395   __s16 d_padding3 ;
2396   char d_padding4[8] ;
2397};
2398#line 146 "include/linux/dqblk_xfs.h"
2399struct fs_qfilestat {
2400   __u64 qfs_ino ;
2401   __u64 qfs_nblks ;
2402   __u32 qfs_nextents ;
2403};
2404#line 146 "include/linux/dqblk_xfs.h"
2405typedef struct fs_qfilestat fs_qfilestat_t;
2406#line 152 "include/linux/dqblk_xfs.h"
2407struct fs_quota_stat {
2408   __s8 qs_version ;
2409   __u16 qs_flags ;
2410   __s8 qs_pad ;
2411   fs_qfilestat_t qs_uquota ;
2412   fs_qfilestat_t qs_gquota ;
2413   __u32 qs_incoredqs ;
2414   __s32 qs_btimelimit ;
2415   __s32 qs_itimelimit ;
2416   __s32 qs_rtbtimelimit ;
2417   __u16 qs_bwarnlimit ;
2418   __u16 qs_iwarnlimit ;
2419};
2420#line 17 "include/linux/dqblk_qtree.h"
2421struct dquot;
2422#line 17
2423struct dquot;
2424#line 185 "include/linux/quota.h"
2425typedef __kernel_uid32_t qid_t;
2426#line 186 "include/linux/quota.h"
2427typedef long long qsize_t;
2428#line 200 "include/linux/quota.h"
2429struct mem_dqblk {
2430   qsize_t dqb_bhardlimit ;
2431   qsize_t dqb_bsoftlimit ;
2432   qsize_t dqb_curspace ;
2433   qsize_t dqb_rsvspace ;
2434   qsize_t dqb_ihardlimit ;
2435   qsize_t dqb_isoftlimit ;
2436   qsize_t dqb_curinodes ;
2437   time_t dqb_btime ;
2438   time_t dqb_itime ;
2439};
2440#line 215
2441struct quota_format_type;
2442#line 215
2443struct quota_format_type;
2444#line 217 "include/linux/quota.h"
2445struct mem_dqinfo {
2446   struct quota_format_type *dqi_format ;
2447   int dqi_fmt_id ;
2448   struct list_head dqi_dirty_list ;
2449   unsigned long dqi_flags ;
2450   unsigned int dqi_bgrace ;
2451   unsigned int dqi_igrace ;
2452   qsize_t dqi_maxblimit ;
2453   qsize_t dqi_maxilimit ;
2454   void *dqi_priv ;
2455};
2456#line 230
2457struct super_block;
2458#line 288 "include/linux/quota.h"
2459struct dquot {
2460   struct hlist_node dq_hash ;
2461   struct list_head dq_inuse ;
2462   struct list_head dq_free ;
2463   struct list_head dq_dirty ;
2464   struct mutex dq_lock ;
2465   atomic_t dq_count ;
2466   wait_queue_head_t dq_wait_unused ;
2467   struct super_block *dq_sb ;
2468   unsigned int dq_id ;
2469   loff_t dq_off ;
2470   unsigned long dq_flags ;
2471   short dq_type ;
2472   struct mem_dqblk dq_dqb ;
2473};
2474#line 305 "include/linux/quota.h"
2475struct quota_format_ops {
2476   int (*check_quota_file)(struct super_block *sb , int type ) ;
2477   int (*read_file_info)(struct super_block *sb , int type ) ;
2478   int (*write_file_info)(struct super_block *sb , int type ) ;
2479   int (*free_file_info)(struct super_block *sb , int type ) ;
2480   int (*read_dqblk)(struct dquot *dquot ) ;
2481   int (*commit_dqblk)(struct dquot *dquot ) ;
2482   int (*release_dqblk)(struct dquot *dquot ) ;
2483};
2484#line 316 "include/linux/quota.h"
2485struct dquot_operations {
2486   int (*write_dquot)(struct dquot * ) ;
2487   struct dquot *(*alloc_dquot)(struct super_block * , int  ) ;
2488   void (*destroy_dquot)(struct dquot * ) ;
2489   int (*acquire_dquot)(struct dquot * ) ;
2490   int (*release_dquot)(struct dquot * ) ;
2491   int (*mark_dirty)(struct dquot * ) ;
2492   int (*write_info)(struct super_block * , int  ) ;
2493   qsize_t *(*get_reserved_space)(struct inode * ) ;
2494};
2495#line 329
2496struct path;
2497#line 332 "include/linux/quota.h"
2498struct quotactl_ops {
2499   int (*quota_on)(struct super_block * , int  , int  , struct path * ) ;
2500   int (*quota_on_meta)(struct super_block * , int  , int  ) ;
2501   int (*quota_off)(struct super_block * , int  ) ;
2502   int (*quota_sync)(struct super_block * , int  , int  ) ;
2503   int (*get_info)(struct super_block * , int  , struct if_dqinfo * ) ;
2504   int (*set_info)(struct super_block * , int  , struct if_dqinfo * ) ;
2505   int (*get_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
2506   int (*set_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
2507   int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
2508   int (*set_xstate)(struct super_block * , unsigned int  , int  ) ;
2509};
2510#line 345 "include/linux/quota.h"
2511struct quota_format_type {
2512   int qf_fmt_id ;
2513   struct quota_format_ops  const  *qf_ops ;
2514   struct module *qf_owner ;
2515   struct quota_format_type *qf_next ;
2516};
2517#line 399 "include/linux/quota.h"
2518struct quota_info {
2519   unsigned int flags ;
2520   struct mutex dqio_mutex ;
2521   struct mutex dqonoff_mutex ;
2522   struct rw_semaphore dqptr_sem ;
2523   struct inode *files[2] ;
2524   struct mem_dqinfo info[2] ;
2525   struct quota_format_ops  const  *ops[2] ;
2526};
2527#line 532 "include/linux/fs.h"
2528struct page;
2529#line 533
2530struct address_space;
2531#line 534
2532struct writeback_control;
2533#line 534
2534struct writeback_control;
2535#line 577 "include/linux/fs.h"
2536union __anonunion_arg_246 {
2537   char *buf ;
2538   void *data ;
2539};
2540#line 577 "include/linux/fs.h"
2541struct __anonstruct_read_descriptor_t_245 {
2542   size_t written ;
2543   size_t count ;
2544   union __anonunion_arg_246 arg ;
2545   int error ;
2546};
2547#line 577 "include/linux/fs.h"
2548typedef struct __anonstruct_read_descriptor_t_245 read_descriptor_t;
2549#line 590 "include/linux/fs.h"
2550struct address_space_operations {
2551   int (*writepage)(struct page *page , struct writeback_control *wbc ) ;
2552   int (*readpage)(struct file * , struct page * ) ;
2553   int (*writepages)(struct address_space * , struct writeback_control * ) ;
2554   int (*set_page_dirty)(struct page *page ) ;
2555   int (*readpages)(struct file *filp , struct address_space *mapping , struct list_head *pages ,
2556                    unsigned int nr_pages ) ;
2557   int (*write_begin)(struct file * , struct address_space *mapping , loff_t pos ,
2558                      unsigned int len , unsigned int flags , struct page **pagep ,
2559                      void **fsdata ) ;
2560   int (*write_end)(struct file * , struct address_space *mapping , loff_t pos , unsigned int len ,
2561                    unsigned int copied , struct page *page , void *fsdata ) ;
2562   sector_t (*bmap)(struct address_space * , sector_t  ) ;
2563   void (*invalidatepage)(struct page * , unsigned long  ) ;
2564   int (*releasepage)(struct page * , gfp_t  ) ;
2565   void (*freepage)(struct page * ) ;
2566   ssize_t (*direct_IO)(int  , struct kiocb * , struct iovec  const  *iov , loff_t offset ,
2567                        unsigned long nr_segs ) ;
2568   int (*get_xip_mem)(struct address_space * , unsigned long  , int  , void ** , unsigned long * ) ;
2569   int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode  ) ;
2570   int (*launder_page)(struct page * ) ;
2571   int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long  ) ;
2572   int (*error_remove_page)(struct address_space * , struct page * ) ;
2573};
2574#line 645
2575struct backing_dev_info;
2576#line 646 "include/linux/fs.h"
2577struct address_space {
2578   struct inode *host ;
2579   struct radix_tree_root page_tree ;
2580   spinlock_t tree_lock ;
2581   unsigned int i_mmap_writable ;
2582   struct prio_tree_root i_mmap ;
2583   struct list_head i_mmap_nonlinear ;
2584   struct mutex i_mmap_mutex ;
2585   unsigned long nrpages ;
2586   unsigned long writeback_index ;
2587   struct address_space_operations  const  *a_ops ;
2588   unsigned long flags ;
2589   struct backing_dev_info *backing_dev_info ;
2590   spinlock_t private_lock ;
2591   struct list_head private_list ;
2592   struct address_space *assoc_mapping ;
2593} __attribute__((__aligned__(sizeof(long )))) ;
2594#line 669
2595struct request_queue;
2596#line 669
2597struct request_queue;
2598#line 671
2599struct hd_struct;
2600#line 671
2601struct gendisk;
2602#line 671 "include/linux/fs.h"
2603struct block_device {
2604   dev_t bd_dev ;
2605   int bd_openers ;
2606   struct inode *bd_inode ;
2607   struct super_block *bd_super ;
2608   struct mutex bd_mutex ;
2609   struct list_head bd_inodes ;
2610   void *bd_claiming ;
2611   void *bd_holder ;
2612   int bd_holders ;
2613   bool bd_write_holder ;
2614   struct list_head bd_holder_disks ;
2615   struct block_device *bd_contains ;
2616   unsigned int bd_block_size ;
2617   struct hd_struct *bd_part ;
2618   unsigned int bd_part_count ;
2619   int bd_invalidated ;
2620   struct gendisk *bd_disk ;
2621   struct request_queue *bd_queue ;
2622   struct list_head bd_list ;
2623   unsigned long bd_private ;
2624   int bd_fsfreeze_count ;
2625   struct mutex bd_fsfreeze_mutex ;
2626};
2627#line 749
2628struct posix_acl;
2629#line 749
2630struct posix_acl;
2631#line 761
2632struct inode_operations;
2633#line 761 "include/linux/fs.h"
2634union __anonunion____missing_field_name_247 {
2635   unsigned int const   i_nlink ;
2636   unsigned int __i_nlink ;
2637};
2638#line 761 "include/linux/fs.h"
2639union __anonunion____missing_field_name_248 {
2640   struct list_head i_dentry ;
2641   struct rcu_head i_rcu ;
2642};
2643#line 761
2644struct file_operations;
2645#line 761
2646struct file_lock;
2647#line 761
2648struct cdev;
2649#line 761 "include/linux/fs.h"
2650union __anonunion____missing_field_name_249 {
2651   struct pipe_inode_info *i_pipe ;
2652   struct block_device *i_bdev ;
2653   struct cdev *i_cdev ;
2654};
2655#line 761 "include/linux/fs.h"
2656struct inode {
2657   umode_t i_mode ;
2658   unsigned short i_opflags ;
2659   uid_t i_uid ;
2660   gid_t i_gid ;
2661   unsigned int i_flags ;
2662   struct posix_acl *i_acl ;
2663   struct posix_acl *i_default_acl ;
2664   struct inode_operations  const  *i_op ;
2665   struct super_block *i_sb ;
2666   struct address_space *i_mapping ;
2667   void *i_security ;
2668   unsigned long i_ino ;
2669   union __anonunion____missing_field_name_247 __annonCompField44 ;
2670   dev_t i_rdev ;
2671   struct timespec i_atime ;
2672   struct timespec i_mtime ;
2673   struct timespec i_ctime ;
2674   spinlock_t i_lock ;
2675   unsigned short i_bytes ;
2676   blkcnt_t i_blocks ;
2677   loff_t i_size ;
2678   unsigned long i_state ;
2679   struct mutex i_mutex ;
2680   unsigned long dirtied_when ;
2681   struct hlist_node i_hash ;
2682   struct list_head i_wb_list ;
2683   struct list_head i_lru ;
2684   struct list_head i_sb_list ;
2685   union __anonunion____missing_field_name_248 __annonCompField45 ;
2686   atomic_t i_count ;
2687   unsigned int i_blkbits ;
2688   u64 i_version ;
2689   atomic_t i_dio_count ;
2690   atomic_t i_writecount ;
2691   struct file_operations  const  *i_fop ;
2692   struct file_lock *i_flock ;
2693   struct address_space i_data ;
2694   struct dquot *i_dquot[2] ;
2695   struct list_head i_devices ;
2696   union __anonunion____missing_field_name_249 __annonCompField46 ;
2697   __u32 i_generation ;
2698   __u32 i_fsnotify_mask ;
2699   struct hlist_head i_fsnotify_marks ;
2700   atomic_t i_readcount ;
2701   void *i_private ;
2702};
2703#line 942 "include/linux/fs.h"
2704struct fown_struct {
2705   rwlock_t lock ;
2706   struct pid *pid ;
2707   enum pid_type pid_type ;
2708   uid_t uid ;
2709   uid_t euid ;
2710   int signum ;
2711};
2712#line 953 "include/linux/fs.h"
2713struct file_ra_state {
2714   unsigned long start ;
2715   unsigned int size ;
2716   unsigned int async_size ;
2717   unsigned int ra_pages ;
2718   unsigned int mmap_miss ;
2719   loff_t prev_pos ;
2720};
2721#line 976 "include/linux/fs.h"
2722union __anonunion_f_u_250 {
2723   struct list_head fu_list ;
2724   struct rcu_head fu_rcuhead ;
2725};
2726#line 976 "include/linux/fs.h"
2727struct file {
2728   union __anonunion_f_u_250 f_u ;
2729   struct path f_path ;
2730   struct file_operations  const  *f_op ;
2731   spinlock_t f_lock ;
2732   int f_sb_list_cpu ;
2733   atomic_long_t f_count ;
2734   unsigned int f_flags ;
2735   fmode_t f_mode ;
2736   loff_t f_pos ;
2737   struct fown_struct f_owner ;
2738   struct cred  const  *f_cred ;
2739   struct file_ra_state f_ra ;
2740   u64 f_version ;
2741   void *f_security ;
2742   void *private_data ;
2743   struct list_head f_ep_links ;
2744   struct list_head f_tfile_llink ;
2745   struct address_space *f_mapping ;
2746   unsigned long f_mnt_write_state ;
2747};
2748#line 1111 "include/linux/fs.h"
2749typedef struct files_struct *fl_owner_t;
2750#line 1113 "include/linux/fs.h"
2751struct file_lock_operations {
2752   void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
2753   void (*fl_release_private)(struct file_lock * ) ;
2754};
2755#line 1118 "include/linux/fs.h"
2756struct lock_manager_operations {
2757   int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
2758   void (*lm_notify)(struct file_lock * ) ;
2759   int (*lm_grant)(struct file_lock * , struct file_lock * , int  ) ;
2760   void (*lm_release_private)(struct file_lock * ) ;
2761   void (*lm_break)(struct file_lock * ) ;
2762   int (*lm_change)(struct file_lock ** , int  ) ;
2763};
2764#line 4 "include/linux/nfs_fs_i.h"
2765struct nlm_lockowner;
2766#line 4
2767struct nlm_lockowner;
2768#line 9 "include/linux/nfs_fs_i.h"
2769struct nfs_lock_info {
2770   u32 state ;
2771   struct nlm_lockowner *owner ;
2772   struct list_head list ;
2773};
2774#line 15
2775struct nfs4_lock_state;
2776#line 15
2777struct nfs4_lock_state;
2778#line 16 "include/linux/nfs_fs_i.h"
2779struct nfs4_lock_info {
2780   struct nfs4_lock_state *owner ;
2781};
2782#line 1138 "include/linux/fs.h"
2783struct fasync_struct;
2784#line 1138 "include/linux/fs.h"
2785struct __anonstruct_afs_252 {
2786   struct list_head link ;
2787   int state ;
2788};
2789#line 1138 "include/linux/fs.h"
2790union __anonunion_fl_u_251 {
2791   struct nfs_lock_info nfs_fl ;
2792   struct nfs4_lock_info nfs4_fl ;
2793   struct __anonstruct_afs_252 afs ;
2794};
2795#line 1138 "include/linux/fs.h"
2796struct file_lock {
2797   struct file_lock *fl_next ;
2798   struct list_head fl_link ;
2799   struct list_head fl_block ;
2800   fl_owner_t fl_owner ;
2801   unsigned int fl_flags ;
2802   unsigned char fl_type ;
2803   unsigned int fl_pid ;
2804   struct pid *fl_nspid ;
2805   wait_queue_head_t fl_wait ;
2806   struct file *fl_file ;
2807   loff_t fl_start ;
2808   loff_t fl_end ;
2809   struct fasync_struct *fl_fasync ;
2810   unsigned long fl_break_time ;
2811   unsigned long fl_downgrade_time ;
2812   struct file_lock_operations  const  *fl_ops ;
2813   struct lock_manager_operations  const  *fl_lmops ;
2814   union __anonunion_fl_u_251 fl_u ;
2815};
2816#line 1378 "include/linux/fs.h"
2817struct fasync_struct {
2818   spinlock_t fa_lock ;
2819   int magic ;
2820   int fa_fd ;
2821   struct fasync_struct *fa_next ;
2822   struct file *fa_file ;
2823   struct rcu_head fa_rcu ;
2824};
2825#line 1418
2826struct file_system_type;
2827#line 1418
2828struct super_operations;
2829#line 1418
2830struct xattr_handler;
2831#line 1418
2832struct mtd_info;
2833#line 1418 "include/linux/fs.h"
2834struct super_block {
2835   struct list_head s_list ;
2836   dev_t s_dev ;
2837   unsigned char s_dirt ;
2838   unsigned char s_blocksize_bits ;
2839   unsigned long s_blocksize ;
2840   loff_t s_maxbytes ;
2841   struct file_system_type *s_type ;
2842   struct super_operations  const  *s_op ;
2843   struct dquot_operations  const  *dq_op ;
2844   struct quotactl_ops  const  *s_qcop ;
2845   struct export_operations  const  *s_export_op ;
2846   unsigned long s_flags ;
2847   unsigned long s_magic ;
2848   struct dentry *s_root ;
2849   struct rw_semaphore s_umount ;
2850   struct mutex s_lock ;
2851   int s_count ;
2852   atomic_t s_active ;
2853   void *s_security ;
2854   struct xattr_handler  const  **s_xattr ;
2855   struct list_head s_inodes ;
2856   struct hlist_bl_head s_anon ;
2857   struct list_head *s_files ;
2858   struct list_head s_mounts ;
2859   struct list_head s_dentry_lru ;
2860   int s_nr_dentry_unused ;
2861   spinlock_t s_inode_lru_lock  __attribute__((__aligned__((1) <<  (6) ))) ;
2862   struct list_head s_inode_lru ;
2863   int s_nr_inodes_unused ;
2864   struct block_device *s_bdev ;
2865   struct backing_dev_info *s_bdi ;
2866   struct mtd_info *s_mtd ;
2867   struct hlist_node s_instances ;
2868   struct quota_info s_dquot ;
2869   int s_frozen ;
2870   wait_queue_head_t s_wait_unfrozen ;
2871   char s_id[32] ;
2872   u8 s_uuid[16] ;
2873   void *s_fs_info ;
2874   unsigned int s_max_links ;
2875   fmode_t s_mode ;
2876   u32 s_time_gran ;
2877   struct mutex s_vfs_rename_mutex ;
2878   char *s_subtype ;
2879   char *s_options ;
2880   struct dentry_operations  const  *s_d_op ;
2881   int cleancache_poolid ;
2882   struct shrinker s_shrink ;
2883   atomic_long_t s_remove_count ;
2884   int s_readonly_remount ;
2885};
2886#line 1567 "include/linux/fs.h"
2887struct fiemap_extent_info {
2888   unsigned int fi_flags ;
2889   unsigned int fi_extents_mapped ;
2890   unsigned int fi_extents_max ;
2891   struct fiemap_extent *fi_extents_start ;
2892};
2893#line 1609 "include/linux/fs.h"
2894struct file_operations {
2895   struct module *owner ;
2896   loff_t (*llseek)(struct file * , loff_t  , int  ) ;
2897   ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
2898   ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
2899   ssize_t (*aio_read)(struct kiocb * , struct iovec  const  * , unsigned long  ,
2900                       loff_t  ) ;
2901   ssize_t (*aio_write)(struct kiocb * , struct iovec  const  * , unsigned long  ,
2902                        loff_t  ) ;
2903   int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
2904                                                   loff_t  , u64  , unsigned int  ) ) ;
2905   unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
2906   long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
2907   long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
2908   int (*mmap)(struct file * , struct vm_area_struct * ) ;
2909   int (*open)(struct inode * , struct file * ) ;
2910   int (*flush)(struct file * , fl_owner_t id ) ;
2911   int (*release)(struct inode * , struct file * ) ;
2912   int (*fsync)(struct file * , loff_t  , loff_t  , int datasync ) ;
2913   int (*aio_fsync)(struct kiocb * , int datasync ) ;
2914   int (*fasync)(int  , struct file * , int  ) ;
2915   int (*lock)(struct file * , int  , struct file_lock * ) ;
2916   ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
2917                       int  ) ;
2918   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
2919                                      unsigned long  , unsigned long  ) ;
2920   int (*check_flags)(int  ) ;
2921   int (*flock)(struct file * , int  , struct file_lock * ) ;
2922   ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t  ,
2923                           unsigned int  ) ;
2924   ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t  ,
2925                          unsigned int  ) ;
2926   int (*setlease)(struct file * , long  , struct file_lock ** ) ;
2927   long (*fallocate)(struct file *file , int mode , loff_t offset , loff_t len ) ;
2928};
2929#line 1639 "include/linux/fs.h"
2930struct inode_operations {
2931   struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
2932   void *(*follow_link)(struct dentry * , struct nameidata * ) ;
2933   int (*permission)(struct inode * , int  ) ;
2934   struct posix_acl *(*get_acl)(struct inode * , int  ) ;
2935   int (*readlink)(struct dentry * , char * , int  ) ;
2936   void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
2937   int (*create)(struct inode * , struct dentry * , umode_t  , struct nameidata * ) ;
2938   int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
2939   int (*unlink)(struct inode * , struct dentry * ) ;
2940   int (*symlink)(struct inode * , struct dentry * , char const   * ) ;
2941   int (*mkdir)(struct inode * , struct dentry * , umode_t  ) ;
2942   int (*rmdir)(struct inode * , struct dentry * ) ;
2943   int (*mknod)(struct inode * , struct dentry * , umode_t  , dev_t  ) ;
2944   int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
2945   void (*truncate)(struct inode * ) ;
2946   int (*setattr)(struct dentry * , struct iattr * ) ;
2947   int (*getattr)(struct vfsmount *mnt , struct dentry * , struct kstat * ) ;
2948   int (*setxattr)(struct dentry * , char const   * , void const   * , size_t  , int  ) ;
2949   ssize_t (*getxattr)(struct dentry * , char const   * , void * , size_t  ) ;
2950   ssize_t (*listxattr)(struct dentry * , char * , size_t  ) ;
2951   int (*removexattr)(struct dentry * , char const   * ) ;
2952   void (*truncate_range)(struct inode * , loff_t  , loff_t  ) ;
2953   int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 start , u64 len ) ;
2954} __attribute__((__aligned__((1) <<  (6) ))) ;
2955#line 1669
2956struct seq_file;
2957#line 1684 "include/linux/fs.h"
2958struct super_operations {
2959   struct inode *(*alloc_inode)(struct super_block *sb ) ;
2960   void (*destroy_inode)(struct inode * ) ;
2961   void (*dirty_inode)(struct inode * , int flags ) ;
2962   int (*write_inode)(struct inode * , struct writeback_control *wbc ) ;
2963   int (*drop_inode)(struct inode * ) ;
2964   void (*evict_inode)(struct inode * ) ;
2965   void (*put_super)(struct super_block * ) ;
2966   void (*write_super)(struct super_block * ) ;
2967   int (*sync_fs)(struct super_block *sb , int wait ) ;
2968   int (*freeze_fs)(struct super_block * ) ;
2969   int (*unfreeze_fs)(struct super_block * ) ;
2970   int (*statfs)(struct dentry * , struct kstatfs * ) ;
2971   int (*remount_fs)(struct super_block * , int * , char * ) ;
2972   void (*umount_begin)(struct super_block * ) ;
2973   int (*show_options)(struct seq_file * , struct dentry * ) ;
2974   int (*show_devname)(struct seq_file * , struct dentry * ) ;
2975   int (*show_path)(struct seq_file * , struct dentry * ) ;
2976   int (*show_stats)(struct seq_file * , struct dentry * ) ;
2977   ssize_t (*quota_read)(struct super_block * , int  , char * , size_t  , loff_t  ) ;
2978   ssize_t (*quota_write)(struct super_block * , int  , char const   * , size_t  ,
2979                          loff_t  ) ;
2980   int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t  ) ;
2981   int (*nr_cached_objects)(struct super_block * ) ;
2982   void (*free_cached_objects)(struct super_block * , int  ) ;
2983};
2984#line 1835 "include/linux/fs.h"
2985struct file_system_type {
2986   char const   *name ;
2987   int fs_flags ;
2988   struct dentry *(*mount)(struct file_system_type * , int  , char const   * , void * ) ;
2989   void (*kill_sb)(struct super_block * ) ;
2990   struct module *owner ;
2991   struct file_system_type *next ;
2992   struct hlist_head fs_supers ;
2993   struct lock_class_key s_lock_key ;
2994   struct lock_class_key s_umount_key ;
2995   struct lock_class_key s_vfs_rename_key ;
2996   struct lock_class_key i_lock_key ;
2997   struct lock_class_key i_mutex_key ;
2998   struct lock_class_key i_mutex_dir_key ;
2999};
3000#line 11 "include/linux/proc_fs.h"
3001struct completion;
3002#line 12
3003struct mm_struct;
3004#line 117
3005struct pid_namespace;
3006#line 243
3007struct nsproxy;
3008#line 38 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3009struct mxds_args {
3010   u32 func ;
3011   u32 args ;
3012   u32 xarg ;
3013};
3014#line 1 "<compiler builtins>"
3015long __builtin_expect(long val , long res ) ;
3016#line 100 "include/linux/printk.h"
3017extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
3018#line 152 "include/linux/mutex.h"
3019void mutex_lock(struct mutex *lock ) ;
3020#line 153
3021int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
3022#line 154
3023int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
3024#line 168
3025int mutex_trylock(struct mutex *lock ) ;
3026#line 169
3027void mutex_unlock(struct mutex *lock ) ;
3028#line 170
3029int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
3030#line 67 "include/linux/module.h"
3031int init_module(void) ;
3032#line 68
3033void cleanup_module(void) ;
3034#line 160 "include/linux/acpi.h"
3035extern acpi_status wmi_evaluate_method(char const   *guid , u8 instance , u32 method_id ,
3036                                       struct acpi_buffer  const  *in , struct acpi_buffer *out ) ;
3037#line 172
3038extern bool wmi_has_guid(char const   *guid ) ;
3039#line 27 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3040static char const   __mod_author27[19]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3041__aligned__(1)))  = 
3042#line 27 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3043  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
3044        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'D', 
3045        (char const   )'a',      (char const   )'v',      (char const   )'e',      (char const   )' ', 
3046        (char const   )'A',      (char const   )'i',      (char const   )'r',      (char const   )'l', 
3047        (char const   )'i',      (char const   )'e',      (char const   )'\000'};
3048#line 28 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3049static char const   __mod_description28[27]  __attribute__((__used__, __unused__,
3050__section__(".modinfo"), __aligned__(1)))  = 
3051#line 28
3052  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
3053        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
3054        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
3055        (char const   )'M',      (char const   )'X',      (char const   )'M',      (char const   )' ', 
3056        (char const   )'W',      (char const   )'M',      (char const   )'I',      (char const   )' ', 
3057        (char const   )'D',      (char const   )'r',      (char const   )'i',      (char const   )'v', 
3058        (char const   )'e',      (char const   )'r',      (char const   )'\000'};
3059#line 29 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3060static char const   __mod_license29[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3061__aligned__(1)))  = 
3062#line 29
3063  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
3064        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
3065        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
3066#line 33 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3067static char const   __mod_alias33[47]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3068__aligned__(1)))  = 
3069#line 33
3070  {      (char const   )'a',      (char const   )'l',      (char const   )'i',      (char const   )'a', 
3071        (char const   )'s',      (char const   )'=',      (char const   )'w',      (char const   )'m', 
3072        (char const   )'i',      (char const   )':',      (char const   )'F',      (char const   )'6', 
3073        (char const   )'C',      (char const   )'B',      (char const   )'5',      (char const   )'C', 
3074        (char const   )'3',      (char const   )'C',      (char const   )'-',      (char const   )'9', 
3075        (char const   )'C',      (char const   )'A',      (char const   )'E',      (char const   )'-', 
3076        (char const   )'4',      (char const   )'E',      (char const   )'B',      (char const   )'D', 
3077        (char const   )'-',      (char const   )'B',      (char const   )'5',      (char const   )'7', 
3078        (char const   )'7',      (char const   )'-',      (char const   )'9',      (char const   )'3', 
3079        (char const   )'1',      (char const   )'E',      (char const   )'A',      (char const   )'3', 
3080        (char const   )'2',      (char const   )'A',      (char const   )'2',      (char const   )'C', 
3081        (char const   )'C',      (char const   )'0',      (char const   )'\000'};
3082#line 44 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3083int mxm_wmi_call_mxds(int adapter ) 
3084{ struct mxds_args args ;
3085  struct acpi_buffer input ;
3086  struct acpi_buffer output ;
3087  acpi_status status ;
3088  struct mxds_args *__cil_tmp6 ;
3089  unsigned long __cil_tmp7 ;
3090  unsigned long __cil_tmp8 ;
3091  struct acpi_buffer *__cil_tmp9 ;
3092  unsigned long __cil_tmp10 ;
3093  struct acpi_buffer *__cil_tmp11 ;
3094  unsigned long __cil_tmp12 ;
3095  u8 __cil_tmp13 ;
3096  u32 __cil_tmp14 ;
3097  struct acpi_buffer  const  *__cil_tmp15 ;
3098
3099  {
3100  {
3101#line 46
3102  __cil_tmp6 = & args;
3103#line 46
3104  *((u32 *)__cil_tmp6) = (u32 )1396987981;
3105#line 46
3106  __cil_tmp7 = (unsigned long )(& args) + 4;
3107#line 46
3108  *((u32 *)__cil_tmp7) = (u32 )0;
3109#line 46
3110  __cil_tmp8 = (unsigned long )(& args) + 8;
3111#line 46
3112  *((u32 *)__cil_tmp8) = (u32 )1;
3113#line 51
3114  __cil_tmp9 = & input;
3115#line 51
3116  *((acpi_size *)__cil_tmp9) = (acpi_size )12UL;
3117#line 51
3118  __cil_tmp10 = (unsigned long )(& input) + 8;
3119#line 51
3120  *((void **)__cil_tmp10) = (void *)(& args);
3121#line 52
3122  __cil_tmp11 = & output;
3123#line 52
3124  *((acpi_size *)__cil_tmp11) = (acpi_size )-1;
3125#line 52
3126  __cil_tmp12 = (unsigned long )(& output) + 8;
3127#line 52
3128  *((void **)__cil_tmp12) = (void *)0;
3129#line 55
3130  printk("calling mux switch %d\n", adapter);
3131#line 57
3132  __cil_tmp13 = (u8 )1;
3133#line 57
3134  __cil_tmp14 = (u32 )adapter;
3135#line 57
3136  __cil_tmp15 = (struct acpi_buffer  const  *)(& input);
3137#line 57
3138  status = wmi_evaluate_method("F6CB5C3C-9CAE-4EBD-B577-931EA32A2CC0", __cil_tmp13,
3139                               __cil_tmp14, __cil_tmp15, & output);
3140  }
3141#line 60
3142  if (status) {
3143#line 61
3144    return ((int )status);
3145  } else {
3146
3147  }
3148  {
3149#line 63
3150  printk("mux switched %d\n", status);
3151  }
3152#line 64
3153  return (0);
3154}
3155}
3156#line 67
3157extern void *__crc_mxm_wmi_call_mxds  __attribute__((__weak__)) ;
3158#line 67 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3159static unsigned long const   __kcrctab_mxm_wmi_call_mxds  __attribute__((__used__,
3160__unused__, __section__("___kcrctab_gpl+mxm_wmi_call_mxds")))  =    (unsigned long const   )((unsigned long )(& __crc_mxm_wmi_call_mxds));
3161#line 67 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3162static char const   __kstrtab_mxm_wmi_call_mxds[18]  __attribute__((__section__("__ksymtab_strings"),
3163__aligned__(1)))  = 
3164#line 67
3165  {      (char const   )'m',      (char const   )'x',      (char const   )'m',      (char const   )'_', 
3166        (char const   )'w',      (char const   )'m',      (char const   )'i',      (char const   )'_', 
3167        (char const   )'c',      (char const   )'a',      (char const   )'l',      (char const   )'l', 
3168        (char const   )'_',      (char const   )'m',      (char const   )'x',      (char const   )'d', 
3169        (char const   )'s',      (char const   )'\000'};
3170#line 67 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3171static struct kernel_symbol  const  __ksymtab_mxm_wmi_call_mxds  __attribute__((__used__,
3172__unused__, __section__("___ksymtab_gpl+mxm_wmi_call_mxds")))  =    {(unsigned long )(& mxm_wmi_call_mxds), __kstrtab_mxm_wmi_call_mxds};
3173#line 69 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3174int mxm_wmi_call_mxmx(int adapter ) 
3175{ struct mxds_args args ;
3176  struct acpi_buffer input ;
3177  struct acpi_buffer output ;
3178  acpi_status status ;
3179  struct mxds_args *__cil_tmp6 ;
3180  unsigned long __cil_tmp7 ;
3181  unsigned long __cil_tmp8 ;
3182  struct acpi_buffer *__cil_tmp9 ;
3183  unsigned long __cil_tmp10 ;
3184  struct acpi_buffer *__cil_tmp11 ;
3185  unsigned long __cil_tmp12 ;
3186  u8 __cil_tmp13 ;
3187  u32 __cil_tmp14 ;
3188  struct acpi_buffer  const  *__cil_tmp15 ;
3189
3190  {
3191  {
3192#line 71
3193  __cil_tmp6 = & args;
3194#line 71
3195  *((u32 *)__cil_tmp6) = (u32 )1396986692;
3196#line 71
3197  __cil_tmp7 = (unsigned long )(& args) + 4;
3198#line 71
3199  *((u32 *)__cil_tmp7) = (u32 )0;
3200#line 71
3201  __cil_tmp8 = (unsigned long )(& args) + 8;
3202#line 71
3203  *((u32 *)__cil_tmp8) = (u32 )1;
3204#line 76
3205  __cil_tmp9 = & input;
3206#line 76
3207  *((acpi_size *)__cil_tmp9) = (acpi_size )12UL;
3208#line 76
3209  __cil_tmp10 = (unsigned long )(& input) + 8;
3210#line 76
3211  *((void **)__cil_tmp10) = (void *)(& args);
3212#line 77
3213  __cil_tmp11 = & output;
3214#line 77
3215  *((acpi_size *)__cil_tmp11) = (acpi_size )-1;
3216#line 77
3217  __cil_tmp12 = (unsigned long )(& output) + 8;
3218#line 77
3219  *((void **)__cil_tmp12) = (void *)0;
3220#line 80
3221  printk("calling mux switch %d\n", adapter);
3222#line 82
3223  __cil_tmp13 = (u8 )1;
3224#line 82
3225  __cil_tmp14 = (u32 )adapter;
3226#line 82
3227  __cil_tmp15 = (struct acpi_buffer  const  *)(& input);
3228#line 82
3229  status = wmi_evaluate_method("F6CB5C3C-9CAE-4EBD-B577-931EA32A2CC0", __cil_tmp13,
3230                               __cil_tmp14, __cil_tmp15, & output);
3231  }
3232#line 85
3233  if (status) {
3234#line 86
3235    return ((int )status);
3236  } else {
3237
3238  }
3239  {
3240#line 88
3241  printk("mux mutex set switched %d\n", status);
3242  }
3243#line 89
3244  return (0);
3245}
3246}
3247#line 92
3248extern void *__crc_mxm_wmi_call_mxmx  __attribute__((__weak__)) ;
3249#line 92 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3250static unsigned long const   __kcrctab_mxm_wmi_call_mxmx  __attribute__((__used__,
3251__unused__, __section__("___kcrctab_gpl+mxm_wmi_call_mxmx")))  =    (unsigned long const   )((unsigned long )(& __crc_mxm_wmi_call_mxmx));
3252#line 92 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3253static char const   __kstrtab_mxm_wmi_call_mxmx[18]  __attribute__((__section__("__ksymtab_strings"),
3254__aligned__(1)))  = 
3255#line 92
3256  {      (char const   )'m',      (char const   )'x',      (char const   )'m',      (char const   )'_', 
3257        (char const   )'w',      (char const   )'m',      (char const   )'i',      (char const   )'_', 
3258        (char const   )'c',      (char const   )'a',      (char const   )'l',      (char const   )'l', 
3259        (char const   )'_',      (char const   )'m',      (char const   )'x',      (char const   )'m', 
3260        (char const   )'x',      (char const   )'\000'};
3261#line 92 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3262static struct kernel_symbol  const  __ksymtab_mxm_wmi_call_mxmx  __attribute__((__used__,
3263__unused__, __section__("___ksymtab_gpl+mxm_wmi_call_mxmx")))  =    {(unsigned long )(& mxm_wmi_call_mxmx), __kstrtab_mxm_wmi_call_mxmx};
3264#line 94 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3265bool mxm_wmi_supported(void) 
3266{ bool guid_valid ;
3267
3268  {
3269  {
3270#line 97
3271  guid_valid = wmi_has_guid("F6CB5C3C-9CAE-4EBD-B577-931EA32A2CC0");
3272  }
3273#line 98
3274  return (guid_valid);
3275}
3276}
3277#line 100
3278extern void *__crc_mxm_wmi_supported  __attribute__((__weak__)) ;
3279#line 100 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3280static unsigned long const   __kcrctab_mxm_wmi_supported  __attribute__((__used__,
3281__unused__, __section__("___kcrctab_gpl+mxm_wmi_supported")))  =    (unsigned long const   )((unsigned long )(& __crc_mxm_wmi_supported));
3282#line 100 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3283static char const   __kstrtab_mxm_wmi_supported[18]  __attribute__((__section__("__ksymtab_strings"),
3284__aligned__(1)))  = 
3285#line 100
3286  {      (char const   )'m',      (char const   )'x',      (char const   )'m',      (char const   )'_', 
3287        (char const   )'w',      (char const   )'m',      (char const   )'i',      (char const   )'_', 
3288        (char const   )'s',      (char const   )'u',      (char const   )'p',      (char const   )'p', 
3289        (char const   )'o',      (char const   )'r',      (char const   )'t',      (char const   )'e', 
3290        (char const   )'d',      (char const   )'\000'};
3291#line 100 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3292static struct kernel_symbol  const  __ksymtab_mxm_wmi_supported  __attribute__((__used__,
3293__unused__, __section__("___ksymtab_gpl+mxm_wmi_supported")))  =    {(unsigned long )(& mxm_wmi_supported), __kstrtab_mxm_wmi_supported};
3294#line 102
3295static int mxm_wmi_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
3296#line 102 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3297static int mxm_wmi_init(void) 
3298{ 
3299
3300  {
3301#line 104
3302  return (0);
3303}
3304}
3305#line 107
3306static void mxm_wmi_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
3307#line 107 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3308static void mxm_wmi_exit(void) 
3309{ 
3310
3311  {
3312#line 109
3313  return;
3314}
3315}
3316#line 111 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3317int init_module(void) 
3318{ int tmp___7 ;
3319
3320  {
3321  {
3322#line 111
3323  tmp___7 = mxm_wmi_init();
3324  }
3325#line 111
3326  return (tmp___7);
3327}
3328}
3329#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3330void cleanup_module(void) 
3331{ 
3332
3333  {
3334  {
3335#line 112
3336  mxm_wmi_exit();
3337  }
3338#line 112
3339  return;
3340}
3341}
3342#line 130
3343void ldv_check_final_state(void) ;
3344#line 136
3345extern void ldv_initialize(void) ;
3346#line 139
3347extern int __VERIFIER_nondet_int(void) ;
3348#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3349int LDV_IN_INTERRUPT  ;
3350#line 145 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3351void main(void) 
3352{ int tmp___7 ;
3353  int tmp___8 ;
3354  int tmp___9 ;
3355
3356  {
3357  {
3358#line 157
3359  LDV_IN_INTERRUPT = 1;
3360#line 166
3361  ldv_initialize();
3362#line 176
3363  tmp___7 = mxm_wmi_init();
3364  }
3365#line 176
3366  if (tmp___7) {
3367#line 177
3368    goto ldv_final;
3369  } else {
3370
3371  }
3372  {
3373#line 179
3374  while (1) {
3375    while_continue: /* CIL Label */ ;
3376    {
3377#line 179
3378    tmp___9 = __VERIFIER_nondet_int();
3379    }
3380#line 179
3381    if (tmp___9) {
3382
3383    } else {
3384#line 179
3385      goto while_break;
3386    }
3387    {
3388#line 182
3389    tmp___8 = __VERIFIER_nondet_int();
3390    }
3391    {
3392#line 184
3393    goto switch_default;
3394#line 182
3395    if (0) {
3396      switch_default: /* CIL Label */ 
3397#line 184
3398      goto switch_break;
3399    } else {
3400      switch_break: /* CIL Label */ ;
3401    }
3402    }
3403  }
3404  while_break: /* CIL Label */ ;
3405  }
3406  {
3407#line 200
3408  mxm_wmi_exit();
3409  }
3410  ldv_final: 
3411  {
3412#line 203
3413  ldv_check_final_state();
3414  }
3415#line 206
3416  return;
3417}
3418}
3419#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3420void ldv_blast_assert(void) 
3421{ 
3422
3423  {
3424  ERROR: 
3425#line 6
3426  goto ERROR;
3427}
3428}
3429#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3430extern int __VERIFIER_nondet_int(void) ;
3431#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3432int ldv_mutex  =    1;
3433#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3434int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
3435{ int nondetermined ;
3436
3437  {
3438#line 29
3439  if (ldv_mutex == 1) {
3440
3441  } else {
3442    {
3443#line 29
3444    ldv_blast_assert();
3445    }
3446  }
3447  {
3448#line 32
3449  nondetermined = __VERIFIER_nondet_int();
3450  }
3451#line 35
3452  if (nondetermined) {
3453#line 38
3454    ldv_mutex = 2;
3455#line 40
3456    return (0);
3457  } else {
3458#line 45
3459    return (-4);
3460  }
3461}
3462}
3463#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3464int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
3465{ int nondetermined ;
3466
3467  {
3468#line 57
3469  if (ldv_mutex == 1) {
3470
3471  } else {
3472    {
3473#line 57
3474    ldv_blast_assert();
3475    }
3476  }
3477  {
3478#line 60
3479  nondetermined = __VERIFIER_nondet_int();
3480  }
3481#line 63
3482  if (nondetermined) {
3483#line 66
3484    ldv_mutex = 2;
3485#line 68
3486    return (0);
3487  } else {
3488#line 73
3489    return (-4);
3490  }
3491}
3492}
3493#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3494int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
3495{ int atomic_value_after_dec ;
3496
3497  {
3498#line 83
3499  if (ldv_mutex == 1) {
3500
3501  } else {
3502    {
3503#line 83
3504    ldv_blast_assert();
3505    }
3506  }
3507  {
3508#line 86
3509  atomic_value_after_dec = __VERIFIER_nondet_int();
3510  }
3511#line 89
3512  if (atomic_value_after_dec == 0) {
3513#line 92
3514    ldv_mutex = 2;
3515#line 94
3516    return (1);
3517  } else {
3518
3519  }
3520#line 98
3521  return (0);
3522}
3523}
3524#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3525void mutex_lock(struct mutex *lock ) 
3526{ 
3527
3528  {
3529#line 108
3530  if (ldv_mutex == 1) {
3531
3532  } else {
3533    {
3534#line 108
3535    ldv_blast_assert();
3536    }
3537  }
3538#line 110
3539  ldv_mutex = 2;
3540#line 111
3541  return;
3542}
3543}
3544#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3545int mutex_trylock(struct mutex *lock ) 
3546{ int nondetermined ;
3547
3548  {
3549#line 121
3550  if (ldv_mutex == 1) {
3551
3552  } else {
3553    {
3554#line 121
3555    ldv_blast_assert();
3556    }
3557  }
3558  {
3559#line 124
3560  nondetermined = __VERIFIER_nondet_int();
3561  }
3562#line 127
3563  if (nondetermined) {
3564#line 130
3565    ldv_mutex = 2;
3566#line 132
3567    return (1);
3568  } else {
3569#line 137
3570    return (0);
3571  }
3572}
3573}
3574#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3575void mutex_unlock(struct mutex *lock ) 
3576{ 
3577
3578  {
3579#line 147
3580  if (ldv_mutex == 2) {
3581
3582  } else {
3583    {
3584#line 147
3585    ldv_blast_assert();
3586    }
3587  }
3588#line 149
3589  ldv_mutex = 1;
3590#line 150
3591  return;
3592}
3593}
3594#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3595void ldv_check_final_state(void) 
3596{ 
3597
3598  {
3599#line 156
3600  if (ldv_mutex == 1) {
3601
3602  } else {
3603    {
3604#line 156
3605    ldv_blast_assert();
3606    }
3607  }
3608#line 157
3609  return;
3610}
3611}
3612#line 215 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5734/dscv_tempdir/dscv/ri/32_1/drivers/platform/x86/mxm-wmi.c.common.c"
3613long s__builtin_expect(long val , long res ) 
3614{ 
3615
3616  {
3617#line 216
3618  return (val);
3619}
3620}