Showing error 1257

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--tty--serial--uartlite.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 6721
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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