ClabureDB: Classified Bug-Reports Database

   /* Generated by CIL v. 1.3.7 */
   /* print_CIL_Input is true */
   
   #line 23 "include/asm-generic/int-ll64.h"
   typedef unsigned short __u16;
   #line 26 "include/asm-generic/int-ll64.h"
   typedef unsigned int __u32;
   #line 30 "include/asm-generic/int-ll64.h"
   typedef unsigned long long __u64;
  #line 45 "include/asm-generic/int-ll64.h"
  typedef short s16;
  #line 46 "include/asm-generic/int-ll64.h"
  typedef unsigned short u16;
  #line 49 "include/asm-generic/int-ll64.h"
  typedef unsigned int u32;
  #line 14 "include/asm-generic/posix_types.h"
  typedef long __kernel_long_t;
  #line 15 "include/asm-generic/posix_types.h"
  typedef unsigned long __kernel_ulong_t;
  #line 75 "include/asm-generic/posix_types.h"
  typedef __kernel_ulong_t __kernel_size_t;
  #line 76 "include/asm-generic/posix_types.h"
  typedef __kernel_long_t __kernel_ssize_t;
  #line 27 "include/linux/types.h"
  typedef unsigned short umode_t;
  #line 63 "include/linux/types.h"
  typedef __kernel_size_t size_t;
  #line 68 "include/linux/types.h"
  typedef __kernel_ssize_t ssize_t;
  #line 219 "include/linux/types.h"
  struct __anonstruct_atomic_t_7 {
     int counter ;
  };
  #line 219 "include/linux/types.h"
  typedef struct __anonstruct_atomic_t_7 atomic_t;
  #line 229 "include/linux/types.h"
  struct list_head {
     struct list_head *next ;
     struct list_head *prev ;
  };
  #line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  struct module;
  #line 56
  struct module;
  #line 146 "include/linux/init.h"
  typedef void (*ctor_fn_t)(void);
  #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
  struct task_struct;
  #line 20
  struct task_struct;
  #line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  struct task_struct;
  #line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  struct task_struct;
  #line 329
  struct arch_spinlock;
  #line 329
  struct arch_spinlock;
  #line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
  struct task_struct;
  #line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
  struct task_struct;
  #line 10 "include/asm-generic/bug.h"
  struct bug_entry {
     int bug_addr_disp ;
     int file_disp ;
     unsigned short line ;
     unsigned short flags ;
  };
  #line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
  struct static_key;
  #line 234
  struct static_key;
  #line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  typedef u16 __ticket_t;
  #line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  typedef u32 __ticketpair_t;
  #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  struct __raw_tickets {
     __ticket_t head ;
     __ticket_t tail ;
  };
  #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  union __anonunion____missing_field_name_36 {
     __ticketpair_t head_tail ;
     struct __raw_tickets tickets ;
  };
  #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  struct arch_spinlock {
     union __anonunion____missing_field_name_36 __annonCompField17 ;
  };
  #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  typedef struct arch_spinlock arch_spinlock_t;
  #line 12 "include/linux/lockdep.h"
  struct task_struct;
  #line 20 "include/linux/spinlock_types.h"
  struct raw_spinlock {
     arch_spinlock_t raw_lock ;
     unsigned int magic ;
    unsigned int owner_cpu ;
    void *owner ;
 };
 #line 64 "include/linux/spinlock_types.h"
 union __anonunion____missing_field_name_39 {
    struct raw_spinlock rlock ;
 };
 #line 64 "include/linux/spinlock_types.h"
 struct spinlock {
    union __anonunion____missing_field_name_39 __annonCompField19 ;
 };
 #line 64 "include/linux/spinlock_types.h"
 typedef struct spinlock spinlock_t;
 #line 49 "include/linux/wait.h"
 struct __wait_queue_head {
    spinlock_t lock ;
    struct list_head task_list ;
 };
 #line 53 "include/linux/wait.h"
 typedef struct __wait_queue_head wait_queue_head_t;
 #line 55
 struct task_struct;
 #line 48 "include/linux/mutex.h"
 struct mutex {
    atomic_t count ;
    spinlock_t wait_lock ;
    struct list_head wait_list ;
    struct task_struct *owner ;
    char const   *name ;
    void *magic ;
 };
 #line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 struct task_struct;
 #line 18 "include/linux/elf.h"
 typedef __u64 Elf64_Addr;
 #line 19 "include/linux/elf.h"
 typedef __u16 Elf64_Half;
 #line 23 "include/linux/elf.h"
 typedef __u32 Elf64_Word;
 #line 24 "include/linux/elf.h"
 typedef __u64 Elf64_Xword;
 #line 194 "include/linux/elf.h"
 struct elf64_sym {
    Elf64_Word st_name ;
    unsigned char st_info ;
    unsigned char st_other ;
    Elf64_Half st_shndx ;
    Elf64_Addr st_value ;
    Elf64_Xword st_size ;
 };
 #line 194 "include/linux/elf.h"
 typedef struct elf64_sym Elf64_Sym;
 #line 20 "include/linux/kobject_ns.h"
 struct sock;
 #line 20
 struct sock;
 #line 21
 struct kobject;
 #line 21
 struct kobject;
 #line 27
 enum kobj_ns_type {
     KOBJ_NS_TYPE_NONE = 0,
     KOBJ_NS_TYPE_NET = 1,
     KOBJ_NS_TYPES = 2
 } ;
 #line 40 "include/linux/kobject_ns.h"
 struct kobj_ns_type_operations {
    enum kobj_ns_type type ;
    void *(*grab_current_ns)(void) ;
    void const   *(*netlink_ns)(struct sock *sk ) ;
    void const   *(*initial_ns)(void) ;
    void (*drop_ns)(void * ) ;
 };
 #line 22 "include/linux/sysfs.h"
 struct kobject;
 #line 23
 struct module;
 #line 24
 enum kobj_ns_type;
 #line 26 "include/linux/sysfs.h"
 struct attribute {
    char const   *name ;
    umode_t mode ;
 };
 #line 112 "include/linux/sysfs.h"
 struct sysfs_ops {
    ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
    ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
    void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 };
 #line 118
 struct sysfs_dirent;
 #line 118
 struct sysfs_dirent;
 #line 22 "include/linux/kref.h"
 struct kref {
    atomic_t refcount ;
 };
 #line 60 "include/linux/kobject.h"
 struct kset;
 #line 60
 struct kobj_type;
 #line 60 "include/linux/kobject.h"
 struct kobject {
    char const   *name ;
    struct list_head entry ;
    struct kobject *parent ;
    struct kset *kset ;
    struct kobj_type *ktype ;
    struct sysfs_dirent *sd ;
    struct kref kref ;
    unsigned int state_initialized : 1 ;
    unsigned int state_in_sysfs : 1 ;
    unsigned int state_add_uevent_sent : 1 ;
    unsigned int state_remove_uevent_sent : 1 ;
    unsigned int uevent_suppress : 1 ;
 };
 #line 108 "include/linux/kobject.h"
 struct kobj_type {
    void (*release)(struct kobject *kobj ) ;
    struct sysfs_ops  const  *sysfs_ops ;
    struct attribute **default_attrs ;
    struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
    void const   *(*namespace)(struct kobject *kobj ) ;
 };
 #line 116 "include/linux/kobject.h"
 struct kobj_uevent_env {
    char *envp[32] ;
    int envp_idx ;
    char buf[2048] ;
    int buflen ;
 };
 #line 123 "include/linux/kobject.h"
 struct kset_uevent_ops {
    int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
    char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
    int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 };
 #line 140
 struct sock;
 #line 159 "include/linux/kobject.h"
 struct kset {
    struct list_head list ;
    spinlock_t list_lock ;
    struct kobject kobj ;
    struct kset_uevent_ops  const  *uevent_ops ;
 };
 #line 39 "include/linux/moduleparam.h"
 struct kernel_param;
 #line 39
 struct kernel_param;
 #line 41 "include/linux/moduleparam.h"
 struct kernel_param_ops {
    int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
    int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
    void (*free)(void *arg ) ;
 };
 #line 50
 struct kparam_string;
 #line 50
 struct kparam_array;
 #line 50 "include/linux/moduleparam.h"
 union __anonunion____missing_field_name_199 {
    void *arg ;
    struct kparam_string  const  *str ;
    struct kparam_array  const  *arr ;
 };
 #line 50 "include/linux/moduleparam.h"
 struct kernel_param {
    char const   *name ;
    struct kernel_param_ops  const  *ops ;
    u16 perm ;
    s16 level ;
    union __anonunion____missing_field_name_199 __annonCompField32 ;
 };
 #line 63 "include/linux/moduleparam.h"
 struct kparam_string {
    unsigned int maxlen ;
    char *string ;
 };
 #line 69 "include/linux/moduleparam.h"
 struct kparam_array {
    unsigned int max ;
    unsigned int elemsize ;
    unsigned int *num ;
    struct kernel_param_ops  const  *ops ;
    void *elem ;
 };
 #line 445
 struct module;
 #line 80 "include/linux/jump_label.h"
 struct module;
 #line 143 "include/linux/jump_label.h"
 struct static_key {
    atomic_t enabled ;
 };
 #line 22 "include/linux/tracepoint.h"
 struct module;
 #line 23
 struct tracepoint;
 #line 23
 struct tracepoint;
 #line 25 "include/linux/tracepoint.h"
 struct tracepoint_func {
    void *func ;
    void *data ;
 };
 #line 30 "include/linux/tracepoint.h"
 struct tracepoint {
    char const   *name ;
    struct static_key key ;
    void (*regfunc)(void) ;
    void (*unregfunc)(void) ;
    struct tracepoint_func *funcs ;
 };
 #line 19 "include/linux/export.h"
 struct kernel_symbol {
    unsigned long value ;
    char const   *name ;
 };
 #line 8 "include/asm-generic/module.h"
 struct mod_arch_specific {
 
 };
 #line 35 "include/linux/module.h"
 struct module;
 #line 37
 struct module_param_attrs;
 #line 37 "include/linux/module.h"
 struct module_kobject {
    struct kobject kobj ;
    struct module *mod ;
    struct kobject *drivers_dir ;
    struct module_param_attrs *mp ;
 };
 #line 44 "include/linux/module.h"
 struct module_attribute {
    struct attribute attr ;
    ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
    ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
                     size_t count ) ;
    void (*setup)(struct module * , char const   * ) ;
    int (*test)(struct module * ) ;
    void (*free)(struct module * ) ;
 };
 #line 71
 struct exception_table_entry;
 #line 71
 struct exception_table_entry;
 #line 199
 enum module_state {
     MODULE_STATE_LIVE = 0,
     MODULE_STATE_COMING = 1,
     MODULE_STATE_GOING = 2
 } ;
 #line 215 "include/linux/module.h"
 struct module_ref {
    unsigned long incs ;
    unsigned long decs ;
 } __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 #line 220
 struct module_sect_attrs;
 #line 220
 struct module_notes_attrs;
 #line 220
 struct ftrace_event_call;
 #line 220 "include/linux/module.h"
 struct module {
    enum module_state state ;
    struct list_head list ;
    char name[64UL - sizeof(unsigned long )] ;
    struct module_kobject mkobj ;
    struct module_attribute *modinfo_attrs ;
    char const   *version ;
    char const   *srcversion ;
    struct kobject *holders_dir ;
    struct kernel_symbol  const  *syms ;
    unsigned long const   *crcs ;
    unsigned int num_syms ;
    struct kernel_param *kp ;
    unsigned int num_kp ;
    unsigned int num_gpl_syms ;
    struct kernel_symbol  const  *gpl_syms ;
    unsigned long const   *gpl_crcs ;
    struct kernel_symbol  const  *unused_syms ;
    unsigned long const   *unused_crcs ;
    unsigned int num_unused_syms ;
    unsigned int num_unused_gpl_syms ;
    struct kernel_symbol  const  *unused_gpl_syms ;
    unsigned long const   *unused_gpl_crcs ;
    struct kernel_symbol  const  *gpl_future_syms ;
    unsigned long const   *gpl_future_crcs ;
    unsigned int num_gpl_future_syms ;
    unsigned int num_exentries ;
    struct exception_table_entry *extable ;
    int (*init)(void) ;
    void *module_init ;
    void *module_core ;
    unsigned int init_size ;
    unsigned int core_size ;
    unsigned int init_text_size ;
    unsigned int core_text_size ;
    unsigned int init_ro_size ;
    unsigned int core_ro_size ;
    struct mod_arch_specific arch ;
    unsigned int taints ;
    unsigned int num_bugs ;
    struct list_head bug_list ;
    struct bug_entry *bug_table ;
    Elf64_Sym *symtab ;
    Elf64_Sym *core_symtab ;
    unsigned int num_symtab ;
    unsigned int core_num_syms ;
    char *strtab ;
    char *core_strtab ;
    struct module_sect_attrs *sect_attrs ;
    struct module_notes_attrs *notes_attrs ;
    char *args ;
    void *percpu ;
    unsigned int percpu_size ;
    unsigned int num_tracepoints ;
    struct tracepoint * const  *tracepoints_ptrs ;
    unsigned int num_trace_bprintk_fmt ;
    char const   **trace_bprintk_fmt_start ;
    struct ftrace_event_call **trace_events ;
    unsigned int num_trace_events ;
    struct list_head source_list ;
    struct list_head target_list ;
    struct task_struct *waiter ;
    void (*exit)(void) ;
    struct module_ref *refptr ;
    ctor_fn_t *ctors ;
    unsigned int num_ctors ;
 };
 #line 36 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h"
 struct pi_protocol;
 #line 36 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h"
 struct pi_adapter {
    struct pi_protocol *proto ;
    int port ;
    int mode ;
    int delay ;
    int devtype ;
    char *device ;
    int unit ;
    int saved_r0 ;
    int saved_r2 ;
    int reserved ;
    unsigned long private ;
    wait_queue_head_t parq ;
    void *pardev ;
    char *parname ;
    int claimed ;
    void (*claim_cont)(void) ;
 };
 #line 57 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h"
 typedef struct pi_adapter PIA;
 #line 135 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h"
 struct pi_protocol {
    char name[8] ;
    int index ;
    int max_mode ;
    int epp_first ;
    int default_delay ;
    int max_units ;
    void (*write_regr)(PIA * , int  , int  , int  ) ;
    int (*read_regr)(PIA * , int  , int  ) ;
    void (*write_block)(PIA * , char * , int  ) ;
    void (*read_block)(PIA * , char * , int  ) ;
    void (*connect)(PIA * ) ;
    void (*disconnect)(PIA * ) ;
    int (*test_port)(PIA * ) ;
    int (*probe_unit)(PIA * ) ;
    int (*test_proto)(PIA * , char * , int  ) ;
    void (*log_adapter)(PIA * , char * , int  ) ;
    int (*init_proto)(PIA * ) ;
    void (*release_proto)(PIA * ) ;
    struct module *owner ;
 };
 #line 164 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h"
 typedef struct pi_protocol PIP;
 #line 1 "<compiler builtins>"
 long __builtin_expect(long val , long res ) ;
 #line 100 "include/linux/printk.h"
 extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
 #line 152 "include/linux/mutex.h"
 void mutex_lock(struct mutex *lock ) ;
 #line 153
 int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
 #line 154
 int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
 #line 168
 int mutex_trylock(struct mutex *lock ) ;
 #line 169
 void mutex_unlock(struct mutex *lock ) ;
 #line 170
 int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
 #line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
 __inline static void outb(unsigned char value , int port )  __attribute__((__no_instrument_function__)) ;
 #line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
 __inline static void outb(unsigned char value , int port ) 
 { 
 
   {
 #line 308
   __asm__  volatile   ("out"
                        "b"
                        " %"
                        "b"
                        "0, %w1": : "a" (value), "Nd" (port));
 #line 308
   return;
 }
 }
 #line 308
 __inline static unsigned char inb(int port )  __attribute__((__no_instrument_function__)) ;
 #line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
 __inline static unsigned char inb(int port ) 
 { unsigned char value ;
 
   {
 #line 308
   __asm__  volatile   ("in"
                        "b"
                        " %w1, %"
                        "b"
                        "0": "=a" (value): "Nd" (port));
 #line 308
   return (value);
 }
 }
 #line 26 "include/linux/export.h"
 extern struct module __this_module ;
 #line 67 "include/linux/module.h"
 int init_module(void) ;
 #line 68
 void cleanup_module(void) ;
 #line 8 "include/asm-generic/delay.h"
 extern void __udelay(unsigned long usecs ) ;
 #line 166 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h"
 extern int paride_register(PIP * ) ;
 #line 167
 extern void paride_unregister(PIP * ) ;
 #line 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
 static void fit2_write_regr(PIA *pi , int cont , int regr , int val ) 
 { unsigned long __cil_tmp5 ;
   unsigned long __cil_tmp6 ;
   int __cil_tmp7 ;
   int __cil_tmp8 ;
   unsigned long __cil_tmp9 ;
   unsigned long __cil_tmp10 ;
   unsigned long __cil_tmp11 ;
   unsigned long __cil_tmp12 ;
   int __cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   unsigned char __cil_tmp15 ;
   unsigned long __cil_tmp16 ;
   unsigned long __cil_tmp17 ;
   int __cil_tmp18 ;
   unsigned long __cil_tmp19 ;
   unsigned long __cil_tmp20 ;
   unsigned long __cil_tmp21 ;
   unsigned long __cil_tmp22 ;
   int __cil_tmp23 ;
   unsigned long __cil_tmp24 ;
   unsigned long __cil_tmp25 ;
   unsigned long __cil_tmp26 ;
   int __cil_tmp27 ;
   int __cil_tmp28 ;
   unsigned long __cil_tmp29 ;
   unsigned long __cil_tmp30 ;
   unsigned long __cil_tmp31 ;
   unsigned long __cil_tmp32 ;
   int __cil_tmp33 ;
   unsigned long __cil_tmp34 ;
   unsigned char __cil_tmp35 ;
   unsigned long __cil_tmp36 ;
   unsigned long __cil_tmp37 ;
   int __cil_tmp38 ;
   unsigned long __cil_tmp39 ;
   unsigned long __cil_tmp40 ;
   unsigned long __cil_tmp41 ;
   unsigned long __cil_tmp42 ;
   int __cil_tmp43 ;
   unsigned long __cil_tmp44 ;
   unsigned long __cil_tmp45 ;
   unsigned long __cil_tmp46 ;
   int __cil_tmp47 ;
   int __cil_tmp48 ;
   unsigned long __cil_tmp49 ;
   unsigned long __cil_tmp50 ;
   unsigned long __cil_tmp51 ;
   unsigned long __cil_tmp52 ;
   int __cil_tmp53 ;
   unsigned long __cil_tmp54 ;
   unsigned long __cil_tmp55 ;
   unsigned long __cil_tmp56 ;
   int __cil_tmp57 ;
   unsigned long __cil_tmp58 ;
   unsigned long __cil_tmp59 ;
   unsigned long __cil_tmp60 ;
   unsigned long __cil_tmp61 ;
   int __cil_tmp62 ;
   unsigned long __cil_tmp63 ;
   unsigned long __cil_tmp64 ;
   unsigned long __cil_tmp65 ;
   int __cil_tmp66 ;
   int __cil_tmp67 ;
   unsigned long __cil_tmp68 ;
   unsigned long __cil_tmp69 ;
   unsigned long __cil_tmp70 ;
   unsigned long __cil_tmp71 ;
   int __cil_tmp72 ;
   unsigned long __cil_tmp73 ;
 
   {
 #line 43
   if (cont == 1) {
 #line 43
     return;
   } else {
 
   }
   {
 #line 44
   __cil_tmp5 = (unsigned long )pi;
 #line 44
   __cil_tmp6 = __cil_tmp5 + 8;
 #line 44
   __cil_tmp7 = *((int *)__cil_tmp6);
 #line 44
   __cil_tmp8 = __cil_tmp7 + 2;
 #line 44
   outb((unsigned char)12, __cil_tmp8);
   }
   {
 #line 44
   __cil_tmp9 = (unsigned long )pi;
 #line 44
   __cil_tmp10 = __cil_tmp9 + 16;
 #line 44
   if (*((int *)__cil_tmp10)) {
     {
 #line 44
     __cil_tmp11 = (unsigned long )pi;
 #line 44
     __cil_tmp12 = __cil_tmp11 + 16;
 #line 44
     __cil_tmp13 = *((int *)__cil_tmp12);
 #line 44
     __cil_tmp14 = (unsigned long )__cil_tmp13;
 #line 44
     __udelay(__cil_tmp14);
     }
   } else {
 
   }
   }
   {
 #line 44
   __cil_tmp15 = (unsigned char )regr;
 #line 44
   __cil_tmp16 = (unsigned long )pi;
 #line 44
   __cil_tmp17 = __cil_tmp16 + 8;
 #line 44
   __cil_tmp18 = *((int *)__cil_tmp17);
 #line 44
   outb(__cil_tmp15, __cil_tmp18);
   }
   {
 #line 44
   __cil_tmp19 = (unsigned long )pi;
 #line 44
   __cil_tmp20 = __cil_tmp19 + 16;
 #line 44
   if (*((int *)__cil_tmp20)) {
     {
 #line 44
     __cil_tmp21 = (unsigned long )pi;
 #line 44
     __cil_tmp22 = __cil_tmp21 + 16;
 #line 44
     __cil_tmp23 = *((int *)__cil_tmp22);
 #line 44
     __cil_tmp24 = (unsigned long )__cil_tmp23;
 #line 44
     __udelay(__cil_tmp24);
     }
   } else {
 
   }
   }
   {
 #line 44
   __cil_tmp25 = (unsigned long )pi;
 #line 44
   __cil_tmp26 = __cil_tmp25 + 8;
 #line 44
   __cil_tmp27 = *((int *)__cil_tmp26);
 #line 44
   __cil_tmp28 = __cil_tmp27 + 2;
 #line 44
   outb((unsigned char)4, __cil_tmp28);
   }
   {
 #line 44
   __cil_tmp29 = (unsigned long )pi;
 #line 44
   __cil_tmp30 = __cil_tmp29 + 16;
 #line 44
   if (*((int *)__cil_tmp30)) {
     {
 #line 44
     __cil_tmp31 = (unsigned long )pi;
 #line 44
     __cil_tmp32 = __cil_tmp31 + 16;
 #line 44
     __cil_tmp33 = *((int *)__cil_tmp32);
 #line 44
     __cil_tmp34 = (unsigned long )__cil_tmp33;
 #line 44
     __udelay(__cil_tmp34);
     }
   } else {
 
   }
   }
   {
 #line 44
   __cil_tmp35 = (unsigned char )val;
 #line 44
   __cil_tmp36 = (unsigned long )pi;
 #line 44
   __cil_tmp37 = __cil_tmp36 + 8;
 #line 44
   __cil_tmp38 = *((int *)__cil_tmp37);
 #line 44
   outb(__cil_tmp35, __cil_tmp38);
   }
   {
 #line 44
   __cil_tmp39 = (unsigned long )pi;
 #line 44
   __cil_tmp40 = __cil_tmp39 + 16;
 #line 44
   if (*((int *)__cil_tmp40)) {
     {
 #line 44
     __cil_tmp41 = (unsigned long )pi;
 #line 44
     __cil_tmp42 = __cil_tmp41 + 16;
 #line 44
     __cil_tmp43 = *((int *)__cil_tmp42);
 #line 44
     __cil_tmp44 = (unsigned long )__cil_tmp43;
 #line 44
     __udelay(__cil_tmp44);
     }
   } else {
 
   }
   }
   {
 #line 44
   __cil_tmp45 = (unsigned long )pi;
 #line 44
   __cil_tmp46 = __cil_tmp45 + 8;
 #line 44
   __cil_tmp47 = *((int *)__cil_tmp46);
 #line 44
   __cil_tmp48 = __cil_tmp47 + 2;
 #line 44
   outb((unsigned char)5, __cil_tmp48);
   }
   {
 #line 44
   __cil_tmp49 = (unsigned long )pi;
 #line 44
   __cil_tmp50 = __cil_tmp49 + 16;
 #line 44
   if (*((int *)__cil_tmp50)) {
     {
 #line 44
     __cil_tmp51 = (unsigned long )pi;
 #line 44
     __cil_tmp52 = __cil_tmp51 + 16;
 #line 44
     __cil_tmp53 = *((int *)__cil_tmp52);
 #line 44
     __cil_tmp54 = (unsigned long )__cil_tmp53;
 #line 44
     __udelay(__cil_tmp54);
     }
   } else {
 
   }
   }
   {
 #line 44
   __cil_tmp55 = (unsigned long )pi;
 #line 44
   __cil_tmp56 = __cil_tmp55 + 8;
 #line 44
   __cil_tmp57 = *((int *)__cil_tmp56);
 #line 44
   outb((unsigned char)0, __cil_tmp57);
   }
   {
 #line 44
   __cil_tmp58 = (unsigned long )pi;
 #line 44
   __cil_tmp59 = __cil_tmp58 + 16;
 #line 44
   if (*((int *)__cil_tmp59)) {
     {
 #line 44
     __cil_tmp60 = (unsigned long )pi;
 #line 44
     __cil_tmp61 = __cil_tmp60 + 16;
 #line 44
     __cil_tmp62 = *((int *)__cil_tmp61);
 #line 44
     __cil_tmp63 = (unsigned long )__cil_tmp62;
 #line 44
     __udelay(__cil_tmp63);
     }
   } else {
 
   }
   }
   {
 #line 44
   __cil_tmp64 = (unsigned long )pi;
 #line 44
   __cil_tmp65 = __cil_tmp64 + 8;
 #line 44
   __cil_tmp66 = *((int *)__cil_tmp65);
 #line 44
   __cil_tmp67 = __cil_tmp66 + 2;
 #line 44
   outb((unsigned char)4, __cil_tmp67);
   }
   {
 #line 44
   __cil_tmp68 = (unsigned long )pi;
 #line 44
   __cil_tmp69 = __cil_tmp68 + 16;
 #line 44
   if (*((int *)__cil_tmp69)) {
     {
 #line 44
     __cil_tmp70 = (unsigned long )pi;
 #line 44
     __cil_tmp71 = __cil_tmp70 + 16;
 #line 44
     __cil_tmp72 = *((int *)__cil_tmp71);
 #line 44
     __cil_tmp73 = (unsigned long )__cil_tmp72;
 #line 44
     __udelay(__cil_tmp73);
     }
   } else {
 
   }
   }
 #line 45
   return;
 }
 }
 #line 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
 static int fit2_read_regr(PIA *pi , int cont , int regr ) 
 { int a ;
   int b ;
   int r ;
   unsigned char tmp ;
   unsigned char tmp___0 ;
   unsigned long __cil_tmp9 ;
   unsigned long __cil_tmp10 ;
   int __cil_tmp11 ;
   int __cil_tmp12 ;
   unsigned long __cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   unsigned long __cil_tmp15 ;
   unsigned long __cil_tmp16 ;
   int __cil_tmp17 ;
   unsigned long __cil_tmp18 ;
   unsigned char __cil_tmp19 ;
   unsigned long __cil_tmp20 ;
   unsigned long __cil_tmp21 ;
   int __cil_tmp22 ;
   unsigned long __cil_tmp23 ;
   unsigned long __cil_tmp24 ;
   unsigned long __cil_tmp25 ;
   unsigned long __cil_tmp26 ;
   int __cil_tmp27 ;
   unsigned long __cil_tmp28 ;
   unsigned long __cil_tmp29 ;
   unsigned long __cil_tmp30 ;
   int __cil_tmp31 ;
   int __cil_tmp32 ;
   unsigned long __cil_tmp33 ;
   unsigned long __cil_tmp34 ;
   unsigned long __cil_tmp35 ;
   unsigned long __cil_tmp36 ;
   int __cil_tmp37 ;
   unsigned long __cil_tmp38 ;
   unsigned long __cil_tmp39 ;
   unsigned long __cil_tmp40 ;
   int __cil_tmp41 ;
   int __cil_tmp42 ;
   unsigned long __cil_tmp43 ;
   unsigned long __cil_tmp44 ;
   unsigned long __cil_tmp45 ;
   unsigned long __cil_tmp46 ;
   int __cil_tmp47 ;
   unsigned long __cil_tmp48 ;
   unsigned long __cil_tmp49 ;
   unsigned long __cil_tmp50 ;
   int __cil_tmp51 ;
   unsigned long __cil_tmp52 ;
   unsigned long __cil_tmp53 ;
   unsigned long __cil_tmp54 ;
   unsigned long __cil_tmp55 ;
   int __cil_tmp56 ;
   unsigned long __cil_tmp57 ;
   unsigned long __cil_tmp58 ;
   unsigned long __cil_tmp59 ;
   unsigned long __cil_tmp60 ;
   unsigned long __cil_tmp61 ;
   int __cil_tmp62 ;
   unsigned long __cil_tmp63 ;
   unsigned long __cil_tmp64 ;
   unsigned long __cil_tmp65 ;
   int __cil_tmp66 ;
   int __cil_tmp67 ;
   int __cil_tmp68 ;
   unsigned long __cil_tmp69 ;
   unsigned long __cil_tmp70 ;
   int __cil_tmp71 ;
   unsigned long __cil_tmp72 ;
   unsigned long __cil_tmp73 ;
   unsigned long __cil_tmp74 ;
   unsigned long __cil_tmp75 ;
   int __cil_tmp76 ;
   unsigned long __cil_tmp77 ;
   unsigned long __cil_tmp78 ;
   unsigned long __cil_tmp79 ;
   unsigned long __cil_tmp80 ;
   unsigned long __cil_tmp81 ;
   int __cil_tmp82 ;
   unsigned long __cil_tmp83 ;
   unsigned long __cil_tmp84 ;
   unsigned long __cil_tmp85 ;
   int __cil_tmp86 ;
   int __cil_tmp87 ;
   int __cil_tmp88 ;
   unsigned long __cil_tmp89 ;
   unsigned long __cil_tmp90 ;
   int __cil_tmp91 ;
   int __cil_tmp92 ;
   unsigned long __cil_tmp93 ;
   unsigned long __cil_tmp94 ;
   unsigned long __cil_tmp95 ;
   unsigned long __cil_tmp96 ;
   int __cil_tmp97 ;
   unsigned long __cil_tmp98 ;
   int __cil_tmp99 ;
   int __cil_tmp100 ;
   int __cil_tmp101 ;
 
   {
 #line 51
   if (cont) {
 #line 52
     if (regr != 6) {
 #line 52
       return (255);
     } else {
 
     }
 #line 53
     r = 7;
   } else {
 #line 54
     r = regr + 16;
   }
   {
 #line 56
   __cil_tmp9 = (unsigned long )pi;
 #line 56
   __cil_tmp10 = __cil_tmp9 + 8;
 #line 56
   __cil_tmp11 = *((int *)__cil_tmp10);
 #line 56
   __cil_tmp12 = __cil_tmp11 + 2;
 #line 56
   outb((unsigned char)12, __cil_tmp12);
   }
  {
#line 56
  __cil_tmp13 = (unsigned long )pi;
#line 56
  __cil_tmp14 = __cil_tmp13 + 16;
#line 56
  if (*((int *)__cil_tmp14)) {
    {
#line 56
    __cil_tmp15 = (unsigned long )pi;
#line 56
    __cil_tmp16 = __cil_tmp15 + 16;
#line 56
    __cil_tmp17 = *((int *)__cil_tmp16);
#line 56
    __cil_tmp18 = (unsigned long )__cil_tmp17;
#line 56
    __udelay(__cil_tmp18);
    }
  } else {

  }
  }
  {
#line 56
  __cil_tmp19 = (unsigned char )r;
#line 56
  __cil_tmp20 = (unsigned long )pi;
#line 56
  __cil_tmp21 = __cil_tmp20 + 8;
#line 56
  __cil_tmp22 = *((int *)__cil_tmp21);
#line 56
  outb(__cil_tmp19, __cil_tmp22);
  }
  {
#line 56
  __cil_tmp23 = (unsigned long )pi;
#line 56
  __cil_tmp24 = __cil_tmp23 + 16;
#line 56
  if (*((int *)__cil_tmp24)) {
    {
#line 56
    __cil_tmp25 = (unsigned long )pi;
#line 56
    __cil_tmp26 = __cil_tmp25 + 16;
#line 56
    __cil_tmp27 = *((int *)__cil_tmp26);
#line 56
    __cil_tmp28 = (unsigned long )__cil_tmp27;
#line 56
    __udelay(__cil_tmp28);
    }
  } else {

  }
  }
  {
#line 56
  __cil_tmp29 = (unsigned long )pi;
#line 56
  __cil_tmp30 = __cil_tmp29 + 8;
#line 56
  __cil_tmp31 = *((int *)__cil_tmp30);
#line 56
  __cil_tmp32 = __cil_tmp31 + 2;
#line 56
  outb((unsigned char)4, __cil_tmp32);
  }
  {
#line 56
  __cil_tmp33 = (unsigned long )pi;
#line 56
  __cil_tmp34 = __cil_tmp33 + 16;
#line 56
  if (*((int *)__cil_tmp34)) {
    {
#line 56
    __cil_tmp35 = (unsigned long )pi;
#line 56
    __cil_tmp36 = __cil_tmp35 + 16;
#line 56
    __cil_tmp37 = *((int *)__cil_tmp36);
#line 56
    __cil_tmp38 = (unsigned long )__cil_tmp37;
#line 56
    __udelay(__cil_tmp38);
    }
  } else {

  }
  }
  {
#line 56
  __cil_tmp39 = (unsigned long )pi;
#line 56
  __cil_tmp40 = __cil_tmp39 + 8;
#line 56
  __cil_tmp41 = *((int *)__cil_tmp40);
#line 56
  __cil_tmp42 = __cil_tmp41 + 2;
#line 56
  outb((unsigned char)5, __cil_tmp42);
  }
  {
#line 56
  __cil_tmp43 = (unsigned long )pi;
#line 56
  __cil_tmp44 = __cil_tmp43 + 16;
#line 56
  if (*((int *)__cil_tmp44)) {
    {
#line 56
    __cil_tmp45 = (unsigned long )pi;
#line 56
    __cil_tmp46 = __cil_tmp45 + 16;
#line 56
    __cil_tmp47 = *((int *)__cil_tmp46);
#line 56
    __cil_tmp48 = (unsigned long )__cil_tmp47;
#line 56
    __udelay(__cil_tmp48);
    }
  } else {

  }
  }
  {
#line 57
  __cil_tmp49 = (unsigned long )pi;
#line 57
  __cil_tmp50 = __cil_tmp49 + 8;
#line 57
  __cil_tmp51 = *((int *)__cil_tmp50);
#line 57
  outb((unsigned char)0, __cil_tmp51);
  }
  {
#line 57
  __cil_tmp52 = (unsigned long )pi;
#line 57
  __cil_tmp53 = __cil_tmp52 + 16;
#line 57
  if (*((int *)__cil_tmp53)) {
    {
#line 57
    __cil_tmp54 = (unsigned long )pi;
#line 57
    __cil_tmp55 = __cil_tmp54 + 16;
#line 57
    __cil_tmp56 = *((int *)__cil_tmp55);
#line 57
    __cil_tmp57 = (unsigned long )__cil_tmp56;
#line 57
    __udelay(__cil_tmp57);
    }
  } else {

  }
  }
  {
#line 57
  __cil_tmp58 = (unsigned long )pi;
#line 57
  __cil_tmp59 = __cil_tmp58 + 16;
#line 57
  if (*((int *)__cil_tmp59)) {
    {
#line 57
    __cil_tmp60 = (unsigned long )pi;
#line 57
    __cil_tmp61 = __cil_tmp60 + 16;
#line 57
    __cil_tmp62 = *((int *)__cil_tmp61);
#line 57
    __cil_tmp63 = (unsigned long )__cil_tmp62;
#line 57
    __udelay(__cil_tmp63);
    }
  } else {

  }
  }
  {
#line 57
  __cil_tmp64 = (unsigned long )pi;
#line 57
  __cil_tmp65 = __cil_tmp64 + 8;
#line 57
  __cil_tmp66 = *((int *)__cil_tmp65);
#line 57
  __cil_tmp67 = __cil_tmp66 + 1;
#line 57
  tmp = inb(__cil_tmp67);
#line 57
  __cil_tmp68 = (int )tmp;
#line 57
  a = __cil_tmp68 & 255;
#line 58
  __cil_tmp69 = (unsigned long )pi;
#line 58
  __cil_tmp70 = __cil_tmp69 + 8;
#line 58
  __cil_tmp71 = *((int *)__cil_tmp70);
#line 58
  outb((unsigned char)1, __cil_tmp71);
  }
  {
#line 58
  __cil_tmp72 = (unsigned long )pi;
#line 58
  __cil_tmp73 = __cil_tmp72 + 16;
#line 58
  if (*((int *)__cil_tmp73)) {
    {
#line 58
    __cil_tmp74 = (unsigned long )pi;
#line 58
    __cil_tmp75 = __cil_tmp74 + 16;
#line 58
    __cil_tmp76 = *((int *)__cil_tmp75);
#line 58
    __cil_tmp77 = (unsigned long )__cil_tmp76;
#line 58
    __udelay(__cil_tmp77);
    }
  } else {

  }
  }
  {
#line 58
  __cil_tmp78 = (unsigned long )pi;
#line 58
  __cil_tmp79 = __cil_tmp78 + 16;
#line 58
  if (*((int *)__cil_tmp79)) {
    {
#line 58
    __cil_tmp80 = (unsigned long )pi;
#line 58
    __cil_tmp81 = __cil_tmp80 + 16;
#line 58
    __cil_tmp82 = *((int *)__cil_tmp81);
#line 58
    __cil_tmp83 = (unsigned long )__cil_tmp82;
#line 58
    __udelay(__cil_tmp83);
    }
  } else {

  }
  }
  {
#line 58
  __cil_tmp84 = (unsigned long )pi;
#line 58
  __cil_tmp85 = __cil_tmp84 + 8;
#line 58
  __cil_tmp86 = *((int *)__cil_tmp85);
#line 58
  __cil_tmp87 = __cil_tmp86 + 1;
#line 58
  tmp___0 = inb(__cil_tmp87);
#line 58
  __cil_tmp88 = (int )tmp___0;
#line 58
  b = __cil_tmp88 & 255;
#line 59
  __cil_tmp89 = (unsigned long )pi;
#line 59
  __cil_tmp90 = __cil_tmp89 + 8;
#line 59
  __cil_tmp91 = *((int *)__cil_tmp90);
#line 59
  __cil_tmp92 = __cil_tmp91 + 2;
#line 59
  outb((unsigned char)4, __cil_tmp92);
  }
  {
#line 59
  __cil_tmp93 = (unsigned long )pi;
#line 59
  __cil_tmp94 = __cil_tmp93 + 16;
#line 59
  if (*((int *)__cil_tmp94)) {
    {
#line 59
    __cil_tmp95 = (unsigned long )pi;
#line 59
    __cil_tmp96 = __cil_tmp95 + 16;
#line 59
    __cil_tmp97 = *((int *)__cil_tmp96);
#line 59
    __cil_tmp98 = (unsigned long )__cil_tmp97;
#line 59
    __udelay(__cil_tmp98);
    }
  } else {

  }
  }
  {
#line 61
  __cil_tmp99 = b & 240;
#line 61
  __cil_tmp100 = a >> 4;
#line 61
  __cil_tmp101 = __cil_tmp100 & 15;
#line 61
  return (__cil_tmp101 | __cil_tmp99);
  }
}
}
#line 65 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
static void fit2_read_block(PIA *pi , char *buf , int count ) 
{ int k ;
  int a ;
  int b ;
  int c ;
  int d ;
  unsigned char tmp ;
  unsigned char tmp___0 ;
  unsigned char tmp___1 ;
  unsigned char tmp___2 ;
  unsigned char tmp___3 ;
  unsigned char tmp___4 ;
  unsigned char tmp___5 ;
  unsigned char tmp___6 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  int __cil_tmp19 ;
  int __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  int __cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  int __cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  unsigned long __cil_tmp33 ;
  int __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  int __cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  int __cil_tmp39 ;
  int __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  int __cil_tmp45 ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  int __cil_tmp49 ;
  int __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  int __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned long __cil_tmp58 ;
  int __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  unsigned long __cil_tmp62 ;
  unsigned long __cil_tmp63 ;
  int __cil_tmp64 ;
  unsigned long __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  unsigned long __cil_tmp68 ;
  unsigned long __cil_tmp69 ;
  int __cil_tmp70 ;
  unsigned long __cil_tmp71 ;
  unsigned long __cil_tmp72 ;
  unsigned long __cil_tmp73 ;
  int __cil_tmp74 ;
  int __cil_tmp75 ;
  int __cil_tmp76 ;
  unsigned long __cil_tmp77 ;
  unsigned long __cil_tmp78 ;
  int __cil_tmp79 ;
  unsigned long __cil_tmp80 ;
  unsigned long __cil_tmp81 ;
  unsigned long __cil_tmp82 ;
  unsigned long __cil_tmp83 ;
  int __cil_tmp84 ;
  unsigned long __cil_tmp85 ;
  unsigned long __cil_tmp86 ;
  unsigned long __cil_tmp87 ;
  unsigned long __cil_tmp88 ;
  unsigned long __cil_tmp89 ;
  int __cil_tmp90 ;
  unsigned long __cil_tmp91 ;
  unsigned long __cil_tmp92 ;
  unsigned long __cil_tmp93 ;
  int __cil_tmp94 ;
  int __cil_tmp95 ;
  int __cil_tmp96 ;
  unsigned long __cil_tmp97 ;
  unsigned long __cil_tmp98 ;
  int __cil_tmp99 ;
  unsigned long __cil_tmp100 ;
  unsigned long __cil_tmp101 ;
  unsigned long __cil_tmp102 ;
  unsigned long __cil_tmp103 ;
  int __cil_tmp104 ;
  unsigned long __cil_tmp105 ;
  unsigned long __cil_tmp106 ;
  unsigned long __cil_tmp107 ;
  unsigned long __cil_tmp108 ;
  unsigned long __cil_tmp109 ;
  int __cil_tmp110 ;
  unsigned long __cil_tmp111 ;
  unsigned long __cil_tmp112 ;
  unsigned long __cil_tmp113 ;
  int __cil_tmp114 ;
  int __cil_tmp115 ;
  int __cil_tmp116 ;
  unsigned long __cil_tmp117 ;
  unsigned long __cil_tmp118 ;
  int __cil_tmp119 ;
  unsigned long __cil_tmp120 ;
  unsigned long __cil_tmp121 ;
  unsigned long __cil_tmp122 ;
  unsigned long __cil_tmp123 ;
  int __cil_tmp124 ;
  unsigned long __cil_tmp125 ;
  unsigned long __cil_tmp126 ;
  unsigned long __cil_tmp127 ;
  unsigned long __cil_tmp128 ;
  unsigned long __cil_tmp129 ;
  int __cil_tmp130 ;
  unsigned long __cil_tmp131 ;
  unsigned long __cil_tmp132 ;
  unsigned long __cil_tmp133 ;
  int __cil_tmp134 ;
  int __cil_tmp135 ;
  int __cil_tmp136 ;
  int __cil_tmp137 ;
  char *__cil_tmp138 ;
  int __cil_tmp139 ;
  int __cil_tmp140 ;
  int __cil_tmp141 ;
  int __cil_tmp142 ;
  int __cil_tmp143 ;
  int __cil_tmp144 ;
  char *__cil_tmp145 ;
  int __cil_tmp146 ;
  int __cil_tmp147 ;
  int __cil_tmp148 ;
  int __cil_tmp149 ;
  unsigned long __cil_tmp150 ;
  unsigned long __cil_tmp151 ;
  int __cil_tmp152 ;
  int __cil_tmp153 ;
  unsigned long __cil_tmp154 ;
  unsigned long __cil_tmp155 ;
  unsigned long __cil_tmp156 ;
  unsigned long __cil_tmp157 ;
  int __cil_tmp158 ;
  unsigned long __cil_tmp159 ;
  unsigned long __cil_tmp160 ;
  unsigned long __cil_tmp161 ;
  int __cil_tmp162 ;
  int __cil_tmp163 ;
  unsigned long __cil_tmp164 ;
  unsigned long __cil_tmp165 ;
  unsigned long __cil_tmp166 ;
  unsigned long __cil_tmp167 ;
  int __cil_tmp168 ;
  unsigned long __cil_tmp169 ;
  unsigned long __cil_tmp170 ;
  unsigned long __cil_tmp171 ;
  unsigned long __cil_tmp172 ;
  unsigned long __cil_tmp173 ;
  int __cil_tmp174 ;
  unsigned long __cil_tmp175 ;
  unsigned long __cil_tmp176 ;
  unsigned long __cil_tmp177 ;
  int __cil_tmp178 ;
  int __cil_tmp179 ;
  int __cil_tmp180 ;
  unsigned long __cil_tmp181 ;
  unsigned long __cil_tmp182 ;
  int __cil_tmp183 ;
  unsigned long __cil_tmp184 ;
  unsigned long __cil_tmp185 ;
  unsigned long __cil_tmp186 ;
  unsigned long __cil_tmp187 ;
  int __cil_tmp188 ;
  unsigned long __cil_tmp189 ;
  unsigned long __cil_tmp190 ;
  unsigned long __cil_tmp191 ;
  unsigned long __cil_tmp192 ;
  unsigned long __cil_tmp193 ;
  int __cil_tmp194 ;
  unsigned long __cil_tmp195 ;
  unsigned long __cil_tmp196 ;
  unsigned long __cil_tmp197 ;
  int __cil_tmp198 ;
  int __cil_tmp199 ;
  int __cil_tmp200 ;
  unsigned long __cil_tmp201 ;
  unsigned long __cil_tmp202 ;
  int __cil_tmp203 ;
  unsigned long __cil_tmp204 ;
  unsigned long __cil_tmp205 ;
  unsigned long __cil_tmp206 ;
  unsigned long __cil_tmp207 ;
  int __cil_tmp208 ;
  unsigned long __cil_tmp209 ;
  unsigned long __cil_tmp210 ;
  unsigned long __cil_tmp211 ;
  unsigned long __cil_tmp212 ;
  unsigned long __cil_tmp213 ;
  int __cil_tmp214 ;
  unsigned long __cil_tmp215 ;
  unsigned long __cil_tmp216 ;
  unsigned long __cil_tmp217 ;
  int __cil_tmp218 ;
  int __cil_tmp219 ;
  int __cil_tmp220 ;
  unsigned long __cil_tmp221 ;
  unsigned long __cil_tmp222 ;
  int __cil_tmp223 ;
  unsigned long __cil_tmp224 ;
  unsigned long __cil_tmp225 ;
  unsigned long __cil_tmp226 ;
  unsigned long __cil_tmp227 ;
  int __cil_tmp228 ;
  unsigned long __cil_tmp229 ;
  unsigned long __cil_tmp230 ;
  unsigned long __cil_tmp231 ;
  unsigned long __cil_tmp232 ;
  unsigned long __cil_tmp233 ;
  int __cil_tmp234 ;
  unsigned long __cil_tmp235 ;
  unsigned long __cil_tmp236 ;
  unsigned long __cil_tmp237 ;
  int __cil_tmp238 ;
  int __cil_tmp239 ;
  int __cil_tmp240 ;
  int __cil_tmp241 ;
  int __cil_tmp242 ;
  char *__cil_tmp243 ;
  int __cil_tmp244 ;
  int __cil_tmp245 ;
  int __cil_tmp246 ;
  int __cil_tmp247 ;
  int __cil_tmp248 ;
  int __cil_tmp249 ;
  char *__cil_tmp250 ;
  int __cil_tmp251 ;
  int __cil_tmp252 ;
  int __cil_tmp253 ;
  int __cil_tmp254 ;
  unsigned long __cil_tmp255 ;
  unsigned long __cil_tmp256 ;
  int __cil_tmp257 ;
  int __cil_tmp258 ;
  unsigned long __cil_tmp259 ;
  unsigned long __cil_tmp260 ;
  unsigned long __cil_tmp261 ;
  unsigned long __cil_tmp262 ;
  int __cil_tmp263 ;
  unsigned long __cil_tmp264 ;

  {
  {
#line 69
  __cil_tmp17 = (unsigned long )pi;
#line 69
  __cil_tmp18 = __cil_tmp17 + 8;
#line 69
  __cil_tmp19 = *((int *)__cil_tmp18);
#line 69
  __cil_tmp20 = __cil_tmp19 + 2;
#line 69
  outb((unsigned char)12, __cil_tmp20);
  }
  {
#line 69
  __cil_tmp21 = (unsigned long )pi;
#line 69
  __cil_tmp22 = __cil_tmp21 + 16;
#line 69
  if (*((int *)__cil_tmp22)) {
    {
#line 69
    __cil_tmp23 = (unsigned long )pi;
#line 69
    __cil_tmp24 = __cil_tmp23 + 16;
#line 69
    __cil_tmp25 = *((int *)__cil_tmp24);
#line 69
    __cil_tmp26 = (unsigned long )__cil_tmp25;
#line 69
    __udelay(__cil_tmp26);
    }
  } else {

  }
  }
  {
#line 69
  __cil_tmp27 = (unsigned long )pi;
#line 69
  __cil_tmp28 = __cil_tmp27 + 8;
#line 69
  __cil_tmp29 = *((int *)__cil_tmp28);
#line 69
  outb((unsigned char)16, __cil_tmp29);
  }
  {
#line 69
  __cil_tmp30 = (unsigned long )pi;
#line 69
  __cil_tmp31 = __cil_tmp30 + 16;
#line 69
  if (*((int *)__cil_tmp31)) {
    {
#line 69
    __cil_tmp32 = (unsigned long )pi;
#line 69
    __cil_tmp33 = __cil_tmp32 + 16;
#line 69
    __cil_tmp34 = *((int *)__cil_tmp33);
#line 69
    __cil_tmp35 = (unsigned long )__cil_tmp34;
#line 69
    __udelay(__cil_tmp35);
    }
  } else {

  }
  }
#line 71
  k = 0;
  {
#line 71
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 71
    __cil_tmp36 = count / 4;
#line 71
    if (k < __cil_tmp36) {

    } else {
#line 71
      goto while_break;
    }
    }
    {
#line 73
    __cil_tmp37 = (unsigned long )pi;
#line 73
    __cil_tmp38 = __cil_tmp37 + 8;
#line 73
    __cil_tmp39 = *((int *)__cil_tmp38);
#line 73
    __cil_tmp40 = __cil_tmp39 + 2;
#line 73
    outb((unsigned char)4, __cil_tmp40);
    }
    {
#line 73
    __cil_tmp41 = (unsigned long )pi;
#line 73
    __cil_tmp42 = __cil_tmp41 + 16;
#line 73
    if (*((int *)__cil_tmp42)) {
      {
#line 73
      __cil_tmp43 = (unsigned long )pi;
#line 73
      __cil_tmp44 = __cil_tmp43 + 16;
#line 73
      __cil_tmp45 = *((int *)__cil_tmp44);
#line 73
      __cil_tmp46 = (unsigned long )__cil_tmp45;
#line 73
      __udelay(__cil_tmp46);
      }
    } else {

    }
    }
    {
#line 73
    __cil_tmp47 = (unsigned long )pi;
#line 73
    __cil_tmp48 = __cil_tmp47 + 8;
#line 73
    __cil_tmp49 = *((int *)__cil_tmp48);
#line 73
    __cil_tmp50 = __cil_tmp49 + 2;
#line 73
    outb((unsigned char)5, __cil_tmp50);
    }
    {
#line 73
    __cil_tmp51 = (unsigned long )pi;
#line 73
    __cil_tmp52 = __cil_tmp51 + 16;
#line 73
    if (*((int *)__cil_tmp52)) {
      {
#line 73
      __cil_tmp53 = (unsigned long )pi;
#line 73
      __cil_tmp54 = __cil_tmp53 + 16;
#line 73
      __cil_tmp55 = *((int *)__cil_tmp54);
#line 73
      __cil_tmp56 = (unsigned long )__cil_tmp55;
#line 73
      __udelay(__cil_tmp56);
      }
    } else {

    }
    }
    {
#line 74
    __cil_tmp57 = (unsigned long )pi;
#line 74
    __cil_tmp58 = __cil_tmp57 + 8;
#line 74
    __cil_tmp59 = *((int *)__cil_tmp58);
#line 74
    outb((unsigned char)0, __cil_tmp59);
    }
    {
#line 74
    __cil_tmp60 = (unsigned long )pi;
#line 74
    __cil_tmp61 = __cil_tmp60 + 16;
#line 74
    if (*((int *)__cil_tmp61)) {
      {
#line 74
      __cil_tmp62 = (unsigned long )pi;
#line 74
      __cil_tmp63 = __cil_tmp62 + 16;
#line 74
      __cil_tmp64 = *((int *)__cil_tmp63);
#line 74
      __cil_tmp65 = (unsigned long )__cil_tmp64;
#line 74
      __udelay(__cil_tmp65);
      }
    } else {

    }
    }
    {
#line 74
    __cil_tmp66 = (unsigned long )pi;
#line 74
    __cil_tmp67 = __cil_tmp66 + 16;
#line 74
    if (*((int *)__cil_tmp67)) {
      {
#line 74
      __cil_tmp68 = (unsigned long )pi;
#line 74
      __cil_tmp69 = __cil_tmp68 + 16;
#line 74
      __cil_tmp70 = *((int *)__cil_tmp69);
#line 74
      __cil_tmp71 = (unsigned long )__cil_tmp70;
#line 74
      __udelay(__cil_tmp71);
      }
    } else {

    }
    }
    {
#line 74
    __cil_tmp72 = (unsigned long )pi;
#line 74
    __cil_tmp73 = __cil_tmp72 + 8;
#line 74
    __cil_tmp74 = *((int *)__cil_tmp73);
#line 74
    __cil_tmp75 = __cil_tmp74 + 1;
#line 74
    tmp = inb(__cil_tmp75);
#line 74
    __cil_tmp76 = (int )tmp;
#line 74
    a = __cil_tmp76 & 255;
#line 74
    __cil_tmp77 = (unsigned long )pi;
#line 74
    __cil_tmp78 = __cil_tmp77 + 8;
#line 74
    __cil_tmp79 = *((int *)__cil_tmp78);
#line 74
    outb((unsigned char)1, __cil_tmp79);
    }
    {
#line 74
    __cil_tmp80 = (unsigned long )pi;
#line 74
    __cil_tmp81 = __cil_tmp80 + 16;
#line 74
    if (*((int *)__cil_tmp81)) {
      {
#line 74
      __cil_tmp82 = (unsigned long )pi;
#line 74
      __cil_tmp83 = __cil_tmp82 + 16;
#line 74
      __cil_tmp84 = *((int *)__cil_tmp83);
#line 74
      __cil_tmp85 = (unsigned long )__cil_tmp84;
#line 74
      __udelay(__cil_tmp85);
      }
    } else {

    }
    }
    {
#line 74
    __cil_tmp86 = (unsigned long )pi;
#line 74
    __cil_tmp87 = __cil_tmp86 + 16;
#line 74
    if (*((int *)__cil_tmp87)) {
      {
#line 74
      __cil_tmp88 = (unsigned long )pi;
#line 74
      __cil_tmp89 = __cil_tmp88 + 16;
#line 74
      __cil_tmp90 = *((int *)__cil_tmp89);
#line 74
      __cil_tmp91 = (unsigned long )__cil_tmp90;
#line 74
      __udelay(__cil_tmp91);
      }
    } else {

    }
    }
    {
#line 74
    __cil_tmp92 = (unsigned long )pi;
#line 74
    __cil_tmp93 = __cil_tmp92 + 8;
#line 74
    __cil_tmp94 = *((int *)__cil_tmp93);
#line 74
    __cil_tmp95 = __cil_tmp94 + 1;
#line 74
    tmp___0 = inb(__cil_tmp95);
#line 74
    __cil_tmp96 = (int )tmp___0;
#line 74
    b = __cil_tmp96 & 255;
#line 75
    __cil_tmp97 = (unsigned long )pi;
#line 75
    __cil_tmp98 = __cil_tmp97 + 8;
#line 75
    __cil_tmp99 = *((int *)__cil_tmp98);
#line 75
    outb((unsigned char)3, __cil_tmp99);
    }
    {
#line 75
    __cil_tmp100 = (unsigned long )pi;
#line 75
    __cil_tmp101 = __cil_tmp100 + 16;
#line 75
    if (*((int *)__cil_tmp101)) {
      {
#line 75
      __cil_tmp102 = (unsigned long )pi;
#line 75
      __cil_tmp103 = __cil_tmp102 + 16;
#line 75
      __cil_tmp104 = *((int *)__cil_tmp103);
#line 75
      __cil_tmp105 = (unsigned long )__cil_tmp104;
#line 75
      __udelay(__cil_tmp105);
      }
    } else {

    }
    }
    {
#line 75
    __cil_tmp106 = (unsigned long )pi;
#line 75
    __cil_tmp107 = __cil_tmp106 + 16;
#line 75
    if (*((int *)__cil_tmp107)) {
      {
#line 75
      __cil_tmp108 = (unsigned long )pi;
#line 75
      __cil_tmp109 = __cil_tmp108 + 16;
#line 75
      __cil_tmp110 = *((int *)__cil_tmp109);
#line 75
      __cil_tmp111 = (unsigned long )__cil_tmp110;
#line 75
      __udelay(__cil_tmp111);
      }
    } else {

    }
    }
    {
#line 75
    __cil_tmp112 = (unsigned long )pi;
#line 75
    __cil_tmp113 = __cil_tmp112 + 8;
#line 75
    __cil_tmp114 = *((int *)__cil_tmp113);
#line 75
    __cil_tmp115 = __cil_tmp114 + 1;
#line 75
    tmp___1 = inb(__cil_tmp115);
#line 75
    __cil_tmp116 = (int )tmp___1;
#line 75
    c = __cil_tmp116 & 255;
#line 75
    __cil_tmp117 = (unsigned long )pi;
#line 75
    __cil_tmp118 = __cil_tmp117 + 8;
#line 75
    __cil_tmp119 = *((int *)__cil_tmp118);
#line 75
    outb((unsigned char)2, __cil_tmp119);
    }
    {
#line 75
    __cil_tmp120 = (unsigned long )pi;
#line 75
    __cil_tmp121 = __cil_tmp120 + 16;
#line 75
    if (*((int *)__cil_tmp121)) {
      {
#line 75
      __cil_tmp122 = (unsigned long )pi;
#line 75
      __cil_tmp123 = __cil_tmp122 + 16;
#line 75
      __cil_tmp124 = *((int *)__cil_tmp123);
#line 75
      __cil_tmp125 = (unsigned long )__cil_tmp124;
#line 75
      __udelay(__cil_tmp125);
      }
    } else {

    }
    }
    {
#line 75
    __cil_tmp126 = (unsigned long )pi;
#line 75
    __cil_tmp127 = __cil_tmp126 + 16;
#line 75
    if (*((int *)__cil_tmp127)) {
      {
#line 75
      __cil_tmp128 = (unsigned long )pi;
#line 75
      __cil_tmp129 = __cil_tmp128 + 16;
#line 75
      __cil_tmp130 = *((int *)__cil_tmp129);
#line 75
      __cil_tmp131 = (unsigned long )__cil_tmp130;
#line 75
      __udelay(__cil_tmp131);
      }
    } else {

    }
    }
    {
#line 75
    __cil_tmp132 = (unsigned long )pi;
#line 75
    __cil_tmp133 = __cil_tmp132 + 8;
#line 75
    __cil_tmp134 = *((int *)__cil_tmp133);
#line 75
    __cil_tmp135 = __cil_tmp134 + 1;
#line 75
    tmp___2 = inb(__cil_tmp135);
#line 75
    __cil_tmp136 = (int )tmp___2;
#line 75
    d = __cil_tmp136 & 255;
#line 76
    __cil_tmp137 = 4 * k;
#line 76
    __cil_tmp138 = buf + __cil_tmp137;
#line 76
    __cil_tmp139 = b & 240;
#line 76
    __cil_tmp140 = a >> 4;
#line 76
    __cil_tmp141 = __cil_tmp140 & 15;
#line 76
    __cil_tmp142 = __cil_tmp141 | __cil_tmp139;
#line 76
    *__cil_tmp138 = (char )__cil_tmp142;
#line 77
    __cil_tmp143 = 4 * k;
#line 77
    __cil_tmp144 = __cil_tmp143 + 1;
#line 77
    __cil_tmp145 = buf + __cil_tmp144;
#line 77
    __cil_tmp146 = c & 240;
#line 77
    __cil_tmp147 = d >> 4;
#line 77
    __cil_tmp148 = __cil_tmp147 & 15;
#line 77
    __cil_tmp149 = __cil_tmp148 | __cil_tmp146;
#line 77
    *__cil_tmp145 = (char )__cil_tmp149;
#line 79
    __cil_tmp150 = (unsigned long )pi;
#line 79
    __cil_tmp151 = __cil_tmp150 + 8;
#line 79
    __cil_tmp152 = *((int *)__cil_tmp151);
#line 79
    __cil_tmp153 = __cil_tmp152 + 2;
#line 79
    outb((unsigned char)4, __cil_tmp153);
    }
    {
#line 79
    __cil_tmp154 = (unsigned long )pi;
#line 79
    __cil_tmp155 = __cil_tmp154 + 16;
#line 79
    if (*((int *)__cil_tmp155)) {
      {
#line 79
      __cil_tmp156 = (unsigned long )pi;
#line 79
      __cil_tmp157 = __cil_tmp156 + 16;
#line 79
      __cil_tmp158 = *((int *)__cil_tmp157);
#line 79
      __cil_tmp159 = (unsigned long )__cil_tmp158;
#line 79
      __udelay(__cil_tmp159);
      }
    } else {

    }
    }
    {
#line 79
    __cil_tmp160 = (unsigned long )pi;
#line 79
    __cil_tmp161 = __cil_tmp160 + 8;
#line 79
    __cil_tmp162 = *((int *)__cil_tmp161);
#line 79
    __cil_tmp163 = __cil_tmp162 + 2;
#line 79
    outb((unsigned char)5, __cil_tmp163);
    }
    {
#line 79
    __cil_tmp164 = (unsigned long )pi;
#line 79
    __cil_tmp165 = __cil_tmp164 + 16;
#line 79
    if (*((int *)__cil_tmp165)) {
      {
#line 79
      __cil_tmp166 = (unsigned long )pi;
#line 79
      __cil_tmp167 = __cil_tmp166 + 16;
#line 79
      __cil_tmp168 = *((int *)__cil_tmp167);
#line 79
      __cil_tmp169 = (unsigned long )__cil_tmp168;
#line 79
      __udelay(__cil_tmp169);
      }
    } else {

    }
    }
    {
#line 80
    __cil_tmp170 = (unsigned long )pi;
#line 80
    __cil_tmp171 = __cil_tmp170 + 16;
#line 80
    if (*((int *)__cil_tmp171)) {
      {
#line 80
      __cil_tmp172 = (unsigned long )pi;
#line 80
      __cil_tmp173 = __cil_tmp172 + 16;
#line 80
      __cil_tmp174 = *((int *)__cil_tmp173);
#line 80
      __cil_tmp175 = (unsigned long )__cil_tmp174;
#line 80
      __udelay(__cil_tmp175);
      }
    } else {

    }
    }
    {
#line 80
    __cil_tmp176 = (unsigned long )pi;
#line 80
    __cil_tmp177 = __cil_tmp176 + 8;
#line 80
    __cil_tmp178 = *((int *)__cil_tmp177);
#line 80
    __cil_tmp179 = __cil_tmp178 + 1;
#line 80
    tmp___3 = inb(__cil_tmp179);
#line 80
    __cil_tmp180 = (int )tmp___3;
#line 80
    a = __cil_tmp180 & 255;
#line 80
    __cil_tmp181 = (unsigned long )pi;
#line 80
    __cil_tmp182 = __cil_tmp181 + 8;
#line 80
    __cil_tmp183 = *((int *)__cil_tmp182);
#line 80
    outb((unsigned char)3, __cil_tmp183);
    }
    {
#line 80
    __cil_tmp184 = (unsigned long )pi;
#line 80
    __cil_tmp185 = __cil_tmp184 + 16;
#line 80
    if (*((int *)__cil_tmp185)) {
      {
#line 80
      __cil_tmp186 = (unsigned long )pi;
#line 80
      __cil_tmp187 = __cil_tmp186 + 16;
#line 80
      __cil_tmp188 = *((int *)__cil_tmp187);
#line 80
      __cil_tmp189 = (unsigned long )__cil_tmp188;
#line 80
      __udelay(__cil_tmp189);
      }
    } else {

    }
    }
    {
#line 80
    __cil_tmp190 = (unsigned long )pi;
#line 80
    __cil_tmp191 = __cil_tmp190 + 16;
#line 80
    if (*((int *)__cil_tmp191)) {
      {
#line 80
      __cil_tmp192 = (unsigned long )pi;
#line 80
      __cil_tmp193 = __cil_tmp192 + 16;
#line 80
      __cil_tmp194 = *((int *)__cil_tmp193);
#line 80
      __cil_tmp195 = (unsigned long )__cil_tmp194;
#line 80
      __udelay(__cil_tmp195);
      }
    } else {

    }
    }
    {
#line 80
    __cil_tmp196 = (unsigned long )pi;
#line 80
    __cil_tmp197 = __cil_tmp196 + 8;
#line 80
    __cil_tmp198 = *((int *)__cil_tmp197);
#line 80
    __cil_tmp199 = __cil_tmp198 + 1;
#line 80
    tmp___4 = inb(__cil_tmp199);
#line 80
    __cil_tmp200 = (int )tmp___4;
#line 80
    b = __cil_tmp200 & 255;
#line 81
    __cil_tmp201 = (unsigned long )pi;
#line 81
    __cil_tmp202 = __cil_tmp201 + 8;
#line 81
    __cil_tmp203 = *((int *)__cil_tmp202);
#line 81
    outb((unsigned char)1, __cil_tmp203);
    }
    {
#line 81
    __cil_tmp204 = (unsigned long )pi;
#line 81
    __cil_tmp205 = __cil_tmp204 + 16;
#line 81
    if (*((int *)__cil_tmp205)) {
      {
#line 81
      __cil_tmp206 = (unsigned long )pi;
#line 81
      __cil_tmp207 = __cil_tmp206 + 16;
#line 81
      __cil_tmp208 = *((int *)__cil_tmp207);
#line 81
      __cil_tmp209 = (unsigned long )__cil_tmp208;
#line 81
      __udelay(__cil_tmp209);
      }
    } else {

    }
    }
    {
#line 81
    __cil_tmp210 = (unsigned long )pi;
#line 81
    __cil_tmp211 = __cil_tmp210 + 16;
#line 81
    if (*((int *)__cil_tmp211)) {
      {
#line 81
      __cil_tmp212 = (unsigned long )pi;
#line 81
      __cil_tmp213 = __cil_tmp212 + 16;
#line 81
      __cil_tmp214 = *((int *)__cil_tmp213);
#line 81
      __cil_tmp215 = (unsigned long )__cil_tmp214;
#line 81
      __udelay(__cil_tmp215);
      }
    } else {

    }
    }
    {
#line 81
    __cil_tmp216 = (unsigned long )pi;
#line 81
    __cil_tmp217 = __cil_tmp216 + 8;
#line 81
    __cil_tmp218 = *((int *)__cil_tmp217);
#line 81
    __cil_tmp219 = __cil_tmp218 + 1;
#line 81
    tmp___5 = inb(__cil_tmp219);
#line 81
    __cil_tmp220 = (int )tmp___5;
#line 81
    c = __cil_tmp220 & 255;
#line 81
    __cil_tmp221 = (unsigned long )pi;
#line 81
    __cil_tmp222 = __cil_tmp221 + 8;
#line 81
    __cil_tmp223 = *((int *)__cil_tmp222);
#line 81
    outb((unsigned char)0, __cil_tmp223);
    }
    {
#line 81
    __cil_tmp224 = (unsigned long )pi;
#line 81
    __cil_tmp225 = __cil_tmp224 + 16;
#line 81
    if (*((int *)__cil_tmp225)) {
      {
#line 81
      __cil_tmp226 = (unsigned long )pi;
#line 81
      __cil_tmp227 = __cil_tmp226 + 16;
#line 81
      __cil_tmp228 = *((int *)__cil_tmp227);
#line 81
      __cil_tmp229 = (unsigned long )__cil_tmp228;
#line 81
      __udelay(__cil_tmp229);
      }
    } else {

    }
    }
    {
#line 81
    __cil_tmp230 = (unsigned long )pi;
#line 81
    __cil_tmp231 = __cil_tmp230 + 16;
#line 81
    if (*((int *)__cil_tmp231)) {
      {
#line 81
      __cil_tmp232 = (unsigned long )pi;
#line 81
      __cil_tmp233 = __cil_tmp232 + 16;
#line 81
      __cil_tmp234 = *((int *)__cil_tmp233);
#line 81
      __cil_tmp235 = (unsigned long )__cil_tmp234;
#line 81
      __udelay(__cil_tmp235);
      }
    } else {

    }
    }
    {
#line 81
    __cil_tmp236 = (unsigned long )pi;
#line 81
    __cil_tmp237 = __cil_tmp236 + 8;
#line 81
    __cil_tmp238 = *((int *)__cil_tmp237);
#line 81
    __cil_tmp239 = __cil_tmp238 + 1;
#line 81
    tmp___6 = inb(__cil_tmp239);
#line 81
    __cil_tmp240 = (int )tmp___6;
#line 81
    d = __cil_tmp240 & 255;
#line 82
    __cil_tmp241 = 4 * k;
#line 82
    __cil_tmp242 = __cil_tmp241 + 2;
#line 82
    __cil_tmp243 = buf + __cil_tmp242;
#line 82
    __cil_tmp244 = c & 240;
#line 82
    __cil_tmp245 = d >> 4;
#line 82
    __cil_tmp246 = __cil_tmp245 & 15;
#line 82
    __cil_tmp247 = __cil_tmp246 | __cil_tmp244;
#line 82
    *__cil_tmp243 = (char )__cil_tmp247;
#line 83
    __cil_tmp248 = 4 * k;
#line 83
    __cil_tmp249 = __cil_tmp248 + 3;
#line 83
    __cil_tmp250 = buf + __cil_tmp249;
#line 83
    __cil_tmp251 = b & 240;
#line 83
    __cil_tmp252 = a >> 4;
#line 83
    __cil_tmp253 = __cil_tmp252 & 15;
#line 83
    __cil_tmp254 = __cil_tmp253 | __cil_tmp251;
#line 83
    *__cil_tmp250 = (char )__cil_tmp254;
#line 71
    k = k + 1;
    }
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 87
  __cil_tmp255 = (unsigned long )pi;
#line 87
  __cil_tmp256 = __cil_tmp255 + 8;
#line 87
  __cil_tmp257 = *((int *)__cil_tmp256);
#line 87
  __cil_tmp258 = __cil_tmp257 + 2;
#line 87
  outb((unsigned char)4, __cil_tmp258);
  }
  {
#line 87
  __cil_tmp259 = (unsigned long )pi;
#line 87
  __cil_tmp260 = __cil_tmp259 + 16;
#line 87
  if (*((int *)__cil_tmp260)) {
    {
#line 87
    __cil_tmp261 = (unsigned long )pi;
#line 87
    __cil_tmp262 = __cil_tmp261 + 16;
#line 87
    __cil_tmp263 = *((int *)__cil_tmp262);
#line 87
    __cil_tmp264 = (unsigned long )__cil_tmp263;
#line 87
    __udelay(__cil_tmp264);
    }
  } else {

  }
  }
#line 89
  return;
}
}
#line 91 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
static void fit2_write_block(PIA *pi , char *buf , int count ) 
{ int k ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  int __cil_tmp7 ;
  int __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  int __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  int __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  int __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  int __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  int __cil_tmp27 ;
  int __cil_tmp28 ;
  unsigned long __cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  int __cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  int __cil_tmp35 ;
  char *__cil_tmp36 ;
  char __cil_tmp37 ;
  unsigned char __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  int __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  int __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  unsigned long __cil_tmp49 ;
  int __cil_tmp50 ;
  int __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  unsigned long __cil_tmp55 ;
  int __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  int __cil_tmp58 ;
  int __cil_tmp59 ;
  char *__cil_tmp60 ;
  char __cil_tmp61 ;
  unsigned char __cil_tmp62 ;
  unsigned long __cil_tmp63 ;
  unsigned long __cil_tmp64 ;
  int __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  unsigned long __cil_tmp68 ;
  unsigned long __cil_tmp69 ;
  int __cil_tmp70 ;
  unsigned long __cil_tmp71 ;
  unsigned long __cil_tmp72 ;
  unsigned long __cil_tmp73 ;
  int __cil_tmp74 ;
  int __cil_tmp75 ;
  unsigned long __cil_tmp76 ;
  unsigned long __cil_tmp77 ;
  unsigned long __cil_tmp78 ;
  unsigned long __cil_tmp79 ;
  int __cil_tmp80 ;
  unsigned long __cil_tmp81 ;

  {
  {
#line 96
  __cil_tmp5 = (unsigned long )pi;
#line 96
  __cil_tmp6 = __cil_tmp5 + 8;
#line 96
  __cil_tmp7 = *((int *)__cil_tmp6);
#line 96
  __cil_tmp8 = __cil_tmp7 + 2;
#line 96
  outb((unsigned char)12, __cil_tmp8);
  }
  {
#line 96
  __cil_tmp9 = (unsigned long )pi;
#line 96
  __cil_tmp10 = __cil_tmp9 + 16;
#line 96
  if (*((int *)__cil_tmp10)) {
    {
#line 96
    __cil_tmp11 = (unsigned long )pi;
#line 96
    __cil_tmp12 = __cil_tmp11 + 16;
#line 96
    __cil_tmp13 = *((int *)__cil_tmp12);
#line 96
    __cil_tmp14 = (unsigned long )__cil_tmp13;
#line 96
    __udelay(__cil_tmp14);
    }
  } else {

  }
  }
  {
#line 96
  __cil_tmp15 = (unsigned long )pi;
#line 96
  __cil_tmp16 = __cil_tmp15 + 8;
#line 96
  __cil_tmp17 = *((int *)__cil_tmp16);
#line 96
  outb((unsigned char)0, __cil_tmp17);
  }
  {
#line 96
  __cil_tmp18 = (unsigned long )pi;
#line 96
  __cil_tmp19 = __cil_tmp18 + 16;
#line 96
  if (*((int *)__cil_tmp19)) {
    {
#line 96
    __cil_tmp20 = (unsigned long )pi;
#line 96
    __cil_tmp21 = __cil_tmp20 + 16;
#line 96
    __cil_tmp22 = *((int *)__cil_tmp21);
#line 96
    __cil_tmp23 = (unsigned long )__cil_tmp22;
#line 96
    __udelay(__cil_tmp23);
    }
  } else {

  }
  }
#line 97
  k = 0;
  {
#line 97
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 97
    __cil_tmp24 = count / 2;
#line 97
    if (k < __cil_tmp24) {

    } else {
#line 97
      goto while_break;
    }
    }
    {
#line 98
    __cil_tmp25 = (unsigned long )pi;
#line 98
    __cil_tmp26 = __cil_tmp25 + 8;
#line 98
    __cil_tmp27 = *((int *)__cil_tmp26);
#line 98
    __cil_tmp28 = __cil_tmp27 + 2;
#line 98
    outb((unsigned char)4, __cil_tmp28);
    }
    {
#line 98
    __cil_tmp29 = (unsigned long )pi;
#line 98
    __cil_tmp30 = __cil_tmp29 + 16;
#line 98
    if (*((int *)__cil_tmp30)) {
      {
#line 98
      __cil_tmp31 = (unsigned long )pi;
#line 98
      __cil_tmp32 = __cil_tmp31 + 16;
#line 98
      __cil_tmp33 = *((int *)__cil_tmp32);
#line 98
      __cil_tmp34 = (unsigned long )__cil_tmp33;
#line 98
      __udelay(__cil_tmp34);
      }
    } else {

    }
    }
    {
#line 98
    __cil_tmp35 = 2 * k;
#line 98
    __cil_tmp36 = buf + __cil_tmp35;
#line 98
    __cil_tmp37 = *__cil_tmp36;
#line 98
    __cil_tmp38 = (unsigned char )__cil_tmp37;
#line 98
    __cil_tmp39 = (unsigned long )pi;
#line 98
    __cil_tmp40 = __cil_tmp39 + 8;
#line 98
    __cil_tmp41 = *((int *)__cil_tmp40);
#line 98
    outb(__cil_tmp38, __cil_tmp41);
    }
    {
#line 98
    __cil_tmp42 = (unsigned long )pi;
#line 98
    __cil_tmp43 = __cil_tmp42 + 16;
#line 98
    if (*((int *)__cil_tmp43)) {
      {
#line 98
      __cil_tmp44 = (unsigned long )pi;
#line 98
      __cil_tmp45 = __cil_tmp44 + 16;
#line 98
      __cil_tmp46 = *((int *)__cil_tmp45);
#line 98
      __cil_tmp47 = (unsigned long )__cil_tmp46;
#line 98
      __udelay(__cil_tmp47);
      }
    } else {

    }
    }
    {
#line 99
    __cil_tmp48 = (unsigned long )pi;
#line 99
    __cil_tmp49 = __cil_tmp48 + 8;
#line 99
    __cil_tmp50 = *((int *)__cil_tmp49);
#line 99
    __cil_tmp51 = __cil_tmp50 + 2;
#line 99
    outb((unsigned char)5, __cil_tmp51);
    }
    {
#line 99
    __cil_tmp52 = (unsigned long )pi;
#line 99
    __cil_tmp53 = __cil_tmp52 + 16;
#line 99
    if (*((int *)__cil_tmp53)) {
      {
#line 99
      __cil_tmp54 = (unsigned long )pi;
#line 99
      __cil_tmp55 = __cil_tmp54 + 16;
#line 99
      __cil_tmp56 = *((int *)__cil_tmp55);
#line 99
      __cil_tmp57 = (unsigned long )__cil_tmp56;
#line 99
      __udelay(__cil_tmp57);
      }
    } else {

    }
    }
    {
#line 99
    __cil_tmp58 = 2 * k;
#line 99
    __cil_tmp59 = __cil_tmp58 + 1;
#line 99
    __cil_tmp60 = buf + __cil_tmp59;
#line 99
    __cil_tmp61 = *__cil_tmp60;
#line 99
    __cil_tmp62 = (unsigned char )__cil_tmp61;
#line 99
    __cil_tmp63 = (unsigned long )pi;
#line 99
    __cil_tmp64 = __cil_tmp63 + 8;
#line 99
    __cil_tmp65 = *((int *)__cil_tmp64);
#line 99
    outb(__cil_tmp62, __cil_tmp65);
    }
    {
#line 99
    __cil_tmp66 = (unsigned long )pi;
#line 99
    __cil_tmp67 = __cil_tmp66 + 16;
#line 99
    if (*((int *)__cil_tmp67)) {
      {
#line 99
      __cil_tmp68 = (unsigned long )pi;
#line 99
      __cil_tmp69 = __cil_tmp68 + 16;
#line 99
      __cil_tmp70 = *((int *)__cil_tmp69);
#line 99
      __cil_tmp71 = (unsigned long )__cil_tmp70;
#line 99
      __udelay(__cil_tmp71);
      }
    } else {

    }
    }
#line 97
    k = k + 1;
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 101
  __cil_tmp72 = (unsigned long )pi;
#line 101
  __cil_tmp73 = __cil_tmp72 + 8;
#line 101
  __cil_tmp74 = *((int *)__cil_tmp73);
#line 101
  __cil_tmp75 = __cil_tmp74 + 2;
#line 101
  outb((unsigned char)4, __cil_tmp75);
  }
  {
#line 101
  __cil_tmp76 = (unsigned long )pi;
#line 101
  __cil_tmp77 = __cil_tmp76 + 16;
#line 101
  if (*((int *)__cil_tmp77)) {
    {
#line 101
    __cil_tmp78 = (unsigned long )pi;
#line 101
    __cil_tmp79 = __cil_tmp78 + 16;
#line 101
    __cil_tmp80 = *((int *)__cil_tmp79);
#line 101
    __cil_tmp81 = (unsigned long )__cil_tmp80;
#line 101
    __udelay(__cil_tmp81);
    }
  } else {

  }
  }
#line 102
  return;
}
}
#line 104 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
static void fit2_connect(PIA *pi ) 
{ unsigned char tmp ;
  unsigned char tmp___0 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  int __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  int __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  int __cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  int __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  int __cil_tmp24 ;
  int __cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  int __cil_tmp28 ;
  unsigned long __cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  int __cil_tmp31 ;
  int __cil_tmp32 ;
  unsigned long __cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  int __cil_tmp37 ;
  unsigned long __cil_tmp38 ;

  {
  {
#line 106
  __cil_tmp4 = (unsigned long )pi;
#line 106
  __cil_tmp5 = __cil_tmp4 + 16;
#line 106
  if (*((int *)__cil_tmp5)) {
    {
#line 106
    __cil_tmp6 = (unsigned long )pi;
#line 106
    __cil_tmp7 = __cil_tmp6 + 16;
#line 106
    __cil_tmp8 = *((int *)__cil_tmp7);
#line 106
    __cil_tmp9 = (unsigned long )__cil_tmp8;
#line 106
    __udelay(__cil_tmp9);
    }
  } else {

  }
  }
  {
#line 106
  __cil_tmp10 = (unsigned long )pi;
#line 106
  __cil_tmp11 = __cil_tmp10 + 8;
#line 106
  __cil_tmp12 = *((int *)__cil_tmp11);
#line 106
  tmp = inb(__cil_tmp12);
#line 106
  __cil_tmp13 = (unsigned long )pi;
#line 106
  __cil_tmp14 = __cil_tmp13 + 36;
#line 106
  __cil_tmp15 = (int )tmp;
#line 106
  *((int *)__cil_tmp14) = __cil_tmp15 & 255;
  }
  {
#line 107
  __cil_tmp16 = (unsigned long )pi;
#line 107
  __cil_tmp17 = __cil_tmp16 + 16;
#line 107
  if (*((int *)__cil_tmp17)) {
    {
#line 107
    __cil_tmp18 = (unsigned long )pi;
#line 107
    __cil_tmp19 = __cil_tmp18 + 16;
#line 107
    __cil_tmp20 = *((int *)__cil_tmp19);
#line 107
    __cil_tmp21 = (unsigned long )__cil_tmp20;
#line 107
    __udelay(__cil_tmp21);
    }
  } else {

  }
  }
  {
#line 107
  __cil_tmp22 = (unsigned long )pi;
#line 107
  __cil_tmp23 = __cil_tmp22 + 8;
#line 107
  __cil_tmp24 = *((int *)__cil_tmp23);
#line 107
  __cil_tmp25 = __cil_tmp24 + 2;
#line 107
  tmp___0 = inb(__cil_tmp25);
#line 107
  __cil_tmp26 = (unsigned long )pi;
#line 107
  __cil_tmp27 = __cil_tmp26 + 40;
#line 107
  __cil_tmp28 = (int )tmp___0;
#line 107
  *((int *)__cil_tmp27) = __cil_tmp28 & 255;
#line 108
  __cil_tmp29 = (unsigned long )pi;
#line 108
  __cil_tmp30 = __cil_tmp29 + 8;
#line 108
  __cil_tmp31 = *((int *)__cil_tmp30);
#line 108
  __cil_tmp32 = __cil_tmp31 + 2;
#line 108
  outb((unsigned char)204, __cil_tmp32);
  }
  {
#line 108
  __cil_tmp33 = (unsigned long )pi;
#line 108
  __cil_tmp34 = __cil_tmp33 + 16;
#line 108
  if (*((int *)__cil_tmp34)) {
    {
#line 108
    __cil_tmp35 = (unsigned long )pi;
#line 108
    __cil_tmp36 = __cil_tmp35 + 16;
#line 108
    __cil_tmp37 = *((int *)__cil_tmp36);
#line 108
    __cil_tmp38 = (unsigned long )__cil_tmp37;
#line 108
    __udelay(__cil_tmp38);
    }
  } else {

  }
  }
#line 109
  return;
}
}
#line 111 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
static void fit2_disconnect(PIA *pi ) 
{ unsigned long __cil_tmp2 ;
  unsigned long __cil_tmp3 ;
  int __cil_tmp4 ;
  unsigned char __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  int __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  int __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  int __cil_tmp17 ;
  unsigned char __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  int __cil_tmp21 ;
  int __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  int __cil_tmp27 ;
  unsigned long __cil_tmp28 ;

  {
  {
#line 113
  __cil_tmp2 = (unsigned long )pi;
#line 113
  __cil_tmp3 = __cil_tmp2 + 36;
#line 113
  __cil_tmp4 = *((int *)__cil_tmp3);
#line 113
  __cil_tmp5 = (unsigned char )__cil_tmp4;
#line 113
  __cil_tmp6 = (unsigned long )pi;
#line 113
  __cil_tmp7 = __cil_tmp6 + 8;
#line 113
  __cil_tmp8 = *((int *)__cil_tmp7);
#line 113
  outb(__cil_tmp5, __cil_tmp8);
  }
  {
#line 113
  __cil_tmp9 = (unsigned long )pi;
#line 113
  __cil_tmp10 = __cil_tmp9 + 16;
#line 113
  if (*((int *)__cil_tmp10)) {
    {
#line 113
    __cil_tmp11 = (unsigned long )pi;
#line 113
    __cil_tmp12 = __cil_tmp11 + 16;
#line 113
    __cil_tmp13 = *((int *)__cil_tmp12);
#line 113
    __cil_tmp14 = (unsigned long )__cil_tmp13;
#line 113
    __udelay(__cil_tmp14);
    }
  } else {

  }
  }
  {
#line 114
  __cil_tmp15 = (unsigned long )pi;
#line 114
  __cil_tmp16 = __cil_tmp15 + 40;
#line 114
  __cil_tmp17 = *((int *)__cil_tmp16);
#line 114
  __cil_tmp18 = (unsigned char )__cil_tmp17;
#line 114
  __cil_tmp19 = (unsigned long )pi;
#line 114
  __cil_tmp20 = __cil_tmp19 + 8;
#line 114
  __cil_tmp21 = *((int *)__cil_tmp20);
#line 114
  __cil_tmp22 = __cil_tmp21 + 2;
#line 114
  outb(__cil_tmp18, __cil_tmp22);
  }
  {
#line 114
  __cil_tmp23 = (unsigned long )pi;
#line 114
  __cil_tmp24 = __cil_tmp23 + 16;
#line 114
  if (*((int *)__cil_tmp24)) {
    {
#line 114
    __cil_tmp25 = (unsigned long )pi;
#line 114
    __cil_tmp26 = __cil_tmp25 + 16;
#line 114
    __cil_tmp27 = *((int *)__cil_tmp26);
#line 114
    __cil_tmp28 = (unsigned long )__cil_tmp27;
#line 114
    __udelay(__cil_tmp28);
    }
  } else {

  }
  }
#line 115
  return;
}
}
#line 117 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
static void fit2_log_adapter(PIA *pi , char *scratch , int verbose ) 
{ unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  char *__cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  int __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  int __cil_tmp12 ;

  {
  {
#line 119
  __cil_tmp4 = (unsigned long )pi;
#line 119
  __cil_tmp5 = __cil_tmp4 + 24;
#line 119
  __cil_tmp6 = *((char **)__cil_tmp5);
#line 119
  __cil_tmp7 = (unsigned long )pi;
#line 119
  __cil_tmp8 = __cil_tmp7 + 8;
#line 119
  __cil_tmp9 = *((int *)__cil_tmp8);
#line 119
  __cil_tmp10 = (unsigned long )pi;
#line 119
  __cil_tmp11 = __cil_tmp10 + 16;
#line 119
  __cil_tmp12 = *((int *)__cil_tmp11);
#line 119
  printk("%s: fit2 %s, FIT 2000 adapter at 0x%x, delay %d\n", __cil_tmp6, "1.0", __cil_tmp9,
         __cil_tmp12);
  }
#line 122
  return;
}
}
#line 124 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
static struct pi_protocol fit2  = 
#line 124
     {{(char )'f', (char )'i', (char )'t', (char )'2', (char )'\000', (char)0, (char)0,
     (char)0}, 0, 1, 2, 1, 1, & fit2_write_regr, & fit2_read_regr, & fit2_write_block,
    & fit2_read_block, & fit2_connect, & fit2_disconnect, (int (*)(PIA * ))0, (int (*)(PIA * ))0,
    (int (*)(PIA * , char * , int  ))0, & fit2_log_adapter, (int (*)(PIA * ))0, (void (*)(PIA * ))0,
    & __this_module};
