Showing error 253

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