Showing error 669

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


Source:

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