#line 140
static int fit2_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
#line 140 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
static int fit2_init(void) 
{ int tmp ;

  {
  {
#line 142
  tmp = paride_register(& fit2);
  }
#line 142
  return (tmp);
}
}
#line 145
static void fit2_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
#line 145 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
static void fit2_exit(void) 
{ 

  {
  {
#line 147
  paride_unregister(& fit2);
  }
#line 148
  return;
}
}
#line 150 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
static char const   __mod_license150[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 150
  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
#line 151 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
int init_module(void) 
{ int tmp ;

  {
  {
#line 151
  tmp = fit2_init();
  }
#line 151
  return (tmp);
}
}
#line 152 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
void cleanup_module(void) 
{ 

  {
  {
#line 152
  fit2_exit();
  }
#line 152
  return;
}
}
#line 170
void ldv_check_final_state(void) ;
#line 176
extern void ldv_initialize(void) ;
#line 179
extern int __VERIFIER_nondet_int(void) ;
#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
int LDV_IN_INTERRUPT  ;
#line 185 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
void main(void) 
{ PIA *var_fit2_write_regr_0_p0 ;
  int var_fit2_write_regr_0_p1 ;
  int var_fit2_write_regr_0_p2 ;
  int var_fit2_write_regr_0_p3 ;
  PIA *var_fit2_read_regr_1_p0 ;
  int var_fit2_read_regr_1_p1 ;
  int var_fit2_read_regr_1_p2 ;
  PIA *var_fit2_write_block_3_p0 ;
  char *var_fit2_write_block_3_p1 ;
  int var_fit2_write_block_3_p2 ;
  PIA *var_fit2_read_block_2_p0 ;
  char *var_fit2_read_block_2_p1 ;
  int var_fit2_read_block_2_p2 ;
  PIA *var_fit2_connect_4_p0 ;
  PIA *var_fit2_disconnect_5_p0 ;
  PIA *var_fit2_log_adapter_6_p0 ;
  char *var_fit2_log_adapter_6_p1 ;
  int var_fit2_log_adapter_6_p2 ;
  int tmp ;
  int ldv_s_fit2_pi_protocol ;
  int tmp___0 ;
  int tmp___1 ;
  int __cil_tmp23 ;

  {
  {
#line 270
  LDV_IN_INTERRUPT = 1;
#line 279
  ldv_initialize();
#line 288
  tmp = fit2_init();
  }
#line 288
  if (tmp) {
#line 289
    goto ldv_final;
  } else {

  }
#line 290
  ldv_s_fit2_pi_protocol = 0;
  {
#line 294
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 294
    tmp___1 = __VERIFIER_nondet_int();
    }
#line 294
    if (tmp___1) {

    } else {
      {
#line 294
      __cil_tmp23 = ldv_s_fit2_pi_protocol == 0;
#line 294
      if (! __cil_tmp23) {

      } else {
#line 294
        goto while_break;
      }
      }
    }
    {
#line 298
    tmp___0 = __VERIFIER_nondet_int();
    }
#line 300
    if (tmp___0 == 0) {
#line 300
      goto case_0;
    } else
#line 319
    if (tmp___0 == 1) {
#line 319
      goto case_1;
    } else
#line 338
    if (tmp___0 == 2) {
#line 338
      goto case_2;
    } else
#line 357
    if (tmp___0 == 3) {
#line 357
      goto case_3;
    } else
#line 376
    if (tmp___0 == 4) {
#line 376
      goto case_4;
    } else
#line 395
    if (tmp___0 == 5) {
#line 395
      goto case_5;
    } else
#line 414
    if (tmp___0 == 6) {
#line 414
      goto case_6;
    } else {
      {
#line 433
      goto switch_default;
#line 298
      if (0) {
        case_0: /* CIL Label */ 
#line 303
        if (ldv_s_fit2_pi_protocol == 0) {
          {
#line 311
          fit2_connect(var_fit2_connect_4_p0);
#line 312
          ldv_s_fit2_pi_protocol = ldv_s_fit2_pi_protocol + 1;
          }
        } else {

        }
#line 318
        goto switch_break;
        case_1: /* CIL Label */ 
#line 322
        if (ldv_s_fit2_pi_protocol == 1) {
          {
#line 330
          fit2_disconnect(var_fit2_disconnect_5_p0);
#line 331
          ldv_s_fit2_pi_protocol = 0;
          }
        } else {

        }
#line 337
        goto switch_break;
        case_2: /* CIL Label */ 
        {
#line 349
        fit2_write_regr(var_fit2_write_regr_0_p0, var_fit2_write_regr_0_p1, var_fit2_write_regr_0_p2,
                        var_fit2_write_regr_0_p3);
        }
#line 356
        goto switch_break;
        case_3: /* CIL Label */ 
        {
#line 368
        fit2_read_regr(var_fit2_read_regr_1_p0, var_fit2_read_regr_1_p1, var_fit2_read_regr_1_p2);
        }
#line 375
        goto switch_break;
        case_4: /* CIL Label */ 
        {
#line 387
        fit2_write_block(var_fit2_write_block_3_p0, var_fit2_write_block_3_p1, var_fit2_write_block_3_p2);
        }
#line 394
        goto switch_break;
        case_5: /* CIL Label */ 
        {
#line 406
        fit2_read_block(var_fit2_read_block_2_p0, var_fit2_read_block_2_p1, var_fit2_read_block_2_p2);
        }
#line 413
        goto switch_break;
        case_6: /* CIL Label */ 
        {
#line 425
        fit2_log_adapter(var_fit2_log_adapter_6_p0, var_fit2_log_adapter_6_p1, var_fit2_log_adapter_6_p2);
        }
#line 432
        goto switch_break;
        switch_default: /* CIL Label */ 
#line 433
        goto switch_break;
      } else {
        switch_break: /* CIL Label */ ;
      }
      }
    }
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 448
  fit2_exit();
  }
  ldv_final: 
  {
#line 451
  ldv_check_final_state();
  }
#line 454
  return;
}
}
#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
void ldv_blast_assert(void) 
{ 

  {
  ERROR: 
#line 6
  goto ERROR;
}
}
#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
extern int __VERIFIER_nondet_int(void) ;
#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int ldv_mutex  =    1;
#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 29
  if (ldv_mutex == 1) {

  } else {
    {
#line 29
    ldv_blast_assert();
    }
  }
  {
#line 32
  nondetermined = __VERIFIER_nondet_int();
  }
