Showing error 808

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/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--hid--hid-twinhan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3310
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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