Showing error 1074

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


Source:

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