#line 35
  if (nondetermined) {
#line 38
    ldv_mutex = 2;
#line 40
    return (0);
  } else {
#line 45
    return (-4);
  }
}
}
#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 57
  if (ldv_mutex == 1) {

  } else {
    {
#line 57
    ldv_blast_assert();
    }
  }
  {
#line 60
  nondetermined = __VERIFIER_nondet_int();
  }
#line 63
  if (nondetermined) {
#line 66
    ldv_mutex = 2;
#line 68
    return (0);
  } else {
#line 73
    return (-4);
  }
}
}
#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
{ int atomic_value_after_dec ;

  {
#line 83
  if (ldv_mutex == 1) {

  } else {
    {
#line 83
    ldv_blast_assert();
    }
  }
  {
#line 86
  atomic_value_after_dec = __VERIFIER_nondet_int();
  }
#line 89
  if (atomic_value_after_dec == 0) {
#line 92
    ldv_mutex = 2;
#line 94
    return (1);
  } else {

  }
#line 98
  return (0);
}
}
#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void mutex_lock(struct mutex *lock ) 
{ 

  {
#line 108
  if (ldv_mutex == 1) {

  } else {
    {
#line 108
    ldv_blast_assert();
    }
  }
#line 110
  ldv_mutex = 2;
#line 111
  return;
}
}
#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int mutex_trylock(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 121
  if (ldv_mutex == 1) {

  } else {
    {
#line 121
    ldv_blast_assert();
    }
  }
  {
#line 124
  nondetermined = __VERIFIER_nondet_int();
  }
#line 127
  if (nondetermined) {
#line 130
    ldv_mutex = 2;
#line 132
    return (1);
  } else {
#line 137
    return (0);
  }
}
}
#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void mutex_unlock(struct mutex *lock ) 
{ 

  {
#line 147
  if (ldv_mutex == 2) {

  } else {
    {
#line 147
    ldv_blast_assert();
    }
  }
#line 149
  ldv_mutex = 1;
#line 150
  return;
}
}
#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void ldv_check_final_state(void) 
{ 

  {
#line 156
  if (ldv_mutex == 1) {

  } else {
    {
#line 156
    ldv_blast_assert();
    }
  }
#line 157
  return;
}
}
#line 463 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16802/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/fit2.c.common.c"
long s__builtin_expect(long val , long res ) 
{ 

  {
#line 464
  return (val);
}
}