Showing error 272

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--mouse--gpio_mouse.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3710
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 20 "include/asm-generic/int-ll64.h"
   7typedef unsigned char __u8;
   8#line 22 "include/asm-generic/int-ll64.h"
   9typedef short __s16;
  10#line 23 "include/asm-generic/int-ll64.h"
  11typedef unsigned short __u16;
  12#line 25 "include/asm-generic/int-ll64.h"
  13typedef int __s32;
  14#line 26 "include/asm-generic/int-ll64.h"
  15typedef unsigned int __u32;
  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 52 "include/asm-generic/posix_types.h"
  37typedef unsigned int __kernel_uid32_t;
  38#line 53 "include/asm-generic/posix_types.h"
  39typedef unsigned int __kernel_gid32_t;
  40#line 75 "include/asm-generic/posix_types.h"
  41typedef __kernel_ulong_t __kernel_size_t;
  42#line 76 "include/asm-generic/posix_types.h"
  43typedef __kernel_long_t __kernel_ssize_t;
  44#line 91 "include/asm-generic/posix_types.h"
  45typedef long long __kernel_loff_t;
  46#line 92 "include/asm-generic/posix_types.h"
  47typedef __kernel_long_t __kernel_time_t;
  48#line 21 "include/linux/types.h"
  49typedef __u32 __kernel_dev_t;
  50#line 24 "include/linux/types.h"
  51typedef __kernel_dev_t dev_t;
  52#line 27 "include/linux/types.h"
  53typedef unsigned short umode_t;
  54#line 38 "include/linux/types.h"
  55typedef _Bool bool;
  56#line 40 "include/linux/types.h"
  57typedef __kernel_uid32_t uid_t;
  58#line 41 "include/linux/types.h"
  59typedef __kernel_gid32_t gid_t;
  60#line 54 "include/linux/types.h"
  61typedef __kernel_loff_t loff_t;
  62#line 63 "include/linux/types.h"
  63typedef __kernel_size_t size_t;
  64#line 68 "include/linux/types.h"
  65typedef __kernel_ssize_t ssize_t;
  66#line 78 "include/linux/types.h"
  67typedef __kernel_time_t time_t;
  68#line 142 "include/linux/types.h"
  69typedef unsigned long sector_t;
  70#line 143 "include/linux/types.h"
  71typedef unsigned long blkcnt_t;
  72#line 202 "include/linux/types.h"
  73typedef unsigned int gfp_t;
  74#line 203 "include/linux/types.h"
  75typedef unsigned int fmode_t;
  76#line 206 "include/linux/types.h"
  77typedef u64 phys_addr_t;
  78#line 211 "include/linux/types.h"
  79typedef phys_addr_t resource_size_t;
  80#line 219 "include/linux/types.h"
  81struct __anonstruct_atomic_t_7 {
  82   int counter ;
  83};
  84#line 219 "include/linux/types.h"
  85typedef struct __anonstruct_atomic_t_7 atomic_t;
  86#line 224 "include/linux/types.h"
  87struct __anonstruct_atomic64_t_8 {
  88   long counter ;
  89};
  90#line 224 "include/linux/types.h"
  91typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  92#line 229 "include/linux/types.h"
  93struct list_head {
  94   struct list_head *next ;
  95   struct list_head *prev ;
  96};
  97#line 233
  98struct hlist_node;
  99#line 233 "include/linux/types.h"
 100struct hlist_head {
 101   struct hlist_node *first ;
 102};
 103#line 237 "include/linux/types.h"
 104struct hlist_node {
 105   struct hlist_node *next ;
 106   struct hlist_node **pprev ;
 107};
 108#line 253 "include/linux/types.h"
 109struct rcu_head {
 110   struct rcu_head *next ;
 111   void (*func)(struct rcu_head *head ) ;
 112};
 113#line 146 "include/linux/init.h"
 114typedef void (*ctor_fn_t)(void);
 115#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 116struct module;
 117#line 56
 118struct module;
 119#line 9 "include/linux/dynamic_debug.h"
 120struct _ddebug {
 121   char const   *modname ;
 122   char const   *function ;
 123   char const   *filename ;
 124   char const   *format ;
 125   unsigned int lineno : 18 ;
 126   unsigned int flags : 8 ;
 127} __attribute__((__aligned__(8))) ;
 128#line 47
 129struct device;
 130#line 47
 131struct device;
 132#line 135 "include/linux/kernel.h"
 133struct completion;
 134#line 135
 135struct completion;
 136#line 349
 137struct pid;
 138#line 349
 139struct pid;
 140#line 12 "include/linux/thread_info.h"
 141struct timespec;
 142#line 12
 143struct timespec;
 144#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
 145struct page;
 146#line 18
 147struct page;
 148#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
 149struct task_struct;
 150#line 20
 151struct task_struct;
 152#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 153struct task_struct;
 154#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 155struct file;
 156#line 295
 157struct file;
 158#line 313
 159struct seq_file;
 160#line 313
 161struct seq_file;
 162#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 163struct page;
 164#line 52
 165struct task_struct;
 166#line 329
 167struct arch_spinlock;
 168#line 329
 169struct arch_spinlock;
 170#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 171struct task_struct;
 172#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 173struct task_struct;
 174#line 10 "include/asm-generic/bug.h"
 175struct bug_entry {
 176   int bug_addr_disp ;
 177   int file_disp ;
 178   unsigned short line ;
 179   unsigned short flags ;
 180};
 181#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 182struct static_key;
 183#line 234
 184struct static_key;
 185#line 23 "include/asm-generic/atomic-long.h"
 186typedef atomic64_t atomic_long_t;
 187#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 188typedef u16 __ticket_t;
 189#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 190typedef u32 __ticketpair_t;
 191#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 192struct __raw_tickets {
 193   __ticket_t head ;
 194   __ticket_t tail ;
 195};
 196#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 197union __anonunion____missing_field_name_36 {
 198   __ticketpair_t head_tail ;
 199   struct __raw_tickets tickets ;
 200};
 201#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 202struct arch_spinlock {
 203   union __anonunion____missing_field_name_36 __annonCompField17 ;
 204};
 205#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 206typedef struct arch_spinlock arch_spinlock_t;
 207#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 208struct __anonstruct____missing_field_name_38 {
 209   u32 read ;
 210   s32 write ;
 211};
 212#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 213union __anonunion_arch_rwlock_t_37 {
 214   s64 lock ;
 215   struct __anonstruct____missing_field_name_38 __annonCompField18 ;
 216};
 217#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 218typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_t;
 219#line 12 "include/linux/lockdep.h"
 220struct task_struct;
 221#line 391 "include/linux/lockdep.h"
 222struct lock_class_key {
 223
 224};
 225#line 20 "include/linux/spinlock_types.h"
 226struct raw_spinlock {
 227   arch_spinlock_t raw_lock ;
 228   unsigned int magic ;
 229   unsigned int owner_cpu ;
 230   void *owner ;
 231};
 232#line 20 "include/linux/spinlock_types.h"
 233typedef struct raw_spinlock raw_spinlock_t;
 234#line 64 "include/linux/spinlock_types.h"
 235union __anonunion____missing_field_name_39 {
 236   struct raw_spinlock rlock ;
 237};
 238#line 64 "include/linux/spinlock_types.h"
 239struct spinlock {
 240   union __anonunion____missing_field_name_39 __annonCompField19 ;
 241};
 242#line 64 "include/linux/spinlock_types.h"
 243typedef struct spinlock spinlock_t;
 244#line 11 "include/linux/rwlock_types.h"
 245struct __anonstruct_rwlock_t_40 {
 246   arch_rwlock_t raw_lock ;
 247   unsigned int magic ;
 248   unsigned int owner_cpu ;
 249   void *owner ;
 250};
 251#line 11 "include/linux/rwlock_types.h"
 252typedef struct __anonstruct_rwlock_t_40 rwlock_t;
 253#line 119 "include/linux/seqlock.h"
 254struct seqcount {
 255   unsigned int sequence ;
 256};
 257#line 119 "include/linux/seqlock.h"
 258typedef struct seqcount seqcount_t;
 259#line 14 "include/linux/time.h"
 260struct timespec {
 261   __kernel_time_t tv_sec ;
 262   long tv_nsec ;
 263};
 264#line 62 "include/linux/stat.h"
 265struct kstat {
 266   u64 ino ;
 267   dev_t dev ;
 268   umode_t mode ;
 269   unsigned int nlink ;
 270   uid_t uid ;
 271   gid_t gid ;
 272   dev_t rdev ;
 273   loff_t size ;
 274   struct timespec atime ;
 275   struct timespec mtime ;
 276   struct timespec ctime ;
 277   unsigned long blksize ;
 278   unsigned long long blocks ;
 279};
 280#line 49 "include/linux/wait.h"
 281struct __wait_queue_head {
 282   spinlock_t lock ;
 283   struct list_head task_list ;
 284};
 285#line 53 "include/linux/wait.h"
 286typedef struct __wait_queue_head wait_queue_head_t;
 287#line 55
 288struct task_struct;
 289#line 60 "include/linux/pageblock-flags.h"
 290struct page;
 291#line 48 "include/linux/mutex.h"
 292struct mutex {
 293   atomic_t count ;
 294   spinlock_t wait_lock ;
 295   struct list_head wait_list ;
 296   struct task_struct *owner ;
 297   char const   *name ;
 298   void *magic ;
 299};
 300#line 19 "include/linux/rwsem.h"
 301struct rw_semaphore;
 302#line 19
 303struct rw_semaphore;
 304#line 25 "include/linux/rwsem.h"
 305struct rw_semaphore {
 306   long count ;
 307   raw_spinlock_t wait_lock ;
 308   struct list_head wait_list ;
 309};
 310#line 25 "include/linux/completion.h"
 311struct completion {
 312   unsigned int done ;
 313   wait_queue_head_t wait ;
 314};
 315#line 9 "include/linux/memory_hotplug.h"
 316struct page;
 317#line 18 "include/linux/ioport.h"
 318struct resource {
 319   resource_size_t start ;
 320   resource_size_t end ;
 321   char const   *name ;
 322   unsigned long flags ;
 323   struct resource *parent ;
 324   struct resource *sibling ;
 325   struct resource *child ;
 326};
 327#line 202
 328struct device;
 329#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 330struct device;
 331#line 46 "include/linux/ktime.h"
 332union ktime {
 333   s64 tv64 ;
 334};
 335#line 59 "include/linux/ktime.h"
 336typedef union ktime ktime_t;
 337#line 10 "include/linux/timer.h"
 338struct tvec_base;
 339#line 10
 340struct tvec_base;
 341#line 12 "include/linux/timer.h"
 342struct timer_list {
 343   struct list_head entry ;
 344   unsigned long expires ;
 345   struct tvec_base *base ;
 346   void (*function)(unsigned long  ) ;
 347   unsigned long data ;
 348   int slack ;
 349   int start_pid ;
 350   void *start_site ;
 351   char start_comm[16] ;
 352};
 353#line 17 "include/linux/workqueue.h"
 354struct work_struct;
 355#line 17
 356struct work_struct;
 357#line 79 "include/linux/workqueue.h"
 358struct work_struct {
 359   atomic_long_t data ;
 360   struct list_head entry ;
 361   void (*func)(struct work_struct *work ) ;
 362};
 363#line 92 "include/linux/workqueue.h"
 364struct delayed_work {
 365   struct work_struct work ;
 366   struct timer_list timer ;
 367};
 368#line 42 "include/linux/pm.h"
 369struct device;
 370#line 50 "include/linux/pm.h"
 371struct pm_message {
 372   int event ;
 373};
 374#line 50 "include/linux/pm.h"
 375typedef struct pm_message pm_message_t;
 376#line 264 "include/linux/pm.h"
 377struct dev_pm_ops {
 378   int (*prepare)(struct device *dev ) ;
 379   void (*complete)(struct device *dev ) ;
 380   int (*suspend)(struct device *dev ) ;
 381   int (*resume)(struct device *dev ) ;
 382   int (*freeze)(struct device *dev ) ;
 383   int (*thaw)(struct device *dev ) ;
 384   int (*poweroff)(struct device *dev ) ;
 385   int (*restore)(struct device *dev ) ;
 386   int (*suspend_late)(struct device *dev ) ;
 387   int (*resume_early)(struct device *dev ) ;
 388   int (*freeze_late)(struct device *dev ) ;
 389   int (*thaw_early)(struct device *dev ) ;
 390   int (*poweroff_late)(struct device *dev ) ;
 391   int (*restore_early)(struct device *dev ) ;
 392   int (*suspend_noirq)(struct device *dev ) ;
 393   int (*resume_noirq)(struct device *dev ) ;
 394   int (*freeze_noirq)(struct device *dev ) ;
 395   int (*thaw_noirq)(struct device *dev ) ;
 396   int (*poweroff_noirq)(struct device *dev ) ;
 397   int (*restore_noirq)(struct device *dev ) ;
 398   int (*runtime_suspend)(struct device *dev ) ;
 399   int (*runtime_resume)(struct device *dev ) ;
 400   int (*runtime_idle)(struct device *dev ) ;
 401};
 402#line 458
 403enum rpm_status {
 404    RPM_ACTIVE = 0,
 405    RPM_RESUMING = 1,
 406    RPM_SUSPENDED = 2,
 407    RPM_SUSPENDING = 3
 408} ;
 409#line 480
 410enum rpm_request {
 411    RPM_REQ_NONE = 0,
 412    RPM_REQ_IDLE = 1,
 413    RPM_REQ_SUSPEND = 2,
 414    RPM_REQ_AUTOSUSPEND = 3,
 415    RPM_REQ_RESUME = 4
 416} ;
 417#line 488
 418struct wakeup_source;
 419#line 488
 420struct wakeup_source;
 421#line 495 "include/linux/pm.h"
 422struct pm_subsys_data {
 423   spinlock_t lock ;
 424   unsigned int refcount ;
 425};
 426#line 506
 427struct dev_pm_qos_request;
 428#line 506
 429struct pm_qos_constraints;
 430#line 506 "include/linux/pm.h"
 431struct dev_pm_info {
 432   pm_message_t power_state ;
 433   unsigned int can_wakeup : 1 ;
 434   unsigned int async_suspend : 1 ;
 435   bool is_prepared : 1 ;
 436   bool is_suspended : 1 ;
 437   bool ignore_children : 1 ;
 438   spinlock_t lock ;
 439   struct list_head entry ;
 440   struct completion completion ;
 441   struct wakeup_source *wakeup ;
 442   bool wakeup_path : 1 ;
 443   struct timer_list suspend_timer ;
 444   unsigned long timer_expires ;
 445   struct work_struct work ;
 446   wait_queue_head_t wait_queue ;
 447   atomic_t usage_count ;
 448   atomic_t child_count ;
 449   unsigned int disable_depth : 3 ;
 450   unsigned int idle_notification : 1 ;
 451   unsigned int request_pending : 1 ;
 452   unsigned int deferred_resume : 1 ;
 453   unsigned int run_wake : 1 ;
 454   unsigned int runtime_auto : 1 ;
 455   unsigned int no_callbacks : 1 ;
 456   unsigned int irq_safe : 1 ;
 457   unsigned int use_autosuspend : 1 ;
 458   unsigned int timer_autosuspends : 1 ;
 459   enum rpm_request request ;
 460   enum rpm_status runtime_status ;
 461   int runtime_error ;
 462   int autosuspend_delay ;
 463   unsigned long last_busy ;
 464   unsigned long active_jiffies ;
 465   unsigned long suspended_jiffies ;
 466   unsigned long accounting_timestamp ;
 467   ktime_t suspend_time ;
 468   s64 max_time_suspended_ns ;
 469   struct dev_pm_qos_request *pq_req ;
 470   struct pm_subsys_data *subsys_data ;
 471   struct pm_qos_constraints *constraints ;
 472};
 473#line 564 "include/linux/pm.h"
 474struct dev_pm_domain {
 475   struct dev_pm_ops ops ;
 476};
 477#line 8 "include/linux/vmalloc.h"
 478struct vm_area_struct;
 479#line 8
 480struct vm_area_struct;
 481#line 994 "include/linux/mmzone.h"
 482struct page;
 483#line 10 "include/linux/gfp.h"
 484struct vm_area_struct;
 485#line 29 "include/linux/sysctl.h"
 486struct completion;
 487#line 48 "include/linux/kmod.h"
 488struct cred;
 489#line 48
 490struct cred;
 491#line 49
 492struct file;
 493#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 494struct task_struct;
 495#line 18 "include/linux/elf.h"
 496typedef __u64 Elf64_Addr;
 497#line 19 "include/linux/elf.h"
 498typedef __u16 Elf64_Half;
 499#line 23 "include/linux/elf.h"
 500typedef __u32 Elf64_Word;
 501#line 24 "include/linux/elf.h"
 502typedef __u64 Elf64_Xword;
 503#line 194 "include/linux/elf.h"
 504struct elf64_sym {
 505   Elf64_Word st_name ;
 506   unsigned char st_info ;
 507   unsigned char st_other ;
 508   Elf64_Half st_shndx ;
 509   Elf64_Addr st_value ;
 510   Elf64_Xword st_size ;
 511};
 512#line 194 "include/linux/elf.h"
 513typedef struct elf64_sym Elf64_Sym;
 514#line 438
 515struct file;
 516#line 20 "include/linux/kobject_ns.h"
 517struct sock;
 518#line 20
 519struct sock;
 520#line 21
 521struct kobject;
 522#line 21
 523struct kobject;
 524#line 27
 525enum kobj_ns_type {
 526    KOBJ_NS_TYPE_NONE = 0,
 527    KOBJ_NS_TYPE_NET = 1,
 528    KOBJ_NS_TYPES = 2
 529} ;
 530#line 40 "include/linux/kobject_ns.h"
 531struct kobj_ns_type_operations {
 532   enum kobj_ns_type type ;
 533   void *(*grab_current_ns)(void) ;
 534   void const   *(*netlink_ns)(struct sock *sk ) ;
 535   void const   *(*initial_ns)(void) ;
 536   void (*drop_ns)(void * ) ;
 537};
 538#line 22 "include/linux/sysfs.h"
 539struct kobject;
 540#line 23
 541struct module;
 542#line 24
 543enum kobj_ns_type;
 544#line 26 "include/linux/sysfs.h"
 545struct attribute {
 546   char const   *name ;
 547   umode_t mode ;
 548};
 549#line 56 "include/linux/sysfs.h"
 550struct attribute_group {
 551   char const   *name ;
 552   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 553   struct attribute **attrs ;
 554};
 555#line 85
 556struct file;
 557#line 86
 558struct vm_area_struct;
 559#line 88 "include/linux/sysfs.h"
 560struct bin_attribute {
 561   struct attribute attr ;
 562   size_t size ;
 563   void *private ;
 564   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 565                   loff_t  , size_t  ) ;
 566   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 567                    loff_t  , size_t  ) ;
 568   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 569};
 570#line 112 "include/linux/sysfs.h"
 571struct sysfs_ops {
 572   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 573   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 574   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 575};
 576#line 118
 577struct sysfs_dirent;
 578#line 118
 579struct sysfs_dirent;
 580#line 22 "include/linux/kref.h"
 581struct kref {
 582   atomic_t refcount ;
 583};
 584#line 60 "include/linux/kobject.h"
 585struct kset;
 586#line 60
 587struct kobj_type;
 588#line 60 "include/linux/kobject.h"
 589struct kobject {
 590   char const   *name ;
 591   struct list_head entry ;
 592   struct kobject *parent ;
 593   struct kset *kset ;
 594   struct kobj_type *ktype ;
 595   struct sysfs_dirent *sd ;
 596   struct kref kref ;
 597   unsigned int state_initialized : 1 ;
 598   unsigned int state_in_sysfs : 1 ;
 599   unsigned int state_add_uevent_sent : 1 ;
 600   unsigned int state_remove_uevent_sent : 1 ;
 601   unsigned int uevent_suppress : 1 ;
 602};
 603#line 108 "include/linux/kobject.h"
 604struct kobj_type {
 605   void (*release)(struct kobject *kobj ) ;
 606   struct sysfs_ops  const  *sysfs_ops ;
 607   struct attribute **default_attrs ;
 608   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 609   void const   *(*namespace)(struct kobject *kobj ) ;
 610};
 611#line 116 "include/linux/kobject.h"
 612struct kobj_uevent_env {
 613   char *envp[32] ;
 614   int envp_idx ;
 615   char buf[2048] ;
 616   int buflen ;
 617};
 618#line 123 "include/linux/kobject.h"
 619struct kset_uevent_ops {
 620   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 621   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 622   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 623};
 624#line 140
 625struct sock;
 626#line 159 "include/linux/kobject.h"
 627struct kset {
 628   struct list_head list ;
 629   spinlock_t list_lock ;
 630   struct kobject kobj ;
 631   struct kset_uevent_ops  const  *uevent_ops ;
 632};
 633#line 39 "include/linux/moduleparam.h"
 634struct kernel_param;
 635#line 39
 636struct kernel_param;
 637#line 41 "include/linux/moduleparam.h"
 638struct kernel_param_ops {
 639   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
 640   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
 641   void (*free)(void *arg ) ;
 642};
 643#line 50
 644struct kparam_string;
 645#line 50
 646struct kparam_array;
 647#line 50 "include/linux/moduleparam.h"
 648union __anonunion____missing_field_name_199 {
 649   void *arg ;
 650   struct kparam_string  const  *str ;
 651   struct kparam_array  const  *arr ;
 652};
 653#line 50 "include/linux/moduleparam.h"
 654struct kernel_param {
 655   char const   *name ;
 656   struct kernel_param_ops  const  *ops ;
 657   u16 perm ;
 658   s16 level ;
 659   union __anonunion____missing_field_name_199 __annonCompField32 ;
 660};
 661#line 63 "include/linux/moduleparam.h"
 662struct kparam_string {
 663   unsigned int maxlen ;
 664   char *string ;
 665};
 666#line 69 "include/linux/moduleparam.h"
 667struct kparam_array {
 668   unsigned int max ;
 669   unsigned int elemsize ;
 670   unsigned int *num ;
 671   struct kernel_param_ops  const  *ops ;
 672   void *elem ;
 673};
 674#line 445
 675struct module;
 676#line 80 "include/linux/jump_label.h"
 677struct module;
 678#line 143 "include/linux/jump_label.h"
 679struct static_key {
 680   atomic_t enabled ;
 681};
 682#line 22 "include/linux/tracepoint.h"
 683struct module;
 684#line 23
 685struct tracepoint;
 686#line 23
 687struct tracepoint;
 688#line 25 "include/linux/tracepoint.h"
 689struct tracepoint_func {
 690   void *func ;
 691   void *data ;
 692};
 693#line 30 "include/linux/tracepoint.h"
 694struct tracepoint {
 695   char const   *name ;
 696   struct static_key key ;
 697   void (*regfunc)(void) ;
 698   void (*unregfunc)(void) ;
 699   struct tracepoint_func *funcs ;
 700};
 701#line 19 "include/linux/export.h"
 702struct kernel_symbol {
 703   unsigned long value ;
 704   char const   *name ;
 705};
 706#line 8 "include/asm-generic/module.h"
 707struct mod_arch_specific {
 708
 709};
 710#line 35 "include/linux/module.h"
 711struct module;
 712#line 37
 713struct module_param_attrs;
 714#line 37 "include/linux/module.h"
 715struct module_kobject {
 716   struct kobject kobj ;
 717   struct module *mod ;
 718   struct kobject *drivers_dir ;
 719   struct module_param_attrs *mp ;
 720};
 721#line 44 "include/linux/module.h"
 722struct module_attribute {
 723   struct attribute attr ;
 724   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 725   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 726                    size_t count ) ;
 727   void (*setup)(struct module * , char const   * ) ;
 728   int (*test)(struct module * ) ;
 729   void (*free)(struct module * ) ;
 730};
 731#line 71
 732struct exception_table_entry;
 733#line 71
 734struct exception_table_entry;
 735#line 199
 736enum module_state {
 737    MODULE_STATE_LIVE = 0,
 738    MODULE_STATE_COMING = 1,
 739    MODULE_STATE_GOING = 2
 740} ;
 741#line 215 "include/linux/module.h"
 742struct module_ref {
 743   unsigned long incs ;
 744   unsigned long decs ;
 745} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 746#line 220
 747struct module_sect_attrs;
 748#line 220
 749struct module_notes_attrs;
 750#line 220
 751struct ftrace_event_call;
 752#line 220 "include/linux/module.h"
 753struct module {
 754   enum module_state state ;
 755   struct list_head list ;
 756   char name[64UL - sizeof(unsigned long )] ;
 757   struct module_kobject mkobj ;
 758   struct module_attribute *modinfo_attrs ;
 759   char const   *version ;
 760   char const   *srcversion ;
 761   struct kobject *holders_dir ;
 762   struct kernel_symbol  const  *syms ;
 763   unsigned long const   *crcs ;
 764   unsigned int num_syms ;
 765   struct kernel_param *kp ;
 766   unsigned int num_kp ;
 767   unsigned int num_gpl_syms ;
 768   struct kernel_symbol  const  *gpl_syms ;
 769   unsigned long const   *gpl_crcs ;
 770   struct kernel_symbol  const  *unused_syms ;
 771   unsigned long const   *unused_crcs ;
 772   unsigned int num_unused_syms ;
 773   unsigned int num_unused_gpl_syms ;
 774   struct kernel_symbol  const  *unused_gpl_syms ;
 775   unsigned long const   *unused_gpl_crcs ;
 776   struct kernel_symbol  const  *gpl_future_syms ;
 777   unsigned long const   *gpl_future_crcs ;
 778   unsigned int num_gpl_future_syms ;
 779   unsigned int num_exentries ;
 780   struct exception_table_entry *extable ;
 781   int (*init)(void) ;
 782   void *module_init ;
 783   void *module_core ;
 784   unsigned int init_size ;
 785   unsigned int core_size ;
 786   unsigned int init_text_size ;
 787   unsigned int core_text_size ;
 788   unsigned int init_ro_size ;
 789   unsigned int core_ro_size ;
 790   struct mod_arch_specific arch ;
 791   unsigned int taints ;
 792   unsigned int num_bugs ;
 793   struct list_head bug_list ;
 794   struct bug_entry *bug_table ;
 795   Elf64_Sym *symtab ;
 796   Elf64_Sym *core_symtab ;
 797   unsigned int num_symtab ;
 798   unsigned int core_num_syms ;
 799   char *strtab ;
 800   char *core_strtab ;
 801   struct module_sect_attrs *sect_attrs ;
 802   struct module_notes_attrs *notes_attrs ;
 803   char *args ;
 804   void *percpu ;
 805   unsigned int percpu_size ;
 806   unsigned int num_tracepoints ;
 807   struct tracepoint * const  *tracepoints_ptrs ;
 808   unsigned int num_trace_bprintk_fmt ;
 809   char const   **trace_bprintk_fmt_start ;
 810   struct ftrace_event_call **trace_events ;
 811   unsigned int num_trace_events ;
 812   struct list_head source_list ;
 813   struct list_head target_list ;
 814   struct task_struct *waiter ;
 815   void (*exit)(void) ;
 816   struct module_ref *refptr ;
 817   ctor_fn_t *ctors ;
 818   unsigned int num_ctors ;
 819};
 820#line 19 "include/linux/klist.h"
 821struct klist_node;
 822#line 19
 823struct klist_node;
 824#line 39 "include/linux/klist.h"
 825struct klist_node {
 826   void *n_klist ;
 827   struct list_head n_node ;
 828   struct kref n_ref ;
 829};
 830#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 831struct dma_map_ops;
 832#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 833struct dev_archdata {
 834   void *acpi_handle ;
 835   struct dma_map_ops *dma_ops ;
 836   void *iommu ;
 837};
 838#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 839struct pdev_archdata {
 840
 841};
 842#line 28 "include/linux/device.h"
 843struct device;
 844#line 29
 845struct device_private;
 846#line 29
 847struct device_private;
 848#line 30
 849struct device_driver;
 850#line 30
 851struct device_driver;
 852#line 31
 853struct driver_private;
 854#line 31
 855struct driver_private;
 856#line 32
 857struct module;
 858#line 33
 859struct class;
 860#line 33
 861struct class;
 862#line 34
 863struct subsys_private;
 864#line 34
 865struct subsys_private;
 866#line 35
 867struct bus_type;
 868#line 35
 869struct bus_type;
 870#line 36
 871struct device_node;
 872#line 36
 873struct device_node;
 874#line 37
 875struct iommu_ops;
 876#line 37
 877struct iommu_ops;
 878#line 39 "include/linux/device.h"
 879struct bus_attribute {
 880   struct attribute attr ;
 881   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
 882   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
 883};
 884#line 89
 885struct device_attribute;
 886#line 89
 887struct driver_attribute;
 888#line 89 "include/linux/device.h"
 889struct bus_type {
 890   char const   *name ;
 891   char const   *dev_name ;
 892   struct device *dev_root ;
 893   struct bus_attribute *bus_attrs ;
 894   struct device_attribute *dev_attrs ;
 895   struct driver_attribute *drv_attrs ;
 896   int (*match)(struct device *dev , struct device_driver *drv ) ;
 897   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 898   int (*probe)(struct device *dev ) ;
 899   int (*remove)(struct device *dev ) ;
 900   void (*shutdown)(struct device *dev ) ;
 901   int (*suspend)(struct device *dev , pm_message_t state ) ;
 902   int (*resume)(struct device *dev ) ;
 903   struct dev_pm_ops  const  *pm ;
 904   struct iommu_ops *iommu_ops ;
 905   struct subsys_private *p ;
 906};
 907#line 127
 908struct device_type;
 909#line 214
 910struct of_device_id;
 911#line 214 "include/linux/device.h"
 912struct device_driver {
 913   char const   *name ;
 914   struct bus_type *bus ;
 915   struct module *owner ;
 916   char const   *mod_name ;
 917   bool suppress_bind_attrs ;
 918   struct of_device_id  const  *of_match_table ;
 919   int (*probe)(struct device *dev ) ;
 920   int (*remove)(struct device *dev ) ;
 921   void (*shutdown)(struct device *dev ) ;
 922   int (*suspend)(struct device *dev , pm_message_t state ) ;
 923   int (*resume)(struct device *dev ) ;
 924   struct attribute_group  const  **groups ;
 925   struct dev_pm_ops  const  *pm ;
 926   struct driver_private *p ;
 927};
 928#line 249 "include/linux/device.h"
 929struct driver_attribute {
 930   struct attribute attr ;
 931   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
 932   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
 933};
 934#line 330
 935struct class_attribute;
 936#line 330 "include/linux/device.h"
 937struct class {
 938   char const   *name ;
 939   struct module *owner ;
 940   struct class_attribute *class_attrs ;
 941   struct device_attribute *dev_attrs ;
 942   struct bin_attribute *dev_bin_attrs ;
 943   struct kobject *dev_kobj ;
 944   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 945   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 946   void (*class_release)(struct class *class ) ;
 947   void (*dev_release)(struct device *dev ) ;
 948   int (*suspend)(struct device *dev , pm_message_t state ) ;
 949   int (*resume)(struct device *dev ) ;
 950   struct kobj_ns_type_operations  const  *ns_type ;
 951   void const   *(*namespace)(struct device *dev ) ;
 952   struct dev_pm_ops  const  *pm ;
 953   struct subsys_private *p ;
 954};
 955#line 397 "include/linux/device.h"
 956struct class_attribute {
 957   struct attribute attr ;
 958   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
 959   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
 960                    size_t count ) ;
 961   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
 962};
 963#line 465 "include/linux/device.h"
 964struct device_type {
 965   char const   *name ;
 966   struct attribute_group  const  **groups ;
 967   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 968   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 969   void (*release)(struct device *dev ) ;
 970   struct dev_pm_ops  const  *pm ;
 971};
 972#line 476 "include/linux/device.h"
 973struct device_attribute {
 974   struct attribute attr ;
 975   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
 976   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
 977                    size_t count ) ;
 978};
 979#line 559 "include/linux/device.h"
 980struct device_dma_parameters {
 981   unsigned int max_segment_size ;
 982   unsigned long segment_boundary_mask ;
 983};
 984#line 627
 985struct dma_coherent_mem;
 986#line 627 "include/linux/device.h"
 987struct device {
 988   struct device *parent ;
 989   struct device_private *p ;
 990   struct kobject kobj ;
 991   char const   *init_name ;
 992   struct device_type  const  *type ;
 993   struct mutex mutex ;
 994   struct bus_type *bus ;
 995   struct device_driver *driver ;
 996   void *platform_data ;
 997   struct dev_pm_info power ;
 998   struct dev_pm_domain *pm_domain ;
 999   int numa_node ;
1000   u64 *dma_mask ;
1001   u64 coherent_dma_mask ;
1002   struct device_dma_parameters *dma_parms ;
1003   struct list_head dma_pools ;
1004   struct dma_coherent_mem *dma_mem ;
1005   struct dev_archdata archdata ;
1006   struct device_node *of_node ;
1007   dev_t devt ;
1008   u32 id ;
1009   spinlock_t devres_lock ;
1010   struct list_head devres_head ;
1011   struct klist_node knode_class ;
1012   struct class *class ;
1013   struct attribute_group  const  **groups ;
1014   void (*release)(struct device *dev ) ;
1015};
1016#line 43 "include/linux/pm_wakeup.h"
1017struct wakeup_source {
1018   char const   *name ;
1019   struct list_head entry ;
1020   spinlock_t lock ;
1021   struct timer_list timer ;
1022   unsigned long timer_expires ;
1023   ktime_t total_time ;
1024   ktime_t max_time ;
1025   ktime_t last_time ;
1026   unsigned long event_count ;
1027   unsigned long active_count ;
1028   unsigned long relax_count ;
1029   unsigned long hit_count ;
1030   unsigned int active : 1 ;
1031};
1032#line 12 "include/linux/mod_devicetable.h"
1033typedef unsigned long kernel_ulong_t;
1034#line 219 "include/linux/mod_devicetable.h"
1035struct of_device_id {
1036   char name[32] ;
1037   char type[32] ;
1038   char compatible[128] ;
1039   void *data ;
1040};
1041#line 312 "include/linux/mod_devicetable.h"
1042struct input_device_id {
1043   kernel_ulong_t flags ;
1044   __u16 bustype ;
1045   __u16 vendor ;
1046   __u16 product ;
1047   __u16 version ;
1048   kernel_ulong_t evbit[1] ;
1049   kernel_ulong_t keybit[12] ;
1050   kernel_ulong_t relbit[1] ;
1051   kernel_ulong_t absbit[1] ;
1052   kernel_ulong_t mscbit[1] ;
1053   kernel_ulong_t ledbit[1] ;
1054   kernel_ulong_t sndbit[1] ;
1055   kernel_ulong_t ffbit[2] ;
1056   kernel_ulong_t swbit[1] ;
1057   kernel_ulong_t driver_info ;
1058};
1059#line 506 "include/linux/mod_devicetable.h"
1060struct platform_device_id {
1061   char name[20] ;
1062   kernel_ulong_t driver_data  __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
1063};
1064#line 17 "include/linux/platform_device.h"
1065struct mfd_cell;
1066#line 17
1067struct mfd_cell;
1068#line 19 "include/linux/platform_device.h"
1069struct platform_device {
1070   char const   *name ;
1071   int id ;
1072   struct device dev ;
1073   u32 num_resources ;
1074   struct resource *resource ;
1075   struct platform_device_id  const  *id_entry ;
1076   struct mfd_cell *mfd_cell ;
1077   struct pdev_archdata archdata ;
1078};
1079#line 164 "include/linux/platform_device.h"
1080struct platform_driver {
1081   int (*probe)(struct platform_device * ) ;
1082   int (*remove)(struct platform_device * ) ;
1083   void (*shutdown)(struct platform_device * ) ;
1084   int (*suspend)(struct platform_device * , pm_message_t state ) ;
1085   int (*resume)(struct platform_device * ) ;
1086   struct device_driver driver ;
1087   struct platform_device_id  const  *id_table ;
1088};
1089#line 43 "include/linux/input.h"
1090struct input_id {
1091   __u16 bustype ;
1092   __u16 vendor ;
1093   __u16 product ;
1094   __u16 version ;
1095};
1096#line 69 "include/linux/input.h"
1097struct input_absinfo {
1098   __s32 value ;
1099   __s32 minimum ;
1100   __s32 maximum ;
1101   __s32 fuzz ;
1102   __s32 flat ;
1103   __s32 resolution ;
1104};
1105#line 93 "include/linux/input.h"
1106struct input_keymap_entry {
1107   __u8 flags ;
1108   __u8 len ;
1109   __u16 index ;
1110   __u32 keycode ;
1111   __u8 scancode[32] ;
1112};
1113#line 957 "include/linux/input.h"
1114struct ff_replay {
1115   __u16 length ;
1116   __u16 delay ;
1117};
1118#line 967 "include/linux/input.h"
1119struct ff_trigger {
1120   __u16 button ;
1121   __u16 interval ;
1122};
1123#line 984 "include/linux/input.h"
1124struct ff_envelope {
1125   __u16 attack_length ;
1126   __u16 attack_level ;
1127   __u16 fade_length ;
1128   __u16 fade_level ;
1129};
1130#line 996 "include/linux/input.h"
1131struct ff_constant_effect {
1132   __s16 level ;
1133   struct ff_envelope envelope ;
1134};
1135#line 1007 "include/linux/input.h"
1136struct ff_ramp_effect {
1137   __s16 start_level ;
1138   __s16 end_level ;
1139   struct ff_envelope envelope ;
1140};
1141#line 1023 "include/linux/input.h"
1142struct ff_condition_effect {
1143   __u16 right_saturation ;
1144   __u16 left_saturation ;
1145   __s16 right_coeff ;
1146   __s16 left_coeff ;
1147   __u16 deadband ;
1148   __s16 center ;
1149};
1150#line 1052 "include/linux/input.h"
1151struct ff_periodic_effect {
1152   __u16 waveform ;
1153   __u16 period ;
1154   __s16 magnitude ;
1155   __s16 offset ;
1156   __u16 phase ;
1157   struct ff_envelope envelope ;
1158   __u32 custom_len ;
1159   __s16 *custom_data ;
1160};
1161#line 1073 "include/linux/input.h"
1162struct ff_rumble_effect {
1163   __u16 strong_magnitude ;
1164   __u16 weak_magnitude ;
1165};
1166#line 1101 "include/linux/input.h"
1167union __anonunion_u_202 {
1168   struct ff_constant_effect constant ;
1169   struct ff_ramp_effect ramp ;
1170   struct ff_periodic_effect periodic ;
1171   struct ff_condition_effect condition[2] ;
1172   struct ff_rumble_effect rumble ;
1173};
1174#line 1101 "include/linux/input.h"
1175struct ff_effect {
1176   __u16 type ;
1177   __s16 id ;
1178   __u16 direction ;
1179   struct ff_trigger trigger ;
1180   struct ff_replay replay ;
1181   union __anonunion_u_202 u ;
1182};
1183#line 15 "include/linux/blk_types.h"
1184struct page;
1185#line 16
1186struct block_device;
1187#line 16
1188struct block_device;
1189#line 33 "include/linux/list_bl.h"
1190struct hlist_bl_node;
1191#line 33 "include/linux/list_bl.h"
1192struct hlist_bl_head {
1193   struct hlist_bl_node *first ;
1194};
1195#line 37 "include/linux/list_bl.h"
1196struct hlist_bl_node {
1197   struct hlist_bl_node *next ;
1198   struct hlist_bl_node **pprev ;
1199};
1200#line 13 "include/linux/dcache.h"
1201struct nameidata;
1202#line 13
1203struct nameidata;
1204#line 14
1205struct path;
1206#line 14
1207struct path;
1208#line 15
1209struct vfsmount;
1210#line 15
1211struct vfsmount;
1212#line 35 "include/linux/dcache.h"
1213struct qstr {
1214   unsigned int hash ;
1215   unsigned int len ;
1216   unsigned char const   *name ;
1217};
1218#line 88
1219struct inode;
1220#line 88
1221struct dentry_operations;
1222#line 88
1223struct super_block;
1224#line 88 "include/linux/dcache.h"
1225union __anonunion_d_u_203 {
1226   struct list_head d_child ;
1227   struct rcu_head d_rcu ;
1228};
1229#line 88 "include/linux/dcache.h"
1230struct dentry {
1231   unsigned int d_flags ;
1232   seqcount_t d_seq ;
1233   struct hlist_bl_node d_hash ;
1234   struct dentry *d_parent ;
1235   struct qstr d_name ;
1236   struct inode *d_inode ;
1237   unsigned char d_iname[32] ;
1238   unsigned int d_count ;
1239   spinlock_t d_lock ;
1240   struct dentry_operations  const  *d_op ;
1241   struct super_block *d_sb ;
1242   unsigned long d_time ;
1243   void *d_fsdata ;
1244   struct list_head d_lru ;
1245   union __anonunion_d_u_203 d_u ;
1246   struct list_head d_subdirs ;
1247   struct list_head d_alias ;
1248};
1249#line 131 "include/linux/dcache.h"
1250struct dentry_operations {
1251   int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1252   int (*d_hash)(struct dentry  const  * , struct inode  const  * , struct qstr * ) ;
1253   int (*d_compare)(struct dentry  const  * , struct inode  const  * , struct dentry  const  * ,
1254                    struct inode  const  * , unsigned int  , char const   * , struct qstr  const  * ) ;
1255   int (*d_delete)(struct dentry  const  * ) ;
1256   void (*d_release)(struct dentry * ) ;
1257   void (*d_prune)(struct dentry * ) ;
1258   void (*d_iput)(struct dentry * , struct inode * ) ;
1259   char *(*d_dname)(struct dentry * , char * , int  ) ;
1260   struct vfsmount *(*d_automount)(struct path * ) ;
1261   int (*d_manage)(struct dentry * , bool  ) ;
1262} __attribute__((__aligned__((1) <<  (6) ))) ;
1263#line 4 "include/linux/path.h"
1264struct dentry;
1265#line 5
1266struct vfsmount;
1267#line 7 "include/linux/path.h"
1268struct path {
1269   struct vfsmount *mnt ;
1270   struct dentry *dentry ;
1271};
1272#line 64 "include/linux/radix-tree.h"
1273struct radix_tree_node;
1274#line 64 "include/linux/radix-tree.h"
1275struct radix_tree_root {
1276   unsigned int height ;
1277   gfp_t gfp_mask ;
1278   struct radix_tree_node *rnode ;
1279};
1280#line 14 "include/linux/prio_tree.h"
1281struct prio_tree_node;
1282#line 20 "include/linux/prio_tree.h"
1283struct prio_tree_node {
1284   struct prio_tree_node *left ;
1285   struct prio_tree_node *right ;
1286   struct prio_tree_node *parent ;
1287   unsigned long start ;
1288   unsigned long last ;
1289};
1290#line 28 "include/linux/prio_tree.h"
1291struct prio_tree_root {
1292   struct prio_tree_node *prio_tree_node ;
1293   unsigned short index_bits ;
1294   unsigned short raw ;
1295};
1296#line 6 "include/linux/pid.h"
1297enum pid_type {
1298    PIDTYPE_PID = 0,
1299    PIDTYPE_PGID = 1,
1300    PIDTYPE_SID = 2,
1301    PIDTYPE_MAX = 3
1302} ;
1303#line 50
1304struct pid_namespace;
1305#line 50 "include/linux/pid.h"
1306struct upid {
1307   int nr ;
1308   struct pid_namespace *ns ;
1309   struct hlist_node pid_chain ;
1310};
1311#line 57 "include/linux/pid.h"
1312struct pid {
1313   atomic_t count ;
1314   unsigned int level ;
1315   struct hlist_head tasks[3] ;
1316   struct rcu_head rcu ;
1317   struct upid numbers[1] ;
1318};
1319#line 100
1320struct pid_namespace;
1321#line 18 "include/linux/capability.h"
1322struct task_struct;
1323#line 377
1324struct dentry;
1325#line 16 "include/linux/fiemap.h"
1326struct fiemap_extent {
1327   __u64 fe_logical ;
1328   __u64 fe_physical ;
1329   __u64 fe_length ;
1330   __u64 fe_reserved64[2] ;
1331   __u32 fe_flags ;
1332   __u32 fe_reserved[3] ;
1333};
1334#line 8 "include/linux/shrinker.h"
1335struct shrink_control {
1336   gfp_t gfp_mask ;
1337   unsigned long nr_to_scan ;
1338};
1339#line 31 "include/linux/shrinker.h"
1340struct shrinker {
1341   int (*shrink)(struct shrinker * , struct shrink_control *sc ) ;
1342   int seeks ;
1343   long batch ;
1344   struct list_head list ;
1345   atomic_long_t nr_in_batch ;
1346};
1347#line 10 "include/linux/migrate_mode.h"
1348enum migrate_mode {
1349    MIGRATE_ASYNC = 0,
1350    MIGRATE_SYNC_LIGHT = 1,
1351    MIGRATE_SYNC = 2
1352} ;
1353#line 408 "include/linux/fs.h"
1354struct export_operations;
1355#line 408
1356struct export_operations;
1357#line 410
1358struct iovec;
1359#line 410
1360struct iovec;
1361#line 411
1362struct nameidata;
1363#line 412
1364struct kiocb;
1365#line 412
1366struct kiocb;
1367#line 413
1368struct kobject;
1369#line 414
1370struct pipe_inode_info;
1371#line 414
1372struct pipe_inode_info;
1373#line 415
1374struct poll_table_struct;
1375#line 415
1376struct poll_table_struct;
1377#line 416
1378struct kstatfs;
1379#line 416
1380struct kstatfs;
1381#line 417
1382struct vm_area_struct;
1383#line 418
1384struct vfsmount;
1385#line 419
1386struct cred;
1387#line 469 "include/linux/fs.h"
1388struct iattr {
1389   unsigned int ia_valid ;
1390   umode_t ia_mode ;
1391   uid_t ia_uid ;
1392   gid_t ia_gid ;
1393   loff_t ia_size ;
1394   struct timespec ia_atime ;
1395   struct timespec ia_mtime ;
1396   struct timespec ia_ctime ;
1397   struct file *ia_file ;
1398};
1399#line 129 "include/linux/quota.h"
1400struct if_dqinfo {
1401   __u64 dqi_bgrace ;
1402   __u64 dqi_igrace ;
1403   __u32 dqi_flags ;
1404   __u32 dqi_valid ;
1405};
1406#line 50 "include/linux/dqblk_xfs.h"
1407struct fs_disk_quota {
1408   __s8 d_version ;
1409   __s8 d_flags ;
1410   __u16 d_fieldmask ;
1411   __u32 d_id ;
1412   __u64 d_blk_hardlimit ;
1413   __u64 d_blk_softlimit ;
1414   __u64 d_ino_hardlimit ;
1415   __u64 d_ino_softlimit ;
1416   __u64 d_bcount ;
1417   __u64 d_icount ;
1418   __s32 d_itimer ;
1419   __s32 d_btimer ;
1420   __u16 d_iwarns ;
1421   __u16 d_bwarns ;
1422   __s32 d_padding2 ;
1423   __u64 d_rtb_hardlimit ;
1424   __u64 d_rtb_softlimit ;
1425   __u64 d_rtbcount ;
1426   __s32 d_rtbtimer ;
1427   __u16 d_rtbwarns ;
1428   __s16 d_padding3 ;
1429   char d_padding4[8] ;
1430};
1431#line 146 "include/linux/dqblk_xfs.h"
1432struct fs_qfilestat {
1433   __u64 qfs_ino ;
1434   __u64 qfs_nblks ;
1435   __u32 qfs_nextents ;
1436};
1437#line 146 "include/linux/dqblk_xfs.h"
1438typedef struct fs_qfilestat fs_qfilestat_t;
1439#line 152 "include/linux/dqblk_xfs.h"
1440struct fs_quota_stat {
1441   __s8 qs_version ;
1442   __u16 qs_flags ;
1443   __s8 qs_pad ;
1444   fs_qfilestat_t qs_uquota ;
1445   fs_qfilestat_t qs_gquota ;
1446   __u32 qs_incoredqs ;
1447   __s32 qs_btimelimit ;
1448   __s32 qs_itimelimit ;
1449   __s32 qs_rtbtimelimit ;
1450   __u16 qs_bwarnlimit ;
1451   __u16 qs_iwarnlimit ;
1452};
1453#line 17 "include/linux/dqblk_qtree.h"
1454struct dquot;
1455#line 17
1456struct dquot;
1457#line 185 "include/linux/quota.h"
1458typedef __kernel_uid32_t qid_t;
1459#line 186 "include/linux/quota.h"
1460typedef long long qsize_t;
1461#line 200 "include/linux/quota.h"
1462struct mem_dqblk {
1463   qsize_t dqb_bhardlimit ;
1464   qsize_t dqb_bsoftlimit ;
1465   qsize_t dqb_curspace ;
1466   qsize_t dqb_rsvspace ;
1467   qsize_t dqb_ihardlimit ;
1468   qsize_t dqb_isoftlimit ;
1469   qsize_t dqb_curinodes ;
1470   time_t dqb_btime ;
1471   time_t dqb_itime ;
1472};
1473#line 215
1474struct quota_format_type;
1475#line 215
1476struct quota_format_type;
1477#line 217 "include/linux/quota.h"
1478struct mem_dqinfo {
1479   struct quota_format_type *dqi_format ;
1480   int dqi_fmt_id ;
1481   struct list_head dqi_dirty_list ;
1482   unsigned long dqi_flags ;
1483   unsigned int dqi_bgrace ;
1484   unsigned int dqi_igrace ;
1485   qsize_t dqi_maxblimit ;
1486   qsize_t dqi_maxilimit ;
1487   void *dqi_priv ;
1488};
1489#line 230
1490struct super_block;
1491#line 288 "include/linux/quota.h"
1492struct dquot {
1493   struct hlist_node dq_hash ;
1494   struct list_head dq_inuse ;
1495   struct list_head dq_free ;
1496   struct list_head dq_dirty ;
1497   struct mutex dq_lock ;
1498   atomic_t dq_count ;
1499   wait_queue_head_t dq_wait_unused ;
1500   struct super_block *dq_sb ;
1501   unsigned int dq_id ;
1502   loff_t dq_off ;
1503   unsigned long dq_flags ;
1504   short dq_type ;
1505   struct mem_dqblk dq_dqb ;
1506};
1507#line 305 "include/linux/quota.h"
1508struct quota_format_ops {
1509   int (*check_quota_file)(struct super_block *sb , int type ) ;
1510   int (*read_file_info)(struct super_block *sb , int type ) ;
1511   int (*write_file_info)(struct super_block *sb , int type ) ;
1512   int (*free_file_info)(struct super_block *sb , int type ) ;
1513   int (*read_dqblk)(struct dquot *dquot ) ;
1514   int (*commit_dqblk)(struct dquot *dquot ) ;
1515   int (*release_dqblk)(struct dquot *dquot ) ;
1516};
1517#line 316 "include/linux/quota.h"
1518struct dquot_operations {
1519   int (*write_dquot)(struct dquot * ) ;
1520   struct dquot *(*alloc_dquot)(struct super_block * , int  ) ;
1521   void (*destroy_dquot)(struct dquot * ) ;
1522   int (*acquire_dquot)(struct dquot * ) ;
1523   int (*release_dquot)(struct dquot * ) ;
1524   int (*mark_dirty)(struct dquot * ) ;
1525   int (*write_info)(struct super_block * , int  ) ;
1526   qsize_t *(*get_reserved_space)(struct inode * ) ;
1527};
1528#line 329
1529struct path;
1530#line 332 "include/linux/quota.h"
1531struct quotactl_ops {
1532   int (*quota_on)(struct super_block * , int  , int  , struct path * ) ;
1533   int (*quota_on_meta)(struct super_block * , int  , int  ) ;
1534   int (*quota_off)(struct super_block * , int  ) ;
1535   int (*quota_sync)(struct super_block * , int  , int  ) ;
1536   int (*get_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1537   int (*set_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1538   int (*get_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1539   int (*set_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1540   int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1541   int (*set_xstate)(struct super_block * , unsigned int  , int  ) ;
1542};
1543#line 345 "include/linux/quota.h"
1544struct quota_format_type {
1545   int qf_fmt_id ;
1546   struct quota_format_ops  const  *qf_ops ;
1547   struct module *qf_owner ;
1548   struct quota_format_type *qf_next ;
1549};
1550#line 399 "include/linux/quota.h"
1551struct quota_info {
1552   unsigned int flags ;
1553   struct mutex dqio_mutex ;
1554   struct mutex dqonoff_mutex ;
1555   struct rw_semaphore dqptr_sem ;
1556   struct inode *files[2] ;
1557   struct mem_dqinfo info[2] ;
1558   struct quota_format_ops  const  *ops[2] ;
1559};
1560#line 532 "include/linux/fs.h"
1561struct page;
1562#line 533
1563struct address_space;
1564#line 533
1565struct address_space;
1566#line 534
1567struct writeback_control;
1568#line 534
1569struct writeback_control;
1570#line 577 "include/linux/fs.h"
1571union __anonunion_arg_211 {
1572   char *buf ;
1573   void *data ;
1574};
1575#line 577 "include/linux/fs.h"
1576struct __anonstruct_read_descriptor_t_210 {
1577   size_t written ;
1578   size_t count ;
1579   union __anonunion_arg_211 arg ;
1580   int error ;
1581};
1582#line 577 "include/linux/fs.h"
1583typedef struct __anonstruct_read_descriptor_t_210 read_descriptor_t;
1584#line 590 "include/linux/fs.h"
1585struct address_space_operations {
1586   int (*writepage)(struct page *page , struct writeback_control *wbc ) ;
1587   int (*readpage)(struct file * , struct page * ) ;
1588   int (*writepages)(struct address_space * , struct writeback_control * ) ;
1589   int (*set_page_dirty)(struct page *page ) ;
1590   int (*readpages)(struct file *filp , struct address_space *mapping , struct list_head *pages ,
1591                    unsigned int nr_pages ) ;
1592   int (*write_begin)(struct file * , struct address_space *mapping , loff_t pos ,
1593                      unsigned int len , unsigned int flags , struct page **pagep ,
1594                      void **fsdata ) ;
1595   int (*write_end)(struct file * , struct address_space *mapping , loff_t pos , unsigned int len ,
1596                    unsigned int copied , struct page *page , void *fsdata ) ;
1597   sector_t (*bmap)(struct address_space * , sector_t  ) ;
1598   void (*invalidatepage)(struct page * , unsigned long  ) ;
1599   int (*releasepage)(struct page * , gfp_t  ) ;
1600   void (*freepage)(struct page * ) ;
1601   ssize_t (*direct_IO)(int  , struct kiocb * , struct iovec  const  *iov , loff_t offset ,
1602                        unsigned long nr_segs ) ;
1603   int (*get_xip_mem)(struct address_space * , unsigned long  , int  , void ** , unsigned long * ) ;
1604   int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode  ) ;
1605   int (*launder_page)(struct page * ) ;
1606   int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long  ) ;
1607   int (*error_remove_page)(struct address_space * , struct page * ) ;
1608};
1609#line 645
1610struct backing_dev_info;
1611#line 645
1612struct backing_dev_info;
1613#line 646 "include/linux/fs.h"
1614struct address_space {
1615   struct inode *host ;
1616   struct radix_tree_root page_tree ;
1617   spinlock_t tree_lock ;
1618   unsigned int i_mmap_writable ;
1619   struct prio_tree_root i_mmap ;
1620   struct list_head i_mmap_nonlinear ;
1621   struct mutex i_mmap_mutex ;
1622   unsigned long nrpages ;
1623   unsigned long writeback_index ;
1624   struct address_space_operations  const  *a_ops ;
1625   unsigned long flags ;
1626   struct backing_dev_info *backing_dev_info ;
1627   spinlock_t private_lock ;
1628   struct list_head private_list ;
1629   struct address_space *assoc_mapping ;
1630} __attribute__((__aligned__(sizeof(long )))) ;
1631#line 669
1632struct request_queue;
1633#line 669
1634struct request_queue;
1635#line 671
1636struct hd_struct;
1637#line 671
1638struct gendisk;
1639#line 671 "include/linux/fs.h"
1640struct block_device {
1641   dev_t bd_dev ;
1642   int bd_openers ;
1643   struct inode *bd_inode ;
1644   struct super_block *bd_super ;
1645   struct mutex bd_mutex ;
1646   struct list_head bd_inodes ;
1647   void *bd_claiming ;
1648   void *bd_holder ;
1649   int bd_holders ;
1650   bool bd_write_holder ;
1651   struct list_head bd_holder_disks ;
1652   struct block_device *bd_contains ;
1653   unsigned int bd_block_size ;
1654   struct hd_struct *bd_part ;
1655   unsigned int bd_part_count ;
1656   int bd_invalidated ;
1657   struct gendisk *bd_disk ;
1658   struct request_queue *bd_queue ;
1659   struct list_head bd_list ;
1660   unsigned long bd_private ;
1661   int bd_fsfreeze_count ;
1662   struct mutex bd_fsfreeze_mutex ;
1663};
1664#line 749
1665struct posix_acl;
1666#line 749
1667struct posix_acl;
1668#line 761
1669struct inode_operations;
1670#line 761 "include/linux/fs.h"
1671union __anonunion____missing_field_name_212 {
1672   unsigned int const   i_nlink ;
1673   unsigned int __i_nlink ;
1674};
1675#line 761 "include/linux/fs.h"
1676union __anonunion____missing_field_name_213 {
1677   struct list_head i_dentry ;
1678   struct rcu_head i_rcu ;
1679};
1680#line 761
1681struct file_operations;
1682#line 761
1683struct file_lock;
1684#line 761
1685struct cdev;
1686#line 761 "include/linux/fs.h"
1687union __anonunion____missing_field_name_214 {
1688   struct pipe_inode_info *i_pipe ;
1689   struct block_device *i_bdev ;
1690   struct cdev *i_cdev ;
1691};
1692#line 761 "include/linux/fs.h"
1693struct inode {
1694   umode_t i_mode ;
1695   unsigned short i_opflags ;
1696   uid_t i_uid ;
1697   gid_t i_gid ;
1698   unsigned int i_flags ;
1699   struct posix_acl *i_acl ;
1700   struct posix_acl *i_default_acl ;
1701   struct inode_operations  const  *i_op ;
1702   struct super_block *i_sb ;
1703   struct address_space *i_mapping ;
1704   void *i_security ;
1705   unsigned long i_ino ;
1706   union __anonunion____missing_field_name_212 __annonCompField33 ;
1707   dev_t i_rdev ;
1708   struct timespec i_atime ;
1709   struct timespec i_mtime ;
1710   struct timespec i_ctime ;
1711   spinlock_t i_lock ;
1712   unsigned short i_bytes ;
1713   blkcnt_t i_blocks ;
1714   loff_t i_size ;
1715   unsigned long i_state ;
1716   struct mutex i_mutex ;
1717   unsigned long dirtied_when ;
1718   struct hlist_node i_hash ;
1719   struct list_head i_wb_list ;
1720   struct list_head i_lru ;
1721   struct list_head i_sb_list ;
1722   union __anonunion____missing_field_name_213 __annonCompField34 ;
1723   atomic_t i_count ;
1724   unsigned int i_blkbits ;
1725   u64 i_version ;
1726   atomic_t i_dio_count ;
1727   atomic_t i_writecount ;
1728   struct file_operations  const  *i_fop ;
1729   struct file_lock *i_flock ;
1730   struct address_space i_data ;
1731   struct dquot *i_dquot[2] ;
1732   struct list_head i_devices ;
1733   union __anonunion____missing_field_name_214 __annonCompField35 ;
1734   __u32 i_generation ;
1735   __u32 i_fsnotify_mask ;
1736   struct hlist_head i_fsnotify_marks ;
1737   atomic_t i_readcount ;
1738   void *i_private ;
1739};
1740#line 942 "include/linux/fs.h"
1741struct fown_struct {
1742   rwlock_t lock ;
1743   struct pid *pid ;
1744   enum pid_type pid_type ;
1745   uid_t uid ;
1746   uid_t euid ;
1747   int signum ;
1748};
1749#line 953 "include/linux/fs.h"
1750struct file_ra_state {
1751   unsigned long start ;
1752   unsigned int size ;
1753   unsigned int async_size ;
1754   unsigned int ra_pages ;
1755   unsigned int mmap_miss ;
1756   loff_t prev_pos ;
1757};
1758#line 976 "include/linux/fs.h"
1759union __anonunion_f_u_215 {
1760   struct list_head fu_list ;
1761   struct rcu_head fu_rcuhead ;
1762};
1763#line 976 "include/linux/fs.h"
1764struct file {
1765   union __anonunion_f_u_215 f_u ;
1766   struct path f_path ;
1767   struct file_operations  const  *f_op ;
1768   spinlock_t f_lock ;
1769   int f_sb_list_cpu ;
1770   atomic_long_t f_count ;
1771   unsigned int f_flags ;
1772   fmode_t f_mode ;
1773   loff_t f_pos ;
1774   struct fown_struct f_owner ;
1775   struct cred  const  *f_cred ;
1776   struct file_ra_state f_ra ;
1777   u64 f_version ;
1778   void *f_security ;
1779   void *private_data ;
1780   struct list_head f_ep_links ;
1781   struct list_head f_tfile_llink ;
1782   struct address_space *f_mapping ;
1783   unsigned long f_mnt_write_state ;
1784};
1785#line 1111
1786struct files_struct;
1787#line 1111 "include/linux/fs.h"
1788typedef struct files_struct *fl_owner_t;
1789#line 1113 "include/linux/fs.h"
1790struct file_lock_operations {
1791   void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1792   void (*fl_release_private)(struct file_lock * ) ;
1793};
1794#line 1118 "include/linux/fs.h"
1795struct lock_manager_operations {
1796   int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1797   void (*lm_notify)(struct file_lock * ) ;
1798   int (*lm_grant)(struct file_lock * , struct file_lock * , int  ) ;
1799   void (*lm_release_private)(struct file_lock * ) ;
1800   void (*lm_break)(struct file_lock * ) ;
1801   int (*lm_change)(struct file_lock ** , int  ) ;
1802};
1803#line 4 "include/linux/nfs_fs_i.h"
1804struct nlm_lockowner;
1805#line 4
1806struct nlm_lockowner;
1807#line 9 "include/linux/nfs_fs_i.h"
1808struct nfs_lock_info {
1809   u32 state ;
1810   struct nlm_lockowner *owner ;
1811   struct list_head list ;
1812};
1813#line 15
1814struct nfs4_lock_state;
1815#line 15
1816struct nfs4_lock_state;
1817#line 16 "include/linux/nfs_fs_i.h"
1818struct nfs4_lock_info {
1819   struct nfs4_lock_state *owner ;
1820};
1821#line 1138 "include/linux/fs.h"
1822struct fasync_struct;
1823#line 1138 "include/linux/fs.h"
1824struct __anonstruct_afs_217 {
1825   struct list_head link ;
1826   int state ;
1827};
1828#line 1138 "include/linux/fs.h"
1829union __anonunion_fl_u_216 {
1830   struct nfs_lock_info nfs_fl ;
1831   struct nfs4_lock_info nfs4_fl ;
1832   struct __anonstruct_afs_217 afs ;
1833};
1834#line 1138 "include/linux/fs.h"
1835struct file_lock {
1836   struct file_lock *fl_next ;
1837   struct list_head fl_link ;
1838   struct list_head fl_block ;
1839   fl_owner_t fl_owner ;
1840   unsigned int fl_flags ;
1841   unsigned char fl_type ;
1842   unsigned int fl_pid ;
1843   struct pid *fl_nspid ;
1844   wait_queue_head_t fl_wait ;
1845   struct file *fl_file ;
1846   loff_t fl_start ;
1847   loff_t fl_end ;
1848   struct fasync_struct *fl_fasync ;
1849   unsigned long fl_break_time ;
1850   unsigned long fl_downgrade_time ;
1851   struct file_lock_operations  const  *fl_ops ;
1852   struct lock_manager_operations  const  *fl_lmops ;
1853   union __anonunion_fl_u_216 fl_u ;
1854};
1855#line 1378 "include/linux/fs.h"
1856struct fasync_struct {
1857   spinlock_t fa_lock ;
1858   int magic ;
1859   int fa_fd ;
1860   struct fasync_struct *fa_next ;
1861   struct file *fa_file ;
1862   struct rcu_head fa_rcu ;
1863};
1864#line 1418
1865struct file_system_type;
1866#line 1418
1867struct super_operations;
1868#line 1418
1869struct xattr_handler;
1870#line 1418
1871struct mtd_info;
1872#line 1418 "include/linux/fs.h"
1873struct super_block {
1874   struct list_head s_list ;
1875   dev_t s_dev ;
1876   unsigned char s_dirt ;
1877   unsigned char s_blocksize_bits ;
1878   unsigned long s_blocksize ;
1879   loff_t s_maxbytes ;
1880   struct file_system_type *s_type ;
1881   struct super_operations  const  *s_op ;
1882   struct dquot_operations  const  *dq_op ;
1883   struct quotactl_ops  const  *s_qcop ;
1884   struct export_operations  const  *s_export_op ;
1885   unsigned long s_flags ;
1886   unsigned long s_magic ;
1887   struct dentry *s_root ;
1888   struct rw_semaphore s_umount ;
1889   struct mutex s_lock ;
1890   int s_count ;
1891   atomic_t s_active ;
1892   void *s_security ;
1893   struct xattr_handler  const  **s_xattr ;
1894   struct list_head s_inodes ;
1895   struct hlist_bl_head s_anon ;
1896   struct list_head *s_files ;
1897   struct list_head s_mounts ;
1898   struct list_head s_dentry_lru ;
1899   int s_nr_dentry_unused ;
1900   spinlock_t s_inode_lru_lock  __attribute__((__aligned__((1) <<  (6) ))) ;
1901   struct list_head s_inode_lru ;
1902   int s_nr_inodes_unused ;
1903   struct block_device *s_bdev ;
1904   struct backing_dev_info *s_bdi ;
1905   struct mtd_info *s_mtd ;
1906   struct hlist_node s_instances ;
1907   struct quota_info s_dquot ;
1908   int s_frozen ;
1909   wait_queue_head_t s_wait_unfrozen ;
1910   char s_id[32] ;
1911   u8 s_uuid[16] ;
1912   void *s_fs_info ;
1913   unsigned int s_max_links ;
1914   fmode_t s_mode ;
1915   u32 s_time_gran ;
1916   struct mutex s_vfs_rename_mutex ;
1917   char *s_subtype ;
1918   char *s_options ;
1919   struct dentry_operations  const  *s_d_op ;
1920   int cleancache_poolid ;
1921   struct shrinker s_shrink ;
1922   atomic_long_t s_remove_count ;
1923   int s_readonly_remount ;
1924};
1925#line 1567 "include/linux/fs.h"
1926struct fiemap_extent_info {
1927   unsigned int fi_flags ;
1928   unsigned int fi_extents_mapped ;
1929   unsigned int fi_extents_max ;
1930   struct fiemap_extent *fi_extents_start ;
1931};
1932#line 1609 "include/linux/fs.h"
1933struct file_operations {
1934   struct module *owner ;
1935   loff_t (*llseek)(struct file * , loff_t  , int  ) ;
1936   ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
1937   ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
1938   ssize_t (*aio_read)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1939                       loff_t  ) ;
1940   ssize_t (*aio_write)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1941                        loff_t  ) ;
1942   int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
1943                                                   loff_t  , u64  , unsigned int  ) ) ;
1944   unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1945   long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1946   long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1947   int (*mmap)(struct file * , struct vm_area_struct * ) ;
1948   int (*open)(struct inode * , struct file * ) ;
1949   int (*flush)(struct file * , fl_owner_t id ) ;
1950   int (*release)(struct inode * , struct file * ) ;
1951   int (*fsync)(struct file * , loff_t  , loff_t  , int datasync ) ;
1952   int (*aio_fsync)(struct kiocb * , int datasync ) ;
1953   int (*fasync)(int  , struct file * , int  ) ;
1954   int (*lock)(struct file * , int  , struct file_lock * ) ;
1955   ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
1956                       int  ) ;
1957   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
1958                                      unsigned long  , unsigned long  ) ;
1959   int (*check_flags)(int  ) ;
1960   int (*flock)(struct file * , int  , struct file_lock * ) ;
1961   ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t  ,
1962                           unsigned int  ) ;
1963   ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t  ,
1964                          unsigned int  ) ;
1965   int (*setlease)(struct file * , long  , struct file_lock ** ) ;
1966   long (*fallocate)(struct file *file , int mode , loff_t offset , loff_t len ) ;
1967};
1968#line 1639 "include/linux/fs.h"
1969struct inode_operations {
1970   struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1971   void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1972   int (*permission)(struct inode * , int  ) ;
1973   struct posix_acl *(*get_acl)(struct inode * , int  ) ;
1974   int (*readlink)(struct dentry * , char * , int  ) ;
1975   void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
1976   int (*create)(struct inode * , struct dentry * , umode_t  , struct nameidata * ) ;
1977   int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
1978   int (*unlink)(struct inode * , struct dentry * ) ;
1979   int (*symlink)(struct inode * , struct dentry * , char const   * ) ;
1980   int (*mkdir)(struct inode * , struct dentry * , umode_t  ) ;
1981   int (*rmdir)(struct inode * , struct dentry * ) ;
1982   int (*mknod)(struct inode * , struct dentry * , umode_t  , dev_t  ) ;
1983   int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
1984   void (*truncate)(struct inode * ) ;
1985   int (*setattr)(struct dentry * , struct iattr * ) ;
1986   int (*getattr)(struct vfsmount *mnt , struct dentry * , struct kstat * ) ;
1987   int (*setxattr)(struct dentry * , char const   * , void const   * , size_t  , int  ) ;
1988   ssize_t (*getxattr)(struct dentry * , char const   * , void * , size_t  ) ;
1989   ssize_t (*listxattr)(struct dentry * , char * , size_t  ) ;
1990   int (*removexattr)(struct dentry * , char const   * ) ;
1991   void (*truncate_range)(struct inode * , loff_t  , loff_t  ) ;
1992   int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 start , u64 len ) ;
1993} __attribute__((__aligned__((1) <<  (6) ))) ;
1994#line 1669
1995struct seq_file;
1996#line 1684 "include/linux/fs.h"
1997struct super_operations {
1998   struct inode *(*alloc_inode)(struct super_block *sb ) ;
1999   void (*destroy_inode)(struct inode * ) ;
2000   void (*dirty_inode)(struct inode * , int flags ) ;
2001   int (*write_inode)(struct inode * , struct writeback_control *wbc ) ;
2002   int (*drop_inode)(struct inode * ) ;
2003   void (*evict_inode)(struct inode * ) ;
2004   void (*put_super)(struct super_block * ) ;
2005   void (*write_super)(struct super_block * ) ;
2006   int (*sync_fs)(struct super_block *sb , int wait ) ;
2007   int (*freeze_fs)(struct super_block * ) ;
2008   int (*unfreeze_fs)(struct super_block * ) ;
2009   int (*statfs)(struct dentry * , struct kstatfs * ) ;
2010   int (*remount_fs)(struct super_block * , int * , char * ) ;
2011   void (*umount_begin)(struct super_block * ) ;
2012   int (*show_options)(struct seq_file * , struct dentry * ) ;
2013   int (*show_devname)(struct seq_file * , struct dentry * ) ;
2014   int (*show_path)(struct seq_file * , struct dentry * ) ;
2015   int (*show_stats)(struct seq_file * , struct dentry * ) ;
2016   ssize_t (*quota_read)(struct super_block * , int  , char * , size_t  , loff_t  ) ;
2017   ssize_t (*quota_write)(struct super_block * , int  , char const   * , size_t  ,
2018                          loff_t  ) ;
2019   int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t  ) ;
2020   int (*nr_cached_objects)(struct super_block * ) ;
2021   void (*free_cached_objects)(struct super_block * , int  ) ;
2022};
2023#line 1835 "include/linux/fs.h"
2024struct file_system_type {
2025   char const   *name ;
2026   int fs_flags ;
2027   struct dentry *(*mount)(struct file_system_type * , int  , char const   * , void * ) ;
2028   void (*kill_sb)(struct super_block * ) ;
2029   struct module *owner ;
2030   struct file_system_type *next ;
2031   struct hlist_head fs_supers ;
2032   struct lock_class_key s_lock_key ;
2033   struct lock_class_key s_umount_key ;
2034   struct lock_class_key s_vfs_rename_key ;
2035   struct lock_class_key i_lock_key ;
2036   struct lock_class_key i_mutex_key ;
2037   struct lock_class_key i_mutex_dir_key ;
2038};
2039#line 1250 "include/linux/input.h"
2040struct ff_device;
2041#line 1250
2042struct input_mt_slot;
2043#line 1250
2044struct input_handle;
2045#line 1250 "include/linux/input.h"
2046struct input_dev {
2047   char const   *name ;
2048   char const   *phys ;
2049   char const   *uniq ;
2050   struct input_id id ;
2051   unsigned long propbit[((32UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2052   unsigned long evbit[((32UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2053   unsigned long keybit[((768UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2054   unsigned long relbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2055   unsigned long absbit[((64UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2056   unsigned long mscbit[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2057   unsigned long ledbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2058   unsigned long sndbit[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2059   unsigned long ffbit[((128UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2060   unsigned long swbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2061   unsigned int hint_events_per_packet ;
2062   unsigned int keycodemax ;
2063   unsigned int keycodesize ;
2064   void *keycode ;
2065   int (*setkeycode)(struct input_dev *dev , struct input_keymap_entry  const  *ke ,
2066                     unsigned int *old_keycode ) ;
2067   int (*getkeycode)(struct input_dev *dev , struct input_keymap_entry *ke ) ;
2068   struct ff_device *ff ;
2069   unsigned int repeat_key ;
2070   struct timer_list timer ;
2071   int rep[2] ;
2072   struct input_mt_slot *mt ;
2073   int mtsize ;
2074   int slot ;
2075   int trkid ;
2076   struct input_absinfo *absinfo ;
2077   unsigned long key[((768UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2078   unsigned long led[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2079   unsigned long snd[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2080   unsigned long sw[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2081   int (*open)(struct input_dev *dev ) ;
2082   void (*close)(struct input_dev *dev ) ;
2083   int (*flush)(struct input_dev *dev , struct file *file ) ;
2084   int (*event)(struct input_dev *dev , unsigned int type , unsigned int code , int value ) ;
2085   struct input_handle *grab ;
2086   spinlock_t event_lock ;
2087   struct mutex mutex ;
2088   unsigned int users ;
2089   bool going_away ;
2090   bool sync ;
2091   struct device dev ;
2092   struct list_head h_list ;
2093   struct list_head node ;
2094};
2095#line 1370
2096struct input_handle;
2097#line 1409 "include/linux/input.h"
2098struct input_handler {
2099   void *private ;
2100   void (*event)(struct input_handle *handle , unsigned int type , unsigned int code ,
2101                 int value ) ;
2102   bool (*filter)(struct input_handle *handle , unsigned int type , unsigned int code ,
2103                  int value ) ;
2104   bool (*match)(struct input_handler *handler , struct input_dev *dev ) ;
2105   int (*connect)(struct input_handler *handler , struct input_dev *dev , struct input_device_id  const  *id ) ;
2106   void (*disconnect)(struct input_handle *handle ) ;
2107   void (*start)(struct input_handle *handle ) ;
2108   struct file_operations  const  *fops ;
2109   int minor ;
2110   char const   *name ;
2111   struct input_device_id  const  *id_table ;
2112   struct list_head h_list ;
2113   struct list_head node ;
2114};
2115#line 1442 "include/linux/input.h"
2116struct input_handle {
2117   void *private ;
2118   int open ;
2119   char const   *name ;
2120   struct input_dev *dev ;
2121   struct input_handler *handler ;
2122   struct list_head d_node ;
2123   struct list_head h_node ;
2124};
2125#line 1619 "include/linux/input.h"
2126struct ff_device {
2127   int (*upload)(struct input_dev *dev , struct ff_effect *effect , struct ff_effect *old ) ;
2128   int (*erase)(struct input_dev *dev , int effect_id ) ;
2129   int (*playback)(struct input_dev *dev , int effect_id , int value ) ;
2130   void (*set_gain)(struct input_dev *dev , u16 gain ) ;
2131   void (*set_autocenter)(struct input_dev *dev , u16 magnitude ) ;
2132   void (*destroy)(struct ff_device * ) ;
2133   void *private ;
2134   unsigned long ffbit[((128UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2135   struct mutex mutex ;
2136   int max_effects ;
2137   struct ff_effect *effects ;
2138   struct file *effect_owners[] ;
2139};
2140#line 37 "include/linux/input-polldev.h"
2141struct input_polled_dev {
2142   void *private ;
2143   void (*open)(struct input_polled_dev *dev ) ;
2144   void (*close)(struct input_polled_dev *dev ) ;
2145   void (*poll)(struct input_polled_dev *dev ) ;
2146   unsigned int poll_interval ;
2147   unsigned int poll_interval_max ;
2148   unsigned int poll_interval_min ;
2149   struct input_dev *input ;
2150   struct delayed_work work ;
2151};
2152#line 28 "include/linux/of.h"
2153typedef u32 phandle;
2154#line 31 "include/linux/of.h"
2155struct property {
2156   char *name ;
2157   int length ;
2158   void *value ;
2159   struct property *next ;
2160   unsigned long _flags ;
2161   unsigned int unique_id ;
2162};
2163#line 44
2164struct proc_dir_entry;
2165#line 44 "include/linux/of.h"
2166struct device_node {
2167   char const   *name ;
2168   char const   *type ;
2169   phandle phandle ;
2170   char *full_name ;
2171   struct property *properties ;
2172   struct property *deadprops ;
2173   struct device_node *parent ;
2174   struct device_node *child ;
2175   struct device_node *sibling ;
2176   struct device_node *next ;
2177   struct device_node *allnext ;
2178   struct proc_dir_entry *pde ;
2179   struct kref kref ;
2180   unsigned long _flags ;
2181   void *data ;
2182};
2183#line 44 "include/asm-generic/gpio.h"
2184struct device;
2185#line 46
2186struct seq_file;
2187#line 47
2188struct module;
2189#line 48
2190struct device_node;
2191#line 42 "include/linux/gpio_mouse.h"
2192struct __anonstruct____missing_field_name_221 {
2193   int up ;
2194   int down ;
2195   int left ;
2196   int right ;
2197   int bleft ;
2198   int bmiddle ;
2199   int bright ;
2200};
2201#line 42 "include/linux/gpio_mouse.h"
2202union __anonunion____missing_field_name_220 {
2203   struct __anonstruct____missing_field_name_221 __annonCompField36 ;
2204   int pins[7] ;
2205};
2206#line 42 "include/linux/gpio_mouse.h"
2207struct gpio_mouse_platform_data {
2208   int scan_ms ;
2209   int polarity ;
2210   union __anonunion____missing_field_name_220 __annonCompField37 ;
2211};
2212#line 1 "<compiler builtins>"
2213long __builtin_expect(long val , long res ) ;
2214#line 49 "include/linux/dynamic_debug.h"
2215extern int ( /* format attribute */  __dynamic_dev_dbg)(struct _ddebug *descriptor ,
2216                                                        struct device  const  *dev ,
2217                                                        char const   *fmt  , ...) ;
2218#line 152 "include/linux/mutex.h"
2219void mutex_lock(struct mutex *lock ) ;
2220#line 153
2221int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
2222#line 154
2223int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
2224#line 168
2225int mutex_trylock(struct mutex *lock ) ;
2226#line 169
2227void mutex_unlock(struct mutex *lock ) ;
2228#line 170
2229int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
2230#line 26 "include/linux/export.h"
2231extern struct module __this_module ;
2232#line 67 "include/linux/module.h"
2233int init_module(void) ;
2234#line 68
2235void cleanup_module(void) ;
2236#line 792 "include/linux/device.h"
2237extern void *dev_get_drvdata(struct device  const  *dev ) ;
2238#line 793
2239extern int dev_set_drvdata(struct device *dev , void *data ) ;
2240#line 891
2241extern int ( /* format attribute */  dev_err)(struct device  const  *dev , char const   *fmt 
2242                                              , ...) ;
2243#line 174 "include/linux/platform_device.h"
2244extern int platform_driver_register(struct platform_driver * ) ;
2245#line 175
2246extern void platform_driver_unregister(struct platform_driver * ) ;
2247#line 183
2248__inline static void *platform_get_drvdata(struct platform_device  const  *pdev )  __attribute__((__no_instrument_function__)) ;
2249#line 183 "include/linux/platform_device.h"
2250__inline static void *platform_get_drvdata(struct platform_device  const  *pdev ) 
2251{ void *tmp ;
2252  unsigned long __cil_tmp3 ;
2253  unsigned long __cil_tmp4 ;
2254  struct device  const  *__cil_tmp5 ;
2255
2256  {
2257  {
2258#line 185
2259  __cil_tmp3 = (unsigned long )pdev;
2260#line 185
2261  __cil_tmp4 = __cil_tmp3 + 16;
2262#line 185
2263  __cil_tmp5 = (struct device  const  *)__cil_tmp4;
2264#line 185
2265  tmp = dev_get_drvdata(__cil_tmp5);
2266  }
2267#line 185
2268  return (tmp);
2269}
2270}
2271#line 188
2272__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )  __attribute__((__no_instrument_function__)) ;
2273#line 188 "include/linux/platform_device.h"
2274__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) 
2275{ unsigned long __cil_tmp3 ;
2276  unsigned long __cil_tmp4 ;
2277  struct device *__cil_tmp5 ;
2278
2279  {
2280  {
2281#line 190
2282  __cil_tmp3 = (unsigned long )pdev;
2283#line 190
2284  __cil_tmp4 = __cil_tmp3 + 16;
2285#line 190
2286  __cil_tmp5 = (struct device *)__cil_tmp4;
2287#line 190
2288  dev_set_drvdata(__cil_tmp5, data);
2289  }
2290#line 191
2291  return;
2292}
2293}
2294#line 1502 "include/linux/input.h"
2295extern void input_event(struct input_dev *dev , unsigned int type , unsigned int code ,
2296                        int value ) ;
2297#line 1505
2298__inline static void input_report_key(struct input_dev *dev , unsigned int code ,
2299                                      int value )  __attribute__((__no_instrument_function__)) ;
2300#line 1505 "include/linux/input.h"
2301__inline static void input_report_key(struct input_dev *dev , unsigned int code ,
2302                                      int value ) 
2303{ int __cil_tmp4 ;
2304  int __cil_tmp5 ;
2305
2306  {
2307  {
2308#line 1507
2309  __cil_tmp4 = ! value;
2310#line 1507
2311  __cil_tmp5 = ! __cil_tmp4;
2312#line 1507
2313  input_event(dev, 1U, code, __cil_tmp5);
2314  }
2315#line 1508
2316  return;
2317}
2318}
2319#line 1510
2320__inline static void input_report_rel(struct input_dev *dev , unsigned int code ,
2321                                      int value )  __attribute__((__no_instrument_function__)) ;
2322#line 1510 "include/linux/input.h"
2323__inline static void input_report_rel(struct input_dev *dev , unsigned int code ,
2324                                      int value ) 
2325{ 
2326
2327  {
2328  {
2329#line 1512
2330  input_event(dev, 2U, code, value);
2331  }
2332#line 1513
2333  return;
2334}
2335}
2336#line 1530
2337__inline static void input_sync(struct input_dev *dev )  __attribute__((__no_instrument_function__)) ;
2338#line 1530 "include/linux/input.h"
2339__inline static void input_sync(struct input_dev *dev ) 
2340{ 
2341
2342  {
2343  {
2344#line 1532
2345  input_event(dev, 0U, 0U, 0);
2346  }
2347#line 1533
2348  return;
2349}
2350}
2351#line 1540
2352extern void input_set_capability(struct input_dev *dev , unsigned int type , unsigned int code ) ;
2353#line 53 "include/linux/input-polldev.h"
2354extern struct input_polled_dev *input_allocate_polled_device(void) ;
2355#line 54
2356extern void input_free_polled_device(struct input_polled_dev *dev ) ;
2357#line 55
2358extern int input_register_polled_device(struct input_polled_dev *dev ) ;
2359#line 56
2360extern void input_unregister_polled_device(struct input_polled_dev *dev ) ;
2361#line 153 "include/asm-generic/gpio.h"
2362extern int gpio_request(unsigned int gpio , char const   *label ) ;
2363#line 154
2364extern void gpio_free(unsigned int gpio ) ;
2365#line 156
2366extern int gpio_direction_input(unsigned int gpio ) ;
2367#line 169
2368extern int __gpio_get_value(unsigned int gpio ) ;
2369#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
2370__inline static int gpio_get_value(unsigned int gpio )  __attribute__((__no_instrument_function__)) ;
2371#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
2372__inline static int gpio_get_value(unsigned int gpio ) 
2373{ int tmp ;
2374
2375  {
2376  {
2377#line 28
2378  tmp = __gpio_get_value(gpio);
2379  }
2380#line 28
2381  return (tmp);
2382}
2383}
2384#line 24 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
2385static void gpio_mouse_scan(struct input_polled_dev *dev ) 
2386{ struct gpio_mouse_platform_data *gpio ;
2387  struct input_dev *input ;
2388  int x ;
2389  int y ;
2390  int tmp ;
2391  int tmp___0 ;
2392  int tmp___1 ;
2393  int tmp___2 ;
2394  int tmp___3 ;
2395  int tmp___4 ;
2396  int tmp___5 ;
2397  void *__cil_tmp13 ;
2398  unsigned long __cil_tmp14 ;
2399  unsigned long __cil_tmp15 ;
2400  unsigned long __cil_tmp16 ;
2401  unsigned long __cil_tmp17 ;
2402  unsigned long __cil_tmp18 ;
2403  unsigned long __cil_tmp19 ;
2404  int __cil_tmp20 ;
2405  unsigned long __cil_tmp21 ;
2406  unsigned long __cil_tmp22 ;
2407  unsigned long __cil_tmp23 ;
2408  unsigned long __cil_tmp24 ;
2409  int __cil_tmp25 ;
2410  unsigned int __cil_tmp26 ;
2411  unsigned long __cil_tmp27 ;
2412  unsigned long __cil_tmp28 ;
2413  int __cil_tmp29 ;
2414  int __cil_tmp30 ;
2415  unsigned long __cil_tmp31 ;
2416  unsigned long __cil_tmp32 ;
2417  unsigned long __cil_tmp33 ;
2418  unsigned long __cil_tmp34 ;
2419  int __cil_tmp35 ;
2420  unsigned long __cil_tmp36 ;
2421  unsigned long __cil_tmp37 ;
2422  unsigned long __cil_tmp38 ;
2423  unsigned long __cil_tmp39 ;
2424  int __cil_tmp40 ;
2425  unsigned int __cil_tmp41 ;
2426  unsigned long __cil_tmp42 ;
2427  unsigned long __cil_tmp43 ;
2428  int __cil_tmp44 ;
2429  int __cil_tmp45 ;
2430  unsigned long __cil_tmp46 ;
2431  unsigned long __cil_tmp47 ;
2432  unsigned long __cil_tmp48 ;
2433  unsigned long __cil_tmp49 ;
2434  int __cil_tmp50 ;
2435  unsigned long __cil_tmp51 ;
2436  unsigned long __cil_tmp52 ;
2437  unsigned long __cil_tmp53 ;
2438  unsigned long __cil_tmp54 ;
2439  int __cil_tmp55 ;
2440  unsigned int __cil_tmp56 ;
2441  unsigned long __cil_tmp57 ;
2442  unsigned long __cil_tmp58 ;
2443  int __cil_tmp59 ;
2444  int __cil_tmp60 ;
2445  unsigned long __cil_tmp61 ;
2446  unsigned long __cil_tmp62 ;
2447  unsigned long __cil_tmp63 ;
2448  unsigned long __cil_tmp64 ;
2449  int __cil_tmp65 ;
2450  unsigned int __cil_tmp66 ;
2451  unsigned long __cil_tmp67 ;
2452  unsigned long __cil_tmp68 ;
2453  unsigned long __cil_tmp69 ;
2454  unsigned long __cil_tmp70 ;
2455  int __cil_tmp71 ;
2456  unsigned int __cil_tmp72 ;
2457  unsigned long __cil_tmp73 ;
2458  unsigned long __cil_tmp74 ;
2459  int __cil_tmp75 ;
2460  int __cil_tmp76 ;
2461  unsigned long __cil_tmp77 ;
2462  unsigned long __cil_tmp78 ;
2463  int __cil_tmp79 ;
2464  int __cil_tmp80 ;
2465  unsigned long __cil_tmp81 ;
2466  unsigned long __cil_tmp82 ;
2467  unsigned long __cil_tmp83 ;
2468  unsigned long __cil_tmp84 ;
2469  int __cil_tmp85 ;
2470  unsigned int __cil_tmp86 ;
2471  unsigned long __cil_tmp87 ;
2472  unsigned long __cil_tmp88 ;
2473  int __cil_tmp89 ;
2474  unsigned int __cil_tmp90 ;
2475  unsigned long __cil_tmp91 ;
2476  unsigned long __cil_tmp92 ;
2477  int __cil_tmp93 ;
2478  int __cil_tmp94 ;
2479  unsigned long __cil_tmp95 ;
2480  unsigned long __cil_tmp96 ;
2481  int __cil_tmp97 ;
2482  int __cil_tmp98 ;
2483
2484  {
2485#line 26
2486  __cil_tmp13 = *((void **)dev);
2487#line 26
2488  gpio = (struct gpio_mouse_platform_data *)__cil_tmp13;
2489#line 27
2490  __cil_tmp14 = (unsigned long )dev;
2491#line 27
2492  __cil_tmp15 = __cil_tmp14 + 48;
2493#line 27
2494  input = *((struct input_dev **)__cil_tmp15);
2495  {
2496#line 30
2497  __cil_tmp16 = 0 + 16;
2498#line 30
2499  __cil_tmp17 = 8 + __cil_tmp16;
2500#line 30
2501  __cil_tmp18 = (unsigned long )gpio;
2502#line 30
2503  __cil_tmp19 = __cil_tmp18 + __cil_tmp17;
2504#line 30
2505  __cil_tmp20 = *((int *)__cil_tmp19);
2506#line 30
2507  if (__cil_tmp20 >= 0) {
2508    {
2509#line 31
2510    __cil_tmp21 = 0 + 16;
2511#line 31
2512    __cil_tmp22 = 8 + __cil_tmp21;
2513#line 31
2514    __cil_tmp23 = (unsigned long )gpio;
2515#line 31
2516    __cil_tmp24 = __cil_tmp23 + __cil_tmp22;
2517#line 31
2518    __cil_tmp25 = *((int *)__cil_tmp24);
2519#line 31
2520    __cil_tmp26 = (unsigned int )__cil_tmp25;
2521#line 31
2522    tmp = gpio_get_value(__cil_tmp26);
2523#line 31
2524    __cil_tmp27 = (unsigned long )gpio;
2525#line 31
2526    __cil_tmp28 = __cil_tmp27 + 4;
2527#line 31
2528    __cil_tmp29 = *((int *)__cil_tmp28);
2529#line 31
2530    __cil_tmp30 = tmp ^ __cil_tmp29;
2531#line 31
2532    input_report_key(input, 272U, __cil_tmp30);
2533    }
2534  } else {
2535
2536  }
2537  }
2538  {
2539#line 33
2540  __cil_tmp31 = 0 + 20;
2541#line 33
2542  __cil_tmp32 = 8 + __cil_tmp31;
2543#line 33
2544  __cil_tmp33 = (unsigned long )gpio;
2545#line 33
2546  __cil_tmp34 = __cil_tmp33 + __cil_tmp32;
2547#line 33
2548  __cil_tmp35 = *((int *)__cil_tmp34);
2549#line 33
2550  if (__cil_tmp35 >= 0) {
2551    {
2552#line 34
2553    __cil_tmp36 = 0 + 20;
2554#line 34
2555    __cil_tmp37 = 8 + __cil_tmp36;
2556#line 34
2557    __cil_tmp38 = (unsigned long )gpio;
2558#line 34
2559    __cil_tmp39 = __cil_tmp38 + __cil_tmp37;
2560#line 34
2561    __cil_tmp40 = *((int *)__cil_tmp39);
2562#line 34
2563    __cil_tmp41 = (unsigned int )__cil_tmp40;
2564#line 34
2565    tmp___0 = gpio_get_value(__cil_tmp41);
2566#line 34
2567    __cil_tmp42 = (unsigned long )gpio;
2568#line 34
2569    __cil_tmp43 = __cil_tmp42 + 4;
2570#line 34
2571    __cil_tmp44 = *((int *)__cil_tmp43);
2572#line 34
2573    __cil_tmp45 = tmp___0 ^ __cil_tmp44;
2574#line 34
2575    input_report_key(input, 274U, __cil_tmp45);
2576    }
2577  } else {
2578
2579  }
2580  }
2581  {
2582#line 36
2583  __cil_tmp46 = 0 + 24;
2584#line 36
2585  __cil_tmp47 = 8 + __cil_tmp46;
2586#line 36
2587  __cil_tmp48 = (unsigned long )gpio;
2588#line 36
2589  __cil_tmp49 = __cil_tmp48 + __cil_tmp47;
2590#line 36
2591  __cil_tmp50 = *((int *)__cil_tmp49);
2592#line 36
2593  if (__cil_tmp50 >= 0) {
2594    {
2595#line 37
2596    __cil_tmp51 = 0 + 24;
2597#line 37
2598    __cil_tmp52 = 8 + __cil_tmp51;
2599#line 37
2600    __cil_tmp53 = (unsigned long )gpio;
2601#line 37
2602    __cil_tmp54 = __cil_tmp53 + __cil_tmp52;
2603#line 37
2604    __cil_tmp55 = *((int *)__cil_tmp54);
2605#line 37
2606    __cil_tmp56 = (unsigned int )__cil_tmp55;
2607#line 37
2608    tmp___1 = gpio_get_value(__cil_tmp56);
2609#line 37
2610    __cil_tmp57 = (unsigned long )gpio;
2611#line 37
2612    __cil_tmp58 = __cil_tmp57 + 4;
2613#line 37
2614    __cil_tmp59 = *((int *)__cil_tmp58);
2615#line 37
2616    __cil_tmp60 = tmp___1 ^ __cil_tmp59;
2617#line 37
2618    input_report_key(input, 273U, __cil_tmp60);
2619    }
2620  } else {
2621
2622  }
2623  }
2624  {
2625#line 40
2626  __cil_tmp61 = 0 + 12;
2627#line 40
2628  __cil_tmp62 = 8 + __cil_tmp61;
2629#line 40
2630  __cil_tmp63 = (unsigned long )gpio;
2631#line 40
2632  __cil_tmp64 = __cil_tmp63 + __cil_tmp62;
2633#line 40
2634  __cil_tmp65 = *((int *)__cil_tmp64);
2635#line 40
2636  __cil_tmp66 = (unsigned int )__cil_tmp65;
2637#line 40
2638  tmp___2 = gpio_get_value(__cil_tmp66);
2639#line 40
2640  __cil_tmp67 = 0 + 8;
2641#line 40
2642  __cil_tmp68 = 8 + __cil_tmp67;
2643#line 40
2644  __cil_tmp69 = (unsigned long )gpio;
2645#line 40
2646  __cil_tmp70 = __cil_tmp69 + __cil_tmp68;
2647#line 40
2648  __cil_tmp71 = *((int *)__cil_tmp70);
2649#line 40
2650  __cil_tmp72 = (unsigned int )__cil_tmp71;
2651#line 40
2652  tmp___3 = gpio_get_value(__cil_tmp72);
2653#line 40
2654  __cil_tmp73 = (unsigned long )gpio;
2655#line 40
2656  __cil_tmp74 = __cil_tmp73 + 4;
2657#line 40
2658  __cil_tmp75 = *((int *)__cil_tmp74);
2659#line 40
2660  __cil_tmp76 = tmp___3 ^ __cil_tmp75;
2661#line 40
2662  __cil_tmp77 = (unsigned long )gpio;
2663#line 40
2664  __cil_tmp78 = __cil_tmp77 + 4;
2665#line 40
2666  __cil_tmp79 = *((int *)__cil_tmp78);
2667#line 40
2668  __cil_tmp80 = tmp___2 ^ __cil_tmp79;
2669#line 40
2670  x = __cil_tmp80 - __cil_tmp76;
2671#line 42
2672  __cil_tmp81 = 0 + 4;
2673#line 42
2674  __cil_tmp82 = 8 + __cil_tmp81;
2675#line 42
2676  __cil_tmp83 = (unsigned long )gpio;
2677#line 42
2678  __cil_tmp84 = __cil_tmp83 + __cil_tmp82;
2679#line 42
2680  __cil_tmp85 = *((int *)__cil_tmp84);
2681#line 42
2682  __cil_tmp86 = (unsigned int )__cil_tmp85;
2683#line 42
2684  tmp___4 = gpio_get_value(__cil_tmp86);
2685#line 42
2686  __cil_tmp87 = (unsigned long )gpio;
2687#line 42
2688  __cil_tmp88 = __cil_tmp87 + 8;
2689#line 42
2690  __cil_tmp89 = *((int *)__cil_tmp88);
2691#line 42
2692  __cil_tmp90 = (unsigned int )__cil_tmp89;
2693#line 42
2694  tmp___5 = gpio_get_value(__cil_tmp90);
2695#line 42
2696  __cil_tmp91 = (unsigned long )gpio;
2697#line 42
2698  __cil_tmp92 = __cil_tmp91 + 4;
2699#line 42
2700  __cil_tmp93 = *((int *)__cil_tmp92);
2701#line 42
2702  __cil_tmp94 = tmp___5 ^ __cil_tmp93;
2703#line 42
2704  __cil_tmp95 = (unsigned long )gpio;
2705#line 42
2706  __cil_tmp96 = __cil_tmp95 + 4;
2707#line 42
2708  __cil_tmp97 = *((int *)__cil_tmp96);
2709#line 42
2710  __cil_tmp98 = tmp___4 ^ __cil_tmp97;
2711#line 42
2712  y = __cil_tmp98 - __cil_tmp94;
2713#line 45
2714  input_report_rel(input, 0U, x);
2715#line 46
2716  input_report_rel(input, 1U, y);
2717#line 47
2718  input_sync(input);
2719  }
2720#line 48
2721  return;
2722}
2723}
2724#line 84
2725static int gpio_mouse_probe(struct platform_device *pdev )  __attribute__((__section__(".devinit.text"),
2726__no_instrument_function__)) ;
2727#line 84 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
2728static struct _ddebug  __attribute__((__aligned__(8))) descriptor  __attribute__((__used__,
2729__section__("__verbose")))  =    {"gpio_mouse", "gpio_mouse_probe", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c",
2730    "no left button defined\n", 84U, 0U};
2731#line 132
2732static int gpio_mouse_probe(struct platform_device *pdev )  __attribute__((__section__(".devinit.text"),
2733__no_instrument_function__)) ;
2734#line 132 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
2735static struct _ddebug  __attribute__((__aligned__(8))) descriptor___0  __attribute__((__used__,
2736__section__("__verbose")))  =    {"gpio_mouse", "gpio_mouse_probe", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c",
2737    "%d ms scan time, buttons: %s%s%s\n", 136U, 0U};
2738#line 50
2739static int gpio_mouse_probe(struct platform_device *pdev )  __attribute__((__section__(".devinit.text"),
2740__no_instrument_function__)) ;
2741#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
2742static int gpio_mouse_probe(struct platform_device *pdev ) 
2743{ struct gpio_mouse_platform_data *pdata ;
2744  struct input_polled_dev *input_poll ;
2745  struct input_dev *input ;
2746  int pin ;
2747  int i ;
2748  int error ;
2749  long tmp ;
2750  char const   *tmp___0 ;
2751  char const   *tmp___1 ;
2752  char const   *tmp___2 ;
2753  long tmp___3 ;
2754  unsigned long __cil_tmp13 ;
2755  unsigned long __cil_tmp14 ;
2756  unsigned long __cil_tmp15 ;
2757  void *__cil_tmp16 ;
2758  unsigned long __cil_tmp17 ;
2759  unsigned long __cil_tmp18 ;
2760  struct device *__cil_tmp19 ;
2761  struct device  const  *__cil_tmp20 ;
2762  int __cil_tmp21 ;
2763  unsigned long __cil_tmp22 ;
2764  unsigned long __cil_tmp23 ;
2765  struct device *__cil_tmp24 ;
2766  struct device  const  *__cil_tmp25 ;
2767  unsigned long __cil_tmp26 ;
2768  unsigned long __cil_tmp27 ;
2769  unsigned long __cil_tmp28 ;
2770  unsigned long __cil_tmp29 ;
2771  unsigned long __cil_tmp30 ;
2772  unsigned long __cil_tmp31 ;
2773  unsigned long __cil_tmp32 ;
2774  struct device *__cil_tmp33 ;
2775  struct device  const  *__cil_tmp34 ;
2776  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp35 ;
2777  unsigned int __cil_tmp36 ;
2778  unsigned int __cil_tmp37 ;
2779  int __cil_tmp38 ;
2780  int __cil_tmp39 ;
2781  long __cil_tmp40 ;
2782  unsigned long __cil_tmp41 ;
2783  unsigned long __cil_tmp42 ;
2784  struct device *__cil_tmp43 ;
2785  struct device  const  *__cil_tmp44 ;
2786  unsigned int __cil_tmp45 ;
2787  unsigned long __cil_tmp46 ;
2788  unsigned long __cil_tmp47 ;
2789  struct device *__cil_tmp48 ;
2790  struct device  const  *__cil_tmp49 ;
2791  unsigned int __cil_tmp50 ;
2792  unsigned long __cil_tmp51 ;
2793  unsigned long __cil_tmp52 ;
2794  struct device *__cil_tmp53 ;
2795  struct device  const  *__cil_tmp54 ;
2796  void *__cil_tmp55 ;
2797  unsigned long __cil_tmp56 ;
2798  unsigned long __cil_tmp57 ;
2799  unsigned long __cil_tmp58 ;
2800  unsigned long __cil_tmp59 ;
2801  int __cil_tmp60 ;
2802  unsigned long __cil_tmp61 ;
2803  unsigned long __cil_tmp62 ;
2804  unsigned long __cil_tmp63 ;
2805  unsigned long __cil_tmp64 ;
2806  unsigned long __cil_tmp65 ;
2807  unsigned long __cil_tmp66 ;
2808  unsigned long __cil_tmp67 ;
2809  unsigned long __cil_tmp68 ;
2810  unsigned long __cil_tmp69 ;
2811  unsigned long __cil_tmp70 ;
2812  unsigned long __cil_tmp71 ;
2813  unsigned long __cil_tmp72 ;
2814  int __cil_tmp73 ;
2815  unsigned long __cil_tmp74 ;
2816  unsigned long __cil_tmp75 ;
2817  unsigned long __cil_tmp76 ;
2818  unsigned long __cil_tmp77 ;
2819  int __cil_tmp78 ;
2820  unsigned long __cil_tmp79 ;
2821  unsigned long __cil_tmp80 ;
2822  unsigned long __cil_tmp81 ;
2823  unsigned long __cil_tmp82 ;
2824  int __cil_tmp83 ;
2825  unsigned long __cil_tmp84 ;
2826  unsigned long __cil_tmp85 ;
2827  struct device *__cil_tmp86 ;
2828  struct device  const  *__cil_tmp87 ;
2829  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp88 ;
2830  unsigned int __cil_tmp89 ;
2831  unsigned int __cil_tmp90 ;
2832  int __cil_tmp91 ;
2833  int __cil_tmp92 ;
2834  long __cil_tmp93 ;
2835  unsigned long __cil_tmp94 ;
2836  unsigned long __cil_tmp95 ;
2837  unsigned long __cil_tmp96 ;
2838  unsigned long __cil_tmp97 ;
2839  int __cil_tmp98 ;
2840  unsigned long __cil_tmp99 ;
2841  unsigned long __cil_tmp100 ;
2842  unsigned long __cil_tmp101 ;
2843  unsigned long __cil_tmp102 ;
2844  int __cil_tmp103 ;
2845  unsigned long __cil_tmp104 ;
2846  unsigned long __cil_tmp105 ;
2847  unsigned long __cil_tmp106 ;
2848  unsigned long __cil_tmp107 ;
2849  int __cil_tmp108 ;
2850  unsigned long __cil_tmp109 ;
2851  unsigned long __cil_tmp110 ;
2852  struct device *__cil_tmp111 ;
2853  struct device  const  *__cil_tmp112 ;
2854  int __cil_tmp113 ;
2855  void *__cil_tmp114 ;
2856  unsigned long __cil_tmp115 ;
2857  unsigned long __cil_tmp116 ;
2858  unsigned long __cil_tmp117 ;
2859  unsigned long __cil_tmp118 ;
2860  unsigned long __cil_tmp119 ;
2861  unsigned int __cil_tmp120 ;
2862
2863  {
2864#line 52
2865  __cil_tmp13 = 16 + 184;
2866#line 52
2867  __cil_tmp14 = (unsigned long )pdev;
2868#line 52
2869  __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
2870#line 52
2871  __cil_tmp16 = *((void **)__cil_tmp15);
2872#line 52
2873  pdata = (struct gpio_mouse_platform_data *)__cil_tmp16;
2874#line 58
2875  if (! pdata) {
2876    {
2877#line 59
2878    __cil_tmp17 = (unsigned long )pdev;
2879#line 59
2880    __cil_tmp18 = __cil_tmp17 + 16;
2881#line 59
2882    __cil_tmp19 = (struct device *)__cil_tmp18;
2883#line 59
2884    __cil_tmp20 = (struct device  const  *)__cil_tmp19;
2885#line 59
2886    dev_err(__cil_tmp20, "no platform data\n");
2887#line 60
2888    error = -6;
2889    }
2890#line 61
2891    goto out;
2892  } else {
2893
2894  }
2895  {
2896#line 64
2897  __cil_tmp21 = *((int *)pdata);
2898#line 64
2899  if (__cil_tmp21 < 0) {
2900    {
2901#line 65
2902    __cil_tmp22 = (unsigned long )pdev;
2903#line 65
2904    __cil_tmp23 = __cil_tmp22 + 16;
2905#line 65
2906    __cil_tmp24 = (struct device *)__cil_tmp23;
2907#line 65
2908    __cil_tmp25 = (struct device  const  *)__cil_tmp24;
2909#line 65
2910    dev_err(__cil_tmp25, "invalid scan time\n");
2911#line 66
2912    error = -22;
2913    }
2914#line 67
2915    goto out;
2916  } else {
2917
2918  }
2919  }
2920#line 70
2921  i = 0;
2922  {
2923#line 70
2924  while (1) {
2925    while_continue: /* CIL Label */ ;
2926#line 70
2927    if (i < 7) {
2928
2929    } else {
2930#line 70
2931      goto while_break;
2932    }
2933#line 71
2934    __cil_tmp26 = i * 4UL;
2935#line 71
2936    __cil_tmp27 = 0 + __cil_tmp26;
2937#line 71
2938    __cil_tmp28 = 8 + __cil_tmp27;
2939#line 71
2940    __cil_tmp29 = (unsigned long )pdata;
2941#line 71
2942    __cil_tmp30 = __cil_tmp29 + __cil_tmp28;
2943#line 71
2944    pin = *((int *)__cil_tmp30);
2945#line 73
2946    if (pin < 0) {
2947#line 75
2948      if (i <= 3) {
2949        {
2950#line 77
2951        __cil_tmp31 = (unsigned long )pdev;
2952#line 77
2953        __cil_tmp32 = __cil_tmp31 + 16;
2954#line 77
2955        __cil_tmp33 = (struct device *)__cil_tmp32;
2956#line 77
2957        __cil_tmp34 = (struct device  const  *)__cil_tmp33;
2958#line 77
2959        dev_err(__cil_tmp34, "missing GPIO for directions\n");
2960#line 79
2961        error = -22;
2962        }
2963#line 80
2964        goto out_free_gpios;
2965      } else {
2966
2967      }
2968#line 83
2969      if (i == 4) {
2970        {
2971#line 84
2972        while (1) {
2973          while_continue___0: /* CIL Label */ ;
2974          {
2975#line 84
2976          while (1) {
2977            while_continue___1: /* CIL Label */ ;
2978            {
2979#line 84
2980            __cil_tmp35 = & descriptor;
2981#line 84
2982            __cil_tmp36 = __cil_tmp35->flags;
2983#line 84
2984            __cil_tmp37 = __cil_tmp36 & 1U;
2985#line 84
2986            __cil_tmp38 = ! __cil_tmp37;
2987#line 84
2988            __cil_tmp39 = ! __cil_tmp38;
2989#line 84
2990            __cil_tmp40 = (long )__cil_tmp39;
2991#line 84
2992            tmp = __builtin_expect(__cil_tmp40, 0L);
2993            }
2994#line 84
2995            if (tmp) {
2996              {
2997#line 84
2998              __cil_tmp41 = (unsigned long )pdev;
2999#line 84
3000              __cil_tmp42 = __cil_tmp41 + 16;
3001#line 84
3002              __cil_tmp43 = (struct device *)__cil_tmp42;
3003#line 84
3004              __cil_tmp44 = (struct device  const  *)__cil_tmp43;
3005#line 84
3006              __dynamic_dev_dbg(& descriptor, __cil_tmp44, "no left button defined\n");
3007              }
3008            } else {
3009
3010            }
3011#line 84
3012            goto while_break___1;
3013          }
3014          while_break___1: /* CIL Label */ ;
3015          }
3016#line 84
3017          goto while_break___0;
3018        }
3019        while_break___0: /* CIL Label */ ;
3020        }
3021      } else {
3022
3023      }
3024    } else {
3025      {
3026#line 87
3027      __cil_tmp45 = (unsigned int )pin;
3028#line 87
3029      error = gpio_request(__cil_tmp45, "gpio_mouse");
3030      }
3031#line 88
3032      if (error) {
3033        {
3034#line 89
3035        __cil_tmp46 = (unsigned long )pdev;
3036#line 89
3037        __cil_tmp47 = __cil_tmp46 + 16;
3038#line 89
3039        __cil_tmp48 = (struct device *)__cil_tmp47;
3040#line 89
3041        __cil_tmp49 = (struct device  const  *)__cil_tmp48;
3042#line 89
3043        dev_err(__cil_tmp49, "fail %d pin (%d idx)\n", pin, i);
3044        }
3045#line 91
3046        goto out_free_gpios;
3047      } else {
3048
3049      }
3050      {
3051#line 94
3052      __cil_tmp50 = (unsigned int )pin;
3053#line 94
3054      gpio_direction_input(__cil_tmp50);
3055      }
3056    }
3057#line 70
3058    i = i + 1;
3059  }
3060  while_break: /* CIL Label */ ;
3061  }
3062  {
3063#line 98
3064  input_poll = input_allocate_polled_device();
3065  }
3066#line 99
3067  if (! input_poll) {
3068    {
3069#line 100
3070    __cil_tmp51 = (unsigned long )pdev;
3071#line 100
3072    __cil_tmp52 = __cil_tmp51 + 16;
3073#line 100
3074    __cil_tmp53 = (struct device *)__cil_tmp52;
3075#line 100
3076    __cil_tmp54 = (struct device  const  *)__cil_tmp53;
3077#line 100
3078    dev_err(__cil_tmp54, "not enough memory for input device\n");
3079#line 101
3080    error = -12;
3081    }
3082#line 102
3083    goto out_free_gpios;
3084  } else {
3085
3086  }
3087  {
3088#line 105
3089  __cil_tmp55 = (void *)input_poll;
3090#line 105
3091  platform_set_drvdata(pdev, __cil_tmp55);
3092#line 108
3093  *((void **)input_poll) = (void *)pdata;
3094#line 109
3095  __cil_tmp56 = (unsigned long )input_poll;
3096#line 109
3097  __cil_tmp57 = __cil_tmp56 + 24;
3098#line 109
3099  *((void (**)(struct input_polled_dev *dev ))__cil_tmp57) = & gpio_mouse_scan;
3100#line 110
3101  __cil_tmp58 = (unsigned long )input_poll;
3102#line 110
3103  __cil_tmp59 = __cil_tmp58 + 32;
3104#line 110
3105  __cil_tmp60 = *((int *)pdata);
3106#line 110
3107  *((unsigned int *)__cil_tmp59) = (unsigned int )__cil_tmp60;
3108#line 112
3109  __cil_tmp61 = (unsigned long )input_poll;
3110#line 112
3111  __cil_tmp62 = __cil_tmp61 + 48;
3112#line 112
3113  input = *((struct input_dev **)__cil_tmp62);
3114#line 113
3115  *((char const   **)input) = *((char const   **)pdev);
3116#line 114
3117  __cil_tmp63 = (unsigned long )input;
3118#line 114
3119  __cil_tmp64 = __cil_tmp63 + 24;
3120#line 114
3121  *((__u16 *)__cil_tmp64) = (__u16 )25;
3122#line 115
3123  __cil_tmp65 = (unsigned long )input;
3124#line 115
3125  __cil_tmp66 = __cil_tmp65 + 648;
3126#line 115
3127  __cil_tmp67 = (unsigned long )pdev;
3128#line 115
3129  __cil_tmp68 = __cil_tmp67 + 16;
3130#line 115
3131  *((struct device **)__cil_tmp66) = (struct device *)__cil_tmp68;
3132#line 117
3133  input_set_capability(input, 2U, 0U);
3134#line 118
3135  input_set_capability(input, 2U, 1U);
3136  }
3137  {
3138#line 119
3139  __cil_tmp69 = 0 + 16;
3140#line 119
3141  __cil_tmp70 = 8 + __cil_tmp69;
3142#line 119
3143  __cil_tmp71 = (unsigned long )pdata;
3144#line 119
3145  __cil_tmp72 = __cil_tmp71 + __cil_tmp70;
3146#line 119
3147  __cil_tmp73 = *((int *)__cil_tmp72);
3148#line 119
3149  if (__cil_tmp73 >= 0) {
3150    {
3151#line 120
3152    input_set_capability(input, 1U, 272U);
3153    }
3154  } else {
3155
3156  }
3157  }
3158  {
3159#line 121
3160  __cil_tmp74 = 0 + 20;
3161#line 121
3162  __cil_tmp75 = 8 + __cil_tmp74;
3163#line 121
3164  __cil_tmp76 = (unsigned long )pdata;
3165#line 121
3166  __cil_tmp77 = __cil_tmp76 + __cil_tmp75;
3167#line 121
3168  __cil_tmp78 = *((int *)__cil_tmp77);
3169#line 121
3170  if (__cil_tmp78 >= 0) {
3171    {
3172#line 122
3173    input_set_capability(input, 1U, 274U);
3174    }
3175  } else {
3176
3177  }
3178  }
3179  {
3180#line 123
3181  __cil_tmp79 = 0 + 24;
3182#line 123
3183  __cil_tmp80 = 8 + __cil_tmp79;
3184#line 123
3185  __cil_tmp81 = (unsigned long )pdata;
3186#line 123
3187  __cil_tmp82 = __cil_tmp81 + __cil_tmp80;
3188#line 123
3189  __cil_tmp83 = *((int *)__cil_tmp82);
3190#line 123
3191  if (__cil_tmp83 >= 0) {
3192    {
3193#line 124
3194    input_set_capability(input, 1U, 273U);
3195    }
3196  } else {
3197
3198  }
3199  }
3200  {
3201#line 126
3202  error = input_register_polled_device(input_poll);
3203  }
3204#line 127
3205  if (error) {
3206    {
3207#line 128
3208    __cil_tmp84 = (unsigned long )pdev;
3209#line 128
3210    __cil_tmp85 = __cil_tmp84 + 16;
3211#line 128
3212    __cil_tmp86 = (struct device *)__cil_tmp85;
3213#line 128
3214    __cil_tmp87 = (struct device  const  *)__cil_tmp86;
3215#line 128
3216    dev_err(__cil_tmp87, "could not register input device\n");
3217    }
3218#line 129
3219    goto out_free_polldev;
3220  } else {
3221
3222  }
3223  {
3224#line 132
3225  while (1) {
3226    while_continue___2: /* CIL Label */ ;
3227    {
3228#line 132
3229    while (1) {
3230      while_continue___3: /* CIL Label */ ;
3231      {
3232#line 132
3233      __cil_tmp88 = & descriptor___0;
3234#line 132
3235      __cil_tmp89 = __cil_tmp88->flags;
3236#line 132
3237      __cil_tmp90 = __cil_tmp89 & 1U;
3238#line 132
3239      __cil_tmp91 = ! __cil_tmp90;
3240#line 132
3241      __cil_tmp92 = ! __cil_tmp91;
3242#line 132
3243      __cil_tmp93 = (long )__cil_tmp92;
3244#line 132
3245      tmp___3 = __builtin_expect(__cil_tmp93, 0L);
3246      }
3247#line 132
3248      if (tmp___3) {
3249        {
3250#line 132
3251        __cil_tmp94 = 0 + 24;
3252#line 132
3253        __cil_tmp95 = 8 + __cil_tmp94;
3254#line 132
3255        __cil_tmp96 = (unsigned long )pdata;
3256#line 132
3257        __cil_tmp97 = __cil_tmp96 + __cil_tmp95;
3258#line 132
3259        __cil_tmp98 = *((int *)__cil_tmp97);
3260#line 132
3261        if (__cil_tmp98 < 0) {
3262#line 132
3263          tmp___0 = "";
3264        } else {
3265#line 132
3266          tmp___0 = "right";
3267        }
3268        }
3269        {
3270#line 132
3271        __cil_tmp99 = 0 + 20;
3272#line 132
3273        __cil_tmp100 = 8 + __cil_tmp99;
3274#line 132
3275        __cil_tmp101 = (unsigned long )pdata;
3276#line 132
3277        __cil_tmp102 = __cil_tmp101 + __cil_tmp100;
3278#line 132
3279        __cil_tmp103 = *((int *)__cil_tmp102);
3280#line 132
3281        if (__cil_tmp103 < 0) {
3282#line 132
3283          tmp___1 = "";
3284        } else {
3285#line 132
3286          tmp___1 = "middle ";
3287        }
3288        }
3289        {
3290#line 132
3291        __cil_tmp104 = 0 + 16;
3292#line 132
3293        __cil_tmp105 = 8 + __cil_tmp104;
3294#line 132
3295        __cil_tmp106 = (unsigned long )pdata;
3296#line 132
3297        __cil_tmp107 = __cil_tmp106 + __cil_tmp105;
3298#line 132
3299        __cil_tmp108 = *((int *)__cil_tmp107);
3300#line 132
3301        if (__cil_tmp108 < 0) {
3302#line 132
3303          tmp___2 = "";
3304        } else {
3305#line 132
3306          tmp___2 = "left ";
3307        }
3308        }
3309        {
3310#line 132
3311        __cil_tmp109 = (unsigned long )pdev;
3312#line 132
3313        __cil_tmp110 = __cil_tmp109 + 16;
3314#line 132
3315        __cil_tmp111 = (struct device *)__cil_tmp110;
3316#line 132
3317        __cil_tmp112 = (struct device  const  *)__cil_tmp111;
3318#line 132
3319        __cil_tmp113 = *((int *)pdata);
3320#line 132
3321        __dynamic_dev_dbg(& descriptor___0, __cil_tmp112, "%d ms scan time, buttons: %s%s%s\n",
3322                          __cil_tmp113, tmp___2, tmp___1, tmp___0);
3323        }
3324      } else {
3325
3326      }
3327#line 132
3328      goto while_break___3;
3329    }
3330    while_break___3: /* CIL Label */ ;
3331    }
3332#line 132
3333    goto while_break___2;
3334  }
3335  while_break___2: /* CIL Label */ ;
3336  }
3337#line 138
3338  return (0);
3339  out_free_polldev: 
3340  {
3341#line 141
3342  input_free_polled_device(input_poll);
3343#line 142
3344  __cil_tmp114 = (void *)0;
3345#line 142
3346  platform_set_drvdata(pdev, __cil_tmp114);
3347  }
3348  out_free_gpios: 
3349  {
3350#line 145
3351  while (1) {
3352    while_continue___4: /* CIL Label */ ;
3353#line 145
3354    i = i - 1;
3355#line 145
3356    if (i >= 0) {
3357
3358    } else {
3359#line 145
3360      goto while_break___4;
3361    }
3362#line 146
3363    __cil_tmp115 = i * 4UL;
3364#line 146
3365    __cil_tmp116 = 0 + __cil_tmp115;
3366#line 146
3367    __cil_tmp117 = 8 + __cil_tmp116;
3368#line 146
3369    __cil_tmp118 = (unsigned long )pdata;
3370#line 146
3371    __cil_tmp119 = __cil_tmp118 + __cil_tmp117;
3372#line 146
3373    pin = *((int *)__cil_tmp119);
3374#line 147
3375    if (pin) {
3376      {
3377#line 148
3378      __cil_tmp120 = (unsigned int )pin;
3379#line 148
3380      gpio_free(__cil_tmp120);
3381      }
3382    } else {
3383
3384    }
3385  }
3386  while_break___4: /* CIL Label */ ;
3387  }
3388  out: 
3389#line 151
3390  return (error);
3391}
3392}
3393#line 154
3394static int gpio_mouse_remove(struct platform_device *pdev )  __attribute__((__section__(".devexit.text"),
3395__no_instrument_function__)) ;
3396#line 154 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3397static int gpio_mouse_remove(struct platform_device *pdev ) 
3398{ struct input_polled_dev *input ;
3399  void *tmp ;
3400  struct gpio_mouse_platform_data *pdata ;
3401  int pin ;
3402  int i ;
3403  struct platform_device  const  *__cil_tmp7 ;
3404  void *__cil_tmp8 ;
3405  unsigned long __cil_tmp9 ;
3406  unsigned long __cil_tmp10 ;
3407  unsigned long __cil_tmp11 ;
3408  unsigned long __cil_tmp12 ;
3409  unsigned long __cil_tmp13 ;
3410  unsigned int __cil_tmp14 ;
3411  void *__cil_tmp15 ;
3412
3413  {
3414  {
3415#line 156
3416  __cil_tmp7 = (struct platform_device  const  *)pdev;
3417#line 156
3418  tmp = platform_get_drvdata(__cil_tmp7);
3419#line 156
3420  input = (struct input_polled_dev *)tmp;
3421#line 157
3422  __cil_tmp8 = *((void **)input);
3423#line 157
3424  pdata = (struct gpio_mouse_platform_data *)__cil_tmp8;
3425#line 160
3426  input_unregister_polled_device(input);
3427#line 161
3428  input_free_polled_device(input);
3429#line 163
3430  i = 0;
3431  }
3432  {
3433#line 163
3434  while (1) {
3435    while_continue: /* CIL Label */ ;
3436#line 163
3437    if (i < 7) {
3438
3439    } else {
3440#line 163
3441      goto while_break;
3442    }
3443#line 164
3444    __cil_tmp9 = i * 4UL;
3445#line 164
3446    __cil_tmp10 = 0 + __cil_tmp9;
3447#line 164
3448    __cil_tmp11 = 8 + __cil_tmp10;
3449#line 164
3450    __cil_tmp12 = (unsigned long )pdata;
3451#line 164
3452    __cil_tmp13 = __cil_tmp12 + __cil_tmp11;
3453#line 164
3454    pin = *((int *)__cil_tmp13);
3455#line 165
3456    if (pin >= 0) {
3457      {
3458#line 166
3459      __cil_tmp14 = (unsigned int )pin;
3460#line 166
3461      gpio_free(__cil_tmp14);
3462      }
3463    } else {
3464
3465    }
3466#line 163
3467    i = i + 1;
3468  }
3469  while_break: /* CIL Label */ ;
3470  }
3471  {
3472#line 169
3473  __cil_tmp15 = (void *)0;
3474#line 169
3475  platform_set_drvdata(pdev, __cil_tmp15);
3476  }
3477#line 171
3478  return (0);
3479}
3480}
3481#line 174 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3482static struct platform_driver gpio_mouse_device_driver  =    {& gpio_mouse_probe, & gpio_mouse_remove, (void (*)(struct platform_device * ))0,
3483    (int (*)(struct platform_device * , pm_message_t state ))0, (int (*)(struct platform_device * ))0,
3484    {"gpio_mouse", (struct bus_type *)0, & __this_module, (char const   *)0, (_Bool)0,
3485     (struct of_device_id  const  *)0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
3486     (void (*)(struct device *dev ))0, (int (*)(struct device *dev , pm_message_t state ))0,
3487     (int (*)(struct device *dev ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
3488     (struct driver_private *)0}, (struct platform_device_id  const  *)0};
3489#line 182
3490static int gpio_mouse_device_driver_init(void)  __attribute__((__section__(".init.text"),
3491__no_instrument_function__)) ;
3492#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3493static int gpio_mouse_device_driver_init(void) 
3494{ int tmp ;
3495
3496  {
3497  {
3498#line 182
3499  tmp = platform_driver_register(& gpio_mouse_device_driver);
3500  }
3501#line 182
3502  return (tmp);
3503}
3504}
3505#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3506int init_module(void) 
3507{ int tmp ;
3508
3509  {
3510  {
3511#line 182
3512  tmp = gpio_mouse_device_driver_init();
3513  }
3514#line 182
3515  return (tmp);
3516}
3517}
3518#line 182
3519static void gpio_mouse_device_driver_exit(void)  __attribute__((__section__(".exit.text"),
3520__no_instrument_function__)) ;
3521#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3522static void gpio_mouse_device_driver_exit(void) 
3523{ 
3524
3525  {
3526  {
3527#line 182
3528  platform_driver_unregister(& gpio_mouse_device_driver);
3529  }
3530#line 182
3531  return;
3532}
3533}
3534#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3535void cleanup_module(void) 
3536{ 
3537
3538  {
3539  {
3540#line 182
3541  gpio_mouse_device_driver_exit();
3542  }
3543#line 182
3544  return;
3545}
3546}
3547#line 184 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3548static char const   __mod_author184[53]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3549__aligned__(1)))  = 
3550#line 184
3551  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
3552        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'H', 
3553        (char const   )'a',      (char const   )'n',      (char const   )'s',      (char const   )'-', 
3554        (char const   )'C',      (char const   )'h',      (char const   )'r',      (char const   )'i', 
3555        (char const   )'s',      (char const   )'t',      (char const   )'i',      (char const   )'a', 
3556        (char const   )'n',      (char const   )' ',      (char const   )'E',      (char const   )'g', 
3557        (char const   )'t',      (char const   )'v',      (char const   )'e',      (char const   )'d', 
3558        (char const   )'t',      (char const   )' ',      (char const   )'<',      (char const   )'e', 
3559        (char const   )'g',      (char const   )'t',      (char const   )'v',      (char const   )'e', 
3560        (char const   )'d',      (char const   )'t',      (char const   )'@',      (char const   )'s', 
3561        (char const   )'a',      (char const   )'m',      (char const   )'f',      (char const   )'u', 
3562        (char const   )'n',      (char const   )'d',      (char const   )'e',      (char const   )'t', 
3563        (char const   )'.',      (char const   )'n',      (char const   )'o',      (char const   )'>', 
3564        (char const   )'\000'};
3565#line 185 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3566static char const   __mod_description185[30]  __attribute__((__used__, __unused__,
3567__section__(".modinfo"), __aligned__(1)))  = 
3568#line 185
3569  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
3570        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
3571        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
3572        (char const   )'G',      (char const   )'P',      (char const   )'I',      (char const   )'O', 
3573        (char const   )' ',      (char const   )'m',      (char const   )'o',      (char const   )'u', 
3574        (char const   )'s',      (char const   )'e',      (char const   )' ',      (char const   )'d', 
3575        (char const   )'r',      (char const   )'i',      (char const   )'v',      (char const   )'e', 
3576        (char const   )'r',      (char const   )'\000'};
3577#line 186 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3578static char const   __mod_license186[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3579__aligned__(1)))  = 
3580#line 186
3581  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
3582        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
3583        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
3584#line 187 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3585static char const   __mod_alias187[26]  __attribute__((__used__, __unused__, __section__(".modinfo"),
3586__aligned__(1)))  = 
3587#line 187
3588  {      (char const   )'a',      (char const   )'l',      (char const   )'i',      (char const   )'a', 
3589        (char const   )'s',      (char const   )'=',      (char const   )'p',      (char const   )'l', 
3590        (char const   )'a',      (char const   )'t',      (char const   )'f',      (char const   )'o', 
3591        (char const   )'r',      (char const   )'m',      (char const   )':',      (char const   )'g', 
3592        (char const   )'p',      (char const   )'i',      (char const   )'o',      (char const   )'_', 
3593        (char const   )'m',      (char const   )'o',      (char const   )'u',      (char const   )'s', 
3594        (char const   )'e',      (char const   )'\000'};
3595#line 206
3596void ldv_check_final_state(void) ;
3597#line 209
3598extern void ldv_check_return_value(int res ) ;
3599#line 212
3600extern void ldv_initialize(void) ;
3601#line 215
3602extern int __VERIFIER_nondet_int(void) ;
3603#line 218 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3604int LDV_IN_INTERRUPT  ;
3605#line 233 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3606static int res_gpio_mouse_probe_1  ;
3607#line 221 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3608void main(void) 
3609{ struct platform_device *var_group1 ;
3610  int ldv_s_gpio_mouse_device_driver_platform_driver ;
3611  int tmp ;
3612  int tmp___0 ;
3613  int __cil_tmp5 ;
3614
3615  {
3616  {
3617#line 241
3618  LDV_IN_INTERRUPT = 1;
3619#line 250
3620  ldv_initialize();
3621#line 251
3622  ldv_s_gpio_mouse_device_driver_platform_driver = 0;
3623  }
3624  {
3625#line 254
3626  while (1) {
3627    while_continue: /* CIL Label */ ;
3628    {
3629#line 254
3630    tmp___0 = __VERIFIER_nondet_int();
3631    }
3632#line 254
3633    if (tmp___0) {
3634
3635    } else {
3636      {
3637#line 254
3638      __cil_tmp5 = ldv_s_gpio_mouse_device_driver_platform_driver == 0;
3639#line 254
3640      if (! __cil_tmp5) {
3641
3642      } else {
3643#line 254
3644        goto while_break;
3645      }
3646      }
3647    }
3648    {
3649#line 258
3650    tmp = __VERIFIER_nondet_int();
3651    }
3652#line 260
3653    if (tmp == 0) {
3654#line 260
3655      goto case_0;
3656    } else {
3657      {
3658#line 279
3659      goto switch_default;
3660#line 258
3661      if (0) {
3662        case_0: /* CIL Label */ 
3663#line 263
3664        if (ldv_s_gpio_mouse_device_driver_platform_driver == 0) {
3665          {
3666#line 268
3667          res_gpio_mouse_probe_1 = gpio_mouse_probe(var_group1);
3668#line 269
3669          ldv_check_return_value(res_gpio_mouse_probe_1);
3670          }
3671#line 270
3672          if (res_gpio_mouse_probe_1) {
3673#line 271
3674            goto ldv_module_exit;
3675          } else {
3676
3677          }
3678#line 272
3679          ldv_s_gpio_mouse_device_driver_platform_driver = 0;
3680        } else {
3681
3682        }
3683#line 278
3684        goto switch_break;
3685        switch_default: /* CIL Label */ 
3686#line 279
3687        goto switch_break;
3688      } else {
3689        switch_break: /* CIL Label */ ;
3690      }
3691      }
3692    }
3693  }
3694  while_break: /* CIL Label */ ;
3695  }
3696  ldv_module_exit: 
3697  {
3698#line 288
3699  ldv_check_final_state();
3700  }
3701#line 291
3702  return;
3703}
3704}
3705#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3706void ldv_blast_assert(void) 
3707{ 
3708
3709  {
3710  ERROR: 
3711#line 6
3712  goto ERROR;
3713}
3714}
3715#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3716extern int __VERIFIER_nondet_int(void) ;
3717#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3718int ldv_mutex  =    1;
3719#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3720int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
3721{ int nondetermined ;
3722
3723  {
3724#line 29
3725  if (ldv_mutex == 1) {
3726
3727  } else {
3728    {
3729#line 29
3730    ldv_blast_assert();
3731    }
3732  }
3733  {
3734#line 32
3735  nondetermined = __VERIFIER_nondet_int();
3736  }
3737#line 35
3738  if (nondetermined) {
3739#line 38
3740    ldv_mutex = 2;
3741#line 40
3742    return (0);
3743  } else {
3744#line 45
3745    return (-4);
3746  }
3747}
3748}
3749#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3750int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
3751{ int nondetermined ;
3752
3753  {
3754#line 57
3755  if (ldv_mutex == 1) {
3756
3757  } else {
3758    {
3759#line 57
3760    ldv_blast_assert();
3761    }
3762  }
3763  {
3764#line 60
3765  nondetermined = __VERIFIER_nondet_int();
3766  }
3767#line 63
3768  if (nondetermined) {
3769#line 66
3770    ldv_mutex = 2;
3771#line 68
3772    return (0);
3773  } else {
3774#line 73
3775    return (-4);
3776  }
3777}
3778}
3779#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3780int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
3781{ int atomic_value_after_dec ;
3782
3783  {
3784#line 83
3785  if (ldv_mutex == 1) {
3786
3787  } else {
3788    {
3789#line 83
3790    ldv_blast_assert();
3791    }
3792  }
3793  {
3794#line 86
3795  atomic_value_after_dec = __VERIFIER_nondet_int();
3796  }
3797#line 89
3798  if (atomic_value_after_dec == 0) {
3799#line 92
3800    ldv_mutex = 2;
3801#line 94
3802    return (1);
3803  } else {
3804
3805  }
3806#line 98
3807  return (0);
3808}
3809}
3810#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3811void mutex_lock(struct mutex *lock ) 
3812{ 
3813
3814  {
3815#line 108
3816  if (ldv_mutex == 1) {
3817
3818  } else {
3819    {
3820#line 108
3821    ldv_blast_assert();
3822    }
3823  }
3824#line 110
3825  ldv_mutex = 2;
3826#line 111
3827  return;
3828}
3829}
3830#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3831int mutex_trylock(struct mutex *lock ) 
3832{ int nondetermined ;
3833
3834  {
3835#line 121
3836  if (ldv_mutex == 1) {
3837
3838  } else {
3839    {
3840#line 121
3841    ldv_blast_assert();
3842    }
3843  }
3844  {
3845#line 124
3846  nondetermined = __VERIFIER_nondet_int();
3847  }
3848#line 127
3849  if (nondetermined) {
3850#line 130
3851    ldv_mutex = 2;
3852#line 132
3853    return (1);
3854  } else {
3855#line 137
3856    return (0);
3857  }
3858}
3859}
3860#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3861void mutex_unlock(struct mutex *lock ) 
3862{ 
3863
3864  {
3865#line 147
3866  if (ldv_mutex == 2) {
3867
3868  } else {
3869    {
3870#line 147
3871    ldv_blast_assert();
3872    }
3873  }
3874#line 149
3875  ldv_mutex = 1;
3876#line 150
3877  return;
3878}
3879}
3880#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3881void ldv_check_final_state(void) 
3882{ 
3883
3884  {
3885#line 156
3886  if (ldv_mutex == 1) {
3887
3888  } else {
3889    {
3890#line 156
3891    ldv_blast_assert();
3892    }
3893  }
3894#line 157
3895  return;
3896}
3897}
3898#line 300 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/drivers/input/mouse/gpio_mouse.c.common.c"
3899long s__builtin_expect(long val , long res ) 
3900{ 
3901
3902  {
3903#line 301
3904  return (val);
3905}
3906}