text: /* Generated by CIL v. 1.3.7 */
  /* print_CIL_Input is true */
  
  #line 25 "cprover/ddverify/include/ddverify/pthread.h"
  struct __pthread_mutex_t_struct {
     _Bool locked ;
  };
  #line 30 "cprover/ddverify/include/ddverify/pthread.h"
  struct __pthread_mutexattr_t_struct {
     int dummy ;
  };
  #line 52 "cprover/ddverify/include/ddverify/pthread.h"
  typedef struct __pthread_mutex_t_struct pthread_mutex_t;
  #line 53 "cprover/ddverify/include/ddverify/pthread.h"
  typedef struct __pthread_mutexattr_t_struct pthread_mutexattr_t;
  #line 5 "./include/asm/posix_types.h"
  typedef unsigned short __kernel_mode_t;
  #line 12 "./include/asm/posix_types.h"
  typedef unsigned int __kernel_size_t;
  #line 13 "./include/asm/posix_types.h"
  typedef int __kernel_ssize_t;
  #line 4 "./include/asm/types.h"
  typedef unsigned short umode_t;
  #line 13 "./include/asm/types.h"
  typedef unsigned int __u32;
  #line 30 "./include/asm/types.h"
  typedef unsigned long long u64;
  #line 9 "./include/linux/types.h"
  typedef __u32 __kernel_dev_t;
  #line 11 "./include/linux/types.h"
  typedef __kernel_dev_t dev_t;
  #line 13 "./include/linux/types.h"
  typedef __kernel_mode_t mode_t;
  #line 42 "./include/linux/types.h"
  typedef long long loff_t;
  #line 51 "./include/linux/types.h"
  typedef __kernel_size_t size_t;
  #line 56 "./include/linux/types.h"
  typedef __kernel_ssize_t ssize_t;
  #line 15 "cprover/ddverify/include/ddverify/pthread.h"
  struct __pthread_t_struct {
     int id ;
  };
  #line 20 "cprover/ddverify/include/ddverify/pthread.h"
  struct __pthread_attr_t_struct {
     int dummy ;
  };
  #line 50 "cprover/ddverify/include/ddverify/pthread.h"
  typedef struct __pthread_t_struct pthread_t;
  #line 51 "cprover/ddverify/include/ddverify/pthread.h"
  typedef struct __pthread_attr_t_struct pthread_attr_t;
  #line 12 "./include/linux/spinlock_types.h"
  struct __anonstruct_spinlock_t_10 {
     int init ;
     int locked ;
  };
  #line 12 "./include/linux/spinlock_types.h"
  typedef struct __anonstruct_spinlock_t_10 spinlock_t;
  #line 6 "./include/asm/atomic.h"
  typedef int atomic_t;
  #line 67 "./include/linux/gfp.h"
  struct page;
  #line 67
  struct page;
  #line 4 "./include/linux/timer.h"
  struct timer_list {
     unsigned long expires ;
     void (*function)(unsigned long  ) ;
     unsigned long data ;
     short __ddv_active ;
     short __ddv_init ;
  };
  #line 4 "./include/linux/dcache.h"
  struct inode;
  #line 4
  struct inode;
  #line 4 "./include/linux/dcache.h"
  struct dentry {
     struct inode *d_inode ;
  };
  #line 265 "./include/linux/fs.h"
  struct file;
  #line 265
  struct file;
  #line 269
  struct poll_table_struct;
  #line 269
  struct poll_table_struct;
  #line 270
  struct vm_area_struct;
  #line 270
  struct vm_area_struct;
  #line 328 "./include/linux/fs.h"
  struct address_space_operations {
     int (*prepare_write)(struct file * , struct page * , unsigned int  , unsigned int  ) ;
     int (*commit_write)(struct file * , struct page * , unsigned int  , unsigned int  ) ;
  };
  #line 338 "./include/linux/fs.h"
  struct address_space {
     struct inode *host ;
     struct address_space_operations  const  *a_ops ;
  } __attribute__((__aligned__(sizeof(long )))) ;
  #line 343
  struct gendisk;
  #line 343
  struct gendisk;
  #line 343 "./include/linux/fs.h"
  struct block_device {
     struct inode *bd_inode ;
     struct block_device *bd_contains ;
     unsigned int bd_block_size ;
     struct gendisk *bd_disk ;
  };
  #line 352
  struct cdev;
  #line 352
  struct cdev;
  #line 352 "./include/linux/fs.h"
  union __anonunion____missing_field_name_14 {
     struct block_device *i_bdev ;
     struct cdev *i_cdev ;
  };
  #line 352 "./include/linux/fs.h"
  struct inode {
     umode_t i_mode ;
     dev_t i_rdev ;
     loff_t i_size ;
     union __anonunion____missing_field_name_14 __annonCompField1 ;
  };
  #line 386
  struct file_operations;
  #line 386
  struct file_operations;
  #line 386 "./include/linux/fs.h"
  struct file {
     struct dentry *f_dentry ;
     struct file_operations  const  *f_op ;
     atomic_t f_count ;
     unsigned int f_flags ;
     mode_t f_mode ;
     loff_t f_pos ;
     void *private_data ;
     struct address_space *f_mapping ;
  };
  #line 406
  struct files_struct;
  #line 406
  struct files_struct;
  #line 406 "./include/linux/fs.h"
  typedef struct files_struct *fl_owner_t;
  #line 409 "./include/linux/fs.h"
  struct file_lock {
     int something ;
  };
  #line 435
  struct module;
  #line 435
  struct module;
  #line 457 "./include/linux/fs.h"
  struct __anonstruct_read_descriptor_t_15 {
     size_t written ;
     size_t count ;
  };
  #line 457 "./include/linux/fs.h"
  typedef struct __anonstruct_read_descriptor_t_15 read_descriptor_t;
  #line 475 "./include/linux/fs.h"
  struct file_operations {
     struct module *owner ;
     loff_t (*llseek)(struct file * , loff_t  , int  ) ;
     ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
     ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
     int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
                                                     loff_t  , u64  , unsigned int  ) ) ;
     unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
     int (*ioctl)(struct inode * , struct file * , unsigned int  , unsigned long  ) ;
     long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
     long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
     int (*mmap)(struct file * , struct vm_area_struct * ) ;
     int (*open)(struct inode * , struct file * ) ;
     int (*flush)(struct file * , fl_owner_t id ) ;
     int (*release)(struct inode * , struct file * ) ;
     int (*fsync)(struct file * , struct dentry * , int datasync ) ;
     int (*fasync)(int  , struct file * , int  ) ;
     int (*lock)(struct file * , int  , struct file_lock * ) ;
     ssize_t (*sendfile)(struct file * , loff_t * , size_t  , int (*)(read_descriptor_t * ,
                                                                      struct page * ,
                                                                      unsigned long  ,
                                                                      unsigned long  ) ,
                         void * ) ;
     ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
                         int  ) ;
     unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
                                        unsigned long  , unsigned long  ) ;
     int (*check_flags)(int  ) ;
     int (*dir_notify)(struct file *filp , unsigned long arg ) ;
     int (*flock)(struct file * , int  , struct file_lock * ) ;
  };
  #line 5 "./include/linux/cdev.h"
  struct cdev {
     struct module *owner ;
     struct file_operations  const  *ops ;
     dev_t dev ;
     unsigned int count ;
  };
  #line 17 "cprover/ddverify/include/ddverify/cdev.h"
  struct ddv_cdev {
     struct cdev *cdevp ;
     struct file filp ;
     struct inode inode ;
     int open ;
  };
  #line 6 "./include/linux/mod_devicetable.h"
  typedef unsigned long kernel_ulong_t;
  #line 10 "./include/linux/mod_devicetable.h"
  struct pci_device_id {
     __u32 vendor ;
     __u32 device ;
     __u32 subvendor ;
     __u32 subdevice ;
     __u32 class ;
     __u32 class_mask ;
     kernel_ulong_t driver_data ;
  };
  #line 18 "./include/linux/ioport.h"
  struct resource {
     char const   *name ;
     unsigned long start ;
     unsigned long end ;
     unsigned long flags ;
  };
  #line 144 "./include/linux/pm.h"
  struct pm_message {
     int event ;
  };
  #line 144 "./include/linux/pm.h"
  typedef struct pm_message pm_message_t;
  #line 25 "./include/linux/device.h"
  struct device {
     void *driver_data ;
     void (*release)(struct device *dev ) ;
  };
  #line 9 "./include/linux/mm_types.h"
  struct page {
     int something ;
  };
  #line 79 "./include/linux/pci.h"
  typedef int pci_power_t;
  #line 122
  struct pci_bus;
  #line 122
  struct pci_bus;
  #line 122 "./include/linux/pci.h"
  struct pci_dev {
     struct pci_bus *bus ;
     unsigned int devfn ;
     unsigned short vendor ;
     unsigned short device ;
     unsigned short subsystem_vendor ;
     unsigned short subsystem_device ;
     u64 dma_mask ;
     struct device dev ;
     unsigned int irq ;
     struct resource resource[12] ;
  };
  #line 249 "./include/linux/pci.h"
  struct pci_bus {
     unsigned char number ;
  };
  #line 375 "./include/linux/pci.h"
  struct pci_driver {
     char *name ;
     struct pci_device_id  const  *id_table ;
     int (*probe)(struct pci_dev *dev , struct pci_device_id  const  *id ) ;
     void (*remove)(struct pci_dev *dev ) ;
     int (*suspend)(struct pci_dev *dev , pm_message_t state ) ;
     int (*resume)(struct pci_dev *dev ) ;
     int (*enable_wake)(struct pci_dev *dev , pci_power_t state , int enable ) ;
     void (*shutdown)(struct pci_dev *dev ) ;
  };
  #line 6 "cprover/ddverify/include/ddverify/pci.h"
  struct ddv_pci_driver {
     struct pci_driver *pci_driver ;
     struct pci_dev pci_dev ;
     unsigned int no_pci_device_id ;
     int dev_initialized ;
  };
  #line 4 "./include/asm/ptrace.h"
  struct pt_regs {
     int something ;
  };
  #line 28 "./include/linux/interrupt.h"
  typedef int irqreturn_t;
  #line 34 "./include/linux/interrupt.h"
  struct tasklet_struct {
     atomic_t count ;
     void (*func)(unsigned long  ) ;
     unsigned long data ;
     int init ;
  };
  #line 9 "cprover/ddverify/include/ddverify/interrupt.h"
  struct registered_irq {
     irqreturn_t (*handler)(int  , void * , struct pt_regs * ) ;
     void *dev_id ;
  };
  #line 14 "cprover/ddverify/include/ddverify/tasklet.h"
  struct ddv_tasklet {
     struct tasklet_struct *tasklet ;
     unsigned short is_running ;
  };
  #line 14 "cprover/ddverify/include/ddverify/timer.h"
  struct ddv_timer {
     struct timer_list *timer ;
  };
  #line 11 "./include/linux/workqueue.h"
  struct work_struct {
     unsigned long pending ;
     void (*func)(void * ) ;
     void *data ;
     int init ;
  };
  #line 49 "./include/linux/mutex.h"
  struct mutex {
     int locked ;
     int init ;
  };
  #line 4 "./include/asm/semaphore.h"
  struct semaphore {
     int init ;
     int locked ;
  };
  #line 17 "./include/linux/wait.h"
  struct __wait_queue_head {
     int number_process_waiting ;
     int wakeup ;
     int init ;
  };
  #line 22 "./include/linux/wait.h"
  typedef struct __wait_queue_head wait_queue_head_t;
  #line 155 "./include/linux/types.h"
  typedef unsigned int gfp_t;
  #line 34 "./include/linux/miscdevice.h"
  struct miscdevice {
     int minor ;
     char const   *name ;
     struct file_operations  const  *fops ;
  };
  #line 7 "./include/asm/posix_types.h"
  typedef long __kernel_off_t;
  #line 15 "./include/linux/types.h"
  typedef __kernel_off_t off_t;
  #line 6 "./include/asm/termbits.h"
  typedef unsigned char cc_t;
  #line 8 "./include/asm/termbits.h"
  typedef unsigned int tcflag_t;
  #line 11 "./include/asm/termbits.h"
  struct termios {
     tcflag_t c_iflag ;
     tcflag_t c_oflag ;
     tcflag_t c_cflag ;
     tcflag_t c_lflag ;
     cc_t c_line ;
     cc_t c_cc[19] ;
  };
  #line 122 "./include/linux/tty_driver.h"
  struct tty_struct;
  #line 122
  struct tty_struct;
  #line 124 "./include/linux/tty_driver.h"
  struct tty_operations {
     int (*open)(struct tty_struct *tty , struct file *filp ) ;
     void (*close)(struct tty_struct *tty , struct file *filp ) ;
     int (*write)(struct tty_struct *tty , unsigned char const   *buf , int count ) ;
     void (*put_char)(struct tty_struct *tty , unsigned char ch ) ;
     void (*flush_chars)(struct tty_struct *tty ) ;
     int (*write_room)(struct tty_struct *tty ) ;
     int (*chars_in_buffer)(struct tty_struct *tty ) ;
     int (*ioctl)(struct tty_struct *tty , struct file *file , unsigned int cmd , unsigned long arg ) ;
     void (*set_termios)(struct tty_struct *tty , struct termios *old ) ;
     void (*throttle)(struct tty_struct *tty ) ;
     void (*unthrottle)(struct tty_struct *tty ) ;
     void (*stop)(struct tty_struct *tty ) ;
     void (*start)(struct tty_struct *tty ) ;
     void (*hangup)(struct tty_struct *tty ) ;
     void (*break_ctl)(struct tty_struct *tty , int state ) ;
     void (*flush_buffer)(struct tty_struct *tty ) ;
     void (*set_ldisc)(struct tty_struct *tty ) ;
     void (*wait_until_sent)(struct tty_struct *tty , int timeout ) ;
     void (*send_xchar)(struct tty_struct *tty , char ch ) ;
     int (*read_proc)(char *page , char **start , off_t off , int count , int *eof ,
                      void *data ) ;
     int (*write_proc)(struct file *file , char const   *buffer , unsigned long count ,
                       void *data ) ;
     int (*tiocmget)(struct tty_struct *tty , struct file *file ) ;
     int (*tiocmset)(struct tty_struct *tty , struct file *file , unsigned int set ,
                     unsigned int clear ) ;
  };
  #line 155
  struct proc_dir_entry;
  #line 155
  struct proc_dir_entry;
  #line 155 "./include/linux/tty_driver.h"
  struct tty_driver {
     int magic ;
     struct cdev cdev ;
     struct module *owner ;
     char const   *driver_name ;
     char const   *name ;
     int name_base ;
     int major ;
     int minor_start ;
     int minor_num ;
     int num ;
     short type ;
     short subtype ;
     struct termios init_termios ;
     int flags ;
     int refcount ;
     struct proc_dir_entry *proc_entry ;
     int (*open)(struct tty_struct *tty , struct file *filp ) ;
     void (*close)(struct tty_struct *tty , struct file *filp ) ;
     int (*write)(struct tty_struct *tty , unsigned char const   *buf , int count ) ;
     void (*put_char)(struct tty_struct *tty , unsigned char ch ) ;
     void (*flush_chars)(struct tty_struct *tty ) ;
     int (*write_room)(struct tty_struct *tty ) ;
     int (*chars_in_buffer)(struct tty_struct *tty ) ;
     int (*ioctl)(struct tty_struct *tty , struct file *file , unsigned int cmd , unsigned long arg ) ;
     void (*set_termios)(struct tty_struct *tty , struct termios *old ) ;
     void (*throttle)(struct tty_struct *tty ) ;
     void (*unthrottle)(struct tty_struct *tty ) ;
     void (*stop)(struct tty_struct *tty ) ;
     void (*start)(struct tty_struct *tty ) ;
     void (*hangup)(struct tty_struct *tty ) ;
     void (*break_ctl)(struct tty_struct *tty , int state ) ;
     void (*flush_buffer)(struct tty_struct *tty ) ;
     void (*set_ldisc)(struct tty_struct *tty ) ;
     void (*wait_until_sent)(struct tty_struct *tty , int timeout ) ;
     void (*send_xchar)(struct tty_struct *tty , char ch ) ;
     int (*read_proc)(char *page , char **start , off_t off , int count , int *eof ,
                      void *data ) ;
     int (*write_proc)(struct file *file , char const   *buffer , unsigned long count ,
                       void *data ) ;
     int (*tiocmget)(struct tty_struct *tty , struct file *file ) ;
     int (*tiocmset)(struct tty_struct *tty , struct file *file , unsigned int set ,
                     unsigned int clear ) ;
  };
  #line 127 "./include/linux/tty.h"
  struct tty_struct {
     int magic ;
     struct tty_driver *driver ;
     int index ;
     struct termios *termios ;
     struct termios *termios_locked ;
     char name[64] ;
     unsigned long flags ;
     int count ;
     unsigned char stopped : 1 ;
     unsigned char hw_stopped : 1 ;
     unsigned char flow_stopped : 1 ;
     unsigned char packet : 1 ;
     unsigned int receive_room ;
     wait_queue_head_t write_wait ;
     wait_queue_head_t read_wait ;
     void *disc_data ;
     void *driver_data ;
     unsigned char closing : 1 ;
  };
  #line 7 "cprover/ddverify/include/ddverify/tty.h"
  struct ddv_tty_driver {
     struct tty_driver driver ;
     unsigned short allocated ;
     unsigned short registered ;
  };
  #line 1 "preproc_ggZOIw.o"
  #pragma merger(0,"preproc_ggZOIw.i","-x,c")
  #line 11 "cprover/ddverify/include/ddverify/ddverify.h"
  int current_execution_context  ;
  #line 22
  extern int __CPROVER_assert() ;
  #line 42 "cprover/ddverify/include/ddverify/ddverify.h"
  int (*_ddv_module_init)(void)  ;
  #line 43 "cprover/ddverify/include/ddverify/ddverify.h"
  void (*_ddv_module_exit)(void)  ;
  #line 45
  int call_ddv(void) ;
  #line 7 "./include/linux/jiffies.h"
  unsigned long jiffies  ;
  #line 192 "cprover/ddverify/include/ddverify/pthread.h"
  __inline extern int pthread_mutex_init(pthread_mutex_t *__mutex , pthread_mutexattr_t const   *__mutex_attr ) 
  { pthread_mutex_t i ;
    _Bool i_locked4 ;
  
    {
  #line 196
    i_locked4 = (_Bool)0;
  #line 197
    __mutex->locked = i_locked4;
  #line 198
    return (0);
  }
  }
  #line 200 "cprover/ddverify/include/ddverify/pthread.h"
  __inline extern int pthread_mutex_destroy(pthread_mutex_t *__mutex ) 
  { 
  
    {
  #line 202
    return (0);
  }
  }
  #line 206
  extern void __CPROVER_atomic_begin() ;
  #line 207
  extern void __CPROVER_atomic_end() ;
  #line 213
  extern int __CPROVER_assume() ;
  #line 209 "cprover/ddverify/include/ddverify/pthread.h"
  __inline extern int pthread_mutex_lock(pthread_mutex_t *__mutex ) 
  { _Bool __cil_tmp2 ;
    int __cil_tmp3 ;
  
    {
    {
  #line 212
    __CPROVER_atomic_begin();
  #line 213
    __cil_tmp2 = *((_Bool *)__mutex);
  #line 213
    __cil_tmp3 = ! __cil_tmp2;
  #line 213
    __CPROVER_assume(__cil_tmp3);
  #line 214
    *((_Bool *)__mutex) = (_Bool)1;
  #line 215
    __CPROVER_atomic_end();
    }
  #line 216
    return (0);
  }
  }
  #line 219 "cprover/ddverify/include/ddverify/pthread.h"
  __inline extern int pthread_mutex_unlock(pthread_mutex_t *__mutex ) 
  { _Bool __cil_tmp2 ;
    int __cil_tmp3 ;
  
    {
    {
  #line 222
    __cil_tmp2 = *((_Bool *)__mutex);
  #line 222
    __cil_tmp3 = (int )__cil_tmp2;
  #line 222
    __CPROVER_assert(__cil_tmp3, "pthread_mutex_unlock without lock");
  #line 223
    *((_Bool *)__mutex) = (_Bool)0;
    }
  #line 224
    return (0);
  }
  }
  #line 89 "./include/asm/thread_info.h"
  unsigned long current_stack_pointer  ;
  #line 96 "drivers/char/watchdog/sc520_wdt.c"
  char _ddv_module_param_timeout[74]  = 
  #line 96 "drivers/char/watchdog/sc520_wdt.c"
    {      (char )'W',      (char )'a',      (char )'t',      (char )'c', 
          (char )'h',      (char )'d',      (char )'o',      (char )'g', 
          (char )' ',      (char )'t',      (char )'i',      (char )'m', 
          (char )'e',      (char )'o',      (char )'u',      (char )'t', 
          (char )' ',      (char )'i',      (char )'n',      (char )' ', 
          (char )'s',      (char )'e',      (char )'c',      (char )'o', 
          (char )'n',      (char )'d',      (char )'s',      (char )'.', 
          (char )' ',      (char )'(',      (char )'1',      (char )'<', 
          (char )'=',      (char )'t',      (char )'i',      (char )'m', 
          (char )'e',      (char )'o',      (char )'u',      (char )'t', 
          (char )'<',      (char )'=',      (char )'3',      (char )'6', 
          (char )'0',      (char )'0',      (char )',',      (char )' ', 
          (char )'d',      (char )'e',      (char )'f',      (char )'a', 
          (char )'u',      (char )'l',      (char )'t',      (char )'=', 
          (char )'W',      (char )'A',      (char )'T',      (char )'C', 
          (char )'H',      (char )'D',      (char )'O',      (char )'G', 
          (char )'_',      (char )'T',      (char )'I',      (char )'M', 
          (char )'E',      (char )'O',      (char )'U',      (char )'T', 
          (char )')',      (char )'\000'};
  #line 100 "drivers/char/watchdog/sc520_wdt.c"
  char _ddv_module_param_nowayout[75]  = 
  #line 100
    {      (char )'W',      (char )'a',      (char )'t',      (char )'c', 
          (char )'h',      (char )'d',      (char )'o',      (char )'g', 
          (char )' ',      (char )'c',      (char )'a',      (char )'n', 
          (char )'n',      (char )'o',      (char )'t',      (char )' ', 
          (char )'b',      (char )'e',      (char )' ',      (char )'s', 
          (char )'t',      (char )'o',      (char )'p',      (char )'p', 
          (char )'e',      (char )'d',      (char )' ',      (char )'o', 
          (char )'n',      (char )'c',      (char )'e',      (char )' ', 
          (char )'s',      (char )'t',      (char )'a',      (char )'r', 
          (char )'t',      (char )'e',      (char )'d',      (char )' ', 
          (char )'(',      (char )'d',      (char )'e',      (char )'f', 
          (char )'a',      (char )'u',      (char )'l',      (char )'t', 
          (char )'=',      (char )'C',      (char )'O',      (char )'N', 
          (char )'F',      (char )'I',      (char )'G',      (char )'_', 
          (char )'W',      (char )'A',      (char )'T',      (char )'C', 
          (char )'H',      (char )'D',      (char )'O',      (char )'G', 
          (char )'_',      (char )'N',      (char )'O',      (char )'W', 
          (char )'A',      (char )'Y',      (char )'O',      (char )'U', 
          (char )'T',      (char )')',      (char )'\000'};
  #line 440 "drivers/char/watchdog/sc520_wdt.c"
  char _ddv_module_author[24]  = 
  #line 440
    {      (char )'S',      (char )'c',      (char )'o',      (char )'t', 
          (char )'t',      (char )' ',      (char )'a',      (char )'n', 
          (char )'d',      (char )' ',      (char )'B',      (char )'i', 
          (char )'l',      (char )'l',      (char )' ',      (char )'J', 
          (char )'e',      (char )'n',      (char )'n',      (char )'i', 
          (char )'n',      (char )'g',      (char )'s',      (char )'\000'};
  #line 441 "drivers/char/watchdog/sc520_wdt.c"
  char _ddv_module_description[57]  = 
  #line 441
    {      (char )'D',      (char )'r',      (char )'i',      (char )'v', 
          (char )'e',      (char )'r',      (char )' ',      (char )'f', 
          (char )'o',      (char )'r',      (char )' ',      (char )'w', 
          (char )'a',      (char )'t',      (char )'c',      (char )'h', 
          (char )'d',      (char )'o',      (char )'g',      (char )' ', 
          (char )'t',      (char )'i',      (char )'m',      (char )'e', 
          (char )'r',      (char )' ',      (char )'i',      (char )'n', 
          (char )' ',      (char )'A',      (char )'M',      (char )'D', 
          (char )' ',      (char )'\"',      (char )'E',      (char )'l', 
          (char )'a',      (char )'n',      (char )'\"',      (char )' ', 
          (char )'S',      (char )'C',      (char )'5',      (char )'2', 
          (char )'0',      (char )' ',      (char )'u',      (char )'P', 
          (char )'r',      (char )'o',      (char )'c',      (char )'e', 
          (char )'s',      (char )'s',      (char )'o',      (char )'r', 
          (char )'\000'};
  #line 442 "drivers/char/watchdog/sc520_wdt.c"
  char _ddv_module_license[4]  = {      (char )'G',      (char )'P',      (char )'L',      (char )'\000'};
  #line 4 "__main_6t9.c"
  int main(void) 
  { 
  
    {
    {
  #line 12
    call_ddv();
    }
  #line 13
    return (0);
  }
  }
  #line 1 "preproc_MjpQ9P.o"
  #pragma merger(0,"preproc_MjpQ9P.i","-x,c")
  #line 145 "cprover/ddverify/include/ddverify/pthread.h"
  extern int pthread_create(pthread_t *__threadp , pthread_attr_t const   *__attr ,
                            void *(*__start_routine)(void * ) , void *__arg ) ;
  #line 16 "cprover/ddverify/include/ddverify/satabs.h"
  extern unsigned short __VERIFIER_nondet_ushort() ;
  #line 17
  extern int __VERIFIER_nondet_int() ;
  #line 54 "./include/linux/spinlock.h"
  void spin_lock_init(spinlock_t *lock ) ;
  #line 12 "cprover/ddverify/include/ddverify/fixed_cdev.h"
  struct cdev fixed_cdev[10]  ;
  #line 13 "cprover/ddverify/include/ddverify/fixed_cdev.h"
  int fixed_cdev_used  =    0;
  #line 15 "cprover/ddverify/include/ddverify/cdev.h"
  short number_cdev_registered  =    (short)0;
  #line 26 "cprover/ddverify/include/ddverify/cdev.h"
  struct ddv_cdev cdev_registered[10]  ;
  #line 28
  void call_cdev_functions(void) ;
  #line 14 "cprover/ddverify/include/ddverify/pci.h"
  struct ddv_pci_driver registered_pci_driver  ;
  #line 14 "cprover/ddverify/include/ddverify/interrupt.h"
  struct registered_irq registered_irq[16]  ;
  #line 16
  void call_interrupt_handler(void) ;
  #line 12 "cprover/ddverify/include/ddverify/tasklet.h"
  short number_tasklet_registered  =    (short)0;
  #line 19 "cprover/ddverify/include/ddverify/tasklet.h"
  struct ddv_tasklet tasklet_registered[10]  ;
  #line 21
  void call_tasklet_functions(void) ;
  #line 12 "cprover/ddverify/include/ddverify/timer.h"
  short number_timer_registered  =    (short)0;
  #line 18 "cprover/ddverify/include/ddverify/timer.h"
  struct ddv_timer timer_registered[5]  ;
  #line 20
  void call_timer_functions(void) ;
  #line 8 "cprover/ddverify/include/ddverify/workqueue.h"
  struct work_struct *shared_workqueue[10]  ;
  #line 10
  void call_shared_workqueue_functions(void) ;
  #line 9 "./include/linux/smp_lock.h"
  spinlock_t kernel_lock  ;
  #line 17 "cprover/ddverify/src/ddverify/ddverify.c"
  void init_kernel(void) 
  { int i ;
    unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
    void *__cil_tmp4 ;
    unsigned long __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    void *__cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
  
    {
    {
  #line 21
    spin_lock_init(& kernel_lock);
  #line 23
    i = 0;
    }
    {
  #line 23
    while (1) {
      while_continue: /* CIL Label */ ;
  #line 23
      if (i < 10) {
  
      } else {
  #line 23
        goto while_break;
      }
  #line 24
      __cil_tmp2 = i * 8UL;
  #line 24
      __cil_tmp3 = (unsigned long )(shared_workqueue) + __cil_tmp2;
  #line 24
      __cil_tmp4 = (void *)0;
  #line 24
      *((struct work_struct **)__cil_tmp3) = (struct work_struct *)__cil_tmp4;
  #line 23
      i = i + 1;
    }
    while_break: /* CIL Label */ ;
    }
  #line 27
    i = 0;
    {
  #line 27
    while (1) {
      while_continue___0: /* CIL Label */ ;
  #line 27
      if (i < 10) {
  
      } else {
  #line 27
        goto while_break___0;
      }
  #line 28
      __cil_tmp5 = i * 16UL;
  #line 28
      __cil_tmp6 = (unsigned long )(tasklet_registered) + __cil_tmp5;
  #line 28
      __cil_tmp7 = (void *)0;
  #line 28
      *((struct tasklet_struct **)__cil_tmp6) = (struct tasklet_struct *)__cil_tmp7;
  #line 29
      __cil_tmp8 = i * 16UL;
  #line 29
      __cil_tmp9 = __cil_tmp8 + 8;
  #line 29
      __cil_tmp10 = (unsigned long )(tasklet_registered) + __cil_tmp9;
  #line 29
      *((unsigned short *)__cil_tmp10) = (unsigned short)0;
  #line 27
      i = i + 1;
    }
    while_break___0: /* CIL Label */ ;
    }
  #line 31
    return;
  }
  }
  #line 33 "cprover/ddverify/src/ddverify/ddverify.c"
  static void *ddv_2(void *arg ) 
  { unsigned short random ;
  
    {
    {
  #line 37
    while (1) {
      while_continue: /* CIL Label */ ;
      {
  #line 38
      random = __VERIFIER_nondet_ushort();
      }
      {
  #line 41
      if ((int )random == 1) {
  #line 41
        goto case_1;
      } else {
  
      }
  #line 53
      if ((int )random == 2) {
  #line 53
        goto case_2;
      } else {
  
      }
  #line 61
      if ((int )random == 3) {
  #line 61
        goto case_3;
      } else {
  
      }
  #line 69
      if ((int )random == 4) {
  #line 69
        goto case_4;
      } else {
  
      }
  #line 77
      if ((int )random == 5) {
  #line 77
        goto case_5;
      } else {
  
      }
  #line 85
      goto switch_default;
      case_1: /* CIL Label */ 
  #line 52
      goto switch_break;
      case_2: /* CIL Label */ 
      {
  #line 55
      current_execution_context = 2;
  #line 56
      call_timer_functions();
  #line 58
      current_execution_context = 1;
      }
  #line 60
      goto switch_break;
      case_3: /* CIL Label */ 
      {
  #line 63
      current_execution_context = 2;
  #line 64
      call_interrupt_handler();
  #line 66
      current_execution_context = 1;
      }
  #line 68
      goto switch_break;
      case_4: /* CIL Label */ 
      {
  #line 71
      current_execution_context = 1;
  #line 72
      call_shared_workqueue_functions();
  #line 74
      current_execution_context = 1;
      }
  #line 76
      goto switch_break;
      case_5: /* CIL Label */ 
      {
  #line 79
      current_execution_context = 2;
  #line 80
      call_tasklet_functions();
  #line 82
      current_execution_context = 1;
      }
  #line 84
      goto switch_break;
      switch_default: /* CIL Label */ 
  #line 97
      goto switch_break;
      switch_break: /* CIL Label */ ;
      }
  #line 37
      if (! random) {
  #line 37
        goto while_break;
      } else {
  
      }
    }
    while_break: /* CIL Label */ ;
    }
  #line 100
    return ((void *)0);
  }
  }
  #line 102 "cprover/ddverify/src/ddverify/ddverify.c"
  void ddv(void) 
  { pthread_t thread ;
    int tmp ;
    void *__cil_tmp3 ;
    pthread_attr_t const   *__cil_tmp4 ;
    void *__cil_tmp5 ;
  
    {
    {
  #line 111
    __cil_tmp3 = (void *)0;
  #line 111
    __cil_tmp4 = (pthread_attr_t const   *)__cil_tmp3;
  #line 111
    __cil_tmp5 = (void *)0;
  #line 111
    pthread_create(& thread, __cil_tmp4, & ddv_2, __cil_tmp5);
    }
    {
  #line 113
    while (1) {
      while_continue: /* CIL Label */ ;
      {
  #line 114
      current_execution_context = 1;
  #line 116
      call_cdev_functions();
  #line 113
      tmp = __VERIFIER_nondet_int();
      }
  #line 113
      if (! tmp) {
  #line 113
        goto while_break;
      } else {
  
      }
    }
    while_break: /* CIL Label */ ;
    }
  #line 124
    return;
  }
  }
  #line 128
  extern int sc520_wdt_init(void) ;
  #line 131
  extern void sc520_wdt_unload(void) ;
  #line 134 "cprover/ddverify/src/ddverify/ddverify.c"
  int call_ddv(void) 
  { int err ;
  
    {
    {
  #line 138
    current_execution_context = 1;
  #line 140
    init_kernel();
  #line 145
    err = sc520_wdt_init();
    }
  #line 148
    if (err) {
  #line 149
      return (-1);
    } else {
  
    }
    {
  #line 152
    ddv();
  #line 154
    current_execution_context = 1;
  #line 158
    sc520_wdt_unload();
    }
  #line 161
    return (0);
  }
  }
  #line 1 "preproc_vh0wL5.o"
  #pragma merger(0,"preproc_vh0wL5.i","-x,c")
  #line 18 "cprover/ddverify/include/ddverify/satabs.h"
  extern unsigned int __VERIFIER_nondet_uint() ;
  #line 20
  extern unsigned long __VERIFIER_nondet_ulong() ;
  #line 21
  extern char __VERIFIER_nondet_char() ;
  #line 24
  extern loff_t __VERIFIER_nondet_loff_t() ;
  #line 25
  extern size_t __VERIFIER_nondet_size_t() ;
  #line 5 "cprover/ddverify/src/ddverify/cdev.c"
  void call_cdev_functions(void) 
  { int cdev_no ;
    int result ;
    loff_t loff_t_value ;
    int int_value ;
    unsigned int uint_value ;
    unsigned long ulong_value ;
    char char_value ;
    size_t size_t_value ;
    unsigned short tmp ;
    int tmp___0 ;
    unsigned short tmp___1 ;
    int __cil_tmp12 ;
    int __cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    unsigned long __cil_tmp15 ;
    struct cdev *__cil_tmp16 ;
    unsigned long __cil_tmp17 ;
    unsigned long __cil_tmp18 ;
    struct file_operations  const  *__cil_tmp19 ;
    unsigned long __cil_tmp20 ;
    unsigned long __cil_tmp21 ;
    loff_t *__cil_tmp22 ;
    unsigned long __cil_tmp23 ;
    unsigned long __cil_tmp24 ;
    struct cdev *__cil_tmp25 ;
    unsigned long __cil_tmp26 ;
    unsigned long __cil_tmp27 ;
    struct file_operations  const  *__cil_tmp28 ;
    unsigned long __cil_tmp29 ;
    unsigned long __cil_tmp30 ;
    loff_t (*__cil_tmp31)(struct file * , loff_t  , int  ) ;
    unsigned long __cil_tmp32 ;
    unsigned long __cil_tmp33 ;
    unsigned long __cil_tmp34 ;
    struct file *__cil_tmp35 ;
    loff_t *__cil_tmp36 ;
    loff_t __cil_tmp37 ;
    unsigned long __cil_tmp38 ;
    unsigned long __cil_tmp39 ;
    struct cdev *__cil_tmp40 ;
    unsigned long __cil_tmp41 ;
    unsigned long __cil_tmp42 ;
    struct file_operations  const  *__cil_tmp43 ;
    unsigned long __cil_tmp44 ;
    unsigned long __cil_tmp45 ;
    char *__cil_tmp46 ;
    unsigned long __cil_tmp47 ;
    unsigned long __cil_tmp48 ;
    struct cdev *__cil_tmp49 ;
    unsigned long __cil_tmp50 ;
    unsigned long __cil_tmp51 ;
    struct file_operations  const  *__cil_tmp52 ;
    unsigned long __cil_tmp53 ;
    unsigned long __cil_tmp54 ;
    ssize_t (*__cil_tmp55)(struct file * , char * , size_t  , loff_t * ) ;
    unsigned long __cil_tmp56 ;
    unsigned long __cil_tmp57 ;
    unsigned long __cil_tmp58 ;
    struct file *__cil_tmp59 ;
    unsigned long __cil_tmp60 ;
    unsigned long __cil_tmp61 ;
    struct cdev *__cil_tmp62 ;
    unsigned long __cil_tmp63 ;
    unsigned long __cil_tmp64 ;
    struct file_operations  const  *__cil_tmp65 ;
    unsigned long __cil_tmp66 ;
    unsigned long __cil_tmp67 ;
    char *__cil_tmp68 ;
    unsigned long __cil_tmp69 ;
    unsigned long __cil_tmp70 ;
    struct cdev *__cil_tmp71 ;
    unsigned long __cil_tmp72 ;
    unsigned long __cil_tmp73 ;
    struct file_operations  const  *__cil_tmp74 ;
    unsigned long __cil_tmp75 ;
    unsigned long __cil_tmp76 ;
    ssize_t (*__cil_tmp77)(struct file * , char const   * , size_t  , loff_t * ) ;
    unsigned long __cil_tmp78 ;
    unsigned long __cil_tmp79 ;
    unsigned long __cil_tmp80 ;
    struct file *__cil_tmp81 ;
    char const   *__cil_tmp82 ;
    unsigned long __cil_tmp83 ;
    unsigned long __cil_tmp84 ;
    struct cdev *__cil_tmp85 ;
    unsigned long __cil_tmp86 ;
    unsigned long __cil_tmp87 ;
    struct file_operations  const  *__cil_tmp88 ;
    unsigned long __cil_tmp89 ;
    unsigned long __cil_tmp90 ;
    unsigned long __cil_tmp91 ;
    unsigned long __cil_tmp92 ;
    struct cdev *__cil_tmp93 ;
    unsigned long __cil_tmp94 ;
    unsigned long __cil_tmp95 ;
    struct file_operations  const  *__cil_tmp96 ;
    unsigned long __cil_tmp97 ;
    unsigned long __cil_tmp98 ;
    int (*__cil_tmp99)(struct inode * , struct file * , unsigned int  , unsigned long  ) ;
    unsigned long __cil_tmp100 ;
    unsigned long __cil_tmp101 ;
    unsigned long __cil_tmp102 ;
    struct inode *__cil_tmp103 ;
    unsigned long __cil_tmp104 ;
    unsigned long __cil_tmp105 ;
    unsigned long __cil_tmp106 ;
    struct file *__cil_tmp107 ;
    unsigned long __cil_tmp108 ;
    unsigned long __cil_tmp109 ;
    struct cdev *__cil_tmp110 ;
    unsigned long __cil_tmp111 ;
    unsigned long __cil_tmp112 ;
    struct file_operations  const  *__cil_tmp113 ;
    unsigned long __cil_tmp114 ;
    unsigned long __cil_tmp115 ;
    unsigned long __cil_tmp116 ;
    unsigned long __cil_tmp117 ;
    unsigned long __cil_tmp118 ;
    int __cil_tmp119 ;
    unsigned long __cil_tmp120 ;
    unsigned long __cil_tmp121 ;
    struct cdev *__cil_tmp122 ;
    unsigned long __cil_tmp123 ;
    unsigned long __cil_tmp124 ;
    struct file_operations  const  *__cil_tmp125 ;
    unsigned long __cil_tmp126 ;
    unsigned long __cil_tmp127 ;
    int (*__cil_tmp128)(struct inode * , struct file * ) ;
    unsigned long __cil_tmp129 ;
    unsigned long __cil_tmp130 ;
    unsigned long __cil_tmp131 ;
    struct inode *__cil_tmp132 ;
    unsigned long __cil_tmp133 ;
    unsigned long __cil_tmp134 ;
    unsigned long __cil_tmp135 ;
    struct file *__cil_tmp136 ;
    unsigned long __cil_tmp137 ;
    unsigned long __cil_tmp138 ;
    unsigned long __cil_tmp139 ;
    unsigned long __cil_tmp140 ;
    unsigned long __cil_tmp141 ;
    struct cdev *__cil_tmp142 ;
    unsigned long __cil_tmp143 ;
    unsigned long __cil_tmp144 ;
    struct file_operations  const  *__cil_tmp145 ;
    unsigned long __cil_tmp146 ;
    unsigned long __cil_tmp147 ;
    unsigned long __cil_tmp148 ;
    unsigned long __cil_tmp149 ;
    unsigned long __cil_tmp150 ;
    unsigned long __cil_tmp151 ;
    unsigned long __cil_tmp152 ;
    struct cdev *__cil_tmp153 ;
    unsigned long __cil_tmp154 ;
    unsigned long __cil_tmp155 ;
    struct file_operations  const  *__cil_tmp156 ;
    unsigned long __cil_tmp157 ;
    unsigned long __cil_tmp158 ;
    int (*__cil_tmp159)(struct inode * , struct file * ) ;
    unsigned long __cil_tmp160 ;
    unsigned long __cil_tmp161 ;
    unsigned long __cil_tmp162 ;
    struct inode *__cil_tmp163 ;
    unsigned long __cil_tmp164 ;
    unsigned long __cil_tmp165 ;
    unsigned long __cil_tmp166 ;
    struct file *__cil_tmp167 ;
    unsigned long __cil_tmp168 ;
    unsigned long __cil_tmp169 ;
    unsigned long __cil_tmp170 ;
  
    {
    {
  #line 16
    __cil_tmp12 = (int )number_cdev_registered;
  #line 16
    if (__cil_tmp12 == 0) {
  #line 17
      return;
    } else {
  
    }
    }
    {
  #line 20
    tmp = __VERIFIER_nondet_ushort();
  #line 20
    cdev_no = (int )tmp;
    }
  #line 21
    if (0 <= cdev_no) {
      {
  #line 21
      __cil_tmp13 = (int )number_cdev_registered;
  #line 21
      if (cdev_no < __cil_tmp13) {
  #line 21
        tmp___0 = 1;
      } else {
  #line 21
        tmp___0 = 0;
      }
      }
    } else {
  #line 21
      tmp___0 = 0;
    }
    {
  #line 21
    __CPROVER_assume(tmp___0);
  #line 23
    tmp___1 = __VERIFIER_nondet_ushort();
    }
    {
  #line 24
    if ((int )tmp___1 == 0) {
  #line 24
      goto case_0;
    } else {
  
    }
  #line 34
    if ((int )tmp___1 == 1) {
  #line 34
      goto case_1;
    } else {
  
    }
  #line 45
    if ((int )tmp___1 == 2) {
  #line 45
      goto case_2;
    } else {
  
    }
  #line 48
    if ((int )tmp___1 == 3) {
  #line 48
      goto case_3;
    } else {
  
    }
  #line 59
    if ((int )tmp___1 == 4) {
  #line 59
      goto case_4;
    } else {
  
    }
  #line 62
    if ((int )tmp___1 == 5) {
  #line 62
      goto case_5;
    } else {
  
    }
  #line 65
    if ((int )tmp___1 == 6) {
  #line 65
      goto case_6;
    } else {
  
    }
  #line 68
    if ((int )tmp___1 == 7) {
  #line 68
      goto case_7;
    } else {
  
    }
  #line 80
    if ((int )tmp___1 == 8) {
  #line 80
      goto case_8;
    } else {
  
    }
  #line 83
    if ((int )tmp___1 == 9) {
  #line 83
      goto case_9;
    } else {
  
    }
  #line 86
    if ((int )tmp___1 == 10) {
  #line 86
      goto case_10;
    } else {
  
    }
  #line 89
    if ((int )tmp___1 == 11) {
  #line 89
      goto case_11;
    } else {
  
    }
  #line 100
    if ((int )tmp___1 == 12) {
  #line 100
      goto case_12;
    } else {
  
    }
  #line 103
    if ((int )tmp___1 == 13) {
  #line 103
      goto case_13;
    } else {
  
    }
  #line 114
    if ((int )tmp___1 == 14) {
  #line 114
      goto case_14;
    } else {
  
    }
  #line 117
    if ((int )tmp___1 == 15) {
  #line 117
      goto case_15;
    } else {
  
    }
  #line 120
    if ((int )tmp___1 == 16) {
  #line 120
      goto case_16;
    } else {
  
    }
  #line 123
    if ((int )tmp___1 == 17) {
  #line 123
      goto case_17;
    } else {
  
    }
  #line 126
    if ((int )tmp___1 == 18) {
  #line 126
      goto case_18;
    } else {
  
    }
  #line 129
    if ((int )tmp___1 == 19) {
  #line 129
      goto case_19;
    } else {
  
    }
  #line 132
    if ((int )tmp___1 == 20) {
  #line 132
      goto case_20;
    } else {
  
    }
  #line 135
    if ((int )tmp___1 == 21) {
  #line 135
      goto case_21;
    } else {
  
    }
  #line 138
    if ((int )tmp___1 == 22) {
  #line 138
      goto case_22;
    } else {
  
    }
  #line 141
    if ((int )tmp___1 == 23) {
  #line 141
      goto case_23;
    } else {
  
    }
  #line 144
    if ((int )tmp___1 == 24) {
  #line 144
      goto case_24;
    } else {
  
    }
  #line 147
    if ((int )tmp___1 == 25) {
  #line 147
      goto case_25;
    } else {
  
    }
  #line 150
    if ((int )tmp___1 == 26) {
  #line 150
      goto case_26;
    } else {
  
    }
  #line 153
    goto switch_default;
    case_0: /* CIL Label */ 
    {
  #line 25
    __cil_tmp14 = cdev_no * 96UL;
  #line 25
    __cil_tmp15 = (unsigned long )(cdev_registered) + __cil_tmp14;
  #line 25
    __cil_tmp16 = *((struct cdev **)__cil_tmp15);
  #line 25
    __cil_tmp17 = (unsigned long )__cil_tmp16;
  #line 25
    __cil_tmp18 = __cil_tmp17 + 8;
  #line 25
    __cil_tmp19 = *((struct file_operations  const  **)__cil_tmp18);
  #line 25
    __cil_tmp20 = (unsigned long )__cil_tmp19;
  #line 25
    __cil_tmp21 = __cil_tmp20 + 8;
  #line 25
    if (*((loff_t (* const  *)(struct file * , loff_t  , int  ))__cil_tmp21)) {
      {
  #line 26
      __cil_tmp22 = & loff_t_value;
  #line 26
      *__cil_tmp22 = __VERIFIER_nondet_loff_t();
  #line 27
      int_value = __VERIFIER_nondet_int();
  #line 29
      __cil_tmp23 = cdev_no * 96UL;
  #line 29
      __cil_tmp24 = (unsigned long )(cdev_registered) + __cil_tmp23;
  #line 29
      __cil_tmp25 = *((struct cdev **)__cil_tmp24);
  #line 29
      __cil_tmp26 = (unsigned long )__cil_tmp25;
  #line 29
      __cil_tmp27 = __cil_tmp26 + 8;
  #line 29
      __cil_tmp28 = *((struct file_operations  const  **)__cil_tmp27);
  #line 29
      __cil_tmp29 = (unsigned long )__cil_tmp28;
  #line 29
      __cil_tmp30 = __cil_tmp29 + 8;
  #line 29
      __cil_tmp31 = *((loff_t (* const  *)(struct file * , loff_t  , int  ))__cil_tmp30);
  #line 29
      __cil_tmp32 = cdev_no * 96UL;
  #line 29
      __cil_tmp33 = __cil_tmp32 + 8;
  #line 29
      __cil_tmp34 = (unsigned long )(cdev_registered) + __cil_tmp33;
  #line 29
      __cil_tmp35 = (struct file *)__cil_tmp34;
  #line 29
      __cil_tmp36 = & loff_t_value;
  #line 29
      __cil_tmp37 = *__cil_tmp36;
  #line 29
      (*__cil_tmp31)(__cil_tmp35, __cil_tmp37, int_value);
      }
    } else {
  
    }
    }
  #line 33
    goto switch_break;
    case_1: /* CIL Label */ 
    {
  #line 35
    __cil_tmp38 = cdev_no * 96UL;
  #line 35
    __cil_tmp39 = (unsigned long )(cdev_registered) + __cil_tmp38;
  #line 35
    __cil_tmp40 = *((struct cdev **)__cil_tmp39);
  #line 35
    __cil_tmp41 = (unsigned long )__cil_tmp40;
  #line 35
    __cil_tmp42 = __cil_tmp41 + 8;
  #line 35
    __cil_tmp43 = *((struct file_operations  const  **)__cil_tmp42);
  #line 35
    __cil_tmp44 = (unsigned long )__cil_tmp43;
  #line 35
    __cil_tmp45 = __cil_tmp44 + 16;
  #line 35
    if (*((ssize_t (* const  *)(struct file * , char * , size_t  , loff_t * ))__cil_tmp45)) {
      {
  #line 36
      __cil_tmp46 = & char_value;
  #line 36
      *__cil_tmp46 = __VERIFIER_nondet_char();
  #line 37
      size_t_value = __VERIFIER_nondet_size_t();
  #line 39
      __cil_tmp47 = cdev_no * 96UL;
  #line 39
      __cil_tmp48 = (unsigned long )(cdev_registered) + __cil_tmp47;
  #line 39
      __cil_tmp49 = *((struct cdev **)__cil_tmp48);
  #line 39
      __cil_tmp50 = (unsigned long )__cil_tmp49;
  #line 39
      __cil_tmp51 = __cil_tmp50 + 8;
  #line 39
      __cil_tmp52 = *((struct file_operations  const  **)__cil_tmp51);
  #line 39
      __cil_tmp53 = (unsigned long )__cil_tmp52;
  #line 39
      __cil_tmp54 = __cil_tmp53 + 16;
  #line 39
      __cil_tmp55 = *((ssize_t (* const  *)(struct file * , char * , size_t  , loff_t * ))__cil_tmp54);
  #line 39
      __cil_tmp56 = cdev_no * 96UL;
  #line 39
      __cil_tmp57 = __cil_tmp56 + 8;
  #line 39
      __cil_tmp58 = (unsigned long )(cdev_registered) + __cil_tmp57;
  #line 39
      __cil_tmp59 = (struct file *)__cil_tmp58;
  #line 39
      (*__cil_tmp55)(__cil_tmp59, & char_value, size_t_value, & loff_t_value);
      }
    } else {
  
    }
    }
  #line 44
    goto switch_break;
    case_2: /* CIL Label */ 
  #line 47
    goto switch_break;
    case_3: /* CIL Label */ 
    {
  #line 49
    __cil_tmp60 = cdev_no * 96UL;
  #line 49
    __cil_tmp61 = (unsigned long )(cdev_registered) + __cil_tmp60;
  #line 49
    __cil_tmp62 = *((struct cdev **)__cil_tmp61);
  #line 49
    __cil_tmp63 = (unsigned long )__cil_tmp62;
  #line 49
    __cil_tmp64 = __cil_tmp63 + 8;
  #line 49
    __cil_tmp65 = *((struct file_operations  const  **)__cil_tmp64);
  #line 49
    __cil_tmp66 = (unsigned long )__cil_tmp65;
  #line 49
    __cil_tmp67 = __cil_tmp66 + 24;
  #line 49
    if (*((ssize_t (* const  *)(struct file * , char const   * , size_t  , loff_t * ))__cil_tmp67)) {
      {
  #line 50
      __cil_tmp68 = & char_value;
  #line 50
      *__cil_tmp68 = __VERIFIER_nondet_char();
  #line 51
      size_t_value = __VERIFIER_nondet_size_t();
  #line 53
      __cil_tmp69 = cdev_no * 96UL;
  #line 53
      __cil_tmp70 = (unsigned long )(cdev_registered) + __cil_tmp69;
  #line 53
      __cil_tmp71 = *((struct cdev **)__cil_tmp70);
  #line 53
      __cil_tmp72 = (unsigned long )__cil_tmp71;
  #line 53
      __cil_tmp73 = __cil_tmp72 + 8;
  #line 53
      __cil_tmp74 = *((struct file_operations  const  **)__cil_tmp73);
  #line 53
      __cil_tmp75 = (unsigned long )__cil_tmp74;
  #line 53
      __cil_tmp76 = __cil_tmp75 + 24;
  #line 53
      __cil_tmp77 = *((ssize_t (* const  *)(struct file * , char const   * , size_t  ,
                                            loff_t * ))__cil_tmp76);
  #line 53
      __cil_tmp78 = cdev_no * 96UL;
  #line 53
      __cil_tmp79 = __cil_tmp78 + 8;
  #line 53
      __cil_tmp80 = (unsigned long )(cdev_registered) + __cil_tmp79;
  #line 53
      __cil_tmp81 = (struct file *)__cil_tmp80;
  #line 53
      __cil_tmp82 = (char const   *)(& char_value);
  #line 53
      (*__cil_tmp77)(__cil_tmp81, __cil_tmp82, size_t_value, & loff_t_value);
      }
    } else {
  
    }
    }
  #line 58
    goto switch_break;
    case_4: /* CIL Label */ 
  #line 61
    goto switch_break;
    case_5: /* CIL Label */ 
  #line 64
    goto switch_break;
    case_6: /* CIL Label */ 
  #line 67
    goto switch_break;
    case_7: /* CIL Label */ 
    {
  #line 69
    __cil_tmp83 = cdev_no * 96UL;
  #line 69
    __cil_tmp84 = (unsigned long )(cdev_registered) + __cil_tmp83;
  #line 69
    __cil_tmp85 = *((struct cdev **)__cil_tmp84);
  #line 69
    __cil_tmp86 = (unsigned long )__cil_tmp85;
  #line 69
    __cil_tmp87 = __cil_tmp86 + 8;
  #line 69
    __cil_tmp88 = *((struct file_operations  const  **)__cil_tmp87);
  #line 69
    __cil_tmp89 = (unsigned long )__cil_tmp88;
  #line 69
    __cil_tmp90 = __cil_tmp89 + 48;
  #line 69
    if (*((int (* const  *)(struct inode * , struct file * , unsigned int  , unsigned long  ))__cil_tmp90)) {
      {
  #line 70
      uint_value = __VERIFIER_nondet_uint();
  #line 71
      ulong_value = __VERIFIER_nondet_ulong();
  #line 73
      __cil_tmp91 = cdev_no * 96UL;
  #line 73
      __cil_tmp92 = (unsigned long )(cdev_registered) + __cil_tmp91;
  #line 73
      __cil_tmp93 = *((struct cdev **)__cil_tmp92);
  #line 73
      __cil_tmp94 = (unsigned long )__cil_tmp93;
  #line 73
      __cil_tmp95 = __cil_tmp94 + 8;
  #line 73
      __cil_tmp96 = *((struct file_operations  const  **)__cil_tmp95);
  #line 73
      __cil_tmp97 = (unsigned long )__cil_tmp96;
  #line 73
      __cil_tmp98 = __cil_tmp97 + 48;
  #line 73
      __cil_tmp99 = *((int (* const  *)(struct inode * , struct file * , unsigned int  ,
                                        unsigned long  ))__cil_tmp98);
  #line 73
      __cil_tmp100 = cdev_no * 96UL;
  #line 73
      __cil_tmp101 = __cil_tmp100 + 64;
  #line 73
      __cil_tmp102 = (unsigned long )(cdev_registered) + __cil_tmp101;
  #line 73
      __cil_tmp103 = (struct inode *)__cil_tmp102;
  #line 73
      __cil_tmp104 = cdev_no * 96UL;
  #line 73
      __cil_tmp105 = __cil_tmp104 + 8;
  #line 73
      __cil_tmp106 = (unsigned long )(cdev_registered) + __cil_tmp105;
  #line 73
      __cil_tmp107 = (struct file *)__cil_tmp106;
  #line 73
      (*__cil_tmp99)(__cil_tmp103, __cil_tmp107, uint_value, ulong_value);
      }
    } else {
  
    }
    }
  #line 79
    goto switch_break;
    case_8: /* CIL Label */ 
  #line 82
    goto switch_break;
    case_9: /* CIL Label */ 
  #line 85
    goto switch_break;
    case_10: /* CIL Label */ 
  #line 88
    goto switch_break;
    case_11: /* CIL Label */ 
    {
  #line 90
    __cil_tmp108 = cdev_no * 96UL;
  #line 90
    __cil_tmp109 = (unsigned long )(cdev_registered) + __cil_tmp108;
  #line 90
    __cil_tmp110 = *((struct cdev **)__cil_tmp109);
  #line 90
    __cil_tmp111 = (unsigned long )__cil_tmp110;
  #line 90
    __cil_tmp112 = __cil_tmp111 + 8;
  #line 90
    __cil_tmp113 = *((struct file_operations  const  **)__cil_tmp112);
  #line 90
    __cil_tmp114 = (unsigned long )__cil_tmp113;
  #line 90
    __cil_tmp115 = __cil_tmp114 + 80;
  #line 90
    if (*((int (* const  *)(struct inode * , struct file * ))__cil_tmp115)) {
      {
  #line 90
      __cil_tmp116 = cdev_no * 96UL;
  #line 90
      __cil_tmp117 = __cil_tmp116 + 88;
  #line 90
      __cil_tmp118 = (unsigned long )(cdev_registered) + __cil_tmp117;
  #line 90
      __cil_tmp119 = *((int *)__cil_tmp118);
  #line 90
      if (! __cil_tmp119) {
        {
  #line 92
        __cil_tmp120 = cdev_no * 96UL;
  #line 92
        __cil_tmp121 = (unsigned long )(cdev_registered) + __cil_tmp120;
  #line 92
        __cil_tmp122 = *((struct cdev **)__cil_tmp121);
  #line 92
        __cil_tmp123 = (unsigned long )__cil_tmp122;
  #line 92
        __cil_tmp124 = __cil_tmp123 + 8;
  #line 92
        __cil_tmp125 = *((struct file_operations  const  **)__cil_tmp124);
  #line 92
        __cil_tmp126 = (unsigned long )__cil_tmp125;
  #line 92
        __cil_tmp127 = __cil_tmp126 + 80;
  #line 92
        __cil_tmp128 = *((int (* const  *)(struct inode * , struct file * ))__cil_tmp127);
  #line 92
        __cil_tmp129 = cdev_no * 96UL;
  #line 92
        __cil_tmp130 = __cil_tmp129 + 64;
  #line 92
        __cil_tmp131 = (unsigned long )(cdev_registered) + __cil_tmp130;
  #line 92
        __cil_tmp132 = (struct inode *)__cil_tmp131;
  #line 92
        __cil_tmp133 = cdev_no * 96UL;
  #line 92
        __cil_tmp134 = __cil_tmp133 + 8;
  #line 92
        __cil_tmp135 = (unsigned long )(cdev_registered) + __cil_tmp134;
  #line 92
        __cil_tmp136 = (struct file *)__cil_tmp135;
  #line 92
        result = (*__cil_tmp128)(__cil_tmp132, __cil_tmp136);
        }
  #line 95
        if (! result) {
  #line 96
          __cil_tmp137 = cdev_no * 96UL;
  #line 96
          __cil_tmp138 = __cil_tmp137 + 88;
  #line 96
          __cil_tmp139 = (unsigned long )(cdev_registered) + __cil_tmp138;
  #line 96
          *((int *)__cil_tmp139) = 1;
        } else {
  
        }
      } else {
  
      }
      }
    } else {
  
    }
    }
  #line 99
    goto switch_break;
    case_12: /* CIL Label */ 
  #line 102
    goto switch_break;
    case_13: /* CIL Label */ 
    {
  #line 104
    __cil_tmp140 = cdev_no * 96UL;
  #line 104
    __cil_tmp141 = (unsigned long )(cdev_registered) + __cil_tmp140;
  #line 104
    __cil_tmp142 = *((struct cdev **)__cil_tmp141);
  #line 104
    __cil_tmp143 = (unsigned long )__cil_tmp142;
  #line 104
    __cil_tmp144 = __cil_tmp143 + 8;
  #line 104
    __cil_tmp145 = *((struct file_operations  const  **)__cil_tmp144);
  #line 104
    __cil_tmp146 = (unsigned long )__cil_tmp145;
  #line 104
    __cil_tmp147 = __cil_tmp146 + 96;
  #line 104
    if (*((int (* const  *)(struct inode * , struct file * ))__cil_tmp147)) {
      {
  #line 104
      __cil_tmp148 = cdev_no * 96UL;
  #line 104
      __cil_tmp149 = __cil_tmp148 + 88;
  #line 104
      __cil_tmp150 = (unsigned long )(cdev_registered) + __cil_tmp149;
  #line 104
      if (*((int *)__cil_tmp150)) {
        {
  #line 106
        __cil_tmp151 = cdev_no * 96UL;
  #line 106
        __cil_tmp152 = (unsigned long )(cdev_registered) + __cil_tmp151;
  #line 106
        __cil_tmp153 = *((struct cdev **)__cil_tmp152);
  #line 106
        __cil_tmp154 = (unsigned long )__cil_tmp153;
  #line 106
        __cil_tmp155 = __cil_tmp154 + 8;
  #line 106
        __cil_tmp156 = *((struct file_operations  const  **)__cil_tmp155);
  #line 106
        __cil_tmp157 = (unsigned long )__cil_tmp156;
  #line 106
        __cil_tmp158 = __cil_tmp157 + 96;
  #line 106
        __cil_tmp159 = *((int (* const  *)(struct inode * , struct file * ))__cil_tmp158);
  #line 106
        __cil_tmp160 = cdev_no * 96UL;
  #line 106
        __cil_tmp161 = __cil_tmp160 + 64;
  #line 106
        __cil_tmp162 = (unsigned long )(cdev_registered) + __cil_tmp161;
  #line 106
        __cil_tmp163 = (struct inode *)__cil_tmp162;
  #line 106
        __cil_tmp164 = cdev_no * 96UL;
  #line 106
        __cil_tmp165 = __cil_tmp164 + 8;
  #line 106
        __cil_tmp166 = (unsigned long )(cdev_registered) + __cil_tmp165;
  #line 106
        __cil_tmp167 = (struct file *)__cil_tmp166;
  #line 106
        result = (*__cil_tmp159)(__cil_tmp163, __cil_tmp167);
        }
  #line 109
        if (! result) {
  #line 110
          __cil_tmp168 = cdev_no * 96UL;
  #line 110
          __cil_tmp169 = __cil_tmp168 + 88;
  #line 110
          __cil_tmp170 = (unsigned long )(cdev_registered) + __cil_tmp169;
  #line 110
          *((int *)__cil_tmp170) = 0;
        } else {
  
        }
      } else {
  
      }
      }
    } else {
  
    }
    }
  #line 113
    goto switch_break;
    case_14: /* CIL Label */ 
  #line 116
    goto switch_break;
    case_15: /* CIL Label */ 
  #line 119
    goto switch_break;
    case_16: /* CIL Label */ 
  #line 122
    goto switch_break;
    case_17: /* CIL Label */ 
  #line 125
    goto switch_break;
    case_18: /* CIL Label */ 
  #line 128
    goto switch_break;
    case_19: /* CIL Label */ 
  #line 131
    goto switch_break;
    case_20: /* CIL Label */ 
  #line 134
    goto switch_break;
    case_21: /* CIL Label */ 
  #line 137
    goto switch_break;
    case_22: /* CIL Label */ 
  #line 140
    goto switch_break;
    case_23: /* CIL Label */ 
  #line 143
    goto switch_break;
    case_24: /* CIL Label */ 
  #line 146
    goto switch_break;
    case_25: /* CIL Label */ 
  #line 149
    goto switch_break;
    case_26: /* CIL Label */ 
  #line 152
    goto switch_break;
    switch_default: /* CIL Label */ 
  #line 154
    goto switch_break;
    switch_break: /* CIL Label */ ;
    }
  #line 156
    return;
  }
  }
  #line 1 "preproc_iJkaSX.o"
  #pragma merger(0,"preproc_iJkaSX.i","-x,c")
  #line 10 "cprover/ddverify/src/ddverify/interrupt.c"
  void call_interrupt_handler(void) 
  { unsigned short i ;
    struct pt_regs regs ;
    int tmp ;
    int __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    irqreturn_t (*__cil_tmp10)(int  , void * , struct pt_regs * ) ;
    int __cil_tmp11 ;
    unsigned long __cil_tmp12 ;
    unsigned long __cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    void *__cil_tmp15 ;
  
    {
    {
  #line 15
    tmp = __VERIFIER_nondet_int();
  #line 15
    i = (unsigned short )tmp;
  #line 16
    __cil_tmp4 = (int )i;
  #line 16
    __cil_tmp5 = __cil_tmp4 < 16;
  #line 16
    __CPROVER_assume(__cil_tmp5);
    }
    {
  #line 18
    __cil_tmp6 = i * 16UL;
  #line 18
    __cil_tmp7 = (unsigned long )(registered_irq) + __cil_tmp6;
  #line 18
    if (*((irqreturn_t (**)(int  , void * , struct pt_regs * ))__cil_tmp7)) {
      {
  #line 19
      __cil_tmp8 = i * 16UL;
  #line 19
      __cil_tmp9 = (unsigned long )(registered_irq) + __cil_tmp8;
  #line 19
      __cil_tmp10 = *((irqreturn_t (**)(int  , void * , struct pt_regs * ))__cil_tmp9);
  #line 19
      __cil_tmp11 = (int )i;
  #line 19
      __cil_tmp12 = i * 16UL;
  #line 19
      __cil_tmp13 = __cil_tmp12 + 8;
  #line 19
      __cil_tmp14 = (unsigned long )(registered_irq) + __cil_tmp13;
  #line 19
      __cil_tmp15 = *((void **)__cil_tmp14);
  #line 19
      (*__cil_tmp10)(__cil_tmp11, __cil_tmp15, & regs);
      }
    } else {
  
    }
    }
  #line 22
    return;
  }
  }
  #line 1 "preproc_03bMmn.o"
  #pragma merger(0,"preproc_03bMmn.i","-x,c")
  #line 1 "preproc_2XrEkf.o"
  #pragma merger(0,"preproc_2XrEkf.i","-x,c")
  #line 16 "cprover/ddverify/include/ddverify/pci.h"
  int pci_probe_device(void) ;
  #line 17
  void pci_remove_device(void) ;
  #line 19
  void call_pci_functions(void) ;
  #line 7 "cprover/ddverify/src/ddverify/pci.c"
  void create_pci_dev(void) 
  { 
  
    {
  #line 9
    return;
  }
  }
  #line 11 "cprover/ddverify/src/ddverify/pci.c"
  int pci_probe_device(void) 
  { int err ;
    unsigned int dev_id ;
    unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    unsigned int __cil_tmp5 ;
    int __cil_tmp6 ;
    struct ddv_pci_driver *__cil_tmp7 ;
    struct pci_driver *__cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    int (*__cil_tmp11)(struct pci_dev *dev , struct pci_device_id  const  *id ) ;
    unsigned long __cil_tmp12 ;
    struct pci_dev *__cil_tmp13 ;
    struct ddv_pci_driver *__cil_tmp14 ;
    struct pci_driver *__cil_tmp15 ;
    unsigned long __cil_tmp16 ;
    unsigned long __cil_tmp17 ;
    struct pci_device_id  const  *__cil_tmp18 ;
    struct pci_device_id  const  *__cil_tmp19 ;
    unsigned long __cil_tmp20 ;
  
    {
    {
  #line 16
    __cil_tmp3 = (unsigned long )(& registered_pci_driver) + 448;
  #line 16
    *((unsigned int *)__cil_tmp3) = 1U;
  #line 18
    dev_id = __VERIFIER_nondet_uint();
  #line 19
    __cil_tmp4 = (unsigned long )(& registered_pci_driver) + 448;
  #line 19
    __cil_tmp5 = *((unsigned int *)__cil_tmp4);
  #line 19
    __cil_tmp6 = dev_id < __cil_tmp5;
  #line 19
    __CPROVER_assume(__cil_tmp6);
  #line 21
    __cil_tmp7 = & registered_pci_driver;
  #line 21
    __cil_tmp8 = *((struct pci_driver **)__cil_tmp7);
  #line 21
    __cil_tmp9 = (unsigned long )__cil_tmp8;
  #line 21
    __cil_tmp10 = __cil_tmp9 + 16;
  #line 21
    __cil_tmp11 = *((int (**)(struct pci_dev *dev , struct pci_device_id  const  *id ))__cil_tmp10);
  #line 21
    __cil_tmp12 = (unsigned long )(& registered_pci_driver) + 8;
  #line 21
    __cil_tmp13 = (struct pci_dev *)__cil_tmp12;
  #line 21
    __cil_tmp14 = & registered_pci_driver;
  #line 21
    __cil_tmp15 = *((struct pci_driver **)__cil_tmp14);
  #line 21
    __cil_tmp16 = (unsigned long )__cil_tmp15;
  #line 21
    __cil_tmp17 = __cil_tmp16 + 8;
  #line 21
    __cil_tmp18 = *((struct pci_device_id  const  **)__cil_tmp17);
  #line 21
    __cil_tmp19 = __cil_tmp18 + dev_id;
  #line 21
    err = (*__cil_tmp11)(__cil_tmp13, __cil_tmp19);
    }
  #line 24
    if (! err) {
  #line 25
      __cil_tmp20 = (unsigned long )(& registered_pci_driver) + 452;
  #line 25
      *((int *)__cil_tmp20) = 1;
    } else {
  
    }
  #line 28
    return (err);
  }
  }
  #line 31 "cprover/ddverify/src/ddverify/pci.c"
  void pci_remove_device(void) 
  { struct ddv_pci_driver *__cil_tmp1 ;
    struct pci_driver *__cil_tmp2 ;
    unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    void (*__cil_tmp5)(struct pci_dev *dev ) ;
    unsigned long __cil_tmp6 ;
    struct pci_dev *__cil_tmp7 ;
    unsigned long __cil_tmp8 ;
  
    {
    {
  #line 33
    __cil_tmp1 = & registered_pci_driver;
  #line 33
    __cil_tmp2 = *((struct pci_driver **)__cil_tmp1);
  #line 33
    __cil_tmp3 = (unsigned long )__cil_tmp2;
  #line 33
    __cil_tmp4 = __cil_tmp3 + 24;
  #line 33
    __cil_tmp5 = *((void (**)(struct pci_dev *dev ))__cil_tmp4);
  #line 33
    __cil_tmp6 = (unsigned long )(& registered_pci_driver) + 8;
  #line 33
    __cil_tmp7 = (struct pci_dev *)__cil_tmp6;
  #line 33
    (*__cil_tmp5)(__cil_tmp7);
  #line 35
    __cil_tmp8 = (unsigned long )(& registered_pci_driver) + 452;
  #line 35
    *((int *)__cil_tmp8) = 0;
    }
  #line 36
    return;
  }
  }
  #line 38 "cprover/ddverify/src/ddverify/pci.c"
  void call_pci_functions(void) 
  { unsigned int tmp ;
    unsigned long __cil_tmp2 ;
    int __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
  
    {
    {
  #line 40
    tmp = __VERIFIER_nondet_uint();
    }
    {
  #line 41
    if ((int )tmp == 0) {
  #line 41
      goto case_0;
    } else {
  
    }
  #line 46
    if ((int )tmp == 1) {
  #line 46
      goto case_1;
    } else {
  
    }
  #line 52
    goto switch_default;
    case_0: /* CIL Label */ 
    {
  #line 42
    __cil_tmp2 = (unsigned long )(& registered_pci_driver) + 452;
  #line 42
    __cil_tmp3 = *((int *)__cil_tmp2);
  #line 42
    if (! __cil_tmp3) {
      {
  #line 43
      pci_probe_device();
      }
    } else {
  
    }
    }
  #line 45
    goto switch_break;
    case_1: /* CIL Label */ 
    {
  #line 48
    __cil_tmp4 = (unsigned long )(& registered_pci_driver) + 452;
  #line 48
    if (*((int *)__cil_tmp4)) {
      {
  #line 49
      pci_remove_device();
      }
    } else {
  
    }
    }
  #line 51
    goto switch_break;
    switch_default: /* CIL Label */ 
  #line 54
    goto switch_break;
    switch_break: /* CIL Label */ ;
    }
  #line 56
    return;
  }
  }
  #line 1 "preproc_4B4eRJ.o"
  #pragma merger(0,"preproc_4B4eRJ.i","-x,c")
  #line 3 "cprover/ddverify/src/ddverify/tasklet.c"
  void call_tasklet_functions(void) 
  { unsigned int i ;
    int __cil_tmp2 ;
    void *__cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    unsigned long __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    struct tasklet_struct *__cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    struct tasklet_struct *__cil_tmp11 ;
    atomic_t __cil_tmp12 ;
    unsigned long __cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    unsigned long __cil_tmp15 ;
    unsigned long __cil_tmp16 ;
    unsigned long __cil_tmp17 ;
    struct tasklet_struct *__cil_tmp18 ;
    unsigned long __cil_tmp19 ;
    unsigned long __cil_tmp20 ;
    void (*__cil_tmp21)(unsigned long  ) ;
    unsigned long __cil_tmp22 ;
    unsigned long __cil_tmp23 ;
    struct tasklet_struct *__cil_tmp24 ;
    unsigned long __cil_tmp25 ;
    unsigned long __cil_tmp26 ;
    unsigned long __cil_tmp27 ;
    unsigned long __cil_tmp28 ;
    unsigned long __cil_tmp29 ;
    unsigned long __cil_tmp30 ;
    unsigned long __cil_tmp31 ;
    unsigned long __cil_tmp32 ;
    void *__cil_tmp33 ;
  
    {
    {
  #line 6
    __cil_tmp2 = i < 10U;
  #line 6
    __CPROVER_assume(__cil_tmp2);
    }
    {
  #line 8
    __cil_tmp3 = (void *)0;
  #line 8
    __cil_tmp4 = (unsigned long )__cil_tmp3;
  #line 8
    __cil_tmp5 = i * 16UL;
  #line 8
    __cil_tmp6 = (unsigned long )(tasklet_registered) + __cil_tmp5;
  #line 8
    __cil_tmp7 = *((struct tasklet_struct **)__cil_tmp6);
  #line 8
    __cil_tmp8 = (unsigned long )__cil_tmp7;
  #line 8
    if (__cil_tmp8 != __cil_tmp4) {
      {
  #line 8
      __cil_tmp9 = i * 16UL;
  #line 8
      __cil_tmp10 = (unsigned long )(tasklet_registered) + __cil_tmp9;
  #line 8
      __cil_tmp11 = *((struct tasklet_struct **)__cil_tmp10);
  #line 8
      __cil_tmp12 = *((atomic_t *)__cil_tmp11);
  #line 8
      if (__cil_tmp12 == 0) {
        {
  #line 10
        __cil_tmp13 = i * 16UL;
  #line 10
        __cil_tmp14 = __cil_tmp13 + 8;
  #line 10
        __cil_tmp15 = (unsigned long )(tasklet_registered) + __cil_tmp14;
  #line 10
        *((unsigned short *)__cil_tmp15) = (unsigned short)1;
  #line 11
        __cil_tmp16 = i * 16UL;
  #line 11
        __cil_tmp17 = (unsigned long )(tasklet_registered) + __cil_tmp16;
  #line 11
        __cil_tmp18 = *((struct tasklet_struct **)__cil_tmp17);
  #line 11
        __cil_tmp19 = (unsigned long )__cil_tmp18;
  #line 11
        __cil_tmp20 = __cil_tmp19 + 8;
  #line 11
        __cil_tmp21 = *((void (**)(unsigned long  ))__cil_tmp20);
  #line 11
        __cil_tmp22 = i * 16UL;
  #line 11
        __cil_tmp23 = (unsigned long )(tasklet_registered) + __cil_tmp22;
  #line 11
        __cil_tmp24 = *((struct tasklet_struct **)__cil_tmp23);
  #line 11
        __cil_tmp25 = (unsigned long )__cil_tmp24;
  #line 11
        __cil_tmp26 = __cil_tmp25 + 16;
  #line 11
        __cil_tmp27 = *((unsigned long *)__cil_tmp26);
  #line 11
        (*__cil_tmp21)(__cil_tmp27);
  #line 12
        __cil_tmp28 = i * 16UL;
  #line 12
        __cil_tmp29 = __cil_tmp28 + 8;
  #line 12
        __cil_tmp30 = (unsigned long )(tasklet_registered) + __cil_tmp29;
  #line 12
        *((unsigned short *)__cil_tmp30) = (unsigned short)0;
  #line 13
        __cil_tmp31 = i * 16UL;
  #line 13
        __cil_tmp32 = (unsigned long )(tasklet_registered) + __cil_tmp31;
  #line 13
        __cil_tmp33 = (void *)0;
  #line 13
        *((struct tasklet_struct **)__cil_tmp32) = (struct tasklet_struct *)__cil_tmp33;
        }
      } else {
  
      }
      }
    } else {
  
    }
    }
  #line 15
    return;
  }
  }
  #line 1 "preproc_mma9Wb.o"
  #pragma merger(0,"preproc_mma9Wb.i","-x,c")
  #line 4 "cprover/ddverify/src/ddverify/timer.c"
  void call_timer_functions(void) 
  { unsigned short i ;
    unsigned short tmp ;
    int __cil_tmp3 ;
    int __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    struct timer_list *__cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    unsigned long __cil_tmp11 ;
    unsigned long __cil_tmp12 ;
    struct timer_list *__cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    unsigned long __cil_tmp15 ;
    void (*__cil_tmp16)(unsigned long  ) ;
    unsigned long __cil_tmp17 ;
    unsigned long __cil_tmp18 ;
    struct timer_list *__cil_tmp19 ;
    unsigned long __cil_tmp20 ;
    unsigned long __cil_tmp21 ;
    unsigned long __cil_tmp22 ;
  
    {
    {
  #line 6
    tmp = __VERIFIER_nondet_ushort();
  #line 6
    i = tmp;
  #line 8
    __cil_tmp3 = (int )number_timer_registered;
  #line 8
    __cil_tmp4 = (int )i;
  #line 8
    __cil_tmp5 = __cil_tmp4 < __cil_tmp3;
  #line 8
    __CPROVER_assume(__cil_tmp5);
    }
    {
  #line 10
    __cil_tmp6 = i * 8UL;
  #line 10
    __cil_tmp7 = (unsigned long )(timer_registered) + __cil_tmp6;
  #line 10
    __cil_tmp8 = *((struct timer_list **)__cil_tmp7);
  #line 10
    __cil_tmp9 = (unsigned long )__cil_tmp8;
  #line 10
    __cil_tmp10 = __cil_tmp9 + 24;
  #line 10
    if (*((short *)__cil_tmp10)) {
      {
  #line 11
      __cil_tmp11 = i * 8UL;
  #line 11
      __cil_tmp12 = (unsigned long )(timer_registered) + __cil_tmp11;
  #line 11
      __cil_tmp13 = *((struct timer_list **)__cil_tmp12);
  #line 11
      __cil_tmp14 = (unsigned long )__cil_tmp13;
  #line 11
      __cil_tmp15 = __cil_tmp14 + 8;
  #line 11
      __cil_tmp16 = *((void (**)(unsigned long  ))__cil_tmp15);
  #line 11
      __cil_tmp17 = i * 8UL;
  #line 11
      __cil_tmp18 = (unsigned long )(timer_registered) + __cil_tmp17;
  #line 11
      __cil_tmp19 = *((struct timer_list **)__cil_tmp18);
  #line 11
      __cil_tmp20 = (unsigned long )__cil_tmp19;
  #line 11
      __cil_tmp21 = __cil_tmp20 + 16;
  #line 11
      __cil_tmp22 = *((unsigned long *)__cil_tmp21);
  #line 11
      (*__cil_tmp16)(__cil_tmp22);
      }
    } else {
  
    }
    }
  #line 13
    return;
  }
  }
  #line 1 "preproc_lIu5gX.o"
  #pragma merger(0,"preproc_lIu5gX.i","-x,c")
  #line 90 "./include/linux/ioport.h"
  struct resource *request_region(unsigned long start , unsigned long len , char const   *name ) ;
  #line 92
  void release_region(unsigned long start , unsigned long len ) ;
  #line 96
  extern struct resource *request_mem_region(unsigned long start , unsigned long len ,
                                             char const   *name ) ;
  #line 98
  extern void release_mem_region(unsigned long start , unsigned long len ) ;
  #line 10 "cprover/ddverify/include/ddverify/satabs.h"
  extern void *malloc(size_t size ) ;
  #line 8 "./drivers/pci/pci.c"
  __inline int pci_enable_device(struct pci_dev *dev ) 
  { int i ;
    unsigned int tmp ;
    unsigned short tmp___0 ;
    unsigned long __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    unsigned long __cil_tmp11 ;
    unsigned long __cil_tmp12 ;
    unsigned long __cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    unsigned long __cil_tmp15 ;
    unsigned long __cil_tmp16 ;
    unsigned long __cil_tmp17 ;
    unsigned long __cil_tmp18 ;
    unsigned long __cil_tmp19 ;
    unsigned long __cil_tmp20 ;
    unsigned long __cil_tmp21 ;
    unsigned long __cil_tmp22 ;
    unsigned long __cil_tmp23 ;
    unsigned long __cil_tmp24 ;
    unsigned long __cil_tmp25 ;
    unsigned long __cil_tmp26 ;
  
    {
  #line 12
    i = 0;
    {
  #line 12
    while (1) {
      while_continue: /* CIL Label */ ;
  #line 12
      if (i < 12) {
  
      } else {
  #line 12
        goto while_break;
      }
      {
  #line 13
      __cil_tmp5 = i * 32UL;
  #line 13
      __cil_tmp6 = __cil_tmp5 + 24;
  #line 13
      __cil_tmp7 = 56 + __cil_tmp6;
  #line 13
      __cil_tmp8 = (unsigned long )dev;
  #line 13
      __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
  #line 13
      *((unsigned long *)__cil_tmp9) = 256UL;
  #line 14
      tmp = __VERIFIER_nondet_uint();
  #line 14
      __cil_tmp10 = i * 32UL;
  #line 14
      __cil_tmp11 = __cil_tmp10 + 8;
  #line 14
      __cil_tmp12 = 56 + __cil_tmp11;
  #line 14
      __cil_tmp13 = (unsigned long )dev;
  #line 14
      __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
  #line 14
      *((unsigned long *)__cil_tmp14) = (unsigned long )tmp;
  #line 15
      tmp___0 = __VERIFIER_nondet_ushort();
  #line 15
      __cil_tmp15 = i * 32UL;
  #line 15
      __cil_tmp16 = __cil_tmp15 + 16;
  #line 15
      __cil_tmp17 = 56 + __cil_tmp16;
  #line 15
      __cil_tmp18 = (unsigned long )dev;
  #line 15
      __cil_tmp19 = __cil_tmp18 + __cil_tmp17;
  #line 15
      __cil_tmp20 = (unsigned long )tmp___0;
  #line 15
      __cil_tmp21 = i * 32UL;
  #line 15
      __cil_tmp22 = __cil_tmp21 + 8;
  #line 15
      __cil_tmp23 = 56 + __cil_tmp22;
  #line 15
      __cil_tmp24 = (unsigned long )dev;
  #line 15
      __cil_tmp25 = __cil_tmp24 + __cil_tmp23;
  #line 15
      __cil_tmp26 = *((unsigned long *)__cil_tmp25);
  #line 15
      *((unsigned long *)__cil_tmp19) = __cil_tmp26 + __cil_tmp20;
  #line 12
      i = i + 1;
      }
    }
    while_break: /* CIL Label */ ;
    }
  #line 17
    return (0);
  }
  }
  #line 19 "./drivers/pci/pci.c"
  __inline struct pci_dev *pci_get_class(unsigned int class , struct pci_dev *from ) 
  { void *tmp ;
    int tmp___0 ;
    void *__cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    size_t __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    unsigned long __cil_tmp11 ;
    unsigned long __cil_tmp12 ;
    unsigned long __cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    unsigned long __cil_tmp15 ;
    unsigned long __cil_tmp16 ;
    unsigned int __cil_tmp17 ;
    int __cil_tmp18 ;
    void *__cil_tmp19 ;
  
    {
    {
  #line 21
    __cil_tmp5 = (void *)0;
  #line 21
    __cil_tmp6 = (unsigned long )__cil_tmp5;
  #line 21
    __cil_tmp7 = (unsigned long )from;
  #line 21
    if (__cil_tmp7 == __cil_tmp6) {
      {
  #line 22
      __cil_tmp8 = (size_t )440UL;
  #line 22
      tmp = malloc(__cil_tmp8);
  #line 22
      from = (struct pci_dev *)tmp;
      }
    } else {
  
    }
    }
    {
  #line 25
    tmp___0 = __VERIFIER_nondet_int();
    }
  #line 25
    if (tmp___0) {
      {
  #line 26
      __cil_tmp9 = (unsigned long )from;
  #line 26
      __cil_tmp10 = __cil_tmp9 + 12;
  #line 26
      *((unsigned short *)__cil_tmp10) = __VERIFIER_nondet_ushort();
  #line 27
      __cil_tmp11 = (unsigned long )from;
  #line 27
      __cil_tmp12 = __cil_tmp11 + 14;
  #line 27
      *((unsigned short *)__cil_tmp12) = __VERIFIER_nondet_ushort();
  #line 28
      __cil_tmp13 = (unsigned long )from;
  #line 28
      __cil_tmp14 = __cil_tmp13 + 48;
  #line 28
      *((unsigned int *)__cil_tmp14) = __VERIFIER_nondet_uint();
  #line 29
      __cil_tmp15 = (unsigned long )from;
  #line 29
      __cil_tmp16 = __cil_tmp15 + 48;
  #line 29
      __cil_tmp17 = *((unsigned int *)__cil_tmp16);
  #line 29
      __cil_tmp18 = __cil_tmp17 < 16U;
  #line 29
      __CPROVER_assume(__cil_tmp18);
      }
  #line 31
      return (from);
    } else {
      {
  #line 33
      __cil_tmp19 = (void *)0;
  #line 33
      return ((struct pci_dev *)__cil_tmp19);
      }
    }
  }
  }
  #line 37 "./drivers/pci/pci.c"
  __inline int pci_register_driver(struct pci_driver *driver ) 
  { int tmp ;
    struct ddv_pci_driver *__cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    unsigned long __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
  
    {
    {
  #line 39
    tmp = __VERIFIER_nondet_int();
    }
  #line 39
    if (tmp) {
  #line 40
      __cil_tmp3 = & registered_pci_driver;
  #line 40
      *((struct pci_driver **)__cil_tmp3) = driver;
  #line 41
      __cil_tmp4 = (unsigned long )(& registered_pci_driver) + 448;
  #line 41
      __cil_tmp5 = 8UL / 32UL;
  #line 41
      *((unsigned int *)__cil_tmp4) = (unsigned int )__cil_tmp5;
  #line 42
      __cil_tmp6 = (unsigned long )(& registered_pci_driver) + 452;
  #line 42
      *((int *)__cil_tmp6) = 0;
  #line 44
      return (0);
    } else {
  #line 46
      return (-1);
    }
  }
  }
  #line 50 "./drivers/pci/pci.c"
  __inline void pci_unregister_driver(struct pci_driver *driver ) 
  { struct ddv_pci_driver *__cil_tmp2 ;
    void *__cil_tmp3 ;
    unsigned long __cil_tmp4 ;
  
    {
  #line 52
    __cil_tmp2 = & registered_pci_driver;
  #line 52
    __cil_tmp3 = (void *)0;
  #line 52
    *((struct pci_driver **)__cil_tmp2) = (struct pci_driver *)__cil_tmp3;
  #line 53
    __cil_tmp4 = (unsigned long )(& registered_pci_driver) + 448;
  #line 53
    *((unsigned int *)__cil_tmp4) = 0U;
  #line 54
    return;
  }
  }
  #line 56 "./drivers/pci/pci.c"
  __inline void pci_release_region(struct pci_dev *pdev , int bar ) 
  { unsigned long tmp ;
    unsigned long tmp___0 ;
    unsigned long tmp___1 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    unsigned long __cil_tmp11 ;
    unsigned long __cil_tmp12 ;
    unsigned long __cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    unsigned long __cil_tmp15 ;
    unsigned long __cil_tmp16 ;
    unsigned long __cil_tmp17 ;
    unsigned long __cil_tmp18 ;
    unsigned long __cil_tmp19 ;
    unsigned long __cil_tmp20 ;
    unsigned long __cil_tmp21 ;
    unsigned long __cil_tmp22 ;
    unsigned long __cil_tmp23 ;
    unsigned long __cil_tmp24 ;
    unsigned long __cil_tmp25 ;
    unsigned long __cil_tmp26 ;
    unsigned long __cil_tmp27 ;
    unsigned long __cil_tmp28 ;
    unsigned long __cil_tmp29 ;
    unsigned long __cil_tmp30 ;
    unsigned long __cil_tmp31 ;
    unsigned long __cil_tmp32 ;
    unsigned long __cil_tmp33 ;
    unsigned long __cil_tmp34 ;
    unsigned long __cil_tmp35 ;
    unsigned long __cil_tmp36 ;
    unsigned long __cil_tmp37 ;
    unsigned long __cil_tmp38 ;
    unsigned long __cil_tmp39 ;
    unsigned long __cil_tmp40 ;
    unsigned long __cil_tmp41 ;
    unsigned long __cil_tmp42 ;
    unsigned long __cil_tmp43 ;
    unsigned long __cil_tmp44 ;
    unsigned long __cil_tmp45 ;
    unsigned long __cil_tmp46 ;
    unsigned long __cil_tmp47 ;
    unsigned long __cil_tmp48 ;
    unsigned long __cil_tmp49 ;
    unsigned long __cil_tmp50 ;
    unsigned long __cil_tmp51 ;
    unsigned long __cil_tmp52 ;
    unsigned long __cil_tmp53 ;
    unsigned long __cil_tmp54 ;
    unsigned long __cil_tmp55 ;
    unsigned long __cil_tmp56 ;
    unsigned long __cil_tmp57 ;
    unsigned long __cil_tmp58 ;
    unsigned long __cil_tmp59 ;
    unsigned long __cil_tmp60 ;
    unsigned long __cil_tmp61 ;
    unsigned long __cil_tmp62 ;
    unsigned long __cil_tmp63 ;
    unsigned long __cil_tmp64 ;
    unsigned long __cil_tmp65 ;
    unsigned long __cil_tmp66 ;
    unsigned long __cil_tmp67 ;
    unsigned long __cil_tmp68 ;
    unsigned long __cil_tmp69 ;
    unsigned long __cil_tmp70 ;
    unsigned long __cil_tmp71 ;
    unsigned long __cil_tmp72 ;
    unsigned long __cil_tmp73 ;
    unsigned long __cil_tmp74 ;
    unsigned long __cil_tmp75 ;
    unsigned long __cil_tmp76 ;
    unsigned long __cil_tmp77 ;
    unsigned long __cil_tmp78 ;
    unsigned long __cil_tmp79 ;
    unsigned long __cil_tmp80 ;
    unsigned long __cil_tmp81 ;
    unsigned long __cil_tmp82 ;
    unsigned long __cil_tmp83 ;
    unsigned long __cil_tmp84 ;
    unsigned long __cil_tmp85 ;
    unsigned long __cil_tmp86 ;
    unsigned long __cil_tmp87 ;
    unsigned long __cil_tmp88 ;
    unsigned long __cil_tmp89 ;
    unsigned long __cil_tmp90 ;
    unsigned long __cil_tmp91 ;
    unsigned long __cil_tmp92 ;
    unsigned long __cil_tmp93 ;
    unsigned long __cil_tmp94 ;
    unsigned long __cil_tmp95 ;
    unsigned long __cil_tmp96 ;
    unsigned long __cil_tmp97 ;
    unsigned long __cil_tmp98 ;
    unsigned long __cil_tmp99 ;
    unsigned long __cil_tmp100 ;
    unsigned long __cil_tmp101 ;
    unsigned long __cil_tmp102 ;
    unsigned long __cil_tmp103 ;
    unsigned long __cil_tmp104 ;
    unsigned long __cil_tmp105 ;
    unsigned long __cil_tmp106 ;
    unsigned long __cil_tmp107 ;
    unsigned long __cil_tmp108 ;
    unsigned long __cil_tmp109 ;
    unsigned long __cil_tmp110 ;
    unsigned long __cil_tmp111 ;
    unsigned long __cil_tmp112 ;
    unsigned long __cil_tmp113 ;
    unsigned long __cil_tmp114 ;
    unsigned long __cil_tmp115 ;
    unsigned long __cil_tmp116 ;
    unsigned long __cil_tmp117 ;
    unsigned long __cil_tmp118 ;
    unsigned long __cil_tmp119 ;
    unsigned long __cil_tmp120 ;
    unsigned long __cil_tmp121 ;
    unsigned long __cil_tmp122 ;
    unsigned long __cil_tmp123 ;
    unsigned long __cil_tmp124 ;
    unsigned long __cil_tmp125 ;
    unsigned long __cil_tmp126 ;
    unsigned long __cil_tmp127 ;
    unsigned long __cil_tmp128 ;
    unsigned long __cil_tmp129 ;
    unsigned long __cil_tmp130 ;
    unsigned long __cil_tmp131 ;
    unsigned long __cil_tmp132 ;
    unsigned long __cil_tmp133 ;
    unsigned long __cil_tmp134 ;
    unsigned long __cil_tmp135 ;
    unsigned long __cil_tmp136 ;
    unsigned long __cil_tmp137 ;
    unsigned long __cil_tmp138 ;
    unsigned long __cil_tmp139 ;
    unsigned long __cil_tmp140 ;
    unsigned long __cil_tmp141 ;
    unsigned long __cil_tmp142 ;
    unsigned long __cil_tmp143 ;
    unsigned long __cil_tmp144 ;
    unsigned long __cil_tmp145 ;
    unsigned long __cil_tmp146 ;
    unsigned long __cil_tmp147 ;
    unsigned long __cil_tmp148 ;
    unsigned long __cil_tmp149 ;
    unsigned long __cil_tmp150 ;
    unsigned long __cil_tmp151 ;
    unsigned long __cil_tmp152 ;
    unsigned long __cil_tmp153 ;
    unsigned long __cil_tmp154 ;
    unsigned long __cil_tmp155 ;
    unsigned long __cil_tmp156 ;
    unsigned long __cil_tmp157 ;
    unsigned long __cil_tmp158 ;
    unsigned long __cil_tmp159 ;
    unsigned long __cil_tmp160 ;
    unsigned long __cil_tmp161 ;
  
    {
    {
  #line 58
    __cil_tmp6 = bar * 32UL;
  #line 58
    __cil_tmp7 = __cil_tmp6 + 8;
  #line 58
    __cil_tmp8 = 56 + __cil_tmp7;
  #line 58
    __cil_tmp9 = (unsigned long )pdev;
  #line 58
    __cil_tmp10 = __cil_tmp9 + __cil_tmp8;
  #line 58
    __cil_tmp11 = *((unsigned long *)__cil_tmp10);
  #line 58
    if (__cil_tmp11 == 0UL) {
      {
  #line 58
      __cil_tmp12 = bar * 32UL;
  #line 58
      __cil_tmp13 = __cil_tmp12 + 8;
  #line 58
      __cil_tmp14 = 56 + __cil_tmp13;
  #line 58
      __cil_tmp15 = (unsigned long )pdev;
  #line 58
      __cil_tmp16 = __cil_tmp15 + __cil_tmp14;
  #line 58
      __cil_tmp17 = *((unsigned long *)__cil_tmp16);
  #line 58
      __cil_tmp18 = bar * 32UL;
  #line 58
      __cil_tmp19 = __cil_tmp18 + 16;
  #line 58
      __cil_tmp20 = 56 + __cil_tmp19;
  #line 58
      __cil_tmp21 = (unsigned long )pdev;
  #line 58
      __cil_tmp22 = __cil_tmp21 + __cil_tmp20;
  #line 58
      __cil_tmp23 = *((unsigned long *)__cil_tmp22);
  #line 58
      if (__cil_tmp23 == __cil_tmp17) {
  #line 58
        tmp = 0UL;
      } else {
  #line 58
        __cil_tmp24 = bar * 32UL;
  #line 58
        __cil_tmp25 = __cil_tmp24 + 8;
  #line 58
        __cil_tmp26 = 56 + __cil_tmp25;
  #line 58
        __cil_tmp27 = (unsigned long )pdev;
  #line 58
        __cil_tmp28 = __cil_tmp27 + __cil_tmp26;
  #line 58
        __cil_tmp29 = *((unsigned long *)__cil_tmp28);
  #line 58
        __cil_tmp30 = bar * 32UL;
  #line 58
        __cil_tmp31 = __cil_tmp30 + 16;
  #line 58
        __cil_tmp32 = 56 + __cil_tmp31;
  #line 58
        __cil_tmp33 = (unsigned long )pdev;
  #line 58
        __cil_tmp34 = __cil_tmp33 + __cil_tmp32;
  #line 58
        __cil_tmp35 = *((unsigned long *)__cil_tmp34);
  #line 58
        __cil_tmp36 = __cil_tmp35 - __cil_tmp29;
  #line 58
        tmp = __cil_tmp36 + 1UL;
      }
      }
    } else {
  #line 58
      __cil_tmp37 = bar * 32UL;
  #line 58
      __cil_tmp38 = __cil_tmp37 + 8;
  #line 58
      __cil_tmp39 = 56 + __cil_tmp38;
  #line 58
      __cil_tmp40 = (unsigned long )pdev;
  #line 58
      __cil_tmp41 = __cil_tmp40 + __cil_tmp39;
  #line 58
      __cil_tmp42 = *((unsigned long *)__cil_tmp41);
  #line 58
      __cil_tmp43 = bar * 32UL;
  #line 58
      __cil_tmp44 = __cil_tmp43 + 16;
  #line 58
      __cil_tmp45 = 56 + __cil_tmp44;
  #line 58
      __cil_tmp46 = (unsigned long )pdev;
  #line 58
      __cil_tmp47 = __cil_tmp46 + __cil_tmp45;
  #line 58
      __cil_tmp48 = *((unsigned long *)__cil_tmp47);
  #line 58
      __cil_tmp49 = __cil_tmp48 - __cil_tmp42;
  #line 58
      tmp = __cil_tmp49 + 1UL;
    }
    }
  #line 58
    if (tmp == 0UL) {
  #line 59
      return;
    } else {
  
    }
    {
  #line 60
    __cil_tmp50 = bar * 32UL;
  #line 60
    __cil_tmp51 = __cil_tmp50 + 24;
  #line 60
    __cil_tmp52 = 56 + __cil_tmp51;
  #line 60
    __cil_tmp53 = (unsigned long )pdev;
  #line 60
    __cil_tmp54 = __cil_tmp53 + __cil_tmp52;
  #line 60
    __cil_tmp55 = *((unsigned long *)__cil_tmp54);
  #line 60
    if (__cil_tmp55 & 256UL) {
      {
  #line 61
      __cil_tmp56 = bar * 32UL;
  #line 61
      __cil_tmp57 = __cil_tmp56 + 8;
  #line 61
      __cil_tmp58 = 56 + __cil_tmp57;
  #line 61
      __cil_tmp59 = (unsigned long )pdev;
  #line 61
      __cil_tmp60 = __cil_tmp59 + __cil_tmp58;
  #line 61
      __cil_tmp61 = *((unsigned long *)__cil_tmp60);
  #line 61
      if (__cil_tmp61 == 0UL) {
        {
  #line 61
        __cil_tmp62 = bar * 32UL;
  #line 61
        __cil_tmp63 = __cil_tmp62 + 8;
  #line 61
        __cil_tmp64 = 56 + __cil_tmp63;
  #line 61
        __cil_tmp65 = (unsigned long )pdev;
  #line 61
        __cil_tmp66 = __cil_tmp65 + __cil_tmp64;
  #line 61
        __cil_tmp67 = *((unsigned long *)__cil_tmp66);
  #line 61
        __cil_tmp68 = bar * 32UL;
  #line 61
        __cil_tmp69 = __cil_tmp68 + 16;
  #line 61
        __cil_tmp70 = 56 + __cil_tmp69;
  #line 61
        __cil_tmp71 = (unsigned long )pdev;
  #line 61
        __cil_tmp72 = __cil_tmp71 + __cil_tmp70;
  #line 61
        __cil_tmp73 = *((unsigned long *)__cil_tmp72);
  #line 61
        if (__cil_tmp73 == __cil_tmp67) {
  #line 61
          tmp___0 = 0UL;
        } else {
  #line 61
          __cil_tmp74 = bar * 32UL;
  #line 61
          __cil_tmp75 = __cil_tmp74 + 8;
  #line 61
          __cil_tmp76 = 56 + __cil_tmp75;
  #line 61
          __cil_tmp77 = (unsigned long )pdev;
  #line 61
          __cil_tmp78 = __cil_tmp77 + __cil_tmp76;
  #line 61
          __cil_tmp79 = *((unsigned long *)__cil_tmp78);
  #line 61
          __cil_tmp80 = bar * 32UL;
  #line 61
          __cil_tmp81 = __cil_tmp80 + 16;
  #line 61
          __cil_tmp82 = 56 + __cil_tmp81;
  #line 61
          __cil_tmp83 = (unsigned long )pdev;
  #line 61
          __cil_tmp84 = __cil_tmp83 + __cil_tmp82;
  #line 61
          __cil_tmp85 = *((unsigned long *)__cil_tmp84);
  #line 61
          __cil_tmp86 = __cil_tmp85 - __cil_tmp79;
  #line 61
          tmp___0 = __cil_tmp86 + 1UL;
        }
        }
      } else {
  #line 61
        __cil_tmp87 = bar * 32UL;
  #line 61
        __cil_tmp88 = __cil_tmp87 + 8;
  #line 61
        __cil_tmp89 = 56 + __cil_tmp88;
  #line 61
        __cil_tmp90 = (unsigned long )pdev;
  #line 61
        __cil_tmp91 = __cil_tmp90 + __cil_tmp89;
  #line 61
        __cil_tmp92 = *((unsigned long *)__cil_tmp91);
  #line 61
        __cil_tmp93 = bar * 32UL;
  #line 61
        __cil_tmp94 = __cil_tmp93 + 16;
  #line 61
        __cil_tmp95 = 56 + __cil_tmp94;
  #line 61
        __cil_tmp96 = (unsigned long )pdev;
  #line 61
        __cil_tmp97 = __cil_tmp96 + __cil_tmp95;
  #line 61
        __cil_tmp98 = *((unsigned long *)__cil_tmp97);
  #line 61
        __cil_tmp99 = __cil_tmp98 - __cil_tmp92;
  #line 61
        tmp___0 = __cil_tmp99 + 1UL;
      }
      }
      {
  #line 61
      __cil_tmp100 = bar * 32UL;
  #line 61
      __cil_tmp101 = __cil_tmp100 + 8;
  #line 61
      __cil_tmp102 = 56 + __cil_tmp101;
  #line 61
      __cil_tmp103 = (unsigned long )pdev;
  #line 61
      __cil_tmp104 = __cil_tmp103 + __cil_tmp102;
  #line 61
      __cil_tmp105 = *((unsigned long *)__cil_tmp104);
  #line 61
      release_region(__cil_tmp105, tmp___0);
      }
    } else {
      {
  #line 63
      __cil_tmp106 = bar * 32UL;
  #line 63
      __cil_tmp107 = __cil_tmp106 + 24;
  #line 63
      __cil_tmp108 = 56 + __cil_tmp107;
  #line 63
      __cil_tmp109 = (unsigned long )pdev;
  #line 63
      __cil_tmp110 = __cil_tmp109 + __cil_tmp108;
  #line 63
      __cil_tmp111 = *((unsigned long *)__cil_tmp110);
  #line 63
      if (__cil_tmp111 & 512UL) {
        {
  #line 64
        __cil_tmp112 = bar * 32UL;
  #line 64
        __cil_tmp113 = __cil_tmp112 + 8;
  #line 64
        __cil_tmp114 = 56 + __cil_tmp113;
  #line 64
        __cil_tmp115 = (unsigned long )pdev;
  #line 64
        __cil_tmp116 = __cil_tmp115 + __cil_tmp114;
  #line 64
        __cil_tmp117 = *((unsigned long *)__cil_tmp116);
  #line 64
        if (__cil_tmp117 == 0UL) {
          {
  #line 64
          __cil_tmp118 = bar * 32UL;
  #line 64
          __cil_tmp119 = __cil_tmp118 + 8;
  #line 64
          __cil_tmp120 = 56 + __cil_tmp119;
  #line 64
          __cil_tmp121 = (unsigned long )pdev;
  #line 64
          __cil_tmp122 = __cil_tmp121 + __cil_tmp120;
  #line 64
          __cil_tmp123 = *((unsigned long *)__cil_tmp122);
  #line 64
          __cil_tmp124 = bar * 32UL;
  #line 64
          __cil_tmp125 = __cil_tmp124 + 16;
  #line 64
          __cil_tmp126 = 56 + __cil_tmp125;
  #line 64
          __cil_tmp127 = (unsigned long )pdev;
  #line 64
          __cil_tmp128 = __cil_tmp127 + __cil_tmp126;
  #line 64
          __cil_tmp129 = *((unsigned long *)__cil_tmp128);
  #line 64
          if (__cil_tmp129 == __cil_tmp123) {
  #line 64
            tmp___1 = 0UL;
          } else {
  #line 64
            __cil_tmp130 = bar * 32UL;
  #line 64
            __cil_tmp131 = __cil_tmp130 + 8;
  #line 64
            __cil_tmp132 = 56 + __cil_tmp131;
  #line 64
            __cil_tmp133 = (unsigned long )pdev;
  #line 64
            __cil_tmp134 = __cil_tmp133 + __cil_tmp132;
  #line 64
            __cil_tmp135 = *((unsigned long *)__cil_tmp134);
  #line 64
            __cil_tmp136 = bar * 32UL;
  #line 64
            __cil_tmp137 = __cil_tmp136 + 16;
  #line 64
            __cil_tmp138 = 56 + __cil_tmp137;
  #line 64
            __cil_tmp139 = (unsigned long )pdev;
  #line 64
            __cil_tmp140 = __cil_tmp139 + __cil_tmp138;
  #line 64
            __cil_tmp141 = *((unsigned long *)__cil_tmp140);
  #line 64
            __cil_tmp142 = __cil_tmp141 - __cil_tmp135;
  #line 64
            tmp___1 = __cil_tmp142 + 1UL;
          }
          }
        } else {
  #line 64
          __cil_tmp143 = bar * 32UL;
  #line 64
          __cil_tmp144 = __cil_tmp143 + 8;
  #line 64
          __cil_tmp145 = 56 + __cil_tmp144;
  #line 64
          __cil_tmp146 = (unsigned long )pdev;
  #line 64
          __cil_tmp147 = __cil_tmp146 + __cil_tmp145;
  #line 64
          __cil_tmp148 = *((unsigned long *)__cil_tmp147);
  #line 64
          __cil_tmp149 = bar * 32UL;
  #line 64
          __cil_tmp150 = __cil_tmp149 + 16;
  #line 64
          __cil_tmp151 = 56 + __cil_tmp150;
  #line 64
          __cil_tmp152 = (unsigned long )pdev;
  #line 64
          __cil_tmp153 = __cil_tmp152 + __cil_tmp151;
  #line 64
          __cil_tmp154 = *((unsigned long *)__cil_tmp153);
  #line 64
          __cil_tmp155 = __cil_tmp154 - __cil_tmp148;
  #line 64
          tmp___1 = __cil_tmp155 + 1UL;
        }
        }
        {
  #line 64
        __cil_tmp156 = bar * 32UL;
  #line 64
        __cil_tmp157 = __cil_tmp156 + 8;
  #line 64
        __cil_tmp158 = 56 + __cil_tmp157;
  #line 64
        __cil_tmp159 = (unsigned long )pdev;
  #line 64
        __cil_tmp160 = __cil_tmp159 + __cil_tmp158;
  #line 64
        __cil_tmp161 = *((unsigned long *)__cil_tmp160);
  #line 64
        release_mem_region(__cil_tmp161, tmp___1);
        }
      } else {
  
      }
      }
    }
    }
  #line 66
    return;
  }
  }
  #line 68 "./drivers/pci/pci.c"
  __inline int pci_request_region(struct pci_dev *pdev , int bar , char const   *res_name ) 
  { unsigned long tmp ;
    unsigned long tmp___0 ;
    struct resource *tmp___1 ;
    unsigned long tmp___2 ;
    struct resource *tmp___3 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    unsigned long __cil_tmp11 ;
    unsigned long __cil_tmp12 ;
    unsigned long __cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    unsigned long __cil_tmp15 ;
    unsigned long __cil_tmp16 ;
    unsigned long __cil_tmp17 ;
    unsigned long __cil_tmp18 ;
    unsigned long __cil_tmp19 ;
    unsigned long __cil_tmp20 ;
    unsigned long __cil_tmp21 ;
    unsigned long __cil_tmp22 ;
    unsigned long __cil_tmp23 ;
    unsigned long __cil_tmp24 ;
    unsigned long __cil_tmp25 ;
    unsigned long __cil_tmp26 ;
    unsigned long __cil_tmp27 ;
    unsigned long __cil_tmp28 ;
    unsigned long __cil_tmp29 ;
    unsigned long __cil_tmp30 ;
    unsigned long __cil_tmp31 ;
    unsigned long __cil_tmp32 ;
    unsigned long __cil_tmp33 ;
    unsigned long __cil_tmp34 ;
    unsigned long __cil_tmp35 ;
    unsigned long __cil_tmp36 ;
    unsigned long __cil_tmp37 ;
    unsigned long __cil_tmp38 ;
    unsigned long __cil_tmp39 ;
    unsigned long __cil_tmp40 ;
    unsigned long __cil_tmp41 ;
    unsigned long __cil_tmp42 ;
    unsigned long __cil_tmp43 ;
    unsigned long __cil_tmp44 ;
    unsigned long __cil_tmp45 ;
    unsigned long __cil_tmp46 ;
    unsigned long __cil_tmp47 ;
    unsigned long __cil_tmp48 ;
    unsigned long __cil_tmp49 ;
    unsigned long __cil_tmp50 ;
    unsigned long __cil_tmp51 ;
    unsigned long __cil_tmp52 ;
    unsigned long __cil_tmp53 ;
    unsigned long __cil_tmp54 ;
    unsigned long __cil_tmp55 ;
    unsigned long __cil_tmp56 ;
    unsigned long __cil_tmp57 ;
    unsigned long __cil_tmp58 ;
    unsigned long __cil_tmp59 ;
    unsigned long __cil_tmp60 ;
    unsigned long __cil_tmp61 ;
    unsigned long __cil_tmp62 ;
    unsigned long __cil_tmp63 ;
    unsigned long __cil_tmp64 ;
    unsigned long __cil_tmp65 ;
    unsigned long __cil_tmp66 ;
    unsigned long __cil_tmp67 ;
    unsigned long __cil_tmp68 ;
    unsigned long __cil_tmp69 ;
    unsigned long __cil_tmp70 ;
    unsigned long __cil_tmp71 ;
    unsigned long __cil_tmp72 ;
    unsigned long __cil_tmp73 ;
    unsigned long __cil_tmp74 ;
    unsigned long __cil_tmp75 ;
    unsigned long __cil_tmp76 ;
    unsigned long __cil_tmp77 ;
    unsigned long __cil_tmp78 ;
    unsigned long __cil_tmp79 ;
    unsigned long __cil_tmp80 ;
    unsigned long __cil_tmp81 ;
    unsigned long __cil_tmp82 ;
    unsigned long __cil_tmp83 ;
    unsigned long __cil_tmp84 ;
    unsigned long __cil_tmp85 ;
    unsigned long __cil_tmp86 ;
    unsigned long __cil_tmp87 ;
    unsigned long __cil_tmp88 ;
    unsigned long __cil_tmp89 ;
    unsigned long __cil_tmp90 ;
    unsigned long __cil_tmp91 ;
    unsigned long __cil_tmp92 ;
    unsigned long __cil_tmp93 ;
    unsigned long __cil_tmp94 ;
    unsigned long __cil_tmp95 ;
    unsigned long __cil_tmp96 ;
    unsigned long __cil_tmp97 ;
    unsigned long __cil_tmp98 ;
    unsigned long __cil_tmp99 ;
    unsigned long __cil_tmp100 ;
    unsigned long __cil_tmp101 ;
    unsigned long __cil_tmp102 ;
    unsigned long __cil_tmp103 ;
    unsigned long __cil_tmp104 ;
    unsigned long __cil_tmp105 ;
    unsigned long __cil_tmp106 ;
    unsigned long __cil_tmp107 ;
    unsigned long __cil_tmp108 ;
    unsigned long __cil_tmp109 ;
    unsigned long __cil_tmp110 ;
    unsigned long __cil_tmp111 ;
    unsigned long __cil_tmp112 ;
    unsigned long __cil_tmp113 ;
    unsigned long __cil_tmp114 ;
    unsigned long __cil_tmp115 ;
    unsigned long __cil_tmp116 ;
    unsigned long __cil_tmp117 ;
    unsigned long __cil_tmp118 ;
    unsigned long __cil_tmp119 ;
    unsigned long __cil_tmp120 ;
    unsigned long __cil_tmp121 ;
    unsigned long __cil_tmp122 ;
    unsigned long __cil_tmp123 ;
    unsigned long __cil_tmp124 ;
    unsigned long __cil_tmp125 ;
    unsigned long __cil_tmp126 ;
    unsigned long __cil_tmp127 ;
    unsigned long __cil_tmp128 ;
    unsigned long __cil_tmp129 ;
    unsigned long __cil_tmp130 ;
    unsigned long __cil_tmp131 ;
    unsigned long __cil_tmp132 ;
    unsigned long __cil_tmp133 ;
    unsigned long __cil_tmp134 ;
    unsigned long __cil_tmp135 ;
    unsigned long __cil_tmp136 ;
    unsigned long __cil_tmp137 ;
    unsigned long __cil_tmp138 ;
    unsigned long __cil_tmp139 ;
    unsigned long __cil_tmp140 ;
    unsigned long __cil_tmp141 ;
    unsigned long __cil_tmp142 ;
    unsigned long __cil_tmp143 ;
    unsigned long __cil_tmp144 ;
    unsigned long __cil_tmp145 ;
    unsigned long __cil_tmp146 ;
    unsigned long __cil_tmp147 ;
    unsigned long __cil_tmp148 ;
    unsigned long __cil_tmp149 ;
    unsigned long __cil_tmp150 ;
    unsigned long __cil_tmp151 ;
    unsigned long __cil_tmp152 ;
    unsigned long __cil_tmp153 ;
    unsigned long __cil_tmp154 ;
    unsigned long __cil_tmp155 ;
    unsigned long __cil_tmp156 ;
    unsigned long __cil_tmp157 ;
    unsigned long __cil_tmp158 ;
    unsigned long __cil_tmp159 ;
    unsigned long __cil_tmp160 ;
    unsigned long __cil_tmp161 ;
    unsigned long __cil_tmp162 ;
    unsigned long __cil_tmp163 ;
    unsigned long __cil_tmp164 ;
  
    {
    {
  #line 70
    __cil_tmp9 = bar * 32UL;
  #line 70
    __cil_tmp10 = __cil_tmp9 + 8;
  #line 70
    __cil_tmp11 = 56 + __cil_tmp10;
  #line 70
    __cil_tmp12 = (unsigned long )pdev;
  #line 70
    __cil_tmp13 = __cil_tmp12 + __cil_tmp11;
  #line 70
    __cil_tmp14 = *((unsigned long *)__cil_tmp13);
  #line 70
    if (__cil_tmp14 == 0UL) {
      {
  #line 70
      __cil_tmp15 = bar * 32UL;
  #line 70
      __cil_tmp16 = __cil_tmp15 + 8;
  #line 70
      __cil_tmp17 = 56 + __cil_tmp16;
  #line 70
      __cil_tmp18 = (unsigned long )pdev;
  #line 70
      __cil_tmp19 = __cil_tmp18 + __cil_tmp17;
  #line 70
      __cil_tmp20 = *((unsigned long *)__cil_tmp19);
  #line 70
      __cil_tmp21 = bar * 32UL;
  #line 70
      __cil_tmp22 = __cil_tmp21 + 16;
  #line 70
      __cil_tmp23 = 56 + __cil_tmp22;
  #line 70
      __cil_tmp24 = (unsigned long )pdev;
  #line 70
      __cil_tmp25 = __cil_tmp24 + __cil_tmp23;
  #line 70
      __cil_tmp26 = *((unsigned long *)__cil_tmp25);
  #line 70
      if (__cil_tmp26 == __cil_tmp20) {
  #line 70
        tmp = 0UL;
      } else {
  #line 70
        __cil_tmp27 = bar * 32UL;
  #line 70
        __cil_tmp28 = __cil_tmp27 + 8;
  #line 70
        __cil_tmp29 = 56 + __cil_tmp28;
  #line 70
        __cil_tmp30 = (unsigned long )pdev;
  #line 70
        __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
  #line 70
        __cil_tmp32 = *((unsigned long *)__cil_tmp31);
  #line 70
        __cil_tmp33 = bar * 32UL;
  #line 70
        __cil_tmp34 = __cil_tmp33 + 16;
  #line 70
        __cil_tmp35 = 56 + __cil_tmp34;
  #line 70
        __cil_tmp36 = (unsigned long )pdev;
  #line 70
        __cil_tmp37 = __cil_tmp36 + __cil_tmp35;
  #line 70
        __cil_tmp38 = *((unsigned long *)__cil_tmp37);
  #line 70
        __cil_tmp39 = __cil_tmp38 - __cil_tmp32;
  #line 70
        tmp = __cil_tmp39 + 1UL;
      }
      }
    } else {
  #line 70
      __cil_tmp40 = bar * 32UL;
  #line 70
      __cil_tmp41 = __cil_tmp40 + 8;
  #line 70
      __cil_tmp42 = 56 + __cil_tmp41;
  #line 70
      __cil_tmp43 = (unsigned long )pdev;
  #line 70
      __cil_tmp44 = __cil_tmp43 + __cil_tmp42;
  #line 70
      __cil_tmp45 = *((unsigned long *)__cil_tmp44);
  #line 70
      __cil_tmp46 = bar * 32UL;
  #line 70
      __cil_tmp47 = __cil_tmp46 + 16;
  #line 70
      __cil_tmp48 = 56 + __cil_tmp47;
  #line 70
      __cil_tmp49 = (unsigned long )pdev;
  #line 70
      __cil_tmp50 = __cil_tmp49 + __cil_tmp48;
  #line 70
      __cil_tmp51 = *((unsigned long *)__cil_tmp50);
  #line 70
      __cil_tmp52 = __cil_tmp51 - __cil_tmp45;
  #line 70
      tmp = __cil_tmp52 + 1UL;
    }
    }
  #line 70
    if (tmp == 0UL) {
  #line 71
      return (0);
    } else {
  
    }
    {
  #line 73
    __cil_tmp53 = bar * 32UL;
  #line 73
    __cil_tmp54 = __cil_tmp53 + 24;
  #line 73
    __cil_tmp55 = 56 + __cil_tmp54;
  #line 73
    __cil_tmp56 = (unsigned long )pdev;
  #line 73
    __cil_tmp57 = __cil_tmp56 + __cil_tmp55;
  #line 73
    __cil_tmp58 = *((unsigned long *)__cil_tmp57);
  #line 73
    if (__cil_tmp58 & 256UL) {
      {
  #line 74
      __cil_tmp59 = bar * 32UL;
  #line 74
      __cil_tmp60 = __cil_tmp59 + 8;
  #line 74
      __cil_tmp61 = 56 + __cil_tmp60;
  #line 74
      __cil_tmp62 = (unsigned long )pdev;
  #line 74
      __cil_tmp63 = __cil_tmp62 + __cil_tmp61;
  #line 74
      __cil_tmp64 = *((unsigned long *)__cil_tmp63);
  #line 74
      if (__cil_tmp64 == 0UL) {
        {
  #line 74
        __cil_tmp65 = bar * 32UL;
  #line 74
        __cil_tmp66 = __cil_tmp65 + 8;
  #line 74
        __cil_tmp67 = 56 + __cil_tmp66;
  #line 74
        __cil_tmp68 = (unsigned long )pdev;
  #line 74
        __cil_tmp69 = __cil_tmp68 + __cil_tmp67;
  #line 74
        __cil_tmp70 = *((unsigned long *)__cil_tmp69);
  #line 74
        __cil_tmp71 = bar * 32UL;
  #line 74
        __cil_tmp72 = __cil_tmp71 + 16;
  #line 74
        __cil_tmp73 = 56 + __cil_tmp72;
  #line 74
        __cil_tmp74 = (unsigned long )pdev;
  #line 74
        __cil_tmp75 = __cil_tmp74 + __cil_tmp73;
  #line 74
        __cil_tmp76 = *((unsigned long *)__cil_tmp75);
  #line 74
        if (__cil_tmp76 == __cil_tmp70) {
  #line 74
          tmp___0 = 0UL;
        } else {
  #line 74
          __cil_tmp77 = bar * 32UL;
  #line 74
          __cil_tmp78 = __cil_tmp77 + 8;
  #line 74
          __cil_tmp79 = 56 + __cil_tmp78;
  #line 74
          __cil_tmp80 = (unsigned long )pdev;
  #line 74
          __cil_tmp81 = __cil_tmp80 + __cil_tmp79;
  #line 74
          __cil_tmp82 = *((unsigned long *)__cil_tmp81);
  #line 74
          __cil_tmp83 = bar * 32UL;
  #line 74
          __cil_tmp84 = __cil_tmp83 + 16;
  #line 74
          __cil_tmp85 = 56 + __cil_tmp84;
  #line 74
          __cil_tmp86 = (unsigned long )pdev;
  #line 74
          __cil_tmp87 = __cil_tmp86 + __cil_tmp85;
  #line 74
          __cil_tmp88 = *((unsigned long *)__cil_tmp87);
  #line 74
          __cil_tmp89 = __cil_tmp88 - __cil_tmp82;
  #line 74
          tmp___0 = __cil_tmp89 + 1UL;
        }
        }
      } else {
  #line 74
        __cil_tmp90 = bar * 32UL;
  #line 74
        __cil_tmp91 = __cil_tmp90 + 8;
  #line 74
        __cil_tmp92 = 56 + __cil_tmp91;
  #line 74
        __cil_tmp93 = (unsigned long )pdev;
  #line 74
        __cil_tmp94 = __cil_tmp93 + __cil_tmp92;
  #line 74
        __cil_tmp95 = *((unsigned long *)__cil_tmp94);
  #line 74
        __cil_tmp96 = bar * 32UL;
  #line 74
        __cil_tmp97 = __cil_tmp96 + 16;
  #line 74
        __cil_tmp98 = 56 + __cil_tmp97;
  #line 74
        __cil_tmp99 = (unsigned long )pdev;
  #line 74
        __cil_tmp100 = __cil_tmp99 + __cil_tmp98;
  #line 74
        __cil_tmp101 = *((unsigned long *)__cil_tmp100);
  #line 74
        __cil_tmp102 = __cil_tmp101 - __cil_tmp95;
  #line 74
        tmp___0 = __cil_tmp102 + 1UL;
      }
      }
      {
  #line 74
      __cil_tmp103 = bar * 32UL;
  #line 74
      __cil_tmp104 = __cil_tmp103 + 8;
  #line 74
      __cil_tmp105 = 56 + __cil_tmp104;
  #line 74
      __cil_tmp106 = (unsigned long )pdev;
  #line 74
      __cil_tmp107 = __cil_tmp106 + __cil_tmp105;
  #line 74
      __cil_tmp108 = *((unsigned long *)__cil_tmp107);
  #line 74
      tmp___1 = request_region(__cil_tmp108, tmp___0, res_name);
      }
  #line 74
      if (! tmp___1) {
  #line 76
        return (-16);
      } else {
  
      }
    } else {
      {
  #line 78
      __cil_tmp109 = bar * 32UL;
  #line 78
      __cil_tmp110 = __cil_tmp109 + 24;
  #line 78
      __cil_tmp111 = 56 + __cil_tmp110;
  #line 78
      __cil_tmp112 = (unsigned long )pdev;
  #line 78
      __cil_tmp113 = __cil_tmp112 + __cil_tmp111;
  #line 78
      __cil_tmp114 = *((unsigned long *)__cil_tmp113);
  #line 78
      if (__cil_tmp114 & 512UL) {
        {
  #line 79
        __cil_tmp115 = bar * 32UL;
  #line 79
        __cil_tmp116 = __cil_tmp115 + 8;
  #line 79
        __cil_tmp117 = 56 + __cil_tmp116;
  #line 79
        __cil_tmp118 = (unsigned long )pdev;
  #line 79
        __cil_tmp119 = __cil_tmp118 + __cil_tmp117;
  #line 79
        __cil_tmp120 = *((unsigned long *)__cil_tmp119);
  #line 79
        if (__cil_tmp120 == 0UL) {
          {
  #line 79
          __cil_tmp121 = bar * 32UL;
  #line 79
          __cil_tmp122 = __cil_tmp121 + 8;
  #line 79
          __cil_tmp123 = 56 + __cil_tmp122;
  #line 79
          __cil_tmp124 = (unsigned long )pdev;
  #line 79
          __cil_tmp125 = __cil_tmp124 + __cil_tmp123;
  #line 79
          __cil_tmp126 = *((unsigned long *)__cil_tmp125);
  #line 79
          __cil_tmp127 = bar * 32UL;
  #line 79
          __cil_tmp128 = __cil_tmp127 + 16;
  #line 79
          __cil_tmp129 = 56 + __cil_tmp128;
  #line 79
          __cil_tmp130 = (unsigned long )pdev;
  #line 79
          __cil_tmp131 = __cil_tmp130 + __cil_tmp129;
  #line 79
          __cil_tmp132 = *((unsigned long *)__cil_tmp131);
  #line 79
          if (__cil_tmp132 == __cil_tmp126) {
  #line 79
            tmp___2 = 0UL;
          } else {
  #line 79
            __cil_tmp133 = bar * 32UL;
  #line 79
            __cil_tmp134 = __cil_tmp133 + 8;
  #line 79
            __cil_tmp135 = 56 + __cil_tmp134;
  #line 79
            __cil_tmp136 = (unsigned long )pdev;
  #line 79
            __cil_tmp137 = __cil_tmp136 + __cil_tmp135;
  #line 79
            __cil_tmp138 = *((unsigned long *)__cil_tmp137);
  #line 79
            __cil_tmp139 = bar * 32UL;
  #line 79
            __cil_tmp140 = __cil_tmp139 + 16;
  #line 79
            __cil_tmp141 = 56 + __cil_tmp140;
  #line 79
            __cil_tmp142 = (unsigned long )pdev;
  #line 79
            __cil_tmp143 = __cil_tmp142 + __cil_tmp141;
  #line 79
            __cil_tmp144 = *((unsigned long *)__cil_tmp143);
  #line 79
            __cil_tmp145 = __cil_tmp144 - __cil_tmp138;
  #line 79
            tmp___2 = __cil_tmp145 + 1UL;
          }
          }
        } else {
  #line 79
          __cil_tmp146 = bar * 32UL;
  #line 79
          __cil_tmp147 = __cil_tmp146 + 8;
  #line 79
          __cil_tmp148 = 56 + __cil_tmp147;
  #line 79
          __cil_tmp149 = (unsigned long )pdev;
  #line 79
          __cil_tmp150 = __cil_tmp149 + __cil_tmp148;
  #line 79
          __cil_tmp151 = *((unsigned long *)__cil_tmp150);
  #line 79
          __cil_tmp152 = bar * 32UL;
  #line 79
          __cil_tmp153 = __cil_tmp152 + 16;
  #line 79
          __cil_tmp154 = 56 + __cil_tmp153;
  #line 79
          __cil_tmp155 = (unsigned long )pdev;
  #line 79
          __cil_tmp156 = __cil_tmp155 + __cil_tmp154;
  #line 79
          __cil_tmp157 = *((unsigned long *)__cil_tmp156);
  #line 79
          __cil_tmp158 = __cil_tmp157 - __cil_tmp151;
  #line 79
          tmp___2 = __cil_tmp158 + 1UL;
        }
        }
        {
  #line 79
        __cil_tmp159 = bar * 32UL;
  #line 79
        __cil_tmp160 = __cil_tmp159 + 8;
  #line 79
        __cil_tmp161 = 56 + __cil_tmp160;
  #line 79
        __cil_tmp162 = (unsigned long )pdev;
  #line 79
        __cil_tmp163 = __cil_tmp162 + __cil_tmp161;
  #line 79
        __cil_tmp164 = *((unsigned long *)__cil_tmp163);
  #line 79
        tmp___3 = request_mem_region(__cil_tmp164, tmp___2, res_name);
        }
  #line 79
        if (! tmp___3) {
  #line 81
          return (-16);
        } else {
  
        }
      } else {
  
      }
      }
    }
    }
  #line 84
    return (0);
  }
  }
  #line 87 "./drivers/pci/pci.c"
  __inline void pci_release_regions(struct pci_dev *pdev ) 
  { int i ;
  
    {
  #line 91
    i = 0;
    {
  #line 91
    while (1) {
      while_continue: /* CIL Label */ ;
  #line 91
      if (i < 6) {
  
      } else {
  #line 91
        goto while_break;
      }
      {
  #line 92
      pci_release_region(pdev, i);
  #line 91
      i = i + 1;
      }
    }
    while_break: /* CIL Label */ ;
    }
  #line 93
    return;
  }
  }
  #line 95 "./drivers/pci/pci.c"
  __inline int pci_request_regions(struct pci_dev *pdev , char const   *res_name ) 
  { int i ;
    int tmp ;
    int __cil_tmp5 ;
  
    {
  #line 99
    i = 0;
    {
  #line 99
    while (1) {
      while_continue: /* CIL Label */ ;
  #line 99
      if (i < 6) {
  
      } else {
  #line 99
        goto while_break;
      }
      {
  #line 100
      tmp = pci_request_region(pdev, i, res_name);
      }
  #line 100
      if (tmp) {
  #line 101
        goto err_out;
      } else {
  
      }
  #line 99
      i = i + 1;
    }
    while_break: /* CIL Label */ ;
    }
  #line 102
    return (0);
    err_out: 
    {
  #line 105
    while (1) {
      while_continue___0: /* CIL Label */ ;
  #line 105
      i = i - 1;
      {
  #line 105
      __cil_tmp5 = i >= 0;
  #line 105
      if (! __cil_tmp5) {
  #line 105
        goto while_break___0;
      } else {
  
      }
      }
      {
  #line 106
      pci_release_region(pdev, i);
      }
    }
    while_break___0: /* CIL Label */ ;
    }
  #line 108
    return (-16);
  }
  }
  #line 1 "preproc_kFMi4F.o"
  #pragma merger(0,"preproc_kFMi4F.i","-x,c")
  #line 61 "./include/asm/uaccess.h"
  __inline int __get_user(int size , void *ptr ) ;
  #line 71
  __inline unsigned long copy_to_user(void *to , void const   *from , unsigned long n ) ;
  #line 73
  __inline unsigned long copy_from_user(void *to , void *from , unsigned long n ) ;
  #line 20 "cprover/ddverify/include/ddverify/ddverify.h"
  __inline static int assert_context_process(void) 
  { int __cil_tmp1 ;
  
    {
    {
  #line 22
    __cil_tmp1 = current_execution_context == 1;
  #line 22
    __CPROVER_assert(__cil_tmp1, "Process context");
    }
  #line 23
    return (0);
  }
  }
  #line 5 "./arch/i386/lib/usercopy.c"
  __inline int __get_user(int size , void *ptr ) 
  { int tmp ;
  
    {
    {
  #line 8
    assert_context_process();
  #line 10
    tmp = __VERIFIER_nondet_int();
    }
  #line 10
    return (tmp);
  }
  }
  #line 37 "./arch/i386/lib/usercopy.c"
  __inline unsigned long copy_to_user(void *to , void const   *from , unsigned long n ) 
  { unsigned long tmp ;
  
    {
    {
  #line 40
    assert_context_process();
  #line 42
    tmp = __VERIFIER_nondet_ulong();
    }
  #line 42
    return (tmp);
  }
  }
  #line 45 "./arch/i386/lib/usercopy.c"
  __inline unsigned long copy_from_user(void *to , void *from , unsigned long n ) 
  { unsigned long tmp ;
  
    {
    {
  #line 48
    assert_context_process();
  #line 50
    tmp = __VERIFIER_nondet_ulong();
    }
  #line 50
    return (tmp);
  }
  }
  #line 1 "preproc_tEbVHW.o"
  #pragma merger(0,"preproc_tEbVHW.i","-x,c")
  #line 31 "./include/linux/slab.h"
  extern void kfree(void const   *m ) ;
  #line 509 "./include/linux/fs.h"
  int alloc_chrdev_region(dev_t *dev , unsigned int baseminor , unsigned int count ,
                          char const   *name ) ;
  #line 510
  int register_chrdev_region(dev_t from , unsigned int count , char const   *name ) ;
  #line 511
  int register_chrdev(unsigned int major , char const   *name , struct file_operations  const  *fops ) ;
  #line 513
  int unregister_chrdev(unsigned int major , char const   *name ) ;
  #line 12 "./include/linux/cdev.h"
  void cdev_init(struct cdev *cdev , struct file_operations  const  *fops ) ;
  #line 14
  __inline struct cdev *cdev_alloc(void) ;
  #line 18
  int cdev_add(struct cdev *p , dev_t dev , unsigned int count ) ;
  #line 20
  void cdev_del(struct cdev *p ) ;
  #line 24 "./fs/char_dev.c"
  int register_chrdev_region(dev_t from , unsigned int count , char const   *name ) 
  { int return_value ;
    int tmp ;
    int tmp___0 ;
  
    {
    {
  #line 26
    tmp = __VERIFIER_nondet_int();
  #line 26
    return_value = tmp;
    }
  #line 27
    if (return_value == 0) {
  #line 27
      tmp___0 = 1;
    } else
  #line 27
    if (return_value == -1) {
  #line 27
      tmp___0 = 1;
    } else {
  #line 27
      tmp___0 = 0;
    }
    {
  #line 27
    __CPROVER_assume(tmp___0);
    }
  #line 29
    return (return_value);
  }
  }
  #line 43 "./fs/char_dev.c"
  int alloc_chrdev_region(dev_t *dev , unsigned int baseminor , unsigned int count ,
                          char const   *name ) 
  { int major ;
    int return_value ;
    int tmp ;
    int tmp___0 ;
    unsigned int tmp___1 ;
    int __cil_tmp10 ;
    unsigned int __cil_tmp11 ;
  
    {
    {
  #line 47
    tmp = __VERIFIER_nondet_int();
  #line 47
    return_value = tmp;
    }
  #line 48
    if (return_value == 0) {
  #line 48
      tmp___0 = 1;
    } else
  #line 48
    if (return_value == -1) {
  #line 48
      tmp___0 = 1;
    } else {
  #line 48
      tmp___0 = 0;
    }
    {
  #line 48
    __CPROVER_assume(tmp___0);
    }
  #line 50
    if (return_value == 0) {
      {
  #line 51
      tmp___1 = __VERIFIER_nondet_uint();
  #line 51
      major = (int )tmp___1;
  #line 52
      __cil_tmp10 = major << 20;
  #line 52
      __cil_tmp11 = (unsigned int )__cil_tmp10;
  #line 52
      *dev = __cil_tmp11 | baseminor;
      }
    } else {
  
    }
  #line 55
    return (return_value);
  }
  }
  #line 80 "./fs/char_dev.c"
  int register_chrdev(unsigned int major , char const   *name , struct file_operations  const  *fops ) 
  { struct cdev *cdev ;
    int err ;
    int tmp ;
    dev_t __cil_tmp7 ;
    struct module *__cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    unsigned int __cil_tmp11 ;
    void const   *__cil_tmp12 ;
  
    {
    {
  #line 86
    __cil_tmp7 = (dev_t )0;
  #line 86
    tmp = register_chrdev_region(__cil_tmp7, 256U, name);
  #line 86
    major = (unsigned int )tmp;
  #line 88
    cdev = cdev_alloc();
  #line 89
    __cil_tmp8 = *((struct module * const  *)fops);
  #line 89
    *((struct module **)cdev) = (struct module *)__cil_tmp8;
  #line 90
    __cil_tmp9 = (unsigned long )cdev;
  #line 90
    __cil_tmp10 = __cil_tmp9 + 8;
  #line 90
    *((struct file_operations  const  **)__cil_tmp10) = fops;
  #line 92
    __cil_tmp11 = major << 20;
  #line 92
    err = cdev_add(cdev, __cil_tmp11, 256U);
    }
  #line 94
    if (err) {
      {
  #line 95
      __cil_tmp12 = (void const   *)cdev;
  #line 95
      kfree(__cil_tmp12);
      }
  #line 96
      return (err);
    } else {
  
    }
  #line 99
    return ((int )major);
  }
  }
  #line 103 "./fs/char_dev.c"
  int unregister_chrdev(unsigned int major , char const   *name ) 
  { 
  
    {
  #line 105
    return (0);
  }
  }
  #line 108 "./fs/char_dev.c"
  __inline struct cdev *cdev_alloc(void) 
  { int tmp ;
    unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
  
    {
  #line 110
    if (fixed_cdev_used < 10) {
  #line 111
      tmp = fixed_cdev_used;
  #line 111
      fixed_cdev_used = fixed_cdev_used + 1;
      {
  #line 111
      __cil_tmp2 = tmp * 24UL;
  #line 111
      __cil_tmp3 = (unsigned long )(fixed_cdev) + __cil_tmp2;
  #line 111
      return ((struct cdev *)__cil_tmp3);
      }
    } else {
  
    }
  #line 113
    return ((struct cdev *)0);
  }
  }
  #line 125 "./fs/char_dev.c"
  int cdev_add(struct cdev *p , dev_t dev , unsigned int count ) 
  { int return_value ;
    int tmp ;
    int tmp___0 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    int __cil_tmp11 ;
    unsigned long __cil_tmp12 ;
    unsigned long __cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    unsigned long __cil_tmp15 ;
    unsigned long __cil_tmp16 ;
    unsigned long __cil_tmp17 ;
    unsigned long __cil_tmp18 ;
    unsigned long __cil_tmp19 ;
    unsigned long __cil_tmp20 ;
    unsigned long __cil_tmp21 ;
    unsigned long __cil_tmp22 ;
    unsigned long __cil_tmp23 ;
    unsigned long __cil_tmp24 ;
    int __cil_tmp25 ;
    int __cil_tmp26 ;
  
    {
    {
  #line 127
    __cil_tmp7 = (unsigned long )p;
  #line 127
    __cil_tmp8 = __cil_tmp7 + 16;
  #line 127
    *((dev_t *)__cil_tmp8) = dev;
  #line 128
    __cil_tmp9 = (unsigned long )p;
  #line 128
    __cil_tmp10 = __cil_tmp9 + 20;
  #line 128
    *((unsigned int *)__cil_tmp10) = count;
  #line 130
    tmp = __VERIFIER_nondet_int();
  #line 130
    return_value = tmp;
    }
  #line 131
    if (return_value == 0) {
  #line 131
      tmp___0 = 1;
    } else
  #line 131
    if (return_value == -1) {
  #line 131
      tmp___0 = 1;
    } else {
  #line 131
      tmp___0 = 0;
    }
    {
  #line 131
    __CPROVER_assume(tmp___0);
    }
  #line 133
    if (return_value == 0) {
      {
  #line 134
      __cil_tmp11 = (int )number_cdev_registered;
  #line 134
      if (__cil_tmp11 < 10) {
  #line 136
        __cil_tmp12 = number_cdev_registered * 96UL;
  #line 136
        __cil_tmp13 = (unsigned long )(cdev_registered) + __cil_tmp12;
  #line 136
        *((struct cdev **)__cil_tmp13) = p;
  #line 137
        __cil_tmp14 = 64 + 4;
  #line 137
        __cil_tmp15 = number_cdev_registered * 96UL;
  #line 137
        __cil_tmp16 = __cil_tmp15 + __cil_tmp14;
  #line 137
        __cil_tmp17 = (unsigned long )(cdev_registered) + __cil_tmp16;
  #line 137
        *((dev_t *)__cil_tmp17) = dev;
  #line 138
        __cil_tmp18 = 64 + 16;
  #line 138
        __cil_tmp19 = number_cdev_registered * 96UL;
  #line 138
        __cil_tmp20 = __cil_tmp19 + __cil_tmp18;
  #line 138
        __cil_tmp21 = (unsigned long )(cdev_registered) + __cil_tmp20;
  #line 138
        *((struct cdev **)__cil_tmp21) = p;
  #line 139
        __cil_tmp22 = number_cdev_registered * 96UL;
  #line 139
        __cil_tmp23 = __cil_tmp22 + 88;
  #line 139
        __cil_tmp24 = (unsigned long )(cdev_registered) + __cil_tmp23;
  #line 139
        *((int *)__cil_tmp24) = 0;
  #line 141
        __cil_tmp25 = (int )number_cdev_registered;
  #line 141
        __cil_tmp26 = __cil_tmp25 + 1;
  #line 141
        number_cdev_registered = (short )__cil_tmp26;
      } else {
  #line 143
        return (-1);
      }
      }
    } else {
  
    }
  #line 147
    return (return_value);
  }
  }
  #line 157 "./fs/char_dev.c"
  void cdev_del(struct cdev *p ) 
  { int i ;
    int __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    unsigned long __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    struct cdev *__cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
  
    {
  #line 161
    i = 0;
    {
  #line 161
    while (1) {
      while_continue: /* CIL Label */ ;
      {
  #line 161
      __cil_tmp3 = (int )number_cdev_registered;
  #line 161
      if (i < __cil_tmp3) {
  
      } else {
  #line 161
        goto while_break;
      }
      }
      {
  #line 162
      __cil_tmp4 = (unsigned long )p;
  #line 162
      __cil_tmp5 = i * 96UL;
  #line 162
      __cil_tmp6 = (unsigned long )(cdev_registered) + __cil_tmp5;
  #line 162
      __cil_tmp7 = *((struct cdev **)__cil_tmp6);
  #line 162
      __cil_tmp8 = (unsigned long )__cil_tmp7;
  #line 162
      if (__cil_tmp8 == __cil_tmp4) {
  #line 163
        __cil_tmp9 = i * 96UL;
  #line 163
        __cil_tmp10 = (unsigned long )(cdev_registered) + __cil_tmp9;
  #line 163
        *((struct cdev **)__cil_tmp10) = (struct cdev *)0;
  #line 165
        return;
      } else {
  
      }
      }
  #line 161
      i = i + 1;
    }
    while_break: /* CIL Label */ ;
    }
  #line 168
    return;
  }
  }
  #line 178 "./fs/char_dev.c"
  void cdev_init(struct cdev *cdev , struct file_operations  const  *fops ) 
  { unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
  
    {
  #line 180
    __cil_tmp3 = (unsigned long )cdev;
  #line 180
    __cil_tmp4 = __cil_tmp3 + 8;
  #line 180
    *((struct file_operations  const  **)__cil_tmp4) = fops;
  #line 181
    return;
  }
  }
  #line 1 "preproc_zJ3ett.o"
  #pragma merger(0,"preproc_zJ3ett.i","-x,c")
  #line 61 "./include/linux/mutex.h"
  void mutex_init(struct mutex *lock ) ;
  #line 63
  __inline void mutex_lock(struct mutex *lock ) ;
  #line 65
  void mutex_unlock(struct mutex *lock ) ;
  #line 26 "./kernel/mutex.c"
  void mutex_init(struct mutex *lock ) 
  { int __cil_tmp2 ;
    int __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    unsigned long __cil_tmp5 ;
  
    {
    {
  #line 30
    __CPROVER_atomic_begin();
  #line 32
    __cil_tmp2 = *((int *)lock);
  #line 32
    __cil_tmp3 = ! __cil_tmp2;
  #line 32
    __CPROVER_assert(__cil_tmp3, "Locked mutex must not be reinitialized");
  #line 34
    *((int *)lock) = 0;
  #line 35
    __cil_tmp4 = (unsigned long )lock;
  #line 35
    __cil_tmp5 = __cil_tmp4 + 4;
  #line 35
    *((int *)__cil_tmp5) = 1;
  #line 36
    __CPROVER_atomic_end();
    }
  #line 37
    return;
  }
  }
  #line 60 "./kernel/mutex.c"
  __inline void mutex_lock(struct mutex *lock ) 
  { unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
    int __cil_tmp4 ;
    int __cil_tmp5 ;
  
    {
    {
  #line 65
    __CPROVER_atomic_begin();
  #line 66
    assert_context_process();
  #line 67
    __cil_tmp2 = (unsigned long )lock;
  #line 67
    __cil_tmp3 = __cil_tmp2 + 4;
  #line 67
    __cil_tmp4 = *((int *)__cil_tmp3);
  #line 67
    __CPROVER_assert(__cil_tmp4, "Mutex is not initialized");
  #line 68
    __CPROVER_atomic_end();
    }
    {
  #line 71
    while (1) {
      while_continue: /* CIL Label */ ;
      {
  #line 73
      __CPROVER_atomic_begin();
      }
      {
  #line 74
      __cil_tmp5 = *((int *)lock);
  #line 74
      if (__cil_tmp5 == 0) {
        {
  #line 76
        *((int *)lock) = 1;
  #line 77
        __CPROVER_atomic_end();
        }
  #line 78
        return;
      } else {
  
      }
      }
      {
  #line 80
      __CPROVER_atomic_end();
      }
    }
    while_break: /* CIL Label */ ;
    }
  }
  }
  #line 96 "./kernel/mutex.c"
  void mutex_unlock(struct mutex *lock ) 
  { int __cil_tmp2 ;
  
    {
    {
  #line 99
    __CPROVER_atomic_begin();
  #line 100
    assert_context_process();
  #line 102
    __cil_tmp2 = *((int *)lock);
  #line 102
    __CPROVER_assert(__cil_tmp2, "Unlock a not locked mutex");
  #line 104
    *((int *)lock) = 0;
  #line 105
    __CPROVER_atomic_end();
    }
  #line 106
    return;
  }
  }
  #line 1 "preproc_n2X7uo.o"
  #pragma merger(0,"preproc_n2X7uo.i","-x,c")
  #line 22 "cprover/ddverify/include/ddverify/satabs.h"
  extern unsigned char __VERIFIER_nondet_uchar() ;
  #line 23
  extern unsigned int __VERIFIER_nondet_unsigned() ;
  #line 10 "cprover/ddverify/include/ddverify/ioport.h"
  int ddv_ioport_request_start  ;
  #line 11 "cprover/ddverify/include/ddverify/ioport.h"
  int ddv_ioport_request_len  ;
  #line 15 "./kernel/resource.c"
  struct resource *request_region(unsigned long start , unsigned long len , char const   *name ) 
  { struct resource *resource ;
    void *tmp ;
    size_t __cil_tmp6 ;
  
    {
    {
  #line 18
    __cil_tmp6 = (size_t )32UL;
  #line 18
    tmp = malloc(__cil_tmp6);
  #line 18
    resource = (struct resource *)tmp;
  #line 23
    ddv_ioport_request_start = (int )start;
  #line 24
    ddv_ioport_request_len = (int )len;
    }
  #line 26
    return (resource);
  }
  }
  #line 29 "./kernel/resource.c"
  void release_region(unsigned long start , unsigned long len ) 
  { unsigned int i ;
  
    {
  #line 31
    i = 0U;
  #line 37
    ddv_ioport_request_start = 0;
  #line 38
    ddv_ioport_request_len = 0;
  #line 39
    return;
  }
  }
  #line 41 "./kernel/resource.c"
  __inline unsigned char inb(unsigned int port ) 
  { int tmp ;
    unsigned char tmp___0 ;
    unsigned int __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned int __cil_tmp6 ;
  
    {
    {
  #line 44
    __cil_tmp4 = (unsigned int )ddv_ioport_request_start;
  #line 44
    if (port >= __cil_tmp4) {
      {
  #line 44
      __cil_tmp5 = ddv_ioport_request_start + ddv_ioport_request_len;
  #line 44
      __cil_tmp6 = (unsigned int )__cil_tmp5;
  #line 44
      if (port < __cil_tmp6) {
  #line 44
        tmp = 1;
      } else {
  #line 44
        tmp = 0;
      }
      }
    } else {
  #line 44
      tmp = 0;
    }
    }
    {
  #line 44
    __CPROVER_assert(tmp, "I/O port is requested");
  #line 46
    tmp___0 = __VERIFIER_nondet_uchar();
    }
  #line 46
    return (tmp___0);
  }
  }
  #line 49 "./kernel/resource.c"
  __inline void outb(unsigned char byte , unsigned int port ) 
  { int tmp ;
    unsigned int __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned int __cil_tmp6 ;
  
    {
    {
  #line 52
    __cil_tmp4 = (unsigned int )ddv_ioport_request_start;
  #line 52
    if (port >= __cil_tmp4) {
      {
  #line 52
      __cil_tmp5 = ddv_ioport_request_start + ddv_ioport_request_len;
  #line 52
      __cil_tmp6 = (unsigned int )__cil_tmp5;
  #line 52
      if (port < __cil_tmp6) {
  #line 52
        tmp = 1;
      } else {
  #line 52
        tmp = 0;
      }
      }
    } else {
  #line 52
      tmp = 0;
    }
    }
    {
  #line 52
    __CPROVER_assert(tmp, "I/O port is requested");
    }
  #line 53
    return;
  }
  }
  #line 55 "./kernel/resource.c"
  __inline unsigned short inw(unsigned int port ) 
  { int tmp ;
    unsigned short tmp___0 ;
    unsigned int __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned int __cil_tmp6 ;
  
    {
    {
  #line 58
    __cil_tmp4 = (unsigned int )ddv_ioport_request_start;
  #line 58
    if (port >= __cil_tmp4) {
      {
  #line 58
      __cil_tmp5 = ddv_ioport_request_start + ddv_ioport_request_len;
  #line 58
      __cil_tmp6 = (unsigned int )__cil_tmp5;
  #line 58
      if (port < __cil_tmp6) {
  #line 58
        tmp = 1;
      } else {
  #line 58
        tmp = 0;
      }
      }
    } else {
  #line 58
      tmp = 0;
    }
    }
    {
  #line 58
    __CPROVER_assert(tmp, "I/O port is requested");
  #line 60
    tmp___0 = __VERIFIER_nondet_ushort();
    }
  #line 60
    return (tmp___0);
  }
  }
  #line 63 "./kernel/resource.c"
  __inline void outw(unsigned short word , unsigned int port ) 
  { int tmp ;
    unsigned int __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned int __cil_tmp6 ;
  
    {
    {
  #line 66
    __cil_tmp4 = (unsigned int )ddv_ioport_request_start;
  #line 66
    if (port >= __cil_tmp4) {
      {
  #line 66
      __cil_tmp5 = ddv_ioport_request_start + ddv_ioport_request_len;
  #line 66
      __cil_tmp6 = (unsigned int )__cil_tmp5;
  #line 66
      if (port < __cil_tmp6) {
  #line 66
        tmp = 1;
      } else {
  #line 66
        tmp = 0;
      }
      }
    } else {
  #line 66
      tmp = 0;
    }
    }
    {
  #line 66
    __CPROVER_assert(tmp, "I/O port is requested");
    }
  #line 67
    return;
  }
  }
  #line 69 "./kernel/resource.c"
  __inline unsigned int inl(unsigned int port ) 
  { int tmp ;
    unsigned int tmp___0 ;
    unsigned int __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned int __cil_tmp6 ;
  
    {
    {
  #line 72
    __cil_tmp4 = (unsigned int )ddv_ioport_request_start;
  #line 72
    if (port >= __cil_tmp4) {
      {
  #line 72
      __cil_tmp5 = ddv_ioport_request_start + ddv_ioport_request_len;
  #line 72
      __cil_tmp6 = (unsigned int )__cil_tmp5;
  #line 72
      if (port < __cil_tmp6) {
  #line 72
        tmp = 1;
      } else {
  #line 72
        tmp = 0;
      }
      }
    } else {
  #line 72
      tmp = 0;
    }
    }
    {
  #line 72
    __CPROVER_assert(tmp, "I/O port is requested");
  #line 74
    tmp___0 = __VERIFIER_nondet_unsigned();
    }
  #line 74
    return (tmp___0);
  }
  }
  #line 77 "./kernel/resource.c"
  __inline void outl(unsigned int doubleword , unsigned int port ) 
  { int tmp ;
    unsigned int __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned int __cil_tmp6 ;
  
    {
    {
  #line 80
    __cil_tmp4 = (unsigned int )ddv_ioport_request_start;
  #line 80
    if (port >= __cil_tmp4) {
      {
  #line 80
      __cil_tmp5 = ddv_ioport_request_start + ddv_ioport_request_len;
  #line 80
      __cil_tmp6 = (unsigned int )__cil_tmp5;
  #line 80
      if (port < __cil_tmp6) {
  #line 80
        tmp = 1;
      } else {
  #line 80
        tmp = 0;
      }
      }
    } else {
  #line 80
      tmp = 0;
    }
    }
    {
  #line 80
    __CPROVER_assert(tmp, "I/O port is requested");
    }
  #line 81
    return;
  }
  }
  #line 1 "preproc_b73RtZ.o"
  #pragma merger(0,"preproc_b73RtZ.i","-x,c")
  #line 19 "cprover/ddverify/include/ddverify/satabs.h"
  extern long __VERIFIER_nondet_long() ;
  #line 46 "./include/linux/sched.h"
  long schedule_timeout(long timeout ) ;
  #line 48
  void schedule(void) ;
  #line 31 "./kernel/sched.c"
  void schedule(void) 
  { 
  
    {
    {
  #line 33
    assert_context_process();
    }
  #line 34
    return;
  }
  }
  #line 36 "./kernel/sched.c"
  long schedule_timeout(long timeout ) 
  { long tmp ;
  
    {
    {
  #line 38
    assert_context_process();
  #line 40
    tmp = __VERIFIER_nondet_long();
    }
  #line 40
    return (tmp);
  }
  }
  #line 1 "preproc_YCof8w.o"
  #pragma merger(0,"preproc_YCof8w.i","-x,c")
  #line 23 "./include/asm/semaphore.h"
  __inline void sema_init(struct semaphore *sem , int val ) ;
  #line 25
  __inline void init_MUTEX(struct semaphore *sem ) ;
  #line 27
  __inline void init_MUTEX_LOCKED(struct semaphore *sem ) ;
  #line 29
  __inline void down(struct semaphore *sem ) ;
  #line 31
  __inline int down_interruptible(struct semaphore *sem ) ;
  #line 33
  __inline int down_trylock(struct semaphore *sem ) ;
  #line 35
  __inline void up(struct semaphore *sem ) ;
  #line 6 "./arch/i386/kernel/semaphore.c"
  __inline void sema_init(struct semaphore *sem , int val ) 
  { unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
  
    {
    {
  #line 9
    __CPROVER_atomic_begin();
  #line 10
    *((int *)sem) = 1;
  #line 11
    __cil_tmp3 = (unsigned long )sem;
  #line 11
    __cil_tmp4 = __cil_tmp3 + 4;
  #line 11
    *((int *)__cil_tmp4) = 0;
  #line 12
    __CPROVER_atomic_end();
    }
  #line 13
    return;
  }
  }
  #line 15 "./arch/i386/kernel/semaphore.c"
  __inline void init_MUTEX(struct semaphore *sem ) 
  { unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
  
    {
    {
  #line 18
    __CPROVER_atomic_begin();
  #line 19
    *((int *)sem) = 1;
  #line 20
    __cil_tmp2 = (unsigned long )sem;
  #line 20
    __cil_tmp3 = __cil_tmp2 + 4;
  #line 20
    *((int *)__cil_tmp3) = 0;
  #line 21
    __CPROVER_atomic_end();
    }
  #line 22
    return;
  }
  }
  #line 24 "./arch/i386/kernel/semaphore.c"
  __inline void init_MUTEX_LOCKED(struct semaphore *sem ) 
  { unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
  
    {
    {
  #line 27
    __CPROVER_atomic_begin();
  #line 28
    *((int *)sem) = 1;
  #line 29
    __cil_tmp2 = (unsigned long )sem;
  #line 29
    __cil_tmp3 = __cil_tmp2 + 4;
  #line 29
    *((int *)__cil_tmp3) = 1;
  #line 30
    __CPROVER_atomic_end();
    }
  #line 31
    return;
  }
  }
  #line 33 "./arch/i386/kernel/semaphore.c"
  __inline void down(struct semaphore *sem ) 
  { int __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
  
    {
    {
  #line 38
    __CPROVER_atomic_begin();
  #line 39
    assert_context_process();
  #line 40
    __cil_tmp2 = *((int *)sem);
  #line 40
    __CPROVER_assert(__cil_tmp2, "Semaphore is not initialized");
  #line 41
    __CPROVER_atomic_end();
    }
    {
  #line 44
    while (1) {
      while_continue: /* CIL Label */ ;
      {
  #line 46
      __CPROVER_atomic_begin();
      }
      {
  #line 47
      __cil_tmp3 = (unsigned long )sem;
  #line 47
      __cil_tmp4 = __cil_tmp3 + 4;
  #line 47
      __cil_tmp5 = *((int *)__cil_tmp4);
  #line 47
      if (__cil_tmp5 == 0) {
        {
  #line 49
        __cil_tmp6 = (unsigned long )sem;
  #line 49
        __cil_tmp7 = __cil_tmp6 + 4;
  #line 49
        *((int *)__cil_tmp7) = 1;
  #line 50
        __CPROVER_atomic_end();
        }
  #line 51
        return;
      } else {
  
      }
      }
      {
  #line 53
      __CPROVER_atomic_end();
      }
    }
    while_break: /* CIL Label */ ;
    }
  }
  }
  #line 58 "./arch/i386/kernel/semaphore.c"
  __inline int down_interruptible(struct semaphore *sem ) 
  { int tmp ;
    int __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    unsigned long __cil_tmp5 ;
    int __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
  
    {
    {
  #line 63
    __CPROVER_atomic_begin();
  #line 64
    assert_context_process();
  #line 65
    __cil_tmp3 = *((int *)sem);
  #line 65
    __CPROVER_assert(__cil_tmp3, "Semaphore is not initialized");
  #line 66
    __CPROVER_atomic_end();
    }
    {
  #line 69
    while (1) {
      while_continue: /* CIL Label */ ;
      {
  #line 71
      __CPROVER_atomic_begin();
      }
      {
  #line 72
      __cil_tmp4 = (unsigned long )sem;
  #line 72
      __cil_tmp5 = __cil_tmp4 + 4;
  #line 72
      __cil_tmp6 = *((int *)__cil_tmp5);
  #line 72
      if (__cil_tmp6 == 0) {
        {
  #line 74
        __cil_tmp7 = (unsigned long )sem;
  #line 74
        __cil_tmp8 = __cil_tmp7 + 4;
  #line 74
        *((int *)__cil_tmp8) = 1;
  #line 75
        __CPROVER_atomic_end();
        }
  #line 76
        return (0);
      } else {
  
      }
      }
      {
  #line 78
      tmp = __VERIFIER_nondet_int();
      }
  #line 78
      if (tmp) {
        {
  #line 79
        __CPROVER_atomic_end();
        }
  #line 80
        return (-1);
      } else {
  
      }
      {
  #line 83
      __CPROVER_atomic_end();
      }
    }
    while_break: /* CIL Label */ ;
    }
  }
  }
  #line 88 "./arch/i386/kernel/semaphore.c"
  __inline int down_trylock(struct semaphore *sem ) 
  { int __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
  
    {
    {
  #line 91
    __CPROVER_atomic_begin();
  #line 94
    __cil_tmp2 = *((int *)sem);
  #line 94
    __CPROVER_assert(__cil_tmp2, "Semaphore is not initialized");
    }
    {
  #line 97
    __cil_tmp3 = (unsigned long )sem;
  #line 97
    __cil_tmp4 = __cil_tmp3 + 4;
  #line 97
    __cil_tmp5 = *((int *)__cil_tmp4);
  #line 97
    if (__cil_tmp5 == 0) {
      {
  #line 98
      __cil_tmp6 = (unsigned long )sem;
  #line 98
      __cil_tmp7 = __cil_tmp6 + 4;
  #line 98
      *((int *)__cil_tmp7) = 1;
  #line 99
      __CPROVER_atomic_end();
      }
  #line 100
      return (-1);
    } else {
  
    }
    }
    {
  #line 102
    __CPROVER_atomic_end();
    }
  #line 103
    return (0);
  }
  }
  #line 106 "./arch/i386/kernel/semaphore.c"
  __inline void up(struct semaphore *sem ) 
  { unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
    int __cil_tmp4 ;
    unsigned long __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
  
    {
    {
  #line 109
    __CPROVER_atomic_begin();
  #line 110
    assert_context_process();
  #line 112
    __cil_tmp2 = (unsigned long )sem;
  #line 112
    __cil_tmp3 = __cil_tmp2 + 4;
  #line 112
    __cil_tmp4 = *((int *)__cil_tmp3);
  #line 112
    __CPROVER_assert(__cil_tmp4, "Unlock a not locked semaphore");
  #line 114
    __cil_tmp5 = (unsigned long )sem;
  #line 114
    __cil_tmp6 = __cil_tmp5 + 4;
  #line 114
    *((int *)__cil_tmp6) = 0;
  #line 115
    __CPROVER_atomic_end();
    }
  #line 116
    return;
  }
  }
  #line 1 "preproc_tkU6QR.o"
  #pragma merger(0,"preproc_tkU6QR.i","-x,c")
  #line 50 "./include/linux/interrupt.h"
  __inline void tasklet_schedule(struct tasklet_struct *t ) ;
  #line 65
  void tasklet_init(struct tasklet_struct *t , void (*func)(unsigned long  ) , unsigned long data ) ;
  #line 12 "./kernel/softirq.c"
  __inline void tasklet_schedule(struct tasklet_struct *t ) 
  { int i ;
    int next_free ;
    unsigned long __cil_tmp4 ;
    unsigned long __cil_tmp5 ;
    int __cil_tmp6 ;
    void *__cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    struct tasklet_struct *__cil_tmp11 ;
    unsigned long __cil_tmp12 ;
    unsigned long __cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    unsigned long __cil_tmp15 ;
    struct tasklet_struct *__cil_tmp16 ;
    unsigned long __cil_tmp17 ;
    unsigned long __cil_tmp18 ;
    unsigned long __cil_tmp19 ;
    unsigned long __cil_tmp20 ;
    unsigned short __cil_tmp21 ;
    int __cil_tmp22 ;
    int __cil_tmp23 ;
    unsigned long __cil_tmp24 ;
    unsigned long __cil_tmp25 ;
    unsigned long __cil_tmp26 ;
    unsigned long __cil_tmp27 ;
    unsigned long __cil_tmp28 ;
  
    {
    {
  #line 15
    next_free = -1;
  #line 18
    __cil_tmp4 = (unsigned long )t;
  #line 18
    __cil_tmp5 = __cil_tmp4 + 24;
  #line 18
    __cil_tmp6 = *((int *)__cil_tmp5);
  #line 18
    __CPROVER_assert(__cil_tmp6, "Tasklet is uninitialized!");
  #line 21
    i = 0;
    }
    {
  #line 21
    while (1) {
      while_continue: /* CIL Label */ ;
  #line 21
      if (i < 10) {
  
      } else {
  #line 21
        goto while_break;
      }
      {
  #line 22
      __cil_tmp7 = (void *)0;
  #line 22
      __cil_tmp8 = (unsigned long )__cil_tmp7;
  #line 22
      __cil_tmp9 = i * 16UL;
  #line 22
      __cil_tmp10 = (unsigned long )(tasklet_registered) + __cil_tmp9;
  #line 22
      __cil_tmp11 = *((struct tasklet_struct **)__cil_tmp10);
  #line 22
      __cil_tmp12 = (unsigned long )__cil_tmp11;
  #line 22
      if (__cil_tmp12 == __cil_tmp8) {
  #line 23
        next_free = i;
      } else {
  
      }
      }
      {
  #line 25
      __cil_tmp13 = (unsigned long )t;
  #line 25
      __cil_tmp14 = i * 16UL;
  #line 25
      __cil_tmp15 = (unsigned long )(tasklet_registered) + __cil_tmp14;
  #line 25
      __cil_tmp16 = *((struct tasklet_struct **)__cil_tmp15);
  #line 25
      __cil_tmp17 = (unsigned long )__cil_tmp16;
  #line 25
      if (__cil_tmp17 == __cil_tmp13) {
        {
  #line 25
        __cil_tmp18 = i * 16UL;
  #line 25
        __cil_tmp19 = __cil_tmp18 + 8;
  #line 25
        __cil_tmp20 = (unsigned long )(tasklet_registered) + __cil_tmp19;
  #line 25
        __cil_tmp21 = *((unsigned short *)__cil_tmp20);
  #line 25
        __cil_tmp22 = (int )__cil_tmp21;
  #line 25
        if (__cil_tmp22 == 0) {
  #line 27
          return;
        } else {
  
        }
        }
      } else {
  
      }
      }
  #line 21
      i = i + 1;
    }
    while_break: /* CIL Label */ ;
    }
    {
  #line 33
    __cil_tmp23 = next_free != -1;
  #line 33
    __CPROVER_assert(__cil_tmp23, "Number of supported tasklets is insufficient");
  #line 36
    __cil_tmp24 = next_free * 16UL;
  #line 36
    __cil_tmp25 = (unsigned long )(tasklet_registered) + __cil_tmp24;
  #line 36
    *((struct tasklet_struct **)__cil_tmp25) = t;
  #line 37
    __cil_tmp26 = next_free * 16UL;
  #line 37
    __cil_tmp27 = __cil_tmp26 + 8;
  #line 37
    __cil_tmp28 = (unsigned long )(tasklet_registered) + __cil_tmp27;
  #line 37
    *((unsigned short *)__cil_tmp28) = (unsigned short)0;
    }
  #line 38
    return;
  }
  }
  #line 42 "./kernel/softirq.c"
  void tasklet_init(struct tasklet_struct *t , void (*func)(unsigned long  ) , unsigned long data ) 
  { unsigned long __cil_tmp4 ;
    unsigned long __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
  
    {
  #line 45
    *((atomic_t *)t) = 0;
  #line 46
    __cil_tmp4 = (unsigned long )t;
  #line 46
    __cil_tmp5 = __cil_tmp4 + 24;
  #line 46
    *((int *)__cil_tmp5) = 0;
  #line 47
    __cil_tmp6 = (unsigned long )t;
  #line 47
    __cil_tmp7 = __cil_tmp6 + 8;
  #line 47
    *((void (**)(unsigned long  ))__cil_tmp7) = func;
  #line 48
    __cil_tmp8 = (unsigned long )t;
  #line 48
    __cil_tmp9 = __cil_tmp8 + 16;
  #line 48
    *((unsigned long *)__cil_tmp9) = data;
  #line 49
    return;
  }
  }
  #line 1 "preproc_lzKrXP.o"
  #pragma merger(0,"preproc_lzKrXP.i","-x,c")
  #line 55 "./include/linux/spinlock.h"
  __inline void spin_lock(spinlock_t *lock ) ;
  #line 56
  __inline void spin_lock_irqsave(spinlock_t *lock , unsigned long flags ) ;
  #line 60
  __inline void spin_unlock(spinlock_t *lock ) ;
  #line 61
  __inline void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags ) ;
  #line 20 "./kernel/spinlock.c"
  void spin_lock_init(spinlock_t *lock ) 
  { unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
  
    {
  #line 22
    *((int *)lock) = 1;
  #line 23
    __cil_tmp2 = (unsigned long )lock;
  #line 23
    __cil_tmp3 = __cil_tmp2 + 4;
  #line 23
    *((int *)__cil_tmp3) = 0;
  #line 24
    return;
  }
  }
  #line 26 "./kernel/spinlock.c"
  __inline void spin_lock(spinlock_t *lock ) 
  { int __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
  
    {
    {
  #line 31
    __CPROVER_atomic_begin();
  #line 32
    __cil_tmp2 = *((int *)lock);
  #line 32
    __CPROVER_assert(__cil_tmp2, "Spinlock is not initialized");
  #line 33
    __CPROVER_atomic_end();
    }
    {
  #line 36
    while (1) {
      while_continue: /* CIL Label */ ;
      {
  #line 38
      __CPROVER_atomic_begin();
      }
      {
  #line 39
      __cil_tmp3 = (unsigned long )lock;
  #line 39
      __cil_tmp4 = __cil_tmp3 + 4;
  #line 39
      __cil_tmp5 = *((int *)__cil_tmp4);
  #line 39
      if (__cil_tmp5 == 0) {
        {
  #line 41
        __cil_tmp6 = (unsigned long )lock;
  #line 41
        __cil_tmp7 = __cil_tmp6 + 4;
  #line 41
        *((int *)__cil_tmp7) = 1;
  #line 42
        __CPROVER_atomic_end();
        }
  #line 43
        return;
      } else {
  
      }
      }
      {
  #line 45
      __CPROVER_atomic_end();
      }
    }
    while_break: /* CIL Label */ ;
    }
  }
  }
  #line 50 "./kernel/spinlock.c"
  __inline void spin_lock_irqsave(spinlock_t *lock , unsigned long flags ) 
  { int __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    unsigned long __cil_tmp5 ;
    int __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
  
    {
    {
  #line 55
    __CPROVER_atomic_begin();
  #line 56
    __cil_tmp3 = *((int *)lock);
  #line 56
    __CPROVER_assert(__cil_tmp3, "Spinlock is not initialized");
  #line 57
    __CPROVER_atomic_end();
    }
    {
  #line 60
    while (1) {
      while_continue: /* CIL Label */ ;
      {
  #line 62
      __CPROVER_atomic_begin();
      }
      {
  #line 63
      __cil_tmp4 = (unsigned long )lock;
  #line 63
      __cil_tmp5 = __cil_tmp4 + 4;
  #line 63
      __cil_tmp6 = *((int *)__cil_tmp5);
  #line 63
      if (__cil_tmp6 == 0) {
        {
  #line 65
        __cil_tmp7 = (unsigned long )lock;
  #line 65
        __cil_tmp8 = __cil_tmp7 + 4;
  #line 65
        *((int *)__cil_tmp8) = 1;
  #line 66
        __CPROVER_atomic_end();
        }
  #line 67
        return;
      } else {
  
      }
      }
      {
  #line 69
      __CPROVER_atomic_end();
      }
    }
    while_break: /* CIL Label */ ;
    }
  }
  }
  #line 122 "./kernel/spinlock.c"
  __inline void spin_unlock(spinlock_t *lock ) 
  { unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
    int __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
  
    {
    {
  #line 125
    __CPROVER_atomic_begin();
  #line 127
    __cil_tmp2 = (unsigned long )lock;
  #line 127
    __cil_tmp3 = __cil_tmp2 + 4;
  #line 127
    __cil_tmp4 = *((int *)__cil_tmp3);
  #line 127
    __cil_tmp5 = __cil_tmp4 == 1;
  #line 127
    __CPROVER_assert(__cil_tmp5, "Unlock a not locked spinlock");
  #line 129
    __cil_tmp6 = (unsigned long )lock;
  #line 129
    __cil_tmp7 = __cil_tmp6 + 4;
  #line 129
    *((int *)__cil_tmp7) = 0;
  #line 130
    __CPROVER_atomic_end();
    }
  #line 131
    return;
  }
  }
  #line 133 "./kernel/spinlock.c"
  __inline void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags ) 
  { unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    int __cil_tmp5 ;
    int __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
  
    {
    {
  #line 136
    __CPROVER_atomic_begin();
  #line 138
    __cil_tmp3 = (unsigned long )lock;
  #line 138
    __cil_tmp4 = __cil_tmp3 + 4;
  #line 138
    __cil_tmp5 = *((int *)__cil_tmp4);
  #line 138
    __cil_tmp6 = __cil_tmp5 == 1;
  #line 138
    __CPROVER_assert(__cil_tmp6, "Unlock a not locked spinlock");
  #line 140
    __cil_tmp7 = (unsigned long )lock;
  #line 140
    __cil_tmp8 = __cil_tmp7 + 4;
  #line 140
    *((int *)__cil_tmp8) = 0;
  #line 141
    __CPROVER_atomic_end();
    }
  #line 142
    return;
  }
  }
  #line 1 "preproc_ghkA3T.o"
  #pragma merger(0,"preproc_ghkA3T.i","-x,c")
  #line 26 "./include/linux/timer.h"
  void init_timer(struct timer_list *timer ) ;
  #line 27
  __inline void add_timer(struct timer_list *timer ) ;
  #line 28
  void add_timer_on(struct timer_list *timer , int cpu ) ;
  #line 29
  int del_timer(struct timer_list *timer ) ;
  #line 30
  int mod_timer(struct timer_list *timer , unsigned long expires ) ;
  #line 32 "./kernel/timer.c"
  void init_timer(struct timer_list *timer ) 
  { int __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    unsigned long __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    int __cil_tmp9 ;
    int __cil_tmp10 ;
  
    {
    {
  #line 34
    __cil_tmp2 = (int )number_timer_registered;
  #line 34
    if (__cil_tmp2 < 5) {
  #line 35
      __cil_tmp3 = (unsigned long )timer;
  #line 35
      __cil_tmp4 = __cil_tmp3 + 24;
  #line 35
      *((short *)__cil_tmp4) = (short)0;
  #line 36
      __cil_tmp5 = (unsigned long )timer;
  #line 36
      __cil_tmp6 = __cil_tmp5 + 26;
  #line 36
      *((short *)__cil_tmp6) = (short)1;
  #line 37
      __cil_tmp7 = number_timer_registered * 8UL;
  #line 37
      __cil_tmp8 = (unsigned long )(timer_registered) + __cil_tmp7;
  #line 37
      *((struct timer_list **)__cil_tmp8) = timer;
  #line 39
      __cil_tmp9 = (int )number_timer_registered;
  #line 39
      __cil_tmp10 = __cil_tmp9 + 1;
  #line 39
      number_timer_registered = (short )__cil_tmp10;
    } else {
  
    }
    }
  #line 41
    return;
  }
  }
  #line 43 "./kernel/timer.c"
  __inline void add_timer(struct timer_list *timer ) 
  { unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
    short __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
  
    {
    {
  #line 47
    __cil_tmp2 = (unsigned long )timer;
  #line 47
    __cil_tmp3 = __cil_tmp2 + 26;
  #line 47
    __cil_tmp4 = *((short *)__cil_tmp3);
  #line 47
    __cil_tmp5 = (int )__cil_tmp4;
  #line 47
    __CPROVER_assert(__cil_tmp5, "Timer is initialized");
  #line 49
    __cil_tmp6 = (unsigned long )timer;
  #line 49
    __cil_tmp7 = __cil_tmp6 + 24;
  #line 49
    *((short *)__cil_tmp7) = (short)1;
    }
  #line 50
    return;
  }
  }
  #line 59 "./kernel/timer.c"
  void add_timer_on(struct timer_list *timer , int cpu ) 
  { 
  
    {
    {
  #line 62
    add_timer(timer);
    }
  #line 63
    return;
  }
  }
  #line 86 "./kernel/timer.c"
  int mod_timer(struct timer_list *timer , unsigned long expires ) 
  { unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    short __cil_tmp5 ;
    int __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
  
    {
    {
  #line 90
    __cil_tmp3 = (unsigned long )timer;
  #line 90
    __cil_tmp4 = __cil_tmp3 + 26;
  #line 90
    __cil_tmp5 = *((short *)__cil_tmp4);
  #line 90
    __cil_tmp6 = (int )__cil_tmp5;
  #line 90
    __CPROVER_assert(__cil_tmp6, "Timer is initialized");
  #line 92
    *((unsigned long *)timer) = expires;
  #line 93
    __cil_tmp7 = (unsigned long )timer;
  #line 93
    __cil_tmp8 = __cil_tmp7 + 24;
  #line 93
    *((short *)__cil_tmp8) = (short)1;
    }
  #line 94
    return (0);
  }
  }
  #line 107 "./kernel/timer.c"
  int del_timer(struct timer_list *timer ) 
  { unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
  
    {
  #line 109
    __cil_tmp2 = (unsigned long )timer;
  #line 109
    __cil_tmp3 = __cil_tmp2 + 24;
  #line 109
    *((short *)__cil_tmp3) = (short)0;
  #line 110
    return (0);
  }
  }
  #line 1 "preproc_VEdeYf.o"
  #pragma merger(0,"preproc_VEdeYf.i","-x,c")
  #line 47 "./include/linux/wait.h"
  void init_waitqueue_head(wait_queue_head_t *q ) ;
  #line 55
  __inline void wake_up(wait_queue_head_t *q ) ;
  #line 8 "./kernel/wait.c"
  void init_waitqueue_head(wait_queue_head_t *q ) 
  { unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
  
    {
  #line 10
    __cil_tmp2 = (unsigned long )q;
  #line 10
    __cil_tmp3 = __cil_tmp2 + 8;
  #line 10
    *((int *)__cil_tmp3) = 1;
  #line 11
    return;
  }
  }
  #line 13 "./kernel/wait.c"
  __inline void wake_up(wait_queue_head_t *q ) 
  { unsigned long __cil_tmp2 ;
    unsigned long __cil_tmp3 ;
    int __cil_tmp4 ;
  
    {
    {
  #line 17
    __cil_tmp2 = (unsigned long )q;
  #line 17
    __cil_tmp3 = __cil_tmp2 + 8;
  #line 17
    __cil_tmp4 = *((int *)__cil_tmp3);
  #line 17
    __CPROVER_assert(__cil_tmp4, "Wait queue is initialized!");
    }
  #line 19
    return;
  }
  }
  #line 1 "preproc_hPNJHm.o"
  #pragma merger(0,"preproc_hPNJHm.i","-x,c")
  #line 47 "./include/linux/workqueue.h"
  __inline int schedule_work(struct work_struct *work ) ;
  #line 23 "./kernel/workqueue.c"
  __inline int schedule_work(struct work_struct *work ) 
  { int i ;
    unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    int __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    struct work_struct *__cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    void *__cil_tmp11 ;
    unsigned long __cil_tmp12 ;
    unsigned long __cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    struct work_struct *__cil_tmp15 ;
    unsigned long __cil_tmp16 ;
    unsigned long __cil_tmp17 ;
    unsigned long __cil_tmp18 ;
  
    {
    {
  #line 29
    __cil_tmp3 = (unsigned long )work;
  #line 29
    __cil_tmp4 = __cil_tmp3 + 24;
  #line 29
    __cil_tmp5 = *((int *)__cil_tmp4);
  #line 29
    __CPROVER_assert(__cil_tmp5, "Work queue is initalized");
  #line 32
    i = 0;
    }
    {
  #line 32
    while (1) {
      while_continue: /* CIL Label */ ;
  #line 32
      if (i < 10) {
  
      } else {
  #line 32
        goto while_break;
      }
      {
  #line 33
      __cil_tmp6 = (unsigned long )work;
  #line 33
      __cil_tmp7 = i * 8UL;
  #line 33
      __cil_tmp8 = (unsigned long )(shared_workqueue) + __cil_tmp7;
  #line 33
      __cil_tmp9 = *((struct work_struct **)__cil_tmp8);
  #line 33
      __cil_tmp10 = (unsigned long )__cil_tmp9;
  #line 33
      if (__cil_tmp10 == __cil_tmp6) {
  #line 34
        return (0);
      } else {
  
      }
      }
      {
  #line 37
      __cil_tmp11 = (void *)0;
  #line 37
      __cil_tmp12 = (unsigned long )__cil_tmp11;
  #line 37
      __cil_tmp13 = i * 8UL;
  #line 37
      __cil_tmp14 = (unsigned long )(shared_workqueue) + __cil_tmp13;
  #line 37
      __cil_tmp15 = *((struct work_struct **)__cil_tmp14);
  #line 37
      __cil_tmp16 = (unsigned long )__cil_tmp15;
  #line 37
      if (__cil_tmp16 == __cil_tmp12) {
  #line 38
        __cil_tmp17 = i * 8UL;
  #line 38
        __cil_tmp18 = (unsigned long )(shared_workqueue) + __cil_tmp17;
  #line 38
        *((struct work_struct **)__cil_tmp18) = work;
  #line 40
        return (1);
      } else {
  
      }
      }
  #line 32
      i = i + 1;
    }
    while_break: /* CIL Label */ ;
    }
  #line 45
    return (-1);
  }
  }
  #line 48 "./kernel/workqueue.c"
  void call_shared_workqueue_functions(void) 
  { unsigned short i ;
    unsigned short tmp ;
    int __cil_tmp3 ;
    int __cil_tmp4 ;
    void *__cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    struct work_struct *__cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    unsigned long __cil_tmp11 ;
    unsigned long __cil_tmp12 ;
    struct work_struct *__cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    unsigned long __cil_tmp15 ;
    void (*__cil_tmp16)(void * ) ;
    unsigned long __cil_tmp17 ;
    unsigned long __cil_tmp18 ;
    struct work_struct *__cil_tmp19 ;
    unsigned long __cil_tmp20 ;
    unsigned long __cil_tmp21 ;
    void *__cil_tmp22 ;
    unsigned long __cil_tmp23 ;
    unsigned long __cil_tmp24 ;
    void *__cil_tmp25 ;
  
    {
    {
  #line 50
    tmp = __VERIFIER_nondet_ushort();
  #line 50
    i = tmp;
  #line 51
    __cil_tmp3 = (int )i;
  #line 51
    __cil_tmp4 = __cil_tmp3 < 10;
  #line 51
    __CPROVER_assume(__cil_tmp4);
    }
    {
  #line 53
    __cil_tmp5 = (void *)0;
  #line 53
    __cil_tmp6 = (unsigned long )__cil_tmp5;
  #line 53
    __cil_tmp7 = i * 8UL;
  #line 53
    __cil_tmp8 = (unsigned long )(shared_workqueue) + __cil_tmp7;
  #line 53
    __cil_tmp9 = *((struct work_struct **)__cil_tmp8);
  #line 53
    __cil_tmp10 = (unsigned long )__cil_tmp9;
  #line 53
    if (__cil_tmp10 != __cil_tmp6) {
      {
  #line 54
      __cil_tmp11 = i * 8UL;
  #line 54
      __cil_tmp12 = (unsigned long )(shared_workqueue) + __cil_tmp11;
  #line 54
      __cil_tmp13 = *((struct work_struct **)__cil_tmp12);
  #line 54
      __cil_tmp14 = (unsigned long )__cil_tmp13;
  #line 54
      __cil_tmp15 = __cil_tmp14 + 8;
  #line 54
      __cil_tmp16 = *((void (**)(void * ))__cil_tmp15);
  #line 54
      __cil_tmp17 = i * 8UL;
  #line 54
      __cil_tmp18 = (unsigned long )(shared_workqueue) + __cil_tmp17;
  #line 54
      __cil_tmp19 = *((struct work_struct **)__cil_tmp18);
  #line 54
      __cil_tmp20 = (unsigned long )__cil_tmp19;
  #line 54
      __cil_tmp21 = __cil_tmp20 + 16;
  #line 54
      __cil_tmp22 = *((void **)__cil_tmp21);
  #line 54
      (*__cil_tmp16)(__cil_tmp22);
  #line 55
      __cil_tmp23 = i * 8UL;
  #line 55
      __cil_tmp24 = (unsigned long )(shared_workqueue) + __cil_tmp23;
  #line 55
      __cil_tmp25 = (void *)0;
  #line 55
      *((struct work_struct **)__cil_tmp24) = (struct work_struct *)__cil_tmp25;
      }
    } else {
  
    }
    }
  #line 57
    return;
  }
  }
  #line 1 "preproc_kSJxWg.o"
  #pragma merger(0,"preproc_kSJxWg.i","-x,c")
  #line 75 "./include/linux/interrupt.h"
  int request_irq(unsigned int irq , irqreturn_t (*handler)(int  , void * , struct pt_regs * ) ,
                  unsigned long irqflags , char const   *devname , void *dev_id ) ;
  #line 78
  void free_irq(unsigned int irq , void *dev_id ) ;
  #line 27 "./kernel/irq/manage.c"
  void free_irq(unsigned int irq , void *dev_id ) 
  { unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    void *__cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
  
    {
  #line 29
    __cil_tmp3 = irq * 16UL;
  #line 29
    __cil_tmp4 = (unsigned long )(registered_irq) + __cil_tmp3;
  #line 29
    __cil_tmp5 = (void *)0;
  #line 29
    *((irqreturn_t (**)(int  , void * , struct pt_regs * ))__cil_tmp4) = (irqreturn_t (*)(int  ,
                                                                                          void * ,
                                                                                          struct pt_regs * ))__cil_tmp5;
  #line 30
    __cil_tmp6 = irq * 16UL;
  #line 30
    __cil_tmp7 = __cil_tmp6 + 8;
  #line 30
    __cil_tmp8 = (unsigned long )(registered_irq) + __cil_tmp7;
  #line 30
    *((void **)__cil_tmp8) = (void *)0;
  #line 31
    return;
  }
  }
  #line 62 "./kernel/irq/manage.c"
  int request_irq(unsigned int irq , irqreturn_t (*handler)(int  , void * , struct pt_regs * ) ,
                  unsigned long irqflags , char const   *devname , void *dev_id ) 
  { int tmp ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    unsigned long __cil_tmp11 ;
  
    {
    {
  #line 65
    tmp = __VERIFIER_nondet_int();
    }
  #line 65
    if (tmp) {
  #line 66
      __cil_tmp7 = irq * 16UL;
  #line 66
      __cil_tmp8 = (unsigned long )(registered_irq) + __cil_tmp7;
  #line 66
      *((irqreturn_t (**)(int  , void * , struct pt_regs * ))__cil_tmp8) = handler;
  #line 67
      __cil_tmp9 = irq * 16UL;
  #line 67
      __cil_tmp10 = __cil_tmp9 + 8;
  #line 67
      __cil_tmp11 = (unsigned long )(registered_irq) + __cil_tmp10;
  #line 67
      *((void **)__cil_tmp11) = dev_id;
  #line 69
      return (0);
    } else {
  #line 71
      return (-1);
    }
  }
  }
  #line 1 "preproc_sYmZsa.o"
  #pragma merger(0,"preproc_sYmZsa.i","-x,c")
  #line 55 "./include/linux/gfp.h"
  unsigned long __get_free_pages(gfp_t gfp_mask , unsigned int order ) ;
  #line 57
  __inline unsigned long __get_free_page(gfp_t gfp_mask ) ;
  #line 59
  unsigned long get_zeroed_page(gfp_t gfp_mask ) ;
  #line 70
  struct page *alloc_pages(gfp_t gfp_mask , unsigned int order ) ;
  #line 72
  __inline struct page *alloc_page(gfp_t gfp_mask ) ;
  #line 22 "./mm/page_alloc.c"
  unsigned long get_zeroed_page(gfp_t gfp_mask ) 
  { 
  
    {
  #line 25
    if (gfp_mask & 16U) {
      {
  #line 26
      assert_context_process();
      }
    } else {
  
    }
  #line 28
    return (0UL);
  }
  }
  #line 42 "./mm/page_alloc.c"
  struct page *alloc_pages(gfp_t gfp_mask , unsigned int order ) 
  { 
  
    {
  #line 46
    if (gfp_mask & 16U) {
      {
  #line 47
      assert_context_process();
      }
    } else {
  
    }
  #line 49
    return ((struct page *)0);
  }
  }
  #line 51 "./mm/page_alloc.c"
  __inline struct page *alloc_page(gfp_t gfp_mask ) 
  { 
  
    {
  #line 54
    if (gfp_mask & 16U) {
      {
  #line 55
      assert_context_process();
      }
    } else {
  
    }
  #line 57
    return ((struct page *)0);
  }
  }
  #line 62 "./mm/page_alloc.c"
  unsigned long __get_free_pages(gfp_t gfp_mask , unsigned int order ) 
  { 
  
    {
  #line 65
    if (gfp_mask & 16U) {
      {
  #line 66
      assert_context_process();
      }
    } else {
  
    }
  #line 68
    return (0UL);
  }
  }
  #line 70 "./mm/page_alloc.c"
  __inline unsigned long __get_free_page(gfp_t gfp_mask ) 
  { 
  
    {
  #line 73
    if (gfp_mask & 16U) {
      {
  #line 74
      assert_context_process();
      }
    } else {
  
    }
  #line 76
    return (0UL);
  }
  }
  #line 1 "preproc_8318HF.o"
  #pragma merger(0,"preproc_8318HF.i","-x,c")
  #line 27 "./include/linux/slab.h"
  void *kmalloc(size_t size , gfp_t flags ) ;
  #line 29
  void *kzalloc(size_t size , gfp_t flags ) ;
  #line 95 "./mm/slab.c"
  void *kmalloc(size_t size , gfp_t flags ) 
  { void *tmp ;
  
    {
  #line 97
    if (flags & 16U) {
      {
  #line 98
      assert_context_process();
      }
    } else {
  
    }
    {
  #line 101
    tmp = malloc(size);
    }
  #line 101
    return (tmp);
  }
  }
  #line 104 "./mm/slab.c"
  void *kzalloc(size_t size , gfp_t flags ) 
  { void *tmp ;
  
    {
  #line 106
    if (flags & 16U) {
      {
  #line 107
      assert_context_process();
      }
    } else {
  
    }
    {
  #line 110
    tmp = malloc(size);
    }
  #line 110
    return (tmp);
  }
  }
  #line 1 "preproc_hdcSZC.o"
  #pragma merger(0,"preproc_hdcSZC.i","-x,c")
  #line 9 "./include/linux/vmalloc.h"
  void *vmalloc(unsigned long size ) ;
  #line 24 "./mm/vmalloc.c"
  void *vmalloc(unsigned long size ) 
  { void *tmp ;
    size_t __cil_tmp3 ;
  
    {
    {
  #line 26
    __cil_tmp3 = (size_t )size;
  #line 26
    tmp = malloc(__cil_tmp3);
    }
  #line 26
    return (tmp);
  }
  }
  #line 1 "preproc_L6KO8D.o"
  #pragma merger(0,"preproc_L6KO8D.i","-x,c")
  #line 28 "./include/linux/module.h"
  extern struct module __this_module ;
  #line 40 "./include/linux/miscdevice.h"
  int misc_register(struct miscdevice *misc ) ;
  #line 67 "./drivers/char/misc.c"
  int misc_register(struct miscdevice *misc ) 
  { int i ;
    dev_t dev ;
    int tmp ;
    unsigned long __cil_tmp5 ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    unsigned long __cil_tmp10 ;
    unsigned long __cil_tmp11 ;
    int __cil_tmp12 ;
    int __cil_tmp13 ;
    int __cil_tmp14 ;
    unsigned long __cil_tmp15 ;
    unsigned long __cil_tmp16 ;
    struct cdev *__cil_tmp17 ;
  
    {
  #line 72
    if (fixed_cdev_used < 10) {
      {
  #line 73
      i = fixed_cdev_used;
  #line 74
      fixed_cdev_used = fixed_cdev_used + 1;
  #line 76
      __cil_tmp5 = i * 24UL;
  #line 76
      __cil_tmp6 = (unsigned long )(fixed_cdev) + __cil_tmp5;
  #line 76
      *((struct module **)__cil_tmp6) = & __this_module;
  #line 77
      __cil_tmp7 = i * 24UL;
  #line 77
      __cil_tmp8 = __cil_tmp7 + 8;
  #line 77
      __cil_tmp9 = (unsigned long )(fixed_cdev) + __cil_tmp8;
  #line 77
      __cil_tmp10 = (unsigned long )misc;
  #line 77
      __cil_tmp11 = __cil_tmp10 + 16;
  #line 77
      *((struct file_operations  const  **)__cil_tmp9) = *((struct file_operations  const  **)__cil_tmp11);
  #line 79
      __cil_tmp12 = *((int *)misc);
  #line 79
      __cil_tmp13 = 10 << 20;
  #line 79
      __cil_tmp14 = __cil_tmp13 | __cil_tmp12;
  #line 79
      dev = (dev_t )__cil_tmp14;
  #line 81
      __cil_tmp15 = i * 24UL;
  #line 81
      __cil_tmp16 = (unsigned long )(fixed_cdev) + __cil_tmp15;
  #line 81
      __cil_tmp17 = (struct cdev *)__cil_tmp16;
  #line 81
      tmp = cdev_add(__cil_tmp17, dev, 0U);
      }
  #line 81
      return (tmp);
    } else {
  #line 83
      return (-1);
    }
  }
  }
  #line 1 "preproc_BompK0.o"
  #pragma merger(0,"preproc_BompK0.i","-x,c")
  #line 209 "./include/linux/tty_driver.h"
  struct tty_driver *alloc_tty_driver(int lines ) ;
  #line 213
  void tty_set_operations(struct tty_driver *driver , struct tty_operations  const  *op ) ;
  #line 13 "cprover/ddverify/include/ddverify/tty.h"
  struct ddv_tty_driver global_tty_driver  ;
  #line 4 "./drivers/char/tty_io.c"
  struct tty_driver *alloc_tty_driver(int lines ) 
  { void *__cil_tmp2 ;
  
    {
  #line 6
    if (! global_tty_driver.allocated) {
  #line 7
      global_tty_driver.driver.magic = 21506;
  #line 8
      global_tty_driver.driver.num = lines;
    } else {
      {
  #line 10
      __cil_tmp2 = (void *)0;
  #line 10
      return ((struct tty_driver *)__cil_tmp2);
      }
    }
  #line 12
    return ((struct tty_driver *)0);
  }
  }
  #line 14 "./drivers/char/tty_io.c"
  void tty_set_operations(struct tty_driver *driver , struct tty_operations  const  *op ) 
  { unsigned long __cil_tmp3 ;
    unsigned long __cil_tmp4 ;
    int (*__cil_tmp5)(struct tty_struct *tty , struct file *filp ) ;
    unsigned long __cil_tmp6 ;
    unsigned long __cil_tmp7 ;
    unsigned long __cil_tmp8 ;
    unsigned long __cil_tmp9 ;
    void (*__cil_tmp10)(struct tty_struct *tty , struct file *filp ) ;
    unsigned long __cil_tmp11 ;
    unsigned long __cil_tmp12 ;
    unsigned long __cil_tmp13 ;
    unsigned long __cil_tmp14 ;
    int (*__cil_tmp15)(struct tty_struct *tty , unsigned char const   *buf , int count ) ;
    unsigned long __cil_tmp16 ;
    unsigned long __cil_tmp17 ;
    unsigned long __cil_tmp18 ;
    unsigned long __cil_tmp19 ;
    void (*__cil_tmp20)(struct tty_struct *tty , unsigned char ch ) ;
    unsigned long __cil_tmp21 ;
    unsigned long __cil_tmp22 ;
    unsigned long __cil_tmp23 ;
    unsigned long __cil_tmp24 ;
    void (*__cil_tmp25)(struct tty_struct *tty ) ;
    unsigned long __cil_tmp26 ;
    unsigned long __cil_tmp27 ;
    unsigned long __cil_tmp28 ;
    unsigned long __cil_tmp29 ;
    int (*__cil_tmp30)(struct tty_struct *tty ) ;
    unsigned long __cil_tmp31 ;
    unsigned long __cil_tmp32 ;
    unsigned long __cil_tmp33 ;
    unsigned long __cil_tmp34 ;
    int (*__cil_tmp35)(struct tty_struct *tty ) ;
    unsigned long __cil_tmp36 ;
    unsigned long __cil_tmp37 ;
    unsigned long __cil_tmp38 ;
    unsigned long __cil_tmp39 ;
    int (*__cil_tmp40)(struct tty_struct *tty , struct file *file , unsigned int cmd ,
                       unsigned long arg ) ;
    unsigned long __cil_tmp41 ;
    unsigned long __cil_tmp42 ;
    unsigned long __cil_tmp43 ;
    unsigned long __cil_tmp44 ;
    void (*__cil_tmp45)(struct tty_struct *tty , struct termios *old ) ;
    unsigned long __cil_tmp46 ;
    unsigned long __cil_tmp47 ;
    unsigned long __cil_tmp48 ;
    unsigned long __cil_tmp49 ;
    void (*__cil_tmp50)(struct tty_struct *tty ) ;
    unsigned long __cil_tmp51 ;
    unsigned long __cil_tmp52 ;
    unsigned long __cil_tmp53 ;
    unsigned long __cil_tmp54 ;
    void (*__cil_tmp55)(struct tty_struct *tty ) ;
    unsigned long __cil_tmp56 ;
    unsigned long __cil_tmp57 ;
    unsigned long __cil_tmp58 ;
    unsigned long __cil_tmp59 ;
    void (*__cil_tmp60)(struct tty_struct *tty ) ;
    unsigned long __cil_tmp61 ;
    unsigned long __cil_tmp62 ;
    unsigned long __cil_tmp63 ;
    unsigned long __cil_tmp64 ;
    void (*__cil_tmp65)(struct tty_struct *tty ) ;
    unsigned long __cil_tmp66 ;
    unsigned long __cil_tmp67 ;
    unsigned long __cil_tmp68 ;
    unsigned long __cil_tmp69 ;
    void (*__cil_tmp70)(struct tty_struct *tty ) ;
    unsigned long __cil_tmp71 ;
    unsigned long __cil_tmp72 ;
    unsigned long __cil_tmp73 ;
    unsigned long __cil_tmp74 ;
    void (*__cil_tmp75)(struct tty_struct *tty , int state ) ;
    unsigned long __cil_tmp76 ;
    unsigned long __cil_tmp77 ;
    unsigned long __cil_tmp78 ;
    unsigned long __cil_tmp79 ;
    void (*__cil_tmp80)(struct tty_struct *tty ) ;
    unsigned long __cil_tmp81 ;
    unsigned long __cil_tmp82 ;
    unsigned long __cil_tmp83 ;
    unsigned long __cil_tmp84 ;
    void (*__cil_tmp85)(struct tty_struct *tty ) ;
    unsigned long __cil_tmp86 ;
    unsigned long __cil_tmp87 ;
    unsigned long __cil_tmp88 ;
    unsigned long __cil_tmp89 ;
    void (*__cil_tmp90)(struct tty_struct *tty , int timeout ) ;
    unsigned long __cil_tmp91 ;
    unsigned long __cil_tmp92 ;
    unsigned long __cil_tmp93 ;
    unsigned long __cil_tmp94 ;
    void (*__cil_tmp95)(struct tty_struct *tty , char ch ) ;
    unsigned long __cil_tmp96 ;
    unsigned long __cil_tmp97 ;
    unsigned long __cil_tmp98 ;
    unsigned long __cil_tmp99 ;
    int (*__cil_tmp100)(char *page , char **start , off_t off , int count , int *eof ,
                        void *data ) ;
    unsigned long __cil_tmp101 ;
    unsigned long __cil_tmp102 ;
    unsigned long __cil_tmp103 ;
    unsigned long __cil_tmp104 ;
    int (*__cil_tmp105)(struct file *file , char const   *buffer , unsigned long count ,
                        void *data ) ;
    unsigned long __cil_tmp106 ;
    unsigned long __cil_tmp107 ;
    unsigned long __cil_tmp108 ;
    unsigned long __cil_tmp109 ;
    int (*__cil_tmp110)(struct tty_struct *tty , struct file *file ) ;
    unsigned long __cil_tmp111 ;
    unsigned long __cil_tmp112 ;
    unsigned long __cil_tmp113 ;
    unsigned long __cil_tmp114 ;
    int (*__cil_tmp115)(struct tty_struct *tty , struct file *file , unsigned int set ,
                        unsigned int clear ) ;
  
    {
  #line 17
    __cil_tmp3 = (unsigned long )driver;
  #line 17
    __cil_tmp4 = __cil_tmp3 + 136;
  #line 17
    __cil_tmp5 = *((int (* const  *)(struct tty_struct *tty , struct file *filp ))op);
  #line 17
    *((int (**)(struct tty_struct *tty , struct file *filp ))__cil_tmp4) = (int (*)(struct tty_struct *tty ,
                                                                                    struct file *filp ))__cil_tmp5;
  #line 18
    __cil_tmp6 = (unsigned long )driver;
  #line 18
    __cil_tmp7 = __cil_tmp6 + 144;
  #line 18
    __cil_tmp8 = (unsigned long )op;
  #line 18
    __cil_tmp9 = __cil_tmp8 + 8;
  #line 18
    __cil_tmp10 = *((void (* const  *)(struct tty_struct *tty , struct file *filp ))__cil_tmp9);
  #line 18
    *((void (**)(struct tty_struct *tty , struct file *filp ))__cil_tmp7) = (void (*)(struct tty_struct *tty ,
                                                                                      struct file *filp ))__cil_tmp10;
  #line 19
    __cil_tmp11 = (unsigned long )driver;
  #line 19
    __cil_tmp12 = __cil_tmp11 + 152;
  #line 19
    __cil_tmp13 = (unsigned long )op;
  #line 19
    __cil_tmp14 = __cil_tmp13 + 16;
  #line 19
    __cil_tmp15 = *((int (* const  *)(struct tty_struct *tty , unsigned char const   *buf ,
                                      int count ))__cil_tmp14);
  #line 19
    *((int (**)(struct tty_struct *tty , unsigned char const   *buf , int count ))__cil_tmp12) = (int (*)(struct tty_struct *tty ,
                                                                                                          unsigned char const   *buf ,
                                                                                                          int count ))__cil_tmp15;
  #line 20
    __cil_tmp16 = (unsigned long )driver;
  #line 20
    __cil_tmp17 = __cil_tmp16 + 160;
  #line 20
    __cil_tmp18 = (unsigned long )op;
  #line 20
    __cil_tmp19 = __cil_tmp18 + 24;
  #line 20
    __cil_tmp20 = *((void (* const  *)(struct tty_struct *tty , unsigned char ch ))__cil_tmp19);
  #line 20
    *((void (**)(struct tty_struct *tty , unsigned char ch ))__cil_tmp17) = (void (*)(struct tty_struct *tty ,
                                                                                      unsigned char ch ))__cil_tmp20;
  #line 21
    __cil_tmp21 = (unsigned long )driver;
  #line 21
    __cil_tmp22 = __cil_tmp21 + 168;
  #line 21
    __cil_tmp23 = (unsigned long )op;
  #line 21
    __cil_tmp24 = __cil_tmp23 + 32;
  #line 21
    __cil_tmp25 = *((void (* const  *)(struct tty_struct *tty ))__cil_tmp24);
  #line 21
    *((void (**)(struct tty_struct *tty ))__cil_tmp22) = (void (*)(struct tty_struct *tty ))__cil_tmp25;
  #line 22
    __cil_tmp26 = (unsigned long )driver;
  #line 22
    __cil_tmp27 = __cil_tmp26 + 176;
  #line 22
    __cil_tmp28 = (unsigned long )op;
  #line 22
    __cil_tmp29 = __cil_tmp28 + 40;
  #line 22
    __cil_tmp30 = *((int (* const  *)(struct tty_struct *tty ))__cil_tmp29);
  #line 22
    *((int (**)(struct tty_struct *tty ))__cil_tmp27) = (int (*)(struct tty_struct *tty ))__cil_tmp30;
  #line 23
    __cil_tmp31 = (unsigned long )driver;
  #line 23
    __cil_tmp32 = __cil_tmp31 + 184;
  #line 23
    __cil_tmp33 = (unsigned long )op;
  #line 23
    __cil_tmp34 = __cil_tmp33 + 48;
  #line 23
    __cil_tmp35 = *((int (* const  *)(struct tty_struct *tty ))__cil_tmp34);
  #line 23
    *((int (**)(struct tty_struct *tty ))__cil_tmp32) = (int (*)(struct tty_struct *tty ))__cil_tmp35;
  #line 24
    __cil_tmp36 = (unsigned long )driver;
  #line 24
    __cil_tmp37 = __cil_tmp36 + 192;
  #line 24
    __cil_tmp38 = (unsigned long )op;
  #line 24
    __cil_tmp39 = __cil_tmp38 + 56;
  #line 24
    __cil_tmp40 = *((int (* const  *)(struct tty_struct *tty , struct file *file , unsigned int cmd ,
                                      unsigned long arg ))__cil_tmp39);
  #line 24
    *((int (**)(struct tty_struct *tty , struct file *file , unsigned int cmd , unsigned long arg ))__cil_tmp37) = (int (*)(struct tty_struct *tty ,
                                                                                                                            struct file *file ,
                                                                                                                            unsigned int cmd ,
                                                                                                                            unsigned long arg ))__cil_tmp40;
  #line 25
    __cil_tmp41 = (unsigned long )driver;
  #line 25
    __cil_tmp42 = __cil_tmp41 + 200;
  #line 25
    __cil_tmp43 = (unsigned long )op;
  #line 25
    __cil_tmp44 = __cil_tmp43 + 64;
  #line 25
    __cil_tmp45 = *((void (* const  *)(struct tty_struct *tty , struct termios *old ))__cil_tmp44);
  #line 25
    *((void (**)(struct tty_struct *tty , struct termios *old ))__cil_tmp42) = (void (*)(struct tty_struct *tty ,
                                                                                         struct termios *old ))__cil_tmp45;
  #line 26
    __cil_tmp46 = (unsigned long )driver;
  #line 26
    __cil_tmp47 = __cil_tmp46 + 208;
  #line 26
    __cil_tmp48 = (unsigned long )op;
  #line 26
    __cil_tmp49 = __cil_tmp48 + 72;
  #line 26
    __cil_tmp50 = *((void (* const  *)(struct tty_struct *tty ))__cil_tmp49);
  #line 26
    *((void (**)(struct tty_struct *tty ))__cil_tmp47) = (void (*)(struct tty_struct *tty ))__cil_tmp50;
  #line 27
    __cil_tmp51 = (unsigned long )driver;
  #line 27
    __cil_tmp52 = __cil_tmp51 + 216;
  #line 27
    __cil_tmp53 = (unsigned long )op;
  #line 27
    __cil_tmp54 = __cil_tmp53 + 80;
  #line 27
    __cil_tmp55 = *((void (* const  *)(struct tty_struct *tty ))__cil_tmp54);
  #line 27
    *((void (**)(struct tty_struct *tty ))__cil_tmp52) = (void (*)(struct tty_struct *tty ))__cil_tmp55;
  #line 28
    __cil_tmp56 = (unsigned long )driver;
  #line 28
    __cil_tmp57 = __cil_tmp56 + 224;
  #line 28
    __cil_tmp58 = (unsigned long )op;
  #line 28
    __cil_tmp59 = __cil_tmp58 + 88;
  #line 28
    __cil_tmp60 = *((void (* const  *)(struct tty_struct *tty ))__cil_tmp59);
  #line 28
    *((void (**)(struct tty_struct *tty ))__cil_tmp57) = (void (*)(struct tty_struct *tty ))__cil_tmp60;
  #line 29
    __cil_tmp61 = (unsigned long )driver;
  #line 29
    __cil_tmp62 = __cil_tmp61 + 232;
  #line 29
    __cil_tmp63 = (unsigned long )op;
  #line 29
    __cil_tmp64 = __cil_tmp63 + 96;
  #line 29
    __cil_tmp65 = *((void (* const  *)(struct tty_struct *tty ))__cil_tmp64);
  #line 29
    *((void (**)(struct tty_struct *tty ))__cil_tmp62) = (void (*)(struct tty_struct *tty ))__cil_tmp65;
  #line 30
    __cil_tmp66 = (unsigned long )driver;
  #line 30
    __cil_tmp67 = __cil_tmp66 + 240;
  #line 30
    __cil_tmp68 = (unsigned long )op;
  #line 30
    __cil_tmp69 = __cil_tmp68 + 104;
  #line 30
    __cil_tmp70 = *((void (* const  *)(struct tty_struct *tty ))__cil_tmp69);
  #line 30
    *((void (**)(struct tty_struct *tty ))__cil_tmp67) = (void (*)(struct tty_struct *tty ))__cil_tmp70;
  #line 31
    __cil_tmp71 = (unsigned long )driver;
  #line 31
    __cil_tmp72 = __cil_tmp71 + 248;
  #line 31
    __cil_tmp73 = (unsigned long )op;
  #line 31
    __cil_tmp74 = __cil_tmp73 + 112;
  #line 31
    __cil_tmp75 = *((void (* const  *)(struct tty_struct *tty , int state ))__cil_tmp74);
  #line 31
    *((void (**)(struct tty_struct *tty , int state ))__cil_tmp72) = (void (*)(struct tty_struct *tty ,
                                                                               int state ))__cil_tmp75;
  #line 32
    __cil_tmp76 = (unsigned long )driver;
  #line 32
    __cil_tmp77 = __cil_tmp76 + 256;
  #line 32
    __cil_tmp78 = (unsigned long )op;
  #line 32
    __cil_tmp79 = __cil_tmp78 + 120;
  #line 32
    __cil_tmp80 = *((void (* const  *)(struct tty_struct *tty ))__cil_tmp79);
  #line 32
    *((void (**)(struct tty_struct *tty ))__cil_tmp77) = (void (*)(struct tty_struct *tty ))__cil_tmp80;
  #line 33
    __cil_tmp81 = (unsigned long )driver;
  #line 33
    __cil_tmp82 = __cil_tmp81 + 264;
  #line 33
    __cil_tmp83 = (unsigned long )op;
  #line 33
    __cil_tmp84 = __cil_tmp83 + 128;
  #line 33
    __cil_tmp85 = *((void (* const  *)(struct tty_struct *tty ))__cil_tmp84);
  #line 33
    *((void (**)(struct tty_struct *tty ))__cil_tmp82) = (void (*)(struct tty_struct *tty ))__cil_tmp85;
  #line 34
    __cil_tmp86 = (unsigned long )driver;
  #line 34
    __cil_tmp87 = __cil_tmp86 + 272;
  #line 34
    __cil_tmp88 = (unsigned long )op;
  #line 34
    __cil_tmp89 = __cil_tmp88 + 136;
  #line 34
    __cil_tmp90 = *((void (* const  *)(struct tty_struct *tty , int timeout ))__cil_tmp89);
  #line 34
    *((void (**)(struct tty_struct *tty , int timeout ))__cil_tmp87) = (void (*)(struct tty_struct *tty ,
                                                                                 int timeout ))__cil_tmp90;
  #line 35
    __cil_tmp91 = (unsigned long )driver;
  #line 35
    __cil_tmp92 = __cil_tmp91 + 280;
  #line 35
    __cil_tmp93 = (unsigned long )op;
  #line 35
    __cil_tmp94 = __cil_tmp93 + 144;
  #line 35
    __cil_tmp95 = *((void (* const  *)(struct tty_struct *tty , char ch ))__cil_tmp94);
  #line 35
    *((void (**)(struct tty_struct *tty , char ch ))__cil_tmp92) = (void (*)(struct tty_struct *tty ,
                                                                             char ch ))__cil_tmp95;
  #line 36
    __cil_tmp96 = (unsigned long )driver;
  #line 36
    __cil_tmp97 = __cil_tmp96 + 288;
  #line 36
    __cil_tmp98 = (unsigned long )op;
  #line 36
    __cil_tmp99 = __cil_tmp98 + 152;
  #line 36
    __cil_tmp100 = *((int (* const  *)(char *page , char **start , off_t off , int count ,
                                       int *eof , void *data ))__cil_tmp99);
  #line 36
    *((int (**)(char *page , char **start , off_t off , int count , int *eof , void *data ))__cil_tmp97) = (int (*)(char *page ,
                                                                                                                    char **start ,
                                                                                                                    off_t off ,
                                                                                                                    int count ,
                                                                                                                    int *eof ,
                                                                                                                    void *data ))__cil_tmp100;
  #line 37
    __cil_tmp101 = (unsigned long )driver;
  #line 37
    __cil_tmp102 = __cil_tmp101 + 296;
  #line 37
    __cil_tmp103 = (unsigned long )op;
  #line 37
    __cil_tmp104 = __cil_tmp103 + 160;
  #line 37
    __cil_tmp105 = *((int (* const  *)(struct file *file , char const   *buffer , unsigned long count ,
                                       void *data ))__cil_tmp104);
  #line 37
    *((int (**)(struct file *file , char const   *buffer , unsigned long count , void *data ))__cil_tmp102) = (int (*)(struct file *file ,
                                                                                                                       char const   *buffer ,
                                                                                                                       unsigned long count ,
                                                                                                                       void *data ))__cil_tmp105;
  #line 38
    __cil_tmp106 = (unsigned long )driver;
  #line 38
    __cil_tmp107 = __cil_tmp106 + 304;
  #line 38
    __cil_tmp108 = (unsigned long )op;
  #line 38
    __cil_tmp109 = __cil_tmp108 + 168;
  #line 38
    __cil_tmp110 = *((int (* const  *)(struct tty_struct *tty , struct file *file ))__cil_tmp109);
  #line 38
    *((int (**)(struct tty_struct *tty , struct file *file ))__cil_tmp107) = (int (*)(struct tty_struct *tty ,
                                                                                      struct file *file ))__cil_tmp110;
  #line 39
    __cil_tmp111 = (unsigned long )driver;
  #line 39
    __cil_tmp112 = __cil_tmp111 + 312;
  #line 39
    __cil_tmp113 = (unsigned long )op;
  #line 39
    __cil_tmp114 = __cil_tmp113 + 176;
  #line 39
    __cil_tmp115 = *((int (* const  *)(struct tty_struct *tty , struct file *file ,
                                       unsigned int set , unsigned int clear ))__cil_tmp114);
  #line 39
    *((int (**)(struct tty_struct *tty , struct file *file , unsigned int set , unsigned int clear ))__cil_tmp112) = (int (*)(struct tty_struct *tty ,
                                                                                                                              struct file *file ,
                                                                                                                              unsigned int set ,
                                                                                                                              unsigned int clear ))__cil_tmp115;
  #line 40
    return;
  }
  }
  