Showing error 846

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--input--misc--atlas_btns.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 4298
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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