Showing error 249

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


Source:

   1/* Generated by CIL v. 1.3.7 */
   2/* print_CIL_Input is true */
   3
   4#line 19 "include/asm-generic/int-ll64.h"
   5typedef signed char __s8;
   6#line 20 "include/asm-generic/int-ll64.h"
   7typedef unsigned char __u8;
   8#line 22 "include/asm-generic/int-ll64.h"
   9typedef short __s16;
  10#line 23 "include/asm-generic/int-ll64.h"
  11typedef unsigned short __u16;
  12#line 25 "include/asm-generic/int-ll64.h"
  13typedef int __s32;
  14#line 26 "include/asm-generic/int-ll64.h"
  15typedef unsigned int __u32;
  16#line 30 "include/asm-generic/int-ll64.h"
  17typedef unsigned long long __u64;
  18#line 43 "include/asm-generic/int-ll64.h"
  19typedef unsigned char u8;
  20#line 45 "include/asm-generic/int-ll64.h"
  21typedef short s16;
  22#line 46 "include/asm-generic/int-ll64.h"
  23typedef unsigned short u16;
  24#line 48 "include/asm-generic/int-ll64.h"
  25typedef int s32;
  26#line 49 "include/asm-generic/int-ll64.h"
  27typedef unsigned int u32;
  28#line 51 "include/asm-generic/int-ll64.h"
  29typedef long long s64;
  30#line 52 "include/asm-generic/int-ll64.h"
  31typedef unsigned long long u64;
  32#line 14 "include/asm-generic/posix_types.h"
  33typedef long __kernel_long_t;
  34#line 15 "include/asm-generic/posix_types.h"
  35typedef unsigned long __kernel_ulong_t;
  36#line 52 "include/asm-generic/posix_types.h"
  37typedef unsigned int __kernel_uid32_t;
  38#line 53 "include/asm-generic/posix_types.h"
  39typedef unsigned int __kernel_gid32_t;
  40#line 75 "include/asm-generic/posix_types.h"
  41typedef __kernel_ulong_t __kernel_size_t;
  42#line 76 "include/asm-generic/posix_types.h"
  43typedef __kernel_long_t __kernel_ssize_t;
  44#line 91 "include/asm-generic/posix_types.h"
  45typedef long long __kernel_loff_t;
  46#line 92 "include/asm-generic/posix_types.h"
  47typedef __kernel_long_t __kernel_time_t;
  48#line 21 "include/linux/types.h"
  49typedef __u32 __kernel_dev_t;
  50#line 24 "include/linux/types.h"
  51typedef __kernel_dev_t dev_t;
  52#line 27 "include/linux/types.h"
  53typedef unsigned short umode_t;
  54#line 38 "include/linux/types.h"
  55typedef _Bool bool;
  56#line 40 "include/linux/types.h"
  57typedef __kernel_uid32_t uid_t;
  58#line 41 "include/linux/types.h"
  59typedef __kernel_gid32_t gid_t;
  60#line 54 "include/linux/types.h"
  61typedef __kernel_loff_t loff_t;
  62#line 63 "include/linux/types.h"
  63typedef __kernel_size_t size_t;
  64#line 68 "include/linux/types.h"
  65typedef __kernel_ssize_t ssize_t;
  66#line 78 "include/linux/types.h"
  67typedef __kernel_time_t time_t;
  68#line 142 "include/linux/types.h"
  69typedef unsigned long sector_t;
  70#line 143 "include/linux/types.h"
  71typedef unsigned long blkcnt_t;
  72#line 202 "include/linux/types.h"
  73typedef unsigned int gfp_t;
  74#line 203 "include/linux/types.h"
  75typedef unsigned int fmode_t;
  76#line 219 "include/linux/types.h"
  77struct __anonstruct_atomic_t_7 {
  78   int counter ;
  79};
  80#line 219 "include/linux/types.h"
  81typedef struct __anonstruct_atomic_t_7 atomic_t;
  82#line 224 "include/linux/types.h"
  83struct __anonstruct_atomic64_t_8 {
  84   long counter ;
  85};
  86#line 224 "include/linux/types.h"
  87typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  88#line 229 "include/linux/types.h"
  89struct list_head {
  90   struct list_head *next ;
  91   struct list_head *prev ;
  92};
  93#line 233
  94struct hlist_node;
  95#line 233 "include/linux/types.h"
  96struct hlist_head {
  97   struct hlist_node *first ;
  98};
  99#line 237 "include/linux/types.h"
 100struct hlist_node {
 101   struct hlist_node *next ;
 102   struct hlist_node **pprev ;
 103};
 104#line 253 "include/linux/types.h"
 105struct rcu_head {
 106   struct rcu_head *next ;
 107   void (*func)(struct rcu_head *head ) ;
 108};
 109#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 110struct module;
 111#line 56
 112struct module;
 113#line 146 "include/linux/init.h"
 114typedef void (*ctor_fn_t)(void);
 115#line 47 "include/linux/dynamic_debug.h"
 116struct device;
 117#line 47
 118struct device;
 119#line 135 "include/linux/kernel.h"
 120struct completion;
 121#line 135
 122struct completion;
 123#line 349
 124struct pid;
 125#line 349
 126struct pid;
 127#line 37 "include/linux/parport.h"
 128enum __anonenum_parport_device_class_10 {
 129    PARPORT_CLASS_LEGACY = 0,
 130    PARPORT_CLASS_PRINTER = 1,
 131    PARPORT_CLASS_MODEM = 2,
 132    PARPORT_CLASS_NET = 3,
 133    PARPORT_CLASS_HDC = 4,
 134    PARPORT_CLASS_PCMCIA = 5,
 135    PARPORT_CLASS_MEDIA = 6,
 136    PARPORT_CLASS_FDC = 7,
 137    PARPORT_CLASS_PORTS = 8,
 138    PARPORT_CLASS_SCANNER = 9,
 139    PARPORT_CLASS_DIGCAM = 10,
 140    PARPORT_CLASS_OTHER = 11,
 141    PARPORT_CLASS_UNSPEC = 12,
 142    PARPORT_CLASS_SCSIADAPTER = 13
 143} ;
 144#line 37 "include/linux/parport.h"
 145typedef enum __anonenum_parport_device_class_10 parport_device_class;
 146#line 12 "include/linux/thread_info.h"
 147struct timespec;
 148#line 12
 149struct timespec;
 150#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
 151struct page;
 152#line 18
 153struct page;
 154#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
 155struct task_struct;
 156#line 20
 157struct task_struct;
 158#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 159struct task_struct;
 160#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 161struct file;
 162#line 295
 163struct file;
 164#line 313
 165struct seq_file;
 166#line 313
 167struct seq_file;
 168#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 169struct page;
 170#line 52
 171struct task_struct;
 172#line 329
 173struct arch_spinlock;
 174#line 329
 175struct arch_spinlock;
 176#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 177struct task_struct;
 178#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 179struct task_struct;
 180#line 10 "include/asm-generic/bug.h"
 181struct bug_entry {
 182   int bug_addr_disp ;
 183   int file_disp ;
 184   unsigned short line ;
 185   unsigned short flags ;
 186};
 187#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 188struct static_key;
 189#line 234
 190struct static_key;
 191#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 192struct kmem_cache;
 193#line 23 "include/asm-generic/atomic-long.h"
 194typedef atomic64_t atomic_long_t;
 195#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 196typedef u16 __ticket_t;
 197#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 198typedef u32 __ticketpair_t;
 199#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 200struct __raw_tickets {
 201   __ticket_t head ;
 202   __ticket_t tail ;
 203};
 204#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 205union __anonunion____missing_field_name_37 {
 206   __ticketpair_t head_tail ;
 207   struct __raw_tickets tickets ;
 208};
 209#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 210struct arch_spinlock {
 211   union __anonunion____missing_field_name_37 __annonCompField17 ;
 212};
 213#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 214typedef struct arch_spinlock arch_spinlock_t;
 215#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 216struct __anonstruct____missing_field_name_39 {
 217   u32 read ;
 218   s32 write ;
 219};
 220#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 221union __anonunion_arch_rwlock_t_38 {
 222   s64 lock ;
 223   struct __anonstruct____missing_field_name_39 __annonCompField18 ;
 224};
 225#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 226typedef union __anonunion_arch_rwlock_t_38 arch_rwlock_t;
 227#line 12 "include/linux/lockdep.h"
 228struct task_struct;
 229#line 391 "include/linux/lockdep.h"
 230struct lock_class_key {
 231
 232};
 233#line 20 "include/linux/spinlock_types.h"
 234struct raw_spinlock {
 235   arch_spinlock_t raw_lock ;
 236   unsigned int magic ;
 237   unsigned int owner_cpu ;
 238   void *owner ;
 239};
 240#line 20 "include/linux/spinlock_types.h"
 241typedef struct raw_spinlock raw_spinlock_t;
 242#line 64 "include/linux/spinlock_types.h"
 243union __anonunion____missing_field_name_40 {
 244   struct raw_spinlock rlock ;
 245};
 246#line 64 "include/linux/spinlock_types.h"
 247struct spinlock {
 248   union __anonunion____missing_field_name_40 __annonCompField19 ;
 249};
 250#line 64 "include/linux/spinlock_types.h"
 251typedef struct spinlock spinlock_t;
 252#line 11 "include/linux/rwlock_types.h"
 253struct __anonstruct_rwlock_t_41 {
 254   arch_rwlock_t raw_lock ;
 255   unsigned int magic ;
 256   unsigned int owner_cpu ;
 257   void *owner ;
 258};
 259#line 11 "include/linux/rwlock_types.h"
 260typedef struct __anonstruct_rwlock_t_41 rwlock_t;
 261#line 119 "include/linux/seqlock.h"
 262struct seqcount {
 263   unsigned int sequence ;
 264};
 265#line 119 "include/linux/seqlock.h"
 266typedef struct seqcount seqcount_t;
 267#line 14 "include/linux/time.h"
 268struct timespec {
 269   __kernel_time_t tv_sec ;
 270   long tv_nsec ;
 271};
 272#line 49 "include/linux/wait.h"
 273struct __wait_queue_head {
 274   spinlock_t lock ;
 275   struct list_head task_list ;
 276};
 277#line 53 "include/linux/wait.h"
 278typedef struct __wait_queue_head wait_queue_head_t;
 279#line 55
 280struct task_struct;
 281#line 60 "include/linux/pageblock-flags.h"
 282struct page;
 283#line 48 "include/linux/mutex.h"
 284struct mutex {
 285   atomic_t count ;
 286   spinlock_t wait_lock ;
 287   struct list_head wait_list ;
 288   struct task_struct *owner ;
 289   char const   *name ;
 290   void *magic ;
 291};
 292#line 19 "include/linux/rwsem.h"
 293struct rw_semaphore;
 294#line 19
 295struct rw_semaphore;
 296#line 25 "include/linux/rwsem.h"
 297struct rw_semaphore {
 298   long count ;
 299   raw_spinlock_t wait_lock ;
 300   struct list_head wait_list ;
 301};
 302#line 25 "include/linux/completion.h"
 303struct completion {
 304   unsigned int done ;
 305   wait_queue_head_t wait ;
 306};
 307#line 9 "include/linux/memory_hotplug.h"
 308struct page;
 309#line 202 "include/linux/ioport.h"
 310struct device;
 311#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 312struct device;
 313#line 46 "include/linux/ktime.h"
 314union ktime {
 315   s64 tv64 ;
 316};
 317#line 59 "include/linux/ktime.h"
 318typedef union ktime ktime_t;
 319#line 10 "include/linux/timer.h"
 320struct tvec_base;
 321#line 10
 322struct tvec_base;
 323#line 12 "include/linux/timer.h"
 324struct timer_list {
 325   struct list_head entry ;
 326   unsigned long expires ;
 327   struct tvec_base *base ;
 328   void (*function)(unsigned long  ) ;
 329   unsigned long data ;
 330   int slack ;
 331   int start_pid ;
 332   void *start_site ;
 333   char start_comm[16] ;
 334};
 335#line 17 "include/linux/workqueue.h"
 336struct work_struct;
 337#line 17
 338struct work_struct;
 339#line 79 "include/linux/workqueue.h"
 340struct work_struct {
 341   atomic_long_t data ;
 342   struct list_head entry ;
 343   void (*func)(struct work_struct *work ) ;
 344};
 345#line 42 "include/linux/pm.h"
 346struct device;
 347#line 50 "include/linux/pm.h"
 348struct pm_message {
 349   int event ;
 350};
 351#line 50 "include/linux/pm.h"
 352typedef struct pm_message pm_message_t;
 353#line 264 "include/linux/pm.h"
 354struct dev_pm_ops {
 355   int (*prepare)(struct device *dev ) ;
 356   void (*complete)(struct device *dev ) ;
 357   int (*suspend)(struct device *dev ) ;
 358   int (*resume)(struct device *dev ) ;
 359   int (*freeze)(struct device *dev ) ;
 360   int (*thaw)(struct device *dev ) ;
 361   int (*poweroff)(struct device *dev ) ;
 362   int (*restore)(struct device *dev ) ;
 363   int (*suspend_late)(struct device *dev ) ;
 364   int (*resume_early)(struct device *dev ) ;
 365   int (*freeze_late)(struct device *dev ) ;
 366   int (*thaw_early)(struct device *dev ) ;
 367   int (*poweroff_late)(struct device *dev ) ;
 368   int (*restore_early)(struct device *dev ) ;
 369   int (*suspend_noirq)(struct device *dev ) ;
 370   int (*resume_noirq)(struct device *dev ) ;
 371   int (*freeze_noirq)(struct device *dev ) ;
 372   int (*thaw_noirq)(struct device *dev ) ;
 373   int (*poweroff_noirq)(struct device *dev ) ;
 374   int (*restore_noirq)(struct device *dev ) ;
 375   int (*runtime_suspend)(struct device *dev ) ;
 376   int (*runtime_resume)(struct device *dev ) ;
 377   int (*runtime_idle)(struct device *dev ) ;
 378};
 379#line 458
 380enum rpm_status {
 381    RPM_ACTIVE = 0,
 382    RPM_RESUMING = 1,
 383    RPM_SUSPENDED = 2,
 384    RPM_SUSPENDING = 3
 385} ;
 386#line 480
 387enum rpm_request {
 388    RPM_REQ_NONE = 0,
 389    RPM_REQ_IDLE = 1,
 390    RPM_REQ_SUSPEND = 2,
 391    RPM_REQ_AUTOSUSPEND = 3,
 392    RPM_REQ_RESUME = 4
 393} ;
 394#line 488
 395struct wakeup_source;
 396#line 488
 397struct wakeup_source;
 398#line 495 "include/linux/pm.h"
 399struct pm_subsys_data {
 400   spinlock_t lock ;
 401   unsigned int refcount ;
 402};
 403#line 506
 404struct dev_pm_qos_request;
 405#line 506
 406struct pm_qos_constraints;
 407#line 506 "include/linux/pm.h"
 408struct dev_pm_info {
 409   pm_message_t power_state ;
 410   unsigned int can_wakeup : 1 ;
 411   unsigned int async_suspend : 1 ;
 412   bool is_prepared : 1 ;
 413   bool is_suspended : 1 ;
 414   bool ignore_children : 1 ;
 415   spinlock_t lock ;
 416   struct list_head entry ;
 417   struct completion completion ;
 418   struct wakeup_source *wakeup ;
 419   bool wakeup_path : 1 ;
 420   struct timer_list suspend_timer ;
 421   unsigned long timer_expires ;
 422   struct work_struct work ;
 423   wait_queue_head_t wait_queue ;
 424   atomic_t usage_count ;
 425   atomic_t child_count ;
 426   unsigned int disable_depth : 3 ;
 427   unsigned int idle_notification : 1 ;
 428   unsigned int request_pending : 1 ;
 429   unsigned int deferred_resume : 1 ;
 430   unsigned int run_wake : 1 ;
 431   unsigned int runtime_auto : 1 ;
 432   unsigned int no_callbacks : 1 ;
 433   unsigned int irq_safe : 1 ;
 434   unsigned int use_autosuspend : 1 ;
 435   unsigned int timer_autosuspends : 1 ;
 436   enum rpm_request request ;
 437   enum rpm_status runtime_status ;
 438   int runtime_error ;
 439   int autosuspend_delay ;
 440   unsigned long last_busy ;
 441   unsigned long active_jiffies ;
 442   unsigned long suspended_jiffies ;
 443   unsigned long accounting_timestamp ;
 444   ktime_t suspend_time ;
 445   s64 max_time_suspended_ns ;
 446   struct dev_pm_qos_request *pq_req ;
 447   struct pm_subsys_data *subsys_data ;
 448   struct pm_qos_constraints *constraints ;
 449};
 450#line 564 "include/linux/pm.h"
 451struct dev_pm_domain {
 452   struct dev_pm_ops ops ;
 453};
 454#line 8 "include/linux/vmalloc.h"
 455struct vm_area_struct;
 456#line 8
 457struct vm_area_struct;
 458#line 994 "include/linux/mmzone.h"
 459struct page;
 460#line 10 "include/linux/gfp.h"
 461struct vm_area_struct;
 462#line 20 "include/linux/kobject_ns.h"
 463struct sock;
 464#line 20
 465struct sock;
 466#line 21
 467struct kobject;
 468#line 21
 469struct kobject;
 470#line 27
 471enum kobj_ns_type {
 472    KOBJ_NS_TYPE_NONE = 0,
 473    KOBJ_NS_TYPE_NET = 1,
 474    KOBJ_NS_TYPES = 2
 475} ;
 476#line 40 "include/linux/kobject_ns.h"
 477struct kobj_ns_type_operations {
 478   enum kobj_ns_type type ;
 479   void *(*grab_current_ns)(void) ;
 480   void const   *(*netlink_ns)(struct sock *sk ) ;
 481   void const   *(*initial_ns)(void) ;
 482   void (*drop_ns)(void * ) ;
 483};
 484#line 22 "include/linux/sysfs.h"
 485struct kobject;
 486#line 23
 487struct module;
 488#line 24
 489enum kobj_ns_type;
 490#line 26 "include/linux/sysfs.h"
 491struct attribute {
 492   char const   *name ;
 493   umode_t mode ;
 494};
 495#line 56 "include/linux/sysfs.h"
 496struct attribute_group {
 497   char const   *name ;
 498   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 499   struct attribute **attrs ;
 500};
 501#line 85
 502struct file;
 503#line 86
 504struct vm_area_struct;
 505#line 88 "include/linux/sysfs.h"
 506struct bin_attribute {
 507   struct attribute attr ;
 508   size_t size ;
 509   void *private ;
 510   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 511                   loff_t  , size_t  ) ;
 512   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 513                    loff_t  , size_t  ) ;
 514   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 515};
 516#line 112 "include/linux/sysfs.h"
 517struct sysfs_ops {
 518   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 519   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 520   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 521};
 522#line 118
 523struct sysfs_dirent;
 524#line 118
 525struct sysfs_dirent;
 526#line 22 "include/linux/kref.h"
 527struct kref {
 528   atomic_t refcount ;
 529};
 530#line 60 "include/linux/kobject.h"
 531struct kset;
 532#line 60
 533struct kobj_type;
 534#line 60 "include/linux/kobject.h"
 535struct kobject {
 536   char const   *name ;
 537   struct list_head entry ;
 538   struct kobject *parent ;
 539   struct kset *kset ;
 540   struct kobj_type *ktype ;
 541   struct sysfs_dirent *sd ;
 542   struct kref kref ;
 543   unsigned int state_initialized : 1 ;
 544   unsigned int state_in_sysfs : 1 ;
 545   unsigned int state_add_uevent_sent : 1 ;
 546   unsigned int state_remove_uevent_sent : 1 ;
 547   unsigned int uevent_suppress : 1 ;
 548};
 549#line 108 "include/linux/kobject.h"
 550struct kobj_type {
 551   void (*release)(struct kobject *kobj ) ;
 552   struct sysfs_ops  const  *sysfs_ops ;
 553   struct attribute **default_attrs ;
 554   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 555   void const   *(*namespace)(struct kobject *kobj ) ;
 556};
 557#line 116 "include/linux/kobject.h"
 558struct kobj_uevent_env {
 559   char *envp[32] ;
 560   int envp_idx ;
 561   char buf[2048] ;
 562   int buflen ;
 563};
 564#line 123 "include/linux/kobject.h"
 565struct kset_uevent_ops {
 566   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 567   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 568   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 569};
 570#line 140
 571struct sock;
 572#line 159 "include/linux/kobject.h"
 573struct kset {
 574   struct list_head list ;
 575   spinlock_t list_lock ;
 576   struct kobject kobj ;
 577   struct kset_uevent_ops  const  *uevent_ops ;
 578};
 579#line 46 "include/linux/slub_def.h"
 580struct kmem_cache_cpu {
 581   void **freelist ;
 582   unsigned long tid ;
 583   struct page *page ;
 584   struct page *partial ;
 585   int node ;
 586   unsigned int stat[26] ;
 587};
 588#line 57 "include/linux/slub_def.h"
 589struct kmem_cache_node {
 590   spinlock_t list_lock ;
 591   unsigned long nr_partial ;
 592   struct list_head partial ;
 593   atomic_long_t nr_slabs ;
 594   atomic_long_t total_objects ;
 595   struct list_head full ;
 596};
 597#line 73 "include/linux/slub_def.h"
 598struct kmem_cache_order_objects {
 599   unsigned long x ;
 600};
 601#line 80 "include/linux/slub_def.h"
 602struct kmem_cache {
 603   struct kmem_cache_cpu *cpu_slab ;
 604   unsigned long flags ;
 605   unsigned long min_partial ;
 606   int size ;
 607   int objsize ;
 608   int offset ;
 609   int cpu_partial ;
 610   struct kmem_cache_order_objects oo ;
 611   struct kmem_cache_order_objects max ;
 612   struct kmem_cache_order_objects min ;
 613   gfp_t allocflags ;
 614   int refcount ;
 615   void (*ctor)(void * ) ;
 616   int inuse ;
 617   int align ;
 618   int reserved ;
 619   char const   *name ;
 620   struct list_head list ;
 621   struct kobject kobj ;
 622   int remote_node_defrag_ratio ;
 623   struct kmem_cache_node *node[1 << 10] ;
 624};
 625#line 15 "include/linux/blk_types.h"
 626struct page;
 627#line 16
 628struct block_device;
 629#line 16
 630struct block_device;
 631#line 33 "include/linux/list_bl.h"
 632struct hlist_bl_node;
 633#line 33 "include/linux/list_bl.h"
 634struct hlist_bl_head {
 635   struct hlist_bl_node *first ;
 636};
 637#line 37 "include/linux/list_bl.h"
 638struct hlist_bl_node {
 639   struct hlist_bl_node *next ;
 640   struct hlist_bl_node **pprev ;
 641};
 642#line 13 "include/linux/dcache.h"
 643struct nameidata;
 644#line 13
 645struct nameidata;
 646#line 14
 647struct path;
 648#line 14
 649struct path;
 650#line 15
 651struct vfsmount;
 652#line 15
 653struct vfsmount;
 654#line 35 "include/linux/dcache.h"
 655struct qstr {
 656   unsigned int hash ;
 657   unsigned int len ;
 658   unsigned char const   *name ;
 659};
 660#line 88
 661struct inode;
 662#line 88
 663struct dentry_operations;
 664#line 88
 665struct super_block;
 666#line 88 "include/linux/dcache.h"
 667union __anonunion_d_u_140 {
 668   struct list_head d_child ;
 669   struct rcu_head d_rcu ;
 670};
 671#line 88 "include/linux/dcache.h"
 672struct dentry {
 673   unsigned int d_flags ;
 674   seqcount_t d_seq ;
 675   struct hlist_bl_node d_hash ;
 676   struct dentry *d_parent ;
 677   struct qstr d_name ;
 678   struct inode *d_inode ;
 679   unsigned char d_iname[32] ;
 680   unsigned int d_count ;
 681   spinlock_t d_lock ;
 682   struct dentry_operations  const  *d_op ;
 683   struct super_block *d_sb ;
 684   unsigned long d_time ;
 685   void *d_fsdata ;
 686   struct list_head d_lru ;
 687   union __anonunion_d_u_140 d_u ;
 688   struct list_head d_subdirs ;
 689   struct list_head d_alias ;
 690};
 691#line 131 "include/linux/dcache.h"
 692struct dentry_operations {
 693   int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
 694   int (*d_hash)(struct dentry  const  * , struct inode  const  * , struct qstr * ) ;
 695   int (*d_compare)(struct dentry  const  * , struct inode  const  * , struct dentry  const  * ,
 696                    struct inode  const  * , unsigned int  , char const   * , struct qstr  const  * ) ;
 697   int (*d_delete)(struct dentry  const  * ) ;
 698   void (*d_release)(struct dentry * ) ;
 699   void (*d_prune)(struct dentry * ) ;
 700   void (*d_iput)(struct dentry * , struct inode * ) ;
 701   char *(*d_dname)(struct dentry * , char * , int  ) ;
 702   struct vfsmount *(*d_automount)(struct path * ) ;
 703   int (*d_manage)(struct dentry * , bool  ) ;
 704} __attribute__((__aligned__((1) <<  (6) ))) ;
 705#line 4 "include/linux/path.h"
 706struct dentry;
 707#line 5
 708struct vfsmount;
 709#line 7 "include/linux/path.h"
 710struct path {
 711   struct vfsmount *mnt ;
 712   struct dentry *dentry ;
 713};
 714#line 62 "include/linux/stat.h"
 715struct kstat {
 716   u64 ino ;
 717   dev_t dev ;
 718   umode_t mode ;
 719   unsigned int nlink ;
 720   uid_t uid ;
 721   gid_t gid ;
 722   dev_t rdev ;
 723   loff_t size ;
 724   struct timespec atime ;
 725   struct timespec mtime ;
 726   struct timespec ctime ;
 727   unsigned long blksize ;
 728   unsigned long long blocks ;
 729};
 730#line 64 "include/linux/radix-tree.h"
 731struct radix_tree_node;
 732#line 64 "include/linux/radix-tree.h"
 733struct radix_tree_root {
 734   unsigned int height ;
 735   gfp_t gfp_mask ;
 736   struct radix_tree_node *rnode ;
 737};
 738#line 14 "include/linux/prio_tree.h"
 739struct prio_tree_node;
 740#line 20 "include/linux/prio_tree.h"
 741struct prio_tree_node {
 742   struct prio_tree_node *left ;
 743   struct prio_tree_node *right ;
 744   struct prio_tree_node *parent ;
 745   unsigned long start ;
 746   unsigned long last ;
 747};
 748#line 28 "include/linux/prio_tree.h"
 749struct prio_tree_root {
 750   struct prio_tree_node *prio_tree_node ;
 751   unsigned short index_bits ;
 752   unsigned short raw ;
 753};
 754#line 6 "include/linux/pid.h"
 755enum pid_type {
 756    PIDTYPE_PID = 0,
 757    PIDTYPE_PGID = 1,
 758    PIDTYPE_SID = 2,
 759    PIDTYPE_MAX = 3
 760} ;
 761#line 50
 762struct pid_namespace;
 763#line 50 "include/linux/pid.h"
 764struct upid {
 765   int nr ;
 766   struct pid_namespace *ns ;
 767   struct hlist_node pid_chain ;
 768};
 769#line 57 "include/linux/pid.h"
 770struct pid {
 771   atomic_t count ;
 772   unsigned int level ;
 773   struct hlist_head tasks[3] ;
 774   struct rcu_head rcu ;
 775   struct upid numbers[1] ;
 776};
 777#line 100
 778struct pid_namespace;
 779#line 18 "include/linux/capability.h"
 780struct task_struct;
 781#line 377
 782struct dentry;
 783#line 16 "include/linux/semaphore.h"
 784struct semaphore {
 785   raw_spinlock_t lock ;
 786   unsigned int count ;
 787   struct list_head wait_list ;
 788};
 789#line 16 "include/linux/fiemap.h"
 790struct fiemap_extent {
 791   __u64 fe_logical ;
 792   __u64 fe_physical ;
 793   __u64 fe_length ;
 794   __u64 fe_reserved64[2] ;
 795   __u32 fe_flags ;
 796   __u32 fe_reserved[3] ;
 797};
 798#line 8 "include/linux/shrinker.h"
 799struct shrink_control {
 800   gfp_t gfp_mask ;
 801   unsigned long nr_to_scan ;
 802};
 803#line 31 "include/linux/shrinker.h"
 804struct shrinker {
 805   int (*shrink)(struct shrinker * , struct shrink_control *sc ) ;
 806   int seeks ;
 807   long batch ;
 808   struct list_head list ;
 809   atomic_long_t nr_in_batch ;
 810};
 811#line 10 "include/linux/migrate_mode.h"
 812enum migrate_mode {
 813    MIGRATE_ASYNC = 0,
 814    MIGRATE_SYNC_LIGHT = 1,
 815    MIGRATE_SYNC = 2
 816} ;
 817#line 408 "include/linux/fs.h"
 818struct export_operations;
 819#line 408
 820struct export_operations;
 821#line 410
 822struct iovec;
 823#line 410
 824struct iovec;
 825#line 411
 826struct nameidata;
 827#line 412
 828struct kiocb;
 829#line 412
 830struct kiocb;
 831#line 413
 832struct kobject;
 833#line 414
 834struct pipe_inode_info;
 835#line 414
 836struct pipe_inode_info;
 837#line 415
 838struct poll_table_struct;
 839#line 415
 840struct poll_table_struct;
 841#line 416
 842struct kstatfs;
 843#line 416
 844struct kstatfs;
 845#line 417
 846struct vm_area_struct;
 847#line 418
 848struct vfsmount;
 849#line 419
 850struct cred;
 851#line 419
 852struct cred;
 853#line 469 "include/linux/fs.h"
 854struct iattr {
 855   unsigned int ia_valid ;
 856   umode_t ia_mode ;
 857   uid_t ia_uid ;
 858   gid_t ia_gid ;
 859   loff_t ia_size ;
 860   struct timespec ia_atime ;
 861   struct timespec ia_mtime ;
 862   struct timespec ia_ctime ;
 863   struct file *ia_file ;
 864};
 865#line 129 "include/linux/quota.h"
 866struct if_dqinfo {
 867   __u64 dqi_bgrace ;
 868   __u64 dqi_igrace ;
 869   __u32 dqi_flags ;
 870   __u32 dqi_valid ;
 871};
 872#line 50 "include/linux/dqblk_xfs.h"
 873struct fs_disk_quota {
 874   __s8 d_version ;
 875   __s8 d_flags ;
 876   __u16 d_fieldmask ;
 877   __u32 d_id ;
 878   __u64 d_blk_hardlimit ;
 879   __u64 d_blk_softlimit ;
 880   __u64 d_ino_hardlimit ;
 881   __u64 d_ino_softlimit ;
 882   __u64 d_bcount ;
 883   __u64 d_icount ;
 884   __s32 d_itimer ;
 885   __s32 d_btimer ;
 886   __u16 d_iwarns ;
 887   __u16 d_bwarns ;
 888   __s32 d_padding2 ;
 889   __u64 d_rtb_hardlimit ;
 890   __u64 d_rtb_softlimit ;
 891   __u64 d_rtbcount ;
 892   __s32 d_rtbtimer ;
 893   __u16 d_rtbwarns ;
 894   __s16 d_padding3 ;
 895   char d_padding4[8] ;
 896};
 897#line 146 "include/linux/dqblk_xfs.h"
 898struct fs_qfilestat {
 899   __u64 qfs_ino ;
 900   __u64 qfs_nblks ;
 901   __u32 qfs_nextents ;
 902};
 903#line 146 "include/linux/dqblk_xfs.h"
 904typedef struct fs_qfilestat fs_qfilestat_t;
 905#line 152 "include/linux/dqblk_xfs.h"
 906struct fs_quota_stat {
 907   __s8 qs_version ;
 908   __u16 qs_flags ;
 909   __s8 qs_pad ;
 910   fs_qfilestat_t qs_uquota ;
 911   fs_qfilestat_t qs_gquota ;
 912   __u32 qs_incoredqs ;
 913   __s32 qs_btimelimit ;
 914   __s32 qs_itimelimit ;
 915   __s32 qs_rtbtimelimit ;
 916   __u16 qs_bwarnlimit ;
 917   __u16 qs_iwarnlimit ;
 918};
 919#line 17 "include/linux/dqblk_qtree.h"
 920struct dquot;
 921#line 17
 922struct dquot;
 923#line 185 "include/linux/quota.h"
 924typedef __kernel_uid32_t qid_t;
 925#line 186 "include/linux/quota.h"
 926typedef long long qsize_t;
 927#line 200 "include/linux/quota.h"
 928struct mem_dqblk {
 929   qsize_t dqb_bhardlimit ;
 930   qsize_t dqb_bsoftlimit ;
 931   qsize_t dqb_curspace ;
 932   qsize_t dqb_rsvspace ;
 933   qsize_t dqb_ihardlimit ;
 934   qsize_t dqb_isoftlimit ;
 935   qsize_t dqb_curinodes ;
 936   time_t dqb_btime ;
 937   time_t dqb_itime ;
 938};
 939#line 215
 940struct quota_format_type;
 941#line 215
 942struct quota_format_type;
 943#line 217 "include/linux/quota.h"
 944struct mem_dqinfo {
 945   struct quota_format_type *dqi_format ;
 946   int dqi_fmt_id ;
 947   struct list_head dqi_dirty_list ;
 948   unsigned long dqi_flags ;
 949   unsigned int dqi_bgrace ;
 950   unsigned int dqi_igrace ;
 951   qsize_t dqi_maxblimit ;
 952   qsize_t dqi_maxilimit ;
 953   void *dqi_priv ;
 954};
 955#line 230
 956struct super_block;
 957#line 288 "include/linux/quota.h"
 958struct dquot {
 959   struct hlist_node dq_hash ;
 960   struct list_head dq_inuse ;
 961   struct list_head dq_free ;
 962   struct list_head dq_dirty ;
 963   struct mutex dq_lock ;
 964   atomic_t dq_count ;
 965   wait_queue_head_t dq_wait_unused ;
 966   struct super_block *dq_sb ;
 967   unsigned int dq_id ;
 968   loff_t dq_off ;
 969   unsigned long dq_flags ;
 970   short dq_type ;
 971   struct mem_dqblk dq_dqb ;
 972};
 973#line 305 "include/linux/quota.h"
 974struct quota_format_ops {
 975   int (*check_quota_file)(struct super_block *sb , int type ) ;
 976   int (*read_file_info)(struct super_block *sb , int type ) ;
 977   int (*write_file_info)(struct super_block *sb , int type ) ;
 978   int (*free_file_info)(struct super_block *sb , int type ) ;
 979   int (*read_dqblk)(struct dquot *dquot ) ;
 980   int (*commit_dqblk)(struct dquot *dquot ) ;
 981   int (*release_dqblk)(struct dquot *dquot ) ;
 982};
 983#line 316 "include/linux/quota.h"
 984struct dquot_operations {
 985   int (*write_dquot)(struct dquot * ) ;
 986   struct dquot *(*alloc_dquot)(struct super_block * , int  ) ;
 987   void (*destroy_dquot)(struct dquot * ) ;
 988   int (*acquire_dquot)(struct dquot * ) ;
 989   int (*release_dquot)(struct dquot * ) ;
 990   int (*mark_dirty)(struct dquot * ) ;
 991   int (*write_info)(struct super_block * , int  ) ;
 992   qsize_t *(*get_reserved_space)(struct inode * ) ;
 993};
 994#line 329
 995struct path;
 996#line 332 "include/linux/quota.h"
 997struct quotactl_ops {
 998   int (*quota_on)(struct super_block * , int  , int  , struct path * ) ;
 999   int (*quota_on_meta)(struct super_block * , int  , int  ) ;
1000   int (*quota_off)(struct super_block * , int  ) ;
1001   int (*quota_sync)(struct super_block * , int  , int  ) ;
1002   int (*get_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1003   int (*set_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1004   int (*get_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1005   int (*set_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1006   int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1007   int (*set_xstate)(struct super_block * , unsigned int  , int  ) ;
1008};
1009#line 345 "include/linux/quota.h"
1010struct quota_format_type {
1011   int qf_fmt_id ;
1012   struct quota_format_ops  const  *qf_ops ;
1013   struct module *qf_owner ;
1014   struct quota_format_type *qf_next ;
1015};
1016#line 399 "include/linux/quota.h"
1017struct quota_info {
1018   unsigned int flags ;
1019   struct mutex dqio_mutex ;
1020   struct mutex dqonoff_mutex ;
1021   struct rw_semaphore dqptr_sem ;
1022   struct inode *files[2] ;
1023   struct mem_dqinfo info[2] ;
1024   struct quota_format_ops  const  *ops[2] ;
1025};
1026#line 532 "include/linux/fs.h"
1027struct page;
1028#line 533
1029struct address_space;
1030#line 533
1031struct address_space;
1032#line 534
1033struct writeback_control;
1034#line 534
1035struct writeback_control;
1036#line 577 "include/linux/fs.h"
1037union __anonunion_arg_148 {
1038   char *buf ;
1039   void *data ;
1040};
1041#line 577 "include/linux/fs.h"
1042struct __anonstruct_read_descriptor_t_147 {
1043   size_t written ;
1044   size_t count ;
1045   union __anonunion_arg_148 arg ;
1046   int error ;
1047};
1048#line 577 "include/linux/fs.h"
1049typedef struct __anonstruct_read_descriptor_t_147 read_descriptor_t;
1050#line 590 "include/linux/fs.h"
1051struct address_space_operations {
1052   int (*writepage)(struct page *page , struct writeback_control *wbc ) ;
1053   int (*readpage)(struct file * , struct page * ) ;
1054   int (*writepages)(struct address_space * , struct writeback_control * ) ;
1055   int (*set_page_dirty)(struct page *page ) ;
1056   int (*readpages)(struct file *filp , struct address_space *mapping , struct list_head *pages ,
1057                    unsigned int nr_pages ) ;
1058   int (*write_begin)(struct file * , struct address_space *mapping , loff_t pos ,
1059                      unsigned int len , unsigned int flags , struct page **pagep ,
1060                      void **fsdata ) ;
1061   int (*write_end)(struct file * , struct address_space *mapping , loff_t pos , unsigned int len ,
1062                    unsigned int copied , struct page *page , void *fsdata ) ;
1063   sector_t (*bmap)(struct address_space * , sector_t  ) ;
1064   void (*invalidatepage)(struct page * , unsigned long  ) ;
1065   int (*releasepage)(struct page * , gfp_t  ) ;
1066   void (*freepage)(struct page * ) ;
1067   ssize_t (*direct_IO)(int  , struct kiocb * , struct iovec  const  *iov , loff_t offset ,
1068                        unsigned long nr_segs ) ;
1069   int (*get_xip_mem)(struct address_space * , unsigned long  , int  , void ** , unsigned long * ) ;
1070   int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode  ) ;
1071   int (*launder_page)(struct page * ) ;
1072   int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long  ) ;
1073   int (*error_remove_page)(struct address_space * , struct page * ) ;
1074};
1075#line 645
1076struct backing_dev_info;
1077#line 645
1078struct backing_dev_info;
1079#line 646 "include/linux/fs.h"
1080struct address_space {
1081   struct inode *host ;
1082   struct radix_tree_root page_tree ;
1083   spinlock_t tree_lock ;
1084   unsigned int i_mmap_writable ;
1085   struct prio_tree_root i_mmap ;
1086   struct list_head i_mmap_nonlinear ;
1087   struct mutex i_mmap_mutex ;
1088   unsigned long nrpages ;
1089   unsigned long writeback_index ;
1090   struct address_space_operations  const  *a_ops ;
1091   unsigned long flags ;
1092   struct backing_dev_info *backing_dev_info ;
1093   spinlock_t private_lock ;
1094   struct list_head private_list ;
1095   struct address_space *assoc_mapping ;
1096} __attribute__((__aligned__(sizeof(long )))) ;
1097#line 669
1098struct request_queue;
1099#line 669
1100struct request_queue;
1101#line 671
1102struct hd_struct;
1103#line 671
1104struct gendisk;
1105#line 671 "include/linux/fs.h"
1106struct block_device {
1107   dev_t bd_dev ;
1108   int bd_openers ;
1109   struct inode *bd_inode ;
1110   struct super_block *bd_super ;
1111   struct mutex bd_mutex ;
1112   struct list_head bd_inodes ;
1113   void *bd_claiming ;
1114   void *bd_holder ;
1115   int bd_holders ;
1116   bool bd_write_holder ;
1117   struct list_head bd_holder_disks ;
1118   struct block_device *bd_contains ;
1119   unsigned int bd_block_size ;
1120   struct hd_struct *bd_part ;
1121   unsigned int bd_part_count ;
1122   int bd_invalidated ;
1123   struct gendisk *bd_disk ;
1124   struct request_queue *bd_queue ;
1125   struct list_head bd_list ;
1126   unsigned long bd_private ;
1127   int bd_fsfreeze_count ;
1128   struct mutex bd_fsfreeze_mutex ;
1129};
1130#line 749
1131struct posix_acl;
1132#line 749
1133struct posix_acl;
1134#line 761
1135struct inode_operations;
1136#line 761 "include/linux/fs.h"
1137union __anonunion____missing_field_name_149 {
1138   unsigned int const   i_nlink ;
1139   unsigned int __i_nlink ;
1140};
1141#line 761 "include/linux/fs.h"
1142union __anonunion____missing_field_name_150 {
1143   struct list_head i_dentry ;
1144   struct rcu_head i_rcu ;
1145};
1146#line 761
1147struct file_operations;
1148#line 761
1149struct file_lock;
1150#line 761
1151struct cdev;
1152#line 761 "include/linux/fs.h"
1153union __anonunion____missing_field_name_151 {
1154   struct pipe_inode_info *i_pipe ;
1155   struct block_device *i_bdev ;
1156   struct cdev *i_cdev ;
1157};
1158#line 761 "include/linux/fs.h"
1159struct inode {
1160   umode_t i_mode ;
1161   unsigned short i_opflags ;
1162   uid_t i_uid ;
1163   gid_t i_gid ;
1164   unsigned int i_flags ;
1165   struct posix_acl *i_acl ;
1166   struct posix_acl *i_default_acl ;
1167   struct inode_operations  const  *i_op ;
1168   struct super_block *i_sb ;
1169   struct address_space *i_mapping ;
1170   void *i_security ;
1171   unsigned long i_ino ;
1172   union __anonunion____missing_field_name_149 __annonCompField30 ;
1173   dev_t i_rdev ;
1174   struct timespec i_atime ;
1175   struct timespec i_mtime ;
1176   struct timespec i_ctime ;
1177   spinlock_t i_lock ;
1178   unsigned short i_bytes ;
1179   blkcnt_t i_blocks ;
1180   loff_t i_size ;
1181   unsigned long i_state ;
1182   struct mutex i_mutex ;
1183   unsigned long dirtied_when ;
1184   struct hlist_node i_hash ;
1185   struct list_head i_wb_list ;
1186   struct list_head i_lru ;
1187   struct list_head i_sb_list ;
1188   union __anonunion____missing_field_name_150 __annonCompField31 ;
1189   atomic_t i_count ;
1190   unsigned int i_blkbits ;
1191   u64 i_version ;
1192   atomic_t i_dio_count ;
1193   atomic_t i_writecount ;
1194   struct file_operations  const  *i_fop ;
1195   struct file_lock *i_flock ;
1196   struct address_space i_data ;
1197   struct dquot *i_dquot[2] ;
1198   struct list_head i_devices ;
1199   union __anonunion____missing_field_name_151 __annonCompField32 ;
1200   __u32 i_generation ;
1201   __u32 i_fsnotify_mask ;
1202   struct hlist_head i_fsnotify_marks ;
1203   atomic_t i_readcount ;
1204   void *i_private ;
1205};
1206#line 942 "include/linux/fs.h"
1207struct fown_struct {
1208   rwlock_t lock ;
1209   struct pid *pid ;
1210   enum pid_type pid_type ;
1211   uid_t uid ;
1212   uid_t euid ;
1213   int signum ;
1214};
1215#line 953 "include/linux/fs.h"
1216struct file_ra_state {
1217   unsigned long start ;
1218   unsigned int size ;
1219   unsigned int async_size ;
1220   unsigned int ra_pages ;
1221   unsigned int mmap_miss ;
1222   loff_t prev_pos ;
1223};
1224#line 976 "include/linux/fs.h"
1225union __anonunion_f_u_152 {
1226   struct list_head fu_list ;
1227   struct rcu_head fu_rcuhead ;
1228};
1229#line 976 "include/linux/fs.h"
1230struct file {
1231   union __anonunion_f_u_152 f_u ;
1232   struct path f_path ;
1233   struct file_operations  const  *f_op ;
1234   spinlock_t f_lock ;
1235   int f_sb_list_cpu ;
1236   atomic_long_t f_count ;
1237   unsigned int f_flags ;
1238   fmode_t f_mode ;
1239   loff_t f_pos ;
1240   struct fown_struct f_owner ;
1241   struct cred  const  *f_cred ;
1242   struct file_ra_state f_ra ;
1243   u64 f_version ;
1244   void *f_security ;
1245   void *private_data ;
1246   struct list_head f_ep_links ;
1247   struct list_head f_tfile_llink ;
1248   struct address_space *f_mapping ;
1249   unsigned long f_mnt_write_state ;
1250};
1251#line 1111
1252struct files_struct;
1253#line 1111 "include/linux/fs.h"
1254typedef struct files_struct *fl_owner_t;
1255#line 1113 "include/linux/fs.h"
1256struct file_lock_operations {
1257   void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1258   void (*fl_release_private)(struct file_lock * ) ;
1259};
1260#line 1118 "include/linux/fs.h"
1261struct lock_manager_operations {
1262   int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1263   void (*lm_notify)(struct file_lock * ) ;
1264   int (*lm_grant)(struct file_lock * , struct file_lock * , int  ) ;
1265   void (*lm_release_private)(struct file_lock * ) ;
1266   void (*lm_break)(struct file_lock * ) ;
1267   int (*lm_change)(struct file_lock ** , int  ) ;
1268};
1269#line 4 "include/linux/nfs_fs_i.h"
1270struct nlm_lockowner;
1271#line 4
1272struct nlm_lockowner;
1273#line 9 "include/linux/nfs_fs_i.h"
1274struct nfs_lock_info {
1275   u32 state ;
1276   struct nlm_lockowner *owner ;
1277   struct list_head list ;
1278};
1279#line 15
1280struct nfs4_lock_state;
1281#line 15
1282struct nfs4_lock_state;
1283#line 16 "include/linux/nfs_fs_i.h"
1284struct nfs4_lock_info {
1285   struct nfs4_lock_state *owner ;
1286};
1287#line 1138 "include/linux/fs.h"
1288struct fasync_struct;
1289#line 1138 "include/linux/fs.h"
1290struct __anonstruct_afs_154 {
1291   struct list_head link ;
1292   int state ;
1293};
1294#line 1138 "include/linux/fs.h"
1295union __anonunion_fl_u_153 {
1296   struct nfs_lock_info nfs_fl ;
1297   struct nfs4_lock_info nfs4_fl ;
1298   struct __anonstruct_afs_154 afs ;
1299};
1300#line 1138 "include/linux/fs.h"
1301struct file_lock {
1302   struct file_lock *fl_next ;
1303   struct list_head fl_link ;
1304   struct list_head fl_block ;
1305   fl_owner_t fl_owner ;
1306   unsigned int fl_flags ;
1307   unsigned char fl_type ;
1308   unsigned int fl_pid ;
1309   struct pid *fl_nspid ;
1310   wait_queue_head_t fl_wait ;
1311   struct file *fl_file ;
1312   loff_t fl_start ;
1313   loff_t fl_end ;
1314   struct fasync_struct *fl_fasync ;
1315   unsigned long fl_break_time ;
1316   unsigned long fl_downgrade_time ;
1317   struct file_lock_operations  const  *fl_ops ;
1318   struct lock_manager_operations  const  *fl_lmops ;
1319   union __anonunion_fl_u_153 fl_u ;
1320};
1321#line 1378 "include/linux/fs.h"
1322struct fasync_struct {
1323   spinlock_t fa_lock ;
1324   int magic ;
1325   int fa_fd ;
1326   struct fasync_struct *fa_next ;
1327   struct file *fa_file ;
1328   struct rcu_head fa_rcu ;
1329};
1330#line 1418
1331struct file_system_type;
1332#line 1418
1333struct super_operations;
1334#line 1418
1335struct xattr_handler;
1336#line 1418
1337struct mtd_info;
1338#line 1418 "include/linux/fs.h"
1339struct super_block {
1340   struct list_head s_list ;
1341   dev_t s_dev ;
1342   unsigned char s_dirt ;
1343   unsigned char s_blocksize_bits ;
1344   unsigned long s_blocksize ;
1345   loff_t s_maxbytes ;
1346   struct file_system_type *s_type ;
1347   struct super_operations  const  *s_op ;
1348   struct dquot_operations  const  *dq_op ;
1349   struct quotactl_ops  const  *s_qcop ;
1350   struct export_operations  const  *s_export_op ;
1351   unsigned long s_flags ;
1352   unsigned long s_magic ;
1353   struct dentry *s_root ;
1354   struct rw_semaphore s_umount ;
1355   struct mutex s_lock ;
1356   int s_count ;
1357   atomic_t s_active ;
1358   void *s_security ;
1359   struct xattr_handler  const  **s_xattr ;
1360   struct list_head s_inodes ;
1361   struct hlist_bl_head s_anon ;
1362   struct list_head *s_files ;
1363   struct list_head s_mounts ;
1364   struct list_head s_dentry_lru ;
1365   int s_nr_dentry_unused ;
1366   spinlock_t s_inode_lru_lock  __attribute__((__aligned__((1) <<  (6) ))) ;
1367   struct list_head s_inode_lru ;
1368   int s_nr_inodes_unused ;
1369   struct block_device *s_bdev ;
1370   struct backing_dev_info *s_bdi ;
1371   struct mtd_info *s_mtd ;
1372   struct hlist_node s_instances ;
1373   struct quota_info s_dquot ;
1374   int s_frozen ;
1375   wait_queue_head_t s_wait_unfrozen ;
1376   char s_id[32] ;
1377   u8 s_uuid[16] ;
1378   void *s_fs_info ;
1379   unsigned int s_max_links ;
1380   fmode_t s_mode ;
1381   u32 s_time_gran ;
1382   struct mutex s_vfs_rename_mutex ;
1383   char *s_subtype ;
1384   char *s_options ;
1385   struct dentry_operations  const  *s_d_op ;
1386   int cleancache_poolid ;
1387   struct shrinker s_shrink ;
1388   atomic_long_t s_remove_count ;
1389   int s_readonly_remount ;
1390};
1391#line 1567 "include/linux/fs.h"
1392struct fiemap_extent_info {
1393   unsigned int fi_flags ;
1394   unsigned int fi_extents_mapped ;
1395   unsigned int fi_extents_max ;
1396   struct fiemap_extent *fi_extents_start ;
1397};
1398#line 1609 "include/linux/fs.h"
1399struct file_operations {
1400   struct module *owner ;
1401   loff_t (*llseek)(struct file * , loff_t  , int  ) ;
1402   ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
1403   ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
1404   ssize_t (*aio_read)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1405                       loff_t  ) ;
1406   ssize_t (*aio_write)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1407                        loff_t  ) ;
1408   int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
1409                                                   loff_t  , u64  , unsigned int  ) ) ;
1410   unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1411   long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1412   long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1413   int (*mmap)(struct file * , struct vm_area_struct * ) ;
1414   int (*open)(struct inode * , struct file * ) ;
1415   int (*flush)(struct file * , fl_owner_t id ) ;
1416   int (*release)(struct inode * , struct file * ) ;
1417   int (*fsync)(struct file * , loff_t  , loff_t  , int datasync ) ;
1418   int (*aio_fsync)(struct kiocb * , int datasync ) ;
1419   int (*fasync)(int  , struct file * , int  ) ;
1420   int (*lock)(struct file * , int  , struct file_lock * ) ;
1421   ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
1422                       int  ) ;
1423   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
1424                                      unsigned long  , unsigned long  ) ;
1425   int (*check_flags)(int  ) ;
1426   int (*flock)(struct file * , int  , struct file_lock * ) ;
1427   ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t  ,
1428                           unsigned int  ) ;
1429   ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t  ,
1430                          unsigned int  ) ;
1431   int (*setlease)(struct file * , long  , struct file_lock ** ) ;
1432   long (*fallocate)(struct file *file , int mode , loff_t offset , loff_t len ) ;
1433};
1434#line 1639 "include/linux/fs.h"
1435struct inode_operations {
1436   struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1437   void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1438   int (*permission)(struct inode * , int  ) ;
1439   struct posix_acl *(*get_acl)(struct inode * , int  ) ;
1440   int (*readlink)(struct dentry * , char * , int  ) ;
1441   void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
1442   int (*create)(struct inode * , struct dentry * , umode_t  , struct nameidata * ) ;
1443   int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
1444   int (*unlink)(struct inode * , struct dentry * ) ;
1445   int (*symlink)(struct inode * , struct dentry * , char const   * ) ;
1446   int (*mkdir)(struct inode * , struct dentry * , umode_t  ) ;
1447   int (*rmdir)(struct inode * , struct dentry * ) ;
1448   int (*mknod)(struct inode * , struct dentry * , umode_t  , dev_t  ) ;
1449   int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
1450   void (*truncate)(struct inode * ) ;
1451   int (*setattr)(struct dentry * , struct iattr * ) ;
1452   int (*getattr)(struct vfsmount *mnt , struct dentry * , struct kstat * ) ;
1453   int (*setxattr)(struct dentry * , char const   * , void const   * , size_t  , int  ) ;
1454   ssize_t (*getxattr)(struct dentry * , char const   * , void * , size_t  ) ;
1455   ssize_t (*listxattr)(struct dentry * , char * , size_t  ) ;
1456   int (*removexattr)(struct dentry * , char const   * ) ;
1457   void (*truncate_range)(struct inode * , loff_t  , loff_t  ) ;
1458   int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 start , u64 len ) ;
1459} __attribute__((__aligned__((1) <<  (6) ))) ;
1460#line 1669
1461struct seq_file;
1462#line 1684 "include/linux/fs.h"
1463struct super_operations {
1464   struct inode *(*alloc_inode)(struct super_block *sb ) ;
1465   void (*destroy_inode)(struct inode * ) ;
1466   void (*dirty_inode)(struct inode * , int flags ) ;
1467   int (*write_inode)(struct inode * , struct writeback_control *wbc ) ;
1468   int (*drop_inode)(struct inode * ) ;
1469   void (*evict_inode)(struct inode * ) ;
1470   void (*put_super)(struct super_block * ) ;
1471   void (*write_super)(struct super_block * ) ;
1472   int (*sync_fs)(struct super_block *sb , int wait ) ;
1473   int (*freeze_fs)(struct super_block * ) ;
1474   int (*unfreeze_fs)(struct super_block * ) ;
1475   int (*statfs)(struct dentry * , struct kstatfs * ) ;
1476   int (*remount_fs)(struct super_block * , int * , char * ) ;
1477   void (*umount_begin)(struct super_block * ) ;
1478   int (*show_options)(struct seq_file * , struct dentry * ) ;
1479   int (*show_devname)(struct seq_file * , struct dentry * ) ;
1480   int (*show_path)(struct seq_file * , struct dentry * ) ;
1481   int (*show_stats)(struct seq_file * , struct dentry * ) ;
1482   ssize_t (*quota_read)(struct super_block * , int  , char * , size_t  , loff_t  ) ;
1483   ssize_t (*quota_write)(struct super_block * , int  , char const   * , size_t  ,
1484                          loff_t  ) ;
1485   int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t  ) ;
1486   int (*nr_cached_objects)(struct super_block * ) ;
1487   void (*free_cached_objects)(struct super_block * , int  ) ;
1488};
1489#line 1835 "include/linux/fs.h"
1490struct file_system_type {
1491   char const   *name ;
1492   int fs_flags ;
1493   struct dentry *(*mount)(struct file_system_type * , int  , char const   * , void * ) ;
1494   void (*kill_sb)(struct super_block * ) ;
1495   struct module *owner ;
1496   struct file_system_type *next ;
1497   struct hlist_head fs_supers ;
1498   struct lock_class_key s_lock_key ;
1499   struct lock_class_key s_umount_key ;
1500   struct lock_class_key s_vfs_rename_key ;
1501   struct lock_class_key i_lock_key ;
1502   struct lock_class_key i_mutex_key ;
1503   struct lock_class_key i_mutex_dir_key ;
1504};
1505#line 11 "include/linux/proc_fs.h"
1506struct completion;
1507#line 117
1508struct pid_namespace;
1509#line 106 "include/linux/parport.h"
1510struct parport;
1511#line 106
1512struct parport;
1513#line 107
1514struct pardevice;
1515#line 107
1516struct pardevice;
1517#line 109 "include/linux/parport.h"
1518struct pc_parport_state {
1519   unsigned int ctr ;
1520   unsigned int ecr ;
1521};
1522#line 114 "include/linux/parport.h"
1523struct ax_parport_state {
1524   unsigned int ctr ;
1525   unsigned int ecr ;
1526   unsigned int dcsr ;
1527};
1528#line 121 "include/linux/parport.h"
1529struct amiga_parport_state {
1530   unsigned char data ;
1531   unsigned char datadir ;
1532   unsigned char status ;
1533   unsigned char statusdir ;
1534};
1535#line 128 "include/linux/parport.h"
1536struct ax88796_parport_state {
1537   unsigned char cpr ;
1538};
1539#line 132 "include/linux/parport.h"
1540struct ip32_parport_state {
1541   unsigned int dcr ;
1542   unsigned int ecr ;
1543};
1544#line 137 "include/linux/parport.h"
1545union __anonunion_u_158 {
1546   struct pc_parport_state pc ;
1547   struct ax_parport_state ax ;
1548   struct amiga_parport_state amiga ;
1549   struct ax88796_parport_state ax88796 ;
1550   struct ip32_parport_state ip32 ;
1551   void *misc ;
1552};
1553#line 137 "include/linux/parport.h"
1554struct parport_state {
1555   union __anonunion_u_158 u ;
1556};
1557#line 150 "include/linux/parport.h"
1558struct parport_operations {
1559   void (*write_data)(struct parport * , unsigned char  ) ;
1560   unsigned char (*read_data)(struct parport * ) ;
1561   void (*write_control)(struct parport * , unsigned char  ) ;
1562   unsigned char (*read_control)(struct parport * ) ;
1563   unsigned char (*frob_control)(struct parport * , unsigned char mask , unsigned char val ) ;
1564   unsigned char (*read_status)(struct parport * ) ;
1565   void (*enable_irq)(struct parport * ) ;
1566   void (*disable_irq)(struct parport * ) ;
1567   void (*data_forward)(struct parport * ) ;
1568   void (*data_reverse)(struct parport * ) ;
1569   void (*init_state)(struct pardevice * , struct parport_state * ) ;
1570   void (*save_state)(struct parport * , struct parport_state * ) ;
1571   void (*restore_state)(struct parport * , struct parport_state * ) ;
1572   size_t (*epp_write_data)(struct parport *port , void const   *buf , size_t len ,
1573                            int flags ) ;
1574   size_t (*epp_read_data)(struct parport *port , void *buf , size_t len , int flags ) ;
1575   size_t (*epp_write_addr)(struct parport *port , void const   *buf , size_t len ,
1576                            int flags ) ;
1577   size_t (*epp_read_addr)(struct parport *port , void *buf , size_t len , int flags ) ;
1578   size_t (*ecp_write_data)(struct parport *port , void const   *buf , size_t len ,
1579                            int flags ) ;
1580   size_t (*ecp_read_data)(struct parport *port , void *buf , size_t len , int flags ) ;
1581   size_t (*ecp_write_addr)(struct parport *port , void const   *buf , size_t len ,
1582                            int flags ) ;
1583   size_t (*compat_write_data)(struct parport *port , void const   *buf , size_t len ,
1584                               int flags ) ;
1585   size_t (*nibble_read_data)(struct parport *port , void *buf , size_t len , int flags ) ;
1586   size_t (*byte_read_data)(struct parport *port , void *buf , size_t len , int flags ) ;
1587   struct module *owner ;
1588};
1589#line 201 "include/linux/parport.h"
1590struct parport_device_info {
1591   parport_device_class class ;
1592   char const   *class_name ;
1593   char const   *mfr ;
1594   char const   *model ;
1595   char const   *cmdset ;
1596   char const   *description ;
1597};
1598#line 223 "include/linux/parport.h"
1599struct pardevice {
1600   char const   *name ;
1601   struct parport *port ;
1602   int daisy ;
1603   int (*preempt)(void * ) ;
1604   void (*wakeup)(void * ) ;
1605   void *private ;
1606   void (*irq_func)(void * ) ;
1607   unsigned int flags ;
1608   struct pardevice *next ;
1609   struct pardevice *prev ;
1610   struct parport_state *state ;
1611   wait_queue_head_t wait_q ;
1612   unsigned long time ;
1613   unsigned long timeslice ;
1614   long volatile   timeout ;
1615   unsigned long waiting ;
1616   struct pardevice *waitprev ;
1617   struct pardevice *waitnext ;
1618   void *sysctl_table ;
1619};
1620#line 249
1621enum ieee1284_phase {
1622    IEEE1284_PH_FWD_DATA = 0,
1623    IEEE1284_PH_FWD_IDLE = 1,
1624    IEEE1284_PH_TERMINATE = 2,
1625    IEEE1284_PH_NEGOTIATION = 3,
1626    IEEE1284_PH_HBUSY_DNA = 4,
1627    IEEE1284_PH_REV_IDLE = 5,
1628    IEEE1284_PH_HBUSY_DAVAIL = 6,
1629    IEEE1284_PH_REV_DATA = 7,
1630    IEEE1284_PH_ECP_SETUP = 8,
1631    IEEE1284_PH_ECP_FWD_TO_REV = 9,
1632    IEEE1284_PH_ECP_REV_TO_FWD = 10,
1633    IEEE1284_PH_ECP_DIR_UNKNOWN = 11
1634} ;
1635#line 263 "include/linux/parport.h"
1636struct ieee1284_info {
1637   int mode ;
1638   enum ieee1284_phase  volatile  phase ;
1639   struct semaphore irq ;
1640};
1641#line 270 "include/linux/parport.h"
1642struct parport {
1643   unsigned long base ;
1644   unsigned long base_hi ;
1645   unsigned int size ;
1646   char const   *name ;
1647   unsigned int modes ;
1648   int irq ;
1649   int dma ;
1650   int muxport ;
1651   int portnum ;
1652   struct device *dev ;
1653   struct parport *physport ;
1654   struct pardevice *devices ;
1655   struct pardevice *cad ;
1656   int daisy ;
1657   int muxsel ;
1658   struct pardevice *waithead ;
1659   struct pardevice *waittail ;
1660   struct list_head list ;
1661   unsigned int flags ;
1662   void *sysctl_table ;
1663   struct parport_device_info probe_info[5] ;
1664   struct ieee1284_info ieee1284 ;
1665   struct parport_operations *ops ;
1666   void *private_data ;
1667   int number ;
1668   spinlock_t pardevice_lock ;
1669   spinlock_t waitlist_lock ;
1670   rwlock_t cad_lock ;
1671   int spintime ;
1672   atomic_t ref_count ;
1673   unsigned long devflags ;
1674   struct pardevice *proc_device ;
1675   struct list_head full_list ;
1676   struct parport *slaves[3] ;
1677};
1678#line 43 "include/linux/input.h"
1679struct input_id {
1680   __u16 bustype ;
1681   __u16 vendor ;
1682   __u16 product ;
1683   __u16 version ;
1684};
1685#line 69 "include/linux/input.h"
1686struct input_absinfo {
1687   __s32 value ;
1688   __s32 minimum ;
1689   __s32 maximum ;
1690   __s32 fuzz ;
1691   __s32 flat ;
1692   __s32 resolution ;
1693};
1694#line 93 "include/linux/input.h"
1695struct input_keymap_entry {
1696   __u8 flags ;
1697   __u8 len ;
1698   __u16 index ;
1699   __u32 keycode ;
1700   __u8 scancode[32] ;
1701};
1702#line 957 "include/linux/input.h"
1703struct ff_replay {
1704   __u16 length ;
1705   __u16 delay ;
1706};
1707#line 967 "include/linux/input.h"
1708struct ff_trigger {
1709   __u16 button ;
1710   __u16 interval ;
1711};
1712#line 984 "include/linux/input.h"
1713struct ff_envelope {
1714   __u16 attack_length ;
1715   __u16 attack_level ;
1716   __u16 fade_length ;
1717   __u16 fade_level ;
1718};
1719#line 996 "include/linux/input.h"
1720struct ff_constant_effect {
1721   __s16 level ;
1722   struct ff_envelope envelope ;
1723};
1724#line 1007 "include/linux/input.h"
1725struct ff_ramp_effect {
1726   __s16 start_level ;
1727   __s16 end_level ;
1728   struct ff_envelope envelope ;
1729};
1730#line 1023 "include/linux/input.h"
1731struct ff_condition_effect {
1732   __u16 right_saturation ;
1733   __u16 left_saturation ;
1734   __s16 right_coeff ;
1735   __s16 left_coeff ;
1736   __u16 deadband ;
1737   __s16 center ;
1738};
1739#line 1052 "include/linux/input.h"
1740struct ff_periodic_effect {
1741   __u16 waveform ;
1742   __u16 period ;
1743   __s16 magnitude ;
1744   __s16 offset ;
1745   __u16 phase ;
1746   struct ff_envelope envelope ;
1747   __u32 custom_len ;
1748   __s16 *custom_data ;
1749};
1750#line 1073 "include/linux/input.h"
1751struct ff_rumble_effect {
1752   __u16 strong_magnitude ;
1753   __u16 weak_magnitude ;
1754};
1755#line 1101 "include/linux/input.h"
1756union __anonunion_u_159 {
1757   struct ff_constant_effect constant ;
1758   struct ff_ramp_effect ramp ;
1759   struct ff_periodic_effect periodic ;
1760   struct ff_condition_effect condition[2] ;
1761   struct ff_rumble_effect rumble ;
1762};
1763#line 1101 "include/linux/input.h"
1764struct ff_effect {
1765   __u16 type ;
1766   __s16 id ;
1767   __u16 direction ;
1768   struct ff_trigger trigger ;
1769   struct ff_replay replay ;
1770   union __anonunion_u_159 u ;
1771};
1772#line 19 "include/linux/klist.h"
1773struct klist_node;
1774#line 19
1775struct klist_node;
1776#line 39 "include/linux/klist.h"
1777struct klist_node {
1778   void *n_klist ;
1779   struct list_head n_node ;
1780   struct kref n_ref ;
1781};
1782#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1783struct dma_map_ops;
1784#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1785struct dev_archdata {
1786   void *acpi_handle ;
1787   struct dma_map_ops *dma_ops ;
1788   void *iommu ;
1789};
1790#line 28 "include/linux/device.h"
1791struct device;
1792#line 29
1793struct device_private;
1794#line 29
1795struct device_private;
1796#line 30
1797struct device_driver;
1798#line 30
1799struct device_driver;
1800#line 31
1801struct driver_private;
1802#line 31
1803struct driver_private;
1804#line 32
1805struct module;
1806#line 33
1807struct class;
1808#line 33
1809struct class;
1810#line 34
1811struct subsys_private;
1812#line 34
1813struct subsys_private;
1814#line 35
1815struct bus_type;
1816#line 35
1817struct bus_type;
1818#line 36
1819struct device_node;
1820#line 36
1821struct device_node;
1822#line 37
1823struct iommu_ops;
1824#line 37
1825struct iommu_ops;
1826#line 39 "include/linux/device.h"
1827struct bus_attribute {
1828   struct attribute attr ;
1829   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
1830   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
1831};
1832#line 89
1833struct device_attribute;
1834#line 89
1835struct driver_attribute;
1836#line 89 "include/linux/device.h"
1837struct bus_type {
1838   char const   *name ;
1839   char const   *dev_name ;
1840   struct device *dev_root ;
1841   struct bus_attribute *bus_attrs ;
1842   struct device_attribute *dev_attrs ;
1843   struct driver_attribute *drv_attrs ;
1844   int (*match)(struct device *dev , struct device_driver *drv ) ;
1845   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1846   int (*probe)(struct device *dev ) ;
1847   int (*remove)(struct device *dev ) ;
1848   void (*shutdown)(struct device *dev ) ;
1849   int (*suspend)(struct device *dev , pm_message_t state ) ;
1850   int (*resume)(struct device *dev ) ;
1851   struct dev_pm_ops  const  *pm ;
1852   struct iommu_ops *iommu_ops ;
1853   struct subsys_private *p ;
1854};
1855#line 127
1856struct device_type;
1857#line 214
1858struct of_device_id;
1859#line 214 "include/linux/device.h"
1860struct device_driver {
1861   char const   *name ;
1862   struct bus_type *bus ;
1863   struct module *owner ;
1864   char const   *mod_name ;
1865   bool suppress_bind_attrs ;
1866   struct of_device_id  const  *of_match_table ;
1867   int (*probe)(struct device *dev ) ;
1868   int (*remove)(struct device *dev ) ;
1869   void (*shutdown)(struct device *dev ) ;
1870   int (*suspend)(struct device *dev , pm_message_t state ) ;
1871   int (*resume)(struct device *dev ) ;
1872   struct attribute_group  const  **groups ;
1873   struct dev_pm_ops  const  *pm ;
1874   struct driver_private *p ;
1875};
1876#line 249 "include/linux/device.h"
1877struct driver_attribute {
1878   struct attribute attr ;
1879   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
1880   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
1881};
1882#line 330
1883struct class_attribute;
1884#line 330 "include/linux/device.h"
1885struct class {
1886   char const   *name ;
1887   struct module *owner ;
1888   struct class_attribute *class_attrs ;
1889   struct device_attribute *dev_attrs ;
1890   struct bin_attribute *dev_bin_attrs ;
1891   struct kobject *dev_kobj ;
1892   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1893   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1894   void (*class_release)(struct class *class ) ;
1895   void (*dev_release)(struct device *dev ) ;
1896   int (*suspend)(struct device *dev , pm_message_t state ) ;
1897   int (*resume)(struct device *dev ) ;
1898   struct kobj_ns_type_operations  const  *ns_type ;
1899   void const   *(*namespace)(struct device *dev ) ;
1900   struct dev_pm_ops  const  *pm ;
1901   struct subsys_private *p ;
1902};
1903#line 397 "include/linux/device.h"
1904struct class_attribute {
1905   struct attribute attr ;
1906   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
1907   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
1908                    size_t count ) ;
1909   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
1910};
1911#line 465 "include/linux/device.h"
1912struct device_type {
1913   char const   *name ;
1914   struct attribute_group  const  **groups ;
1915   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1916   char *(*devnode)(struct device *dev , umode_t *mode ) ;
1917   void (*release)(struct device *dev ) ;
1918   struct dev_pm_ops  const  *pm ;
1919};
1920#line 476 "include/linux/device.h"
1921struct device_attribute {
1922   struct attribute attr ;
1923   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
1924   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
1925                    size_t count ) ;
1926};
1927#line 559 "include/linux/device.h"
1928struct device_dma_parameters {
1929   unsigned int max_segment_size ;
1930   unsigned long segment_boundary_mask ;
1931};
1932#line 627
1933struct dma_coherent_mem;
1934#line 627 "include/linux/device.h"
1935struct device {
1936   struct device *parent ;
1937   struct device_private *p ;
1938   struct kobject kobj ;
1939   char const   *init_name ;
1940   struct device_type  const  *type ;
1941   struct mutex mutex ;
1942   struct bus_type *bus ;
1943   struct device_driver *driver ;
1944   void *platform_data ;
1945   struct dev_pm_info power ;
1946   struct dev_pm_domain *pm_domain ;
1947   int numa_node ;
1948   u64 *dma_mask ;
1949   u64 coherent_dma_mask ;
1950   struct device_dma_parameters *dma_parms ;
1951   struct list_head dma_pools ;
1952   struct dma_coherent_mem *dma_mem ;
1953   struct dev_archdata archdata ;
1954   struct device_node *of_node ;
1955   dev_t devt ;
1956   u32 id ;
1957   spinlock_t devres_lock ;
1958   struct list_head devres_head ;
1959   struct klist_node knode_class ;
1960   struct class *class ;
1961   struct attribute_group  const  **groups ;
1962   void (*release)(struct device *dev ) ;
1963};
1964#line 43 "include/linux/pm_wakeup.h"
1965struct wakeup_source {
1966   char const   *name ;
1967   struct list_head entry ;
1968   spinlock_t lock ;
1969   struct timer_list timer ;
1970   unsigned long timer_expires ;
1971   ktime_t total_time ;
1972   ktime_t max_time ;
1973   ktime_t last_time ;
1974   unsigned long event_count ;
1975   unsigned long active_count ;
1976   unsigned long relax_count ;
1977   unsigned long hit_count ;
1978   unsigned int active : 1 ;
1979};
1980#line 12 "include/linux/mod_devicetable.h"
1981typedef unsigned long kernel_ulong_t;
1982#line 219 "include/linux/mod_devicetable.h"
1983struct of_device_id {
1984   char name[32] ;
1985   char type[32] ;
1986   char compatible[128] ;
1987   void *data ;
1988};
1989#line 312 "include/linux/mod_devicetable.h"
1990struct input_device_id {
1991   kernel_ulong_t flags ;
1992   __u16 bustype ;
1993   __u16 vendor ;
1994   __u16 product ;
1995   __u16 version ;
1996   kernel_ulong_t evbit[1] ;
1997   kernel_ulong_t keybit[12] ;
1998   kernel_ulong_t relbit[1] ;
1999   kernel_ulong_t absbit[1] ;
2000   kernel_ulong_t mscbit[1] ;
2001   kernel_ulong_t ledbit[1] ;
2002   kernel_ulong_t sndbit[1] ;
2003   kernel_ulong_t ffbit[2] ;
2004   kernel_ulong_t swbit[1] ;
2005   kernel_ulong_t driver_info ;
2006};
2007#line 1250 "include/linux/input.h"
2008struct ff_device;
2009#line 1250
2010struct input_mt_slot;
2011#line 1250
2012struct input_handle;
2013#line 1250 "include/linux/input.h"
2014struct input_dev {
2015   char const   *name ;
2016   char const   *phys ;
2017   char const   *uniq ;
2018   struct input_id id ;
2019   unsigned long propbit[((32UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2020   unsigned long evbit[((32UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2021   unsigned long keybit[((768UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2022   unsigned long relbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2023   unsigned long absbit[((64UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2024   unsigned long mscbit[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2025   unsigned long ledbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2026   unsigned long sndbit[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2027   unsigned long ffbit[((128UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2028   unsigned long swbit[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2029   unsigned int hint_events_per_packet ;
2030   unsigned int keycodemax ;
2031   unsigned int keycodesize ;
2032   void *keycode ;
2033   int (*setkeycode)(struct input_dev *dev , struct input_keymap_entry  const  *ke ,
2034                     unsigned int *old_keycode ) ;
2035   int (*getkeycode)(struct input_dev *dev , struct input_keymap_entry *ke ) ;
2036   struct ff_device *ff ;
2037   unsigned int repeat_key ;
2038   struct timer_list timer ;
2039   int rep[2] ;
2040   struct input_mt_slot *mt ;
2041   int mtsize ;
2042   int slot ;
2043   int trkid ;
2044   struct input_absinfo *absinfo ;
2045   unsigned long key[((768UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2046   unsigned long led[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2047   unsigned long snd[((8UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2048   unsigned long sw[((16UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2049   int (*open)(struct input_dev *dev ) ;
2050   void (*close)(struct input_dev *dev ) ;
2051   int (*flush)(struct input_dev *dev , struct file *file ) ;
2052   int (*event)(struct input_dev *dev , unsigned int type , unsigned int code , int value ) ;
2053   struct input_handle *grab ;
2054   spinlock_t event_lock ;
2055   struct mutex mutex ;
2056   unsigned int users ;
2057   bool going_away ;
2058   bool sync ;
2059   struct device dev ;
2060   struct list_head h_list ;
2061   struct list_head node ;
2062};
2063#line 1370
2064struct input_handle;
2065#line 1409 "include/linux/input.h"
2066struct input_handler {
2067   void *private ;
2068   void (*event)(struct input_handle *handle , unsigned int type , unsigned int code ,
2069                 int value ) ;
2070   bool (*filter)(struct input_handle *handle , unsigned int type , unsigned int code ,
2071                  int value ) ;
2072   bool (*match)(struct input_handler *handler , struct input_dev *dev ) ;
2073   int (*connect)(struct input_handler *handler , struct input_dev *dev , struct input_device_id  const  *id ) ;
2074   void (*disconnect)(struct input_handle *handle ) ;
2075   void (*start)(struct input_handle *handle ) ;
2076   struct file_operations  const  *fops ;
2077   int minor ;
2078   char const   *name ;
2079   struct input_device_id  const  *id_table ;
2080   struct list_head h_list ;
2081   struct list_head node ;
2082};
2083#line 1442 "include/linux/input.h"
2084struct input_handle {
2085   void *private ;
2086   int open ;
2087   char const   *name ;
2088   struct input_dev *dev ;
2089   struct input_handler *handler ;
2090   struct list_head d_node ;
2091   struct list_head h_node ;
2092};
2093#line 1619 "include/linux/input.h"
2094struct ff_device {
2095   int (*upload)(struct input_dev *dev , struct ff_effect *effect , struct ff_effect *old ) ;
2096   int (*erase)(struct input_dev *dev , int effect_id ) ;
2097   int (*playback)(struct input_dev *dev , int effect_id , int value ) ;
2098   void (*set_gain)(struct input_dev *dev , u16 gain ) ;
2099   void (*set_autocenter)(struct input_dev *dev , u16 magnitude ) ;
2100   void (*destroy)(struct ff_device * ) ;
2101   void *private ;
2102   unsigned long ffbit[((128UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
2103   struct mutex mutex ;
2104   int max_effects ;
2105   struct ff_effect *effects ;
2106   struct file *effect_owners[] ;
2107};
2108#line 29 "include/linux/sysctl.h"
2109struct completion;
2110#line 48 "include/linux/kmod.h"
2111struct cred;
2112#line 49
2113struct file;
2114#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
2115struct task_struct;
2116#line 18 "include/linux/elf.h"
2117typedef __u64 Elf64_Addr;
2118#line 19 "include/linux/elf.h"
2119typedef __u16 Elf64_Half;
2120#line 23 "include/linux/elf.h"
2121typedef __u32 Elf64_Word;
2122#line 24 "include/linux/elf.h"
2123typedef __u64 Elf64_Xword;
2124#line 194 "include/linux/elf.h"
2125struct elf64_sym {
2126   Elf64_Word st_name ;
2127   unsigned char st_info ;
2128   unsigned char st_other ;
2129   Elf64_Half st_shndx ;
2130   Elf64_Addr st_value ;
2131   Elf64_Xword st_size ;
2132};
2133#line 194 "include/linux/elf.h"
2134typedef struct elf64_sym Elf64_Sym;
2135#line 438
2136struct file;
2137#line 39 "include/linux/moduleparam.h"
2138struct kernel_param;
2139#line 39
2140struct kernel_param;
2141#line 41 "include/linux/moduleparam.h"
2142struct kernel_param_ops {
2143   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
2144   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
2145   void (*free)(void *arg ) ;
2146};
2147#line 50
2148struct kparam_string;
2149#line 50
2150struct kparam_array;
2151#line 50 "include/linux/moduleparam.h"
2152union __anonunion____missing_field_name_221 {
2153   void *arg ;
2154   struct kparam_string  const  *str ;
2155   struct kparam_array  const  *arr ;
2156};
2157#line 50 "include/linux/moduleparam.h"
2158struct kernel_param {
2159   char const   *name ;
2160   struct kernel_param_ops  const  *ops ;
2161   u16 perm ;
2162   s16 level ;
2163   union __anonunion____missing_field_name_221 __annonCompField35 ;
2164};
2165#line 63 "include/linux/moduleparam.h"
2166struct kparam_string {
2167   unsigned int maxlen ;
2168   char *string ;
2169};
2170#line 69 "include/linux/moduleparam.h"
2171struct kparam_array {
2172   unsigned int max ;
2173   unsigned int elemsize ;
2174   unsigned int *num ;
2175   struct kernel_param_ops  const  *ops ;
2176   void *elem ;
2177};
2178#line 445
2179struct module;
2180#line 80 "include/linux/jump_label.h"
2181struct module;
2182#line 143 "include/linux/jump_label.h"
2183struct static_key {
2184   atomic_t enabled ;
2185};
2186#line 22 "include/linux/tracepoint.h"
2187struct module;
2188#line 23
2189struct tracepoint;
2190#line 23
2191struct tracepoint;
2192#line 25 "include/linux/tracepoint.h"
2193struct tracepoint_func {
2194   void *func ;
2195   void *data ;
2196};
2197#line 30 "include/linux/tracepoint.h"
2198struct tracepoint {
2199   char const   *name ;
2200   struct static_key key ;
2201   void (*regfunc)(void) ;
2202   void (*unregfunc)(void) ;
2203   struct tracepoint_func *funcs ;
2204};
2205#line 19 "include/linux/export.h"
2206struct kernel_symbol {
2207   unsigned long value ;
2208   char const   *name ;
2209};
2210#line 8 "include/asm-generic/module.h"
2211struct mod_arch_specific {
2212
2213};
2214#line 35 "include/linux/module.h"
2215struct module;
2216#line 37
2217struct module_param_attrs;
2218#line 37 "include/linux/module.h"
2219struct module_kobject {
2220   struct kobject kobj ;
2221   struct module *mod ;
2222   struct kobject *drivers_dir ;
2223   struct module_param_attrs *mp ;
2224};
2225#line 44 "include/linux/module.h"
2226struct module_attribute {
2227   struct attribute attr ;
2228   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
2229   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
2230                    size_t count ) ;
2231   void (*setup)(struct module * , char const   * ) ;
2232   int (*test)(struct module * ) ;
2233   void (*free)(struct module * ) ;
2234};
2235#line 71
2236struct exception_table_entry;
2237#line 71
2238struct exception_table_entry;
2239#line 199
2240enum module_state {
2241    MODULE_STATE_LIVE = 0,
2242    MODULE_STATE_COMING = 1,
2243    MODULE_STATE_GOING = 2
2244} ;
2245#line 215 "include/linux/module.h"
2246struct module_ref {
2247   unsigned long incs ;
2248   unsigned long decs ;
2249} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
2250#line 220
2251struct module_sect_attrs;
2252#line 220
2253struct module_notes_attrs;
2254#line 220
2255struct ftrace_event_call;
2256#line 220 "include/linux/module.h"
2257struct module {
2258   enum module_state state ;
2259   struct list_head list ;
2260   char name[64UL - sizeof(unsigned long )] ;
2261   struct module_kobject mkobj ;
2262   struct module_attribute *modinfo_attrs ;
2263   char const   *version ;
2264   char const   *srcversion ;
2265   struct kobject *holders_dir ;
2266   struct kernel_symbol  const  *syms ;
2267   unsigned long const   *crcs ;
2268   unsigned int num_syms ;
2269   struct kernel_param *kp ;
2270   unsigned int num_kp ;
2271   unsigned int num_gpl_syms ;
2272   struct kernel_symbol  const  *gpl_syms ;
2273   unsigned long const   *gpl_crcs ;
2274   struct kernel_symbol  const  *unused_syms ;
2275   unsigned long const   *unused_crcs ;
2276   unsigned int num_unused_syms ;
2277   unsigned int num_unused_gpl_syms ;
2278   struct kernel_symbol  const  *unused_gpl_syms ;
2279   unsigned long const   *unused_gpl_crcs ;
2280   struct kernel_symbol  const  *gpl_future_syms ;
2281   unsigned long const   *gpl_future_crcs ;
2282   unsigned int num_gpl_future_syms ;
2283   unsigned int num_exentries ;
2284   struct exception_table_entry *extable ;
2285   int (*init)(void) ;
2286   void *module_init ;
2287   void *module_core ;
2288   unsigned int init_size ;
2289   unsigned int core_size ;
2290   unsigned int init_text_size ;
2291   unsigned int core_text_size ;
2292   unsigned int init_ro_size ;
2293   unsigned int core_ro_size ;
2294   struct mod_arch_specific arch ;
2295   unsigned int taints ;
2296   unsigned int num_bugs ;
2297   struct list_head bug_list ;
2298   struct bug_entry *bug_table ;
2299   Elf64_Sym *symtab ;
2300   Elf64_Sym *core_symtab ;
2301   unsigned int num_symtab ;
2302   unsigned int core_num_syms ;
2303   char *strtab ;
2304   char *core_strtab ;
2305   struct module_sect_attrs *sect_attrs ;
2306   struct module_notes_attrs *notes_attrs ;
2307   char *args ;
2308   void *percpu ;
2309   unsigned int percpu_size ;
2310   unsigned int num_tracepoints ;
2311   struct tracepoint * const  *tracepoints_ptrs ;
2312   unsigned int num_trace_bprintk_fmt ;
2313   char const   **trace_bprintk_fmt_start ;
2314   struct ftrace_event_call **trace_events ;
2315   unsigned int num_trace_events ;
2316   struct list_head source_list ;
2317   struct list_head target_list ;
2318   struct task_struct *waiter ;
2319   void (*exit)(void) ;
2320   struct module_ref *refptr ;
2321   ctor_fn_t *ctors ;
2322   unsigned int num_ctors ;
2323};
2324#line 48 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2325struct tgfx_config {
2326   int args[8] ;
2327   unsigned int nargs ;
2328};
2329#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2330struct __anonstruct_223 {
2331   int  : 0 ;
2332};
2333#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2334struct __anonstruct_226 {
2335   int  : 0 ;
2336};
2337#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2338struct __anonstruct_229 {
2339   int  : 0 ;
2340};
2341#line 77 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2342struct tgfx {
2343   struct pardevice *pd ;
2344   struct timer_list timer ;
2345   struct input_dev *dev[7] ;
2346   char name[7][64] ;
2347   char phys[7][32] ;
2348   int sticks ;
2349   int used ;
2350   struct mutex sem ;
2351};
2352#line 1 "<compiler builtins>"
2353long __builtin_expect(long val , long res ) ;
2354#line 59 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
2355__inline static void ( __attribute__((__always_inline__)) set_bit)(unsigned int nr ,
2356                                                                   unsigned long volatile   *addr )  __attribute__((__no_instrument_function__)) ;
2357#line 59 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
2358__inline static void ( __attribute__((__always_inline__)) set_bit)(unsigned int nr ,
2359                                                                   unsigned long volatile   *addr ) 
2360{ long volatile   *__cil_tmp3 ;
2361
2362  {
2363#line 68
2364  __cil_tmp3 = (long volatile   *)addr;
2365#line 68
2366  __asm__  volatile   (".section .smp_locks,\"a\"\n"
2367                       ".balign 4\n"
2368                       ".long 671f - .\n"
2369                       ".previous\n"
2370                       "671:"
2371                       "\n\tlock; "
2372                       "bts %1,%0": "+m" (*__cil_tmp3): "Ir" (nr): "memory");
2373#line 71
2374  return;
2375}
2376}
2377#line 100 "include/linux/printk.h"
2378extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
2379#line 322 "include/linux/kernel.h"
2380extern int ( /* format attribute */  snprintf)(char *buf , size_t size , char const   *fmt 
2381                                               , ...) ;
2382#line 22 "include/linux/err.h"
2383__inline static void * __attribute__((__warn_unused_result__)) ERR_PTR(long error )  __attribute__((__no_instrument_function__)) ;
2384#line 22 "include/linux/err.h"
2385__inline static void * __attribute__((__warn_unused_result__)) ERR_PTR(long error ) 
2386{ 
2387
2388  {
2389#line 24
2390  return ((void *)error);
2391}
2392}
2393#line 27
2394__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
2395#line 27 "include/linux/err.h"
2396__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr ) 
2397{ 
2398
2399  {
2400#line 29
2401  return ((long )ptr);
2402}
2403}
2404#line 32
2405__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
2406#line 32 "include/linux/err.h"
2407__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr ) 
2408{ long tmp ;
2409  unsigned long __cil_tmp3 ;
2410  int __cil_tmp4 ;
2411  int __cil_tmp5 ;
2412  int __cil_tmp6 ;
2413  long __cil_tmp7 ;
2414
2415  {
2416  {
2417#line 34
2418  __cil_tmp3 = (unsigned long )ptr;
2419#line 34
2420  __cil_tmp4 = __cil_tmp3 >= 0xfffffffffffff001UL;
2421#line 34
2422  __cil_tmp5 = ! __cil_tmp4;
2423#line 34
2424  __cil_tmp6 = ! __cil_tmp5;
2425#line 34
2426  __cil_tmp7 = (long )__cil_tmp6;
2427#line 34
2428  tmp = __builtin_expect(__cil_tmp7, 0L);
2429  }
2430#line 34
2431  return (tmp);
2432}
2433}
2434#line 82 "include/linux/jiffies.h"
2435extern unsigned long volatile   jiffies  __attribute__((__section__(".data"))) ;
2436#line 115 "include/linux/mutex.h"
2437extern void __mutex_init(struct mutex *lock , char const   *name , struct lock_class_key *key ) ;
2438#line 152
2439void mutex_lock(struct mutex *lock ) ;
2440#line 153
2441int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
2442#line 154
2443int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
2444#line 168
2445int mutex_trylock(struct mutex *lock ) ;
2446#line 169
2447void mutex_unlock(struct mutex *lock ) ;
2448#line 170
2449int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
2450#line 91 "include/linux/timer.h"
2451extern void init_timer_key(struct timer_list *timer , char const   *name , struct lock_class_key *key ) ;
2452#line 211
2453extern int mod_timer(struct timer_list *timer , unsigned long expires ) ;
2454#line 280
2455extern int del_timer_sync(struct timer_list *timer ) ;
2456#line 161 "include/linux/slab.h"
2457extern void kfree(void const   * ) ;
2458#line 221 "include/linux/slub_def.h"
2459extern void *__kmalloc(size_t size , gfp_t flags ) ;
2460#line 268
2461__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2462                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2463#line 268 "include/linux/slub_def.h"
2464__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2465                                                                    gfp_t flags ) 
2466{ void *tmp___2 ;
2467
2468  {
2469  {
2470#line 283
2471  tmp___2 = __kmalloc(size, flags);
2472  }
2473#line 283
2474  return (tmp___2);
2475}
2476}
2477#line 349 "include/linux/slab.h"
2478__inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2479#line 349 "include/linux/slab.h"
2480__inline static void *kzalloc(size_t size , gfp_t flags ) 
2481{ void *tmp ;
2482  unsigned int __cil_tmp4 ;
2483
2484  {
2485  {
2486#line 351
2487  __cil_tmp4 = flags | 32768U;
2488#line 351
2489  tmp = kmalloc(size, __cil_tmp4);
2490  }
2491#line 351
2492  return (tmp);
2493}
2494}
2495#line 368 "include/linux/parport.h"
2496extern struct parport *parport_find_number(int  ) ;
2497#line 376
2498extern void parport_put_port(struct parport * ) ;
2499#line 384
2500extern struct pardevice *parport_register_device(struct parport *port , char const   *name ,
2501                                                 int (*pf)(void * ) , void (*kf)(void * ) ,
2502                                                 void (*irq_func)(void * ) , int flags ,
2503                                                 void *handle ) ;
2504#line 391
2505extern void parport_unregister_device(struct pardevice *dev ) ;
2506#line 397
2507extern int parport_claim(struct pardevice *dev ) ;
2508#line 412
2509extern void parport_release(struct pardevice *dev ) ;
2510#line 792 "include/linux/device.h"
2511extern void *dev_get_drvdata(struct device  const  *dev ) ;
2512#line 793
2513extern int dev_set_drvdata(struct device *dev , void *data ) ;
2514#line 1456 "include/linux/input.h"
2515extern struct input_dev *input_allocate_device(void) ;
2516#line 1457
2517extern void input_free_device(struct input_dev *dev ) ;
2518#line 1470
2519__inline static void *input_get_drvdata(struct input_dev *dev )  __attribute__((__no_instrument_function__)) ;
2520#line 1470 "include/linux/input.h"
2521__inline static void *input_get_drvdata(struct input_dev *dev ) 
2522{ void *tmp ;
2523  unsigned long __cil_tmp3 ;
2524  unsigned long __cil_tmp4 ;
2525  struct device *__cil_tmp5 ;
2526  struct device  const  *__cil_tmp6 ;
2527
2528  {
2529  {
2530#line 1472
2531  __cil_tmp3 = (unsigned long )dev;
2532#line 1472
2533  __cil_tmp4 = __cil_tmp3 + 648;
2534#line 1472
2535  __cil_tmp5 = (struct device *)__cil_tmp4;
2536#line 1472
2537  __cil_tmp6 = (struct device  const  *)__cil_tmp5;
2538#line 1472
2539  tmp = dev_get_drvdata(__cil_tmp6);
2540  }
2541#line 1472
2542  return (tmp);
2543}
2544}
2545#line 1475
2546__inline static void input_set_drvdata(struct input_dev *dev , void *data )  __attribute__((__no_instrument_function__)) ;
2547#line 1475 "include/linux/input.h"
2548__inline static void input_set_drvdata(struct input_dev *dev , void *data ) 
2549{ unsigned long __cil_tmp3 ;
2550  unsigned long __cil_tmp4 ;
2551  struct device *__cil_tmp5 ;
2552
2553  {
2554  {
2555#line 1477
2556  __cil_tmp3 = (unsigned long )dev;
2557#line 1477
2558  __cil_tmp4 = __cil_tmp3 + 648;
2559#line 1477
2560  __cil_tmp5 = (struct device *)__cil_tmp4;
2561#line 1477
2562  dev_set_drvdata(__cil_tmp5, data);
2563  }
2564#line 1478
2565  return;
2566}
2567}
2568#line 1480
2569extern int __attribute__((__warn_unused_result__))  input_register_device(struct input_dev * ) ;
2570#line 1481
2571extern void input_unregister_device(struct input_dev * ) ;
2572#line 1502
2573extern void input_event(struct input_dev *dev , unsigned int type , unsigned int code ,
2574                        int value ) ;
2575#line 1505
2576__inline static void input_report_key(struct input_dev *dev , unsigned int code ,
2577                                      int value )  __attribute__((__no_instrument_function__)) ;
2578#line 1505 "include/linux/input.h"
2579__inline static void input_report_key(struct input_dev *dev , unsigned int code ,
2580                                      int value ) 
2581{ int __cil_tmp4 ;
2582  int __cil_tmp5 ;
2583
2584  {
2585  {
2586#line 1507
2587  __cil_tmp4 = ! value;
2588#line 1507
2589  __cil_tmp5 = ! __cil_tmp4;
2590#line 1507
2591  input_event(dev, 1U, code, __cil_tmp5);
2592  }
2593#line 1508
2594  return;
2595}
2596}
2597#line 1515
2598__inline static void input_report_abs(struct input_dev *dev , unsigned int code ,
2599                                      int value )  __attribute__((__no_instrument_function__)) ;
2600#line 1515 "include/linux/input.h"
2601__inline static void input_report_abs(struct input_dev *dev , unsigned int code ,
2602                                      int value ) 
2603{ 
2604
2605  {
2606  {
2607#line 1517
2608  input_event(dev, 3U, code, value);
2609  }
2610#line 1518
2611  return;
2612}
2613}
2614#line 1530
2615__inline static void input_sync(struct input_dev *dev )  __attribute__((__no_instrument_function__)) ;
2616#line 1530 "include/linux/input.h"
2617__inline static void input_sync(struct input_dev *dev ) 
2618{ 
2619
2620  {
2621  {
2622#line 1532
2623  input_event(dev, 0U, 0U, 0);
2624  }
2625#line 1533
2626  return;
2627}
2628}
2629#line 1558
2630extern void input_set_abs_params(struct input_dev *dev , unsigned int axis , int min ,
2631                                 int max , int fuzz , int flat ) ;
2632#line 356 "include/linux/moduleparam.h"
2633extern struct kernel_param_ops param_ops_int ;
2634#line 437
2635extern struct kernel_param_ops param_array_ops ;
2636#line 67 "include/linux/module.h"
2637int init_module(void) ;
2638#line 68
2639void cleanup_module(void) ;
2640#line 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2641static char const   __mod_author41[39]  __attribute__((__used__, __unused__, __section__(".modinfo"),
2642__aligned__(1)))  = 
2643#line 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2644  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
2645        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'V', 
2646        (char const   )'o',      (char const   )'j',      (char const   )'t',      (char const   )'e', 
2647        (char const   )'c',      (char const   )'h',      (char const   )' ',      (char const   )'P', 
2648        (char const   )'a',      (char const   )'v',      (char const   )'l',      (char const   )'i', 
2649        (char const   )'k',      (char const   )' ',      (char const   )'<',      (char const   )'v', 
2650        (char const   )'o',      (char const   )'j',      (char const   )'t',      (char const   )'e', 
2651        (char const   )'c',      (char const   )'h',      (char const   )'@',      (char const   )'u', 
2652        (char const   )'c',      (char const   )'w',      (char const   )'.',      (char const   )'c', 
2653        (char const   )'z',      (char const   )'>',      (char const   )'\000'};
2654#line 42 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2655static char const   __mod_description42[54]  __attribute__((__used__, __unused__,
2656__section__(".modinfo"), __aligned__(1)))  = 
2657#line 42
2658  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
2659        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
2660        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
2661        (char const   )'T',      (char const   )'u',      (char const   )'r',      (char const   )'b', 
2662        (char const   )'o',      (char const   )'G',      (char const   )'r',      (char const   )'a', 
2663        (char const   )'F',      (char const   )'X',      (char const   )' ',      (char const   )'p', 
2664        (char const   )'a',      (char const   )'r',      (char const   )'a',      (char const   )'l', 
2665        (char const   )'l',      (char const   )'e',      (char const   )'l',      (char const   )' ', 
2666        (char const   )'p',      (char const   )'o',      (char const   )'r',      (char const   )'t', 
2667        (char const   )' ',      (char const   )'i',      (char const   )'n',      (char const   )'t', 
2668        (char const   )'e',      (char const   )'r',      (char const   )'f',      (char const   )'a', 
2669        (char const   )'c',      (char const   )'e',      (char const   )' ',      (char const   )'d', 
2670        (char const   )'r',      (char const   )'i',      (char const   )'v',      (char const   )'e', 
2671        (char const   )'r',      (char const   )'\000'};
2672#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2673static char const   __mod_license43[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
2674__aligned__(1)))  = 
2675#line 43
2676  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
2677        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
2678        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
2679#line 53 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2680static struct tgfx_config tgfx_cfg[3]  __attribute__((__section__(".init.data")))  ;
2681#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2682static struct kparam_array  const  __param_arr_map  =    {(unsigned int )(sizeof(tgfx_cfg[0].args) / sizeof(tgfx_cfg[0].args[0]) + sizeof(struct __anonstruct_223 )),
2683    (unsigned int )sizeof(tgfx_cfg[0].args[0]), & tgfx_cfg[0].nargs, (struct kernel_param_ops  const  *)(& param_ops_int),
2684    (void *)(tgfx_cfg[0].args)};
2685#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2686static char const   __param_str_map[4]  = {      (char const   )'m',      (char const   )'a',      (char const   )'p',      (char const   )'\000'};
2687#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2688static struct kernel_param  const  __param_map  __attribute__((__used__, __unused__,
2689__section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_map, (struct kernel_param_ops  const  *)(& param_array_ops), (u16 )0,
2690    (s16 )0, {.arr = & __param_arr_map}};
2691#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2692static char const   __mod_maptype55[26]  __attribute__((__used__, __unused__, __section__(".modinfo"),
2693__aligned__(1)))  = 
2694#line 55
2695  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
2696        (char const   )'t',      (char const   )'y',      (char const   )'p',      (char const   )'e', 
2697        (char const   )'=',      (char const   )'m',      (char const   )'a',      (char const   )'p', 
2698        (char const   )':',      (char const   )'a',      (char const   )'r',      (char const   )'r', 
2699        (char const   )'a',      (char const   )'y',      (char const   )' ',      (char const   )'o', 
2700        (char const   )'f',      (char const   )' ',      (char const   )'i',      (char const   )'n', 
2701        (char const   )'t',      (char const   )'\000'};
2702#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2703static char const   __mod_map56[72]  __attribute__((__used__, __unused__, __section__(".modinfo"),
2704__aligned__(1)))  = 
2705#line 56
2706  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
2707        (char const   )'=',      (char const   )'m',      (char const   )'a',      (char const   )'p', 
2708        (char const   )':',      (char const   )'D',      (char const   )'e',      (char const   )'s', 
2709        (char const   )'c',      (char const   )'r',      (char const   )'i',      (char const   )'b', 
2710        (char const   )'e',      (char const   )'s',      (char const   )' ',      (char const   )'f', 
2711        (char const   )'i',      (char const   )'r',      (char const   )'s',      (char const   )'t', 
2712        (char const   )' ',      (char const   )'s',      (char const   )'e',      (char const   )'t', 
2713        (char const   )' ',      (char const   )'o',      (char const   )'f',      (char const   )' ', 
2714        (char const   )'d',      (char const   )'e',      (char const   )'v',      (char const   )'i', 
2715        (char const   )'c',      (char const   )'e',      (char const   )'s',      (char const   )' ', 
2716        (char const   )'(',      (char const   )'<',      (char const   )'p',      (char const   )'a', 
2717        (char const   )'r',      (char const   )'p',      (char const   )'o',      (char const   )'r', 
2718        (char const   )'t',      (char const   )'#',      (char const   )'>',      (char const   )',', 
2719        (char const   )'<',      (char const   )'j',      (char const   )'s',      (char const   )'1', 
2720        (char const   )'>',      (char const   )',',      (char const   )'<',      (char const   )'j', 
2721        (char const   )'s',      (char const   )'2',      (char const   )'>',      (char const   )',', 
2722        (char const   )'.',      (char const   )'.',      (char const   )'<',      (char const   )'j', 
2723        (char const   )'s',      (char const   )'7',      (char const   )'>',      (char const   )'\000'};
2724#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2725static struct kparam_array  const  __param_arr_map2  =    {(unsigned int )(sizeof(tgfx_cfg[1].args) / sizeof(tgfx_cfg[1].args[0]) + sizeof(struct __anonstruct_226 )),
2726    (unsigned int )sizeof(tgfx_cfg[1].args[0]), & tgfx_cfg[1].nargs, (struct kernel_param_ops  const  *)(& param_ops_int),
2727    (void *)(tgfx_cfg[1].args)};
2728#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2729static char const   __param_str_map2[5]  = {      (char const   )'m',      (char const   )'a',      (char const   )'p',      (char const   )'2', 
2730        (char const   )'\000'};
2731#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2732static struct kernel_param  const  __param_map2  __attribute__((__used__, __unused__,
2733__section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_map2, (struct kernel_param_ops  const  *)(& param_array_ops), (u16 )0,
2734    (s16 )0, {.arr = & __param_arr_map2}};
2735#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2736static char const   __mod_map2type57[27]  __attribute__((__used__, __unused__, __section__(".modinfo"),
2737__aligned__(1)))  = 
2738#line 57
2739  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
2740        (char const   )'t',      (char const   )'y',      (char const   )'p',      (char const   )'e', 
2741        (char const   )'=',      (char const   )'m',      (char const   )'a',      (char const   )'p', 
2742        (char const   )'2',      (char const   )':',      (char const   )'a',      (char const   )'r', 
2743        (char const   )'r',      (char const   )'a',      (char const   )'y',      (char const   )' ', 
2744        (char const   )'o',      (char const   )'f',      (char const   )' ',      (char const   )'i', 
2745        (char const   )'n',      (char const   )'t',      (char const   )'\000'};
2746#line 58 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2747static char const   __mod_map258[42]  __attribute__((__used__, __unused__, __section__(".modinfo"),
2748__aligned__(1)))  = 
2749#line 58
2750  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
2751        (char const   )'=',      (char const   )'m',      (char const   )'a',      (char const   )'p', 
2752        (char const   )'2',      (char const   )':',      (char const   )'D',      (char const   )'e', 
2753        (char const   )'s',      (char const   )'c',      (char const   )'r',      (char const   )'i', 
2754        (char const   )'b',      (char const   )'e',      (char const   )'s',      (char const   )' ', 
2755        (char const   )'s',      (char const   )'e',      (char const   )'c',      (char const   )'o', 
2756        (char const   )'n',      (char const   )'d',      (char const   )' ',      (char const   )'s', 
2757        (char const   )'e',      (char const   )'t',      (char const   )' ',      (char const   )'o', 
2758        (char const   )'f',      (char const   )' ',      (char const   )'d',      (char const   )'e', 
2759        (char const   )'v',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
2760        (char const   )'s',      (char const   )'\000'};
2761#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2762static struct kparam_array  const  __param_arr_map3  =    {(unsigned int )(sizeof(tgfx_cfg[2].args) / sizeof(tgfx_cfg[2].args[0]) + sizeof(struct __anonstruct_229 )),
2763    (unsigned int )sizeof(tgfx_cfg[2].args[0]), & tgfx_cfg[2].nargs, (struct kernel_param_ops  const  *)(& param_ops_int),
2764    (void *)(tgfx_cfg[2].args)};
2765#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2766static char const   __param_str_map3[5]  = {      (char const   )'m',      (char const   )'a',      (char const   )'p',      (char const   )'3', 
2767        (char const   )'\000'};
2768#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2769static struct kernel_param  const  __param_map3  __attribute__((__used__, __unused__,
2770__section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_map3, (struct kernel_param_ops  const  *)(& param_array_ops), (u16 )0,
2771    (s16 )0, {.arr = & __param_arr_map3}};
2772#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2773static char const   __mod_map3type59[27]  __attribute__((__used__, __unused__, __section__(".modinfo"),
2774__aligned__(1)))  = 
2775#line 59
2776  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
2777        (char const   )'t',      (char const   )'y',      (char const   )'p',      (char const   )'e', 
2778        (char const   )'=',      (char const   )'m',      (char const   )'a',      (char const   )'p', 
2779        (char const   )'3',      (char const   )':',      (char const   )'a',      (char const   )'r', 
2780        (char const   )'r',      (char const   )'a',      (char const   )'y',      (char const   )' ', 
2781        (char const   )'o',      (char const   )'f',      (char const   )' ',      (char const   )'i', 
2782        (char const   )'n',      (char const   )'t',      (char const   )'\000'};
2783#line 60 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2784static char const   __mod_map360[41]  __attribute__((__used__, __unused__, __section__(".modinfo"),
2785__aligned__(1)))  = 
2786#line 60
2787  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
2788        (char const   )'=',      (char const   )'m',      (char const   )'a',      (char const   )'p', 
2789        (char const   )'3',      (char const   )':',      (char const   )'D',      (char const   )'e', 
2790        (char const   )'s',      (char const   )'c',      (char const   )'r',      (char const   )'i', 
2791        (char const   )'b',      (char const   )'e',      (char const   )'s',      (char const   )' ', 
2792        (char const   )'t',      (char const   )'h',      (char const   )'i',      (char const   )'r', 
2793        (char const   )'d',      (char const   )' ',      (char const   )'s',      (char const   )'e', 
2794        (char const   )'t',      (char const   )' ',      (char const   )'o',      (char const   )'f', 
2795        (char const   )' ',      (char const   )'d',      (char const   )'e',      (char const   )'v', 
2796        (char const   )'i',      (char const   )'c',      (char const   )'e',      (char const   )'s', 
2797        (char const   )'\000'};
2798#line 75 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2799static int tgfx_buttons[5]  = {      288,      289,      290,      291, 
2800        292};
2801#line 77 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2802static struct tgfx *tgfx_base[3]  ;
2803#line 92 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
2804static void tgfx_timer(unsigned long private ) 
2805{ struct tgfx *tgfx ;
2806  struct input_dev *dev ;
2807  int data1 ;
2808  int data2 ;
2809  int i ;
2810  unsigned char tmp ;
2811  unsigned char tmp___0 ;
2812  void *__cil_tmp9 ;
2813  int __cil_tmp10 ;
2814  unsigned long __cil_tmp11 ;
2815  unsigned long __cil_tmp12 ;
2816  int __cil_tmp13 ;
2817  unsigned long __cil_tmp14 ;
2818  unsigned long __cil_tmp15 ;
2819  unsigned long __cil_tmp16 ;
2820  unsigned long __cil_tmp17 ;
2821  struct pardevice *__cil_tmp18 ;
2822  unsigned long __cil_tmp19 ;
2823  unsigned long __cil_tmp20 ;
2824  struct parport *__cil_tmp21 ;
2825  unsigned long __cil_tmp22 ;
2826  unsigned long __cil_tmp23 ;
2827  struct parport_operations *__cil_tmp24 ;
2828  void (*__cil_tmp25)(struct parport * , unsigned char  ) ;
2829  struct pardevice *__cil_tmp26 ;
2830  unsigned long __cil_tmp27 ;
2831  unsigned long __cil_tmp28 ;
2832  struct parport *__cil_tmp29 ;
2833  int __cil_tmp30 ;
2834  int __cil_tmp31 ;
2835  unsigned char __cil_tmp32 ;
2836  struct pardevice *__cil_tmp33 ;
2837  unsigned long __cil_tmp34 ;
2838  unsigned long __cil_tmp35 ;
2839  struct parport *__cil_tmp36 ;
2840  unsigned long __cil_tmp37 ;
2841  unsigned long __cil_tmp38 ;
2842  struct parport_operations *__cil_tmp39 ;
2843  unsigned long __cil_tmp40 ;
2844  unsigned long __cil_tmp41 ;
2845  unsigned char (*__cil_tmp42)(struct parport * ) ;
2846  struct pardevice *__cil_tmp43 ;
2847  unsigned long __cil_tmp44 ;
2848  unsigned long __cil_tmp45 ;
2849  struct parport *__cil_tmp46 ;
2850  int __cil_tmp47 ;
2851  struct pardevice *__cil_tmp48 ;
2852  unsigned long __cil_tmp49 ;
2853  unsigned long __cil_tmp50 ;
2854  struct parport *__cil_tmp51 ;
2855  unsigned long __cil_tmp52 ;
2856  unsigned long __cil_tmp53 ;
2857  struct parport_operations *__cil_tmp54 ;
2858  unsigned long __cil_tmp55 ;
2859  unsigned long __cil_tmp56 ;
2860  unsigned char (*__cil_tmp57)(struct parport * ) ;
2861  struct pardevice *__cil_tmp58 ;
2862  unsigned long __cil_tmp59 ;
2863  unsigned long __cil_tmp60 ;
2864  struct parport *__cil_tmp61 ;
2865  int __cil_tmp62 ;
2866  int __cil_tmp63 ;
2867  int __cil_tmp64 ;
2868  int __cil_tmp65 ;
2869  int __cil_tmp66 ;
2870  int __cil_tmp67 ;
2871  int __cil_tmp68 ;
2872  int __cil_tmp69 ;
2873  int __cil_tmp70 ;
2874  int __cil_tmp71 ;
2875  int __cil_tmp72 ;
2876  int __cil_tmp73 ;
2877  int __cil_tmp74 ;
2878  int __cil_tmp75 ;
2879  int __cil_tmp76 ;
2880  int __cil_tmp77 ;
2881  int __cil_tmp78 ;
2882  int __cil_tmp79 ;
2883  int __cil_tmp80 ;
2884  int __cil_tmp81 ;
2885  unsigned long __cil_tmp82 ;
2886  unsigned long __cil_tmp83 ;
2887  struct timer_list *__cil_tmp84 ;
2888  unsigned long volatile   __cil_tmp85 ;
2889  unsigned long volatile   __cil_tmp86 ;
2890  unsigned long __cil_tmp87 ;
2891
2892  {
2893#line 94
2894  __cil_tmp9 = (void *)private;
2895#line 94
2896  tgfx = (struct tgfx *)__cil_tmp9;
2897#line 98
2898  i = 0;
2899  {
2900#line 98
2901  while (1) {
2902    while_continue: /* CIL Label */ ;
2903#line 98
2904    if (i < 7) {
2905
2906    } else {
2907#line 98
2908      goto while_break;
2909    }
2910    {
2911#line 99
2912    __cil_tmp10 = 1 << i;
2913#line 99
2914    __cil_tmp11 = (unsigned long )tgfx;
2915#line 99
2916    __cil_tmp12 = __cil_tmp11 + 816;
2917#line 99
2918    __cil_tmp13 = *((int *)__cil_tmp12);
2919#line 99
2920    if (__cil_tmp13 & __cil_tmp10) {
2921      {
2922#line 101
2923      __cil_tmp14 = i * 8UL;
2924#line 101
2925      __cil_tmp15 = 88 + __cil_tmp14;
2926#line 101
2927      __cil_tmp16 = (unsigned long )tgfx;
2928#line 101
2929      __cil_tmp17 = __cil_tmp16 + __cil_tmp15;
2930#line 101
2931      dev = *((struct input_dev **)__cil_tmp17);
2932#line 103
2933      __cil_tmp18 = *((struct pardevice **)tgfx);
2934#line 103
2935      __cil_tmp19 = (unsigned long )__cil_tmp18;
2936#line 103
2937      __cil_tmp20 = __cil_tmp19 + 8;
2938#line 103
2939      __cil_tmp21 = *((struct parport **)__cil_tmp20);
2940#line 103
2941      __cil_tmp22 = (unsigned long )__cil_tmp21;
2942#line 103
2943      __cil_tmp23 = __cil_tmp22 + 440;
2944#line 103
2945      __cil_tmp24 = *((struct parport_operations **)__cil_tmp23);
2946#line 103
2947      __cil_tmp25 = *((void (**)(struct parport * , unsigned char  ))__cil_tmp24);
2948#line 103
2949      __cil_tmp26 = *((struct pardevice **)tgfx);
2950#line 103
2951      __cil_tmp27 = (unsigned long )__cil_tmp26;
2952#line 103
2953      __cil_tmp28 = __cil_tmp27 + 8;
2954#line 103
2955      __cil_tmp29 = *((struct parport **)__cil_tmp28);
2956#line 103
2957      __cil_tmp30 = 1 << i;
2958#line 103
2959      __cil_tmp31 = ~ __cil_tmp30;
2960#line 103
2961      __cil_tmp32 = (unsigned char )__cil_tmp31;
2962#line 103
2963      (*__cil_tmp25)(__cil_tmp29, __cil_tmp32);
2964#line 104
2965      __cil_tmp33 = *((struct pardevice **)tgfx);
2966#line 104
2967      __cil_tmp34 = (unsigned long )__cil_tmp33;
2968#line 104
2969      __cil_tmp35 = __cil_tmp34 + 8;
2970#line 104
2971      __cil_tmp36 = *((struct parport **)__cil_tmp35);
2972#line 104
2973      __cil_tmp37 = (unsigned long )__cil_tmp36;
2974#line 104
2975      __cil_tmp38 = __cil_tmp37 + 440;
2976#line 104
2977      __cil_tmp39 = *((struct parport_operations **)__cil_tmp38);
2978#line 104
2979      __cil_tmp40 = (unsigned long )__cil_tmp39;
2980#line 104
2981      __cil_tmp41 = __cil_tmp40 + 40;
2982#line 104
2983      __cil_tmp42 = *((unsigned char (**)(struct parport * ))__cil_tmp41);
2984#line 104
2985      __cil_tmp43 = *((struct pardevice **)tgfx);
2986#line 104
2987      __cil_tmp44 = (unsigned long )__cil_tmp43;
2988#line 104
2989      __cil_tmp45 = __cil_tmp44 + 8;
2990#line 104
2991      __cil_tmp46 = *((struct parport **)__cil_tmp45);
2992#line 104
2993      tmp = (*__cil_tmp42)(__cil_tmp46);
2994#line 104
2995      __cil_tmp47 = (int )tmp;
2996#line 104
2997      data1 = __cil_tmp47 ^ 127;
2998#line 105
2999      __cil_tmp48 = *((struct pardevice **)tgfx);
3000#line 105
3001      __cil_tmp49 = (unsigned long )__cil_tmp48;
3002#line 105
3003      __cil_tmp50 = __cil_tmp49 + 8;
3004#line 105
3005      __cil_tmp51 = *((struct parport **)__cil_tmp50);
3006#line 105
3007      __cil_tmp52 = (unsigned long )__cil_tmp51;
3008#line 105
3009      __cil_tmp53 = __cil_tmp52 + 440;
3010#line 105
3011      __cil_tmp54 = *((struct parport_operations **)__cil_tmp53);
3012#line 105
3013      __cil_tmp55 = (unsigned long )__cil_tmp54;
3014#line 105
3015      __cil_tmp56 = __cil_tmp55 + 24;
3016#line 105
3017      __cil_tmp57 = *((unsigned char (**)(struct parport * ))__cil_tmp56);
3018#line 105
3019      __cil_tmp58 = *((struct pardevice **)tgfx);
3020#line 105
3021      __cil_tmp59 = (unsigned long )__cil_tmp58;
3022#line 105
3023      __cil_tmp60 = __cil_tmp59 + 8;
3024#line 105
3025      __cil_tmp61 = *((struct parport **)__cil_tmp60);
3026#line 105
3027      tmp___0 = (*__cil_tmp57)(__cil_tmp61);
3028#line 105
3029      __cil_tmp62 = (int )tmp___0;
3030#line 105
3031      data2 = __cil_tmp62 ^ 4;
3032#line 107
3033      __cil_tmp63 = data1 & 64;
3034#line 107
3035      __cil_tmp64 = ! __cil_tmp63;
3036#line 107
3037      __cil_tmp65 = ! __cil_tmp64;
3038#line 107
3039      __cil_tmp66 = data1 & 128;
3040#line 107
3041      __cil_tmp67 = ! __cil_tmp66;
3042#line 107
3043      __cil_tmp68 = ! __cil_tmp67;
3044#line 107
3045      __cil_tmp69 = __cil_tmp68 - __cil_tmp65;
3046#line 107
3047      input_report_abs(dev, 0U, __cil_tmp69);
3048#line 108
3049      __cil_tmp70 = data1 & 16;
3050#line 108
3051      __cil_tmp71 = ! __cil_tmp70;
3052#line 108
3053      __cil_tmp72 = ! __cil_tmp71;
3054#line 108
3055      __cil_tmp73 = data1 & 32;
3056#line 108
3057      __cil_tmp74 = ! __cil_tmp73;
3058#line 108
3059      __cil_tmp75 = ! __cil_tmp74;
3060#line 108
3061      __cil_tmp76 = __cil_tmp75 - __cil_tmp72;
3062#line 108
3063      input_report_abs(dev, 1U, __cil_tmp76);
3064#line 110
3065      __cil_tmp77 = data1 & 8;
3066#line 110
3067      input_report_key(dev, 288U, __cil_tmp77);
3068#line 111
3069      __cil_tmp78 = data2 & 2;
3070#line 111
3071      input_report_key(dev, 289U, __cil_tmp78);
3072#line 112
3073      __cil_tmp79 = data2 & 4;
3074#line 112
3075      input_report_key(dev, 290U, __cil_tmp79);
3076#line 113
3077      __cil_tmp80 = data2 & 1;
3078#line 113
3079      input_report_key(dev, 291U, __cil_tmp80);
3080#line 114
3081      __cil_tmp81 = data2 & 8;
3082#line 114
3083      input_report_key(dev, 292U, __cil_tmp81);
3084#line 116
3085      input_sync(dev);
3086      }
3087    } else {
3088
3089    }
3090    }
3091#line 98
3092    i = i + 1;
3093  }
3094  while_break: /* CIL Label */ ;
3095  }
3096  {
3097#line 119
3098  __cil_tmp82 = (unsigned long )tgfx;
3099#line 119
3100  __cil_tmp83 = __cil_tmp82 + 8;
3101#line 119
3102  __cil_tmp84 = (struct timer_list *)__cil_tmp83;
3103#line 119
3104  __cil_tmp85 = (unsigned long volatile   )2;
3105#line 119
3106  __cil_tmp86 = jiffies + __cil_tmp85;
3107#line 119
3108  __cil_tmp87 = (unsigned long )__cil_tmp86;
3109#line 119
3110  mod_timer(__cil_tmp84, __cil_tmp87);
3111  }
3112#line 120
3113  return;
3114}
3115}
3116#line 122 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
3117static int tgfx_open(struct input_dev *dev ) 
3118{ struct tgfx *tgfx ;
3119  void *tmp ;
3120  int err ;
3121  int tmp___0 ;
3122  unsigned long __cil_tmp6 ;
3123  unsigned long __cil_tmp7 ;
3124  struct mutex *__cil_tmp8 ;
3125  unsigned long __cil_tmp9 ;
3126  unsigned long __cil_tmp10 ;
3127  unsigned long __cil_tmp11 ;
3128  unsigned long __cil_tmp12 ;
3129  unsigned long __cil_tmp13 ;
3130  unsigned long __cil_tmp14 ;
3131  int __cil_tmp15 ;
3132  struct pardevice *__cil_tmp16 ;
3133  struct pardevice *__cil_tmp17 ;
3134  unsigned long __cil_tmp18 ;
3135  unsigned long __cil_tmp19 ;
3136  struct parport *__cil_tmp20 ;
3137  unsigned long __cil_tmp21 ;
3138  unsigned long __cil_tmp22 ;
3139  struct parport_operations *__cil_tmp23 ;
3140  unsigned long __cil_tmp24 ;
3141  unsigned long __cil_tmp25 ;
3142  void (*__cil_tmp26)(struct parport * , unsigned char  ) ;
3143  struct pardevice *__cil_tmp27 ;
3144  unsigned long __cil_tmp28 ;
3145  unsigned long __cil_tmp29 ;
3146  struct parport *__cil_tmp30 ;
3147  unsigned long __cil_tmp31 ;
3148  unsigned long __cil_tmp32 ;
3149  struct timer_list *__cil_tmp33 ;
3150  unsigned long volatile   __cil_tmp34 ;
3151  unsigned long volatile   __cil_tmp35 ;
3152  unsigned long __cil_tmp36 ;
3153  unsigned long __cil_tmp37 ;
3154  unsigned long __cil_tmp38 ;
3155  struct mutex *__cil_tmp39 ;
3156
3157  {
3158  {
3159#line 124
3160  tmp = input_get_drvdata(dev);
3161#line 124
3162  tgfx = (struct tgfx *)tmp;
3163#line 127
3164  __cil_tmp6 = (unsigned long )tgfx;
3165#line 127
3166  __cil_tmp7 = __cil_tmp6 + 824;
3167#line 127
3168  __cil_tmp8 = (struct mutex *)__cil_tmp7;
3169#line 127
3170  err = (int )mutex_lock_interruptible(__cil_tmp8);
3171  }
3172#line 128
3173  if (err) {
3174#line 129
3175    return (err);
3176  } else {
3177
3178  }
3179#line 131
3180  __cil_tmp9 = (unsigned long )tgfx;
3181#line 131
3182  __cil_tmp10 = __cil_tmp9 + 820;
3183#line 131
3184  tmp___0 = *((int *)__cil_tmp10);
3185#line 131
3186  __cil_tmp11 = (unsigned long )tgfx;
3187#line 131
3188  __cil_tmp12 = __cil_tmp11 + 820;
3189#line 131
3190  __cil_tmp13 = (unsigned long )tgfx;
3191#line 131
3192  __cil_tmp14 = __cil_tmp13 + 820;
3193#line 131
3194  __cil_tmp15 = *((int *)__cil_tmp14);
3195#line 131
3196  *((int *)__cil_tmp12) = __cil_tmp15 + 1;
3197#line 131
3198  if (tmp___0) {
3199
3200  } else {
3201    {
3202#line 132
3203    __cil_tmp16 = *((struct pardevice **)tgfx);
3204#line 132
3205    parport_claim(__cil_tmp16);
3206#line 133
3207    __cil_tmp17 = *((struct pardevice **)tgfx);
3208#line 133
3209    __cil_tmp18 = (unsigned long )__cil_tmp17;
3210#line 133
3211    __cil_tmp19 = __cil_tmp18 + 8;
3212#line 133
3213    __cil_tmp20 = *((struct parport **)__cil_tmp19);
3214#line 133
3215    __cil_tmp21 = (unsigned long )__cil_tmp20;
3216#line 133
3217    __cil_tmp22 = __cil_tmp21 + 440;
3218#line 133
3219    __cil_tmp23 = *((struct parport_operations **)__cil_tmp22);
3220#line 133
3221    __cil_tmp24 = (unsigned long )__cil_tmp23;
3222#line 133
3223    __cil_tmp25 = __cil_tmp24 + 16;
3224#line 133
3225    __cil_tmp26 = *((void (**)(struct parport * , unsigned char  ))__cil_tmp25);
3226#line 133
3227    __cil_tmp27 = *((struct pardevice **)tgfx);
3228#line 133
3229    __cil_tmp28 = (unsigned long )__cil_tmp27;
3230#line 133
3231    __cil_tmp29 = __cil_tmp28 + 8;
3232#line 133
3233    __cil_tmp30 = *((struct parport **)__cil_tmp29);
3234#line 133
3235    (*__cil_tmp26)(__cil_tmp30, (unsigned char)4);
3236#line 134
3237    __cil_tmp31 = (unsigned long )tgfx;
3238#line 134
3239    __cil_tmp32 = __cil_tmp31 + 8;
3240#line 134
3241    __cil_tmp33 = (struct timer_list *)__cil_tmp32;
3242#line 134
3243    __cil_tmp34 = (unsigned long volatile   )2;
3244#line 134
3245    __cil_tmp35 = jiffies + __cil_tmp34;
3246#line 134
3247    __cil_tmp36 = (unsigned long )__cil_tmp35;
3248#line 134
3249    mod_timer(__cil_tmp33, __cil_tmp36);
3250    }
3251  }
3252  {
3253#line 137
3254  __cil_tmp37 = (unsigned long )tgfx;
3255#line 137
3256  __cil_tmp38 = __cil_tmp37 + 824;
3257#line 137
3258  __cil_tmp39 = (struct mutex *)__cil_tmp38;
3259#line 137
3260  mutex_unlock(__cil_tmp39);
3261  }
3262#line 138
3263  return (0);
3264}
3265}
3266#line 141 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
3267static void tgfx_close(struct input_dev *dev ) 
3268{ struct tgfx *tgfx ;
3269  void *tmp ;
3270  unsigned long __cil_tmp4 ;
3271  unsigned long __cil_tmp5 ;
3272  struct mutex *__cil_tmp6 ;
3273  unsigned long __cil_tmp7 ;
3274  unsigned long __cil_tmp8 ;
3275  unsigned long __cil_tmp9 ;
3276  unsigned long __cil_tmp10 ;
3277  int __cil_tmp11 ;
3278  unsigned long __cil_tmp12 ;
3279  unsigned long __cil_tmp13 ;
3280  unsigned long __cil_tmp14 ;
3281  unsigned long __cil_tmp15 ;
3282  struct timer_list *__cil_tmp16 ;
3283  struct pardevice *__cil_tmp17 ;
3284  unsigned long __cil_tmp18 ;
3285  unsigned long __cil_tmp19 ;
3286  struct parport *__cil_tmp20 ;
3287  unsigned long __cil_tmp21 ;
3288  unsigned long __cil_tmp22 ;
3289  struct parport_operations *__cil_tmp23 ;
3290  unsigned long __cil_tmp24 ;
3291  unsigned long __cil_tmp25 ;
3292  void (*__cil_tmp26)(struct parport * , unsigned char  ) ;
3293  struct pardevice *__cil_tmp27 ;
3294  unsigned long __cil_tmp28 ;
3295  unsigned long __cil_tmp29 ;
3296  struct parport *__cil_tmp30 ;
3297  struct pardevice *__cil_tmp31 ;
3298  unsigned long __cil_tmp32 ;
3299  unsigned long __cil_tmp33 ;
3300  struct mutex *__cil_tmp34 ;
3301
3302  {
3303  {
3304#line 143
3305  tmp = input_get_drvdata(dev);
3306#line 143
3307  tgfx = (struct tgfx *)tmp;
3308#line 145
3309  __cil_tmp4 = (unsigned long )tgfx;
3310#line 145
3311  __cil_tmp5 = __cil_tmp4 + 824;
3312#line 145
3313  __cil_tmp6 = (struct mutex *)__cil_tmp5;
3314#line 145
3315  mutex_lock(__cil_tmp6);
3316#line 146
3317  __cil_tmp7 = (unsigned long )tgfx;
3318#line 146
3319  __cil_tmp8 = __cil_tmp7 + 820;
3320#line 146
3321  __cil_tmp9 = (unsigned long )tgfx;
3322#line 146
3323  __cil_tmp10 = __cil_tmp9 + 820;
3324#line 146
3325  __cil_tmp11 = *((int *)__cil_tmp10);
3326#line 146
3327  *((int *)__cil_tmp8) = __cil_tmp11 - 1;
3328  }
3329  {
3330#line 146
3331  __cil_tmp12 = (unsigned long )tgfx;
3332#line 146
3333  __cil_tmp13 = __cil_tmp12 + 820;
3334#line 146
3335  if (*((int *)__cil_tmp13)) {
3336
3337  } else {
3338    {
3339#line 147
3340    __cil_tmp14 = (unsigned long )tgfx;
3341#line 147
3342    __cil_tmp15 = __cil_tmp14 + 8;
3343#line 147
3344    __cil_tmp16 = (struct timer_list *)__cil_tmp15;
3345#line 147
3346    del_timer_sync(__cil_tmp16);
3347#line 148
3348    __cil_tmp17 = *((struct pardevice **)tgfx);
3349#line 148
3350    __cil_tmp18 = (unsigned long )__cil_tmp17;
3351#line 148
3352    __cil_tmp19 = __cil_tmp18 + 8;
3353#line 148
3354    __cil_tmp20 = *((struct parport **)__cil_tmp19);
3355#line 148
3356    __cil_tmp21 = (unsigned long )__cil_tmp20;
3357#line 148
3358    __cil_tmp22 = __cil_tmp21 + 440;
3359#line 148
3360    __cil_tmp23 = *((struct parport_operations **)__cil_tmp22);
3361#line 148
3362    __cil_tmp24 = (unsigned long )__cil_tmp23;
3363#line 148
3364    __cil_tmp25 = __cil_tmp24 + 16;
3365#line 148
3366    __cil_tmp26 = *((void (**)(struct parport * , unsigned char  ))__cil_tmp25);
3367#line 148
3368    __cil_tmp27 = *((struct pardevice **)tgfx);
3369#line 148
3370    __cil_tmp28 = (unsigned long )__cil_tmp27;
3371#line 148
3372    __cil_tmp29 = __cil_tmp28 + 8;
3373#line 148
3374    __cil_tmp30 = *((struct parport **)__cil_tmp29);
3375#line 148
3376    (*__cil_tmp26)(__cil_tmp30, (unsigned char)0);
3377#line 149
3378    __cil_tmp31 = *((struct pardevice **)tgfx);
3379#line 149
3380    parport_release(__cil_tmp31);
3381    }
3382  }
3383  }
3384  {
3385#line 151
3386  __cil_tmp32 = (unsigned long )tgfx;
3387#line 151
3388  __cil_tmp33 = __cil_tmp32 + 824;
3389#line 151
3390  __cil_tmp34 = (struct mutex *)__cil_tmp33;
3391#line 151
3392  mutex_unlock(__cil_tmp34);
3393  }
3394#line 152
3395  return;
3396}
3397}
3398#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
3399static struct lock_class_key __key___3  ;
3400#line 160
3401static struct tgfx *tgfx_probe(int parport , int *n_buttons , int n_devs )  __attribute__((__section__(".init.text"),
3402__no_instrument_function__)) ;
3403#line 160 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
3404static struct tgfx *tgfx_probe(int parport , int *n_buttons , int n_devs ) 
3405{ struct tgfx *tgfx ;
3406  struct input_dev *input_dev ;
3407  struct parport *pp ;
3408  struct pardevice *pd ;
3409  int i ;
3410  int j ;
3411  int err ;
3412  void *tmp ;
3413  void *tmp___0 ;
3414  void *__cil_tmp13 ;
3415  int (*__cil_tmp14)(void * ) ;
3416  void *__cil_tmp15 ;
3417  void (*__cil_tmp16)(void * ) ;
3418  void *__cil_tmp17 ;
3419  void (*__cil_tmp18)(void * ) ;
3420  int __cil_tmp19 ;
3421  void *__cil_tmp20 ;
3422  unsigned long __cil_tmp21 ;
3423  unsigned long __cil_tmp22 ;
3424  struct mutex *__cil_tmp23 ;
3425  unsigned long __cil_tmp24 ;
3426  unsigned long __cil_tmp25 ;
3427  struct timer_list *__cil_tmp26 ;
3428  void *__cil_tmp27 ;
3429  char const   *__cil_tmp28 ;
3430  void *__cil_tmp29 ;
3431  struct lock_class_key *__cil_tmp30 ;
3432  unsigned long __cil_tmp31 ;
3433  unsigned long __cil_tmp32 ;
3434  unsigned long __cil_tmp33 ;
3435  long __cil_tmp34 ;
3436  unsigned long __cil_tmp35 ;
3437  unsigned long __cil_tmp36 ;
3438  unsigned long __cil_tmp37 ;
3439  int *__cil_tmp38 ;
3440  int __cil_tmp39 ;
3441  int *__cil_tmp40 ;
3442  int __cil_tmp41 ;
3443  int *__cil_tmp42 ;
3444  int __cil_tmp43 ;
3445  unsigned long __cil_tmp44 ;
3446  unsigned long __cil_tmp45 ;
3447  unsigned long __cil_tmp46 ;
3448  unsigned long __cil_tmp47 ;
3449  unsigned long __cil_tmp48 ;
3450  unsigned long __cil_tmp49 ;
3451  int __cil_tmp50 ;
3452  unsigned long __cil_tmp51 ;
3453  unsigned long __cil_tmp52 ;
3454  int __cil_tmp53 ;
3455  unsigned long __cil_tmp54 ;
3456  unsigned long __cil_tmp55 ;
3457  unsigned long __cil_tmp56 ;
3458  unsigned long __cil_tmp57 ;
3459  unsigned long __cil_tmp58 ;
3460  unsigned long __cil_tmp59 ;
3461  char *__cil_tmp60 ;
3462  int *__cil_tmp61 ;
3463  int __cil_tmp62 ;
3464  unsigned long __cil_tmp63 ;
3465  unsigned long __cil_tmp64 ;
3466  unsigned long __cil_tmp65 ;
3467  unsigned long __cil_tmp66 ;
3468  unsigned long __cil_tmp67 ;
3469  unsigned long __cil_tmp68 ;
3470  char *__cil_tmp69 ;
3471  struct pardevice *__cil_tmp70 ;
3472  unsigned long __cil_tmp71 ;
3473  unsigned long __cil_tmp72 ;
3474  struct parport *__cil_tmp73 ;
3475  unsigned long __cil_tmp74 ;
3476  unsigned long __cil_tmp75 ;
3477  char const   *__cil_tmp76 ;
3478  unsigned long __cil_tmp77 ;
3479  unsigned long __cil_tmp78 ;
3480  unsigned long __cil_tmp79 ;
3481  unsigned long __cil_tmp80 ;
3482  unsigned long __cil_tmp81 ;
3483  unsigned long __cil_tmp82 ;
3484  char *__cil_tmp83 ;
3485  unsigned long __cil_tmp84 ;
3486  unsigned long __cil_tmp85 ;
3487  unsigned long __cil_tmp86 ;
3488  unsigned long __cil_tmp87 ;
3489  unsigned long __cil_tmp88 ;
3490  unsigned long __cil_tmp89 ;
3491  unsigned long __cil_tmp90 ;
3492  unsigned long __cil_tmp91 ;
3493  char *__cil_tmp92 ;
3494  unsigned long __cil_tmp93 ;
3495  unsigned long __cil_tmp94 ;
3496  unsigned long __cil_tmp95 ;
3497  unsigned long __cil_tmp96 ;
3498  unsigned long __cil_tmp97 ;
3499  unsigned long __cil_tmp98 ;
3500  unsigned long __cil_tmp99 ;
3501  unsigned long __cil_tmp100 ;
3502  int *__cil_tmp101 ;
3503  int __cil_tmp102 ;
3504  unsigned long __cil_tmp103 ;
3505  unsigned long __cil_tmp104 ;
3506  unsigned long __cil_tmp105 ;
3507  void *__cil_tmp106 ;
3508  unsigned long __cil_tmp107 ;
3509  unsigned long __cil_tmp108 ;
3510  unsigned long __cil_tmp109 ;
3511  unsigned long __cil_tmp110 ;
3512  unsigned long __cil_tmp111 ;
3513  unsigned long __cil_tmp112 ;
3514  unsigned long __cil_tmp113 ;
3515  unsigned long __cil_tmp114 ;
3516  unsigned long __cil_tmp115 ;
3517  unsigned long __cil_tmp116 ;
3518  int *__cil_tmp117 ;
3519  int __cil_tmp118 ;
3520  unsigned long __cil_tmp119 ;
3521  unsigned long __cil_tmp120 ;
3522  int __cil_tmp121 ;
3523  unsigned int __cil_tmp122 ;
3524  unsigned long __cil_tmp123 ;
3525  unsigned long __cil_tmp124 ;
3526  unsigned long __cil_tmp125 ;
3527  unsigned long __cil_tmp126 ;
3528  unsigned long *__cil_tmp127 ;
3529  unsigned long volatile   *__cil_tmp128 ;
3530  unsigned long __cil_tmp129 ;
3531  unsigned long __cil_tmp130 ;
3532  unsigned long __cil_tmp131 ;
3533  unsigned long __cil_tmp132 ;
3534  struct input_dev *__cil_tmp133 ;
3535  unsigned long __cil_tmp134 ;
3536  unsigned long __cil_tmp135 ;
3537  int __cil_tmp136 ;
3538  unsigned long __cil_tmp137 ;
3539  unsigned long __cil_tmp138 ;
3540  unsigned long __cil_tmp139 ;
3541  unsigned long __cil_tmp140 ;
3542  struct input_dev *__cil_tmp141 ;
3543  unsigned long __cil_tmp142 ;
3544  unsigned long __cil_tmp143 ;
3545  unsigned long __cil_tmp144 ;
3546  unsigned long __cil_tmp145 ;
3547  unsigned long __cil_tmp146 ;
3548  unsigned long __cil_tmp147 ;
3549  unsigned long __cil_tmp148 ;
3550  unsigned long __cil_tmp149 ;
3551  struct input_dev *__cil_tmp150 ;
3552  void const   *__cil_tmp151 ;
3553  long __cil_tmp152 ;
3554
3555  {
3556  {
3557#line 169
3558  pp = parport_find_number(parport);
3559  }
3560#line 170
3561  if (! pp) {
3562    {
3563#line 171
3564    printk("<3>turbografx.c: no such parport\n");
3565#line 172
3566    err = -22;
3567    }
3568#line 173
3569    goto err_out;
3570  } else {
3571
3572  }
3573  {
3574#line 176
3575  __cil_tmp13 = (void *)0;
3576#line 176
3577  __cil_tmp14 = (int (*)(void * ))__cil_tmp13;
3578#line 176
3579  __cil_tmp15 = (void *)0;
3580#line 176
3581  __cil_tmp16 = (void (*)(void * ))__cil_tmp15;
3582#line 176
3583  __cil_tmp17 = (void *)0;
3584#line 176
3585  __cil_tmp18 = (void (*)(void * ))__cil_tmp17;
3586#line 176
3587  __cil_tmp19 = 1 << 1;
3588#line 176
3589  __cil_tmp20 = (void *)0;
3590#line 176
3591  pd = parport_register_device(pp, "turbografx", __cil_tmp14, __cil_tmp16, __cil_tmp18,
3592                               __cil_tmp19, __cil_tmp20);
3593  }
3594#line 177
3595  if (! pd) {
3596    {
3597#line 178
3598    printk("<3>turbografx.c: parport busy already - lp.o loaded?\n");
3599#line 179
3600    err = -16;
3601    }
3602#line 180
3603    goto err_put_pp;
3604  } else {
3605
3606  }
3607  {
3608#line 183
3609  tmp = kzalloc(896UL, 208U);
3610#line 183
3611  tgfx = (struct tgfx *)tmp;
3612  }
3613#line 184
3614  if (! tgfx) {
3615    {
3616#line 185
3617    printk("<3>turbografx.c: Not enough memory\n");
3618#line 186
3619    err = -12;
3620    }
3621#line 187
3622    goto err_unreg_pardev;
3623  } else {
3624
3625  }
3626  {
3627#line 190
3628  while (1) {
3629    while_continue: /* CIL Label */ ;
3630    {
3631#line 190
3632    __cil_tmp21 = (unsigned long )tgfx;
3633#line 190
3634    __cil_tmp22 = __cil_tmp21 + 824;
3635#line 190
3636    __cil_tmp23 = (struct mutex *)__cil_tmp22;
3637#line 190
3638    __mutex_init(__cil_tmp23, "&tgfx->sem", & __key___3);
3639    }
3640#line 190
3641    goto while_break;
3642  }
3643  while_break: /* CIL Label */ ;
3644  }
3645  {
3646#line 191
3647  *((struct pardevice **)tgfx) = pd;
3648#line 192
3649  __cil_tmp24 = (unsigned long )tgfx;
3650#line 192
3651  __cil_tmp25 = __cil_tmp24 + 8;
3652#line 192
3653  __cil_tmp26 = (struct timer_list *)__cil_tmp25;
3654#line 192
3655  __cil_tmp27 = (void *)0;
3656#line 192
3657  __cil_tmp28 = (char const   *)__cil_tmp27;
3658#line 192
3659  __cil_tmp29 = (void *)0;
3660#line 192
3661  __cil_tmp30 = (struct lock_class_key *)__cil_tmp29;
3662#line 192
3663  init_timer_key(__cil_tmp26, __cil_tmp28, __cil_tmp30);
3664#line 193
3665  __cil_tmp31 = 8 + 40;
3666#line 193
3667  __cil_tmp32 = (unsigned long )tgfx;
3668#line 193
3669  __cil_tmp33 = __cil_tmp32 + __cil_tmp31;
3670#line 193
3671  __cil_tmp34 = (long )tgfx;
3672#line 193
3673  *((unsigned long *)__cil_tmp33) = (unsigned long )__cil_tmp34;
3674#line 194
3675  __cil_tmp35 = 8 + 32;
3676#line 194
3677  __cil_tmp36 = (unsigned long )tgfx;
3678#line 194
3679  __cil_tmp37 = __cil_tmp36 + __cil_tmp35;
3680#line 194
3681  *((void (**)(unsigned long  ))__cil_tmp37) = & tgfx_timer;
3682#line 196
3683  i = 0;
3684  }
3685  {
3686#line 196
3687  while (1) {
3688    while_continue___0: /* CIL Label */ ;
3689#line 196
3690    if (i < n_devs) {
3691
3692    } else {
3693#line 196
3694      goto while_break___0;
3695    }
3696    {
3697#line 197
3698    __cil_tmp38 = n_buttons + i;
3699#line 197
3700    __cil_tmp39 = *__cil_tmp38;
3701#line 197
3702    if (__cil_tmp39 < 1) {
3703#line 198
3704      goto __Cont;
3705    } else {
3706
3707    }
3708    }
3709    {
3710#line 200
3711    __cil_tmp40 = n_buttons + i;
3712#line 200
3713    __cil_tmp41 = *__cil_tmp40;
3714#line 200
3715    if (__cil_tmp41 > 6) {
3716      {
3717#line 201
3718      __cil_tmp42 = n_buttons + i;
3719#line 201
3720      __cil_tmp43 = *__cil_tmp42;
3721#line 201
3722      printk("<3>turbografx.c: Invalid number of buttons %d\n", __cil_tmp43);
3723#line 202
3724      err = -22;
3725      }
3726#line 203
3727      goto err_unreg_devs;
3728    } else {
3729
3730    }
3731    }
3732    {
3733#line 206
3734    input_dev = input_allocate_device();
3735#line 206
3736    __cil_tmp44 = i * 8UL;
3737#line 206
3738    __cil_tmp45 = 88 + __cil_tmp44;
3739#line 206
3740    __cil_tmp46 = (unsigned long )tgfx;
3741#line 206
3742    __cil_tmp47 = __cil_tmp46 + __cil_tmp45;
3743#line 206
3744    *((struct input_dev **)__cil_tmp47) = input_dev;
3745    }
3746#line 207
3747    if (! input_dev) {
3748      {
3749#line 208
3750      printk("<3>turbografx.c: Not enough memory for input device\n");
3751#line 209
3752      err = -12;
3753      }
3754#line 210
3755      goto err_unreg_devs;
3756    } else {
3757
3758    }
3759    {
3760#line 213
3761    __cil_tmp48 = (unsigned long )tgfx;
3762#line 213
3763    __cil_tmp49 = __cil_tmp48 + 816;
3764#line 213
3765    __cil_tmp50 = 1 << i;
3766#line 213
3767    __cil_tmp51 = (unsigned long )tgfx;
3768#line 213
3769    __cil_tmp52 = __cil_tmp51 + 816;
3770#line 213
3771    __cil_tmp53 = *((int *)__cil_tmp52);
3772#line 213
3773    *((int *)__cil_tmp49) = __cil_tmp53 | __cil_tmp50;
3774#line 214
3775    __cil_tmp54 = 0 * 1UL;
3776#line 214
3777    __cil_tmp55 = i * 64UL;
3778#line 214
3779    __cil_tmp56 = __cil_tmp55 + __cil_tmp54;
3780#line 214
3781    __cil_tmp57 = 144 + __cil_tmp56;
3782#line 214
3783    __cil_tmp58 = (unsigned long )tgfx;
3784#line 214
3785    __cil_tmp59 = __cil_tmp58 + __cil_tmp57;
3786#line 214
3787    __cil_tmp60 = (char *)__cil_tmp59;
3788#line 214
3789    __cil_tmp61 = n_buttons + i;
3790#line 214
3791    __cil_tmp62 = *__cil_tmp61;
3792#line 214
3793    snprintf(__cil_tmp60, 64UL, "TurboGraFX %d-button Multisystem joystick", __cil_tmp62);
3794#line 216
3795    __cil_tmp63 = 0 * 1UL;
3796#line 216
3797    __cil_tmp64 = i * 32UL;
3798#line 216
3799    __cil_tmp65 = __cil_tmp64 + __cil_tmp63;
3800#line 216
3801    __cil_tmp66 = 592 + __cil_tmp65;
3802#line 216
3803    __cil_tmp67 = (unsigned long )tgfx;
3804#line 216
3805    __cil_tmp68 = __cil_tmp67 + __cil_tmp66;
3806#line 216
3807    __cil_tmp69 = (char *)__cil_tmp68;
3808#line 216
3809    __cil_tmp70 = *((struct pardevice **)tgfx);
3810#line 216
3811    __cil_tmp71 = (unsigned long )__cil_tmp70;
3812#line 216
3813    __cil_tmp72 = __cil_tmp71 + 8;
3814#line 216
3815    __cil_tmp73 = *((struct parport **)__cil_tmp72);
3816#line 216
3817    __cil_tmp74 = (unsigned long )__cil_tmp73;
3818#line 216
3819    __cil_tmp75 = __cil_tmp74 + 24;
3820#line 216
3821    __cil_tmp76 = *((char const   **)__cil_tmp75);
3822#line 216
3823    snprintf(__cil_tmp69, 32UL, "%s/input%d", __cil_tmp76, i);
3824#line 219
3825    __cil_tmp77 = 0 * 1UL;
3826#line 219
3827    __cil_tmp78 = i * 64UL;
3828#line 219
3829    __cil_tmp79 = __cil_tmp78 + __cil_tmp77;
3830#line 219
3831    __cil_tmp80 = 144 + __cil_tmp79;
3832#line 219
3833    __cil_tmp81 = (unsigned long )tgfx;
3834#line 219
3835    __cil_tmp82 = __cil_tmp81 + __cil_tmp80;
3836#line 219
3837    __cil_tmp83 = (char *)__cil_tmp82;
3838#line 219
3839    *((char const   **)input_dev) = (char const   *)__cil_tmp83;
3840#line 220
3841    __cil_tmp84 = (unsigned long )input_dev;
3842#line 220
3843    __cil_tmp85 = __cil_tmp84 + 8;
3844#line 220
3845    __cil_tmp86 = 0 * 1UL;
3846#line 220
3847    __cil_tmp87 = i * 32UL;
3848#line 220
3849    __cil_tmp88 = __cil_tmp87 + __cil_tmp86;
3850#line 220
3851    __cil_tmp89 = 592 + __cil_tmp88;
3852#line 220
3853    __cil_tmp90 = (unsigned long )tgfx;
3854#line 220
3855    __cil_tmp91 = __cil_tmp90 + __cil_tmp89;
3856#line 220
3857    __cil_tmp92 = (char *)__cil_tmp91;
3858#line 220
3859    *((char const   **)__cil_tmp85) = (char const   *)__cil_tmp92;
3860#line 221
3861    __cil_tmp93 = (unsigned long )input_dev;
3862#line 221
3863    __cil_tmp94 = __cil_tmp93 + 24;
3864#line 221
3865    *((__u16 *)__cil_tmp94) = (__u16 )21;
3866#line 222
3867    __cil_tmp95 = 24 + 2;
3868#line 222
3869    __cil_tmp96 = (unsigned long )input_dev;
3870#line 222
3871    __cil_tmp97 = __cil_tmp96 + __cil_tmp95;
3872#line 222
3873    *((__u16 *)__cil_tmp97) = (__u16 )3;
3874#line 223
3875    __cil_tmp98 = 24 + 4;
3876#line 223
3877    __cil_tmp99 = (unsigned long )input_dev;
3878#line 223
3879    __cil_tmp100 = __cil_tmp99 + __cil_tmp98;
3880#line 223
3881    __cil_tmp101 = n_buttons + i;
3882#line 223
3883    __cil_tmp102 = *__cil_tmp101;
3884#line 223
3885    *((__u16 *)__cil_tmp100) = (__u16 )__cil_tmp102;
3886#line 224
3887    __cil_tmp103 = 24 + 6;
3888#line 224
3889    __cil_tmp104 = (unsigned long )input_dev;
3890#line 224
3891    __cil_tmp105 = __cil_tmp104 + __cil_tmp103;
3892#line 224
3893    *((__u16 *)__cil_tmp105) = (__u16 )256;
3894#line 226
3895    __cil_tmp106 = (void *)tgfx;
3896#line 226
3897    input_set_drvdata(input_dev, __cil_tmp106);
3898#line 228
3899    __cil_tmp107 = (unsigned long )input_dev;
3900#line 228
3901    __cil_tmp108 = __cil_tmp107 + 504;
3902#line 228
3903    *((int (**)(struct input_dev *dev ))__cil_tmp108) = & tgfx_open;
3904#line 229
3905    __cil_tmp109 = (unsigned long )input_dev;
3906#line 229
3907    __cil_tmp110 = __cil_tmp109 + 512;
3908#line 229
3909    *((void (**)(struct input_dev *dev ))__cil_tmp110) = & tgfx_close;
3910#line 231
3911    __cil_tmp111 = 0 * 8UL;
3912#line 231
3913    __cil_tmp112 = 40 + __cil_tmp111;
3914#line 231
3915    __cil_tmp113 = (unsigned long )input_dev;
3916#line 231
3917    __cil_tmp114 = __cil_tmp113 + __cil_tmp112;
3918#line 231
3919    __cil_tmp115 = 1UL << 3;
3920#line 231
3921    __cil_tmp116 = 1UL << 1;
3922#line 231
3923    *((unsigned long *)__cil_tmp114) = __cil_tmp116 | __cil_tmp115;
3924#line 232
3925    input_set_abs_params(input_dev, 0U, -1, 1, 0, 0);
3926#line 233
3927    input_set_abs_params(input_dev, 1U, -1, 1, 0, 0);
3928#line 235
3929    j = 0;
3930    }
3931    {
3932#line 235
3933    while (1) {
3934      while_continue___1: /* CIL Label */ ;
3935      {
3936#line 235
3937      __cil_tmp117 = n_buttons + i;
3938#line 235
3939      __cil_tmp118 = *__cil_tmp117;
3940#line 235
3941      if (j < __cil_tmp118) {
3942
3943      } else {
3944#line 235
3945        goto while_break___1;
3946      }
3947      }
3948      {
3949#line 236
3950      __cil_tmp119 = j * 4UL;
3951#line 236
3952      __cil_tmp120 = (unsigned long )(tgfx_buttons) + __cil_tmp119;
3953#line 236
3954      __cil_tmp121 = *((int *)__cil_tmp120);
3955#line 236
3956      __cil_tmp122 = (unsigned int )__cil_tmp121;
3957#line 236
3958      __cil_tmp123 = 0 * 8UL;
3959#line 236
3960      __cil_tmp124 = 48 + __cil_tmp123;
3961#line 236
3962      __cil_tmp125 = (unsigned long )input_dev;
3963#line 236
3964      __cil_tmp126 = __cil_tmp125 + __cil_tmp124;
3965#line 236
3966      __cil_tmp127 = (unsigned long *)__cil_tmp126;
3967#line 236
3968      __cil_tmp128 = (unsigned long volatile   *)__cil_tmp127;
3969#line 236
3970      set_bit(__cil_tmp122, __cil_tmp128);
3971#line 235
3972      j = j + 1;
3973      }
3974    }
3975    while_break___1: /* CIL Label */ ;
3976    }
3977    {
3978#line 238
3979    __cil_tmp129 = i * 8UL;
3980#line 238
3981    __cil_tmp130 = 88 + __cil_tmp129;
3982#line 238
3983    __cil_tmp131 = (unsigned long )tgfx;
3984#line 238
3985    __cil_tmp132 = __cil_tmp131 + __cil_tmp130;
3986#line 238
3987    __cil_tmp133 = *((struct input_dev **)__cil_tmp132);
3988#line 238
3989    err = (int )input_register_device(__cil_tmp133);
3990    }
3991#line 239
3992    if (err) {
3993#line 240
3994      goto err_free_dev;
3995    } else {
3996
3997    }
3998    __Cont: /* CIL Label */ 
3999#line 196
4000    i = i + 1;
4001  }
4002  while_break___0: /* CIL Label */ ;
4003  }
4004  {
4005#line 243
4006  __cil_tmp134 = (unsigned long )tgfx;
4007#line 243
4008  __cil_tmp135 = __cil_tmp134 + 816;
4009#line 243
4010  __cil_tmp136 = *((int *)__cil_tmp135);
4011#line 243
4012  if (! __cil_tmp136) {
4013    {
4014#line 244
4015    printk("<3>turbografx.c: No valid devices specified\n");
4016#line 245
4017    err = -22;
4018    }
4019#line 246
4020    goto err_free_tgfx;
4021  } else {
4022
4023  }
4024  }
4025  {
4026#line 249
4027  parport_put_port(pp);
4028  }
4029#line 250
4030  return (tgfx);
4031  err_free_dev: 
4032  {
4033#line 253
4034  __cil_tmp137 = i * 8UL;
4035#line 253
4036  __cil_tmp138 = 88 + __cil_tmp137;
4037#line 253
4038  __cil_tmp139 = (unsigned long )tgfx;
4039#line 253
4040  __cil_tmp140 = __cil_tmp139 + __cil_tmp138;
4041#line 253
4042  __cil_tmp141 = *((struct input_dev **)__cil_tmp140);
4043#line 253
4044  input_free_device(__cil_tmp141);
4045  }
4046  err_unreg_devs: 
4047  {
4048#line 255
4049  while (1) {
4050    while_continue___2: /* CIL Label */ ;
4051#line 255
4052    i = i - 1;
4053#line 255
4054    if (i >= 0) {
4055
4056    } else {
4057#line 255
4058      goto while_break___2;
4059    }
4060    {
4061#line 256
4062    __cil_tmp142 = i * 8UL;
4063#line 256
4064    __cil_tmp143 = 88 + __cil_tmp142;
4065#line 256
4066    __cil_tmp144 = (unsigned long )tgfx;
4067#line 256
4068    __cil_tmp145 = __cil_tmp144 + __cil_tmp143;
4069#line 256
4070    if (*((struct input_dev **)__cil_tmp145)) {
4071      {
4072#line 257
4073      __cil_tmp146 = i * 8UL;
4074#line 257
4075      __cil_tmp147 = 88 + __cil_tmp146;
4076#line 257
4077      __cil_tmp148 = (unsigned long )tgfx;
4078#line 257
4079      __cil_tmp149 = __cil_tmp148 + __cil_tmp147;
4080#line 257
4081      __cil_tmp150 = *((struct input_dev **)__cil_tmp149);
4082#line 257
4083      input_unregister_device(__cil_tmp150);
4084      }
4085    } else {
4086
4087    }
4088    }
4089  }
4090  while_break___2: /* CIL Label */ ;
4091  }
4092  err_free_tgfx: 
4093  {
4094#line 259
4095  __cil_tmp151 = (void const   *)tgfx;
4096#line 259
4097  kfree(__cil_tmp151);
4098  }
4099  err_unreg_pardev: 
4100  {
4101#line 261
4102  parport_unregister_device(pd);
4103  }
4104  err_put_pp: 
4105  {
4106#line 263
4107  parport_put_port(pp);
4108  }
4109  err_out: 
4110  {
4111#line 265
4112  __cil_tmp152 = (long )err;
4113#line 265
4114  tmp___0 = (void *)ERR_PTR(__cil_tmp152);
4115  }
4116#line 265
4117  return ((struct tgfx *)tmp___0);
4118}
4119}
4120#line 268 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
4121static void tgfx_remove(struct tgfx *tgfx ) 
4122{ int i ;
4123  unsigned long __cil_tmp3 ;
4124  unsigned long __cil_tmp4 ;
4125  unsigned long __cil_tmp5 ;
4126  unsigned long __cil_tmp6 ;
4127  unsigned long __cil_tmp7 ;
4128  unsigned long __cil_tmp8 ;
4129  unsigned long __cil_tmp9 ;
4130  unsigned long __cil_tmp10 ;
4131  struct input_dev *__cil_tmp11 ;
4132  struct pardevice *__cil_tmp12 ;
4133  void const   *__cil_tmp13 ;
4134
4135  {
4136#line 272
4137  i = 0;
4138  {
4139#line 272
4140  while (1) {
4141    while_continue: /* CIL Label */ ;
4142#line 272
4143    if (i < 7) {
4144
4145    } else {
4146#line 272
4147      goto while_break;
4148    }
4149    {
4150#line 273
4151    __cil_tmp3 = i * 8UL;
4152#line 273
4153    __cil_tmp4 = 88 + __cil_tmp3;
4154#line 273
4155    __cil_tmp5 = (unsigned long )tgfx;
4156#line 273
4157    __cil_tmp6 = __cil_tmp5 + __cil_tmp4;
4158#line 273
4159    if (*((struct input_dev **)__cil_tmp6)) {
4160      {
4161#line 274
4162      __cil_tmp7 = i * 8UL;
4163#line 274
4164      __cil_tmp8 = 88 + __cil_tmp7;
4165#line 274
4166      __cil_tmp9 = (unsigned long )tgfx;
4167#line 274
4168      __cil_tmp10 = __cil_tmp9 + __cil_tmp8;
4169#line 274
4170      __cil_tmp11 = *((struct input_dev **)__cil_tmp10);
4171#line 274
4172      input_unregister_device(__cil_tmp11);
4173      }
4174    } else {
4175
4176    }
4177    }
4178#line 272
4179    i = i + 1;
4180  }
4181  while_break: /* CIL Label */ ;
4182  }
4183  {
4184#line 275
4185  __cil_tmp12 = *((struct pardevice **)tgfx);
4186#line 275
4187  parport_unregister_device(__cil_tmp12);
4188#line 276
4189  __cil_tmp13 = (void const   *)tgfx;
4190#line 276
4191  kfree(__cil_tmp13);
4192  }
4193#line 277
4194  return;
4195}
4196}
4197#line 279
4198static int tgfx_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
4199#line 279 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
4200static int tgfx_init(void) 
4201{ int i ;
4202  int have_dev ;
4203  int err ;
4204  long tmp ;
4205  long tmp___0 ;
4206  int tmp___1 ;
4207  unsigned long __cil_tmp7 ;
4208  unsigned long __cil_tmp8 ;
4209  unsigned long __cil_tmp9 ;
4210  unsigned int __cil_tmp10 ;
4211  unsigned long __cil_tmp11 ;
4212  unsigned long __cil_tmp12 ;
4213  unsigned long __cil_tmp13 ;
4214  unsigned long __cil_tmp14 ;
4215  unsigned long __cil_tmp15 ;
4216  int __cil_tmp16 ;
4217  unsigned long __cil_tmp17 ;
4218  unsigned long __cil_tmp18 ;
4219  unsigned long __cil_tmp19 ;
4220  unsigned int __cil_tmp20 ;
4221  unsigned long __cil_tmp21 ;
4222  unsigned long __cil_tmp22 ;
4223  unsigned long __cil_tmp23 ;
4224  unsigned long __cil_tmp24 ;
4225  unsigned long __cil_tmp25 ;
4226  unsigned long __cil_tmp26 ;
4227  unsigned long __cil_tmp27 ;
4228  int __cil_tmp28 ;
4229  unsigned long __cil_tmp29 ;
4230  unsigned long __cil_tmp30 ;
4231  unsigned long __cil_tmp31 ;
4232  unsigned long __cil_tmp32 ;
4233  unsigned long __cil_tmp33 ;
4234  int *__cil_tmp34 ;
4235  int *__cil_tmp35 ;
4236  unsigned long __cil_tmp36 ;
4237  unsigned long __cil_tmp37 ;
4238  unsigned long __cil_tmp38 ;
4239  unsigned int __cil_tmp39 ;
4240  unsigned int __cil_tmp40 ;
4241  int __cil_tmp41 ;
4242  unsigned long __cil_tmp42 ;
4243  unsigned long __cil_tmp43 ;
4244  struct tgfx *__cil_tmp44 ;
4245  void const   *__cil_tmp45 ;
4246  unsigned long __cil_tmp46 ;
4247  unsigned long __cil_tmp47 ;
4248  struct tgfx *__cil_tmp48 ;
4249  void const   *__cil_tmp49 ;
4250  unsigned long __cil_tmp50 ;
4251  unsigned long __cil_tmp51 ;
4252  unsigned long __cil_tmp52 ;
4253  unsigned long __cil_tmp53 ;
4254  struct tgfx *__cil_tmp54 ;
4255
4256  {
4257#line 282
4258  have_dev = 0;
4259#line 283
4260  err = 0;
4261#line 285
4262  i = 0;
4263  {
4264#line 285
4265  while (1) {
4266    while_continue: /* CIL Label */ ;
4267#line 285
4268    if (i < 3) {
4269
4270    } else {
4271#line 285
4272      goto while_break;
4273    }
4274    {
4275#line 286
4276    __cil_tmp7 = i * 36UL;
4277#line 286
4278    __cil_tmp8 = __cil_tmp7 + 32;
4279#line 286
4280    __cil_tmp9 = (unsigned long )(tgfx_cfg) + __cil_tmp8;
4281#line 286
4282    __cil_tmp10 = *((unsigned int *)__cil_tmp9);
4283#line 286
4284    if (__cil_tmp10 == 0U) {
4285#line 287
4286      goto __Cont;
4287    } else {
4288      {
4289#line 286
4290      __cil_tmp11 = 0 * 4UL;
4291#line 286
4292      __cil_tmp12 = 0 + __cil_tmp11;
4293#line 286
4294      __cil_tmp13 = i * 36UL;
4295#line 286
4296      __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
4297#line 286
4298      __cil_tmp15 = (unsigned long )(tgfx_cfg) + __cil_tmp14;
4299#line 286
4300      __cil_tmp16 = *((int *)__cil_tmp15);
4301#line 286
4302      if (__cil_tmp16 < 0) {
4303#line 287
4304        goto __Cont;
4305      } else {
4306
4307      }
4308      }
4309    }
4310    }
4311    {
4312#line 289
4313    __cil_tmp17 = i * 36UL;
4314#line 289
4315    __cil_tmp18 = __cil_tmp17 + 32;
4316#line 289
4317    __cil_tmp19 = (unsigned long )(tgfx_cfg) + __cil_tmp18;
4318#line 289
4319    __cil_tmp20 = *((unsigned int *)__cil_tmp19);
4320#line 289
4321    if (__cil_tmp20 < 2U) {
4322      {
4323#line 290
4324      printk("<3>turbografx.c: at least one joystick must be specified\n");
4325#line 291
4326      err = -22;
4327      }
4328#line 292
4329      goto while_break;
4330    } else {
4331
4332    }
4333    }
4334    {
4335#line 295
4336    __cil_tmp21 = i * 8UL;
4337#line 295
4338    __cil_tmp22 = (unsigned long )(tgfx_base) + __cil_tmp21;
4339#line 295
4340    __cil_tmp23 = 0 * 4UL;
4341#line 295
4342    __cil_tmp24 = 0 + __cil_tmp23;
4343#line 295
4344    __cil_tmp25 = i * 36UL;
4345#line 295
4346    __cil_tmp26 = __cil_tmp25 + __cil_tmp24;
4347#line 295
4348    __cil_tmp27 = (unsigned long )(tgfx_cfg) + __cil_tmp26;
4349#line 295
4350    __cil_tmp28 = *((int *)__cil_tmp27);
4351#line 295
4352    __cil_tmp29 = 0 * 4UL;
4353#line 295
4354    __cil_tmp30 = 0 + __cil_tmp29;
4355#line 295
4356    __cil_tmp31 = i * 36UL;
4357#line 295
4358    __cil_tmp32 = __cil_tmp31 + __cil_tmp30;
4359#line 295
4360    __cil_tmp33 = (unsigned long )(tgfx_cfg) + __cil_tmp32;
4361#line 295
4362    __cil_tmp34 = (int *)__cil_tmp33;
4363#line 295
4364    __cil_tmp35 = __cil_tmp34 + 1;
4365#line 295
4366    __cil_tmp36 = i * 36UL;
4367#line 295
4368    __cil_tmp37 = __cil_tmp36 + 32;
4369#line 295
4370    __cil_tmp38 = (unsigned long )(tgfx_cfg) + __cil_tmp37;
4371#line 295
4372    __cil_tmp39 = *((unsigned int *)__cil_tmp38);
4373#line 295
4374    __cil_tmp40 = __cil_tmp39 - 1U;
4375#line 295
4376    __cil_tmp41 = (int )__cil_tmp40;
4377#line 295
4378    *((struct tgfx **)__cil_tmp22) = tgfx_probe(__cil_tmp28, __cil_tmp35, __cil_tmp41);
4379#line 298
4380    __cil_tmp42 = i * 8UL;
4381#line 298
4382    __cil_tmp43 = (unsigned long )(tgfx_base) + __cil_tmp42;
4383#line 298
4384    __cil_tmp44 = *((struct tgfx **)__cil_tmp43);
4385#line 298
4386    __cil_tmp45 = (void const   *)__cil_tmp44;
4387#line 298
4388    tmp___0 = (long )IS_ERR(__cil_tmp45);
4389    }
4390#line 298
4391    if (tmp___0) {
4392      {
4393#line 299
4394      __cil_tmp46 = i * 8UL;
4395#line 299
4396      __cil_tmp47 = (unsigned long )(tgfx_base) + __cil_tmp46;
4397#line 299
4398      __cil_tmp48 = *((struct tgfx **)__cil_tmp47);
4399#line 299
4400      __cil_tmp49 = (void const   *)__cil_tmp48;
4401#line 299
4402      tmp = (long )PTR_ERR(__cil_tmp49);
4403#line 299
4404      err = (int )tmp;
4405      }
4406#line 300
4407      goto while_break;
4408    } else {
4409
4410    }
4411#line 303
4412    have_dev = 1;
4413    __Cont: /* CIL Label */ 
4414#line 285
4415    i = i + 1;
4416  }
4417  while_break: /* CIL Label */ ;
4418  }
4419#line 306
4420  if (err) {
4421    {
4422#line 307
4423    while (1) {
4424      while_continue___0: /* CIL Label */ ;
4425#line 307
4426      i = i - 1;
4427#line 307
4428      if (i >= 0) {
4429
4430      } else {
4431#line 307
4432        goto while_break___0;
4433      }
4434      {
4435#line 308
4436      __cil_tmp50 = i * 8UL;
4437#line 308
4438      __cil_tmp51 = (unsigned long )(tgfx_base) + __cil_tmp50;
4439#line 308
4440      if (*((struct tgfx **)__cil_tmp51)) {
4441        {
4442#line 309
4443        __cil_tmp52 = i * 8UL;
4444#line 309
4445        __cil_tmp53 = (unsigned long )(tgfx_base) + __cil_tmp52;
4446#line 309
4447        __cil_tmp54 = *((struct tgfx **)__cil_tmp53);
4448#line 309
4449        tgfx_remove(__cil_tmp54);
4450        }
4451      } else {
4452
4453      }
4454      }
4455    }
4456    while_break___0: /* CIL Label */ ;
4457    }
4458#line 310
4459    return (err);
4460  } else {
4461
4462  }
4463#line 313
4464  if (have_dev) {
4465#line 313
4466    tmp___1 = 0;
4467  } else {
4468#line 313
4469    tmp___1 = -19;
4470  }
4471#line 313
4472  return (tmp___1);
4473}
4474}
4475#line 316
4476static void tgfx_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
4477#line 316 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
4478static void tgfx_exit(void) 
4479{ int i ;
4480  unsigned long __cil_tmp2 ;
4481  unsigned long __cil_tmp3 ;
4482  unsigned long __cil_tmp4 ;
4483  unsigned long __cil_tmp5 ;
4484  struct tgfx *__cil_tmp6 ;
4485
4486  {
4487#line 320
4488  i = 0;
4489  {
4490#line 320
4491  while (1) {
4492    while_continue: /* CIL Label */ ;
4493#line 320
4494    if (i < 3) {
4495
4496    } else {
4497#line 320
4498      goto while_break;
4499    }
4500    {
4501#line 321
4502    __cil_tmp2 = i * 8UL;
4503#line 321
4504    __cil_tmp3 = (unsigned long )(tgfx_base) + __cil_tmp2;
4505#line 321
4506    if (*((struct tgfx **)__cil_tmp3)) {
4507      {
4508#line 322
4509      __cil_tmp4 = i * 8UL;
4510#line 322
4511      __cil_tmp5 = (unsigned long )(tgfx_base) + __cil_tmp4;
4512#line 322
4513      __cil_tmp6 = *((struct tgfx **)__cil_tmp5);
4514#line 322
4515      tgfx_remove(__cil_tmp6);
4516      }
4517    } else {
4518
4519    }
4520    }
4521#line 320
4522    i = i + 1;
4523  }
4524  while_break: /* CIL Label */ ;
4525  }
4526#line 323
4527  return;
4528}
4529}
4530#line 325 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
4531int init_module(void) 
4532{ int tmp ;
4533
4534  {
4535  {
4536#line 325
4537  tmp = tgfx_init();
4538  }
4539#line 325
4540  return (tmp);
4541}
4542}
4543#line 326 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
4544void cleanup_module(void) 
4545{ 
4546
4547  {
4548  {
4549#line 326
4550  tgfx_exit();
4551  }
4552#line 326
4553  return;
4554}
4555}
4556#line 344
4557void ldv_check_final_state(void) ;
4558#line 350
4559extern void ldv_initialize(void) ;
4560#line 353
4561extern int __VERIFIER_nondet_int(void) ;
4562#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
4563int LDV_IN_INTERRUPT  ;
4564#line 359 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
4565void main(void) 
4566{ unsigned long var_tgfx_timer_0_p0 ;
4567  int tmp ;
4568  int tmp___0 ;
4569  int tmp___1 ;
4570
4571  {
4572  {
4573#line 390
4574  LDV_IN_INTERRUPT = 1;
4575#line 399
4576  ldv_initialize();
4577#line 418
4578  tmp = tgfx_init();
4579  }
4580#line 418
4581  if (tmp) {
4582#line 419
4583    goto ldv_final;
4584  } else {
4585
4586  }
4587  {
4588#line 423
4589  while (1) {
4590    while_continue: /* CIL Label */ ;
4591    {
4592#line 423
4593    tmp___1 = __VERIFIER_nondet_int();
4594    }
4595#line 423
4596    if (tmp___1) {
4597
4598    } else {
4599#line 423
4600      goto while_break;
4601    }
4602    {
4603#line 426
4604    tmp___0 = __VERIFIER_nondet_int();
4605    }
4606#line 428
4607    if (tmp___0 == 0) {
4608#line 428
4609      goto case_0;
4610    } else {
4611      {
4612#line 457
4613      goto switch_default;
4614#line 426
4615      if (0) {
4616        case_0: /* CIL Label */ 
4617        {
4618#line 449
4619        tgfx_timer(var_tgfx_timer_0_p0);
4620        }
4621#line 456
4622        goto switch_break;
4623        switch_default: /* CIL Label */ 
4624#line 457
4625        goto switch_break;
4626      } else {
4627        switch_break: /* CIL Label */ ;
4628      }
4629      }
4630    }
4631  }
4632  while_break: /* CIL Label */ ;
4633  }
4634  {
4635#line 482
4636  tgfx_exit();
4637  }
4638  ldv_final: 
4639  {
4640#line 485
4641  ldv_check_final_state();
4642  }
4643#line 488
4644  return;
4645}
4646}
4647#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4648void ldv_blast_assert(void) 
4649{ 
4650
4651  {
4652  ERROR: 
4653#line 6
4654  goto ERROR;
4655}
4656}
4657#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4658extern int __VERIFIER_nondet_int(void) ;
4659#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4660int ldv_mutex  =    1;
4661#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4662int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
4663{ int nondetermined ;
4664
4665  {
4666#line 29
4667  if (ldv_mutex == 1) {
4668
4669  } else {
4670    {
4671#line 29
4672    ldv_blast_assert();
4673    }
4674  }
4675  {
4676#line 32
4677  nondetermined = __VERIFIER_nondet_int();
4678  }
4679#line 35
4680  if (nondetermined) {
4681#line 38
4682    ldv_mutex = 2;
4683#line 40
4684    return (0);
4685  } else {
4686#line 45
4687    return (-4);
4688  }
4689}
4690}
4691#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4692int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
4693{ int nondetermined ;
4694
4695  {
4696#line 57
4697  if (ldv_mutex == 1) {
4698
4699  } else {
4700    {
4701#line 57
4702    ldv_blast_assert();
4703    }
4704  }
4705  {
4706#line 60
4707  nondetermined = __VERIFIER_nondet_int();
4708  }
4709#line 63
4710  if (nondetermined) {
4711#line 66
4712    ldv_mutex = 2;
4713#line 68
4714    return (0);
4715  } else {
4716#line 73
4717    return (-4);
4718  }
4719}
4720}
4721#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4722int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
4723{ int atomic_value_after_dec ;
4724
4725  {
4726#line 83
4727  if (ldv_mutex == 1) {
4728
4729  } else {
4730    {
4731#line 83
4732    ldv_blast_assert();
4733    }
4734  }
4735  {
4736#line 86
4737  atomic_value_after_dec = __VERIFIER_nondet_int();
4738  }
4739#line 89
4740  if (atomic_value_after_dec == 0) {
4741#line 92
4742    ldv_mutex = 2;
4743#line 94
4744    return (1);
4745  } else {
4746
4747  }
4748#line 98
4749  return (0);
4750}
4751}
4752#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4753void mutex_lock(struct mutex *lock ) 
4754{ 
4755
4756  {
4757#line 108
4758  if (ldv_mutex == 1) {
4759
4760  } else {
4761    {
4762#line 108
4763    ldv_blast_assert();
4764    }
4765  }
4766#line 110
4767  ldv_mutex = 2;
4768#line 111
4769  return;
4770}
4771}
4772#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4773int mutex_trylock(struct mutex *lock ) 
4774{ int nondetermined ;
4775
4776  {
4777#line 121
4778  if (ldv_mutex == 1) {
4779
4780  } else {
4781    {
4782#line 121
4783    ldv_blast_assert();
4784    }
4785  }
4786  {
4787#line 124
4788  nondetermined = __VERIFIER_nondet_int();
4789  }
4790#line 127
4791  if (nondetermined) {
4792#line 130
4793    ldv_mutex = 2;
4794#line 132
4795    return (1);
4796  } else {
4797#line 137
4798    return (0);
4799  }
4800}
4801}
4802#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4803void mutex_unlock(struct mutex *lock ) 
4804{ 
4805
4806  {
4807#line 147
4808  if (ldv_mutex == 2) {
4809
4810  } else {
4811    {
4812#line 147
4813    ldv_blast_assert();
4814    }
4815  }
4816#line 149
4817  ldv_mutex = 1;
4818#line 150
4819  return;
4820}
4821}
4822#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4823void ldv_check_final_state(void) 
4824{ 
4825
4826  {
4827#line 156
4828  if (ldv_mutex == 1) {
4829
4830  } else {
4831    {
4832#line 156
4833    ldv_blast_assert();
4834    }
4835  }
4836#line 157
4837  return;
4838}
4839}
4840#line 497 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4106/dscv_tempdir/dscv/ri/32_1/drivers/input/joystick/turbografx.c.common.c"
4841long s__builtin_expect(long val , long res ) 
4842{ 
4843
4844  {
4845#line 498
4846  return (val);
4847}
4848}