Showing error 252

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