Showing error 257

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