Showing error 673

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