Showing error 274

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--input--serio--ct82c710.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 2524
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 20 "include/asm-generic/int-ll64.h"
   5typedef unsigned char __u8;
   6#line 23 "include/asm-generic/int-ll64.h"
   7typedef unsigned short __u16;
   8#line 26 "include/asm-generic/int-ll64.h"
   9typedef unsigned int __u32;
  10#line 30 "include/asm-generic/int-ll64.h"
  11typedef unsigned long long __u64;
  12#line 43 "include/asm-generic/int-ll64.h"
  13typedef unsigned char u8;
  14#line 45 "include/asm-generic/int-ll64.h"
  15typedef short s16;
  16#line 46 "include/asm-generic/int-ll64.h"
  17typedef unsigned short u16;
  18#line 49 "include/asm-generic/int-ll64.h"
  19typedef unsigned int u32;
  20#line 51 "include/asm-generic/int-ll64.h"
  21typedef long long s64;
  22#line 52 "include/asm-generic/int-ll64.h"
  23typedef unsigned long long u64;
  24#line 14 "include/asm-generic/posix_types.h"
  25typedef long __kernel_long_t;
  26#line 15 "include/asm-generic/posix_types.h"
  27typedef unsigned long __kernel_ulong_t;
  28#line 75 "include/asm-generic/posix_types.h"
  29typedef __kernel_ulong_t __kernel_size_t;
  30#line 76 "include/asm-generic/posix_types.h"
  31typedef __kernel_long_t __kernel_ssize_t;
  32#line 91 "include/asm-generic/posix_types.h"
  33typedef long long __kernel_loff_t;
  34#line 21 "include/linux/types.h"
  35typedef __u32 __kernel_dev_t;
  36#line 24 "include/linux/types.h"
  37typedef __kernel_dev_t dev_t;
  38#line 27 "include/linux/types.h"
  39typedef unsigned short umode_t;
  40#line 38 "include/linux/types.h"
  41typedef _Bool bool;
  42#line 54 "include/linux/types.h"
  43typedef __kernel_loff_t loff_t;
  44#line 63 "include/linux/types.h"
  45typedef __kernel_size_t size_t;
  46#line 68 "include/linux/types.h"
  47typedef __kernel_ssize_t ssize_t;
  48#line 202 "include/linux/types.h"
  49typedef unsigned int gfp_t;
  50#line 206 "include/linux/types.h"
  51typedef u64 phys_addr_t;
  52#line 211 "include/linux/types.h"
  53typedef phys_addr_t resource_size_t;
  54#line 219 "include/linux/types.h"
  55struct __anonstruct_atomic_t_7 {
  56   int counter ;
  57};
  58#line 219 "include/linux/types.h"
  59typedef struct __anonstruct_atomic_t_7 atomic_t;
  60#line 224 "include/linux/types.h"
  61struct __anonstruct_atomic64_t_8 {
  62   long counter ;
  63};
  64#line 224 "include/linux/types.h"
  65typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  66#line 229 "include/linux/types.h"
  67struct list_head {
  68   struct list_head *next ;
  69   struct list_head *prev ;
  70};
  71#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  72struct module;
  73#line 56
  74struct module;
  75#line 146 "include/linux/init.h"
  76typedef void (*ctor_fn_t)(void);
  77#line 47 "include/linux/dynamic_debug.h"
  78struct device;
  79#line 47
  80struct device;
  81#line 135 "include/linux/kernel.h"
  82struct completion;
  83#line 135
  84struct completion;
  85#line 136
  86struct pt_regs;
  87#line 136
  88struct pt_regs;
  89#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
  90struct page;
  91#line 18
  92struct page;
  93#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
  94struct task_struct;
  95#line 20
  96struct task_struct;
  97#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  98struct task_struct;
  99#line 99 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 100struct pt_regs {
 101   unsigned long r15 ;
 102   unsigned long r14 ;
 103   unsigned long r13 ;
 104   unsigned long r12 ;
 105   unsigned long bp ;
 106   unsigned long bx ;
 107   unsigned long r11 ;
 108   unsigned long r10 ;
 109   unsigned long r9 ;
 110   unsigned long r8 ;
 111   unsigned long ax ;
 112   unsigned long cx ;
 113   unsigned long dx ;
 114   unsigned long si ;
 115   unsigned long di ;
 116   unsigned long orig_ax ;
 117   unsigned long ip ;
 118   unsigned long cs ;
 119   unsigned long flags ;
 120   unsigned long sp ;
 121   unsigned long ss ;
 122};
 123#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 124struct __anonstruct____missing_field_name_15 {
 125   unsigned int a ;
 126   unsigned int b ;
 127};
 128#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 129struct __anonstruct____missing_field_name_16 {
 130   u16 limit0 ;
 131   u16 base0 ;
 132   unsigned int base1 : 8 ;
 133   unsigned int type : 4 ;
 134   unsigned int s : 1 ;
 135   unsigned int dpl : 2 ;
 136   unsigned int p : 1 ;
 137   unsigned int limit : 4 ;
 138   unsigned int avl : 1 ;
 139   unsigned int l : 1 ;
 140   unsigned int d : 1 ;
 141   unsigned int g : 1 ;
 142   unsigned int base2 : 8 ;
 143};
 144#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 145union __anonunion____missing_field_name_14 {
 146   struct __anonstruct____missing_field_name_15 __annonCompField5 ;
 147   struct __anonstruct____missing_field_name_16 __annonCompField6 ;
 148};
 149#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 150struct desc_struct {
 151   union __anonunion____missing_field_name_14 __annonCompField7 ;
 152} __attribute__((__packed__)) ;
 153#line 51 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 154struct gate_struct64 {
 155   u16 offset_low ;
 156   u16 segment ;
 157   unsigned int ist : 3 ;
 158   unsigned int zero0 : 5 ;
 159   unsigned int type : 5 ;
 160   unsigned int dpl : 2 ;
 161   unsigned int p : 1 ;
 162   u16 offset_middle ;
 163   u32 offset_high ;
 164   u32 zero1 ;
 165} __attribute__((__packed__)) ;
 166#line 81 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 167typedef struct gate_struct64 gate_desc;
 168#line 94 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 169struct desc_ptr {
 170   unsigned short size ;
 171   unsigned long address ;
 172} __attribute__((__packed__)) ;
 173#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 174struct file;
 175#line 295
 176struct file;
 177#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 178struct page;
 179#line 47
 180struct thread_struct;
 181#line 47
 182struct thread_struct;
 183#line 48
 184struct desc_ptr;
 185#line 49
 186struct tss_struct;
 187#line 49
 188struct tss_struct;
 189#line 51
 190struct desc_struct;
 191#line 52
 192struct task_struct;
 193#line 102 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 194struct pv_cpu_ops {
 195   unsigned long (*get_debugreg)(int regno ) ;
 196   void (*set_debugreg)(int regno , unsigned long value ) ;
 197   void (*clts)(void) ;
 198   unsigned long (*read_cr0)(void) ;
 199   void (*write_cr0)(unsigned long  ) ;
 200   unsigned long (*read_cr4_safe)(void) ;
 201   unsigned long (*read_cr4)(void) ;
 202   void (*write_cr4)(unsigned long  ) ;
 203   unsigned long (*read_cr8)(void) ;
 204   void (*write_cr8)(unsigned long  ) ;
 205   void (*load_tr_desc)(void) ;
 206   void (*load_gdt)(struct desc_ptr  const  * ) ;
 207   void (*load_idt)(struct desc_ptr  const  * ) ;
 208   void (*store_gdt)(struct desc_ptr * ) ;
 209   void (*store_idt)(struct desc_ptr * ) ;
 210   void (*set_ldt)(void const   *desc , unsigned int entries ) ;
 211   unsigned long (*store_tr)(void) ;
 212   void (*load_tls)(struct thread_struct *t , unsigned int cpu ) ;
 213   void (*load_gs_index)(unsigned int idx ) ;
 214   void (*write_ldt_entry)(struct desc_struct *ldt , int entrynum , void const   *desc ) ;
 215   void (*write_gdt_entry)(struct desc_struct * , int entrynum , void const   *desc ,
 216                           int size ) ;
 217   void (*write_idt_entry)(gate_desc * , int entrynum , gate_desc const   *gate ) ;
 218   void (*alloc_ldt)(struct desc_struct *ldt , unsigned int entries ) ;
 219   void (*free_ldt)(struct desc_struct *ldt , unsigned int entries ) ;
 220   void (*load_sp0)(struct tss_struct *tss , struct thread_struct *t ) ;
 221   void (*set_iopl_mask)(unsigned int mask ) ;
 222   void (*wbinvd)(void) ;
 223   void (*io_delay)(void) ;
 224   void (*cpuid)(unsigned int *eax , unsigned int *ebx , unsigned int *ecx , unsigned int *edx ) ;
 225   u64 (*read_msr)(unsigned int msr , int *err ) ;
 226   int (*rdmsr_regs)(u32 *regs ) ;
 227   int (*write_msr)(unsigned int msr , unsigned int low , unsigned int high ) ;
 228   int (*wrmsr_regs)(u32 *regs ) ;
 229   u64 (*read_tsc)(void) ;
 230   u64 (*read_pmc)(int counter ) ;
 231   unsigned long long (*read_tscp)(unsigned int *aux ) ;
 232   void (*irq_enable_sysexit)(void) ;
 233   void (*usergs_sysret64)(void) ;
 234   void (*usergs_sysret32)(void) ;
 235   void (*iret)(void) ;
 236   void (*swapgs)(void) ;
 237   void (*start_context_switch)(struct task_struct *prev ) ;
 238   void (*end_context_switch)(struct task_struct *next ) ;
 239};
 240#line 329
 241struct arch_spinlock;
 242#line 329
 243struct arch_spinlock;
 244#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 245struct task_struct;
 246#line 141 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
 247struct kernel_vm86_regs {
 248   struct pt_regs pt ;
 249   unsigned short es ;
 250   unsigned short __esh ;
 251   unsigned short ds ;
 252   unsigned short __dsh ;
 253   unsigned short fs ;
 254   unsigned short __fsh ;
 255   unsigned short gs ;
 256   unsigned short __gsh ;
 257};
 258#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 259union __anonunion____missing_field_name_24 {
 260   struct pt_regs *regs ;
 261   struct kernel_vm86_regs *vm86 ;
 262};
 263#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 264struct math_emu_info {
 265   long ___orig_eip ;
 266   union __anonunion____missing_field_name_24 __annonCompField8 ;
 267};
 268#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 269struct task_struct;
 270#line 10 "include/asm-generic/bug.h"
 271struct bug_entry {
 272   int bug_addr_disp ;
 273   int file_disp ;
 274   unsigned short line ;
 275   unsigned short flags ;
 276};
 277#line 12 "include/linux/bug.h"
 278struct pt_regs;
 279#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 280struct static_key;
 281#line 234
 282struct static_key;
 283#line 11 "include/linux/personality.h"
 284struct pt_regs;
 285#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 286struct x86_hw_tss {
 287   u32 reserved1 ;
 288   u64 sp0 ;
 289   u64 sp1 ;
 290   u64 sp2 ;
 291   u64 reserved2 ;
 292   u64 ist[7] ;
 293   u32 reserved3 ;
 294   u32 reserved4 ;
 295   u16 reserved5 ;
 296   u16 io_bitmap_base ;
 297} __attribute__((__packed__, __aligned__((1) <<  (6) ))) ;
 298#line 258 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 299struct tss_struct {
 300   struct x86_hw_tss x86_tss ;
 301   unsigned long io_bitmap[8192UL / sizeof(long ) + 1UL] ;
 302   unsigned long stack[64] ;
 303} __attribute__((__aligned__((1) <<  (6) ))) ;
 304#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 305struct i387_fsave_struct {
 306   u32 cwd ;
 307   u32 swd ;
 308   u32 twd ;
 309   u32 fip ;
 310   u32 fcs ;
 311   u32 foo ;
 312   u32 fos ;
 313   u32 st_space[20] ;
 314   u32 status ;
 315};
 316#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 317struct __anonstruct____missing_field_name_31 {
 318   u64 rip ;
 319   u64 rdp ;
 320};
 321#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 322struct __anonstruct____missing_field_name_32 {
 323   u32 fip ;
 324   u32 fcs ;
 325   u32 foo ;
 326   u32 fos ;
 327};
 328#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 329union __anonunion____missing_field_name_30 {
 330   struct __anonstruct____missing_field_name_31 __annonCompField12 ;
 331   struct __anonstruct____missing_field_name_32 __annonCompField13 ;
 332};
 333#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 334union __anonunion____missing_field_name_33 {
 335   u32 padding1[12] ;
 336   u32 sw_reserved[12] ;
 337};
 338#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 339struct i387_fxsave_struct {
 340   u16 cwd ;
 341   u16 swd ;
 342   u16 twd ;
 343   u16 fop ;
 344   union __anonunion____missing_field_name_30 __annonCompField14 ;
 345   u32 mxcsr ;
 346   u32 mxcsr_mask ;
 347   u32 st_space[32] ;
 348   u32 xmm_space[64] ;
 349   u32 padding[12] ;
 350   union __anonunion____missing_field_name_33 __annonCompField15 ;
 351} __attribute__((__aligned__(16))) ;
 352#line 341 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 353struct i387_soft_struct {
 354   u32 cwd ;
 355   u32 swd ;
 356   u32 twd ;
 357   u32 fip ;
 358   u32 fcs ;
 359   u32 foo ;
 360   u32 fos ;
 361   u32 st_space[20] ;
 362   u8 ftop ;
 363   u8 changed ;
 364   u8 lookahead ;
 365   u8 no_update ;
 366   u8 rm ;
 367   u8 alimit ;
 368   struct math_emu_info *info ;
 369   u32 entry_eip ;
 370};
 371#line 361 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 372struct ymmh_struct {
 373   u32 ymmh_space[64] ;
 374};
 375#line 366 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 376struct xsave_hdr_struct {
 377   u64 xstate_bv ;
 378   u64 reserved1[2] ;
 379   u64 reserved2[5] ;
 380} __attribute__((__packed__)) ;
 381#line 372 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 382struct xsave_struct {
 383   struct i387_fxsave_struct i387 ;
 384   struct xsave_hdr_struct xsave_hdr ;
 385   struct ymmh_struct ymmh ;
 386} __attribute__((__packed__, __aligned__(64))) ;
 387#line 379 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 388union thread_xstate {
 389   struct i387_fsave_struct fsave ;
 390   struct i387_fxsave_struct fxsave ;
 391   struct i387_soft_struct soft ;
 392   struct xsave_struct xsave ;
 393};
 394#line 386 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 395struct fpu {
 396   unsigned int last_cpu ;
 397   unsigned int has_fpu ;
 398   union thread_xstate *state ;
 399};
 400#line 433
 401struct kmem_cache;
 402#line 435
 403struct perf_event;
 404#line 435
 405struct perf_event;
 406#line 437 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 407struct thread_struct {
 408   struct desc_struct tls_array[3] ;
 409   unsigned long sp0 ;
 410   unsigned long sp ;
 411   unsigned long usersp ;
 412   unsigned short es ;
 413   unsigned short ds ;
 414   unsigned short fsindex ;
 415   unsigned short gsindex ;
 416   unsigned long fs ;
 417   unsigned long gs ;
 418   struct perf_event *ptrace_bps[4] ;
 419   unsigned long debugreg6 ;
 420   unsigned long ptrace_dr7 ;
 421   unsigned long cr2 ;
 422   unsigned long trap_nr ;
 423   unsigned long error_code ;
 424   struct fpu fpu ;
 425   unsigned long *io_bitmap_ptr ;
 426   unsigned long iopl ;
 427   unsigned int io_bitmap_max ;
 428};
 429#line 23 "include/asm-generic/atomic-long.h"
 430typedef atomic64_t atomic_long_t;
 431#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 432typedef u16 __ticket_t;
 433#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 434typedef u32 __ticketpair_t;
 435#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 436struct __raw_tickets {
 437   __ticket_t head ;
 438   __ticket_t tail ;
 439};
 440#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 441union __anonunion____missing_field_name_36 {
 442   __ticketpair_t head_tail ;
 443   struct __raw_tickets tickets ;
 444};
 445#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 446struct arch_spinlock {
 447   union __anonunion____missing_field_name_36 __annonCompField17 ;
 448};
 449#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 450typedef struct arch_spinlock arch_spinlock_t;
 451#line 12 "include/linux/lockdep.h"
 452struct task_struct;
 453#line 20 "include/linux/spinlock_types.h"
 454struct raw_spinlock {
 455   arch_spinlock_t raw_lock ;
 456   unsigned int magic ;
 457   unsigned int owner_cpu ;
 458   void *owner ;
 459};
 460#line 64 "include/linux/spinlock_types.h"
 461union __anonunion____missing_field_name_39 {
 462   struct raw_spinlock rlock ;
 463};
 464#line 64 "include/linux/spinlock_types.h"
 465struct spinlock {
 466   union __anonunion____missing_field_name_39 __annonCompField19 ;
 467};
 468#line 64 "include/linux/spinlock_types.h"
 469typedef struct spinlock spinlock_t;
 470#line 49 "include/linux/wait.h"
 471struct __wait_queue_head {
 472   spinlock_t lock ;
 473   struct list_head task_list ;
 474};
 475#line 53 "include/linux/wait.h"
 476typedef struct __wait_queue_head wait_queue_head_t;
 477#line 55
 478struct task_struct;
 479#line 60 "include/linux/pageblock-flags.h"
 480struct page;
 481#line 48 "include/linux/mutex.h"
 482struct mutex {
 483   atomic_t count ;
 484   spinlock_t wait_lock ;
 485   struct list_head wait_list ;
 486   struct task_struct *owner ;
 487   char const   *name ;
 488   void *magic ;
 489};
 490#line 25 "include/linux/completion.h"
 491struct completion {
 492   unsigned int done ;
 493   wait_queue_head_t wait ;
 494};
 495#line 9 "include/linux/memory_hotplug.h"
 496struct page;
 497#line 18 "include/linux/ioport.h"
 498struct resource {
 499   resource_size_t start ;
 500   resource_size_t end ;
 501   char const   *name ;
 502   unsigned long flags ;
 503   struct resource *parent ;
 504   struct resource *sibling ;
 505   struct resource *child ;
 506};
 507#line 202
 508struct device;
 509#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 510struct device;
 511#line 46 "include/linux/ktime.h"
 512union ktime {
 513   s64 tv64 ;
 514};
 515#line 59 "include/linux/ktime.h"
 516typedef union ktime ktime_t;
 517#line 10 "include/linux/timer.h"
 518struct tvec_base;
 519#line 10
 520struct tvec_base;
 521#line 12 "include/linux/timer.h"
 522struct timer_list {
 523   struct list_head entry ;
 524   unsigned long expires ;
 525   struct tvec_base *base ;
 526   void (*function)(unsigned long  ) ;
 527   unsigned long data ;
 528   int slack ;
 529   int start_pid ;
 530   void *start_site ;
 531   char start_comm[16] ;
 532};
 533#line 17 "include/linux/workqueue.h"
 534struct work_struct;
 535#line 17
 536struct work_struct;
 537#line 79 "include/linux/workqueue.h"
 538struct work_struct {
 539   atomic_long_t data ;
 540   struct list_head entry ;
 541   void (*func)(struct work_struct *work ) ;
 542};
 543#line 42 "include/linux/pm.h"
 544struct device;
 545#line 50 "include/linux/pm.h"
 546struct pm_message {
 547   int event ;
 548};
 549#line 50 "include/linux/pm.h"
 550typedef struct pm_message pm_message_t;
 551#line 264 "include/linux/pm.h"
 552struct dev_pm_ops {
 553   int (*prepare)(struct device *dev ) ;
 554   void (*complete)(struct device *dev ) ;
 555   int (*suspend)(struct device *dev ) ;
 556   int (*resume)(struct device *dev ) ;
 557   int (*freeze)(struct device *dev ) ;
 558   int (*thaw)(struct device *dev ) ;
 559   int (*poweroff)(struct device *dev ) ;
 560   int (*restore)(struct device *dev ) ;
 561   int (*suspend_late)(struct device *dev ) ;
 562   int (*resume_early)(struct device *dev ) ;
 563   int (*freeze_late)(struct device *dev ) ;
 564   int (*thaw_early)(struct device *dev ) ;
 565   int (*poweroff_late)(struct device *dev ) ;
 566   int (*restore_early)(struct device *dev ) ;
 567   int (*suspend_noirq)(struct device *dev ) ;
 568   int (*resume_noirq)(struct device *dev ) ;
 569   int (*freeze_noirq)(struct device *dev ) ;
 570   int (*thaw_noirq)(struct device *dev ) ;
 571   int (*poweroff_noirq)(struct device *dev ) ;
 572   int (*restore_noirq)(struct device *dev ) ;
 573   int (*runtime_suspend)(struct device *dev ) ;
 574   int (*runtime_resume)(struct device *dev ) ;
 575   int (*runtime_idle)(struct device *dev ) ;
 576};
 577#line 458
 578enum rpm_status {
 579    RPM_ACTIVE = 0,
 580    RPM_RESUMING = 1,
 581    RPM_SUSPENDED = 2,
 582    RPM_SUSPENDING = 3
 583} ;
 584#line 480
 585enum rpm_request {
 586    RPM_REQ_NONE = 0,
 587    RPM_REQ_IDLE = 1,
 588    RPM_REQ_SUSPEND = 2,
 589    RPM_REQ_AUTOSUSPEND = 3,
 590    RPM_REQ_RESUME = 4
 591} ;
 592#line 488
 593struct wakeup_source;
 594#line 488
 595struct wakeup_source;
 596#line 495 "include/linux/pm.h"
 597struct pm_subsys_data {
 598   spinlock_t lock ;
 599   unsigned int refcount ;
 600};
 601#line 506
 602struct dev_pm_qos_request;
 603#line 506
 604struct pm_qos_constraints;
 605#line 506 "include/linux/pm.h"
 606struct dev_pm_info {
 607   pm_message_t power_state ;
 608   unsigned int can_wakeup : 1 ;
 609   unsigned int async_suspend : 1 ;
 610   bool is_prepared : 1 ;
 611   bool is_suspended : 1 ;
 612   bool ignore_children : 1 ;
 613   spinlock_t lock ;
 614   struct list_head entry ;
 615   struct completion completion ;
 616   struct wakeup_source *wakeup ;
 617   bool wakeup_path : 1 ;
 618   struct timer_list suspend_timer ;
 619   unsigned long timer_expires ;
 620   struct work_struct work ;
 621   wait_queue_head_t wait_queue ;
 622   atomic_t usage_count ;
 623   atomic_t child_count ;
 624   unsigned int disable_depth : 3 ;
 625   unsigned int idle_notification : 1 ;
 626   unsigned int request_pending : 1 ;
 627   unsigned int deferred_resume : 1 ;
 628   unsigned int run_wake : 1 ;
 629   unsigned int runtime_auto : 1 ;
 630   unsigned int no_callbacks : 1 ;
 631   unsigned int irq_safe : 1 ;
 632   unsigned int use_autosuspend : 1 ;
 633   unsigned int timer_autosuspends : 1 ;
 634   enum rpm_request request ;
 635   enum rpm_status runtime_status ;
 636   int runtime_error ;
 637   int autosuspend_delay ;
 638   unsigned long last_busy ;
 639   unsigned long active_jiffies ;
 640   unsigned long suspended_jiffies ;
 641   unsigned long accounting_timestamp ;
 642   ktime_t suspend_time ;
 643   s64 max_time_suspended_ns ;
 644   struct dev_pm_qos_request *pq_req ;
 645   struct pm_subsys_data *subsys_data ;
 646   struct pm_qos_constraints *constraints ;
 647};
 648#line 564 "include/linux/pm.h"
 649struct dev_pm_domain {
 650   struct dev_pm_ops ops ;
 651};
 652#line 8 "include/linux/vmalloc.h"
 653struct vm_area_struct;
 654#line 8
 655struct vm_area_struct;
 656#line 994 "include/linux/mmzone.h"
 657struct page;
 658#line 10 "include/linux/gfp.h"
 659struct vm_area_struct;
 660#line 29 "include/linux/sysctl.h"
 661struct completion;
 662#line 49 "include/linux/kmod.h"
 663struct file;
 664#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 665struct task_struct;
 666#line 18 "include/linux/elf.h"
 667typedef __u64 Elf64_Addr;
 668#line 19 "include/linux/elf.h"
 669typedef __u16 Elf64_Half;
 670#line 23 "include/linux/elf.h"
 671typedef __u32 Elf64_Word;
 672#line 24 "include/linux/elf.h"
 673typedef __u64 Elf64_Xword;
 674#line 194 "include/linux/elf.h"
 675struct elf64_sym {
 676   Elf64_Word st_name ;
 677   unsigned char st_info ;
 678   unsigned char st_other ;
 679   Elf64_Half st_shndx ;
 680   Elf64_Addr st_value ;
 681   Elf64_Xword st_size ;
 682};
 683#line 194 "include/linux/elf.h"
 684typedef struct elf64_sym Elf64_Sym;
 685#line 438
 686struct file;
 687#line 20 "include/linux/kobject_ns.h"
 688struct sock;
 689#line 20
 690struct sock;
 691#line 21
 692struct kobject;
 693#line 21
 694struct kobject;
 695#line 27
 696enum kobj_ns_type {
 697    KOBJ_NS_TYPE_NONE = 0,
 698    KOBJ_NS_TYPE_NET = 1,
 699    KOBJ_NS_TYPES = 2
 700} ;
 701#line 40 "include/linux/kobject_ns.h"
 702struct kobj_ns_type_operations {
 703   enum kobj_ns_type type ;
 704   void *(*grab_current_ns)(void) ;
 705   void const   *(*netlink_ns)(struct sock *sk ) ;
 706   void const   *(*initial_ns)(void) ;
 707   void (*drop_ns)(void * ) ;
 708};
 709#line 22 "include/linux/sysfs.h"
 710struct kobject;
 711#line 23
 712struct module;
 713#line 24
 714enum kobj_ns_type;
 715#line 26 "include/linux/sysfs.h"
 716struct attribute {
 717   char const   *name ;
 718   umode_t mode ;
 719};
 720#line 56 "include/linux/sysfs.h"
 721struct attribute_group {
 722   char const   *name ;
 723   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 724   struct attribute **attrs ;
 725};
 726#line 85
 727struct file;
 728#line 86
 729struct vm_area_struct;
 730#line 88 "include/linux/sysfs.h"
 731struct bin_attribute {
 732   struct attribute attr ;
 733   size_t size ;
 734   void *private ;
 735   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 736                   loff_t  , size_t  ) ;
 737   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 738                    loff_t  , size_t  ) ;
 739   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 740};
 741#line 112 "include/linux/sysfs.h"
 742struct sysfs_ops {
 743   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 744   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 745   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 746};
 747#line 118
 748struct sysfs_dirent;
 749#line 118
 750struct sysfs_dirent;
 751#line 22 "include/linux/kref.h"
 752struct kref {
 753   atomic_t refcount ;
 754};
 755#line 60 "include/linux/kobject.h"
 756struct kset;
 757#line 60
 758struct kobj_type;
 759#line 60 "include/linux/kobject.h"
 760struct kobject {
 761   char const   *name ;
 762   struct list_head entry ;
 763   struct kobject *parent ;
 764   struct kset *kset ;
 765   struct kobj_type *ktype ;
 766   struct sysfs_dirent *sd ;
 767   struct kref kref ;
 768   unsigned int state_initialized : 1 ;
 769   unsigned int state_in_sysfs : 1 ;
 770   unsigned int state_add_uevent_sent : 1 ;
 771   unsigned int state_remove_uevent_sent : 1 ;
 772   unsigned int uevent_suppress : 1 ;
 773};
 774#line 108 "include/linux/kobject.h"
 775struct kobj_type {
 776   void (*release)(struct kobject *kobj ) ;
 777   struct sysfs_ops  const  *sysfs_ops ;
 778   struct attribute **default_attrs ;
 779   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 780   void const   *(*namespace)(struct kobject *kobj ) ;
 781};
 782#line 116 "include/linux/kobject.h"
 783struct kobj_uevent_env {
 784   char *envp[32] ;
 785   int envp_idx ;
 786   char buf[2048] ;
 787   int buflen ;
 788};
 789#line 123 "include/linux/kobject.h"
 790struct kset_uevent_ops {
 791   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 792   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 793   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 794};
 795#line 140
 796struct sock;
 797#line 159 "include/linux/kobject.h"
 798struct kset {
 799   struct list_head list ;
 800   spinlock_t list_lock ;
 801   struct kobject kobj ;
 802   struct kset_uevent_ops  const  *uevent_ops ;
 803};
 804#line 39 "include/linux/moduleparam.h"
 805struct kernel_param;
 806#line 39
 807struct kernel_param;
 808#line 41 "include/linux/moduleparam.h"
 809struct kernel_param_ops {
 810   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
 811   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
 812   void (*free)(void *arg ) ;
 813};
 814#line 50
 815struct kparam_string;
 816#line 50
 817struct kparam_array;
 818#line 50 "include/linux/moduleparam.h"
 819union __anonunion____missing_field_name_199 {
 820   void *arg ;
 821   struct kparam_string  const  *str ;
 822   struct kparam_array  const  *arr ;
 823};
 824#line 50 "include/linux/moduleparam.h"
 825struct kernel_param {
 826   char const   *name ;
 827   struct kernel_param_ops  const  *ops ;
 828   u16 perm ;
 829   s16 level ;
 830   union __anonunion____missing_field_name_199 __annonCompField32 ;
 831};
 832#line 63 "include/linux/moduleparam.h"
 833struct kparam_string {
 834   unsigned int maxlen ;
 835   char *string ;
 836};
 837#line 69 "include/linux/moduleparam.h"
 838struct kparam_array {
 839   unsigned int max ;
 840   unsigned int elemsize ;
 841   unsigned int *num ;
 842   struct kernel_param_ops  const  *ops ;
 843   void *elem ;
 844};
 845#line 445
 846struct module;
 847#line 80 "include/linux/jump_label.h"
 848struct module;
 849#line 143 "include/linux/jump_label.h"
 850struct static_key {
 851   atomic_t enabled ;
 852};
 853#line 22 "include/linux/tracepoint.h"
 854struct module;
 855#line 23
 856struct tracepoint;
 857#line 23
 858struct tracepoint;
 859#line 25 "include/linux/tracepoint.h"
 860struct tracepoint_func {
 861   void *func ;
 862   void *data ;
 863};
 864#line 30 "include/linux/tracepoint.h"
 865struct tracepoint {
 866   char const   *name ;
 867   struct static_key key ;
 868   void (*regfunc)(void) ;
 869   void (*unregfunc)(void) ;
 870   struct tracepoint_func *funcs ;
 871};
 872#line 19 "include/linux/export.h"
 873struct kernel_symbol {
 874   unsigned long value ;
 875   char const   *name ;
 876};
 877#line 8 "include/asm-generic/module.h"
 878struct mod_arch_specific {
 879
 880};
 881#line 35 "include/linux/module.h"
 882struct module;
 883#line 37
 884struct module_param_attrs;
 885#line 37 "include/linux/module.h"
 886struct module_kobject {
 887   struct kobject kobj ;
 888   struct module *mod ;
 889   struct kobject *drivers_dir ;
 890   struct module_param_attrs *mp ;
 891};
 892#line 44 "include/linux/module.h"
 893struct module_attribute {
 894   struct attribute attr ;
 895   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 896   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 897                    size_t count ) ;
 898   void (*setup)(struct module * , char const   * ) ;
 899   int (*test)(struct module * ) ;
 900   void (*free)(struct module * ) ;
 901};
 902#line 71
 903struct exception_table_entry;
 904#line 71
 905struct exception_table_entry;
 906#line 199
 907enum module_state {
 908    MODULE_STATE_LIVE = 0,
 909    MODULE_STATE_COMING = 1,
 910    MODULE_STATE_GOING = 2
 911} ;
 912#line 215 "include/linux/module.h"
 913struct module_ref {
 914   unsigned long incs ;
 915   unsigned long decs ;
 916} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 917#line 220
 918struct module_sect_attrs;
 919#line 220
 920struct module_notes_attrs;
 921#line 220
 922struct ftrace_event_call;
 923#line 220 "include/linux/module.h"
 924struct module {
 925   enum module_state state ;
 926   struct list_head list ;
 927   char name[64UL - sizeof(unsigned long )] ;
 928   struct module_kobject mkobj ;
 929   struct module_attribute *modinfo_attrs ;
 930   char const   *version ;
 931   char const   *srcversion ;
 932   struct kobject *holders_dir ;
 933   struct kernel_symbol  const  *syms ;
 934   unsigned long const   *crcs ;
 935   unsigned int num_syms ;
 936   struct kernel_param *kp ;
 937   unsigned int num_kp ;
 938   unsigned int num_gpl_syms ;
 939   struct kernel_symbol  const  *gpl_syms ;
 940   unsigned long const   *gpl_crcs ;
 941   struct kernel_symbol  const  *unused_syms ;
 942   unsigned long const   *unused_crcs ;
 943   unsigned int num_unused_syms ;
 944   unsigned int num_unused_gpl_syms ;
 945   struct kernel_symbol  const  *unused_gpl_syms ;
 946   unsigned long const   *unused_gpl_crcs ;
 947   struct kernel_symbol  const  *gpl_future_syms ;
 948   unsigned long const   *gpl_future_crcs ;
 949   unsigned int num_gpl_future_syms ;
 950   unsigned int num_exentries ;
 951   struct exception_table_entry *extable ;
 952   int (*init)(void) ;
 953   void *module_init ;
 954   void *module_core ;
 955   unsigned int init_size ;
 956   unsigned int core_size ;
 957   unsigned int init_text_size ;
 958   unsigned int core_text_size ;
 959   unsigned int init_ro_size ;
 960   unsigned int core_ro_size ;
 961   struct mod_arch_specific arch ;
 962   unsigned int taints ;
 963   unsigned int num_bugs ;
 964   struct list_head bug_list ;
 965   struct bug_entry *bug_table ;
 966   Elf64_Sym *symtab ;
 967   Elf64_Sym *core_symtab ;
 968   unsigned int num_symtab ;
 969   unsigned int core_num_syms ;
 970   char *strtab ;
 971   char *core_strtab ;
 972   struct module_sect_attrs *sect_attrs ;
 973   struct module_notes_attrs *notes_attrs ;
 974   char *args ;
 975   void *percpu ;
 976   unsigned int percpu_size ;
 977   unsigned int num_tracepoints ;
 978   struct tracepoint * const  *tracepoints_ptrs ;
 979   unsigned int num_trace_bprintk_fmt ;
 980   char const   **trace_bprintk_fmt_start ;
 981   struct ftrace_event_call **trace_events ;
 982   unsigned int num_trace_events ;
 983   struct list_head source_list ;
 984   struct list_head target_list ;
 985   struct task_struct *waiter ;
 986   void (*exit)(void) ;
 987   struct module_ref *refptr ;
 988   ctor_fn_t *ctors ;
 989   unsigned int num_ctors ;
 990};
 991#line 10 "include/linux/irqreturn.h"
 992enum irqreturn {
 993    IRQ_NONE = 0,
 994    IRQ_HANDLED = 1,
 995    IRQ_WAKE_THREAD = 2
 996} ;
 997#line 16 "include/linux/irqreturn.h"
 998typedef enum irqreturn irqreturn_t;
 999#line 32 "include/linux/irq.h"
