Showing error 221

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--hid--hid-tivo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 2893
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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