Showing error 1165

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