Showing error 225

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--hid--hid-wacom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 6754
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 178 "include/linux/types.h"
  73typedef __u16 __le16;
  74#line 202 "include/linux/types.h"
  75typedef unsigned int gfp_t;
  76#line 203 "include/linux/types.h"
  77typedef unsigned int fmode_t;
  78#line 219 "include/linux/types.h"
  79struct __anonstruct_atomic_t_7 {
  80   int counter ;
  81};
  82#line 219 "include/linux/types.h"
  83typedef struct __anonstruct_atomic_t_7 atomic_t;
  84#line 224 "include/linux/types.h"
  85struct __anonstruct_atomic64_t_8 {
  86   long counter ;
  87};
  88#line 224 "include/linux/types.h"
  89typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  90#line 229 "include/linux/types.h"
  91struct list_head {
  92   struct list_head *next ;
  93   struct list_head *prev ;
  94};
  95#line 233
  96struct hlist_node;
  97#line 233 "include/linux/types.h"
  98struct hlist_head {
  99   struct hlist_node *first ;
 100};
 101#line 237 "include/linux/types.h"
 102struct hlist_node {
 103   struct hlist_node *next ;
 104   struct hlist_node **pprev ;
 105};
 106#line 253 "include/linux/types.h"
 107struct rcu_head {
 108   struct rcu_head *next ;
 109   void (*func)(struct rcu_head *head ) ;
 110};
 111#line 202 "include/linux/ioport.h"
 112struct device;
 113#line 202
 114struct device;
 115#line 12 "include/linux/lockdep.h"
 116struct task_struct;
 117#line 12
 118struct task_struct;
 119#line 391 "include/linux/lockdep.h"
 120struct lock_class_key {
 121
 122};
 123#line 20 "include/linux/kobject_ns.h"
 124struct sock;
 125#line 20
 126struct sock;
 127#line 21
 128struct kobject;
 129#line 21
 130struct kobject;
 131#line 27
 132enum kobj_ns_type {
 133    KOBJ_NS_TYPE_NONE = 0,
 134    KOBJ_NS_TYPE_NET = 1,
 135    KOBJ_NS_TYPES = 2
 136} ;
 137#line 40 "include/linux/kobject_ns.h"
 138struct kobj_ns_type_operations {
 139   enum kobj_ns_type type ;
 140   void *(*grab_current_ns)(void) ;
 141   void const   *(*netlink_ns)(struct sock *sk ) ;
 142   void const   *(*initial_ns)(void) ;
 143   void (*drop_ns)(void * ) ;
 144};
 145#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 146struct task_struct;
 147#line 146 "include/linux/init.h"
 148typedef void (*ctor_fn_t)(void);
 149#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 150struct page;
 151#line 295
 152struct file;
 153#line 295
 154struct file;
 155#line 313
 156struct seq_file;
 157#line 313
 158struct seq_file;
 159#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 160struct page;
 161#line 52
 162struct task_struct;
 163#line 329
 164struct arch_spinlock;
 165#line 329
 166struct arch_spinlock;
 167#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 168struct task_struct;
 169#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 170struct module;
 171#line 56
 172struct module;
 173#line 47 "include/linux/dynamic_debug.h"
 174struct device;
 175#line 135 "include/linux/kernel.h"
 176struct completion;
 177#line 135
 178struct completion;
 179#line 349
 180struct pid;
 181#line 349
 182struct pid;
 183#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 184struct task_struct;
 185#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
 186struct page;
 187#line 10 "include/asm-generic/bug.h"
 188struct bug_entry {
 189   int bug_addr_disp ;
 190   int file_disp ;
 191   unsigned short line ;
 192   unsigned short flags ;
 193};
 194#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 195struct static_key;
 196#line 234
 197struct static_key;
 198#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 199struct kmem_cache;
 200#line 23 "include/asm-generic/atomic-long.h"
 201typedef atomic64_t atomic_long_t;
 202#line 22 "include/linux/sysfs.h"
 203struct kobject;
 204#line 23
 205struct module;
 206#line 24
 207enum kobj_ns_type;
 208#line 26 "include/linux/sysfs.h"
 209struct attribute {
 210   char const   *name ;
 211   umode_t mode ;
 212};
 213#line 56 "include/linux/sysfs.h"
 214struct attribute_group {
 215   char const   *name ;
 216   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 217   struct attribute **attrs ;
 218};
 219#line 85
 220struct file;
 221#line 86
 222struct vm_area_struct;
 223#line 86
 224struct vm_area_struct;
 225#line 88 "include/linux/sysfs.h"
 226struct bin_attribute {
 227   struct attribute attr ;
 228   size_t size ;
 229   void *private ;
 230   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 231                   loff_t  , size_t  ) ;
 232   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 233                    loff_t  , size_t  ) ;
 234   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 235};
 236#line 112 "include/linux/sysfs.h"
 237struct sysfs_ops {
 238   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 239   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 240   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 241};
 242#line 118
 243struct sysfs_dirent;
 244#line 118
 245struct sysfs_dirent;
 246#line 12 "include/linux/thread_info.h"
 247struct timespec;
 248#line 12
 249struct timespec;
 250#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
 251struct task_struct;
 252#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 253typedef u16 __ticket_t;
 254#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 255typedef u32 __ticketpair_t;
 256#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 257struct __raw_tickets {
 258   __ticket_t head ;
 259   __ticket_t tail ;
 260};
 261#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 262union __anonunion____missing_field_name_36 {
 263   __ticketpair_t head_tail ;
 264   struct __raw_tickets tickets ;
 265};
 266#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 267struct arch_spinlock {
 268   union __anonunion____missing_field_name_36 __annonCompField17 ;
 269};
 270#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 271typedef struct arch_spinlock arch_spinlock_t;
 272#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 273struct __anonstruct____missing_field_name_38 {
 274   u32 read ;
 275   s32 write ;
 276};
 277#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 278union __anonunion_arch_rwlock_t_37 {
 279   s64 lock ;
 280   struct __anonstruct____missing_field_name_38 __annonCompField18 ;
 281};
 282#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 283typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_t;
 284#line 20 "include/linux/spinlock_types.h"
 285struct raw_spinlock {
 286   arch_spinlock_t raw_lock ;
 287   unsigned int magic ;
 288   unsigned int owner_cpu ;
 289   void *owner ;
 290};
 291#line 20 "include/linux/spinlock_types.h"
 292typedef struct raw_spinlock raw_spinlock_t;
 293#line 64 "include/linux/spinlock_types.h"
 294union __anonunion____missing_field_name_39 {
 295   struct raw_spinlock rlock ;
 296};
 297#line 64 "include/linux/spinlock_types.h"
 298struct spinlock {
 299   union __anonunion____missing_field_name_39 __annonCompField19 ;
 300};
 301#line 64 "include/linux/spinlock_types.h"
 302typedef struct spinlock spinlock_t;
 303#line 11 "include/linux/rwlock_types.h"
 304struct __anonstruct_rwlock_t_40 {
 305   arch_rwlock_t raw_lock ;
 306   unsigned int magic ;
 307   unsigned int owner_cpu ;
 308   void *owner ;
 309};
 310#line 11 "include/linux/rwlock_types.h"
 311typedef struct __anonstruct_rwlock_t_40 rwlock_t;
 312#line 22 "include/linux/kref.h"
 313struct kref {
 314   atomic_t refcount ;
 315};
 316#line 49 "include/linux/wait.h"
 317struct __wait_queue_head {
 318   spinlock_t lock ;
 319   struct list_head task_list ;
 320};
 321#line 53 "include/linux/wait.h"
 322typedef struct __wait_queue_head wait_queue_head_t;
 323#line 55
 324struct task_struct;
 325#line 60 "include/linux/kobject.h"
 326struct kset;
 327#line 60
 328struct kobj_type;
 329#line 60 "include/linux/kobject.h"
 330struct kobject {
 331   char const   *name ;
 332   struct list_head entry ;
 333   struct kobject *parent ;
 334   struct kset *kset ;
 335   struct kobj_type *ktype ;
 336   struct sysfs_dirent *sd ;
 337   struct kref kref ;
 338   unsigned int state_initialized : 1 ;
 339   unsigned int state_in_sysfs : 1 ;
 340   unsigned int state_add_uevent_sent : 1 ;
 341   unsigned int state_remove_uevent_sent : 1 ;
 342   unsigned int uevent_suppress : 1 ;
 343};
 344#line 108 "include/linux/kobject.h"
 345struct kobj_type {
 346   void (*release)(struct kobject *kobj ) ;
 347   struct sysfs_ops  const  *sysfs_ops ;
 348   struct attribute **default_attrs ;
 349   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 350   void const   *(*namespace)(struct kobject *kobj ) ;
 351};
 352#line 116 "include/linux/kobject.h"
 353struct kobj_uevent_env {
 354   char *envp[32] ;
 355   int envp_idx ;
 356   char buf[2048] ;
 357   int buflen ;
 358};
 359#line 123 "include/linux/kobject.h"
 360struct kset_uevent_ops {
 361   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 362   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 363   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 364};
 365#line 140
 366struct sock;
 367#line 159 "include/linux/kobject.h"
 368struct kset {
 369   struct list_head list ;
 370   spinlock_t list_lock ;
 371   struct kobject kobj ;
 372   struct kset_uevent_ops  const  *uevent_ops ;
 373};
 374#line 19 "include/linux/klist.h"
 375struct klist_node;
 376#line 19
 377struct klist_node;
 378#line 39 "include/linux/klist.h"
 379struct klist_node {
 380   void *n_klist ;
 381   struct list_head n_node ;
 382   struct kref n_ref ;
 383};
 384#line 48 "include/linux/mutex.h"
 385struct mutex {
 386   atomic_t count ;
 387   spinlock_t wait_lock ;
 388   struct list_head wait_list ;
 389   struct task_struct *owner ;
 390   char const   *name ;
 391   void *magic ;
 392};
 393#line 119 "include/linux/seqlock.h"
 394struct seqcount {
 395   unsigned int sequence ;
 396};
 397#line 119 "include/linux/seqlock.h"
 398typedef struct seqcount seqcount_t;
 399#line 14 "include/linux/time.h"
 400struct timespec {
 401   __kernel_time_t tv_sec ;
 402   long tv_nsec ;
 403};
 404#line 46 "include/linux/ktime.h"
 405union ktime {
 406   s64 tv64 ;
 407};
 408#line 59 "include/linux/ktime.h"
 409typedef union ktime ktime_t;
 410#line 10 "include/linux/timer.h"
 411struct tvec_base;
 412#line 10
 413struct tvec_base;
 414#line 12 "include/linux/timer.h"
 415struct timer_list {
 416   struct list_head entry ;
 417   unsigned long expires ;
 418   struct tvec_base *base ;
 419   void (*function)(unsigned long  ) ;
 420   unsigned long data ;
 421   int slack ;
 422   int start_pid ;
 423   void *start_site ;
 424   char start_comm[16] ;
 425};
 426#line 17 "include/linux/workqueue.h"
 427struct work_struct;
 428#line 17
 429struct work_struct;
 430#line 79 "include/linux/workqueue.h"
 431struct work_struct {
 432   atomic_long_t data ;
 433   struct list_head entry ;
 434   void (*func)(struct work_struct *work ) ;
 435};
 436#line 25 "include/linux/completion.h"
 437struct completion {
 438   unsigned int done ;
 439   wait_queue_head_t wait ;
 440};
 441#line 42 "include/linux/pm.h"
 442struct device;
 443#line 50 "include/linux/pm.h"
 444struct pm_message {
 445   int event ;
 446};
 447#line 50 "include/linux/pm.h"
 448typedef struct pm_message pm_message_t;
 449#line 264 "include/linux/pm.h"
 450struct dev_pm_ops {
 451   int (*prepare)(struct device *dev ) ;
 452   void (*complete)(struct device *dev ) ;
 453   int (*suspend)(struct device *dev ) ;
 454   int (*resume)(struct device *dev ) ;
 455   int (*freeze)(struct device *dev ) ;
 456   int (*thaw)(struct device *dev ) ;
 457   int (*poweroff)(struct device *dev ) ;
 458   int (*restore)(struct device *dev ) ;
 459   int (*suspend_late)(struct device *dev ) ;
 460   int (*resume_early)(struct device *dev ) ;
 461   int (*freeze_late)(struct device *dev ) ;
 462   int (*thaw_early)(struct device *dev ) ;
 463   int (*poweroff_late)(struct device *dev ) ;
 464   int (*restore_early)(struct device *dev ) ;
 465   int (*suspend_noirq)(struct device *dev ) ;
 466   int (*resume_noirq)(struct device *dev ) ;
 467   int (*freeze_noirq)(struct device *dev ) ;
 468   int (*thaw_noirq)(struct device *dev ) ;
 469   int (*poweroff_noirq)(struct device *dev ) ;
 470   int (*restore_noirq)(struct device *dev ) ;
 471   int (*runtime_suspend)(struct device *dev ) ;
 472   int (*runtime_resume)(struct device *dev ) ;
 473   int (*runtime_idle)(struct device *dev ) ;
 474};
 475#line 458
 476enum rpm_status {
 477    RPM_ACTIVE = 0,
 478    RPM_RESUMING = 1,
 479    RPM_SUSPENDED = 2,
 480    RPM_SUSPENDING = 3
 481} ;
 482#line 480
 483enum rpm_request {
 484    RPM_REQ_NONE = 0,
 485    RPM_REQ_IDLE = 1,
 486    RPM_REQ_SUSPEND = 2,
 487    RPM_REQ_AUTOSUSPEND = 3,
 488    RPM_REQ_RESUME = 4
 489} ;
 490#line 488
 491struct wakeup_source;
 492#line 488
 493struct wakeup_source;
 494#line 495 "include/linux/pm.h"
 495struct pm_subsys_data {
 496   spinlock_t lock ;
 497   unsigned int refcount ;
 498};
 499#line 506
 500struct dev_pm_qos_request;
 501#line 506
 502struct pm_qos_constraints;
 503#line 506 "include/linux/pm.h"
 504struct dev_pm_info {
 505   pm_message_t power_state ;
 506   unsigned int can_wakeup : 1 ;
 507   unsigned int async_suspend : 1 ;
 508   bool is_prepared : 1 ;
 509   bool is_suspended : 1 ;
 510   bool ignore_children : 1 ;
 511   spinlock_t lock ;
 512   struct list_head entry ;
 513   struct completion completion ;
 514   struct wakeup_source *wakeup ;
 515   bool wakeup_path : 1 ;
 516   struct timer_list suspend_timer ;
 517   unsigned long timer_expires ;
 518   struct work_struct work ;
 519   wait_queue_head_t wait_queue ;
 520   atomic_t usage_count ;
 521   atomic_t child_count ;
 522   unsigned int disable_depth : 3 ;
 523   unsigned int idle_notification : 1 ;
 524   unsigned int request_pending : 1 ;
 525   unsigned int deferred_resume : 1 ;
 526   unsigned int run_wake : 1 ;
 527   unsigned int runtime_auto : 1 ;
 528   unsigned int no_callbacks : 1 ;
 529   unsigned int irq_safe : 1 ;
 530   unsigned int use_autosuspend : 1 ;
 531   unsigned int timer_autosuspends : 1 ;
 532   enum rpm_request request ;
 533   enum rpm_status runtime_status ;
 534   int runtime_error ;
 535   int autosuspend_delay ;
 536   unsigned long last_busy ;
 537   unsigned long active_jiffies ;
 538   unsigned long suspended_jiffies ;
 539   unsigned long accounting_timestamp ;
 540   ktime_t suspend_time ;
 541   s64 max_time_suspended_ns ;
 542   struct dev_pm_qos_request *pq_req ;
 543   struct pm_subsys_data *subsys_data ;
 544   struct pm_qos_constraints *constraints ;
 545};
 546#line 564 "include/linux/pm.h"
 547struct dev_pm_domain {
 548   struct dev_pm_ops ops ;
 549};
 550#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 551struct dma_map_ops;
 552#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 553struct dev_archdata {
 554   void *acpi_handle ;
 555   struct dma_map_ops *dma_ops ;
 556   void *iommu ;
 557};
 558#line 28 "include/linux/device.h"
 559struct device;
 560#line 29
 561struct device_private;
 562#line 29
 563struct device_private;
 564#line 30
 565struct device_driver;
 566#line 30
 567struct device_driver;
 568#line 31
 569struct driver_private;
 570#line 31
 571struct driver_private;
 572#line 32
 573struct module;
 574#line 33
 575struct class;
 576#line 33
 577struct class;
 578#line 34
 579struct subsys_private;
 580#line 34
 581struct subsys_private;
 582#line 35
 583struct bus_type;
 584#line 35
 585struct bus_type;
 586#line 36
 587struct device_node;
 588#line 36
 589struct device_node;
 590#line 37
 591struct iommu_ops;
 592#line 37
 593struct iommu_ops;
 594#line 39 "include/linux/device.h"
 595struct bus_attribute {
 596   struct attribute attr ;
 597   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
 598   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
 599};
 600#line 89
 601struct device_attribute;
 602#line 89
 603struct driver_attribute;
 604#line 89 "include/linux/device.h"
 605struct bus_type {
 606   char const   *name ;
 607   char const   *dev_name ;
 608   struct device *dev_root ;
 609   struct bus_attribute *bus_attrs ;
 610   struct device_attribute *dev_attrs ;
 611   struct driver_attribute *drv_attrs ;
 612   int (*match)(struct device *dev , struct device_driver *drv ) ;
 613   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 614   int (*probe)(struct device *dev ) ;
 615   int (*remove)(struct device *dev ) ;
 616   void (*shutdown)(struct device *dev ) ;
 617   int (*suspend)(struct device *dev , pm_message_t state ) ;
 618   int (*resume)(struct device *dev ) ;
 619   struct dev_pm_ops  const  *pm ;
 620   struct iommu_ops *iommu_ops ;
 621   struct subsys_private *p ;
 622};
 623#line 127
 624struct device_type;
 625#line 214
 626struct of_device_id;
 627#line 214 "include/linux/device.h"
 628struct device_driver {
 629   char const   *name ;
 630   struct bus_type *bus ;
 631   struct module *owner ;
 632   char const   *mod_name ;
 633   bool suppress_bind_attrs ;
 634   struct of_device_id  const  *of_match_table ;
 635   int (*probe)(struct device *dev ) ;
 636   int (*remove)(struct device *dev ) ;
 637   void (*shutdown)(struct device *dev ) ;
 638   int (*suspend)(struct device *dev , pm_message_t state ) ;
 639   int (*resume)(struct device *dev ) ;
 640   struct attribute_group  const  **groups ;
 641   struct dev_pm_ops  const  *pm ;
 642   struct driver_private *p ;
 643};
 644#line 249 "include/linux/device.h"
 645struct driver_attribute {
 646   struct attribute attr ;
 647   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
 648   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
 649};
 650#line 330
 651struct class_attribute;
 652#line 330 "include/linux/device.h"
 653struct class {
 654   char const   *name ;
 655   struct module *owner ;
 656   struct class_attribute *class_attrs ;
 657   struct device_attribute *dev_attrs ;
 658   struct bin_attribute *dev_bin_attrs ;
 659   struct kobject *dev_kobj ;
 660   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 661   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 662   void (*class_release)(struct class *class ) ;
 663   void (*dev_release)(struct device *dev ) ;
 664   int (*suspend)(struct device *dev , pm_message_t state ) ;
 665   int (*resume)(struct device *dev ) ;
 666   struct kobj_ns_type_operations  const  *ns_type ;
 667   void const   *(*namespace)(struct device *dev ) ;
 668   struct dev_pm_ops  const  *pm ;
 669   struct subsys_private *p ;
 670};
 671#line 397 "include/linux/device.h"
 672struct class_attribute {
 673   struct attribute attr ;
 674   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
 675   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
 676                    size_t count ) ;
 677   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
 678};
 679#line 465 "include/linux/device.h"
 680struct device_type {
 681   char const   *name ;
 682   struct attribute_group  const  **groups ;
 683   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 684   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 685   void (*release)(struct device *dev ) ;
 686   struct dev_pm_ops  const  *pm ;
 687};
 688#line 476 "include/linux/device.h"
 689struct device_attribute {
 690   struct attribute attr ;
 691   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
 692   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
 693                    size_t count ) ;
 694};
 695#line 559 "include/linux/device.h"
 696struct device_dma_parameters {
 697   unsigned int max_segment_size ;
 698   unsigned long segment_boundary_mask ;
 699};
 700#line 627
 701struct dma_coherent_mem;
 702#line 627 "include/linux/device.h"
 703struct device {
 704   struct device *parent ;
 705   struct device_private *p ;
 706   struct kobject kobj ;
 707   char const   *init_name ;
 708   struct device_type  const  *type ;
 709   struct mutex mutex ;
 710   struct bus_type *bus ;
 711   struct device_driver *driver ;
 712   void *platform_data ;
 713   struct dev_pm_info power ;
 714   struct dev_pm_domain *pm_domain ;
 715   int numa_node ;
 716   u64 *dma_mask ;
 717   u64 coherent_dma_mask ;
 718   struct device_dma_parameters *dma_parms ;
 719   struct list_head dma_pools ;
 720   struct dma_coherent_mem *dma_mem ;
 721   struct dev_archdata archdata ;
 722   struct device_node *of_node ;
 723   dev_t devt ;
 724   u32 id ;
 725   spinlock_t devres_lock ;
 726   struct list_head devres_head ;
 727   struct klist_node knode_class ;
 728   struct class *class ;
 729   struct attribute_group  const  **groups ;
 730   void (*release)(struct device *dev ) ;
 731};
 732#line 43 "include/linux/pm_wakeup.h"
 733struct wakeup_source {
 734   char const   *name ;
 735   struct list_head entry ;
 736   spinlock_t lock ;
 737   struct timer_list timer ;
 738   unsigned long timer_expires ;
 739   ktime_t total_time ;
 740   ktime_t max_time ;
 741   ktime_t last_time ;
 742   unsigned long event_count ;
 743   unsigned long active_count ;
 744   unsigned long relax_count ;
 745   unsigned long hit_count ;
 746   unsigned int active : 1 ;
 747};
 748#line 60 "include/linux/pageblock-flags.h"
 749struct page;
 750#line 19 "include/linux/rwsem.h"
 751struct rw_semaphore;
 752#line 19
 753struct rw_semaphore;
 754#line 25 "include/linux/rwsem.h"
 755struct rw_semaphore {
 756   long count ;
 757   raw_spinlock_t wait_lock ;
 758   struct list_head wait_list ;
 759};
 760#line 9 "include/linux/memory_hotplug.h"
 761struct page;
 762#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 763struct device;
 764#line 8 "include/linux/vmalloc.h"
 765struct vm_area_struct;
 766#line 994 "include/linux/mmzone.h"
 767struct page;
 768#line 10 "include/linux/gfp.h"
 769struct vm_area_struct;
 770#line 46 "include/linux/slub_def.h"
 771struct kmem_cache_cpu {
 772   void **freelist ;
 773   unsigned long tid ;
 774   struct page *page ;
 775   struct page *partial ;
 776   int node ;
 777   unsigned int stat[26] ;
 778};
 779#line 57 "include/linux/slub_def.h"
 780struct kmem_cache_node {
 781   spinlock_t list_lock ;
 782   unsigned long nr_partial ;
 783   struct list_head partial ;
 784   atomic_long_t nr_slabs ;
 785   atomic_long_t total_objects ;
 786   struct list_head full ;
 787};
 788#line 73 "include/linux/slub_def.h"
 789struct kmem_cache_order_objects {
 790   unsigned long x ;
 791};
 792#line 80 "include/linux/slub_def.h"
 793struct kmem_cache {
 794   struct kmem_cache_cpu *cpu_slab ;
 795   unsigned long flags ;
 796   unsigned long min_partial ;
 797   int size ;
 798   int objsize ;
 799   int offset ;
 800   int cpu_partial ;
 801   struct kmem_cache_order_objects oo ;
 802   struct kmem_cache_order_objects max ;
 803   struct kmem_cache_order_objects min ;
 804   gfp_t allocflags ;
 805   int refcount ;
 806   void (*ctor)(void * ) ;
 807   int inuse ;
 808   int align ;
 809   int reserved ;
 810   char const   *name ;
 811   struct list_head list ;
 812   struct kobject kobj ;
 813   int remote_node_defrag_ratio ;
 814   struct kmem_cache_node *node[1 << 10] ;
 815};
 816#line 12 "include/linux/mod_devicetable.h"
 817typedef unsigned long kernel_ulong_t;
 818#line 136 "include/linux/mod_devicetable.h"
 819struct hid_device_id {
 820   __u16 bus ;
 821   __u16 pad1 ;
 822   __u32 vendor ;
 823   __u32 product ;
 824   kernel_ulong_t driver_data  __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
 825};
 826#line 219 "include/linux/mod_devicetable.h"
 827struct of_device_id {
 828   char name[32] ;
 829   char type[32] ;
 830   char compatible[128] ;
 831   void *data ;
 832};
 833#line 312 "include/linux/mod_devicetable.h"
 834struct input_device_id {
 835   kernel_ulong_t flags ;
 836   __u16 bustype ;
 837   __u16 vendor ;
 838   __u16 product ;
 839   __u16 version ;
 840   kernel_ulong_t evbit[1] ;
 841   kernel_ulong_t keybit[12] ;
 842   kernel_ulong_t relbit[1] ;
 843   kernel_ulong_t absbit[1] ;
 844   kernel_ulong_t mscbit[1] ;
 845   kernel_ulong_t ledbit[1] ;
 846   kernel_ulong_t sndbit[1] ;
 847   kernel_ulong_t ffbit[2] ;
 848   kernel_ulong_t swbit[1] ;
 849   kernel_ulong_t driver_info ;
 850};
 851#line 43 "include/linux/input.h"
 852struct input_id {
 853   __u16 bustype ;
 854   __u16 vendor ;
 855   __u16 product ;
 856   __u16 version ;
 857};
 858#line 69 "include/linux/input.h"
 859struct input_absinfo {
 860   __s32 value ;
 861   __s32 minimum ;
 862   __s32 maximum ;
 863   __s32 fuzz ;
 864   __s32 flat ;
 865   __s32 resolution ;
 866};
 867#line 93 "include/linux/input.h"
 868struct input_keymap_entry {
 869   __u8 flags ;
 870   __u8 len ;
 871   __u16 index ;
 872   __u32 keycode ;
 873   __u8 scancode[32] ;
 874};
 875#line 957 "include/linux/input.h"
 876struct ff_replay {
 877   __u16 length ;
 878   __u16 delay ;
 879};
 880#line 967 "include/linux/input.h"
 881struct ff_trigger {
 882   __u16 button ;
 883   __u16 interval ;
 884};
 885#line 984 "include/linux/input.h"
 886struct ff_envelope {
 887   __u16 attack_length ;
 888   __u16 attack_level ;
 889   __u16 fade_length ;
 890   __u16 fade_level ;
 891};
 892#line 996 "include/linux/input.h"
 893struct ff_constant_effect {
 894   __s16 level ;
 895   struct ff_envelope envelope ;
 896};
 897#line 1007 "include/linux/input.h"
 898struct ff_ramp_effect {
 899   __s16 start_level ;
 900   __s16 end_level ;
 901   struct ff_envelope envelope ;
 902};
 903#line 1023 "include/linux/input.h"
 904struct ff_condition_effect {
 905   __u16 right_saturation ;
 906   __u16 left_saturation ;
 907   __s16 right_coeff ;
 908   __s16 left_coeff ;
 909   __u16 deadband ;
 910   __s16 center ;
 911};
 912#line 1052 "include/linux/input.h"
 913struct ff_periodic_effect {
 914   __u16 waveform ;
 915   __u16 period ;
 916   __s16 magnitude ;
 917   __s16 offset ;
 918   __u16 phase ;
 919   struct ff_envelope envelope ;
 920   __u32 custom_len ;
 921   __s16 *custom_data ;
 922};
 923#line 1073 "include/linux/input.h"
 924struct ff_rumble_effect {
 925   __u16 strong_magnitude ;
 926   __u16 weak_magnitude ;
 927};
 928#line 1101 "include/linux/input.h"
 929union __anonunion_u_140 {
 930   struct ff_constant_effect constant ;
 931   struct ff_ramp_effect ramp ;
 932   struct ff_periodic_effect periodic ;
 933   struct ff_condition_effect condition[2] ;
 934   struct ff_rumble_effect rumble ;
 935};
 936#line 1101 "include/linux/input.h"
 937struct ff_effect {
 938   __u16 type ;
 939   __s16 id ;
 940   __u16 direction ;
 941   struct ff_trigger trigger ;
 942   struct ff_replay replay ;
 943   union __anonunion_u_140 u ;
 944};
 945#line 15 "include/linux/blk_types.h"
 946struct page;
 947#line 16
 948struct block_device;
 949#line 16
 950struct block_device;
 951#line 33 "include/linux/list_bl.h"
 952struct hlist_bl_node;
 953#line 33 "include/linux/list_bl.h"
 954struct hlist_bl_head {
 955   struct hlist_bl_node *first ;
 956};
 957#line 37 "include/linux/list_bl.h"
 958struct hlist_bl_node {
 959   struct hlist_bl_node *next ;
 960   struct hlist_bl_node **pprev ;
 961};
 962#line 13 "include/linux/dcache.h"
 963struct nameidata;
 964#line 13
 965struct nameidata;
 966#line 14
 967struct path;
 968#line 14
 969struct path;
 970#line 15
 971struct vfsmount;
 972#line 15
 973struct vfsmount;
 974#line 35 "include/linux/dcache.h"
 975struct qstr {
 976   unsigned int hash ;
 977   unsigned int len ;
 978   unsigned char const   *name ;
 979};
 980#line 88
 981struct inode;
 982#line 88
 983struct dentry_operations;
 984#line 88
 985struct super_block;
 986#line 88 "include/linux/dcache.h"
 987union __anonunion_d_u_141 {
 988   struct list_head d_child ;
 989   struct rcu_head d_rcu ;
 990};
 991#line 88 "include/linux/dcache.h"
 992struct dentry {
 993   unsigned int d_flags ;
 994   seqcount_t d_seq ;
 995   struct hlist_bl_node d_hash ;
 996   struct dentry *d_parent ;
 997   struct qstr d_name ;
 998   struct inode *d_inode ;
 999   unsigned char d_iname[32] ;
1000   unsigned int d_count ;
1001   spinlock_t d_lock ;
1002   struct dentry_operations  const  *d_op ;
1003   struct super_block *d_sb ;
1004   unsigned long d_time ;
1005   void *d_fsdata ;
1006   struct list_head d_lru ;
1007   union __anonunion_d_u_141 d_u ;
1008   struct list_head d_subdirs ;
1009   struct list_head d_alias ;
1010};
1011#line 131 "include/linux/dcache.h"
1012struct dentry_operations {
1013   int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1014   int (*d_hash)(struct dentry  const  * , struct inode  const  * , struct qstr * ) ;
1015   int (*d_compare)(struct dentry  const  * , struct inode  const  * , struct dentry  const  * ,
1016                    struct inode  const  * , unsigned int  , char const   * , struct qstr  const  * ) ;
1017   int (*d_delete)(struct dentry  const  * ) ;
1018   void (*d_release)(struct dentry * ) ;
1019   void (*d_prune)(struct dentry * ) ;
1020   void (*d_iput)(struct dentry * , struct inode * ) ;
1021   char *(*d_dname)(struct dentry * , char * , int  ) ;
1022   struct vfsmount *(*d_automount)(struct path * ) ;
1023   int (*d_manage)(struct dentry * , bool  ) ;
1024} __attribute__((__aligned__((1) <<  (6) ))) ;
1025#line 4 "include/linux/path.h"
1026struct dentry;
1027#line 5
1028struct vfsmount;
1029#line 7 "include/linux/path.h"
1030struct path {
1031   struct vfsmount *mnt ;
1032   struct dentry *dentry ;
1033};
1034#line 62 "include/linux/stat.h"
1035struct kstat {
1036   u64 ino ;
1037   dev_t dev ;
1038   umode_t mode ;
1039   unsigned int nlink ;
1040   uid_t uid ;
1041   gid_t gid ;
1042   dev_t rdev ;
1043   loff_t size ;
1044   struct timespec atime ;
1045   struct timespec mtime ;
1046   struct timespec ctime ;
1047   unsigned long blksize ;
1048   unsigned long long blocks ;
1049};
1050#line 64 "include/linux/radix-tree.h"
1051struct radix_tree_node;
1052#line 64 "include/linux/radix-tree.h"
1053struct radix_tree_root {
1054   unsigned int height ;
1055   gfp_t gfp_mask ;
1056   struct radix_tree_node *rnode ;
1057};
1058#line 14 "include/linux/prio_tree.h"
1059struct prio_tree_node;
1060#line 20 "include/linux/prio_tree.h"
1061struct prio_tree_node {
1062   struct prio_tree_node *left ;
1063   struct prio_tree_node *right ;
1064   struct prio_tree_node *parent ;
1065   unsigned long start ;
1066   unsigned long last ;
1067};
1068#line 28 "include/linux/prio_tree.h"
1069struct prio_tree_root {
1070   struct prio_tree_node *prio_tree_node ;
1071   unsigned short index_bits ;
1072   unsigned short raw ;
1073};
1074#line 6 "include/linux/pid.h"
1075enum pid_type {
1076    PIDTYPE_PID = 0,
1077    PIDTYPE_PGID = 1,
1078    PIDTYPE_SID = 2,
1079    PIDTYPE_MAX = 3
1080} ;
1081#line 50
1082struct pid_namespace;
1083#line 50 "include/linux/pid.h"
1084struct upid {
1085   int nr ;
1086   struct pid_namespace *ns ;
1087   struct hlist_node pid_chain ;
1088};
1089#line 57 "include/linux/pid.h"
1090struct pid {
1091   atomic_t count ;
1092   unsigned int level ;
1093   struct hlist_head tasks[3] ;
1094   struct rcu_head rcu ;
1095   struct upid numbers[1] ;
1096};
1097#line 100
1098struct pid_namespace;
1099#line 18 "include/linux/capability.h"
1100struct task_struct;
1101#line 377
1102struct dentry;
1103#line 16 "include/linux/semaphore.h"
1104struct semaphore {
1105   raw_spinlock_t lock ;
1106   unsigned int count ;
1107   struct list_head wait_list ;
1108};
1109#line 16 "include/linux/fiemap.h"
1110struct fiemap_extent {
1111   __u64 fe_logical ;
1112   __u64 fe_physical ;
1113   __u64 fe_length ;
1114   __u64 fe_reserved64[2] ;
1115   __u32 fe_flags ;
1116   __u32 fe_reserved[3] ;
1117};
1118#line 8 "include/linux/shrinker.h"
1119struct shrink_control {
1120   gfp_t gfp_mask ;
1121   unsigned long nr_to_scan ;
1122};
1123#line 31 "include/linux/shrinker.h"
1124struct shrinker {
1125   int (*shrink)(struct shrinker * , struct shrink_control *sc ) ;
1126   int seeks ;
1127   long batch ;
1128   struct list_head list ;
1129   atomic_long_t nr_in_batch ;
1130};
1131#line 10 "include/linux/migrate_mode.h"
1132enum migrate_mode {
1133    MIGRATE_ASYNC = 0,
1134    MIGRATE_SYNC_LIGHT = 1,
1135    MIGRATE_SYNC = 2
1136} ;
1137#line 408 "include/linux/fs.h"
1138struct export_operations;
1139#line 408
1140struct export_operations;
1141#line 410
1142struct iovec;
1143#line 410
1144struct iovec;
1145#line 411
1146struct nameidata;
1147#line 412
1148struct kiocb;
1149#line 412
1150struct kiocb;
1151#line 413
1152struct kobject;
1153#line 414
1154struct pipe_inode_info;
1155#line 414
1156struct pipe_inode_info;
1157#line 415
1158struct poll_table_struct;
1159#line 415
1160struct poll_table_struct;
1161#line 416
1162struct kstatfs;
1163#line 416
1164struct kstatfs;
1165#line 417
1166struct vm_area_struct;
1167#line 418
1168struct vfsmount;
1169#line 419
1170struct cred;
1171#line 419
1172struct cred;
1173#line 469 "include/linux/fs.h"
1174struct iattr {
1175   unsigned int ia_valid ;
1176   umode_t ia_mode ;
1177   uid_t ia_uid ;
1178   gid_t ia_gid ;
1179   loff_t ia_size ;
1180   struct timespec ia_atime ;
1181   struct timespec ia_mtime ;
1182   struct timespec ia_ctime ;
1183   struct file *ia_file ;
1184};
1185#line 129 "include/linux/quota.h"
1186struct if_dqinfo {
1187   __u64 dqi_bgrace ;
1188   __u64 dqi_igrace ;
1189   __u32 dqi_flags ;
1190   __u32 dqi_valid ;
1191};
1192#line 50 "include/linux/dqblk_xfs.h"
1193struct fs_disk_quota {
1194   __s8 d_version ;
1195   __s8 d_flags ;
1196   __u16 d_fieldmask ;
1197   __u32 d_id ;
1198   __u64 d_blk_hardlimit ;
1199   __u64 d_blk_softlimit ;
1200   __u64 d_ino_hardlimit ;
1201   __u64 d_ino_softlimit ;
1202   __u64 d_bcount ;
1203   __u64 d_icount ;
1204   __s32 d_itimer ;
1205   __s32 d_btimer ;
1206   __u16 d_iwarns ;
1207   __u16 d_bwarns ;
1208   __s32 d_padding2 ;
1209   __u64 d_rtb_hardlimit ;
1210   __u64 d_rtb_softlimit ;
1211   __u64 d_rtbcount ;
1212   __s32 d_rtbtimer ;
1213   __u16 d_rtbwarns ;
1214   __s16 d_padding3 ;
1215   char d_padding4[8] ;
1216};
1217#line 146 "include/linux/dqblk_xfs.h"
1218struct fs_qfilestat {
1219   __u64 qfs_ino ;
1220   __u64 qfs_nblks ;
1221   __u32 qfs_nextents ;
1222};
1223#line 146 "include/linux/dqblk_xfs.h"
1224typedef struct fs_qfilestat fs_qfilestat_t;
1225#line 152 "include/linux/dqblk_xfs.h"
1226struct fs_quota_stat {
1227   __s8 qs_version ;
1228   __u16 qs_flags ;
1229   __s8 qs_pad ;
1230   fs_qfilestat_t qs_uquota ;
1231   fs_qfilestat_t qs_gquota ;
1232   __u32 qs_incoredqs ;
1233   __s32 qs_btimelimit ;
1234   __s32 qs_itimelimit ;
1235   __s32 qs_rtbtimelimit ;
1236   __u16 qs_bwarnlimit ;
1237   __u16 qs_iwarnlimit ;
1238};
1239#line 17 "include/linux/dqblk_qtree.h"
1240struct dquot;
1241#line 17
1242struct dquot;
1243#line 185 "include/linux/quota.h"
1244typedef __kernel_uid32_t qid_t;
1245#line 186 "include/linux/quota.h"
1246typedef long long qsize_t;
1247#line 200 "include/linux/quota.h"
1248struct mem_dqblk {
1249   qsize_t dqb_bhardlimit ;
1250   qsize_t dqb_bsoftlimit ;
1251   qsize_t dqb_curspace ;
1252   qsize_t dqb_rsvspace ;
1253   qsize_t dqb_ihardlimit ;
1254   qsize_t dqb_isoftlimit ;
1255   qsize_t dqb_curinodes ;
1256   time_t dqb_btime ;
1257   time_t dqb_itime ;
1258};
1259#line 215
1260struct quota_format_type;
1261#line 215
1262struct quota_format_type;
1263#line 217 "include/linux/quota.h"
1264struct mem_dqinfo {
1265   struct quota_format_type *dqi_format ;
1266   int dqi_fmt_id ;
1267   struct list_head dqi_dirty_list ;
1268   unsigned long dqi_flags ;
1269   unsigned int dqi_bgrace ;
1270   unsigned int dqi_igrace ;
1271   qsize_t dqi_maxblimit ;
1272   qsize_t dqi_maxilimit ;
1273   void *dqi_priv ;
1274};
1275#line 230
1276struct super_block;
1277#line 288 "include/linux/quota.h"
1278struct dquot {
1279   struct hlist_node dq_hash ;
1280   struct list_head dq_inuse ;
1281   struct list_head dq_free ;
1282   struct list_head dq_dirty ;
1283   struct mutex dq_lock ;
1284   atomic_t dq_count ;
1285   wait_queue_head_t dq_wait_unused ;
1286   struct super_block *dq_sb ;
1287   unsigned int dq_id ;
1288   loff_t dq_off ;
1289   unsigned long dq_flags ;
1290   short dq_type ;
1291   struct mem_dqblk dq_dqb ;
1292};
1293#line 305 "include/linux/quota.h"
1294struct quota_format_ops {
1295   int (*check_quota_file)(struct super_block *sb , int type ) ;
1296   int (*read_file_info)(struct super_block *sb , int type ) ;
1297   int (*write_file_info)(struct super_block *sb , int type ) ;
1298   int (*free_file_info)(struct super_block *sb , int type ) ;
1299   int (*read_dqblk)(struct dquot *dquot ) ;
1300   int (*commit_dqblk)(struct dquot *dquot ) ;
1301   int (*release_dqblk)(struct dquot *dquot ) ;
1302};
1303#line 316 "include/linux/quota.h"
1304struct dquot_operations {
1305   int (*write_dquot)(struct dquot * ) ;
1306   struct dquot *(*alloc_dquot)(struct super_block * , int  ) ;
1307   void (*destroy_dquot)(struct dquot * ) ;
1308   int (*acquire_dquot)(struct dquot * ) ;
1309   int (*release_dquot)(struct dquot * ) ;
1310   int (*mark_dirty)(struct dquot * ) ;
1311   int (*write_info)(struct super_block * , int  ) ;
1312   qsize_t *(*get_reserved_space)(struct inode * ) ;
1313};
1314#line 329
1315struct path;
1316#line 332 "include/linux/quota.h"
1317struct quotactl_ops {
1318   int (*quota_on)(struct super_block * , int  , int  , struct path * ) ;
1319   int (*quota_on_meta)(struct super_block * , int  , int  ) ;
1320   int (*quota_off)(struct super_block * , int  ) ;
1321   int (*quota_sync)(struct super_block * , int  , int  ) ;
1322   int (*get_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1323   int (*set_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1324   int (*get_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1325   int (*set_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1326   int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1327   int (*set_xstate)(struct super_block * , unsigned int  , int  ) ;
1328};
1329#line 345 "include/linux/quota.h"
1330struct quota_format_type {
1331   int qf_fmt_id ;
1332   struct quota_format_ops  const  *qf_ops ;
1333   struct module *qf_owner ;
1334   struct quota_format_type *qf_next ;
1335};
1336#line 399 "include/linux/quota.h"
1337struct quota_info {
1338   unsigned int flags ;
1339   struct mutex dqio_mutex ;
1340   struct mutex dqonoff_mutex ;
1341   struct rw_semaphore dqptr_sem ;
1342   struct inode *files[2] ;
1343   struct mem_dqinfo info[2] ;
1344   struct quota_format_ops  const  *ops[2] ;
1345};
1346#line 532 "include/linux/fs.h"
1347struct page;
1348#line 533
1349struct address_space;
1350#line 533
1351struct address_space;
1352#line 534
1353struct writeback_control;
1354#line 534
1355struct writeback_control;
1356#line 577 "include/linux/fs.h"
1357union __anonunion_arg_149 {
1358   char *buf ;
1359   void *data ;
1360};
1361#line 577 "include/linux/fs.h"
1362struct __anonstruct_read_descriptor_t_148 {
1363   size_t written ;
1364   size_t count ;
1365   union __anonunion_arg_149 arg ;
1366   int error ;
1367};
1368#line 577 "include/linux/fs.h"
1369typedef struct __anonstruct_read_descriptor_t_148 read_descriptor_t;
1370#line 590 "include/linux/fs.h"
1371struct address_space_operations {
1372   int (*writepage)(struct page *page , struct writeback_control *wbc ) ;
1373   int (*readpage)(struct file * , struct page * ) ;
1374   int (*writepages)(struct address_space * , struct writeback_control * ) ;
1375   int (*set_page_dirty)(struct page *page ) ;
1376   int (*readpages)(struct file *filp , struct address_space *mapping , struct list_head *pages ,
1377                    unsigned int nr_pages ) ;
1378   int (*write_begin)(struct file * , struct address_space *mapping , loff_t pos ,
1379                      unsigned int len , unsigned int flags , struct page **pagep ,
1380                      void **fsdata ) ;
1381   int (*write_end)(struct file * , struct address_space *mapping , loff_t pos , unsigned int len ,
1382                    unsigned int copied , struct page *page , void *fsdata ) ;
1383   sector_t (*bmap)(struct address_space * , sector_t  ) ;
1384   void (*invalidatepage)(struct page * , unsigned long  ) ;
1385   int (*releasepage)(struct page * , gfp_t  ) ;
1386   void (*freepage)(struct page * ) ;
1387   ssize_t (*direct_IO)(int  , struct kiocb * , struct iovec  const  *iov , loff_t offset ,
1388                        unsigned long nr_segs ) ;
1389   int (*get_xip_mem)(struct address_space * , unsigned long  , int  , void ** , unsigned long * ) ;
1390   int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode  ) ;
1391   int (*launder_page)(struct page * ) ;
1392   int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long  ) ;
1393   int (*error_remove_page)(struct address_space * , struct page * ) ;
1394};
1395#line 645
1396struct backing_dev_info;
1397#line 645
1398struct backing_dev_info;
1399#line 646 "include/linux/fs.h"
1400struct address_space {
1401   struct inode *host ;
1402   struct radix_tree_root page_tree ;
1403   spinlock_t tree_lock ;
1404   unsigned int i_mmap_writable ;
1405   struct prio_tree_root i_mmap ;
1406   struct list_head i_mmap_nonlinear ;
1407   struct mutex i_mmap_mutex ;
1408   unsigned long nrpages ;
1409   unsigned long writeback_index ;
1410   struct address_space_operations  const  *a_ops ;
1411   unsigned long flags ;
1412   struct backing_dev_info *backing_dev_info ;
1413   spinlock_t private_lock ;
1414   struct list_head private_list ;
1415   struct address_space *assoc_mapping ;
1416} __attribute__((__aligned__(sizeof(long )))) ;
1417#line 669
1418struct request_queue;
1419#line 669
1420struct request_queue;
1421#line 671
1422struct hd_struct;
1423#line 671
1424struct gendisk;
1425#line 671 "include/linux/fs.h"
1426struct block_device {
1427   dev_t bd_dev ;
1428   int bd_openers ;
1429   struct inode *bd_inode ;
1430   struct super_block *bd_super ;
1431   struct mutex bd_mutex ;
1432   struct list_head bd_inodes ;
1433   void *bd_claiming ;
1434   void *bd_holder ;
1435   int bd_holders ;
1436   bool bd_write_holder ;
1437   struct list_head bd_holder_disks ;
1438   struct block_device *bd_contains ;
1439   unsigned int bd_block_size ;
1440   struct hd_struct *bd_part ;
1441   unsigned int bd_part_count ;
1442   int bd_invalidated ;
1443   struct gendisk *bd_disk ;
1444   struct request_queue *bd_queue ;
1445   struct list_head bd_list ;
1446   unsigned long bd_private ;
1447   int bd_fsfreeze_count ;
1448   struct mutex bd_fsfreeze_mutex ;
1449};
1450#line 749
1451struct posix_acl;
1452#line 749
1453struct posix_acl;
1454#line 761
1455struct inode_operations;
1456#line 761 "include/linux/fs.h"
1457union __anonunion____missing_field_name_150 {
1458   unsigned int const   i_nlink ;
1459   unsigned int __i_nlink ;
1460};
1461#line 761 "include/linux/fs.h"
1462union __anonunion____missing_field_name_151 {
1463   struct list_head i_dentry ;
1464   struct rcu_head i_rcu ;
1465};
1466#line 761
1467struct file_operations;
1468#line 761
1469struct file_lock;
1470#line 761
1471struct cdev;
1472#line 761 "include/linux/fs.h"
1473union __anonunion____missing_field_name_152 {
1474   struct pipe_inode_info *i_pipe ;
1475   struct block_device *i_bdev ;
1476   struct cdev *i_cdev ;
1477};
1478#line 761 "include/linux/fs.h"
1479struct inode {
1480   umode_t i_mode ;
1481   unsigned short i_opflags ;
1482   uid_t i_uid ;
1483   gid_t i_gid ;
1484   unsigned int i_flags ;
1485   struct posix_acl *i_acl ;
1486   struct posix_acl *i_default_acl ;
1487   struct inode_operations  const  *i_op ;
1488   struct super_block *i_sb ;
1489   struct address_space *i_mapping ;
1490   void *i_security ;
1491   unsigned long i_ino ;
1492   union __anonunion____missing_field_name_150 __annonCompField30 ;
1493   dev_t i_rdev ;
1494   struct timespec i_atime ;
1495   struct timespec i_mtime ;
1496   struct timespec i_ctime ;
1497   spinlock_t i_lock ;
1498   unsigned short i_bytes ;
1499   blkcnt_t i_blocks ;
1500   loff_t i_size ;
1501   unsigned long i_state ;
1502   struct mutex i_mutex ;
1503   unsigned long dirtied_when ;
1504   struct hlist_node i_hash ;
1505   struct list_head i_wb_list ;
1506   struct list_head i_lru ;
1507   struct list_head i_sb_list ;
1508   union __anonunion____missing_field_name_151 __annonCompField31 ;
1509   atomic_t i_count ;
1510   unsigned int i_blkbits ;
1511   u64 i_version ;
1512   atomic_t i_dio_count ;
1513   atomic_t i_writecount ;
1514   struct file_operations  const  *i_fop ;
1515   struct file_lock *i_flock ;
1516   struct address_space i_data ;
1517   struct dquot *i_dquot[2] ;
1518   struct list_head i_devices ;
1519   union __anonunion____missing_field_name_152 __annonCompField32 ;
1520   __u32 i_generation ;
1521   __u32 i_fsnotify_mask ;
1522   struct hlist_head i_fsnotify_marks ;
1523   atomic_t i_readcount ;
1524   void *i_private ;
1525};
1526#line 942 "include/linux/fs.h"
1527struct fown_struct {
1528   rwlock_t lock ;
1529   struct pid *pid ;
1530   enum pid_type pid_type ;
1531   uid_t uid ;
1532   uid_t euid ;
1533   int signum ;
1534};
1535#line 953 "include/linux/fs.h"
1536struct file_ra_state {
1537   unsigned long start ;
1538   unsigned int size ;
1539   unsigned int async_size ;
1540   unsigned int ra_pages ;
1541   unsigned int mmap_miss ;
1542   loff_t prev_pos ;
1543};
1544#line 976 "include/linux/fs.h"
1545union __anonunion_f_u_153 {
1546   struct list_head fu_list ;
1547   struct rcu_head fu_rcuhead ;
1548};
1549#line 976 "include/linux/fs.h"
1550struct file {
1551   union __anonunion_f_u_153 f_u ;
1552   struct path f_path ;
1553   struct file_operations  const  *f_op ;
1554   spinlock_t f_lock ;
1555   int f_sb_list_cpu ;
1556   atomic_long_t f_count ;
1557   unsigned int f_flags ;
1558   fmode_t f_mode ;
1559   loff_t f_pos ;
1560   struct fown_struct f_owner ;
1561   struct cred  const  *f_cred ;
1562   struct file_ra_state f_ra ;
1563   u64 f_version ;
1564   void *f_security ;
1565   void *private_data ;
1566   struct list_head f_ep_links ;
1567   struct list_head f_tfile_llink ;
1568   struct address_space *f_mapping ;
1569   unsigned long f_mnt_write_state ;
1570};
1571#line 1111
1572struct files_struct;
1573#line 1111 "include/linux/fs.h"
1574typedef struct files_struct *fl_owner_t;
1575#line 1113 "include/linux/fs.h"
1576struct file_lock_operations {
1577   void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1578   void (*fl_release_private)(struct file_lock * ) ;
1579};
1580#line 1118 "include/linux/fs.h"
1581struct lock_manager_operations {
1582   int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1583   void (*lm_notify)(struct file_lock * ) ;
1584   int (*lm_grant)(struct file_lock * , struct file_lock * , int  ) ;
1585   void (*lm_release_private)(struct file_lock * ) ;
1586   void (*lm_break)(struct file_lock * ) ;
1587   int (*lm_change)(struct file_lock ** , int  ) ;
1588};
1589#line 4 "include/linux/nfs_fs_i.h"
1590struct nlm_lockowner;
1591#line 4
1592struct nlm_lockowner;
1593#line 9 "include/linux/nfs_fs_i.h"
1594struct nfs_lock_info {
1595   u32 state ;
1596   struct nlm_lockowner *owner ;
1597   struct list_head list ;
1598};
1599#line 15
1600struct nfs4_lock_state;
1601#line 15
1602struct nfs4_lock_state;
1603#line 16 "include/linux/nfs_fs_i.h"
1604struct nfs4_lock_info {
1605   struct nfs4_lock_state *owner ;
1606};
1607#line 1138 "include/linux/fs.h"
1608struct fasync_struct;
1609#line 1138 "include/linux/fs.h"
1610struct __anonstruct_afs_155 {
1611   struct list_head link ;
1612   int state ;
1613};
1614#line 1138 "include/linux/fs.h"
1615union __anonunion_fl_u_154 {
1616   struct nfs_lock_info nfs_fl ;
1617   struct nfs4_lock_info nfs4_fl ;
1618   struct __anonstruct_afs_155 afs ;
1619};
1620#line 1138 "include/linux/fs.h"
1621struct file_lock {
1622   struct file_lock *fl_next ;
1623   struct list_head fl_link ;
1624   struct list_head fl_block ;
1625   fl_owner_t fl_owner ;
1626   unsigned int fl_flags ;
1627   unsigned char fl_type ;
1628   unsigned int fl_pid ;
1629   struct pid *fl_nspid ;
1630   wait_queue_head_t fl_wait ;
1631   struct file *fl_file ;
1632   loff_t fl_start ;
1633   loff_t fl_end ;
1634   struct fasync_struct *fl_fasync ;
1635   unsigned long fl_break_time ;
1636   unsigned long fl_downgrade_time ;
1637   struct file_lock_operations  const  *fl_ops ;
1638   struct lock_manager_operations  const  *fl_lmops ;
1639   union __anonunion_fl_u_154 fl_u ;
1640};
1641#line 1378 "include/linux/fs.h"
1642struct fasync_struct {
1643   spinlock_t fa_lock ;
1644   int magic ;
1645   int fa_fd ;
1646   struct fasync_struct *fa_next ;
1647   struct file *fa_file ;
1648   struct rcu_head fa_rcu ;
1649};
1650#line 1418
1651struct file_system_type;
1652#line 1418
1653struct super_operations;
1654#line 1418
1655struct xattr_handler;
1656#line 1418
1657struct mtd_info;
1658#line 1418 "include/linux/fs.h"
1659struct super_block {
1660   struct list_head s_list ;
1661   dev_t s_dev ;
1662   unsigned char s_dirt ;
1663   unsigned char s_blocksize_bits ;
1664   unsigned long s_blocksize ;
1665   loff_t s_maxbytes ;
1666   struct file_system_type *s_type ;
1667   struct super_operations  const  *s_op ;
1668   struct dquot_operations  const  *dq_op ;
1669   struct quotactl_ops  const  *s_qcop ;
1670   struct export_operations  const  *s_export_op ;
1671   unsigned long s_flags ;
1672   unsigned long s_magic ;
1673   struct dentry *s_root ;
1674   struct rw_semaphore s_umount ;
1675   struct mutex s_lock ;
1676   int s_count ;
1677   atomic_t s_active ;
1678   void *s_security ;
1679   struct xattr_handler  const  **s_xattr ;
1680   struct list_head s_inodes ;
1681   struct hlist_bl_head s_anon ;
1682   struct list_head *s_files ;
1683   struct list_head s_mounts ;
1684   struct list_head s_dentry_lru ;
1685   int s_nr_dentry_unused ;
1686   spinlock_t s_inode_lru_lock  __attribute__((__aligned__((1) <<  (6) ))) ;
1687   struct list_head s_inode_lru ;
1688   int s_nr_inodes_unused ;
1689   struct block_device *s_bdev ;
1690   struct backing_dev_info *s_bdi ;
1691   struct mtd_info *s_mtd ;
1692   struct hlist_node s_instances ;
1693   struct quota_info s_dquot ;
1694   int s_frozen ;
1695   wait_queue_head_t s_wait_unfrozen ;
1696   char s_id[32] ;
1697   u8 s_uuid[16] ;
1698   void *s_fs_info ;
1699   unsigned int s_max_links ;
1700   fmode_t s_mode ;
1701   u32 s_time_gran ;
1702   struct mutex s_vfs_rename_mutex ;
1703   char *s_subtype ;
1704   char *s_options ;
1705   struct dentry_operations  const  *s_d_op ;
1706   int cleancache_poolid ;
1707   struct shrinker s_shrink ;
1708   atomic_long_t s_remove_count ;
1709   int s_readonly_remount ;
1710};
1711#line 1567 "include/linux/fs.h"
1712struct fiemap_extent_info {
1713   unsigned int fi_flags ;
1714   unsigned int fi_extents_mapped ;
1715   unsigned int fi_extents_max ;
1716   struct fiemap_extent *fi_extents_start ;
1717};
1718#line 1609 "include/linux/fs.h"
1719struct file_operations {
1720   struct module *owner ;
1721   loff_t (*llseek)(struct file * , loff_t  , int  ) ;
1722   ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
1723   ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
1724   ssize_t (*aio_read)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1725                       loff_t  ) ;
1726   ssize_t (*aio_write)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1727                        loff_t  ) ;
1728   int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
1729                                                   loff_t  , u64  , unsigned int  ) ) ;
1730   unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1731   long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1732   long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1733   int (*mmap)(struct file * , struct vm_area_struct * ) ;
1734   int (*open)(struct inode * , struct file * ) ;
1735   int (*flush)(struct file * , fl_owner_t id ) ;
1736   int (*release)(struct inode * , struct file * ) ;
1737   int (*fsync)(struct file * , loff_t  , loff_t  , int datasync ) ;
1738   int (*aio_fsync)(struct kiocb * , int datasync ) ;
1739   int (*fasync)(int  , struct file * , int  ) ;
1740   int (*lock)(struct file * , int  , struct file_lock * ) ;
1741   ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
1742                       int  ) ;
1743   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
1744                                      unsigned long  , unsigned long  ) ;
1745   int (*check_flags)(int  ) ;
1746   int (*flock)(struct file * , int  , struct file_lock * ) ;
1747   ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t  ,
1748                           unsigned int  ) ;
1749   ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t  ,
1750                          unsigned int  ) ;
1751   int (*setlease)(struct file * , long  , struct file_lock ** ) ;
1752   long (*fallocate)(struct file *file , int mode , loff_t offset , loff_t len ) ;
1753};
1754#line 1639 "include/linux/fs.h"
1755struct inode_operations {
1756   struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1757   void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1758   int (*permission)(struct inode * , int  ) ;
1759   struct posix_acl *(*get_acl)(struct inode * , int  ) ;
1760   int (*readlink)(struct dentry * , char * , int  ) ;
1761   void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
1762   int (*create)(struct inode * , struct dentry * , umode_t  , struct nameidata * ) ;
1763   int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
1764   int (*unlink)(struct inode * , struct dentry * ) ;
1765   int (*symlink)(struct inode * , struct dentry * , char const   * ) ;
1766   int (*mkdir)(struct inode * , struct dentry * , umode_t  ) ;
1767   int (*rmdir)(struct inode * , struct dentry * ) ;
1768   int (*mknod)(struct inode * , struct dentry * , umode_t  , dev_t  ) ;
1769   int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
1770   void (*truncate)(struct inode * ) ;
1771   int (*setattr)(struct dentry * , struct iattr * ) ;
1772   int (*getattr)(struct vfsmount *mnt , struct dentry * , struct kstat * ) ;
1773   int (*setxattr)(struct dentry * , char const   * , void const   * , size_t  , int  ) ;
1774   ssize_t (*getxattr)(struct dentry * , char const   * , void * , size_t  ) ;
1775   ssize_t (*listxattr)(struct dentry * , char * , size_t  ) ;
1776   int (*removexattr)(struct dentry * , char const   * ) ;
1777   void (*truncate_range)(struct inode * , loff_t  , loff_t  ) ;
1778   int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 start , u64 len ) ;
1779} __attribute__((__aligned__((1) <<  (6) ))) ;
1780#line 1669
1781struct seq_file;
1782#line 1684 "include/linux/fs.h"
1783struct super_operations {
1784   struct inode *(*alloc_inode)(struct super_block *sb ) ;
1785   void (*destroy_inode)(struct inode * ) ;
1786   void (*dirty_inode)(struct inode * , int flags ) ;
1787   int (*write_inode)(struct inode * , struct writeback_control *wbc ) ;
1788   int (*drop_inode)(struct inode * ) ;
1789   void (*evict_inode)(struct inode * ) ;
1790   void (*put_super)(struct super_block * ) ;
1791   void (*write_super)(struct super_block * ) ;
1792   int (*sync_fs)(struct super_block *sb , int wait ) ;
1793   int (*freeze_fs)(struct super_block * ) ;
1794   int (*unfreeze_fs)(struct super_block * ) ;
1795   int (*statfs)(struct dentry * , struct kstatfs * ) ;
1796   int (*remount_fs)(struct super_block * , int * , char * ) ;
1797   void (*umount_begin)(struct super_block * ) ;
1798   int (*show_options)(struct seq_file * , struct dentry * ) ;
1799   int (*show_devname)(struct seq_file * , struct dentry * ) ;
1800   int (*show_path)(struct seq_file * , struct dentry * ) ;
1801   int (*show_stats)(struct seq_file * , struct dentry * ) ;
1802   ssize_t (*quota_read)(struct super_block * , int  , char * , size_t  , loff_t  ) ;
1803   ssize_t (*quota_write)(struct super_block * , int  , char const   * , size_t  ,
1804                          loff_t  ) ;
1805   int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t  ) ;
1806   int (*nr_cached_objects)(struct super_block * ) ;
1807   void (*free_cached_objects)(struct super_block * , int  ) ;
1808};
1809#line 1835 "include/linux/fs.h"
1810struct file_system_type {
1811   char const   *name ;
1812   int fs_flags ;
1813   struct dentry *(*mount)(struct file_system_type * , int  , char const   * , void * ) ;
1814   void (*kill_sb)(struct super_block * ) ;
1815   struct module *owner ;
1816   struct file_system_type *next ;
1817   struct hlist_head fs_supers ;
1818   struct lock_class_key s_lock_key ;
1819   struct lock_class_key s_umount_key ;
1820   struct lock_class_key s_vfs_rename_key ;
1821   struct lock_class_key i_lock_key ;
1822   struct lock_class_key i_mutex_key ;
1823   struct lock_class_key i_mutex_dir_key ;
1824};
1825#line 1250 "include/linux/input.h"
1826struct ff_device;
1827#line 1250
1828struct input_mt_slot;
1829#line 1250
1830struct input_handle;
1831#line 1250 "include/linux/input.h"
1832struct input_dev {
1833   char const   *name ;
1834   char const   *phys ;
1835   char const   *uniq ;
1836   struct input_id id ;
1837   unsigned long propbit[((32UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1838   unsigned long evbit[((32UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1839   unsigned long keybit[((768UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1840   unsigned long relbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1841   unsigned long absbit[((64UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1842   unsigned long mscbit[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1843   unsigned long ledbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1844   unsigned long sndbit[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1845   unsigned long ffbit[((128UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1846   unsigned long swbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1847   unsigned int hint_events_per_packet ;
1848   unsigned int keycodemax ;
1849   unsigned int keycodesize ;
1850   void *keycode ;
1851   int (*setkeycode)(struct input_dev *dev , struct input_keymap_entry  const  *ke ,
1852                     unsigned int *old_keycode ) ;
1853   int (*getkeycode)(struct input_dev *dev , struct input_keymap_entry *ke ) ;
1854   struct ff_device *ff ;
1855   unsigned int repeat_key ;
1856   struct timer_list timer ;
1857   int rep[2] ;
1858   struct input_mt_slot *mt ;
1859   int mtsize ;
1860   int slot ;
1861   int trkid ;
1862   struct input_absinfo *absinfo ;
1863   unsigned long key[((768UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1864   unsigned long led[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1865   unsigned long snd[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1866   unsigned long sw[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1867   int (*open)(struct input_dev *dev ) ;
1868   void (*close)(struct input_dev *dev ) ;
1869   int (*flush)(struct input_dev *dev , struct file *file ) ;
1870   int (*event)(struct input_dev *dev , unsigned int type , unsigned int code , int value ) ;
1871   struct input_handle *grab ;
1872   spinlock_t event_lock ;
1873   struct mutex mutex ;
1874   unsigned int users ;
1875   bool going_away ;
1876   bool sync ;
1877   struct device dev ;
1878   struct list_head h_list ;
1879   struct list_head node ;
1880};
1881#line 1370
1882struct input_handle;
1883#line 1409 "include/linux/input.h"
1884struct input_handler {
1885   void *private ;
1886   void (*event)(struct input_handle *handle , unsigned int type , unsigned int code ,
1887                 int value ) ;
1888   bool (*filter)(struct input_handle *handle , unsigned int type , unsigned int code ,
1889                  int value ) ;
1890   bool (*match)(struct input_handler *handler , struct input_dev *dev ) ;
1891   int (*connect)(struct input_handler *handler , struct input_dev *dev , struct input_device_id  const  *id ) ;
1892   void (*disconnect)(struct input_handle *handle ) ;
1893   void (*start)(struct input_handle *handle ) ;
1894   struct file_operations  const  *fops ;
1895   int minor ;
1896   char const   *name ;
1897   struct input_device_id  const  *id_table ;
1898   struct list_head h_list ;
1899   struct list_head node ;
1900};
1901#line 1442 "include/linux/input.h"
1902struct input_handle {
1903   void *private ;
1904   int open ;
1905   char const   *name ;
1906   struct input_dev *dev ;
1907   struct input_handler *handler ;
1908   struct list_head d_node ;
1909   struct list_head h_node ;
1910};
1911#line 1619 "include/linux/input.h"
1912struct ff_device {
1913   int (*upload)(struct input_dev *dev , struct ff_effect *effect , struct ff_effect *old ) ;
1914   int (*erase)(struct input_dev *dev , int effect_id ) ;
1915   int (*playback)(struct input_dev *dev , int effect_id , int value ) ;
1916   void (*set_gain)(struct input_dev *dev , u16 gain ) ;
1917   void (*set_autocenter)(struct input_dev *dev , u16 magnitude ) ;
1918   void (*destroy)(struct ff_device * ) ;
1919   void *private ;
1920   unsigned long ffbit[((128UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
1921   struct mutex mutex ;
1922   int max_effects ;
1923   struct ff_effect *effects ;
1924   struct file *effect_owners[] ;
1925};
1926#line 20 "include/linux/leds.h"
1927struct device;
1928#line 25
1929enum led_brightness {
1930    LED_OFF = 0,
1931    LED_HALF = 127,
1932    LED_FULL = 255
1933} ;
1934#line 31
1935struct led_trigger;
1936#line 31 "include/linux/leds.h"
1937struct led_classdev {
1938   char const   *name ;
1939   int brightness ;
1940   int max_brightness ;
1941   int flags ;
1942   void (*brightness_set)(struct led_classdev *led_cdev , enum led_brightness brightness ) ;
1943   enum led_brightness (*brightness_get)(struct led_classdev *led_cdev ) ;
1944   int (*blink_set)(struct led_classdev *led_cdev , unsigned long *delay_on , unsigned long *delay_off ) ;
1945   struct device *dev ;
1946   struct list_head node ;
1947   char const   *default_trigger ;
1948   unsigned long blink_delay_on ;
1949   unsigned long blink_delay_off ;
1950   struct timer_list blink_timer ;
1951   int blink_brightness ;
1952   struct rw_semaphore trigger_lock ;
1953   struct led_trigger *trigger ;
1954   struct list_head trig_list ;
1955   void *trigger_data ;
1956};
1957#line 122 "include/linux/leds.h"
1958struct led_trigger {
1959   char const   *name ;
1960   void (*activate)(struct led_classdev *led_cdev ) ;
1961   void (*deactivate)(struct led_classdev *led_cdev ) ;
1962   rwlock_t leddev_list_lock ;
1963   struct list_head led_cdevs ;
1964   struct list_head next_trig ;
1965};
1966#line 19 "include/linux/power_supply.h"
1967struct device;
1968#line 84
1969enum power_supply_property {
1970    POWER_SUPPLY_PROP_STATUS = 0,
1971    POWER_SUPPLY_PROP_CHARGE_TYPE = 1,
1972    POWER_SUPPLY_PROP_HEALTH = 2,
1973    POWER_SUPPLY_PROP_PRESENT = 3,
1974    POWER_SUPPLY_PROP_ONLINE = 4,
1975    POWER_SUPPLY_PROP_TECHNOLOGY = 5,
1976    POWER_SUPPLY_PROP_CYCLE_COUNT = 6,
1977    POWER_SUPPLY_PROP_VOLTAGE_MAX = 7,
1978    POWER_SUPPLY_PROP_VOLTAGE_MIN = 8,
1979    POWER_SUPPLY_PROP_VOLTAGE_MAX_DESIGN = 9,
1980    POWER_SUPPLY_PROP_VOLTAGE_MIN_DESIGN = 10,
1981    POWER_SUPPLY_PROP_VOLTAGE_NOW = 11,
1982    POWER_SUPPLY_PROP_VOLTAGE_AVG = 12,
1983    POWER_SUPPLY_PROP_CURRENT_MAX = 13,
1984    POWER_SUPPLY_PROP_CURRENT_NOW = 14,
1985    POWER_SUPPLY_PROP_CURRENT_AVG = 15,
1986    POWER_SUPPLY_PROP_POWER_NOW = 16,
1987    POWER_SUPPLY_PROP_POWER_AVG = 17,
1988    POWER_SUPPLY_PROP_CHARGE_FULL_DESIGN = 18,
1989    POWER_SUPPLY_PROP_CHARGE_EMPTY_DESIGN = 19,
1990    POWER_SUPPLY_PROP_CHARGE_FULL = 20,
1991    POWER_SUPPLY_PROP_CHARGE_EMPTY = 21,
1992    POWER_SUPPLY_PROP_CHARGE_NOW = 22,
1993    POWER_SUPPLY_PROP_CHARGE_AVG = 23,
1994    POWER_SUPPLY_PROP_CHARGE_COUNTER = 24,
1995    POWER_SUPPLY_PROP_ENERGY_FULL_DESIGN = 25,
1996    POWER_SUPPLY_PROP_ENERGY_EMPTY_DESIGN = 26,
1997    POWER_SUPPLY_PROP_ENERGY_FULL = 27,
1998    POWER_SUPPLY_PROP_ENERGY_EMPTY = 28,
1999    POWER_SUPPLY_PROP_ENERGY_NOW = 29,
2000    POWER_SUPPLY_PROP_ENERGY_AVG = 30,
2001    POWER_SUPPLY_PROP_CAPACITY = 31,
2002    POWER_SUPPLY_PROP_CAPACITY_LEVEL = 32,
2003    POWER_SUPPLY_PROP_TEMP = 33,
2004    POWER_SUPPLY_PROP_TEMP_AMBIENT = 34,
2005    POWER_SUPPLY_PROP_TIME_TO_EMPTY_NOW = 35,
2006    POWER_SUPPLY_PROP_TIME_TO_EMPTY_AVG = 36,
2007    POWER_SUPPLY_PROP_TIME_TO_FULL_NOW = 37,
2008    POWER_SUPPLY_PROP_TIME_TO_FULL_AVG = 38,
2009    POWER_SUPPLY_PROP_TYPE = 39,
2010    POWER_SUPPLY_PROP_SCOPE = 40,
2011    POWER_SUPPLY_PROP_MODEL_NAME = 41,
2012    POWER_SUPPLY_PROP_MANUFACTURER = 42,
2013    POWER_SUPPLY_PROP_SERIAL_NUMBER = 43
2014} ;
2015#line 133
2016enum power_supply_type {
2017    POWER_SUPPLY_TYPE_UNKNOWN = 0,
2018    POWER_SUPPLY_TYPE_BATTERY = 1,
2019    POWER_SUPPLY_TYPE_UPS = 2,
2020    POWER_SUPPLY_TYPE_MAINS = 3,
2021    POWER_SUPPLY_TYPE_USB = 4,
2022    POWER_SUPPLY_TYPE_USB_DCP = 5,
2023    POWER_SUPPLY_TYPE_USB_CDP = 6,
2024    POWER_SUPPLY_TYPE_USB_ACA = 7
2025} ;
2026#line 144 "include/linux/power_supply.h"
2027union power_supply_propval {
2028   int intval ;
2029   char const   *strval ;
2030};
2031#line 149 "include/linux/power_supply.h"
2032struct power_supply {
2033   char const   *name ;
2034   enum power_supply_type type ;
2035   enum power_supply_property *properties ;
2036   size_t num_properties ;
2037   char **supplied_to ;
2038   size_t num_supplicants ;
2039   int (*get_property)(struct power_supply *psy , enum power_supply_property psp ,
2040                       union power_supply_propval *val ) ;
2041   int (*set_property)(struct power_supply *psy , enum power_supply_property psp ,
2042                       union power_supply_propval  const  *val ) ;
2043   int (*property_is_writeable)(struct power_supply *psy , enum power_supply_property psp ) ;
2044   void (*external_power_changed)(struct power_supply *psy ) ;
2045   void (*set_charged)(struct power_supply *psy ) ;
2046   int use_for_apm ;
2047   struct device *dev ;
2048   struct work_struct changed_work ;
2049   struct led_trigger *charging_full_trig ;
2050   char *charging_full_trig_name ;
2051   struct led_trigger *charging_trig ;
2052   char *charging_trig_name ;
2053   struct led_trigger *full_trig ;
2054   char *full_trig_name ;
2055   struct led_trigger *online_trig ;
2056   char *online_trig_name ;
2057   struct led_trigger *charging_blink_full_solid_trig ;
2058   char *charging_blink_full_solid_trig_name ;
2059};
2060#line 367 "include/linux/hid.h"
2061struct hid_collection {
2062   unsigned int type ;
2063   unsigned int usage ;
2064   unsigned int level ;
2065};
2066#line 373 "include/linux/hid.h"
2067struct hid_usage {
2068   unsigned int hid ;
2069   unsigned int collection_index ;
2070   __u16 code ;
2071   __u8 type ;
2072   __s8 hat_min ;
2073   __s8 hat_max ;
2074   __s8 hat_dir ;
2075};
2076#line 384
2077struct hid_input;
2078#line 384
2079struct hid_input;
2080#line 386
2081struct hid_report;
2082#line 386 "include/linux/hid.h"
2083struct hid_field {
2084   unsigned int physical ;
2085   unsigned int logical ;
2086   unsigned int application ;
2087   struct hid_usage *usage ;
2088   unsigned int maxusage ;
2089   unsigned int flags ;
2090   unsigned int report_offset ;
2091   unsigned int report_size ;
2092   unsigned int report_count ;
2093   unsigned int report_type ;
2094   __s32 *value ;
2095   __s32 logical_minimum ;
2096   __s32 logical_maximum ;
2097   __s32 physical_minimum ;
2098   __s32 physical_maximum ;
2099   __s32 unit_exponent ;
2100   unsigned int unit ;
2101   struct hid_report *report ;
2102   unsigned int index ;
2103   struct hid_input *hidinput ;
2104   __u16 dpad ;
2105};
2106#line 413
2107struct hid_device;
2108#line 413 "include/linux/hid.h"
2109struct hid_report {
2110   struct list_head list ;
2111   unsigned int id ;
2112   unsigned int type ;
2113   struct hid_field *field[128] ;
2114   unsigned int maxfield ;
2115   unsigned int size ;
2116   struct hid_device *device ;
2117};
2118#line 423 "include/linux/hid.h"
2119struct hid_report_enum {
2120   unsigned int numbered ;
2121   struct list_head report_list ;
2122   struct hid_report *report_id_hash[256] ;
2123};
2124#line 454 "include/linux/hid.h"
2125struct hid_input {
2126   struct list_head list ;
2127   struct hid_report *report ;
2128   struct input_dev *input ;
2129};
2130#line 460
2131enum hid_type {
2132    HID_TYPE_OTHER = 0,
2133    HID_TYPE_USBMOUSE = 1,
2134    HID_TYPE_USBNONE = 2
2135} ;
2136#line 466
2137struct hid_driver;
2138#line 466
2139struct hid_driver;
2140#line 467
2141struct hid_ll_driver;
2142#line 467
2143struct hid_ll_driver;
2144#line 469 "include/linux/hid.h"
2145struct hid_device {
2146   __u8 *rdesc ;
2147   unsigned int rsize ;
2148   struct hid_collection *collection ;
2149   unsigned int collection_size ;
2150   unsigned int maxcollection ;
2151   unsigned int maxapplication ;
2152   __u16 bus ;
2153   __u32 vendor ;
2154   __u32 product ;
2155   __u32 version ;
2156   enum hid_type type ;
2157   unsigned int country ;
2158   struct hid_report_enum report_enum[3] ;
2159   struct semaphore driver_lock ;
2160   struct device dev ;
2161   struct hid_driver *driver ;
2162   struct hid_ll_driver *ll_driver ;
2163   unsigned int status ;
2164   unsigned int claimed ;
2165   unsigned int quirks ;
2166   struct list_head inputs ;
2167   void *hiddev ;
2168   void *hidraw ;
2169   int minor ;
2170   int open ;
2171   char name[128] ;
2172   char phys[64] ;
2173   char uniq[64] ;
2174   void *driver_data ;
2175   int (*ff_init)(struct hid_device * ) ;
2176   int (*hiddev_connect)(struct hid_device * , unsigned int  ) ;
2177   void (*hiddev_disconnect)(struct hid_device * ) ;
2178   void (*hiddev_hid_event)(struct hid_device * , struct hid_field *field , struct hid_usage * ,
2179                            __s32  ) ;
2180   void (*hiddev_report_event)(struct hid_device * , struct hid_report * ) ;
2181   int (*hid_get_raw_report)(struct hid_device * , unsigned char  , __u8 * , size_t  ,
2182                             unsigned char  ) ;
2183   int (*hid_output_raw_report)(struct hid_device * , __u8 * , size_t  , unsigned char  ) ;
2184   unsigned short debug ;
2185   struct dentry *debug_dir ;
2186   struct dentry *debug_rdesc ;
2187   struct dentry *debug_events ;
2188   struct list_head debug_list ;
2189   wait_queue_head_t debug_wait ;
2190};
2191#line 595 "include/linux/hid.h"
2192struct hid_report_id {
2193   __u32 report_type ;
2194};
2195#line 598 "include/linux/hid.h"
2196struct hid_usage_id {
2197   __u32 usage_hid ;
2198   __u32 usage_type ;
2199   __u32 usage_code ;
2200};
2201#line 638 "include/linux/hid.h"
2202struct hid_driver {
2203   char *name ;
2204   struct hid_device_id  const  *id_table ;
2205   struct list_head dyn_list ;
2206   spinlock_t dyn_lock ;
2207   int (*probe)(struct hid_device *dev , struct hid_device_id  const  *id ) ;
2208   void (*remove)(struct hid_device *dev ) ;
2209   struct hid_report_id  const  *report_table ;
2210   int (*raw_event)(struct hid_device *hdev , struct hid_report *report , u8 *data ,
2211                    int size ) ;
2212   struct hid_usage_id  const  *usage_table ;
2213   int (*event)(struct hid_device *hdev , struct hid_field *field , struct hid_usage *usage ,
2214                __s32 value ) ;
2215   __u8 *(*report_fixup)(struct hid_device *hdev , __u8 *buf , unsigned int *size ) ;
2216   int (*input_mapping)(struct hid_device *hdev , struct hid_input *hidinput , struct hid_field *field ,
2217                        struct hid_usage *usage , unsigned long **bit , int *max ) ;
2218   int (*input_mapped)(struct hid_device *hdev , struct hid_input *hidinput , struct hid_field *field ,
2219                       struct hid_usage *usage , unsigned long **bit , int *max ) ;
2220   void (*feature_mapping)(struct hid_device *hdev , struct hid_field *field , struct hid_usage *usage ) ;
2221   int (*suspend)(struct hid_device *hdev , pm_message_t message ) ;
2222   int (*resume)(struct hid_device *hdev ) ;
2223   int (*reset_resume)(struct hid_device *hdev ) ;
2224   struct device_driver driver ;
2225};
2226#line 686 "include/linux/hid.h"
2227struct hid_ll_driver {
2228   int (*start)(struct hid_device *hdev ) ;
2229   void (*stop)(struct hid_device *hdev ) ;
2230   int (*open)(struct hid_device *hdev ) ;
2231   void (*close)(struct hid_device *hdev ) ;
2232   int (*power)(struct hid_device *hdev , int level ) ;
2233   int (*hidinput_input_event)(struct input_dev *idev , unsigned int type , unsigned int code ,
2234                               int value ) ;
2235   int (*parse)(struct hid_device *hdev ) ;
2236};
2237#line 29 "include/linux/sysctl.h"
2238struct completion;
2239#line 48 "include/linux/kmod.h"
2240struct cred;
2241#line 49
2242struct file;
2243#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
2244struct task_struct;
2245#line 18 "include/linux/elf.h"
2246typedef __u64 Elf64_Addr;
2247#line 19 "include/linux/elf.h"
2248typedef __u16 Elf64_Half;
2249#line 23 "include/linux/elf.h"
2250typedef __u32 Elf64_Word;
2251#line 24 "include/linux/elf.h"
2252typedef __u64 Elf64_Xword;
2253#line 194 "include/linux/elf.h"
2254struct elf64_sym {
2255   Elf64_Word st_name ;
2256   unsigned char st_info ;
2257   unsigned char st_other ;
2258   Elf64_Half st_shndx ;
2259   Elf64_Addr st_value ;
2260   Elf64_Xword st_size ;
2261};
2262#line 194 "include/linux/elf.h"
2263typedef struct elf64_sym Elf64_Sym;
2264#line 438
2265struct file;
2266#line 39 "include/linux/moduleparam.h"
2267struct kernel_param;
2268#line 39
2269struct kernel_param;
2270#line 41 "include/linux/moduleparam.h"
2271struct kernel_param_ops {
2272   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
2273   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
2274   void (*free)(void *arg ) ;
2275};
2276#line 50
2277struct kparam_string;
2278#line 50
2279struct kparam_array;
2280#line 50 "include/linux/moduleparam.h"
2281union __anonunion____missing_field_name_225 {
2282   void *arg ;
2283   struct kparam_string  const  *str ;
2284   struct kparam_array  const  *arr ;
2285};
2286#line 50 "include/linux/moduleparam.h"
2287struct kernel_param {
2288   char const   *name ;
2289   struct kernel_param_ops  const  *ops ;
2290   u16 perm ;
2291   s16 level ;
2292   union __anonunion____missing_field_name_225 __annonCompField35 ;
2293};
2294#line 63 "include/linux/moduleparam.h"
2295struct kparam_string {
2296   unsigned int maxlen ;
2297   char *string ;
2298};
2299#line 69 "include/linux/moduleparam.h"
2300struct kparam_array {
2301   unsigned int max ;
2302   unsigned int elemsize ;
2303   unsigned int *num ;
2304   struct kernel_param_ops  const  *ops ;
2305   void *elem ;
2306};
2307#line 445
2308struct module;
2309#line 80 "include/linux/jump_label.h"
2310struct module;
2311#line 143 "include/linux/jump_label.h"
2312struct static_key {
2313   atomic_t enabled ;
2314};
2315#line 22 "include/linux/tracepoint.h"
2316struct module;
2317#line 23
2318struct tracepoint;
2319#line 23
2320struct tracepoint;
2321#line 25 "include/linux/tracepoint.h"
2322struct tracepoint_func {
2323   void *func ;
2324   void *data ;
2325};
2326#line 30 "include/linux/tracepoint.h"
2327struct tracepoint {
2328   char const   *name ;
2329   struct static_key key ;
2330   void (*regfunc)(void) ;
2331   void (*unregfunc)(void) ;
2332   struct tracepoint_func *funcs ;
2333};
2334#line 19 "include/linux/export.h"
2335struct kernel_symbol {
2336   unsigned long value ;
2337   char const   *name ;
2338};
2339#line 8 "include/asm-generic/module.h"
2340struct mod_arch_specific {
2341
2342};
2343#line 35 "include/linux/module.h"
2344struct module;
2345#line 37
2346struct module_param_attrs;
2347#line 37 "include/linux/module.h"
2348struct module_kobject {
2349   struct kobject kobj ;
2350   struct module *mod ;
2351   struct kobject *drivers_dir ;
2352   struct module_param_attrs *mp ;
2353};
2354#line 44 "include/linux/module.h"
2355struct module_attribute {
2356   struct attribute attr ;
2357   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
2358   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
2359                    size_t count ) ;
2360   void (*setup)(struct module * , char const   * ) ;
2361   int (*test)(struct module * ) ;
2362   void (*free)(struct module * ) ;
2363};
2364#line 71
2365struct exception_table_entry;
2366#line 71
2367struct exception_table_entry;
2368#line 199
2369enum module_state {
2370    MODULE_STATE_LIVE = 0,
2371    MODULE_STATE_COMING = 1,
2372    MODULE_STATE_GOING = 2
2373} ;
2374#line 215 "include/linux/module.h"
2375struct module_ref {
2376   unsigned long incs ;
2377   unsigned long decs ;
2378} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
2379#line 220
2380struct module_sect_attrs;
2381#line 220
2382struct module_notes_attrs;
2383#line 220
2384struct ftrace_event_call;
2385#line 220 "include/linux/module.h"
2386struct module {
2387   enum module_state state ;
2388   struct list_head list ;
2389   char name[64UL - sizeof(unsigned long )] ;
2390   struct module_kobject mkobj ;
2391   struct module_attribute *modinfo_attrs ;
2392   char const   *version ;
2393   char const   *srcversion ;
2394   struct kobject *holders_dir ;
2395   struct kernel_symbol  const  *syms ;
2396   unsigned long const   *crcs ;
2397   unsigned int num_syms ;
2398   struct kernel_param *kp ;
2399   unsigned int num_kp ;
2400   unsigned int num_gpl_syms ;
2401   struct kernel_symbol  const  *gpl_syms ;
2402   unsigned long const   *gpl_crcs ;
2403   struct kernel_symbol  const  *unused_syms ;
2404   unsigned long const   *unused_crcs ;
2405   unsigned int num_unused_syms ;
2406   unsigned int num_unused_gpl_syms ;
2407   struct kernel_symbol  const  *unused_gpl_syms ;
2408   unsigned long const   *unused_gpl_crcs ;
2409   struct kernel_symbol  const  *gpl_future_syms ;
2410   unsigned long const   *gpl_future_crcs ;
2411   unsigned int num_gpl_future_syms ;
2412   unsigned int num_exentries ;
2413   struct exception_table_entry *extable ;
2414   int (*init)(void) ;
2415   void *module_init ;
2416   void *module_core ;
2417   unsigned int init_size ;
2418   unsigned int core_size ;
2419   unsigned int init_text_size ;
2420   unsigned int core_text_size ;
2421   unsigned int init_ro_size ;
2422   unsigned int core_ro_size ;
2423   struct mod_arch_specific arch ;
2424   unsigned int taints ;
2425   unsigned int num_bugs ;
2426   struct list_head bug_list ;
2427   struct bug_entry *bug_table ;
2428   Elf64_Sym *symtab ;
2429   Elf64_Sym *core_symtab ;
2430   unsigned int num_symtab ;
2431   unsigned int core_num_syms ;
2432   char *strtab ;
2433   char *core_strtab ;
2434   struct module_sect_attrs *sect_attrs ;
2435   struct module_notes_attrs *notes_attrs ;
2436   char *args ;
2437   void *percpu ;
2438   unsigned int percpu_size ;
2439   unsigned int num_tracepoints ;
2440   struct tracepoint * const  *tracepoints_ptrs ;
2441   unsigned int num_trace_bprintk_fmt ;
2442   char const   **trace_bprintk_fmt_start ;
2443   struct ftrace_event_call **trace_events ;
2444   unsigned int num_trace_events ;
2445   struct list_head source_list ;
2446   struct list_head target_list ;
2447   struct task_struct *waiter ;
2448   void (*exit)(void) ;
2449   struct module_ref *refptr ;
2450   ctor_fn_t *ctors ;
2451   unsigned int num_ctors ;
2452};
2453#line 37 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
2454struct wacom_data {
2455   __u16 tool ;
2456   __u16 butstate ;
2457   __u8 whlstate ;
2458   __u8 features ;
2459   __u32 id ;
2460   __u32 serial ;
2461   unsigned char high_speed ;
2462   int battery_capacity ;
2463   struct power_supply battery ;
2464   struct power_supply ac ;
2465};
2466#line 602 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
2467struct __anonstruct_227 {
2468   int  : 0 ;
2469};
2470#line 619 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
2471struct __anonstruct_228 {
2472   int  : 0 ;
2473};
2474#line 1 "<compiler builtins>"
2475long __builtin_expect(long val , long res ) ;
2476#line 82 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
2477__inline static void __set_bit(int nr , unsigned long volatile   *addr )  __attribute__((__no_instrument_function__)) ;
2478#line 82 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
2479__inline static void __set_bit(int nr , unsigned long volatile   *addr ) 
2480{ long volatile   *__cil_tmp3 ;
2481
2482  {
2483#line 84
2484  __cil_tmp3 = (long volatile   *)addr;
2485#line 84
2486  __asm__  volatile   ("bts %1,%0": "+m" (*__cil_tmp3): "Ir" (nr): "memory");
2487#line 85
2488  return;
2489}
2490}
2491#line 100 "include/linux/printk.h"
2492extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
2493#line 320 "include/linux/kernel.h"
2494extern int ( /* format attribute */  sprintf)(char *buf , char const   *fmt  , ...) ;
2495#line 322
2496extern int ( /* format attribute */  snprintf)(char *buf , size_t size , char const   *fmt 
2497                                               , ...) ;
2498#line 334
2499extern int ( /* format attribute */  sscanf)(char const   * , char const   *  , ...) ;
2500#line 84 "include/linux/string.h"
2501extern __kernel_size_t strnlen(char const   * , __kernel_size_t  ) ;
2502#line 152 "include/linux/mutex.h"
2503void mutex_lock(struct mutex *lock ) ;
2504#line 153
2505int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
2506#line 154
2507int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
2508#line 168
2509int mutex_trylock(struct mutex *lock ) ;
2510#line 169
2511void mutex_unlock(struct mutex *lock ) ;
2512#line 170
2513int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
2514#line 507 "include/linux/device.h"
2515extern int device_create_file(struct device *device , struct device_attribute  const  *entry ) ;
2516#line 509
2517extern void device_remove_file(struct device *dev , struct device_attribute  const  *attr ) ;
2518#line 792
2519extern void *dev_get_drvdata(struct device  const  *dev ) ;
2520#line 793
2521extern int dev_set_drvdata(struct device *dev , void *data ) ;
2522#line 891
2523extern int ( /* format attribute */  dev_err)(struct device  const  *dev , char const   *fmt 
2524                                              , ...) ;
2525#line 893
2526extern int ( /* format attribute */  dev_warn)(struct device  const  *dev , char const   *fmt 
2527                                               , ...) ;
2528#line 161 "include/linux/slab.h"
2529extern void kfree(void const   * ) ;
2530#line 221 "include/linux/slub_def.h"
2531extern void *__kmalloc(size_t size , gfp_t flags ) ;
2532#line 268
2533__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2534                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2535#line 268 "include/linux/slub_def.h"
2536__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2537                                                                    gfp_t flags ) 
2538{ void *tmp___2 ;
2539
2540  {
2541  {
2542#line 283
2543  tmp___2 = __kmalloc(size, flags);
2544  }
2545#line 283
2546  return (tmp___2);
2547}
2548}
2549#line 349 "include/linux/slab.h"
2550__inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2551#line 349 "include/linux/slab.h"
2552__inline static void *kzalloc(size_t size , gfp_t flags ) 
2553{ void *tmp ;
2554  unsigned int __cil_tmp4 ;
2555
2556  {
2557  {
2558#line 351
2559  __cil_tmp4 = flags | 32768U;
2560#line 351
2561  tmp = kmalloc(size, __cil_tmp4);
2562  }
2563#line 351
2564  return (tmp);
2565}
2566}
2567#line 1502 "include/linux/input.h"
2568extern void input_event(struct input_dev *dev , unsigned int type , unsigned int code ,
2569                        int value ) ;
2570#line 1505
2571__inline static void input_report_key(struct input_dev *dev , unsigned int code ,
2572                                      int value )  __attribute__((__no_instrument_function__)) ;
2573#line 1505 "include/linux/input.h"
2574__inline static void input_report_key(struct input_dev *dev , unsigned int code ,
2575                                      int value ) 
2576{ int __cil_tmp4 ;
2577  int __cil_tmp5 ;
2578
2579  {
2580  {
2581#line 1507
2582  __cil_tmp4 = ! value;
2583#line 1507
2584  __cil_tmp5 = ! __cil_tmp4;
2585#line 1507
2586  input_event(dev, 1U, code, __cil_tmp5);
2587  }
2588#line 1508
2589  return;
2590}
2591}
2592#line 1510
2593__inline static void input_report_rel(struct input_dev *dev , unsigned int code ,
2594                                      int value )  __attribute__((__no_instrument_function__)) ;
2595#line 1510 "include/linux/input.h"
2596__inline static void input_report_rel(struct input_dev *dev , unsigned int code ,
2597                                      int value ) 
2598{ 
2599
2600  {
2601  {
2602#line 1512
2603  input_event(dev, 2U, code, value);
2604  }
2605#line 1513
2606  return;
2607}
2608}
2609#line 1515
2610__inline static void input_report_abs(struct input_dev *dev , unsigned int code ,
2611                                      int value )  __attribute__((__no_instrument_function__)) ;
2612#line 1515 "include/linux/input.h"
2613__inline static void input_report_abs(struct input_dev *dev , unsigned int code ,
2614                                      int value ) 
2615{ 
2616
2617  {
2618  {
2619#line 1517
2620  input_event(dev, 3U, code, value);
2621  }
2622#line 1518
2623  return;
2624}
2625}
2626#line 1530
2627__inline static void input_sync(struct input_dev *dev )  __attribute__((__no_instrument_function__)) ;
2628#line 1530 "include/linux/input.h"
2629__inline static void input_sync(struct input_dev *dev ) 
2630{ 
2631
2632  {
2633  {
2634#line 1532
2635  input_event(dev, 0U, 0U, 0);
2636  }
2637#line 1533
2638  return;
2639}
2640}
2641#line 1540
2642extern void input_set_capability(struct input_dev *dev , unsigned int type , unsigned int code ) ;
2643#line 1558
2644extern void input_set_abs_params(struct input_dev *dev , unsigned int axis , int min ,
2645                                 int max , int fuzz , int flat ) ;
2646#line 1578
2647__inline static int input_abs_get_max(struct input_dev *dev , unsigned int axis )  __attribute__((__no_instrument_function__)) ;
2648#line 1578 "include/linux/input.h"
2649__inline static int input_abs_get_max(struct input_dev *dev , unsigned int axis ) 
2650{ __s32 tmp ;
2651  unsigned long __cil_tmp4 ;
2652  unsigned long __cil_tmp5 ;
2653  unsigned long __cil_tmp6 ;
2654  unsigned long __cil_tmp7 ;
2655  struct input_absinfo *__cil_tmp8 ;
2656  struct input_absinfo *__cil_tmp9 ;
2657  unsigned long __cil_tmp10 ;
2658  unsigned long __cil_tmp11 ;
2659
2660  {
2661  {
2662#line 1578
2663  __cil_tmp4 = (unsigned long )dev;
2664#line 1578
2665  __cil_tmp5 = __cil_tmp4 + 376;
2666#line 1578
2667  if (*((struct input_absinfo **)__cil_tmp5)) {
2668#line 1578
2669    __cil_tmp6 = (unsigned long )dev;
2670#line 1578
2671    __cil_tmp7 = __cil_tmp6 + 376;
2672#line 1578
2673    __cil_tmp8 = *((struct input_absinfo **)__cil_tmp7);
2674#line 1578
2675    __cil_tmp9 = __cil_tmp8 + axis;
2676#line 1578
2677    __cil_tmp10 = (unsigned long )__cil_tmp9;
2678#line 1578
2679    __cil_tmp11 = __cil_tmp10 + 8;
2680#line 1578
2681    tmp = *((__s32 *)__cil_tmp11);
2682  } else {
2683#line 1578
2684    tmp = 0;
2685  }
2686  }
2687#line 1578
2688  return (tmp);
2689}
2690}
2691#line 220 "include/linux/power_supply.h"
2692extern int power_supply_register(struct device *parent , struct power_supply *psy ) ;
2693#line 222
2694extern void power_supply_unregister(struct power_supply *psy ) ;
2695#line 223
2696extern int power_supply_powers(struct power_supply *psy , struct device *dev ) ;
2697#line 543 "include/linux/hid.h"
2698__inline static void *hid_get_drvdata(struct hid_device *hdev )  __attribute__((__no_instrument_function__)) ;
2699#line 543 "include/linux/hid.h"
2700__inline static void *hid_get_drvdata(struct hid_device *hdev ) 
2701{ void *tmp ;
2702  unsigned long __cil_tmp3 ;
2703  unsigned long __cil_tmp4 ;
2704  struct device *__cil_tmp5 ;
2705  struct device  const  *__cil_tmp6 ;
2706
2707  {
2708  {
2709#line 545
2710  __cil_tmp3 = (unsigned long )hdev;
2711#line 545
2712  __cil_tmp4 = __cil_tmp3 + 6328;
2713#line 545
2714  __cil_tmp5 = (struct device *)__cil_tmp4;
2715#line 545
2716  __cil_tmp6 = (struct device  const  *)__cil_tmp5;
2717#line 545
2718  tmp = dev_get_drvdata(__cil_tmp6);
2719  }
2720#line 545
2721  return (tmp);
2722}
2723}
2724#line 548
2725__inline static void hid_set_drvdata(struct hid_device *hdev , void *data )  __attribute__((__no_instrument_function__)) ;
2726#line 548 "include/linux/hid.h"
2727__inline static void hid_set_drvdata(struct hid_device *hdev , void *data ) 
2728{ unsigned long __cil_tmp3 ;
2729  unsigned long __cil_tmp4 ;
2730  struct device *__cil_tmp5 ;
2731
2732  {
2733  {
2734#line 550
2735  __cil_tmp3 = (unsigned long )hdev;
2736#line 550
2737  __cil_tmp4 = __cil_tmp3 + 6328;
2738#line 550
2739  __cil_tmp5 = (struct device *)__cil_tmp4;
2740#line 550
2741  dev_set_drvdata(__cil_tmp5, data);
2742  }
2743#line 551
2744  return;
2745}
2746}
2747#line 715
2748extern int __attribute__((__warn_unused_result__))  __hid_register_driver(struct hid_driver * ,
2749                                                                          struct module * ,
2750                                                                          char const   *mod_name ) ;
2751#line 722
2752extern void hid_unregister_driver(struct hid_driver * ) ;
2753#line 739
2754extern int hid_connect(struct hid_device *hid , unsigned int connect_mask ) ;
2755#line 740
2756extern void hid_disconnect(struct hid_device *hid ) ;
2757#line 806
2758__inline static int __attribute__((__warn_unused_result__))  hid_parse(struct hid_device *hdev )  __attribute__((__no_instrument_function__)) ;
2759#line 806 "include/linux/hid.h"
2760__inline static int __attribute__((__warn_unused_result__))  hid_parse(struct hid_device *hdev ) 
2761{ int ret ;
2762  unsigned long __cil_tmp3 ;
2763  unsigned long __cil_tmp4 ;
2764  unsigned int __cil_tmp5 ;
2765  unsigned long __cil_tmp6 ;
2766  unsigned long __cil_tmp7 ;
2767  struct hid_ll_driver *__cil_tmp8 ;
2768  unsigned long __cil_tmp9 ;
2769  unsigned long __cil_tmp10 ;
2770  int (*__cil_tmp11)(struct hid_device *hdev ) ;
2771  unsigned long __cil_tmp12 ;
2772  unsigned long __cil_tmp13 ;
2773  unsigned long __cil_tmp14 ;
2774  unsigned long __cil_tmp15 ;
2775  unsigned int __cil_tmp16 ;
2776
2777  {
2778  {
2779#line 810
2780  __cil_tmp3 = (unsigned long )hdev;
2781#line 810
2782  __cil_tmp4 = __cil_tmp3 + 7112;
2783#line 810
2784  __cil_tmp5 = *((unsigned int *)__cil_tmp4);
2785#line 810
2786  if (__cil_tmp5 & 2U) {
2787#line 811
2788    return (0);
2789  } else {
2790
2791  }
2792  }
2793  {
2794#line 813
2795  __cil_tmp6 = (unsigned long )hdev;
2796#line 813
2797  __cil_tmp7 = __cil_tmp6 + 7104;
2798#line 813
2799  __cil_tmp8 = *((struct hid_ll_driver **)__cil_tmp7);
2800#line 813
2801  __cil_tmp9 = (unsigned long )__cil_tmp8;
2802#line 813
2803  __cil_tmp10 = __cil_tmp9 + 48;
2804#line 813
2805  __cil_tmp11 = *((int (**)(struct hid_device *hdev ))__cil_tmp10);
2806#line 813
2807  ret = (*__cil_tmp11)(hdev);
2808  }
2809#line 814
2810  if (! ret) {
2811#line 815
2812    __cil_tmp12 = (unsigned long )hdev;
2813#line 815
2814    __cil_tmp13 = __cil_tmp12 + 7112;
2815#line 815
2816    __cil_tmp14 = (unsigned long )hdev;
2817#line 815
2818    __cil_tmp15 = __cil_tmp14 + 7112;
2819#line 815
2820    __cil_tmp16 = *((unsigned int *)__cil_tmp15);
2821#line 815
2822    *((unsigned int *)__cil_tmp13) = __cil_tmp16 | 2U;
2823  } else {
2824
2825  }
2826#line 817
2827  return (ret);
2828}
2829}
2830#line 830
2831__inline static int __attribute__((__warn_unused_result__))  hid_hw_start(struct hid_device *hdev ,
2832                                                                          unsigned int connect_mask )  __attribute__((__no_instrument_function__)) ;
2833#line 830 "include/linux/hid.h"
2834__inline static int __attribute__((__warn_unused_result__))  hid_hw_start(struct hid_device *hdev ,
2835                                                                          unsigned int connect_mask ) 
2836{ int ret ;
2837  int tmp ;
2838  unsigned long __cil_tmp5 ;
2839  unsigned long __cil_tmp6 ;
2840  struct hid_ll_driver *__cil_tmp7 ;
2841  int (*__cil_tmp8)(struct hid_device *hdev ) ;
2842  unsigned long __cil_tmp9 ;
2843  unsigned long __cil_tmp10 ;
2844  struct hid_ll_driver *__cil_tmp11 ;
2845  unsigned long __cil_tmp12 ;
2846  unsigned long __cil_tmp13 ;
2847  void (*__cil_tmp14)(struct hid_device *hdev ) ;
2848
2849  {
2850  {
2851#line 833
2852  __cil_tmp5 = (unsigned long )hdev;
2853#line 833
2854  __cil_tmp6 = __cil_tmp5 + 7104;
2855#line 833
2856  __cil_tmp7 = *((struct hid_ll_driver **)__cil_tmp6);
2857#line 833
2858  __cil_tmp8 = *((int (**)(struct hid_device *hdev ))__cil_tmp7);
2859#line 833
2860  tmp = (*__cil_tmp8)(hdev);
2861#line 833
2862  ret = tmp;
2863  }
2864#line 834
2865  if (ret) {
2866#line 835
2867    return (ret);
2868  } else
2869#line 834
2870  if (! connect_mask) {
2871#line 835
2872    return (ret);
2873  } else {
2874
2875  }
2876  {
2877#line 836
2878  ret = hid_connect(hdev, connect_mask);
2879  }
2880#line 837
2881  if (ret) {
2882    {
2883#line 838
2884    __cil_tmp9 = (unsigned long )hdev;
2885#line 838
2886    __cil_tmp10 = __cil_tmp9 + 7104;
2887#line 838
2888    __cil_tmp11 = *((struct hid_ll_driver **)__cil_tmp10);
2889#line 838
2890    __cil_tmp12 = (unsigned long )__cil_tmp11;
2891#line 838
2892    __cil_tmp13 = __cil_tmp12 + 8;
2893#line 838
2894    __cil_tmp14 = *((void (**)(struct hid_device *hdev ))__cil_tmp13);
2895#line 838
2896    (*__cil_tmp14)(hdev);
2897    }
2898  } else {
2899
2900  }
2901#line 839
2902  return (ret);
2903}
2904}
2905#line 850
2906__inline static void hid_hw_stop(struct hid_device *hdev )  __attribute__((__no_instrument_function__)) ;
2907#line 850 "include/linux/hid.h"
2908__inline static void hid_hw_stop(struct hid_device *hdev ) 
2909{ unsigned long __cil_tmp2 ;
2910  unsigned long __cil_tmp3 ;
2911  struct hid_ll_driver *__cil_tmp4 ;
2912  unsigned long __cil_tmp5 ;
2913  unsigned long __cil_tmp6 ;
2914  void (*__cil_tmp7)(struct hid_device *hdev ) ;
2915
2916  {
2917  {
2918#line 852
2919  hid_disconnect(hdev);
2920#line 853
2921  __cil_tmp2 = (unsigned long )hdev;
2922#line 853
2923  __cil_tmp3 = __cil_tmp2 + 7104;
2924#line 853
2925  __cil_tmp4 = *((struct hid_ll_driver **)__cil_tmp3);
2926#line 853
2927  __cil_tmp5 = (unsigned long )__cil_tmp4;
2928#line 853
2929  __cil_tmp6 = __cil_tmp5 + 8;
2930#line 853
2931  __cil_tmp7 = *((void (**)(struct hid_device *hdev ))__cil_tmp6);
2932#line 853
2933  (*__cil_tmp7)(hdev);
2934  }
2935#line 854
2936  return;
2937}
2938}
2939#line 26 "include/linux/export.h"
2940extern struct module __this_module ;
2941#line 67 "include/linux/module.h"
2942int init_module(void) ;
2943#line 68
2944void cleanup_module(void) ;
2945#line 54 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
2946static unsigned short batcap[8]  = 
2947#line 54 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
2948  {      (unsigned short)1,      (unsigned short)15,      (unsigned short)25,      (unsigned short)35, 
2949        (unsigned short)50,      (unsigned short)70,      (unsigned short)100,      (unsigned short)0};
2950#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
2951static enum power_supply_property wacom_battery_props[3]  = {      (enum power_supply_property )3,      (enum power_supply_property )31,      (enum power_supply_property )40};
2952#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
2953static enum power_supply_property wacom_ac_props[3]  = {      (enum power_supply_property )3,      (enum power_supply_property )4,      (enum power_supply_property )40};
2954#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
2955static int wacom_battery_get_property(struct power_supply *psy , enum power_supply_property psp ,
2956                                      union power_supply_propval *val ) 
2957{ struct wacom_data *wdata ;
2958  struct power_supply  const  *__mptr ;
2959  int power_state ;
2960  int ret ;
2961  struct wacom_data *__cil_tmp8 ;
2962  unsigned long __cil_tmp9 ;
2963  unsigned long __cil_tmp10 ;
2964  struct power_supply *__cil_tmp11 ;
2965  unsigned int __cil_tmp12 ;
2966  char *__cil_tmp13 ;
2967  char *__cil_tmp14 ;
2968  unsigned long __cil_tmp15 ;
2969  unsigned long __cil_tmp16 ;
2970  int __cil_tmp17 ;
2971  unsigned long __cil_tmp18 ;
2972  unsigned long __cil_tmp19 ;
2973  unsigned short __cil_tmp20 ;
2974
2975  {
2976#line 72
2977  __mptr = (struct power_supply  const  *)psy;
2978#line 72
2979  __cil_tmp8 = (struct wacom_data *)0;
2980#line 72
2981  __cil_tmp9 = (unsigned long )__cil_tmp8;
2982#line 72
2983  __cil_tmp10 = __cil_tmp9 + 24;
2984#line 72
2985  __cil_tmp11 = (struct power_supply *)__cil_tmp10;
2986#line 72
2987  __cil_tmp12 = (unsigned int )__cil_tmp11;
2988#line 72
2989  __cil_tmp13 = (char *)__mptr;
2990#line 72
2991  __cil_tmp14 = __cil_tmp13 - __cil_tmp12;
2992#line 72
2993  wdata = (struct wacom_data *)__cil_tmp14;
2994#line 74
2995  __cil_tmp15 = (unsigned long )wdata;
2996#line 74
2997  __cil_tmp16 = __cil_tmp15 + 20;
2998#line 74
2999  __cil_tmp17 = *((int *)__cil_tmp16);
3000#line 74
3001  __cil_tmp18 = __cil_tmp17 * 2UL;
3002#line 74
3003  __cil_tmp19 = (unsigned long )(batcap) + __cil_tmp18;
3004#line 74
3005  __cil_tmp20 = *((unsigned short *)__cil_tmp19);
3006#line 74
3007  power_state = (int )__cil_tmp20;
3008#line 75
3009  ret = 0;
3010#line 78
3011  if ((int )psp == 3) {
3012#line 78
3013    goto case_3;
3014  } else
3015#line 81
3016  if ((int )psp == 40) {
3017#line 81
3018    goto case_40;
3019  } else
3020#line 84
3021  if ((int )psp == 31) {
3022#line 84
3023    goto case_31;
3024  } else {
3025    {
3026#line 91
3027    goto switch_default;
3028#line 77
3029    if (0) {
3030      case_3: /* CIL Label */ 
3031#line 79
3032      *((int *)val) = 1;
3033#line 80
3034      goto switch_break;
3035      case_40: /* CIL Label */ 
3036#line 82
3037      *((int *)val) = 2;
3038#line 83
3039      goto switch_break;
3040      case_31: /* CIL Label */ 
3041#line 86
3042      if (power_state == 0) {
3043#line 87
3044        *((int *)val) = 100;
3045      } else {
3046#line 89
3047        *((int *)val) = power_state;
3048      }
3049#line 90
3050      goto switch_break;
3051      switch_default: /* CIL Label */ 
3052#line 92
3053      ret = -22;
3054#line 93
3055      goto switch_break;
3056    } else {
3057      switch_break: /* CIL Label */ ;
3058    }
3059    }
3060  }
3061#line 95
3062  return (ret);
3063}
3064}
3065#line 98 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
3066static int wacom_ac_get_property(struct power_supply *psy , enum power_supply_property psp ,
3067                                 union power_supply_propval *val ) 
3068{ struct wacom_data *wdata ;
3069  struct power_supply  const  *__mptr ;
3070  int power_state ;
3071  int ret ;
3072  struct wacom_data *__cil_tmp8 ;
3073  unsigned long __cil_tmp9 ;
3074  unsigned long __cil_tmp10 ;
3075  struct power_supply *__cil_tmp11 ;
3076  unsigned int __cil_tmp12 ;
3077  char *__cil_tmp13 ;
3078  char *__cil_tmp14 ;
3079  unsigned long __cil_tmp15 ;
3080  unsigned long __cil_tmp16 ;
3081  int __cil_tmp17 ;
3082  unsigned long __cil_tmp18 ;
3083  unsigned long __cil_tmp19 ;
3084  unsigned short __cil_tmp20 ;
3085
3086  {
3087#line 102
3088  __mptr = (struct power_supply  const  *)psy;
3089#line 102
3090  __cil_tmp8 = (struct wacom_data *)0;
3091#line 102
3092  __cil_tmp9 = (unsigned long )__cil_tmp8;
3093#line 102
3094  __cil_tmp10 = __cil_tmp9 + 240;
3095#line 102
3096  __cil_tmp11 = (struct power_supply *)__cil_tmp10;
3097#line 102
3098  __cil_tmp12 = (unsigned int )__cil_tmp11;
3099#line 102
3100  __cil_tmp13 = (char *)__mptr;
3101#line 102
3102  __cil_tmp14 = __cil_tmp13 - __cil_tmp12;
3103#line 102
3104  wdata = (struct wacom_data *)__cil_tmp14;
3105#line 103
3106  __cil_tmp15 = (unsigned long )wdata;
3107#line 103
3108  __cil_tmp16 = __cil_tmp15 + 20;
3109#line 103
3110  __cil_tmp17 = *((int *)__cil_tmp16);
3111#line 103
3112  __cil_tmp18 = __cil_tmp17 * 2UL;
3113#line 103
3114  __cil_tmp19 = (unsigned long )(batcap) + __cil_tmp18;
3115#line 103
3116  __cil_tmp20 = *((unsigned short *)__cil_tmp19);
3117#line 103
3118  power_state = (int )__cil_tmp20;
3119#line 104
3120  ret = 0;
3121#line 107
3122  if ((int )psp == 3) {
3123#line 107
3124    goto case_3;
3125  } else
3126#line 109
3127  if ((int )psp == 4) {
3128#line 109
3129    goto case_3;
3130  } else
3131#line 115
3132  if ((int )psp == 40) {
3133#line 115
3134    goto case_40;
3135  } else {
3136    {
3137#line 118
3138    goto switch_default;
3139#line 106
3140    if (0) {
3141      case_3: /* CIL Label */ 
3142      case_4: /* CIL Label */ 
3143#line 110
3144      if (power_state == 0) {
3145#line 111
3146        *((int *)val) = 1;
3147      } else {
3148#line 113
3149        *((int *)val) = 0;
3150      }
3151#line 114
3152      goto switch_break;
3153      case_40: /* CIL Label */ 
3154#line 116
3155      *((int *)val) = 2;
3156#line 117
3157      goto switch_break;
3158      switch_default: /* CIL Label */ 
3159#line 119
3160      ret = -22;
3161#line 120
3162      goto switch_break;
3163    } else {
3164      switch_break: /* CIL Label */ ;
3165    }
3166    }
3167  }
3168#line 122
3169  return (ret);
3170}
3171}
3172#line 126 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
3173static void wacom_set_features(struct hid_device *hdev ) 
3174{ int ret ;
3175  __u8 rep_data[2] ;
3176  unsigned long __cil_tmp4 ;
3177  unsigned long __cil_tmp5 ;
3178  unsigned long __cil_tmp6 ;
3179  unsigned long __cil_tmp7 ;
3180  unsigned long __cil_tmp8 ;
3181  unsigned long __cil_tmp9 ;
3182  int (*__cil_tmp10)(struct hid_device * , __u8 * , size_t  , unsigned char  ) ;
3183  unsigned long __cil_tmp11 ;
3184  unsigned long __cil_tmp12 ;
3185  __u8 *__cil_tmp13 ;
3186  size_t __cil_tmp14 ;
3187
3188  {
3189  {
3190#line 132
3191  __cil_tmp4 = 0 * 1UL;
3192#line 132
3193  __cil_tmp5 = (unsigned long )(rep_data) + __cil_tmp4;
3194#line 132
3195  *((__u8 *)__cil_tmp5) = (__u8 )3;
3196#line 133
3197  __cil_tmp6 = 1 * 1UL;
3198#line 133
3199  __cil_tmp7 = (unsigned long )(rep_data) + __cil_tmp6;
3200#line 133
3201  *((__u8 *)__cil_tmp7) = (__u8 )32;
3202#line 134
3203  __cil_tmp8 = (unsigned long )hdev;
3204#line 134
3205  __cil_tmp9 = __cil_tmp8 + 7480;
3206#line 134
3207  __cil_tmp10 = *((int (**)(struct hid_device * , __u8 * , size_t  , unsigned char  ))__cil_tmp9);
3208#line 134
3209  __cil_tmp11 = 0 * 1UL;
3210#line 134
3211  __cil_tmp12 = (unsigned long )(rep_data) + __cil_tmp11;
3212#line 134
3213  __cil_tmp13 = (__u8 *)__cil_tmp12;
3214#line 134
3215  __cil_tmp14 = (size_t )2;
3216#line 134
3217  ret = (*__cil_tmp10)(hdev, __cil_tmp13, __cil_tmp14, (unsigned char)2);
3218  }
3219#line 136
3220  return;
3221}
3222}
3223#line 139 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
3224static void wacom_poke(struct hid_device *hdev , u8 speed ) 
3225{ struct wacom_data *wdata ;
3226  void *tmp ;
3227  int limit ;
3228  int ret ;
3229  char rep_data[2] ;
3230  int tmp___0 ;
3231  int tmp___1 ;
3232  unsigned long __cil_tmp10 ;
3233  unsigned long __cil_tmp11 ;
3234  unsigned long __cil_tmp12 ;
3235  unsigned long __cil_tmp13 ;
3236  unsigned long __cil_tmp14 ;
3237  unsigned long __cil_tmp15 ;
3238  int (*__cil_tmp16)(struct hid_device * , __u8 * , size_t  , unsigned char  ) ;
3239  unsigned long __cil_tmp17 ;
3240  unsigned long __cil_tmp18 ;
3241  char *__cil_tmp19 ;
3242  __u8 *__cil_tmp20 ;
3243  size_t __cil_tmp21 ;
3244  int __cil_tmp22 ;
3245  unsigned long __cil_tmp23 ;
3246  unsigned long __cil_tmp24 ;
3247  unsigned long __cil_tmp25 ;
3248  unsigned long __cil_tmp26 ;
3249  unsigned long __cil_tmp27 ;
3250  unsigned long __cil_tmp28 ;
3251  unsigned long __cil_tmp29 ;
3252  unsigned long __cil_tmp30 ;
3253  int (*__cil_tmp31)(struct hid_device * , __u8 * , size_t  , unsigned char  ) ;
3254  unsigned long __cil_tmp32 ;
3255  unsigned long __cil_tmp33 ;
3256  char *__cil_tmp34 ;
3257  __u8 *__cil_tmp35 ;
3258  size_t __cil_tmp36 ;
3259  unsigned long __cil_tmp37 ;
3260  unsigned long __cil_tmp38 ;
3261  unsigned long __cil_tmp39 ;
3262  unsigned long __cil_tmp40 ;
3263  struct device *__cil_tmp41 ;
3264  struct device  const  *__cil_tmp42 ;
3265  unsigned long __cil_tmp43 ;
3266  unsigned long __cil_tmp44 ;
3267  char __cil_tmp45 ;
3268  int __cil_tmp46 ;
3269
3270  {
3271  {
3272#line 141
3273  tmp = hid_get_drvdata(hdev);
3274#line 141
3275  wdata = (struct wacom_data *)tmp;
3276#line 145
3277  __cil_tmp10 = 0 * 1UL;
3278#line 145
3279  __cil_tmp11 = (unsigned long )(rep_data) + __cil_tmp10;
3280#line 145
3281  *((char *)__cil_tmp11) = (char)3;
3282#line 145
3283  __cil_tmp12 = 1 * 1UL;
3284#line 145
3285  __cil_tmp13 = (unsigned long )(rep_data) + __cil_tmp12;
3286#line 145
3287  *((char *)__cil_tmp13) = (char)0;
3288#line 146
3289  limit = 3;
3290  }
3291  {
3292#line 147
3293  while (1) {
3294    while_continue: /* CIL Label */ ;
3295    {
3296#line 148
3297    __cil_tmp14 = (unsigned long )hdev;
3298#line 148
3299    __cil_tmp15 = __cil_tmp14 + 7480;
3300#line 148
3301    __cil_tmp16 = *((int (**)(struct hid_device * , __u8 * , size_t  , unsigned char  ))__cil_tmp15);
3302#line 148
3303    __cil_tmp17 = 0 * 1UL;
3304#line 148
3305    __cil_tmp18 = (unsigned long )(rep_data) + __cil_tmp17;
3306#line 148
3307    __cil_tmp19 = (char *)__cil_tmp18;
3308#line 148
3309    __cil_tmp20 = (__u8 *)__cil_tmp19;
3310#line 148
3311    __cil_tmp21 = (size_t )2;
3312#line 148
3313    ret = (*__cil_tmp16)(hdev, __cil_tmp20, __cil_tmp21, (unsigned char)2);
3314    }
3315#line 147
3316    if (ret < 0) {
3317#line 147
3318      tmp___0 = limit;
3319#line 147
3320      limit = limit - 1;
3321#line 147
3322      if (tmp___0 > 0) {
3323
3324      } else {
3325#line 147
3326        goto while_break;
3327      }
3328    } else {
3329#line 147
3330      goto while_break;
3331    }
3332  }
3333  while_break: /* CIL Label */ ;
3334  }
3335#line 152
3336  if (ret >= 0) {
3337    {
3338#line 153
3339    __cil_tmp22 = (int )speed;
3340#line 153
3341    if (__cil_tmp22 == 0) {
3342#line 154
3343      __cil_tmp23 = 0 * 1UL;
3344#line 154
3345      __cil_tmp24 = (unsigned long )(rep_data) + __cil_tmp23;
3346#line 154
3347      *((char *)__cil_tmp24) = (char)5;
3348    } else {
3349#line 156
3350      __cil_tmp25 = 0 * 1UL;
3351#line 156
3352      __cil_tmp26 = (unsigned long )(rep_data) + __cil_tmp25;
3353#line 156
3354      *((char *)__cil_tmp26) = (char)6;
3355    }
3356    }
3357#line 158
3358    __cil_tmp27 = 1 * 1UL;
3359#line 158
3360    __cil_tmp28 = (unsigned long )(rep_data) + __cil_tmp27;
3361#line 158
3362    *((char *)__cil_tmp28) = (char)0;
3363#line 159
3364    limit = 3;
3365    {
3366#line 160
3367    while (1) {
3368      while_continue___0: /* CIL Label */ ;
3369      {
3370#line 161
3371      __cil_tmp29 = (unsigned long )hdev;
3372#line 161
3373      __cil_tmp30 = __cil_tmp29 + 7480;
3374#line 161
3375      __cil_tmp31 = *((int (**)(struct hid_device * , __u8 * , size_t  , unsigned char  ))__cil_tmp30);
3376#line 161
3377      __cil_tmp32 = 0 * 1UL;
3378#line 161
3379      __cil_tmp33 = (unsigned long )(rep_data) + __cil_tmp32;
3380#line 161
3381      __cil_tmp34 = (char *)__cil_tmp33;
3382#line 161
3383      __cil_tmp35 = (__u8 *)__cil_tmp34;
3384#line 161
3385      __cil_tmp36 = (size_t )2;
3386#line 161
3387      ret = (*__cil_tmp31)(hdev, __cil_tmp35, __cil_tmp36, (unsigned char)2);
3388      }
3389#line 160
3390      if (ret < 0) {
3391#line 160
3392        tmp___1 = limit;
3393#line 160
3394        limit = limit - 1;
3395#line 160
3396        if (tmp___1 > 0) {
3397
3398        } else {
3399#line 160
3400          goto while_break___0;
3401        }
3402      } else {
3403#line 160
3404        goto while_break___0;
3405      }
3406    }
3407    while_break___0: /* CIL Label */ ;
3408    }
3409#line 165
3410    if (ret >= 0) {
3411#line 166
3412      __cil_tmp37 = (unsigned long )wdata;
3413#line 166
3414      __cil_tmp38 = __cil_tmp37 + 16;
3415#line 166
3416      *((unsigned char *)__cil_tmp38) = speed;
3417#line 167
3418      return;
3419    } else {
3420
3421    }
3422  } else {
3423
3424  }
3425  {
3426#line 175
3427  __cil_tmp39 = (unsigned long )hdev;
3428#line 175
3429  __cil_tmp40 = __cil_tmp39 + 6328;
3430#line 175
3431  __cil_tmp41 = (struct device *)__cil_tmp40;
3432#line 175
3433  __cil_tmp42 = (struct device  const  *)__cil_tmp41;
3434#line 175
3435  __cil_tmp43 = 0 * 1UL;
3436#line 175
3437  __cil_tmp44 = (unsigned long )(rep_data) + __cil_tmp43;
3438#line 175
3439  __cil_tmp45 = *((char *)__cil_tmp44);
3440#line 175
3441  __cil_tmp46 = (int )__cil_tmp45;
3442#line 175
3443  dev_warn(__cil_tmp42, "failed to poke device, command %d, err %d\n", __cil_tmp46,
3444           ret);
3445  }
3446#line 177
3447  return;
3448}
3449}
3450#line 180 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
3451static ssize_t wacom_show_speed(struct device *dev , struct device_attribute *attr ,
3452                                char *buf ) 
3453{ struct wacom_data *wdata ;
3454  void *tmp ;
3455  int tmp___0 ;
3456  struct device  const  *__cil_tmp7 ;
3457  unsigned long __cil_tmp8 ;
3458  unsigned long __cil_tmp9 ;
3459  unsigned long __cil_tmp10 ;
3460  unsigned char __cil_tmp11 ;
3461  int __cil_tmp12 ;
3462
3463  {
3464  {
3465#line 184
3466  __cil_tmp7 = (struct device  const  *)dev;
3467#line 184
3468  tmp = dev_get_drvdata(__cil_tmp7);
3469#line 184
3470  wdata = (struct wacom_data *)tmp;
3471#line 186
3472  __cil_tmp8 = 1UL << 12;
3473#line 186
3474  __cil_tmp9 = (unsigned long )wdata;
3475#line 186
3476  __cil_tmp10 = __cil_tmp9 + 16;
3477#line 186
3478  __cil_tmp11 = *((unsigned char *)__cil_tmp10);
3479#line 186
3480  __cil_tmp12 = (int )__cil_tmp11;
3481#line 186
3482  tmp___0 = snprintf(buf, __cil_tmp8, "%i\n", __cil_tmp12);
3483  }
3484#line 186
3485  return ((ssize_t )tmp___0);
3486}
3487}
3488#line 189 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
3489static ssize_t wacom_store_speed(struct device *dev , struct device_attribute *attr ,
3490                                 char const   *buf , size_t count ) 
3491{ struct hid_device *hdev ;
3492  struct device  const  *__mptr ;
3493  int new_speed ;
3494  int tmp ;
3495  __kernel_size_t tmp___0 ;
3496  struct hid_device *__cil_tmp10 ;
3497  unsigned long __cil_tmp11 ;
3498  unsigned long __cil_tmp12 ;
3499  struct device *__cil_tmp13 ;
3500  unsigned int __cil_tmp14 ;
3501  char *__cil_tmp15 ;
3502  char *__cil_tmp16 ;
3503  int *__cil_tmp17 ;
3504  int __cil_tmp18 ;
3505  int *__cil_tmp19 ;
3506  int __cil_tmp20 ;
3507  u8 __cil_tmp21 ;
3508  unsigned long __cil_tmp22 ;
3509  int *__cil_tmp23 ;
3510  int __cil_tmp24 ;
3511  int *__cil_tmp25 ;
3512  int __cil_tmp26 ;
3513  u8 __cil_tmp27 ;
3514  unsigned long __cil_tmp28 ;
3515
3516  {
3517  {
3518#line 193
3519  __mptr = (struct device  const  *)dev;
3520#line 193
3521  __cil_tmp10 = (struct hid_device *)0;
3522#line 193
3523  __cil_tmp11 = (unsigned long )__cil_tmp10;
3524#line 193
3525  __cil_tmp12 = __cil_tmp11 + 6328;
3526#line 193
3527  __cil_tmp13 = (struct device *)__cil_tmp12;
3528#line 193
3529  __cil_tmp14 = (unsigned int )__cil_tmp13;
3530#line 193
3531  __cil_tmp15 = (char *)__mptr;
3532#line 193
3533  __cil_tmp16 = __cil_tmp15 - __cil_tmp14;
3534#line 193
3535  hdev = (struct hid_device *)__cil_tmp16;
3536#line 196
3537  tmp = sscanf(buf, "%1d", & new_speed);
3538  }
3539#line 196
3540  if (tmp != 1) {
3541#line 197
3542    return ((ssize_t )-22);
3543  } else {
3544
3545  }
3546  {
3547#line 199
3548  __cil_tmp17 = & new_speed;
3549#line 199
3550  __cil_tmp18 = *__cil_tmp17;
3551#line 199
3552  if (__cil_tmp18 == 0) {
3553    {
3554#line 200
3555    __cil_tmp19 = & new_speed;
3556#line 200
3557    __cil_tmp20 = *__cil_tmp19;
3558#line 200
3559    __cil_tmp21 = (u8 )__cil_tmp20;
3560#line 200
3561    wacom_poke(hdev, __cil_tmp21);
3562#line 201
3563    __cil_tmp22 = 1UL << 12;
3564#line 201
3565    tmp___0 = strnlen(buf, __cil_tmp22);
3566    }
3567#line 201
3568    return ((ssize_t )tmp___0);
3569  } else {
3570    {
3571#line 199
3572    __cil_tmp23 = & new_speed;
3573#line 199
3574    __cil_tmp24 = *__cil_tmp23;
3575#line 199
3576    if (__cil_tmp24 == 1) {
3577      {
3578#line 200
3579      __cil_tmp25 = & new_speed;
3580#line 200
3581      __cil_tmp26 = *__cil_tmp25;
3582#line 200
3583      __cil_tmp27 = (u8 )__cil_tmp26;
3584#line 200
3585      wacom_poke(hdev, __cil_tmp27);
3586#line 201
3587      __cil_tmp28 = 1UL << 12;
3588#line 201
3589      tmp___0 = strnlen(buf, __cil_tmp28);
3590      }
3591#line 201
3592      return ((ssize_t )tmp___0);
3593    } else {
3594#line 203
3595      return ((ssize_t )-22);
3596    }
3597    }
3598  }
3599  }
3600}
3601}
3602#line 206 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
3603static struct device_attribute dev_attr_speed  =    {{"speed", (umode_t )436}, & wacom_show_speed, & wacom_store_speed};
3604#line 209 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
3605static int wacom_gr_parse_report(struct hid_device *hdev , struct wacom_data *wdata ,
3606                                 struct input_dev *input , unsigned char *data ) 
3607{ int tool ;
3608  int x ;
3609  int y ;
3610  int rw ;
3611  int tmp ;
3612  int tmp___0 ;
3613  int tmp___1 ;
3614  unsigned char *__cil_tmp12 ;
3615  __le16 *__cil_tmp13 ;
3616  __le16 __cil_tmp14 ;
3617  unsigned char *__cil_tmp15 ;
3618  __le16 *__cil_tmp16 ;
3619  __le16 __cil_tmp17 ;
3620  unsigned char *__cil_tmp18 ;
3621  unsigned char __cil_tmp19 ;
3622  int __cil_tmp20 ;
3623  unsigned char *__cil_tmp21 ;
3624  unsigned char __cil_tmp22 ;
3625  int __cil_tmp23 ;
3626  int __cil_tmp24 ;
3627  unsigned char *__cil_tmp25 ;
3628  unsigned char __cil_tmp26 ;
3629  int __cil_tmp27 ;
3630  int __cil_tmp28 ;
3631  __u16 __cil_tmp29 ;
3632  int __cil_tmp30 ;
3633  __u16 __cil_tmp31 ;
3634  int __cil_tmp32 ;
3635  __u16 __cil_tmp33 ;
3636  unsigned int __cil_tmp34 ;
3637  unsigned int __cil_tmp35 ;
3638  unsigned char *__cil_tmp36 ;
3639  unsigned char __cil_tmp37 ;
3640  int __cil_tmp38 ;
3641  int __cil_tmp39 ;
3642  unsigned char *__cil_tmp40 ;
3643  unsigned char __cil_tmp41 ;
3644  int __cil_tmp42 ;
3645  int __cil_tmp43 ;
3646  unsigned char *__cil_tmp44 ;
3647  unsigned char __cil_tmp45 ;
3648  int __cil_tmp46 ;
3649  unsigned char *__cil_tmp47 ;
3650  unsigned char __cil_tmp48 ;
3651  int __cil_tmp49 ;
3652  unsigned char *__cil_tmp50 ;
3653  unsigned char __cil_tmp51 ;
3654  int __cil_tmp52 ;
3655  int __cil_tmp53 ;
3656  unsigned char *__cil_tmp54 ;
3657  unsigned char __cil_tmp55 ;
3658  int __cil_tmp56 ;
3659  int __cil_tmp57 ;
3660  unsigned char *__cil_tmp58 ;
3661  unsigned char __cil_tmp59 ;
3662  int __cil_tmp60 ;
3663  int __cil_tmp61 ;
3664  unsigned char *__cil_tmp62 ;
3665  unsigned char __cil_tmp63 ;
3666  int __cil_tmp64 ;
3667  int __cil_tmp65 ;
3668  __u16 __cil_tmp66 ;
3669  int __cil_tmp67 ;
3670  int __cil_tmp68 ;
3671  unsigned char *__cil_tmp69 ;
3672  unsigned char __cil_tmp70 ;
3673  int __cil_tmp71 ;
3674  int __cil_tmp72 ;
3675  unsigned char *__cil_tmp73 ;
3676  unsigned char __cil_tmp74 ;
3677  int __cil_tmp75 ;
3678  int __cil_tmp76 ;
3679  unsigned char *__cil_tmp77 ;
3680  unsigned char __cil_tmp78 ;
3681  int __cil_tmp79 ;
3682  int __cil_tmp80 ;
3683  unsigned char *__cil_tmp81 ;
3684  unsigned char __cil_tmp82 ;
3685  int __cil_tmp83 ;
3686  unsigned char *__cil_tmp84 ;
3687  unsigned char __cil_tmp85 ;
3688  int __cil_tmp86 ;
3689  unsigned long __cil_tmp87 ;
3690  unsigned long __cil_tmp88 ;
3691  __u16 __cil_tmp89 ;
3692  int __cil_tmp90 ;
3693  unsigned long __cil_tmp91 ;
3694  unsigned long __cil_tmp92 ;
3695  int __cil_tmp93 ;
3696  int __cil_tmp94 ;
3697  unsigned char *__cil_tmp95 ;
3698  unsigned char __cil_tmp96 ;
3699  int __cil_tmp97 ;
3700  int __cil_tmp98 ;
3701  unsigned long __cil_tmp99 ;
3702  unsigned long __cil_tmp100 ;
3703  int __cil_tmp101 ;
3704  unsigned long __cil_tmp102 ;
3705  unsigned long __cil_tmp103 ;
3706
3707  {
3708#line 215
3709  tool = 0;
3710#line 217
3711  __cil_tmp12 = data + 2;
3712#line 217
3713  __cil_tmp13 = (__le16 *)__cil_tmp12;
3714#line 217
3715  __cil_tmp14 = *__cil_tmp13;
3716#line 217
3717  x = (int )__cil_tmp14;
3718#line 218
3719  __cil_tmp15 = data + 4;
3720#line 218
3721  __cil_tmp16 = (__le16 *)__cil_tmp15;
3722#line 218
3723  __cil_tmp17 = *__cil_tmp16;
3724#line 218
3725  y = (int )__cil_tmp17;
3726  {
3727#line 221
3728  __cil_tmp18 = data + 1;
3729#line 221
3730  __cil_tmp19 = *__cil_tmp18;
3731#line 221
3732  __cil_tmp20 = (int )__cil_tmp19;
3733#line 221
3734  if (__cil_tmp20 & 144) {
3735    {
3736#line 222
3737    __cil_tmp21 = data + 1;
3738#line 222
3739    __cil_tmp22 = *__cil_tmp21;
3740#line 222
3741    __cil_tmp23 = (int )__cil_tmp22;
3742#line 222
3743    __cil_tmp24 = __cil_tmp23 >> 5;
3744#line 223
3745    if ((__cil_tmp24 & 3) == 0) {
3746#line 223
3747      goto case_0;
3748    } else
3749#line 227
3750    if ((__cil_tmp24 & 3) == 1) {
3751#line 227
3752      goto case_1;
3753    } else
3754#line 231
3755    if ((__cil_tmp24 & 3) == 2) {
3756#line 231
3757      goto case_2;
3758    } else
3759#line 232
3760    if ((__cil_tmp24 & 3) == 3) {
3761#line 232
3762      goto case_2;
3763    } else
3764#line 222
3765    if (0) {
3766      case_0: /* CIL Label */ 
3767#line 224
3768      tool = 320;
3769#line 225
3770      goto switch_break;
3771      case_1: /* CIL Label */ 
3772#line 228
3773      tool = 321;
3774#line 229
3775      goto switch_break;
3776      case_2: /* CIL Label */ 
3777      case_3: /* CIL Label */ 
3778#line 233
3779      tool = 326;
3780#line 234
3781      goto switch_break;
3782    } else {
3783      switch_break: /* CIL Label */ ;
3784    }
3785    }
3786    {
3787#line 238
3788    __cil_tmp25 = data + 1;
3789#line 238
3790    __cil_tmp26 = *__cil_tmp25;
3791#line 238
3792    __cil_tmp27 = (int )__cil_tmp26;
3793#line 238
3794    __cil_tmp28 = __cil_tmp27 & 16;
3795#line 238
3796    if (! __cil_tmp28) {
3797#line 239
3798      tool = 0;
3799    } else {
3800
3801    }
3802    }
3803  } else {
3804
3805  }
3806  }
3807  {
3808#line 243
3809  __cil_tmp29 = *((__u16 *)wdata);
3810#line 243
3811  __cil_tmp30 = (int )__cil_tmp29;
3812#line 243
3813  if (__cil_tmp30 != tool) {
3814#line 244
3815    if (*((__u16 *)wdata)) {
3816      {
3817#line 246
3818      __cil_tmp31 = *((__u16 *)wdata);
3819#line 246
3820      __cil_tmp32 = (int )__cil_tmp31;
3821#line 246
3822      if (__cil_tmp32 == 326) {
3823        {
3824#line 247
3825        input_report_key(input, 272U, 0);
3826#line 248
3827        input_report_key(input, 273U, 0);
3828#line 249
3829        input_report_key(input, 274U, 0);
3830#line 250
3831        tmp = input_abs_get_max(input, 25U);
3832#line 250
3833        input_report_abs(input, 25U, tmp);
3834        }
3835      } else {
3836        {
3837#line 253
3838        input_report_key(input, 330U, 0);
3839#line 254
3840        input_report_key(input, 331U, 0);
3841#line 255
3842        input_report_key(input, 332U, 0);
3843#line 256
3844        input_report_abs(input, 24U, 0);
3845        }
3846      }
3847      }
3848      {
3849#line 258
3850      __cil_tmp33 = *((__u16 *)wdata);
3851#line 258
3852      __cil_tmp34 = (unsigned int )__cil_tmp33;
3853#line 258
3854      input_report_key(input, __cil_tmp34, 0);
3855#line 259
3856      input_sync(input);
3857      }
3858    } else {
3859
3860    }
3861#line 261
3862    *((__u16 *)wdata) = (__u16 )tool;
3863#line 262
3864    if (tool) {
3865      {
3866#line 263
3867      __cil_tmp35 = (unsigned int )tool;
3868#line 263
3869      input_report_key(input, __cil_tmp35, 1);
3870      }
3871    } else {
3872
3873    }
3874  } else {
3875
3876  }
3877  }
3878#line 266
3879  if (tool) {
3880    {
3881#line 267
3882    input_report_abs(input, 0U, x);
3883#line 268
3884    input_report_abs(input, 1U, y);
3885    }
3886    {
3887#line 270
3888    __cil_tmp36 = data + 1;
3889#line 270
3890    __cil_tmp37 = *__cil_tmp36;
3891#line 270
3892    __cil_tmp38 = (int )__cil_tmp37;
3893#line 270
3894    __cil_tmp39 = __cil_tmp38 >> 5;
3895#line 271
3896    if ((__cil_tmp39 & 3) == 2) {
3897#line 271
3898      goto case_2___0;
3899    } else
3900#line 278
3901    if ((__cil_tmp39 & 3) == 3) {
3902#line 278
3903      goto case_3___0;
3904    } else {
3905      {
3906#line 290
3907      goto switch_default;
3908#line 270
3909      if (0) {
3910        case_2___0: /* CIL Label */ 
3911        {
3912#line 272
3913        __cil_tmp40 = data + 1;
3914#line 272
3915        __cil_tmp41 = *__cil_tmp40;
3916#line 272
3917        __cil_tmp42 = (int )__cil_tmp41;
3918#line 272
3919        __cil_tmp43 = __cil_tmp42 & 4;
3920#line 272
3921        input_report_key(input, 274U, __cil_tmp43);
3922        }
3923        {
3924#line 273
3925        __cil_tmp44 = data + 6;
3926#line 273
3927        __cil_tmp45 = *__cil_tmp44;
3928#line 273
3929        __cil_tmp46 = (int )__cil_tmp45;
3930#line 273
3931        if (__cil_tmp46 & 1) {
3932#line 273
3933          rw = -1;
3934        } else {
3935          {
3936#line 273
3937          __cil_tmp47 = data + 6;
3938#line 273
3939          __cil_tmp48 = *__cil_tmp47;
3940#line 273
3941          __cil_tmp49 = (int )__cil_tmp48;
3942#line 273
3943          if (__cil_tmp49 & 2) {
3944#line 273
3945            tmp___0 = 1;
3946          } else {
3947#line 273
3948            tmp___0 = 0;
3949          }
3950          }
3951#line 273
3952          rw = tmp___0;
3953        }
3954        }
3955        {
3956#line 275
3957        input_report_rel(input, 8U, rw);
3958        }
3959        case_3___0: /* CIL Label */ 
3960        {
3961#line 279
3962        __cil_tmp50 = data + 1;
3963#line 279
3964        __cil_tmp51 = *__cil_tmp50;
3965#line 279
3966        __cil_tmp52 = (int )__cil_tmp51;
3967#line 279
3968        __cil_tmp53 = __cil_tmp52 & 1;
3969#line 279
3970        input_report_key(input, 272U, __cil_tmp53);
3971#line 280
3972        __cil_tmp54 = data + 1;
3973#line 280
3974        __cil_tmp55 = *__cil_tmp54;
3975#line 280
3976        __cil_tmp56 = (int )__cil_tmp55;
3977#line 280
3978        __cil_tmp57 = __cil_tmp56 & 2;
3979#line 280
3980        input_report_key(input, 273U, __cil_tmp57);
3981#line 282
3982        __cil_tmp58 = data + 6;
3983#line 282
3984        __cil_tmp59 = *__cil_tmp58;
3985#line 282
3986        __cil_tmp60 = (int )__cil_tmp59;
3987#line 282
3988        __cil_tmp61 = __cil_tmp60 >> 2;
3989#line 282
3990        rw = 44 - __cil_tmp61;
3991        }
3992#line 283
3993        if (rw < 0) {
3994#line 284
3995          rw = 0;
3996        } else
3997#line 285
3998        if (rw > 31) {
3999#line 286
4000          rw = 31;
4001        } else {
4002
4003        }
4004        {
4005#line 287
4006        input_report_abs(input, 25U, rw);
4007        }
4008#line 288
4009        goto switch_break___0;
4010        switch_default: /* CIL Label */ 
4011        {
4012#line 291
4013        __cil_tmp62 = data + 1;
4014#line 291
4015        __cil_tmp63 = *__cil_tmp62;
4016#line 291
4017        __cil_tmp64 = (int )__cil_tmp63;
4018#line 291
4019        __cil_tmp65 = __cil_tmp64 & 8;
4020#line 291
4021        __cil_tmp66 = (__u16 )__cil_tmp65;
4022#line 291
4023        __cil_tmp67 = (int )__cil_tmp66;
4024#line 291
4025        __cil_tmp68 = __cil_tmp67 << 5;
4026#line 291
4027        __cil_tmp69 = data + 6;
4028#line 291
4029        __cil_tmp70 = *__cil_tmp69;
4030#line 291
4031        __cil_tmp71 = (int )__cil_tmp70;
4032#line 291
4033        __cil_tmp72 = __cil_tmp71 | __cil_tmp68;
4034#line 291
4035        input_report_abs(input, 24U, __cil_tmp72);
4036#line 293
4037        __cil_tmp73 = data + 1;
4038#line 293
4039        __cil_tmp74 = *__cil_tmp73;
4040#line 293
4041        __cil_tmp75 = (int )__cil_tmp74;
4042#line 293
4043        __cil_tmp76 = __cil_tmp75 & 1;
4044#line 293
4045        input_report_key(input, 330U, __cil_tmp76);
4046#line 294
4047        __cil_tmp77 = data + 1;
4048#line 294
4049        __cil_tmp78 = *__cil_tmp77;
4050#line 294
4051        __cil_tmp79 = (int )__cil_tmp78;
4052#line 294
4053        __cil_tmp80 = __cil_tmp79 & 2;
4054#line 294
4055        input_report_key(input, 331U, __cil_tmp80);
4056        }
4057#line 295
4058        if (tool == 320) {
4059          {
4060#line 295
4061          __cil_tmp81 = data + 1;
4062#line 295
4063          __cil_tmp82 = *__cil_tmp81;
4064#line 295
4065          __cil_tmp83 = (int )__cil_tmp82;
4066#line 295
4067          if (__cil_tmp83 & 4) {
4068#line 295
4069            tmp___1 = 1;
4070          } else {
4071#line 295
4072            tmp___1 = 0;
4073          }
4074          }
4075        } else {
4076#line 295
4077          tmp___1 = 0;
4078        }
4079        {
4080#line 295
4081        input_report_key(input, 332U, tmp___1);
4082        }
4083#line 296
4084        goto switch_break___0;
4085      } else {
4086        switch_break___0: /* CIL Label */ ;
4087      }
4088      }
4089    }
4090    }
4091    {
4092#line 299
4093    input_sync(input);
4094    }
4095  } else {
4096
4097  }
4098#line 304
4099  __cil_tmp84 = data + 7;
4100#line 304
4101  __cil_tmp85 = *__cil_tmp84;
4102#line 304
4103  __cil_tmp86 = (int )__cil_tmp85;
4104#line 304
4105  rw = __cil_tmp86 & 3;
4106  {
4107#line 305
4108  __cil_tmp87 = (unsigned long )wdata;
4109#line 305
4110  __cil_tmp88 = __cil_tmp87 + 2;
4111#line 305
4112  __cil_tmp89 = *((__u16 *)__cil_tmp88);
4113#line 305
4114  __cil_tmp90 = (int )__cil_tmp89;
4115#line 305
4116  if (rw != __cil_tmp90) {
4117    {
4118#line 306
4119    __cil_tmp91 = (unsigned long )wdata;
4120#line 306
4121    __cil_tmp92 = __cil_tmp91 + 2;
4122#line 306
4123    *((__u16 *)__cil_tmp92) = (__u16 )rw;
4124#line 307
4125    __cil_tmp93 = rw & 2;
4126#line 307
4127    input_report_key(input, 256U, __cil_tmp93);
4128#line 308
4129    __cil_tmp94 = rw & 1;
4130#line 308
4131    input_report_key(input, 257U, __cil_tmp94);
4132#line 309
4133    input_report_key(input, 325U, 240);
4134#line 310
4135    input_event(input, 4U, 0U, 240);
4136#line 311
4137    input_sync(input);
4138    }
4139  } else {
4140
4141  }
4142  }
4143#line 316
4144  __cil_tmp95 = data + 7;
4145#line 316
4146  __cil_tmp96 = *__cil_tmp95;
4147#line 316
4148  __cil_tmp97 = (int )__cil_tmp96;
4149#line 316
4150  __cil_tmp98 = __cil_tmp97 >> 2;
4151#line 316
4152  rw = __cil_tmp98 & 7;
4153  {
4154#line 317
4155  __cil_tmp99 = (unsigned long )wdata;
4156#line 317
4157  __cil_tmp100 = __cil_tmp99 + 20;
4158#line 317
4159  __cil_tmp101 = *((int *)__cil_tmp100);
4160#line 317
4161  if (rw != __cil_tmp101) {
4162#line 318
4163    __cil_tmp102 = (unsigned long )wdata;
4164#line 318
4165    __cil_tmp103 = __cil_tmp102 + 20;
4166#line 318
4167    *((int *)__cil_tmp103) = rw;
4168  } else {
4169
4170  }
4171  }
4172#line 320
4173  return (1);
4174}
4175}
4176#line 323 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
4177static void wacom_i4_parse_button_report(struct wacom_data *wdata , struct input_dev *input ,
4178                                         unsigned char *data ) 
4179{ __u16 new_butstate ;
4180  __u8 new_whlstate ;
4181  __u8 sync ;
4182  unsigned char *__cil_tmp7 ;
4183  unsigned long __cil_tmp8 ;
4184  unsigned long __cil_tmp9 ;
4185  __u8 __cil_tmp10 ;
4186  int __cil_tmp11 ;
4187  int __cil_tmp12 ;
4188  unsigned long __cil_tmp13 ;
4189  unsigned long __cil_tmp14 ;
4190  int __cil_tmp15 ;
4191  int __cil_tmp16 ;
4192  int __cil_tmp17 ;
4193  unsigned char *__cil_tmp18 ;
4194  unsigned char __cil_tmp19 ;
4195  int __cil_tmp20 ;
4196  int __cil_tmp21 ;
4197  unsigned char *__cil_tmp22 ;
4198  unsigned char __cil_tmp23 ;
4199  int __cil_tmp24 ;
4200  int __cil_tmp25 ;
4201  int __cil_tmp26 ;
4202  unsigned long __cil_tmp27 ;
4203  unsigned long __cil_tmp28 ;
4204  __u16 __cil_tmp29 ;
4205  int __cil_tmp30 ;
4206  int __cil_tmp31 ;
4207  unsigned long __cil_tmp32 ;
4208  unsigned long __cil_tmp33 ;
4209  int __cil_tmp34 ;
4210  int __cil_tmp35 ;
4211  int __cil_tmp36 ;
4212  int __cil_tmp37 ;
4213  int __cil_tmp38 ;
4214  int __cil_tmp39 ;
4215  int __cil_tmp40 ;
4216  int __cil_tmp41 ;
4217  int __cil_tmp42 ;
4218  int __cil_tmp43 ;
4219  int __cil_tmp44 ;
4220  int __cil_tmp45 ;
4221  int __cil_tmp46 ;
4222  int __cil_tmp47 ;
4223  int __cil_tmp48 ;
4224  int __cil_tmp49 ;
4225  int __cil_tmp50 ;
4226  int __cil_tmp51 ;
4227
4228  {
4229#line 328
4230  sync = (__u8 )0;
4231#line 330
4232  __cil_tmp7 = data + 1;
4233#line 330
4234  new_whlstate = *__cil_tmp7;
4235  {
4236#line 331
4237  __cil_tmp8 = (unsigned long )wdata;
4238#line 331
4239  __cil_tmp9 = __cil_tmp8 + 4;
4240#line 331
4241  __cil_tmp10 = *((__u8 *)__cil_tmp9);
4242#line 331
4243  __cil_tmp11 = (int )__cil_tmp10;
4244#line 331
4245  __cil_tmp12 = (int )new_whlstate;
4246#line 331
4247  if (__cil_tmp12 != __cil_tmp11) {
4248#line 332
4249    __cil_tmp13 = (unsigned long )wdata;
4250#line 332
4251    __cil_tmp14 = __cil_tmp13 + 4;
4252#line 332
4253    *((__u8 *)__cil_tmp14) = new_whlstate;
4254    {
4255#line 333
4256    __cil_tmp15 = (int )new_whlstate;
4257#line 333
4258    if (__cil_tmp15 & 128) {
4259      {
4260#line 334
4261      input_report_key(input, 330U, 1);
4262#line 335
4263      __cil_tmp16 = (int )new_whlstate;
4264#line 335
4265      __cil_tmp17 = __cil_tmp16 & 127;
4266#line 335
4267      input_report_abs(input, 8U, __cil_tmp17);
4268#line 336
4269      input_report_key(input, 325U, 1);
4270      }
4271    } else {
4272      {
4273#line 338
4274      input_report_key(input, 330U, 0);
4275#line 339
4276      input_report_abs(input, 8U, 0);
4277#line 340
4278      input_report_key(input, 325U, 0);
4279      }
4280    }
4281    }
4282#line 342
4283    sync = (__u8 )1;
4284  } else {
4285
4286  }
4287  }
4288#line 345
4289  __cil_tmp18 = data + 2;
4290#line 345
4291  __cil_tmp19 = *__cil_tmp18;
4292#line 345
4293  __cil_tmp20 = (int )__cil_tmp19;
4294#line 345
4295  __cil_tmp21 = __cil_tmp20 & 1;
4296#line 345
4297  __cil_tmp22 = data + 3;
4298#line 345
4299  __cil_tmp23 = *__cil_tmp22;
4300#line 345
4301  __cil_tmp24 = (int )__cil_tmp23;
4302#line 345
4303  __cil_tmp25 = __cil_tmp24 << 1;
4304#line 345
4305  __cil_tmp26 = __cil_tmp25 | __cil_tmp21;
4306#line 345
4307  new_butstate = (__u16 )__cil_tmp26;
4308  {
4309#line 346
4310  __cil_tmp27 = (unsigned long )wdata;
4311#line 346
4312  __cil_tmp28 = __cil_tmp27 + 2;
4313#line 346
4314  __cil_tmp29 = *((__u16 *)__cil_tmp28);
4315#line 346
4316  __cil_tmp30 = (int )__cil_tmp29;
4317#line 346
4318  __cil_tmp31 = (int )new_butstate;
4319#line 346
4320  if (__cil_tmp31 != __cil_tmp30) {
4321    {
4322#line 347
4323    __cil_tmp32 = (unsigned long )wdata;
4324#line 347
4325    __cil_tmp33 = __cil_tmp32 + 2;
4326#line 347
4327    *((__u16 *)__cil_tmp33) = new_butstate;
4328#line 348
4329    __cil_tmp34 = (int )new_butstate;
4330#line 348
4331    __cil_tmp35 = __cil_tmp34 & 1;
4332#line 348
4333    input_report_key(input, 256U, __cil_tmp35);
4334#line 349
4335    __cil_tmp36 = (int )new_butstate;
4336#line 349
4337    __cil_tmp37 = __cil_tmp36 & 2;
4338#line 349
4339    input_report_key(input, 257U, __cil_tmp37);
4340#line 350
4341    __cil_tmp38 = (int )new_butstate;
4342#line 350
4343    __cil_tmp39 = __cil_tmp38 & 4;
4344#line 350
4345    input_report_key(input, 258U, __cil_tmp39);
4346#line 351
4347    __cil_tmp40 = (int )new_butstate;
4348#line 351
4349    __cil_tmp41 = __cil_tmp40 & 8;
4350#line 351
4351    input_report_key(input, 259U, __cil_tmp41);
4352#line 352
4353    __cil_tmp42 = (int )new_butstate;
4354#line 352
4355    __cil_tmp43 = __cil_tmp42 & 16;
4356#line 352
4357    input_report_key(input, 260U, __cil_tmp43);
4358#line 353
4359    __cil_tmp44 = (int )new_butstate;
4360#line 353
4361    __cil_tmp45 = __cil_tmp44 & 32;
4362#line 353
4363    input_report_key(input, 261U, __cil_tmp45);
4364#line 354
4365    __cil_tmp46 = (int )new_butstate;
4366#line 354
4367    __cil_tmp47 = __cil_tmp46 & 64;
4368#line 354
4369    input_report_key(input, 262U, __cil_tmp47);
4370#line 355
4371    __cil_tmp48 = (int )new_butstate;
4372#line 355
4373    __cil_tmp49 = __cil_tmp48 & 128;
4374#line 355
4375    input_report_key(input, 263U, __cil_tmp49);
4376#line 356
4377    __cil_tmp50 = (int )new_butstate;
4378#line 356
4379    __cil_tmp51 = __cil_tmp50 & 256;
4380#line 356
4381    input_report_key(input, 264U, __cil_tmp51);
4382#line 357
4383    input_report_key(input, 325U, 1);
4384#line 358
4385    sync = (__u8 )1;
4386    }
4387  } else {
4388
4389  }
4390  }
4391#line 361
4392  if (sync) {
4393    {
4394#line 362
4395    input_report_abs(input, 40U, 15);
4396#line 363
4397    input_event(input, 4U, 0U, -1);
4398#line 364
4399    input_sync(input);
4400    }
4401  } else {
4402
4403  }
4404#line 366
4405  return;
4406}
4407}
4408#line 368 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
4409static void wacom_i4_parse_pen_report(struct wacom_data *wdata , struct input_dev *input ,
4410                                      unsigned char *data ) 
4411{ __u16 x ;
4412  __u16 y ;
4413  __u16 pressure ;
4414  __u8 distance ;
4415  unsigned char *__cil_tmp8 ;
4416  unsigned char __cil_tmp9 ;
4417  __u16 __cil_tmp10 ;
4418  unsigned int __cil_tmp11 ;
4419  unsigned long __cil_tmp12 ;
4420  unsigned long __cil_tmp13 ;
4421  __u32 __cil_tmp14 ;
4422  int __cil_tmp15 ;
4423  unsigned long __cil_tmp16 ;
4424  unsigned long __cil_tmp17 ;
4425  unsigned char *__cil_tmp18 ;
4426  unsigned char __cil_tmp19 ;
4427  int __cil_tmp20 ;
4428  int __cil_tmp21 ;
4429  int __cil_tmp22 ;
4430  unsigned char *__cil_tmp23 ;
4431  unsigned char __cil_tmp24 ;
4432  int __cil_tmp25 ;
4433  int __cil_tmp26 ;
4434  int __cil_tmp27 ;
4435  unsigned char *__cil_tmp28 ;
4436  unsigned char __cil_tmp29 ;
4437  int __cil_tmp30 ;
4438  int __cil_tmp31 ;
4439  unsigned char *__cil_tmp32 ;
4440  unsigned char __cil_tmp33 ;
4441  int __cil_tmp34 ;
4442  int __cil_tmp35 ;
4443  int __cil_tmp36 ;
4444  int __cil_tmp37 ;
4445  int __cil_tmp38 ;
4446  unsigned long __cil_tmp39 ;
4447  unsigned long __cil_tmp40 ;
4448  unsigned char *__cil_tmp41 ;
4449  unsigned char __cil_tmp42 ;
4450  int __cil_tmp43 ;
4451  int __cil_tmp44 ;
4452  unsigned char *__cil_tmp45 ;
4453  unsigned char __cil_tmp46 ;
4454  int __cil_tmp47 ;
4455  int __cil_tmp48 ;
4456  unsigned char *__cil_tmp49 ;
4457  unsigned char __cil_tmp50 ;
4458  int __cil_tmp51 ;
4459  int __cil_tmp52 ;
4460  unsigned char *__cil_tmp53 ;
4461  unsigned char __cil_tmp54 ;
4462  int __cil_tmp55 ;
4463  int __cil_tmp56 ;
4464  unsigned char *__cil_tmp57 ;
4465  unsigned char __cil_tmp58 ;
4466  int __cil_tmp59 ;
4467  int __cil_tmp60 ;
4468  int __cil_tmp61 ;
4469  int __cil_tmp62 ;
4470  int __cil_tmp63 ;
4471  int __cil_tmp64 ;
4472  int __cil_tmp65 ;
4473  unsigned long __cil_tmp66 ;
4474  unsigned long __cil_tmp67 ;
4475  __u32 __cil_tmp68 ;
4476  unsigned char *__cil_tmp69 ;
4477  unsigned char __cil_tmp70 ;
4478  int __cil_tmp71 ;
4479  int __cil_tmp72 ;
4480  int __cil_tmp73 ;
4481  unsigned char *__cil_tmp74 ;
4482  unsigned char __cil_tmp75 ;
4483  int __cil_tmp76 ;
4484  int __cil_tmp77 ;
4485  unsigned char *__cil_tmp78 ;
4486  unsigned char __cil_tmp79 ;
4487  int __cil_tmp80 ;
4488  int __cil_tmp81 ;
4489  int __cil_tmp82 ;
4490  int __cil_tmp83 ;
4491  unsigned char *__cil_tmp84 ;
4492  unsigned char __cil_tmp85 ;
4493  int __cil_tmp86 ;
4494  int __cil_tmp87 ;
4495  unsigned char *__cil_tmp88 ;
4496  unsigned char __cil_tmp89 ;
4497  int __cil_tmp90 ;
4498  int __cil_tmp91 ;
4499  unsigned char *__cil_tmp92 ;
4500  unsigned char __cil_tmp93 ;
4501  int __cil_tmp94 ;
4502  int __cil_tmp95 ;
4503  int __cil_tmp96 ;
4504  int __cil_tmp97 ;
4505  unsigned char *__cil_tmp98 ;
4506  unsigned char __cil_tmp99 ;
4507  int __cil_tmp100 ;
4508  int __cil_tmp101 ;
4509  unsigned char *__cil_tmp102 ;
4510  unsigned char __cil_tmp103 ;
4511  int __cil_tmp104 ;
4512  int __cil_tmp105 ;
4513  int __cil_tmp106 ;
4514  unsigned char *__cil_tmp107 ;
4515  unsigned char __cil_tmp108 ;
4516  int __cil_tmp109 ;
4517  int __cil_tmp110 ;
4518  int __cil_tmp111 ;
4519  int __cil_tmp112 ;
4520  unsigned char *__cil_tmp113 ;
4521  unsigned char __cil_tmp114 ;
4522  int __cil_tmp115 ;
4523  int __cil_tmp116 ;
4524  int __cil_tmp117 ;
4525  int __cil_tmp118 ;
4526  int __cil_tmp119 ;
4527  unsigned char *__cil_tmp120 ;
4528  unsigned char __cil_tmp121 ;
4529  int __cil_tmp122 ;
4530  int __cil_tmp123 ;
4531  unsigned char *__cil_tmp124 ;
4532  unsigned char __cil_tmp125 ;
4533  int __cil_tmp126 ;
4534  int __cil_tmp127 ;
4535  __u16 __cil_tmp128 ;
4536  unsigned int __cil_tmp129 ;
4537  int __cil_tmp130 ;
4538  int __cil_tmp131 ;
4539  int __cil_tmp132 ;
4540  int __cil_tmp133 ;
4541  unsigned long __cil_tmp134 ;
4542  unsigned long __cil_tmp135 ;
4543  __u32 __cil_tmp136 ;
4544  int __cil_tmp137 ;
4545  unsigned long __cil_tmp138 ;
4546  unsigned long __cil_tmp139 ;
4547  __u32 __cil_tmp140 ;
4548  int __cil_tmp141 ;
4549  __u16 __cil_tmp142 ;
4550  unsigned int __cil_tmp143 ;
4551
4552  {
4553  {
4554#line 374
4555  __cil_tmp8 = data + 1;
4556#line 374
4557  __cil_tmp9 = *__cil_tmp8;
4558#line 375
4559  if ((int )__cil_tmp9 == 128) {
4560#line 375
4561    goto case_128;
4562  } else
4563#line 386
4564  if ((int )__cil_tmp9 == 194) {
4565#line 386
4566    goto case_194;
4567  } else {
4568    {
4569#line 403
4570    goto switch_default;
4571#line 374
4572    if (0) {
4573      case_128: /* CIL Label */ 
4574      {
4575#line 376
4576      input_report_key(input, 330U, 0);
4577#line 377
4578      input_report_abs(input, 24U, 0);
4579#line 378
4580      input_report_key(input, 331U, 0);
4581#line 379
4582      input_report_key(input, 332U, 0);
4583#line 380
4584      __cil_tmp10 = *((__u16 *)wdata);
4585#line 380
4586      __cil_tmp11 = (unsigned int )__cil_tmp10;
4587#line 380
4588      input_report_key(input, __cil_tmp11, 0);
4589#line 381
4590      input_report_abs(input, 40U, 0);
4591#line 382
4592      __cil_tmp12 = (unsigned long )wdata;
4593#line 382
4594      __cil_tmp13 = __cil_tmp12 + 12;
4595#line 382
4596      __cil_tmp14 = *((__u32 *)__cil_tmp13);
4597#line 382
4598      __cil_tmp15 = (int )__cil_tmp14;
4599#line 382
4600      input_event(input, 4U, 0U, __cil_tmp15);
4601#line 383
4602      *((__u16 *)wdata) = (__u16 )0;
4603#line 384
4604      input_sync(input);
4605      }
4606#line 385
4607      goto switch_break;
4608      case_194: /* CIL Label */ 
4609#line 387
4610      __cil_tmp16 = (unsigned long )wdata;
4611#line 387
4612      __cil_tmp17 = __cil_tmp16 + 8;
4613#line 387
4614      __cil_tmp18 = data + 8;
4615#line 387
4616      __cil_tmp19 = *__cil_tmp18;
4617#line 387
4618      __cil_tmp20 = (int )__cil_tmp19;
4619#line 387
4620      __cil_tmp21 = __cil_tmp20 & 240;
4621#line 387
4622      __cil_tmp22 = __cil_tmp21 << 12;
4623#line 387
4624      __cil_tmp23 = data + 7;
4625#line 387
4626      __cil_tmp24 = *__cil_tmp23;
4627#line 387
4628      __cil_tmp25 = (int )__cil_tmp24;
4629#line 387
4630      __cil_tmp26 = __cil_tmp25 & 15;
4631#line 387
4632      __cil_tmp27 = __cil_tmp26 << 20;
4633#line 387
4634      __cil_tmp28 = data + 3;
4635#line 387
4636      __cil_tmp29 = *__cil_tmp28;
4637#line 387
4638      __cil_tmp30 = (int )__cil_tmp29;
4639#line 387
4640      __cil_tmp31 = __cil_tmp30 >> 4;
4641#line 387
4642      __cil_tmp32 = data + 2;
4643#line 387
4644      __cil_tmp33 = *__cil_tmp32;
4645#line 387
4646      __cil_tmp34 = (int )__cil_tmp33;
4647#line 387
4648      __cil_tmp35 = __cil_tmp34 << 4;
4649#line 387
4650      __cil_tmp36 = __cil_tmp35 | __cil_tmp31;
4651#line 387
4652      __cil_tmp37 = __cil_tmp36 | __cil_tmp27;
4653#line 387
4654      __cil_tmp38 = __cil_tmp37 | __cil_tmp22;
4655#line 387
4656      *((__u32 *)__cil_tmp17) = (__u32 )__cil_tmp38;
4657#line 390
4658      __cil_tmp39 = (unsigned long )wdata;
4659#line 390
4660      __cil_tmp40 = __cil_tmp39 + 12;
4661#line 390
4662      __cil_tmp41 = data + 7;
4663#line 390
4664      __cil_tmp42 = *__cil_tmp41;
4665#line 390
4666      __cil_tmp43 = (int )__cil_tmp42;
4667#line 390
4668      __cil_tmp44 = __cil_tmp43 >> 4;
4669#line 390
4670      __cil_tmp45 = data + 6;
4671#line 390
4672      __cil_tmp46 = *__cil_tmp45;
4673#line 390
4674      __cil_tmp47 = (int )__cil_tmp46;
4675#line 390
4676      __cil_tmp48 = __cil_tmp47 << 4;
4677#line 390
4678      __cil_tmp49 = data + 5;
4679#line 390
4680      __cil_tmp50 = *__cil_tmp49;
4681#line 390
4682      __cil_tmp51 = (int )__cil_tmp50;
4683#line 390
4684      __cil_tmp52 = __cil_tmp51 << 12;
4685#line 390
4686      __cil_tmp53 = data + 4;
4687#line 390
4688      __cil_tmp54 = *__cil_tmp53;
4689#line 390
4690      __cil_tmp55 = (int )__cil_tmp54;
4691#line 390
4692      __cil_tmp56 = __cil_tmp55 << 20;
4693#line 390
4694      __cil_tmp57 = data + 3;
4695#line 390
4696      __cil_tmp58 = *__cil_tmp57;
4697#line 390
4698      __cil_tmp59 = (int )__cil_tmp58;
4699#line 390
4700      __cil_tmp60 = __cil_tmp59 & 15;
4701#line 390
4702      __cil_tmp61 = __cil_tmp60 << 28;
4703#line 390
4704      __cil_tmp62 = __cil_tmp61 + __cil_tmp56;
4705#line 390
4706      __cil_tmp63 = __cil_tmp62 + __cil_tmp52;
4707#line 390
4708      __cil_tmp64 = __cil_tmp63 + __cil_tmp48;
4709#line 390
4710      __cil_tmp65 = __cil_tmp64 + __cil_tmp44;
4711#line 390
4712      *((__u32 *)__cil_tmp40) = (__u32 )__cil_tmp65;
4713      {
4714#line 394
4715      __cil_tmp66 = (unsigned long )wdata;
4716#line 394
4717      __cil_tmp67 = __cil_tmp66 + 8;
4718#line 394
4719      __cil_tmp68 = *((__u32 *)__cil_tmp67);
4720#line 395
4721      if ((int )__cil_tmp68 == 1050626) {
4722#line 395
4723        goto case_1050626;
4724      } else
4725#line 398
4726      if ((int )__cil_tmp68 == 1050634) {
4727#line 398
4728        goto case_1050634;
4729      } else
4730#line 394
4731      if (0) {
4732        case_1050626: /* CIL Label */ 
4733#line 396
4734        *((__u16 *)wdata) = (__u16 )320;
4735#line 397
4736        goto switch_break___0;
4737        case_1050634: /* CIL Label */ 
4738#line 399
4739        *((__u16 *)wdata) = (__u16 )321;
4740#line 400
4741        goto switch_break___0;
4742      } else {
4743        switch_break___0: /* CIL Label */ ;
4744      }
4745      }
4746#line 402
4747      goto switch_break;
4748      switch_default: /* CIL Label */ 
4749      {
4750#line 404
4751      __cil_tmp69 = data + 9;
4752#line 404
4753      __cil_tmp70 = *__cil_tmp69;
4754#line 404
4755      __cil_tmp71 = (int )__cil_tmp70;
4756#line 404
4757      __cil_tmp72 = __cil_tmp71 & 2;
4758#line 404
4759      __cil_tmp73 = __cil_tmp72 >> 1;
4760#line 404
4761      __cil_tmp74 = data + 3;
4762#line 404
4763      __cil_tmp75 = *__cil_tmp74;
4764#line 404
4765      __cil_tmp76 = (int )__cil_tmp75;
4766#line 404
4767      __cil_tmp77 = __cil_tmp76 << 1;
4768#line 404
4769      __cil_tmp78 = data + 2;
4770#line 404
4771      __cil_tmp79 = *__cil_tmp78;
4772#line 404
4773      __cil_tmp80 = (int )__cil_tmp79;
4774#line 404
4775      __cil_tmp81 = __cil_tmp80 << 9;
4776#line 404
4777      __cil_tmp82 = __cil_tmp81 | __cil_tmp77;
4778#line 404
4779      __cil_tmp83 = __cil_tmp82 | __cil_tmp73;
4780#line 404
4781      x = (__u16 )__cil_tmp83;
4782#line 405
4783      __cil_tmp84 = data + 9;
4784#line 405
4785      __cil_tmp85 = *__cil_tmp84;
4786#line 405
4787      __cil_tmp86 = (int )__cil_tmp85;
4788#line 405
4789      __cil_tmp87 = __cil_tmp86 & 1;
4790#line 405
4791      __cil_tmp88 = data + 5;
4792#line 405
4793      __cil_tmp89 = *__cil_tmp88;
4794#line 405
4795      __cil_tmp90 = (int )__cil_tmp89;
4796#line 405
4797      __cil_tmp91 = __cil_tmp90 << 1;
4798#line 405
4799      __cil_tmp92 = data + 4;
4800#line 405
4801      __cil_tmp93 = *__cil_tmp92;
4802#line 405
4803      __cil_tmp94 = (int )__cil_tmp93;
4804#line 405
4805      __cil_tmp95 = __cil_tmp94 << 9;
4806#line 405
4807      __cil_tmp96 = __cil_tmp95 | __cil_tmp91;
4808#line 405
4809      __cil_tmp97 = __cil_tmp96 | __cil_tmp87;
4810#line 405
4811      y = (__u16 )__cil_tmp97;
4812#line 406
4813      __cil_tmp98 = data + 1;
4814#line 406
4815      __cil_tmp99 = *__cil_tmp98;
4816#line 406
4817      __cil_tmp100 = (int )__cil_tmp99;
4818#line 406
4819      __cil_tmp101 = __cil_tmp100 & 1;
4820#line 406
4821      __cil_tmp102 = data + 7;
4822#line 406
4823      __cil_tmp103 = *__cil_tmp102;
4824#line 406
4825      __cil_tmp104 = (int )__cil_tmp103;
4826#line 406
4827      __cil_tmp105 = __cil_tmp104 & 192;
4828#line 406
4829      __cil_tmp106 = __cil_tmp105 >> 5;
4830#line 406
4831      __cil_tmp107 = data + 6;
4832#line 406
4833      __cil_tmp108 = *__cil_tmp107;
4834#line 406
4835      __cil_tmp109 = (int )__cil_tmp108;
4836#line 406
4837      __cil_tmp110 = __cil_tmp109 << 3;
4838#line 406
4839      __cil_tmp111 = __cil_tmp110 | __cil_tmp106;
4840#line 406
4841      __cil_tmp112 = __cil_tmp111 | __cil_tmp101;
4842#line 406
4843      pressure = (__u16 )__cil_tmp112;
4844#line 408
4845      __cil_tmp113 = data + 9;
4846#line 408
4847      __cil_tmp114 = *__cil_tmp113;
4848#line 408
4849      __cil_tmp115 = (int )__cil_tmp114;
4850#line 408
4851      __cil_tmp116 = __cil_tmp115 >> 2;
4852#line 408
4853      __cil_tmp117 = __cil_tmp116 & 63;
4854#line 408
4855      distance = (__u8 )__cil_tmp117;
4856#line 410
4857      __cil_tmp118 = (int )pressure;
4858#line 410
4859      __cil_tmp119 = __cil_tmp118 > 1;
4860#line 410
4861      input_report_key(input, 330U, __cil_tmp119);
4862#line 412
4863      __cil_tmp120 = data + 1;
4864#line 412
4865      __cil_tmp121 = *__cil_tmp120;
4866#line 412
4867      __cil_tmp122 = (int )__cil_tmp121;
4868#line 412
4869      __cil_tmp123 = __cil_tmp122 & 2;
4870#line 412
4871      input_report_key(input, 331U, __cil_tmp123);
4872#line 413
4873      __cil_tmp124 = data + 1;
4874#line 413
4875      __cil_tmp125 = *__cil_tmp124;
4876#line 413
4877      __cil_tmp126 = (int )__cil_tmp125;
4878#line 413
4879      __cil_tmp127 = __cil_tmp126 & 4;
4880#line 413
4881      input_report_key(input, 332U, __cil_tmp127);
4882#line 414
4883      __cil_tmp128 = *((__u16 *)wdata);
4884#line 414
4885      __cil_tmp129 = (unsigned int )__cil_tmp128;
4886#line 414
4887      input_report_key(input, __cil_tmp129, 1);
4888#line 415
4889      __cil_tmp130 = (int )x;
4890#line 415
4891      input_report_abs(input, 0U, __cil_tmp130);
4892#line 416
4893      __cil_tmp131 = (int )y;
4894#line 416
4895      input_report_abs(input, 1U, __cil_tmp131);
4896#line 417
4897      __cil_tmp132 = (int )pressure;
4898#line 417
4899      input_report_abs(input, 24U, __cil_tmp132);
4900#line 418
4901      __cil_tmp133 = (int )distance;
4902#line 418
4903      input_report_abs(input, 25U, __cil_tmp133);
4904#line 419
4905      __cil_tmp134 = (unsigned long )wdata;
4906#line 419
4907      __cil_tmp135 = __cil_tmp134 + 8;
4908#line 419
4909      __cil_tmp136 = *((__u32 *)__cil_tmp135);
4910#line 419
4911      __cil_tmp137 = (int )__cil_tmp136;
4912#line 419
4913      input_report_abs(input, 40U, __cil_tmp137);
4914#line 420
4915      __cil_tmp138 = (unsigned long )wdata;
4916#line 420
4917      __cil_tmp139 = __cil_tmp138 + 12;
4918#line 420
4919      __cil_tmp140 = *((__u32 *)__cil_tmp139);
4920#line 420
4921      __cil_tmp141 = (int )__cil_tmp140;
4922#line 420
4923      input_event(input, 4U, 0U, __cil_tmp141);
4924#line 421
4925      __cil_tmp142 = *((__u16 *)wdata);
4926#line 421
4927      __cil_tmp143 = (unsigned int )__cil_tmp142;
4928#line 421
4929      input_report_key(input, __cil_tmp143, 1);
4930#line 422
4931      input_sync(input);
4932      }
4933#line 423
4934      goto switch_break;
4935    } else {
4936      switch_break: /* CIL Label */ ;
4937    }
4938    }
4939  }
4940  }
4941#line 426
4942  return;
4943}
4944}
4945#line 429 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
4946static void wacom_i4_parse_report(struct hid_device *hdev , struct wacom_data *wdata ,
4947                                  struct input_dev *input , unsigned char *data ) 
4948{ unsigned char *__cil_tmp5 ;
4949  unsigned char __cil_tmp6 ;
4950  unsigned long __cil_tmp7 ;
4951  unsigned long __cil_tmp8 ;
4952  unsigned char *__cil_tmp9 ;
4953  unsigned long __cil_tmp10 ;
4954  unsigned long __cil_tmp11 ;
4955  struct device *__cil_tmp12 ;
4956  struct device  const  *__cil_tmp13 ;
4957  unsigned char *__cil_tmp14 ;
4958  unsigned char __cil_tmp15 ;
4959  int __cil_tmp16 ;
4960  unsigned char *__cil_tmp17 ;
4961  unsigned char __cil_tmp18 ;
4962  int __cil_tmp19 ;
4963
4964  {
4965  {
4966#line 433
4967  __cil_tmp5 = data + 0;
4968#line 433
4969  __cil_tmp6 = *__cil_tmp5;
4970#line 434
4971  if ((int )__cil_tmp6 == 0) {
4972#line 434
4973    goto case_0;
4974  } else
4975#line 436
4976  if ((int )__cil_tmp6 == 2) {
4977#line 436
4978    goto case_2;
4979  } else
4980#line 439
4981  if ((int )__cil_tmp6 == 3) {
4982#line 439
4983    goto case_3;
4984  } else
4985#line 442
4986  if ((int )__cil_tmp6 == 12) {
4987#line 442
4988    goto case_12;
4989  } else {
4990    {
4991#line 445
4992    goto switch_default;
4993#line 433
4994    if (0) {
4995      case_0: /* CIL Label */ 
4996#line 435
4997      goto switch_break;
4998      case_2: /* CIL Label */ 
4999      {
5000#line 437
5001      wacom_i4_parse_pen_report(wdata, input, data);
5002      }
5003#line 438
5004      goto switch_break;
5005      case_3: /* CIL Label */ 
5006#line 440
5007      __cil_tmp7 = (unsigned long )wdata;
5008#line 440
5009      __cil_tmp8 = __cil_tmp7 + 5;
5010#line 440
5011      __cil_tmp9 = data + 2;
5012#line 440
5013      *((__u8 *)__cil_tmp8) = *__cil_tmp9;
5014#line 441
5015      goto switch_break;
5016      case_12: /* CIL Label */ 
5017      {
5018#line 443
5019      wacom_i4_parse_button_report(wdata, input, data);
5020      }
5021#line 444
5022      goto switch_break;
5023      switch_default: /* CIL Label */ 
5024      {
5025#line 446
5026      __cil_tmp10 = (unsigned long )hdev;
5027#line 446
5028      __cil_tmp11 = __cil_tmp10 + 6328;
5029#line 446
5030      __cil_tmp12 = (struct device *)__cil_tmp11;
5031#line 446
5032      __cil_tmp13 = (struct device  const  *)__cil_tmp12;
5033#line 446
5034      __cil_tmp14 = data + 0;
5035#line 446
5036      __cil_tmp15 = *__cil_tmp14;
5037#line 446
5038      __cil_tmp16 = (int )__cil_tmp15;
5039#line 446
5040      __cil_tmp17 = data + 1;
5041#line 446
5042      __cil_tmp18 = *__cil_tmp17;
5043#line 446
5044      __cil_tmp19 = (int )__cil_tmp18;
5045#line 446
5046      dev_err(__cil_tmp13, "Unknown report: %d,%d\n", __cil_tmp16, __cil_tmp19);
5047      }
5048#line 447
5049      goto switch_break;
5050    } else {
5051      switch_break: /* CIL Label */ ;
5052    }
5053    }
5054  }
5055  }
5056#line 449
5057  return;
5058}
5059}
5060#line 451 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
5061static int wacom_raw_event(struct hid_device *hdev , struct hid_report *report , u8 *raw_data ,
5062                           int size ) 
5063{ struct wacom_data *wdata ;
5064  void *tmp ;
5065  struct hid_input *hidinput ;
5066  struct input_dev *input ;
5067  unsigned char *data ;
5068  int i ;
5069  struct list_head  const  *__mptr ;
5070  int tmp___0 ;
5071  unsigned long __cil_tmp13 ;
5072  unsigned long __cil_tmp14 ;
5073  unsigned int __cil_tmp15 ;
5074  unsigned int __cil_tmp16 ;
5075  unsigned long __cil_tmp17 ;
5076  unsigned long __cil_tmp18 ;
5077  struct list_head *__cil_tmp19 ;
5078  struct hid_input *__cil_tmp20 ;
5079  struct list_head *__cil_tmp21 ;
5080  unsigned int __cil_tmp22 ;
5081  char *__cil_tmp23 ;
5082  char *__cil_tmp24 ;
5083  unsigned long __cil_tmp25 ;
5084  unsigned long __cil_tmp26 ;
5085  unsigned char *__cil_tmp27 ;
5086  unsigned char __cil_tmp28 ;
5087  int __cil_tmp29 ;
5088  unsigned long __cil_tmp30 ;
5089  unsigned long __cil_tmp31 ;
5090  __u32 __cil_tmp32 ;
5091  unsigned char *__cil_tmp33 ;
5092  unsigned char __cil_tmp34 ;
5093  unsigned char *__cil_tmp35 ;
5094  unsigned char *__cil_tmp36 ;
5095  unsigned char *__cil_tmp37 ;
5096  unsigned long __cil_tmp38 ;
5097  unsigned long __cil_tmp39 ;
5098  struct device *__cil_tmp40 ;
5099  struct device  const  *__cil_tmp41 ;
5100  unsigned char *__cil_tmp42 ;
5101  unsigned char __cil_tmp43 ;
5102  int __cil_tmp44 ;
5103  unsigned char *__cil_tmp45 ;
5104  unsigned char __cil_tmp46 ;
5105  int __cil_tmp47 ;
5106
5107  {
5108  {
5109#line 454
5110  tmp = hid_get_drvdata(hdev);
5111#line 454
5112  wdata = (struct wacom_data *)tmp;
5113#line 457
5114  data = raw_data;
5115  }
5116  {
5117#line 460
5118  __cil_tmp13 = (unsigned long )hdev;
5119#line 460
5120  __cil_tmp14 = __cil_tmp13 + 7116;
5121#line 460
5122  __cil_tmp15 = *((unsigned int *)__cil_tmp14);
5123#line 460
5124  __cil_tmp16 = __cil_tmp15 & 1U;
5125#line 460
5126  if (! __cil_tmp16) {
5127#line 461
5128    return (0);
5129  } else {
5130
5131  }
5132  }
5133#line 463
5134  __cil_tmp17 = (unsigned long )hdev;
5135#line 463
5136  __cil_tmp18 = __cil_tmp17 + 7128;
5137#line 463
5138  __cil_tmp19 = *((struct list_head **)__cil_tmp18);
5139#line 463
5140  __mptr = (struct list_head  const  *)__cil_tmp19;
5141#line 463
5142  __cil_tmp20 = (struct hid_input *)0;
5143#line 463
5144  __cil_tmp21 = (struct list_head *)__cil_tmp20;
5145#line 463
5146  __cil_tmp22 = (unsigned int )__cil_tmp21;
5147#line 463
5148  __cil_tmp23 = (char *)__mptr;
5149#line 463
5150  __cil_tmp24 = __cil_tmp23 - __cil_tmp22;
5151#line 463
5152  hidinput = (struct hid_input *)__cil_tmp24;
5153#line 464
5154  __cil_tmp25 = (unsigned long )hidinput;
5155#line 464
5156  __cil_tmp26 = __cil_tmp25 + 24;
5157#line 464
5158  input = *((struct input_dev **)__cil_tmp26);
5159  {
5160#line 467
5161  __cil_tmp27 = data + 0;
5162#line 467
5163  __cil_tmp28 = *__cil_tmp27;
5164#line 467
5165  __cil_tmp29 = (int )__cil_tmp28;
5166#line 467
5167  if (__cil_tmp29 != 3) {
5168#line 468
5169    return (0);
5170  } else {
5171
5172  }
5173  }
5174  {
5175#line 470
5176  __cil_tmp30 = (unsigned long )hdev;
5177#line 470
5178  __cil_tmp31 = __cil_tmp30 + 44;
5179#line 470
5180  __cil_tmp32 = *((__u32 *)__cil_tmp31);
5181#line 471
5182  if ((int )__cil_tmp32 == 129) {
5183#line 471
5184    goto case_129;
5185  } else
5186#line 474
5187  if ((int )__cil_tmp32 == 189) {
5188#line 474
5189    goto case_189;
5190  } else
5191#line 470
5192  if (0) {
5193    case_129: /* CIL Label */ 
5194    {
5195#line 472
5196    tmp___0 = wacom_gr_parse_report(hdev, wdata, input, data);
5197    }
5198#line 472
5199    return (tmp___0);
5200#line 473
5201    goto switch_break;
5202    case_189: /* CIL Label */ 
5203#line 475
5204    i = 1;
5205    {
5206#line 477
5207    __cil_tmp33 = data + 0;
5208#line 477
5209    __cil_tmp34 = *__cil_tmp33;
5210#line 478
5211    if ((int )__cil_tmp34 == 4) {
5212#line 478
5213      goto case_4;
5214    } else
5215#line 482
5216    if ((int )__cil_tmp34 == 3) {
5217#line 482
5218      goto case_3;
5219    } else {
5220      {
5221#line 487
5222      goto switch_default;
5223#line 477
5224      if (0) {
5225        case_4: /* CIL Label */ 
5226        {
5227#line 479
5228        __cil_tmp35 = data + i;
5229#line 479
5230        wacom_i4_parse_report(hdev, wdata, input, __cil_tmp35);
5231#line 480
5232        i = i + 10;
5233        }
5234        case_3: /* CIL Label */ 
5235        {
5236#line 483
5237        __cil_tmp36 = data + i;
5238#line 483
5239        wacom_i4_parse_report(hdev, wdata, input, __cil_tmp36);
5240#line 484
5241        i = i + 10;
5242#line 485
5243        __cil_tmp37 = data + i;
5244#line 485
5245        wacom_i4_parse_report(hdev, wdata, input, __cil_tmp37);
5246        }
5247#line 486
5248        goto switch_break___0;
5249        switch_default: /* CIL Label */ 
5250        {
5251#line 488
5252        __cil_tmp38 = (unsigned long )hdev;
5253#line 488
5254        __cil_tmp39 = __cil_tmp38 + 6328;
5255#line 488
5256        __cil_tmp40 = (struct device *)__cil_tmp39;
5257#line 488
5258        __cil_tmp41 = (struct device  const  *)__cil_tmp40;
5259#line 488
5260        __cil_tmp42 = data + 0;
5261#line 488
5262        __cil_tmp43 = *__cil_tmp42;
5263#line 488
5264        __cil_tmp44 = (int )__cil_tmp43;
5265#line 488
5266        __cil_tmp45 = data + 1;
5267#line 488
5268        __cil_tmp46 = *__cil_tmp45;
5269#line 488
5270        __cil_tmp47 = (int )__cil_tmp46;
5271#line 488
5272        dev_err(__cil_tmp41, "Unknown report: %d,%d size:%d\n", __cil_tmp44, __cil_tmp47,
5273                size);
5274        }
5275#line 490
5276        return (0);
5277      } else {
5278        switch_break___0: /* CIL Label */ ;
5279      }
5280      }
5281    }
5282    }
5283  } else {
5284    switch_break: /* CIL Label */ ;
5285  }
5286  }
5287#line 493
5288  return (1);
5289}
5290}
5291#line 496 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
5292static int wacom_input_mapped(struct hid_device *hdev , struct hid_input *hi , struct hid_field *field ,
5293                              struct hid_usage *usage , unsigned long **bit , int *max ) 
5294{ struct input_dev *input ;
5295  unsigned long __cil_tmp8 ;
5296  unsigned long __cil_tmp9 ;
5297  unsigned long __cil_tmp10 ;
5298  unsigned long __cil_tmp11 ;
5299  unsigned long __cil_tmp12 ;
5300  unsigned long __cil_tmp13 ;
5301  unsigned long *__cil_tmp14 ;
5302  unsigned long volatile   *__cil_tmp15 ;
5303  unsigned long __cil_tmp16 ;
5304  unsigned long __cil_tmp17 ;
5305  unsigned long __cil_tmp18 ;
5306  unsigned long __cil_tmp19 ;
5307  unsigned long __cil_tmp20 ;
5308  unsigned long __cil_tmp21 ;
5309  unsigned long __cil_tmp22 ;
5310  unsigned long __cil_tmp23 ;
5311  unsigned long __cil_tmp24 ;
5312  unsigned long __cil_tmp25 ;
5313  unsigned long __cil_tmp26 ;
5314  unsigned long __cil_tmp27 ;
5315  unsigned long __cil_tmp28 ;
5316  unsigned long __cil_tmp29 ;
5317  unsigned long __cil_tmp30 ;
5318  unsigned long __cil_tmp31 ;
5319  unsigned long __cil_tmp32 ;
5320  unsigned long __cil_tmp33 ;
5321  unsigned long *__cil_tmp34 ;
5322  unsigned long volatile   *__cil_tmp35 ;
5323  unsigned long __cil_tmp36 ;
5324  unsigned long __cil_tmp37 ;
5325  unsigned long __cil_tmp38 ;
5326  unsigned long __cil_tmp39 ;
5327  unsigned long *__cil_tmp40 ;
5328  unsigned long volatile   *__cil_tmp41 ;
5329  unsigned long __cil_tmp42 ;
5330  unsigned long __cil_tmp43 ;
5331  unsigned long __cil_tmp44 ;
5332  unsigned long __cil_tmp45 ;
5333  unsigned long *__cil_tmp46 ;
5334  unsigned long volatile   *__cil_tmp47 ;
5335  unsigned long __cil_tmp48 ;
5336  unsigned long __cil_tmp49 ;
5337  unsigned long __cil_tmp50 ;
5338  unsigned long __cil_tmp51 ;
5339  unsigned long *__cil_tmp52 ;
5340  unsigned long volatile   *__cil_tmp53 ;
5341  unsigned long __cil_tmp54 ;
5342  unsigned long __cil_tmp55 ;
5343  unsigned long __cil_tmp56 ;
5344  unsigned long __cil_tmp57 ;
5345  unsigned long *__cil_tmp58 ;
5346  unsigned long volatile   *__cil_tmp59 ;
5347  unsigned long __cil_tmp60 ;
5348  unsigned long __cil_tmp61 ;
5349  unsigned long __cil_tmp62 ;
5350  unsigned long __cil_tmp63 ;
5351  unsigned long *__cil_tmp64 ;
5352  unsigned long volatile   *__cil_tmp65 ;
5353  unsigned long __cil_tmp66 ;
5354  unsigned long __cil_tmp67 ;
5355  unsigned long __cil_tmp68 ;
5356  unsigned long __cil_tmp69 ;
5357  unsigned long *__cil_tmp70 ;
5358  unsigned long volatile   *__cil_tmp71 ;
5359  unsigned long __cil_tmp72 ;
5360  unsigned long __cil_tmp73 ;
5361  unsigned long __cil_tmp74 ;
5362  unsigned long __cil_tmp75 ;
5363  unsigned long *__cil_tmp76 ;
5364  unsigned long volatile   *__cil_tmp77 ;
5365  unsigned long __cil_tmp78 ;
5366  unsigned long __cil_tmp79 ;
5367  unsigned long __cil_tmp80 ;
5368  unsigned long __cil_tmp81 ;
5369  unsigned long *__cil_tmp82 ;
5370  unsigned long volatile   *__cil_tmp83 ;
5371  unsigned long __cil_tmp84 ;
5372  unsigned long __cil_tmp85 ;
5373  unsigned long __cil_tmp86 ;
5374  unsigned long __cil_tmp87 ;
5375  unsigned long *__cil_tmp88 ;
5376  unsigned long volatile   *__cil_tmp89 ;
5377  unsigned long __cil_tmp90 ;
5378  unsigned long __cil_tmp91 ;
5379  unsigned long __cil_tmp92 ;
5380  unsigned long __cil_tmp93 ;
5381  unsigned long *__cil_tmp94 ;
5382  unsigned long volatile   *__cil_tmp95 ;
5383  unsigned long __cil_tmp96 ;
5384  unsigned long __cil_tmp97 ;
5385  unsigned long __cil_tmp98 ;
5386  unsigned long __cil_tmp99 ;
5387  unsigned long *__cil_tmp100 ;
5388  unsigned long volatile   *__cil_tmp101 ;
5389  unsigned long __cil_tmp102 ;
5390  unsigned long __cil_tmp103 ;
5391  unsigned long __cil_tmp104 ;
5392  unsigned long __cil_tmp105 ;
5393  unsigned long *__cil_tmp106 ;
5394  unsigned long volatile   *__cil_tmp107 ;
5395  unsigned long __cil_tmp108 ;
5396  unsigned long __cil_tmp109 ;
5397  __u32 __cil_tmp110 ;
5398  unsigned long __cil_tmp111 ;
5399  unsigned long __cil_tmp112 ;
5400  unsigned long __cil_tmp113 ;
5401  unsigned long __cil_tmp114 ;
5402  unsigned long *__cil_tmp115 ;
5403  unsigned long volatile   *__cil_tmp116 ;
5404  unsigned long __cil_tmp117 ;
5405  unsigned long __cil_tmp118 ;
5406  unsigned long __cil_tmp119 ;
5407  unsigned long __cil_tmp120 ;
5408  unsigned long *__cil_tmp121 ;
5409  unsigned long volatile   *__cil_tmp122 ;
5410  unsigned long __cil_tmp123 ;
5411  unsigned long __cil_tmp124 ;
5412  unsigned long __cil_tmp125 ;
5413  unsigned long __cil_tmp126 ;
5414  unsigned long *__cil_tmp127 ;
5415  unsigned long volatile   *__cil_tmp128 ;
5416  unsigned long __cil_tmp129 ;
5417  unsigned long __cil_tmp130 ;
5418  unsigned long __cil_tmp131 ;
5419  unsigned long __cil_tmp132 ;
5420  unsigned long *__cil_tmp133 ;
5421  unsigned long volatile   *__cil_tmp134 ;
5422  unsigned long __cil_tmp135 ;
5423  unsigned long __cil_tmp136 ;
5424  unsigned long __cil_tmp137 ;
5425  unsigned long __cil_tmp138 ;
5426  unsigned long *__cil_tmp139 ;
5427  unsigned long volatile   *__cil_tmp140 ;
5428  unsigned long __cil_tmp141 ;
5429  unsigned long __cil_tmp142 ;
5430  unsigned long __cil_tmp143 ;
5431  unsigned long __cil_tmp144 ;
5432  unsigned long *__cil_tmp145 ;
5433  unsigned long volatile   *__cil_tmp146 ;
5434  unsigned long __cil_tmp147 ;
5435  unsigned long __cil_tmp148 ;
5436  unsigned long __cil_tmp149 ;
5437  unsigned long __cil_tmp150 ;
5438  unsigned long *__cil_tmp151 ;
5439  unsigned long volatile   *__cil_tmp152 ;
5440  unsigned long __cil_tmp153 ;
5441  unsigned long __cil_tmp154 ;
5442  unsigned long __cil_tmp155 ;
5443  unsigned long __cil_tmp156 ;
5444  unsigned long *__cil_tmp157 ;
5445  unsigned long volatile   *__cil_tmp158 ;
5446  unsigned long __cil_tmp159 ;
5447  unsigned long __cil_tmp160 ;
5448  unsigned long __cil_tmp161 ;
5449  unsigned long __cil_tmp162 ;
5450  unsigned long *__cil_tmp163 ;
5451  unsigned long volatile   *__cil_tmp164 ;
5452
5453  {
5454  {
5455#line 500
5456  __cil_tmp8 = (unsigned long )hi;
5457#line 500
5458  __cil_tmp9 = __cil_tmp8 + 24;
5459#line 500
5460  input = *((struct input_dev **)__cil_tmp9);
5461#line 502
5462  __cil_tmp10 = 0 * 8UL;
5463#line 502
5464  __cil_tmp11 = 32 + __cil_tmp10;
5465#line 502
5466  __cil_tmp12 = (unsigned long )input;
5467#line 502
5468  __cil_tmp13 = __cil_tmp12 + __cil_tmp11;
5469#line 502
5470  __cil_tmp14 = (unsigned long *)__cil_tmp13;
5471#line 502
5472  __cil_tmp15 = (unsigned long volatile   *)__cil_tmp14;
5473#line 502
5474  __set_bit(0, __cil_tmp15);
5475#line 505
5476  __cil_tmp16 = 0 * 8UL;
5477#line 505
5478  __cil_tmp17 = 40 + __cil_tmp16;
5479#line 505
5480  __cil_tmp18 = (unsigned long )input;
5481#line 505
5482  __cil_tmp19 = __cil_tmp18 + __cil_tmp17;
5483#line 505
5484  __cil_tmp20 = 1UL << 2;
5485#line 505
5486  __cil_tmp21 = 1UL << 3;
5487#line 505
5488  __cil_tmp22 = 1UL << 1;
5489#line 505
5490  __cil_tmp23 = __cil_tmp22 | __cil_tmp21;
5491#line 505
5492  __cil_tmp24 = __cil_tmp23 | __cil_tmp20;
5493#line 505
5494  __cil_tmp25 = 0 * 8UL;
5495#line 505
5496  __cil_tmp26 = 40 + __cil_tmp25;
5497#line 505
5498  __cil_tmp27 = (unsigned long )input;
5499#line 505
5500  __cil_tmp28 = __cil_tmp27 + __cil_tmp26;
5501#line 505
5502  __cil_tmp29 = *((unsigned long *)__cil_tmp28);
5503#line 505
5504  *((unsigned long *)__cil_tmp19) = __cil_tmp29 | __cil_tmp24;
5505#line 507
5506  __cil_tmp30 = 0 * 8UL;
5507#line 507
5508  __cil_tmp31 = 144 + __cil_tmp30;
5509#line 507
5510  __cil_tmp32 = (unsigned long )input;
5511#line 507
5512  __cil_tmp33 = __cil_tmp32 + __cil_tmp31;
5513#line 507
5514  __cil_tmp34 = (unsigned long *)__cil_tmp33;
5515#line 507
5516  __cil_tmp35 = (unsigned long volatile   *)__cil_tmp34;
5517#line 507
5518  __set_bit(8, __cil_tmp35);
5519#line 509
5520  __cil_tmp36 = 0 * 8UL;
5521#line 509
5522  __cil_tmp37 = 48 + __cil_tmp36;
5523#line 509
5524  __cil_tmp38 = (unsigned long )input;
5525#line 509
5526  __cil_tmp39 = __cil_tmp38 + __cil_tmp37;
5527#line 509
5528  __cil_tmp40 = (unsigned long *)__cil_tmp39;
5529#line 509
5530  __cil_tmp41 = (unsigned long volatile   *)__cil_tmp40;
5531#line 509
5532  __set_bit(320, __cil_tmp41);
5533#line 510
5534  __cil_tmp42 = 0 * 8UL;
5535#line 510
5536  __cil_tmp43 = 48 + __cil_tmp42;
5537#line 510
5538  __cil_tmp44 = (unsigned long )input;
5539#line 510
5540  __cil_tmp45 = __cil_tmp44 + __cil_tmp43;
5541#line 510
5542  __cil_tmp46 = (unsigned long *)__cil_tmp45;
5543#line 510
5544  __cil_tmp47 = (unsigned long volatile   *)__cil_tmp46;
5545#line 510
5546  __set_bit(330, __cil_tmp47);
5547#line 511
5548  __cil_tmp48 = 0 * 8UL;
5549#line 511
5550  __cil_tmp49 = 48 + __cil_tmp48;
5551#line 511
5552  __cil_tmp50 = (unsigned long )input;
5553#line 511
5554  __cil_tmp51 = __cil_tmp50 + __cil_tmp49;
5555#line 511
5556  __cil_tmp52 = (unsigned long *)__cil_tmp51;
5557#line 511
5558  __cil_tmp53 = (unsigned long volatile   *)__cil_tmp52;
5559#line 511
5560  __set_bit(331, __cil_tmp53);
5561#line 512
5562  __cil_tmp54 = 0 * 8UL;
5563#line 512
5564  __cil_tmp55 = 48 + __cil_tmp54;
5565#line 512
5566  __cil_tmp56 = (unsigned long )input;
5567#line 512
5568  __cil_tmp57 = __cil_tmp56 + __cil_tmp55;
5569#line 512
5570  __cil_tmp58 = (unsigned long *)__cil_tmp57;
5571#line 512
5572  __cil_tmp59 = (unsigned long volatile   *)__cil_tmp58;
5573#line 512
5574  __set_bit(332, __cil_tmp59);
5575#line 513
5576  __cil_tmp60 = 0 * 8UL;
5577#line 513
5578  __cil_tmp61 = 48 + __cil_tmp60;
5579#line 513
5580  __cil_tmp62 = (unsigned long )input;
5581#line 513
5582  __cil_tmp63 = __cil_tmp62 + __cil_tmp61;
5583#line 513
5584  __cil_tmp64 = (unsigned long *)__cil_tmp63;
5585#line 513
5586  __cil_tmp65 = (unsigned long volatile   *)__cil_tmp64;
5587#line 513
5588  __set_bit(272, __cil_tmp65);
5589#line 514
5590  __cil_tmp66 = 0 * 8UL;
5591#line 514
5592  __cil_tmp67 = 48 + __cil_tmp66;
5593#line 514
5594  __cil_tmp68 = (unsigned long )input;
5595#line 514
5596  __cil_tmp69 = __cil_tmp68 + __cil_tmp67;
5597#line 514
5598  __cil_tmp70 = (unsigned long *)__cil_tmp69;
5599#line 514
5600  __cil_tmp71 = (unsigned long volatile   *)__cil_tmp70;
5601#line 514
5602  __set_bit(273, __cil_tmp71);
5603#line 515
5604  __cil_tmp72 = 0 * 8UL;
5605#line 515
5606  __cil_tmp73 = 48 + __cil_tmp72;
5607#line 515
5608  __cil_tmp74 = (unsigned long )input;
5609#line 515
5610  __cil_tmp75 = __cil_tmp74 + __cil_tmp73;
5611#line 515
5612  __cil_tmp76 = (unsigned long *)__cil_tmp75;
5613#line 515
5614  __cil_tmp77 = (unsigned long volatile   *)__cil_tmp76;
5615#line 515
5616  __set_bit(274, __cil_tmp77);
5617#line 518
5618  input_set_capability(input, 4U, 0U);
5619#line 520
5620  __cil_tmp78 = 0 * 8UL;
5621#line 520
5622  __cil_tmp79 = 48 + __cil_tmp78;
5623#line 520
5624  __cil_tmp80 = (unsigned long )input;
5625#line 520
5626  __cil_tmp81 = __cil_tmp80 + __cil_tmp79;
5627#line 520
5628  __cil_tmp82 = (unsigned long *)__cil_tmp81;
5629#line 520
5630  __cil_tmp83 = (unsigned long volatile   *)__cil_tmp82;
5631#line 520
5632  __set_bit(256, __cil_tmp83);
5633#line 521
5634  __cil_tmp84 = 0 * 8UL;
5635#line 521
5636  __cil_tmp85 = 48 + __cil_tmp84;
5637#line 521
5638  __cil_tmp86 = (unsigned long )input;
5639#line 521
5640  __cil_tmp87 = __cil_tmp86 + __cil_tmp85;
5641#line 521
5642  __cil_tmp88 = (unsigned long *)__cil_tmp87;
5643#line 521
5644  __cil_tmp89 = (unsigned long volatile   *)__cil_tmp88;
5645#line 521
5646  __set_bit(257, __cil_tmp89);
5647#line 522
5648  __cil_tmp90 = 0 * 8UL;
5649#line 522
5650  __cil_tmp91 = 48 + __cil_tmp90;
5651#line 522
5652  __cil_tmp92 = (unsigned long )input;
5653#line 522
5654  __cil_tmp93 = __cil_tmp92 + __cil_tmp91;
5655#line 522
5656  __cil_tmp94 = (unsigned long *)__cil_tmp93;
5657#line 522
5658  __cil_tmp95 = (unsigned long volatile   *)__cil_tmp94;
5659#line 522
5660  __set_bit(325, __cil_tmp95);
5661#line 525
5662  __cil_tmp96 = 0 * 8UL;
5663#line 525
5664  __cil_tmp97 = 48 + __cil_tmp96;
5665#line 525
5666  __cil_tmp98 = (unsigned long )input;
5667#line 525
5668  __cil_tmp99 = __cil_tmp98 + __cil_tmp97;
5669#line 525
5670  __cil_tmp100 = (unsigned long *)__cil_tmp99;
5671#line 525
5672  __cil_tmp101 = (unsigned long volatile   *)__cil_tmp100;
5673#line 525
5674  __set_bit(321, __cil_tmp101);
5675#line 526
5676  __cil_tmp102 = 0 * 8UL;
5677#line 526
5678  __cil_tmp103 = 48 + __cil_tmp102;
5679#line 526
5680  __cil_tmp104 = (unsigned long )input;
5681#line 526
5682  __cil_tmp105 = __cil_tmp104 + __cil_tmp103;
5683#line 526
5684  __cil_tmp106 = (unsigned long *)__cil_tmp105;
5685#line 526
5686  __cil_tmp107 = (unsigned long volatile   *)__cil_tmp106;
5687#line 526
5688  __set_bit(326, __cil_tmp107);
5689  }
5690  {
5691#line 528
5692  __cil_tmp108 = (unsigned long )hdev;
5693#line 528
5694  __cil_tmp109 = __cil_tmp108 + 44;
5695#line 528
5696  __cil_tmp110 = *((__u32 *)__cil_tmp109);
5697#line 529
5698  if ((int )__cil_tmp110 == 129) {
5699#line 529
5700    goto case_129;
5701  } else
5702#line 535
5703  if ((int )__cil_tmp110 == 189) {
5704#line 535
5705    goto case_189;
5706  } else
5707#line 528
5708  if (0) {
5709    case_129: /* CIL Label */ 
5710    {
5711#line 530
5712    input_set_abs_params(input, 0U, 0, 16704, 4, 0);
5713#line 531
5714    input_set_abs_params(input, 1U, 0, 12064, 4, 0);
5715#line 532
5716    input_set_abs_params(input, 24U, 0, 511, 0, 0);
5717#line 533
5718    input_set_abs_params(input, 25U, 0, 32, 0, 0);
5719    }
5720#line 534
5721    goto switch_break;
5722    case_189: /* CIL Label */ 
5723    {
5724#line 536
5725    __cil_tmp111 = 0 * 8UL;
5726#line 536
5727    __cil_tmp112 = 152 + __cil_tmp111;
5728#line 536
5729    __cil_tmp113 = (unsigned long )input;
5730#line 536
5731    __cil_tmp114 = __cil_tmp113 + __cil_tmp112;
5732#line 536
5733    __cil_tmp115 = (unsigned long *)__cil_tmp114;
5734#line 536
5735    __cil_tmp116 = (unsigned long volatile   *)__cil_tmp115;
5736#line 536
5737    __set_bit(8, __cil_tmp116);
5738#line 537
5739    __cil_tmp117 = 0 * 8UL;
5740#line 537
5741    __cil_tmp118 = 152 + __cil_tmp117;
5742#line 537
5743    __cil_tmp119 = (unsigned long )input;
5744#line 537
5745    __cil_tmp120 = __cil_tmp119 + __cil_tmp118;
5746#line 537
5747    __cil_tmp121 = (unsigned long *)__cil_tmp120;
5748#line 537
5749    __cil_tmp122 = (unsigned long volatile   *)__cil_tmp121;
5750#line 537
5751    __set_bit(40, __cil_tmp122);
5752#line 538
5753    __cil_tmp123 = 0 * 8UL;
5754#line 538
5755    __cil_tmp124 = 48 + __cil_tmp123;
5756#line 538
5757    __cil_tmp125 = (unsigned long )input;
5758#line 538
5759    __cil_tmp126 = __cil_tmp125 + __cil_tmp124;
5760#line 538
5761    __cil_tmp127 = (unsigned long *)__cil_tmp126;
5762#line 538
5763    __cil_tmp128 = (unsigned long volatile   *)__cil_tmp127;
5764#line 538
5765    __set_bit(258, __cil_tmp128);
5766#line 539
5767    __cil_tmp129 = 0 * 8UL;
5768#line 539
5769    __cil_tmp130 = 48 + __cil_tmp129;
5770#line 539
5771    __cil_tmp131 = (unsigned long )input;
5772#line 539
5773    __cil_tmp132 = __cil_tmp131 + __cil_tmp130;
5774#line 539
5775    __cil_tmp133 = (unsigned long *)__cil_tmp132;
5776#line 539
5777    __cil_tmp134 = (unsigned long volatile   *)__cil_tmp133;
5778#line 539
5779    __set_bit(259, __cil_tmp134);
5780#line 540
5781    __cil_tmp135 = 0 * 8UL;
5782#line 540
5783    __cil_tmp136 = 48 + __cil_tmp135;
5784#line 540
5785    __cil_tmp137 = (unsigned long )input;
5786#line 540
5787    __cil_tmp138 = __cil_tmp137 + __cil_tmp136;
5788#line 540
5789    __cil_tmp139 = (unsigned long *)__cil_tmp138;
5790#line 540
5791    __cil_tmp140 = (unsigned long volatile   *)__cil_tmp139;
5792#line 540
5793    __set_bit(260, __cil_tmp140);
5794#line 541
5795    __cil_tmp141 = 0 * 8UL;
5796#line 541
5797    __cil_tmp142 = 48 + __cil_tmp141;
5798#line 541
5799    __cil_tmp143 = (unsigned long )input;
5800#line 541
5801    __cil_tmp144 = __cil_tmp143 + __cil_tmp142;
5802#line 541
5803    __cil_tmp145 = (unsigned long *)__cil_tmp144;
5804#line 541
5805    __cil_tmp146 = (unsigned long volatile   *)__cil_tmp145;
5806#line 541
5807    __set_bit(261, __cil_tmp146);
5808#line 542
5809    __cil_tmp147 = 0 * 8UL;
5810#line 542
5811    __cil_tmp148 = 48 + __cil_tmp147;
5812#line 542
5813    __cil_tmp149 = (unsigned long )input;
5814#line 542
5815    __cil_tmp150 = __cil_tmp149 + __cil_tmp148;
5816#line 542
5817    __cil_tmp151 = (unsigned long *)__cil_tmp150;
5818#line 542
5819    __cil_tmp152 = (unsigned long volatile   *)__cil_tmp151;
5820#line 542
5821    __set_bit(262, __cil_tmp152);
5822#line 543
5823    __cil_tmp153 = 0 * 8UL;
5824#line 543
5825    __cil_tmp154 = 48 + __cil_tmp153;
5826#line 543
5827    __cil_tmp155 = (unsigned long )input;
5828#line 543
5829    __cil_tmp156 = __cil_tmp155 + __cil_tmp154;
5830#line 543
5831    __cil_tmp157 = (unsigned long *)__cil_tmp156;
5832#line 543
5833    __cil_tmp158 = (unsigned long volatile   *)__cil_tmp157;
5834#line 543
5835    __set_bit(263, __cil_tmp158);
5836#line 544
5837    __cil_tmp159 = 0 * 8UL;
5838#line 544
5839    __cil_tmp160 = 48 + __cil_tmp159;
5840#line 544
5841    __cil_tmp161 = (unsigned long )input;
5842#line 544
5843    __cil_tmp162 = __cil_tmp161 + __cil_tmp160;
5844#line 544
5845    __cil_tmp163 = (unsigned long *)__cil_tmp162;
5846#line 544
5847    __cil_tmp164 = (unsigned long volatile   *)__cil_tmp163;
5848#line 544
5849    __set_bit(264, __cil_tmp164);
5850#line 545
5851    input_set_abs_params(input, 8U, 0, 71, 0, 0);
5852#line 546
5853    input_set_abs_params(input, 0U, 0, 40640, 4, 0);
5854#line 547
5855    input_set_abs_params(input, 1U, 0, 25400, 4, 0);
5856#line 548
5857    input_set_abs_params(input, 24U, 0, 2047, 0, 0);
5858#line 549
5859    input_set_abs_params(input, 25U, 0, 63, 0, 0);
5860    }
5861#line 550
5862    goto switch_break;
5863  } else {
5864    switch_break: /* CIL Label */ ;
5865  }
5866  }
5867#line 553
5868  return (0);
5869}
5870}
5871#line 556 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
5872static int wacom_probe(struct hid_device *hdev , struct hid_device_id  const  *id ) 
5873{ struct wacom_data *wdata ;
5874  int ret ;
5875  void *tmp ;
5876  void *__cil_tmp6 ;
5877  unsigned long __cil_tmp7 ;
5878  unsigned long __cil_tmp8 ;
5879  unsigned long __cil_tmp9 ;
5880  unsigned long __cil_tmp10 ;
5881  struct device *__cil_tmp11 ;
5882  struct device  const  *__cil_tmp12 ;
5883  void *__cil_tmp13 ;
5884  unsigned long __cil_tmp14 ;
5885  unsigned long __cil_tmp15 ;
5886  struct device *__cil_tmp16 ;
5887  struct device  const  *__cil_tmp17 ;
5888  unsigned long __cil_tmp18 ;
5889  unsigned long __cil_tmp19 ;
5890  struct device *__cil_tmp20 ;
5891  struct device  const  *__cil_tmp21 ;
5892  unsigned long __cil_tmp22 ;
5893  unsigned long __cil_tmp23 ;
5894  struct device *__cil_tmp24 ;
5895  struct device_attribute  const  *__cil_tmp25 ;
5896  unsigned long __cil_tmp26 ;
5897  unsigned long __cil_tmp27 ;
5898  struct device *__cil_tmp28 ;
5899  struct device  const  *__cil_tmp29 ;
5900  unsigned long __cil_tmp30 ;
5901  unsigned long __cil_tmp31 ;
5902  __u32 __cil_tmp32 ;
5903  u8 __cil_tmp33 ;
5904  unsigned long __cil_tmp34 ;
5905  unsigned long __cil_tmp35 ;
5906  unsigned long __cil_tmp36 ;
5907  unsigned long __cil_tmp37 ;
5908  char *__cil_tmp38 ;
5909  unsigned long __cil_tmp39 ;
5910  unsigned long __cil_tmp40 ;
5911  unsigned long __cil_tmp41 ;
5912  unsigned long __cil_tmp42 ;
5913  unsigned long __cil_tmp43 ;
5914  unsigned long __cil_tmp44 ;
5915  unsigned long __cil_tmp45 ;
5916  unsigned long __cil_tmp46 ;
5917  unsigned long __cil_tmp47 ;
5918  unsigned long __cil_tmp48 ;
5919  unsigned long __cil_tmp49 ;
5920  unsigned long __cil_tmp50 ;
5921  unsigned long __cil_tmp51 ;
5922  unsigned long __cil_tmp52 ;
5923  unsigned long __cil_tmp53 ;
5924  unsigned long __cil_tmp54 ;
5925  unsigned long __cil_tmp55 ;
5926  unsigned long __cil_tmp56 ;
5927  unsigned long __cil_tmp57 ;
5928  unsigned long __cil_tmp58 ;
5929  unsigned long __cil_tmp59 ;
5930  unsigned long __cil_tmp60 ;
5931  unsigned long __cil_tmp61 ;
5932  unsigned long __cil_tmp62 ;
5933  struct device *__cil_tmp63 ;
5934  unsigned long __cil_tmp64 ;
5935  unsigned long __cil_tmp65 ;
5936  struct power_supply *__cil_tmp66 ;
5937  unsigned long __cil_tmp67 ;
5938  unsigned long __cil_tmp68 ;
5939  struct device *__cil_tmp69 ;
5940  struct device  const  *__cil_tmp70 ;
5941  unsigned long __cil_tmp71 ;
5942  unsigned long __cil_tmp72 ;
5943  struct power_supply *__cil_tmp73 ;
5944  unsigned long __cil_tmp74 ;
5945  unsigned long __cil_tmp75 ;
5946  struct device *__cil_tmp76 ;
5947  unsigned long __cil_tmp77 ;
5948  unsigned long __cil_tmp78 ;
5949  unsigned long __cil_tmp79 ;
5950  unsigned long __cil_tmp80 ;
5951  unsigned long __cil_tmp81 ;
5952  unsigned long __cil_tmp82 ;
5953  unsigned long __cil_tmp83 ;
5954  unsigned long __cil_tmp84 ;
5955  unsigned long __cil_tmp85 ;
5956  unsigned long __cil_tmp86 ;
5957  unsigned long __cil_tmp87 ;
5958  unsigned long __cil_tmp88 ;
5959  unsigned long __cil_tmp89 ;
5960  unsigned long __cil_tmp90 ;
5961  unsigned long __cil_tmp91 ;
5962  unsigned long __cil_tmp92 ;
5963  unsigned long __cil_tmp93 ;
5964  unsigned long __cil_tmp94 ;
5965  unsigned long __cil_tmp95 ;
5966  unsigned long __cil_tmp96 ;
5967  unsigned long __cil_tmp97 ;
5968  unsigned long __cil_tmp98 ;
5969  struct device *__cil_tmp99 ;
5970  unsigned long __cil_tmp100 ;
5971  unsigned long __cil_tmp101 ;
5972  struct power_supply *__cil_tmp102 ;
5973  unsigned long __cil_tmp103 ;
5974  unsigned long __cil_tmp104 ;
5975  struct device *__cil_tmp105 ;
5976  struct device  const  *__cil_tmp106 ;
5977  unsigned long __cil_tmp107 ;
5978  unsigned long __cil_tmp108 ;
5979  struct power_supply *__cil_tmp109 ;
5980  unsigned long __cil_tmp110 ;
5981  unsigned long __cil_tmp111 ;
5982  struct device *__cil_tmp112 ;
5983  unsigned long __cil_tmp113 ;
5984  unsigned long __cil_tmp114 ;
5985  struct power_supply *__cil_tmp115 ;
5986  unsigned long __cil_tmp116 ;
5987  unsigned long __cil_tmp117 ;
5988  struct device *__cil_tmp118 ;
5989  struct device_attribute  const  *__cil_tmp119 ;
5990  void const   *__cil_tmp120 ;
5991
5992  {
5993  {
5994#line 562
5995  tmp = kzalloc(456UL, 208U);
5996#line 562
5997  wdata = (struct wacom_data *)tmp;
5998  }
5999  {
6000#line 563
6001  __cil_tmp6 = (void *)0;
6002#line 563
6003  __cil_tmp7 = (unsigned long )__cil_tmp6;
6004#line 563
6005  __cil_tmp8 = (unsigned long )wdata;
6006#line 563
6007  if (__cil_tmp8 == __cil_tmp7) {
6008    {
6009#line 564
6010    __cil_tmp9 = (unsigned long )hdev;
6011#line 564
6012    __cil_tmp10 = __cil_tmp9 + 6328;
6013#line 564
6014    __cil_tmp11 = (struct device *)__cil_tmp10;
6015#line 564
6016    __cil_tmp12 = (struct device  const  *)__cil_tmp11;
6017#line 564
6018    dev_err(__cil_tmp12, "can\'t alloc wacom descriptor\n");
6019    }
6020#line 565
6021    return (-12);
6022  } else {
6023
6024  }
6025  }
6026  {
6027#line 568
6028  __cil_tmp13 = (void *)wdata;
6029#line 568
6030  hid_set_drvdata(hdev, __cil_tmp13);
6031#line 571
6032  ret = (int )hid_parse(hdev);
6033  }
6034#line 572
6035  if (ret) {
6036    {
6037#line 573
6038    __cil_tmp14 = (unsigned long )hdev;
6039#line 573
6040    __cil_tmp15 = __cil_tmp14 + 6328;
6041#line 573
6042    __cil_tmp16 = (struct device *)__cil_tmp15;
6043#line 573
6044    __cil_tmp17 = (struct device  const  *)__cil_tmp16;
6045#line 573
6046    dev_err(__cil_tmp17, "parse failed\n");
6047    }
6048#line 574
6049    goto err_free;
6050  } else {
6051
6052  }
6053  {
6054#line 577
6055  ret = (int )hid_hw_start(hdev, 45U);
6056  }
6057#line 578
6058  if (ret) {
6059    {
6060#line 579
6061    __cil_tmp18 = (unsigned long )hdev;
6062#line 579
6063    __cil_tmp19 = __cil_tmp18 + 6328;
6064#line 579
6065    __cil_tmp20 = (struct device *)__cil_tmp19;
6066#line 579
6067    __cil_tmp21 = (struct device  const  *)__cil_tmp20;
6068#line 579
6069    dev_err(__cil_tmp21, "hw start failed\n");
6070    }
6071#line 580
6072    goto err_free;
6073  } else {
6074
6075  }
6076  {
6077#line 583
6078  __cil_tmp22 = (unsigned long )hdev;
6079#line 583
6080  __cil_tmp23 = __cil_tmp22 + 6328;
6081#line 583
6082  __cil_tmp24 = (struct device *)__cil_tmp23;
6083#line 583
6084  __cil_tmp25 = (struct device_attribute  const  *)(& dev_attr_speed);
6085#line 583
6086  ret = device_create_file(__cil_tmp24, __cil_tmp25);
6087  }
6088#line 584
6089  if (ret) {
6090    {
6091#line 585
6092    __cil_tmp26 = (unsigned long )hdev;
6093#line 585
6094    __cil_tmp27 = __cil_tmp26 + 6328;
6095#line 585
6096    __cil_tmp28 = (struct device *)__cil_tmp27;
6097#line 585
6098    __cil_tmp29 = (struct device  const  *)__cil_tmp28;
6099#line 585
6100    dev_warn(__cil_tmp29, "can\'t create sysfs speed attribute err: %d\n", ret);
6101    }
6102  } else {
6103
6104  }
6105  {
6106#line 588
6107  __cil_tmp30 = (unsigned long )hdev;
6108#line 588
6109  __cil_tmp31 = __cil_tmp30 + 44;
6110#line 588
6111  __cil_tmp32 = *((__u32 *)__cil_tmp31);
6112#line 589
6113  if ((int )__cil_tmp32 == 129) {
6114#line 589
6115    goto case_129;
6116  } else
6117#line 593
6118  if ((int )__cil_tmp32 == 189) {
6119#line 593
6120    goto case_189;
6121  } else
6122#line 588
6123  if (0) {
6124    case_129: /* CIL Label */ 
6125    {
6126#line 591
6127    __cil_tmp33 = (u8 )1;
6128#line 591
6129    wacom_poke(hdev, __cil_tmp33);
6130    }
6131#line 592
6132    goto switch_break;
6133    case_189: /* CIL Label */ 
6134    {
6135#line 594
6136    __cil_tmp34 = 0 * 1UL;
6137#line 594
6138    __cil_tmp35 = 7168 + __cil_tmp34;
6139#line 594
6140    __cil_tmp36 = (unsigned long )hdev;
6141#line 594
6142    __cil_tmp37 = __cil_tmp36 + __cil_tmp35;
6143#line 594
6144    __cil_tmp38 = (char *)__cil_tmp37;
6145#line 594
6146    sprintf(__cil_tmp38, "%s", "Wacom Intuos4 WL");
6147#line 595
6148    __cil_tmp39 = (unsigned long )wdata;
6149#line 595
6150    __cil_tmp40 = __cil_tmp39 + 5;
6151#line 595
6152    *((__u8 *)__cil_tmp40) = (__u8 )0;
6153#line 596
6154    wacom_set_features(hdev);
6155    }
6156#line 597
6157    goto switch_break;
6158  } else {
6159    switch_break: /* CIL Label */ ;
6160  }
6161  }
6162  {
6163#line 601
6164  __cil_tmp41 = 24 + 16;
6165#line 601
6166  __cil_tmp42 = (unsigned long )wdata;
6167#line 601
6168  __cil_tmp43 = __cil_tmp42 + __cil_tmp41;
6169#line 601
6170  __cil_tmp44 = 0 * 4UL;
6171#line 601
6172  __cil_tmp45 = (unsigned long )(wacom_battery_props) + __cil_tmp44;
6173#line 601
6174  *((enum power_supply_property **)__cil_tmp43) = (enum power_supply_property *)__cil_tmp45;
6175#line 602
6176  __cil_tmp46 = 24 + 24;
6177#line 602
6178  __cil_tmp47 = (unsigned long )wdata;
6179#line 602
6180  __cil_tmp48 = __cil_tmp47 + __cil_tmp46;
6181#line 602
6182  __cil_tmp49 = 12UL / 4UL;
6183#line 602
6184  *((size_t *)__cil_tmp48) = __cil_tmp49 + 0UL;
6185#line 603
6186  __cil_tmp50 = 24 + 48;
6187#line 603
6188  __cil_tmp51 = (unsigned long )wdata;
6189#line 603
6190  __cil_tmp52 = __cil_tmp51 + __cil_tmp50;
6191#line 603
6192  *((int (**)(struct power_supply *psy , enum power_supply_property psp , union power_supply_propval *val ))__cil_tmp52) = & wacom_battery_get_property;
6193#line 604
6194  __cil_tmp53 = (unsigned long )wdata;
6195#line 604
6196  __cil_tmp54 = __cil_tmp53 + 24;
6197#line 604
6198  *((char const   **)__cil_tmp54) = "wacom_battery";
6199#line 605
6200  __cil_tmp55 = 24 + 8;
6201#line 605
6202  __cil_tmp56 = (unsigned long )wdata;
6203#line 605
6204  __cil_tmp57 = __cil_tmp56 + __cil_tmp55;
6205#line 605
6206  *((enum power_supply_type *)__cil_tmp57) = (enum power_supply_type )1;
6207#line 606
6208  __cil_tmp58 = 24 + 88;
6209#line 606
6210  __cil_tmp59 = (unsigned long )wdata;
6211#line 606
6212  __cil_tmp60 = __cil_tmp59 + __cil_tmp58;
6213#line 606
6214  *((int *)__cil_tmp60) = 0;
6215#line 609
6216  __cil_tmp61 = (unsigned long )hdev;
6217#line 609
6218  __cil_tmp62 = __cil_tmp61 + 6328;
6219#line 609
6220  __cil_tmp63 = (struct device *)__cil_tmp62;
6221#line 609
6222  __cil_tmp64 = (unsigned long )wdata;
6223#line 609
6224  __cil_tmp65 = __cil_tmp64 + 24;
6225#line 609
6226  __cil_tmp66 = (struct power_supply *)__cil_tmp65;
6227#line 609
6228  ret = power_supply_register(__cil_tmp63, __cil_tmp66);
6229  }
6230#line 610
6231  if (ret) {
6232    {
6233#line 611
6234    __cil_tmp67 = (unsigned long )hdev;
6235#line 611
6236    __cil_tmp68 = __cil_tmp67 + 6328;
6237#line 611
6238    __cil_tmp69 = (struct device *)__cil_tmp68;
6239#line 611
6240    __cil_tmp70 = (struct device  const  *)__cil_tmp69;
6241#line 611
6242    dev_warn(__cil_tmp70, "can\'t create sysfs battery attribute, err: %d\n", ret);
6243    }
6244#line 613
6245    goto err_battery;
6246  } else {
6247
6248  }
6249  {
6250#line 616
6251  __cil_tmp71 = (unsigned long )wdata;
6252#line 616
6253  __cil_tmp72 = __cil_tmp71 + 24;
6254#line 616
6255  __cil_tmp73 = (struct power_supply *)__cil_tmp72;
6256#line 616
6257  __cil_tmp74 = (unsigned long )hdev;
6258#line 616
6259  __cil_tmp75 = __cil_tmp74 + 6328;
6260#line 616
6261  __cil_tmp76 = (struct device *)__cil_tmp75;
6262#line 616
6263  power_supply_powers(__cil_tmp73, __cil_tmp76);
6264#line 618
6265  __cil_tmp77 = 240 + 16;
6266#line 618
6267  __cil_tmp78 = (unsigned long )wdata;
6268#line 618
6269  __cil_tmp79 = __cil_tmp78 + __cil_tmp77;
6270#line 618
6271  __cil_tmp80 = 0 * 4UL;
6272#line 618
6273  __cil_tmp81 = (unsigned long )(wacom_ac_props) + __cil_tmp80;
6274#line 618
6275  *((enum power_supply_property **)__cil_tmp79) = (enum power_supply_property *)__cil_tmp81;
6276#line 619
6277  __cil_tmp82 = 240 + 24;
6278#line 619
6279  __cil_tmp83 = (unsigned long )wdata;
6280#line 619
6281  __cil_tmp84 = __cil_tmp83 + __cil_tmp82;
6282#line 619
6283  __cil_tmp85 = 12UL / 4UL;
6284#line 619
6285  *((size_t *)__cil_tmp84) = __cil_tmp85 + 0UL;
6286#line 620
6287  __cil_tmp86 = 240 + 48;
6288#line 620
6289  __cil_tmp87 = (unsigned long )wdata;
6290#line 620
6291  __cil_tmp88 = __cil_tmp87 + __cil_tmp86;
6292#line 620
6293  *((int (**)(struct power_supply *psy , enum power_supply_property psp , union power_supply_propval *val ))__cil_tmp88) = & wacom_ac_get_property;
6294#line 621
6295  __cil_tmp89 = (unsigned long )wdata;
6296#line 621
6297  __cil_tmp90 = __cil_tmp89 + 240;
6298#line 621
6299  *((char const   **)__cil_tmp90) = "wacom_ac";
6300#line 622
6301  __cil_tmp91 = 240 + 8;
6302#line 622
6303  __cil_tmp92 = (unsigned long )wdata;
6304#line 622
6305  __cil_tmp93 = __cil_tmp92 + __cil_tmp91;
6306#line 622
6307  *((enum power_supply_type *)__cil_tmp93) = (enum power_supply_type )3;
6308#line 623
6309  __cil_tmp94 = 240 + 88;
6310#line 623
6311  __cil_tmp95 = (unsigned long )wdata;
6312#line 623
6313  __cil_tmp96 = __cil_tmp95 + __cil_tmp94;
6314#line 623
6315  *((int *)__cil_tmp96) = 0;
6316#line 625
6317  __cil_tmp97 = (unsigned long )hdev;
6318#line 625
6319  __cil_tmp98 = __cil_tmp97 + 6328;
6320#line 625
6321  __cil_tmp99 = (struct device *)__cil_tmp98;
6322#line 625
6323  __cil_tmp100 = (unsigned long )wdata;
6324#line 625
6325  __cil_tmp101 = __cil_tmp100 + 240;
6326#line 625
6327  __cil_tmp102 = (struct power_supply *)__cil_tmp101;
6328#line 625
6329  ret = power_supply_register(__cil_tmp99, __cil_tmp102);
6330  }
6331#line 626
6332  if (ret) {
6333    {
6334#line 627
6335    __cil_tmp103 = (unsigned long )hdev;
6336#line 627
6337    __cil_tmp104 = __cil_tmp103 + 6328;
6338#line 627
6339    __cil_tmp105 = (struct device *)__cil_tmp104;
6340#line 627
6341    __cil_tmp106 = (struct device  const  *)__cil_tmp105;
6342#line 627
6343    dev_warn(__cil_tmp106, "can\'t create ac battery attribute, err: %d\n", ret);
6344    }
6345#line 629
6346    goto err_ac;
6347  } else {
6348
6349  }
6350  {
6351#line 632
6352  __cil_tmp107 = (unsigned long )wdata;
6353#line 632
6354  __cil_tmp108 = __cil_tmp107 + 240;
6355#line 632
6356  __cil_tmp109 = (struct power_supply *)__cil_tmp108;
6357#line 632
6358  __cil_tmp110 = (unsigned long )hdev;
6359#line 632
6360  __cil_tmp111 = __cil_tmp110 + 6328;
6361#line 632
6362  __cil_tmp112 = (struct device *)__cil_tmp111;
6363#line 632
6364  power_supply_powers(__cil_tmp109, __cil_tmp112);
6365  }
6366#line 634
6367  return (0);
6368  err_ac: 
6369  {
6370#line 638
6371  __cil_tmp113 = (unsigned long )wdata;
6372#line 638
6373  __cil_tmp114 = __cil_tmp113 + 24;
6374#line 638
6375  __cil_tmp115 = (struct power_supply *)__cil_tmp114;
6376#line 638
6377  power_supply_unregister(__cil_tmp115);
6378  }
6379  err_battery: 
6380  {
6381#line 640
6382  __cil_tmp116 = (unsigned long )hdev;
6383#line 640
6384  __cil_tmp117 = __cil_tmp116 + 6328;
6385#line 640
6386  __cil_tmp118 = (struct device *)__cil_tmp117;
6387#line 640
6388  __cil_tmp119 = (struct device_attribute  const  *)(& dev_attr_speed);
6389#line 640
6390  device_remove_file(__cil_tmp118, __cil_tmp119);
6391#line 641
6392  hid_hw_stop(hdev);
6393  }
6394  err_free: 
6395  {
6396#line 644
6397  __cil_tmp120 = (void const   *)wdata;
6398#line 644
6399  kfree(__cil_tmp120);
6400  }
6401#line 645
6402  return (ret);
6403}
6404}
6405#line 648 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
6406static void wacom_remove(struct hid_device *hdev ) 
6407{ struct wacom_data *wdata ;
6408  void *tmp ;
6409  void *tmp___0 ;
6410  unsigned long __cil_tmp5 ;
6411  unsigned long __cil_tmp6 ;
6412  struct device *__cil_tmp7 ;
6413  struct device_attribute  const  *__cil_tmp8 ;
6414  unsigned long __cil_tmp9 ;
6415  unsigned long __cil_tmp10 ;
6416  struct power_supply *__cil_tmp11 ;
6417  unsigned long __cil_tmp12 ;
6418  unsigned long __cil_tmp13 ;
6419  struct power_supply *__cil_tmp14 ;
6420  void const   *__cil_tmp15 ;
6421
6422  {
6423  {
6424#line 651
6425  tmp = hid_get_drvdata(hdev);
6426#line 651
6427  wdata = (struct wacom_data *)tmp;
6428#line 653
6429  __cil_tmp5 = (unsigned long )hdev;
6430#line 653
6431  __cil_tmp6 = __cil_tmp5 + 6328;
6432#line 653
6433  __cil_tmp7 = (struct device *)__cil_tmp6;
6434#line 653
6435  __cil_tmp8 = (struct device_attribute  const  *)(& dev_attr_speed);
6436#line 653
6437  device_remove_file(__cil_tmp7, __cil_tmp8);
6438#line 654
6439  hid_hw_stop(hdev);
6440#line 657
6441  __cil_tmp9 = (unsigned long )wdata;
6442#line 657
6443  __cil_tmp10 = __cil_tmp9 + 24;
6444#line 657
6445  __cil_tmp11 = (struct power_supply *)__cil_tmp10;
6446#line 657
6447  power_supply_unregister(__cil_tmp11);
6448#line 658
6449  __cil_tmp12 = (unsigned long )wdata;
6450#line 658
6451  __cil_tmp13 = __cil_tmp12 + 240;
6452#line 658
6453  __cil_tmp14 = (struct power_supply *)__cil_tmp13;
6454#line 658
6455  power_supply_unregister(__cil_tmp14);
6456#line 660
6457  tmp___0 = hid_get_drvdata(hdev);
6458#line 660
6459  __cil_tmp15 = (void const   *)tmp___0;
6460#line 660
6461  kfree(__cil_tmp15);
6462  }
6463#line 661
6464  return;
6465}
6466}
6467#line 663 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
6468static struct hid_device_id  const  wacom_devices[2]  = {      {(__u16 )5, (unsigned short)0, (__u32 )1386, (__u32 )129, 0UL}, 
6469        {(__u16 )5, (unsigned short)0, (__u32 )1386, (__u32 )189, 0UL}};
6470#line 669
6471extern struct hid_device_id  const  __mod_hid_device_table  __attribute__((__unused__,
6472__alias__("wacom_devices"))) ;
6473#line 671 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
6474static struct hid_driver wacom_driver  = 
6475#line 671
6476     {(char *)"wacom", wacom_devices, {(struct list_head *)0, (struct list_head *)0},
6477    {{{{{0U}}, 0U, 0U, (void *)0}}}, & wacom_probe, & wacom_remove, (struct hid_report_id  const  *)0,
6478    & wacom_raw_event, (struct hid_usage_id  const  *)0, (int (*)(struct hid_device *hdev ,
6479                                                                  struct hid_field *field ,
6480                                                                  struct hid_usage *usage ,
6481                                                                  __s32 value ))0,
6482    (__u8 *(*)(struct hid_device *hdev , __u8 *buf , unsigned int *size ))0, (int (*)(struct hid_device *hdev ,
6483                                                                                      struct hid_input *hidinput ,
6484                                                                                      struct hid_field *field ,
6485                                                                                      struct hid_usage *usage ,
6486                                                                                      unsigned long **bit ,
6487                                                                                      int *max ))0,
6488    & wacom_input_mapped, (void (*)(struct hid_device *hdev , struct hid_field *field ,
6489                                    struct hid_usage *usage ))0, (int (*)(struct hid_device *hdev ,
6490                                                                          pm_message_t message ))0,
6491    (int (*)(struct hid_device *hdev ))0, (int (*)(struct hid_device *hdev ))0, {(char const   *)0,
6492                                                                                 (struct bus_type *)0,
6493                                                                                 (struct module *)0,
6494                                                                                 (char const   *)0,
6495                                                                                 (_Bool)0,
6496                                                                                 (struct of_device_id  const  *)0,
6497                                                                                 (int (*)(struct device *dev ))0,
6498                                                                                 (int (*)(struct device *dev ))0,
6499                                                                                 (void (*)(struct device *dev ))0,
6500                                                                                 (int (*)(struct device *dev ,
6501                                                                                          pm_message_t state ))0,
6502                                                                                 (int (*)(struct device *dev ))0,
6503                                                                                 (struct attribute_group  const  **)0,
6504                                                                                 (struct dev_pm_ops  const  *)0,
6505                                                                                 (struct driver_private *)0}};
6506#line 680
6507static int wacom_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
6508#line 680 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
6509static int wacom_init(void) 
6510{ int ret ;
6511
6512  {
6513  {
6514#line 684
6515  ret = (int )__hid_register_driver(& wacom_driver, & __this_module, "hid_wacom");
6516  }
6517#line 685
6518  if (ret) {
6519    {
6520#line 686
6521    printk("<3>hid_wacom: can\'t register wacom driver\n");
6522    }
6523  } else {
6524
6525  }
6526#line 687
6527  return (ret);
6528}
6529}
6530#line 690
6531static void wacom_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
6532#line 690 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
6533static void wacom_exit(void) 
6534{ 
6535
6536  {
6537  {
6538#line 692
6539  hid_unregister_driver(& wacom_driver);
6540  }
6541#line 693
6542  return;
6543}
6544}
6545#line 695 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
6546int init_module(void) 
6547{ int tmp ;
6548
6549  {
6550  {
6551#line 695
6552  tmp = wacom_init();
6553  }
6554#line 695
6555  return (tmp);
6556}
6557}
6558#line 696 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
6559void cleanup_module(void) 
6560{ 
6561
6562  {
6563  {
6564#line 696
6565  wacom_exit();
6566  }
6567#line 696
6568  return;
6569}
6570}
6571#line 697 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
6572static char const   __mod_license697[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
6573__aligned__(1)))  = 
6574#line 697
6575  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
6576        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
6577        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
6578#line 716
6579void ldv_check_final_state(void) ;
6580#line 719
6581extern void ldv_check_return_value(int res ) ;
6582#line 722
6583extern void ldv_initialize(void) ;
6584#line 725
6585extern int __VERIFIER_nondet_int(void) ;
6586#line 728 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
6587int LDV_IN_INTERRUPT  ;
6588#line 756 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
6589static int res_wacom_probe_12  ;
6590#line 731 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/drivers/hid/hid-wacom.c.common.c"
6591void main(void) 
6592{ struct hid_device *var_group1 ;
6593  struct hid_device_id  const  *var_wacom_probe_12_p1 ;
6594  struct hid_report *var_group2 ;
6595  u8 *var_wacom_raw_event_10_p2 ;
6596  int var_wacom_raw_event_10_p3 ;
6597  struct hid_input *var_group3 ;
6598  struct hid_field *var_wacom_input_mapped_11_p2 ;
6599  struct hid_usage *var_wacom_input_mapped_11_p3 ;
6600  unsigned long **var_wacom_input_mapped_11_p4 ;
6601  int *var_wacom_input_mapped_11_p5 ;
6602  int tmp ;
6603  int ldv_s_wacom_driver_hid_driver ;
6604  int tmp___0 ;
6605  int tmp___1 ;
6606  int __cil_tmp15 ;
6607
6608  {
6609  {
6610#line 849
6611  LDV_IN_INTERRUPT = 1;
6612#line 858
6613  ldv_initialize();
6614#line 883
6615  tmp = wacom_init();
6616  }
6617#line 883
6618  if (tmp) {
6619#line 884
6620    goto ldv_final;
6621  } else {
6622
6623  }
6624#line 885
6625  ldv_s_wacom_driver_hid_driver = 0;
6626  {
6627#line 889
6628  while (1) {
6629    while_continue: /* CIL Label */ ;
6630    {
6631#line 889
6632    tmp___1 = __VERIFIER_nondet_int();
6633    }
6634#line 889
6635    if (tmp___1) {
6636
6637    } else {
6638      {
6639#line 889
6640      __cil_tmp15 = ldv_s_wacom_driver_hid_driver == 0;
6641#line 889
6642      if (! __cil_tmp15) {
6643
6644      } else {
6645#line 889
6646        goto while_break;
6647      }
6648      }
6649    }
6650    {
6651#line 893
6652    tmp___0 = __VERIFIER_nondet_int();
6653    }
6654#line 895
6655    if (tmp___0 == 0) {
6656#line 895
6657      goto case_0;
6658    } else
6659#line 931
6660    if (tmp___0 == 1) {
6661#line 931
6662      goto case_1;
6663    } else
6664#line 962
6665    if (tmp___0 == 2) {
6666#line 962
6667      goto case_2;
6668    } else
6669#line 999
6670    if (tmp___0 == 3) {
6671#line 999
6672      goto case_3;
6673    } else {
6674      {
6675#line 1036
6676      goto switch_default;
6677#line 893
6678      if (0) {
6679        case_0: /* CIL Label */ 
6680#line 898
6681        if (ldv_s_wacom_driver_hid_driver == 0) {
6682          {
6683#line 914
6684          res_wacom_probe_12 = wacom_probe(var_group1, var_wacom_probe_12_p1);
6685#line 915
6686          ldv_check_return_value(res_wacom_probe_12);
6687          }
6688#line 916
6689          if (res_wacom_probe_12) {
6690#line 917
6691            goto ldv_module_exit;
6692          } else {
6693
6694          }
6695#line 924
6696          ldv_s_wacom_driver_hid_driver = 0;
6697        } else {
6698
6699        }
6700#line 930
6701        goto switch_break;
6702        case_1: /* CIL Label */ 
6703        {