Showing error 240

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