1000struct module;
1001#line 14 "include/linux/irqdesc.h"
1002struct module;
1003#line 17 "include/linux/profile.h"
1004struct pt_regs;
1005#line 65
1006struct task_struct;
1007#line 88
1008struct pt_regs;
1009#line 94 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess.h"
1010struct exception_table_entry {
1011   unsigned long insn ;
1012   unsigned long fixup ;
1013};
1014#line 132 "include/linux/hardirq.h"
1015struct task_struct;
1016#line 187 "include/linux/interrupt.h"
1017struct device;
1018#line 19 "include/linux/klist.h"
1019struct klist_node;
1020#line 19
1021struct klist_node;
1022#line 39 "include/linux/klist.h"
1023struct klist_node {
1024   void *n_klist ;
1025   struct list_head n_node ;
1026   struct kref n_ref ;
1027};
1028#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1029struct dma_map_ops;
1030#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1031struct dev_archdata {
1032   void *acpi_handle ;
1033   struct dma_map_ops *dma_ops ;
1034   void *iommu ;
1035};
1036#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1037struct pdev_archdata {
1038
1039};
1040#line 28 "include/linux/device.h"
1041struct device;
1042#line 29
1043struct device_private;
1044#line 29
1045struct device_private;
1046#line 30
1047struct device_driver;
1048#line 30
1049struct device_driver;
1050#line 31
1051struct driver_private;
1052#line 31
1053struct driver_private;
1054#line 32
1055struct module;
1056#line 33
1057struct class;
1058#line 33
1059struct class;
1060#line 34
1061struct subsys_private;
1062#line 34
1063struct subsys_private;
1064#line 35
1065struct bus_type;
1066#line 35
1067struct bus_type;
1068#line 36
1069struct device_node;
1070#line 36
1071struct device_node;
1072#line 37
1073struct iommu_ops;
1074#line 37
1075struct iommu_ops;
1076#line 39 "include/linux/device.h"
1077struct bus_attribute {
1078   struct attribute attr ;
1079   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
1080   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
1081};
1082#line 89
1083struct device_attribute;
1084#line 89
1085struct driver_attribute;
1086#line 89 "include/linux/device.h"
1087struct bus_type {
1088   char const   *name ;
1089   char const   *dev_name ;
1090   struct device *dev_root ;
1091   struct bus_attribute *bus_attrs ;
1092   struct device_attribute *dev_attrs ;
1093   struct driver_attribute *drv_attrs ;
1094   int (*match)(struct device *dev , struct device_driver *drv ) ;
1095   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1096   int (*probe)(struct device *dev ) ;
1097   int (*remove)(struct device *dev ) ;
1098   void (*shutdown)(struct device *dev ) ;
1099   int (*suspend)(struct device *dev , pm_message_t state ) ;
1100   int (*resume)(struct device *dev ) ;
1101   struct dev_pm_ops  const  *pm ;
1102   struct iommu_ops *iommu_ops ;
1103   struct subsys_private *p ;
1104};
1105#line 127
1106struct device_type;
1107#line 214
1108struct of_device_id;
1109#line 214 "include/linux/device.h"
1110struct device_driver {
1111   char const   *name ;
1112   struct bus_type *bus ;
1113   struct module *owner ;
1114   char const   *mod_name ;
1115   bool suppress_bind_attrs ;
1116   struct of_device_id  const  *of_match_table ;
1117   int (*probe)(struct device *dev ) ;
1118   int (*remove)(struct device *dev ) ;
1119   void (*shutdown)(struct device *dev ) ;
1120   int (*suspend)(struct device *dev , pm_message_t state ) ;
1121   int (*resume)(struct device *dev ) ;
1122   struct attribute_group  const  **groups ;
1123   struct dev_pm_ops  const  *pm ;
1124   struct driver_private *p ;
1125};
1126#line 249 "include/linux/device.h"
1127struct driver_attribute {
1128   struct attribute attr ;
1129   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
1130   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
1131};
1132#line 330
1133struct class_attribute;
1134#line 330 "include/linux/device.h"
1135struct class {
1136   char const   *name ;
1137   struct module *owner ;
1138   struct class_attribute *class_attrs ;
1139   struct device_attribute *dev_attrs ;
1140   struct bin_attribute *dev_bin_attrs ;
1141   struct kobject *dev_kobj ;
1142   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1143   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1144   void (*class_release)(struct class *class ) ;
1145   void (*dev_release)(struct device *dev ) ;
1146   int (*suspend)(struct device *dev , pm_message_t state ) ;
1147   int (*resume)(struct device *dev ) ;
1148   struct kobj_ns_type_operations  const  *ns_type ;
1149   void const   *(*namespace)(struct device *dev ) ;
1150   struct dev_pm_ops  const  *pm ;
1151   struct subsys_private *p ;
1152};
1153#line 397 "include/linux/device.h"
1154struct class_attribute {
1155   struct attribute attr ;
1156   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
1157   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
1158                    size_t count ) ;
1159   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
1160};
1161#line 465 "include/linux/device.h"
1162struct device_type {
1163   char const   *name ;
1164   struct attribute_group  const  **groups ;
1165   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1166   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1167   void (*release)(struct device *dev ) ;
1168   struct dev_pm_ops  const  *pm ;
1169};
1170#line 476 "include/linux/device.h"
1171struct device_attribute {
1172   struct attribute attr ;
1173   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
1174   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
1175                    size_t count ) ;
1176};
1177#line 559 "include/linux/device.h"
1178struct device_dma_parameters {
1179   unsigned int max_segment_size ;
1180   unsigned long segment_boundary_mask ;
1181};
1182#line 627
1183struct dma_coherent_mem;
1184#line 627 "include/linux/device.h"
1185struct device {
1186   struct device *parent ;
1187   struct device_private *p ;
1188   struct kobject kobj ;
1189   char const   *init_name ;
1190   struct device_type  const  *type ;
1191   struct mutex mutex ;
1192   struct bus_type *bus ;
1193   struct device_driver *driver ;
1194   void *platform_data ;
1195   struct dev_pm_info power ;
1196   struct dev_pm_domain *pm_domain ;
1197   int numa_node ;
1198   u64 *dma_mask ;
1199   u64 coherent_dma_mask ;
1200   struct device_dma_parameters *dma_parms ;
1201   struct list_head dma_pools ;
1202   struct dma_coherent_mem *dma_mem ;
1203   struct dev_archdata archdata ;
1204   struct device_node *of_node ;
1205   dev_t devt ;
1206   u32 id ;
1207   spinlock_t devres_lock ;
1208   struct list_head devres_head ;
1209   struct klist_node knode_class ;
1210   struct class *class ;
1211   struct attribute_group  const  **groups ;
1212   void (*release)(struct device *dev ) ;
1213};
1214#line 43 "include/linux/pm_wakeup.h"
1215struct wakeup_source {
1216   char const   *name ;
1217   struct list_head entry ;
1218   spinlock_t lock ;
1219   struct timer_list timer ;
1220   unsigned long timer_expires ;
1221   ktime_t total_time ;
1222   ktime_t max_time ;
1223   ktime_t last_time ;
1224   unsigned long event_count ;
1225   unsigned long active_count ;
1226   unsigned long relax_count ;
1227   unsigned long hit_count ;
1228   unsigned int active : 1 ;
1229};
1230#line 12 "include/linux/mod_devicetable.h"
1231typedef unsigned long kernel_ulong_t;
1232#line 209 "include/linux/mod_devicetable.h"
1233struct serio_device_id {
1234   __u8 type ;
1235   __u8 extra ;
1236   __u8 id ;
1237   __u8 proto ;
1238};
1239#line 219 "include/linux/mod_devicetable.h"
1240struct of_device_id {
1241   char name[32] ;
1242   char type[32] ;
1243   char compatible[128] ;
1244   void *data ;
1245};
1246#line 506 "include/linux/mod_devicetable.h"
1247struct platform_device_id {
1248   char name[20] ;
1249   kernel_ulong_t driver_data  __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
1250};
1251#line 26 "include/linux/serio.h"
1252struct serio_driver;
1253#line 26 "include/linux/serio.h"
1254struct serio {
1255   void *port_data ;
1256   char name[32] ;
1257   char phys[32] ;
1258   bool manual_bind ;
1259   struct serio_device_id id ;
1260   spinlock_t lock ;
1261   int (*write)(struct serio * , unsigned char  ) ;
1262   int (*open)(struct serio * ) ;
1263   void (*close)(struct serio * ) ;
1264   int (*start)(struct serio * ) ;
1265   void (*stop)(struct serio * ) ;
1266   struct serio *parent ;
1267   struct list_head child_node ;
1268   struct list_head children ;
1269   unsigned int depth ;
1270   struct serio_driver *drv ;
1271   struct mutex drv_mutex ;
1272   struct device dev ;
1273   struct list_head node ;
1274};
1275#line 58 "include/linux/serio.h"
1276struct serio_driver {
1277   char const   *description ;
1278   struct serio_device_id  const  *id_table ;
1279   bool manual_bind ;
1280   void (*write_wakeup)(struct serio * ) ;
1281   irqreturn_t (*interrupt)(struct serio * , unsigned char  , unsigned int  ) ;
1282   int (*connect)(struct serio * , struct serio_driver *drv ) ;
1283   int (*reconnect)(struct serio * ) ;
1284   void (*disconnect)(struct serio * ) ;
1285   void (*cleanup)(struct serio * ) ;
1286   struct device_driver driver ;
1287};
1288#line 17 "include/linux/platform_device.h"
1289struct mfd_cell;
1290#line 17
1291struct mfd_cell;
1292#line 19 "include/linux/platform_device.h"
1293struct platform_device {
1294   char const   *name ;
1295   int id ;
1296   struct device dev ;
1297   u32 num_resources ;
1298   struct resource *resource ;
1299   struct platform_device_id  const  *id_entry ;
1300   struct mfd_cell *mfd_cell ;
1301   struct pdev_archdata archdata ;
1302};
1303#line 164 "include/linux/platform_device.h"
1304struct platform_driver {
1305   int (*probe)(struct platform_device * ) ;
1306   int (*remove)(struct platform_device * ) ;
1307   void (*shutdown)(struct platform_device * ) ;
1308   int (*suspend)(struct platform_device * , pm_message_t state ) ;
1309   int (*resume)(struct platform_device * ) ;
1310   struct device_driver driver ;
1311   struct platform_device_id  const  *id_table ;
1312};
1313#line 46 "include/linux/slub_def.h"
1314struct kmem_cache_cpu {
1315   void **freelist ;
1316   unsigned long tid ;
1317   struct page *page ;
1318   struct page *partial ;
1319   int node ;
1320   unsigned int stat[26] ;
1321};
1322#line 57 "include/linux/slub_def.h"
1323struct kmem_cache_node {
1324   spinlock_t list_lock ;
1325   unsigned long nr_partial ;
1326   struct list_head partial ;
1327   atomic_long_t nr_slabs ;
1328   atomic_long_t total_objects ;
1329   struct list_head full ;
1330};
1331#line 73 "include/linux/slub_def.h"
1332struct kmem_cache_order_objects {
1333   unsigned long x ;
1334};
1335#line 80 "include/linux/slub_def.h"
1336struct kmem_cache {
1337   struct kmem_cache_cpu *cpu_slab ;
1338   unsigned long flags ;
1339   unsigned long min_partial ;
1340   int size ;
1341   int objsize ;
1342   int offset ;
1343   int cpu_partial ;
1344   struct kmem_cache_order_objects oo ;
1345   struct kmem_cache_order_objects max ;
1346   struct kmem_cache_order_objects min ;
1347   gfp_t allocflags ;
1348   int refcount ;
1349   void (*ctor)(void * ) ;
1350   int inuse ;
1351   int align ;
1352   int reserved ;
1353   char const   *name ;
1354   struct list_head list ;
1355   struct kobject kobj ;
1356   int remote_node_defrag_ratio ;
1357   struct kmem_cache_node *node[1 << 10] ;
1358};
1359#line 1 "<compiler builtins>"
1360long __builtin_expect(long val , long res ) ;
1361#line 100 "include/linux/printk.h"
1362extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
1363#line 322 "include/linux/kernel.h"
1364extern int ( /* format attribute */  snprintf)(char *buf , size_t size , char const   *fmt 
1365                                               , ...) ;
1366#line 10 "include/asm-generic/delay.h"
1367extern void __const_udelay(unsigned long xloops ) ;
1368#line 355 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
1369extern struct pv_cpu_ops pv_cpu_ops ;
1370#line 30 "include/linux/string.h"
1371extern size_t strlcpy(char * , char const   * , size_t  ) ;
1372#line 349 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
1373__inline static void slow_down_io(void)  __attribute__((__no_instrument_function__)) ;
1374#line 349 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
1375__inline static void slow_down_io(void) 
1376{ unsigned long __cil_tmp1 ;
1377  void (*__cil_tmp2)(void) ;
1378
1379  {
1380  {
1381#line 351
1382  __cil_tmp1 = (unsigned long )(& pv_cpu_ops) + 216;
1383#line 351
1384  __cil_tmp2 = *((void (**)(void))__cil_tmp1);
1385#line 351
1386  (*__cil_tmp2)();
1387  }
1388#line 357
1389  return;
1390}
1391}
1392#line 152 "include/linux/mutex.h"
1393void mutex_lock(struct mutex *lock ) ;
1394#line 153
1395int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
1396#line 154
1397int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
1398#line 168
1399int mutex_trylock(struct mutex *lock ) ;
1400#line 169
1401void mutex_unlock(struct mutex *lock ) ;
1402#line 170
1403int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
1404#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1405__inline static void outb(unsigned char value , int port )  __attribute__((__no_instrument_function__)) ;
1406#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1407__inline static void outb(unsigned char value , int port ) 
1408{ 
1409
1410  {
1411#line 308
1412  __asm__  volatile   ("out"
1413                       "b"
1414                       " %"
1415                       "b"
1416                       "0, %w1": : "a" (value), "Nd" (port));
1417#line 308
1418  return;
1419}
1420}
1421#line 308
1422__inline static unsigned char inb(int port )  __attribute__((__no_instrument_function__)) ;
1423#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1424__inline static unsigned char inb(int port ) 
1425{ unsigned char value ;
1426
1427  {
1428#line 308
1429  __asm__  volatile   ("in"
1430                       "b"
1431                       " %w1, %"
1432                       "b"
1433                       "0": "=a" (value): "Nd" (port));
1434#line 308
1435  return (value);
1436}
1437}
1438#line 308
1439__inline static void outb_p(unsigned char value , int port )  __attribute__((__no_instrument_function__)) ;
1440#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1441__inline static void outb_p(unsigned char value , int port ) 
1442{ 
1443
1444  {
1445  {
1446#line 308
1447  outb(value, port);
1448#line 308
1449  slow_down_io();
1450  }
1451#line 308
1452  return;
1453}
1454}
1455#line 308
1456__inline static unsigned char inb_p(int port )  __attribute__((__no_instrument_function__)) ;
1457#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1458__inline static unsigned char inb_p(int port ) 
1459{ unsigned char value ;
1460  unsigned char tmp ;
1461
1462  {
1463  {
1464#line 308
1465  tmp = inb(port);
1466#line 308
1467  value = tmp;
1468#line 308
1469  slow_down_io();
1470  }
1471#line 308
1472  return (value);
1473}
1474}
1475#line 26 "include/linux/export.h"
1476extern struct module __this_module ;
1477#line 67 "include/linux/module.h"
1478int init_module(void) ;
1479#line 68
1480void cleanup_module(void) ;
1481#line 126 "include/linux/interrupt.h"
1482extern int __attribute__((__warn_unused_result__))  request_threaded_irq(unsigned int irq ,
1483                                                                         irqreturn_t (*handler)(int  ,
1484                                                                                                void * ) ,
1485                                                                         irqreturn_t (*thread_fn)(int  ,
1486                                                                                                  void * ) ,
1487                                                                         unsigned long flags ,
1488                                                                         char const   *name ,
1489                                                                         void *dev ) ;
1490#line 131
1491__inline static int __attribute__((__warn_unused_result__))  request_irq(unsigned int irq ,
1492                                                                         irqreturn_t (*handler)(int  ,
1493                                                                                                void * ) ,
1494                                                                         unsigned long flags ,
1495                                                                         char const   *name ,
1496                                                                         void *dev )  __attribute__((__no_instrument_function__)) ;
1497#line 131 "include/linux/interrupt.h"
1498__inline static int __attribute__((__warn_unused_result__))  request_irq(unsigned int irq ,
1499                                                                         irqreturn_t (*handler)(int  ,
1500                                                                                                void * ) ,
1501                                                                         unsigned long flags ,
1502                                                                         char const   *name ,
1503                                                                         void *dev ) 
1504{ int tmp ;
1505  void *__cil_tmp7 ;
1506  irqreturn_t (*__cil_tmp8)(int  , void * ) ;
1507
1508  {
1509  {
1510#line 135
1511  __cil_tmp7 = (void *)0;
1512#line 135
1513  __cil_tmp8 = (irqreturn_t (*)(int  , void * ))__cil_tmp7;
1514#line 135
1515  tmp = (int )request_threaded_irq(irq, handler, __cil_tmp8, flags, name, dev);
1516  }
1517#line 135
1518  return (tmp);
1519}
1520}
1521#line 184
1522extern void free_irq(unsigned int  , void * ) ;
1523#line 79 "include/linux/serio.h"
1524extern irqreturn_t serio_interrupt(struct serio *serio , unsigned char data , unsigned int flags ) ;
1525#line 81
1526extern void __serio_register_port(struct serio *serio , struct module *owner ) ;
1527#line 87
1528extern void serio_unregister_port(struct serio *serio ) ;
1529#line 40 "include/linux/platform_device.h"
1530extern void platform_device_unregister(struct platform_device * ) ;
1531#line 155
1532extern struct platform_device *platform_device_alloc(char const   *name , int id ) ;
1533#line 156
1534extern int platform_device_add_resources(struct platform_device *pdev , struct resource  const  *res ,
1535                                         unsigned int num ) ;
1536#line 160
1537extern int platform_device_add(struct platform_device *pdev ) ;
1538#line 162
1539extern void platform_device_put(struct platform_device *pdev ) ;
1540#line 174
1541extern int platform_driver_register(struct platform_driver * ) ;
1542#line 175
1543extern void platform_driver_unregister(struct platform_driver * ) ;
1544#line 221 "include/linux/slub_def.h"
1545extern void *__kmalloc(size_t size , gfp_t flags ) ;
1546#line 268
1547__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
1548                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
1549#line 268 "include/linux/slub_def.h"
1550__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
1551                                                                    gfp_t flags ) 
1552{ void *tmp___2 ;
1553
1554  {
1555  {
1556#line 283
1557  tmp___2 = __kmalloc(size, flags);
1558  }
1559#line 283
1560  return (tmp___2);
1561}
1562}
1563#line 349 "include/linux/slab.h"
1564__inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
1565#line 349 "include/linux/slab.h"
1566__inline static void *kzalloc(size_t size , gfp_t flags ) 
1567{ void *tmp ;
1568  unsigned int __cil_tmp4 ;
1569
1570  {
1571  {
1572#line 351
1573  __cil_tmp4 = flags | 32768U;
1574#line 351
1575  tmp = kmalloc(size, __cil_tmp4);
1576  }
1577#line 351
1578  return (tmp);
1579}
1580}
1581#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1582static char const   __mod_author43[39]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1583__aligned__(1)))  = 
1584#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1585  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
1586        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'V', 
1587        (char const   )'o',      (char const   )'j',      (char const   )'t',      (char const   )'e', 
1588        (char const   )'c',      (char const   )'h',      (char const   )' ',      (char const   )'P', 
1589        (char const   )'a',      (char const   )'v',      (char const   )'l',      (char const   )'i', 
1590        (char const   )'k',      (char const   )' ',      (char const   )'<',      (char const   )'v', 
1591        (char const   )'o',      (char const   )'j',      (char const   )'t',      (char const   )'e', 
1592        (char const   )'c',      (char const   )'h',      (char const   )'@',      (char const   )'u', 
1593        (char const   )'c',      (char const   )'w',      (char const   )'.',      (char const   )'c', 
1594        (char const   )'z',      (char const   )'>',      (char const   )'\000'};
1595#line 44 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1596static char const   __mod_description44[46]  __attribute__((__used__, __unused__,
1597__section__(".modinfo"), __aligned__(1)))  = 
1598#line 44
1599  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
1600        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
1601        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
1602        (char const   )'8',      (char const   )'2',      (char const   )'C',      (char const   )'7', 
1603        (char const   )'1',      (char const   )'0',      (char const   )' ',      (char const   )'C', 
1604        (char const   )'&',      (char const   )'T',      (char const   )' ',      (char const   )'m', 
1605        (char const   )'o',      (char const   )'u',      (char const   )'s',      (char const   )'e', 
1606        (char const   )' ',      (char const   )'p',      (char const   )'o',      (char const   )'r', 
1607        (char const   )'t',      (char const   )' ',      (char const   )'c',      (char const   )'h', 
1608        (char const   )'i',      (char const   )'p',      (char const   )' ',      (char const   )'d', 
1609        (char const   )'r',      (char const   )'i',      (char const   )'v',      (char const   )'e', 
1610        (char const   )'r',      (char const   )'\000'};
1611#line 45 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1612static char const   __mod_license45[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1613__aligned__(1)))  = 
1614#line 45
1615  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
1616        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
1617        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
1618#line 65 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1619static struct serio *ct82c710_port  ;
1620#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1621static struct platform_device *ct82c710_device  ;
1622#line 67 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1623static struct resource ct82c710_iores  ;
1624#line 74 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1625static irqreturn_t ct82c710_interrupt(int cpl , void *dev_id ) 
1626{ unsigned char tmp ;
1627  irqreturn_t tmp___0 ;
1628  struct resource *__cil_tmp5 ;
1629  resource_size_t __cil_tmp6 ;
1630  int __cil_tmp7 ;
1631
1632  {
1633  {
1634#line 76
1635  __cil_tmp5 = & ct82c710_iores;
1636#line 76
1637  __cil_tmp6 = *((resource_size_t *)__cil_tmp5);
1638#line 76
1639  __cil_tmp7 = (int )__cil_tmp6;
1640#line 76
1641  tmp = inb(__cil_tmp7);
1642#line 76
1643  tmp___0 = serio_interrupt(ct82c710_port, tmp, 0U);
1644  }
1645#line 76
1646  return (tmp___0);
1647}
1648}
1649#line 83 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1650static int ct82c170_wait(void) 
1651{ int timeout ;
1652  unsigned char tmp ;
1653  unsigned char tmp___0 ;
1654  struct resource *__cil_tmp4 ;
1655  resource_size_t __cil_tmp5 ;
1656  resource_size_t __cil_tmp6 ;
1657  int __cil_tmp7 ;
1658  int __cil_tmp8 ;
1659  int __cil_tmp9 ;
1660  struct resource *__cil_tmp10 ;
1661  resource_size_t __cil_tmp11 ;
1662  resource_size_t __cil_tmp12 ;
1663  int __cil_tmp13 ;
1664  int __cil_tmp14 ;
1665  struct resource *__cil_tmp15 ;
1666  resource_size_t __cil_tmp16 ;
1667  int __cil_tmp17 ;
1668
1669  {
1670#line 85
1671  timeout = 60000;
1672  {
1673#line 87
1674  while (1) {
1675    while_continue: /* CIL Label */ ;
1676    {
1677#line 87
1678    __cil_tmp4 = & ct82c710_iores;
1679#line 87
1680    __cil_tmp5 = *((resource_size_t *)__cil_tmp4);
1681#line 87
1682    __cil_tmp6 = __cil_tmp5 + 1ULL;
1683#line 87
1684    __cil_tmp7 = (int )__cil_tmp6;
1685#line 87
1686    tmp___0 = inb(__cil_tmp7);
1687    }
1688    {
1689#line 87
1690    __cil_tmp8 = (int )tmp___0;
1691#line 87
1692    __cil_tmp9 = __cil_tmp8 & 7;
1693#line 87
1694    if (__cil_tmp9 != 5) {
1695#line 87
1696      if (timeout) {
1697
1698      } else {
1699#line 87
1700        goto while_break;
1701      }
1702    } else {
1703#line 87
1704      goto while_break;
1705    }
1706    }
1707    {
1708#line 90
1709    __cil_tmp10 = & ct82c710_iores;
1710#line 90
1711    __cil_tmp11 = *((resource_size_t *)__cil_tmp10);
1712#line 90
1713    __cil_tmp12 = __cil_tmp11 + 1ULL;
1714#line 90
1715    __cil_tmp13 = (int )__cil_tmp12;
1716#line 90
1717    tmp = inb_p(__cil_tmp13);
1718    }
1719    {
1720#line 90
1721    __cil_tmp14 = (int )tmp;
1722#line 90
1723    if (__cil_tmp14 & 2) {
1724      {
1725#line 90
1726      __cil_tmp15 = & ct82c710_iores;
1727#line 90
1728      __cil_tmp16 = *((resource_size_t *)__cil_tmp15);
1729#line 90
1730      __cil_tmp17 = (int )__cil_tmp16;
1731#line 90
1732      inb_p(__cil_tmp17);
1733      }
1734    } else {
1735
1736    }
1737    }
1738    {
1739#line 92
1740    __const_udelay(4295UL);
1741#line 93
1742    timeout = timeout - 1;
1743    }
1744  }
1745  while_break: /* CIL Label */ ;
1746  }
1747#line 96
1748  return (! timeout);
1749}
1750}
1751#line 99 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1752static void ct82c710_close(struct serio *serio ) 
1753{ int tmp ;
1754  unsigned char tmp___0 ;
1755  int tmp___1 ;
1756  struct resource *__cil_tmp5 ;
1757  resource_size_t __cil_tmp6 ;
1758  resource_size_t __cil_tmp7 ;
1759  int __cil_tmp8 ;
1760  int __cil_tmp9 ;
1761  int __cil_tmp10 ;
1762  unsigned char __cil_tmp11 ;
1763  struct resource *__cil_tmp12 ;
1764  resource_size_t __cil_tmp13 ;
1765  resource_size_t __cil_tmp14 ;
1766  int __cil_tmp15 ;
1767  void *__cil_tmp16 ;
1768
1769  {
1770  {
1771#line 101
1772  tmp = ct82c170_wait();
1773  }
1774#line 101
1775  if (tmp) {
1776    {
1777#line 102
1778    printk("<4>ct82c710.c: Device busy in close()\n");
1779    }
1780  } else {
1781
1782  }
1783  {
1784#line 104
1785  __cil_tmp5 = & ct82c710_iores;
1786#line 104
1787  __cil_tmp6 = *((resource_size_t *)__cil_tmp5);
1788#line 104
1789  __cil_tmp7 = __cil_tmp6 + 1ULL;
1790#line 104
1791  __cil_tmp8 = (int )__cil_tmp7;
1792#line 104
1793  tmp___0 = inb_p(__cil_tmp8);
1794#line 104
1795  __cil_tmp9 = (int )tmp___0;
1796#line 104
1797  __cil_tmp10 = __cil_tmp9 & -145;
1798#line 104
1799  __cil_tmp11 = (unsigned char )__cil_tmp10;
1800#line 104
1801  __cil_tmp12 = & ct82c710_iores;
1802#line 104
1803  __cil_tmp13 = *((resource_size_t *)__cil_tmp12);
1804#line 104
1805  __cil_tmp14 = __cil_tmp13 + 1ULL;
1806#line 104
1807  __cil_tmp15 = (int )__cil_tmp14;
1808#line 104
1809  outb_p(__cil_tmp11, __cil_tmp15);
1810#line 106
1811  tmp___1 = ct82c170_wait();
1812  }
1813#line 106
1814  if (tmp___1) {
1815    {
1816#line 107
1817    printk("<4>ct82c710.c: Device busy in close()\n");
1818    }
1819  } else {
1820
1821  }
1822  {
1823#line 109
1824  __cil_tmp16 = (void *)0;
1825#line 109
1826  free_irq(12U, __cil_tmp16);
1827  }
1828#line 110
1829  return;
1830}
1831}
1832#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1833static int ct82c710_open(struct serio *serio ) 
1834{ unsigned char status ;
1835  int err ;
1836  int tmp ;
1837  void *__cil_tmp5 ;
1838  struct resource *__cil_tmp6 ;
1839  resource_size_t __cil_tmp7 ;
1840  resource_size_t __cil_tmp8 ;
1841  int __cil_tmp9 ;
1842  int __cil_tmp10 ;
1843  int __cil_tmp11 ;
1844  struct resource *__cil_tmp12 ;
1845  resource_size_t __cil_tmp13 ;
1846  resource_size_t __cil_tmp14 ;
1847  int __cil_tmp15 ;
1848  int __cil_tmp16 ;
1849  int __cil_tmp17 ;
1850  struct resource *__cil_tmp18 ;
1851  resource_size_t __cil_tmp19 ;
1852  resource_size_t __cil_tmp20 ;
1853  int __cil_tmp21 ;
1854  int __cil_tmp22 ;
1855  int __cil_tmp23 ;
1856  struct resource *__cil_tmp24 ;
1857  resource_size_t __cil_tmp25 ;
1858  resource_size_t __cil_tmp26 ;
1859  int __cil_tmp27 ;
1860  int __cil_tmp28 ;
1861  int __cil_tmp29 ;
1862  struct resource *__cil_tmp30 ;
1863  resource_size_t __cil_tmp31 ;
1864  resource_size_t __cil_tmp32 ;
1865  int __cil_tmp33 ;
1866  void *__cil_tmp34 ;
1867
1868  {
1869  {
1870#line 117
1871  __cil_tmp5 = (void *)0;
1872#line 117
1873  err = (int )request_irq(12U, & ct82c710_interrupt, 0UL, "ct82c710", __cil_tmp5);
1874  }
1875#line 118
1876  if (err) {
1877#line 119
1878    return (err);
1879  } else {
1880
1881  }
1882  {
1883#line 121
1884  __cil_tmp6 = & ct82c710_iores;
1885#line 121
1886  __cil_tmp7 = *((resource_size_t *)__cil_tmp6);
1887#line 121
1888  __cil_tmp8 = __cil_tmp7 + 1ULL;
1889#line 121
1890  __cil_tmp9 = (int )__cil_tmp8;
1891#line 121
1892  status = inb_p(__cil_tmp9);
1893#line 123
1894  __cil_tmp10 = (int )status;
1895#line 123
1896  __cil_tmp11 = __cil_tmp10 | 136;
1897#line 123
1898  status = (unsigned char )__cil_tmp11;
1899#line 124
1900  __cil_tmp12 = & ct82c710_iores;
1901#line 124
1902  __cil_tmp13 = *((resource_size_t *)__cil_tmp12);
1903#line 124
1904  __cil_tmp14 = __cil_tmp13 + 1ULL;
1905#line 124
1906  __cil_tmp15 = (int )__cil_tmp14;
1907#line 124
1908  outb_p(status, __cil_tmp15);
1909#line 126
1910  __cil_tmp16 = (int )status;
1911#line 126
1912  __cil_tmp17 = __cil_tmp16 & -9;
1913#line 126
1914  status = (unsigned char )__cil_tmp17;
1915#line 127
1916  __cil_tmp18 = & ct82c710_iores;
1917#line 127
1918  __cil_tmp19 = *((resource_size_t *)__cil_tmp18);
1919#line 127
1920  __cil_tmp20 = __cil_tmp19 + 1ULL;
1921#line 127
1922  __cil_tmp21 = (int )__cil_tmp20;
1923#line 127
1924  outb_p(status, __cil_tmp21);
1925#line 129
1926  __cil_tmp22 = (int )status;
1927#line 129
1928  __cil_tmp23 = __cil_tmp22 | 16;
1929#line 129
1930  status = (unsigned char )__cil_tmp23;
1931#line 130
1932  __cil_tmp24 = & ct82c710_iores;
1933#line 130
1934  __cil_tmp25 = *((resource_size_t *)__cil_tmp24);
1935#line 130
1936  __cil_tmp26 = __cil_tmp25 + 1ULL;
1937#line 130
1938  __cil_tmp27 = (int )__cil_tmp26;
1939#line 130
1940  outb_p(status, __cil_tmp27);
1941  }
1942  {
1943#line 132
1944  while (1) {
1945    while_continue: /* CIL Label */ ;
1946    {
1947#line 132
1948    tmp = ct82c170_wait();
1949    }
1950#line 132
1951    if (tmp) {
1952
1953    } else {
1954#line 132
1955      goto while_break;
1956    }
1957    {
1958#line 133
1959    printk("<3>ct82c710: Device busy in open()\n");
1960#line 134
1961    __cil_tmp28 = (int )status;
1962#line 134
1963    __cil_tmp29 = __cil_tmp28 & -145;
1964#line 134
1965    status = (unsigned char )__cil_tmp29;
1966#line 135
1967    __cil_tmp30 = & ct82c710_iores;
1968#line 135
1969    __cil_tmp31 = *((resource_size_t *)__cil_tmp30);
1970#line 135
1971    __cil_tmp32 = __cil_tmp31 + 1ULL;
1972#line 135
1973    __cil_tmp33 = (int )__cil_tmp32;
1974#line 135
1975    outb_p(status, __cil_tmp33);
1976#line 136
1977    __cil_tmp34 = (void *)0;
1978#line 136
1979    free_irq(12U, __cil_tmp34);
1980    }
1981#line 137
1982    return (-16);
1983  }
1984  while_break: /* CIL Label */ ;
1985  }
1986#line 140
1987  return (0);
1988}
1989}
1990#line 147 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
1991static int ct82c710_write(struct serio *port , unsigned char c ) 
1992{ int tmp ;
1993  struct resource *__cil_tmp4 ;
1994  resource_size_t __cil_tmp5 ;
1995  int __cil_tmp6 ;
1996
1997  {
1998  {
1999#line 149
2000  tmp = ct82c170_wait();
2001  }
2002#line 149
2003  if (tmp) {
2004#line 149
2005    return (-1);
2006  } else {
2007
2008  }
2009  {
2010#line 150
2011  __cil_tmp4 = & ct82c710_iores;
2012#line 150
2013  __cil_tmp5 = *((resource_size_t *)__cil_tmp4);
2014#line 150
2015  __cil_tmp6 = (int )__cil_tmp5;
2016#line 150
2017  outb_p(c, __cil_tmp6);
2018  }
2019#line 151
2020  return (0);
2021}
2022}
2023#line 158
2024static int ct82c710_detect(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
2025#line 158 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2026static int ct82c710_detect(void) 
2027{ unsigned char tmp ;
2028  unsigned char tmp___0 ;
2029  int __cil_tmp3 ;
2030  struct resource *__cil_tmp4 ;
2031  int __cil_tmp5 ;
2032  int __cil_tmp6 ;
2033  unsigned long __cil_tmp7 ;
2034  struct resource *__cil_tmp8 ;
2035  resource_size_t __cil_tmp9 ;
2036  unsigned long __cil_tmp10 ;
2037
2038  {
2039  {
2040#line 160
2041  outb_p((unsigned char)85, 762);
2042#line 161
2043  outb_p((unsigned char)170, 1018);
2044#line 162
2045  outb_p((unsigned char)54, 1018);
2046#line 163
2047  outb_p((unsigned char)228, 1018);
2048#line 164
2049  outb_p((unsigned char)27, 762);
2050#line 165
2051  outb_p((unsigned char)15, 912);
2052#line 166
2053  tmp = inb_p(913);
2054  }
2055  {
2056#line 166
2057  __cil_tmp3 = (int )tmp;
2058#line 166
2059  if (__cil_tmp3 != 228) {
2060#line 167
2061    return (-19);
2062  } else {
2063
2064  }
2065  }
2066  {
2067#line 169
2068  outb_p((unsigned char)13, 912);
2069#line 170
2070  tmp___0 = inb_p(913);
2071#line 170
2072  __cil_tmp4 = & ct82c710_iores;
2073#line 170
2074  __cil_tmp5 = (int )tmp___0;
2075#line 170
2076  __cil_tmp6 = __cil_tmp5 << 2;
2077#line 170
2078  *((resource_size_t *)__cil_tmp4) = (resource_size_t )__cil_tmp6;
2079#line 171
2080  __cil_tmp7 = (unsigned long )(& ct82c710_iores) + 8;
2081#line 171
2082  __cil_tmp8 = & ct82c710_iores;
2083#line 171
2084  __cil_tmp9 = *((resource_size_t *)__cil_tmp8);
2085#line 171
2086  *((resource_size_t *)__cil_tmp7) = __cil_tmp9 + 1ULL;
2087#line 172
2088  __cil_tmp10 = (unsigned long )(& ct82c710_iores) + 24;
2089#line 172
2090  *((unsigned long *)__cil_tmp10) = 256UL;
2091#line 173
2092  outb_p((unsigned char)15, 912);
2093#line 174
2094  outb_p((unsigned char)15, 913);
2095  }
2096#line 176
2097  return (0);
2098}
2099}
2100#line 179
2101static int ct82c710_probe(struct platform_device *dev )  __attribute__((__section__(".devinit.text"),
2102__no_instrument_function__)) ;
2103#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2104static int ct82c710_probe(struct platform_device *dev ) 
2105{ void *tmp ;
2106  unsigned long __cil_tmp3 ;
2107  unsigned long __cil_tmp4 ;
2108  unsigned long __cil_tmp5 ;
2109  unsigned long __cil_tmp6 ;
2110  unsigned long __cil_tmp7 ;
2111  unsigned long __cil_tmp8 ;
2112  unsigned long __cil_tmp9 ;
2113  unsigned long __cil_tmp10 ;
2114  unsigned long __cil_tmp11 ;
2115  unsigned long __cil_tmp12 ;
2116  unsigned long __cil_tmp13 ;
2117  unsigned long __cil_tmp14 ;
2118  unsigned long __cil_tmp15 ;
2119  unsigned long __cil_tmp16 ;
2120  unsigned long __cil_tmp17 ;
2121  unsigned long __cil_tmp18 ;
2122  char *__cil_tmp19 ;
2123  unsigned long __cil_tmp20 ;
2124  unsigned long __cil_tmp21 ;
2125  unsigned long __cil_tmp22 ;
2126  unsigned long __cil_tmp23 ;
2127  char *__cil_tmp24 ;
2128  struct resource *__cil_tmp25 ;
2129  resource_size_t __cil_tmp26 ;
2130  struct resource *__cil_tmp27 ;
2131  resource_size_t __cil_tmp28 ;
2132
2133  {
2134  {
2135#line 181
2136  tmp = kzalloc(1056UL, 208U);
2137#line 181
2138  ct82c710_port = (struct serio *)tmp;
2139  }
2140#line 182
2141  if (! ct82c710_port) {
2142#line 183
2143    return (-12);
2144  } else {
2145
2146  }
2147  {
2148#line 185
2149  __cil_tmp3 = (unsigned long )ct82c710_port;
2150#line 185
2151  __cil_tmp4 = __cil_tmp3 + 73;
2152#line 185
2153  *((__u8 *)__cil_tmp4) = (__u8 )1;
2154#line 186
2155  __cil_tmp5 = (unsigned long )ct82c710_port;
2156#line 186
2157  __cil_tmp6 = __cil_tmp5 + 272;
2158#line 186
2159  __cil_tmp7 = (unsigned long )dev;
2160#line 186
2161  __cil_tmp8 = __cil_tmp7 + 16;
2162#line 186
2163  *((struct device **)__cil_tmp6) = (struct device *)__cil_tmp8;
2164#line 187
2165  __cil_tmp9 = (unsigned long )ct82c710_port;
2166#line 187
2167  __cil_tmp10 = __cil_tmp9 + 112;
2168#line 187
2169  *((int (**)(struct serio * ))__cil_tmp10) = & ct82c710_open;
2170#line 188
2171  __cil_tmp11 = (unsigned long )ct82c710_port;
2172#line 188
2173  __cil_tmp12 = __cil_tmp11 + 120;
2174#line 188
2175  *((void (**)(struct serio * ))__cil_tmp12) = & ct82c710_close;
2176#line 189
2177  __cil_tmp13 = (unsigned long )ct82c710_port;
2178#line 189
2179  __cil_tmp14 = __cil_tmp13 + 104;
2180#line 189
2181  *((int (**)(struct serio * , unsigned char  ))__cil_tmp14) = & ct82c710_write;
2182#line 190
2183  __cil_tmp15 = 0 * 1UL;
2184#line 190
2185  __cil_tmp16 = 8 + __cil_tmp15;
2186#line 190
2187  __cil_tmp17 = (unsigned long )ct82c710_port;
2188#line 190
2189  __cil_tmp18 = __cil_tmp17 + __cil_tmp16;
2190#line 190
2191  __cil_tmp19 = (char *)__cil_tmp18;
2192#line 190
2193  strlcpy(__cil_tmp19, "C&T 82c710 mouse port", 32UL);
2194#line 192
2195  __cil_tmp20 = 0 * 1UL;
2196#line 192
2197  __cil_tmp21 = 40 + __cil_tmp20;
2198#line 192
2199  __cil_tmp22 = (unsigned long )ct82c710_port;
2200#line 192
2201  __cil_tmp23 = __cil_tmp22 + __cil_tmp21;
2202#line 192
2203  __cil_tmp24 = (char *)__cil_tmp23;
2204#line 192
2205  __cil_tmp25 = & ct82c710_iores;
2206#line 192
2207  __cil_tmp26 = *((resource_size_t *)__cil_tmp25);
2208#line 192
2209  snprintf(__cil_tmp24, 32UL, "isa%16llx/serio0", __cil_tmp26);
2210#line 195
2211  __serio_register_port(ct82c710_port, & __this_module);
2212#line 197
2213  __cil_tmp27 = & ct82c710_iores;
2214#line 197
2215  __cil_tmp28 = *((resource_size_t *)__cil_tmp27);
2216#line 197
2217  printk("<6>serio: C&T 82c710 mouse port at %#llx irq %d\n", __cil_tmp28, 12);
2218  }
2219#line 200
2220  return (0);
2221}
2222}
2223#line 203
2224static int ct82c710_remove(struct platform_device *dev )  __attribute__((__section__(".devexit.text"),
2225__no_instrument_function__)) ;
2226#line 203 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2227static int ct82c710_remove(struct platform_device *dev ) 
2228{ 
2229
2230  {
2231  {
2232#line 205
2233  serio_unregister_port(ct82c710_port);
2234  }
2235#line 207
2236  return (0);
2237}
2238}
2239#line 210 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2240static struct platform_driver ct82c710_driver  =    {& ct82c710_probe, & ct82c710_remove, (void (*)(struct platform_device * ))0, (int (*)(struct platform_device * ,
2241                                                                                          pm_message_t state ))0,
2242    (int (*)(struct platform_device * ))0, {"ct82c710", (struct bus_type *)0, & __this_module,
2243                                            (char const   *)0, (_Bool)0, (struct of_device_id  const  *)0,
2244                                            (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
2245                                            (void (*)(struct device *dev ))0, (int (*)(struct device *dev ,
2246                                                                                       pm_message_t state ))0,
2247                                            (int (*)(struct device *dev ))0, (struct attribute_group  const  **)0,
2248                                            (struct dev_pm_ops  const  *)0, (struct driver_private *)0},
2249    (struct platform_device_id  const  *)0};
2250#line 220
2251static int ct82c710_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
2252#line 220 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2253static int ct82c710_init(void) 
2254{ int error ;
2255  struct resource  const  *__cil_tmp2 ;
2256
2257  {
2258  {
2259#line 224
2260  error = ct82c710_detect();
2261  }
2262#line 225
2263  if (error) {
2264#line 226
2265    return (error);
2266  } else {
2267
2268  }
2269  {
2270#line 228
2271  error = platform_driver_register(& ct82c710_driver);
2272  }
2273#line 229
2274  if (error) {
2275#line 230
2276    return (error);
2277  } else {
2278
2279  }
2280  {
2281#line 232
2282  ct82c710_device = platform_device_alloc("ct82c710", -1);
2283  }
2284#line 233
2285  if (! ct82c710_device) {
2286#line 234
2287    error = -12;
2288#line 235
2289    goto err_unregister_driver;
2290  } else {
2291
2292  }
2293  {
2294#line 238
2295  __cil_tmp2 = (struct resource  const  *)(& ct82c710_iores);
2296#line 238
2297  error = platform_device_add_resources(ct82c710_device, __cil_tmp2, 1U);
2298  }
2299#line 239
2300  if (error) {
2301#line 240
2302    goto err_free_device;
2303  } else {
2304
2305  }
2306  {
2307#line 242
2308  error = platform_device_add(ct82c710_device);
2309  }
2310#line 243
2311  if (error) {
2312#line 244
2313    goto err_free_device;
2314  } else {
2315
2316  }
2317#line 246
2318  return (0);
2319  err_free_device: 
2320  {
2321#line 249
2322  platform_device_put(ct82c710_device);
2323  }
2324  err_unregister_driver: 
2325  {
2326#line 251
2327  platform_driver_unregister(& ct82c710_driver);
2328  }
2329#line 252
2330  return (error);
2331}
2332}
2333#line 255
2334static void ct82c710_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
2335#line 255 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2336static void ct82c710_exit(void) 
2337{ 
2338
2339  {
2340  {
2341#line 257
2342  platform_device_unregister(ct82c710_device);
2343#line 258
2344  platform_driver_unregister(& ct82c710_driver);
2345  }
2346#line 259
2347  return;
2348}
2349}
2350#line 261 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2351int init_module(void) 
2352{ int tmp ;
2353
2354  {
2355  {
2356#line 261
2357  tmp = ct82c710_init();
2358  }
2359#line 261
2360  return (tmp);
2361}
2362}
2363#line 262 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2364void cleanup_module(void) 
2365{ 
2366
2367  {
2368  {
2369#line 262
2370  ct82c710_exit();
2371  }
2372#line 262
2373  return;
2374}
2375}
2376#line 280
2377void ldv_check_final_state(void) ;
2378#line 283
2379extern void ldv_check_return_value(int res ) ;
2380#line 286
2381extern void ldv_initialize(void) ;
2382#line 289
2383extern int __VERIFIER_nondet_int(void) ;
2384#line 292 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2385int LDV_IN_INTERRUPT  ;
2386#line 319 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2387static int res_ct82c710_probe_6  ;
2388#line 295 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2389void main(void) 
2390{ struct platform_device *var_group1 ;
2391  int var_ct82c710_interrupt_0_p0 ;
2392  void *var_ct82c710_interrupt_0_p1 ;
2393  int tmp ;
2394  int ldv_s_ct82c710_driver_platform_driver ;
2395  int tmp___0 ;
2396  int tmp___1 ;
2397  int __cil_tmp8 ;
2398
2399  {
2400  {
2401#line 347
2402  LDV_IN_INTERRUPT = 1;
2403#line 356
2404  ldv_initialize();
2405#line 374
2406  tmp = ct82c710_init();
2407  }
2408#line 374
2409  if (tmp) {
2410#line 375
2411    goto ldv_final;
2412  } else {
2413
2414  }
2415#line 376
2416  ldv_s_ct82c710_driver_platform_driver = 0;
2417  {
2418#line 381
2419  while (1) {
2420    while_continue: /* CIL Label */ ;
2421    {
2422#line 381
2423    tmp___1 = __VERIFIER_nondet_int();
2424    }
2425#line 381
2426    if (tmp___1) {
2427
2428    } else {
2429      {
2430#line 381
2431      __cil_tmp8 = ldv_s_ct82c710_driver_platform_driver == 0;
2432#line 381
2433      if (! __cil_tmp8) {
2434
2435      } else {
2436#line 381
2437        goto while_break;
2438      }
2439      }
2440    }
2441    {
2442#line 385
2443    tmp___0 = __VERIFIER_nondet_int();
2444    }
2445#line 387
2446    if (tmp___0 == 0) {
2447#line 387
2448      goto case_0;
2449    } else
2450#line 418
2451    if (tmp___0 == 1) {
2452#line 418
2453      goto case_1;
2454    } else {
2455      {
2456#line 446
2457      goto switch_default;
2458#line 385
2459      if (0) {
2460        case_0: /* CIL Label */ 
2461#line 390
2462        if (ldv_s_ct82c710_driver_platform_driver == 0) {
2463          {
2464#line 407
2465          res_ct82c710_probe_6 = ct82c710_probe(var_group1);
2466#line 408
2467          ldv_check_return_value(res_ct82c710_probe_6);
2468          }
2469#line 409
2470          if (res_ct82c710_probe_6) {
2471#line 410
2472            goto ldv_module_exit;
2473          } else {
2474
2475          }
2476#line 411
2477          ldv_s_ct82c710_driver_platform_driver = 0;
2478        } else {
2479
2480        }
2481#line 417
2482        goto switch_break;
2483        case_1: /* CIL Label */ 
2484        {
2485#line 421
2486        LDV_IN_INTERRUPT = 2;
2487#line 438
2488        ct82c710_interrupt(var_ct82c710_interrupt_0_p0, var_ct82c710_interrupt_0_p1);
2489#line 439
2490        LDV_IN_INTERRUPT = 1;
2491        }
2492#line 445
2493        goto switch_break;
2494        switch_default: /* CIL Label */ 
2495#line 446
2496        goto switch_break;
2497      } else {
2498        switch_break: /* CIL Label */ ;
2499      }
2500      }
2501    }
2502  }
2503  while_break: /* CIL Label */ ;
2504  }
2505  ldv_module_exit: 
2506  {
2507#line 470
2508  ct82c710_exit();
2509  }
2510  ldv_final: 
2511  {
2512#line 473
2513  ldv_check_final_state();
2514  }
2515#line 476
2516  return;
2517}
2518}
2519#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2520void ldv_blast_assert(void) 
2521{ 
2522
2523  {
2524  ERROR: 
2525#line 6
2526  goto ERROR;
2527}
2528}
2529#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2530extern int __VERIFIER_nondet_int(void) ;
2531#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2532int ldv_mutex  =    1;
2533#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2534int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
2535{ int nondetermined ;
2536
2537  {
2538#line 29
2539  if (ldv_mutex == 1) {
2540
2541  } else {
2542    {
2543#line 29
2544    ldv_blast_assert();
2545    }
2546  }
2547  {
2548#line 32
2549  nondetermined = __VERIFIER_nondet_int();
2550  }
2551#line 35
2552  if (nondetermined) {
2553#line 38
2554    ldv_mutex = 2;
2555#line 40
2556    return (0);
2557  } else {
2558#line 45
2559    return (-4);
2560  }
2561}
2562}
2563#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2564int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
2565{ int nondetermined ;
2566
2567  {
2568#line 57
2569  if (ldv_mutex == 1) {
2570
2571  } else {
2572    {
2573#line 57
2574    ldv_blast_assert();
2575    }
2576  }
2577  {
2578#line 60
2579  nondetermined = __VERIFIER_nondet_int();
2580  }
2581#line 63
2582  if (nondetermined) {
2583#line 66
2584    ldv_mutex = 2;
2585#line 68
2586    return (0);
2587  } else {
2588#line 73
2589    return (-4);
2590  }
2591}
2592}
2593#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2594int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
2595{ int atomic_value_after_dec ;
2596
2597  {
2598#line 83
2599  if (ldv_mutex == 1) {
2600
2601  } else {
2602    {
2603#line 83
2604    ldv_blast_assert();
2605    }
2606  }
2607  {
2608#line 86
2609  atomic_value_after_dec = __VERIFIER_nondet_int();
2610  }
2611#line 89
2612  if (atomic_value_after_dec == 0) {
2613#line 92
2614    ldv_mutex = 2;
2615#line 94
2616    return (1);
2617  } else {
2618
2619  }
2620#line 98
2621  return (0);
2622}
2623}
2624#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2625void mutex_lock(struct mutex *lock ) 
2626{ 
2627
2628  {
2629#line 108
2630  if (ldv_mutex == 1) {
2631
2632  } else {
2633    {
2634#line 108
2635    ldv_blast_assert();
2636    }
2637  }
2638#line 110
2639  ldv_mutex = 2;
2640#line 111
2641  return;
2642}
2643}
2644#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2645int mutex_trylock(struct mutex *lock ) 
2646{ int nondetermined ;
2647
2648  {
2649#line 121
2650  if (ldv_mutex == 1) {
2651
2652  } else {
2653    {
2654#line 121
2655    ldv_blast_assert();
2656    }
2657  }
2658  {
2659#line 124
2660  nondetermined = __VERIFIER_nondet_int();
2661  }
2662#line 127
2663  if (nondetermined) {
2664#line 130
2665    ldv_mutex = 2;
2666#line 132
2667    return (1);
2668  } else {
2669#line 137
2670    return (0);
2671  }
2672}
2673}
2674#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2675void mutex_unlock(struct mutex *lock ) 
2676{ 
2677
2678  {
2679#line 147
2680  if (ldv_mutex == 2) {
2681
2682  } else {
2683    {
2684#line 147
2685    ldv_blast_assert();
2686    }
2687  }
2688#line 149
2689  ldv_mutex = 1;
2690#line 150
2691  return;
2692}
2693}
2694#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2695void ldv_check_final_state(void) 
2696{ 
2697
2698  {
2699#line 156
2700  if (ldv_mutex == 1) {
2701
2702  } else {
2703    {
2704#line 156
2705    ldv_blast_assert();
2706    }
2707  }
2708#line 157
2709  return;
2710}
2711}
2712#line 485 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/drivers/input/serio/ct82c710.c.common.c"
2713long s__builtin_expect(long val , long res ) 
2714{ 
2715
2716  {
2717#line 486
2718  return (val);
2719}
2720}