Showing error 757

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