ClabureDB

1/* Generated by CIL v. 1.3.7 */ 2/* print_CIL_Input is true */ 3 4#line 23 "include/asm-generic/int-ll64.h" 5typedef unsigned short __u16; 6#line 26 "include/asm-generic/int-ll64.h" 7typedef unsigned int __u32; 8#line 30 "include/asm-generic/int-ll64.h" 9typedef unsigned long long __u64; 10#line 45 "include/asm-generic/int-ll64.h" 11typedef short s16; 12#line 46 "include/asm-generic/int-ll64.h" 13typedef unsigned short u16; 14#line 49 "include/asm-generic/int-ll64.h" 15typedef unsigned int u32; 16#line 14 "include/asm-generic/posix_types.h" 17typedef long __kernel_long_t; 18#line 15 "include/asm-generic/posix_types.h" 19typedef unsigned long __kernel_ulong_t; 20#line 75 "include/asm-generic/posix_types.h" 21typedef __kernel_ulong_t __kernel_size_t; 22#line 76 "include/asm-generic/posix_types.h" 23typedef __kernel_long_t __kernel_ssize_t; 24#line 27 "include/linux/types.h" 25typedef unsigned short umode_t; 26#line 63 "include/linux/types.h" 27typedef __kernel_size_t size_t; 28#line 68 "include/linux/types.h" 29typedef __kernel_ssize_t ssize_t; 30#line 219 "include/linux/types.h" 31struct __anonstruct_atomic_t_7 { 32 int counter ; 33}; 34#line 219 "include/linux/types.h" 35typedef struct __anonstruct_atomic_t_7 atomic_t; 36#line 229 "include/linux/types.h" 37struct list_head { 38 struct list_head *next ; 39 struct list_head *prev ; 40}; 41#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h" 42struct module; 43#line 56 44struct module; 45#line 146 "include/linux/init.h" 46typedef void (*ctor_fn_t)(void); 47#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h" 48struct task_struct; 49#line 20 50struct task_struct; 51#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 52struct task_struct; 53#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h" 54struct task_struct; 55#line 329 56struct arch_spinlock; 57#line 329 58struct arch_spinlock; 59#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h" 60struct task_struct; 61#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h" 62struct task_struct; 63#line 10 "include/asm-generic/bug.h" 64struct bug_entry { 65 int bug_addr_disp ; 66 int file_disp ; 67 unsigned short line ; 68 unsigned short flags ; 69}; 70#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h" 71struct static_key; 72#line 234 73struct static_key; 74#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 75typedef u16 __ticket_t; 76#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 77typedef u32 __ticketpair_t; 78#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 79struct __raw_tickets { 80 __ticket_t head ; 81 __ticket_t tail ; 82}; 83#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 84union __anonunion____missing_field_name_36 { 85 __ticketpair_t head_tail ; 86 struct __raw_tickets tickets ; 87}; 88#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 89struct arch_spinlock { 90 union __anonunion____missing_field_name_36 __annonCompField17 ; 91}; 92#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 93typedef struct arch_spinlock arch_spinlock_t; 94#line 12 "include/linux/lockdep.h" 95struct task_struct; 96#line 20 "include/linux/spinlock_types.h" 97struct raw_spinlock { 98 arch_spinlock_t raw_lock ; 99 unsigned int magic ; 100 unsigned int owner_cpu ; 101 void *owner ; 102}; 103#line 64 "include/linux/spinlock_types.h" 104union __anonunion____missing_field_name_39 { 105 struct raw_spinlock rlock ; 106}; 107#line 64 "include/linux/spinlock_types.h" 108struct spinlock { 109 union __anonunion____missing_field_name_39 __annonCompField19 ; 110}; 111#line 64 "include/linux/spinlock_types.h" 112typedef struct spinlock spinlock_t; 113#line 49 "include/linux/wait.h" 114struct __wait_queue_head { 115 spinlock_t lock ; 116 struct list_head task_list ; 117}; 118#line 53 "include/linux/wait.h" 119typedef struct __wait_queue_head wait_queue_head_t; 120#line 55 121struct task_struct; 122#line 48 "include/linux/mutex.h" 123struct mutex { 124 atomic_t count ; 125 spinlock_t wait_lock ; 126 struct list_head wait_list ; 127 struct task_struct *owner ; 128 char const *name ; 129 void *magic ; 130}; 131#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h" 132struct task_struct; 133#line 18 "include/linux/elf.h" 134typedef __u64 Elf64_Addr; 135#line 19 "include/linux/elf.h" 136typedef __u16 Elf64_Half; 137#line 23 "include/linux/elf.h" 138typedef __u32 Elf64_Word; 139#line 24 "include/linux/elf.h" 140typedef __u64 Elf64_Xword; 141#line 194 "include/linux/elf.h" 142struct elf64_sym { 143 Elf64_Word st_name ; 144 unsigned char st_info ; 145 unsigned char st_other ; 146 Elf64_Half st_shndx ; 147 Elf64_Addr st_value ; 148 Elf64_Xword st_size ; 149}; 150#line 194 "include/linux/elf.h" 151typedef struct elf64_sym Elf64_Sym; 152#line 20 "include/linux/kobject_ns.h" 153struct sock; 154#line 20 155struct sock; 156#line 21 157struct kobject; 158#line 21 159struct kobject; 160#line 27 161enum kobj_ns_type { 162 KOBJ_NS_TYPE_NONE = 0, 163 KOBJ_NS_TYPE_NET = 1, 164 KOBJ_NS_TYPES = 2 165} ; 166#line 40 "include/linux/kobject_ns.h" 167struct kobj_ns_type_operations { 168 enum kobj_ns_type type ; 169 void *(*grab_current_ns)(void) ; 170 void const *(*netlink_ns)(struct sock *sk ) ; 171 void const *(*initial_ns)(void) ; 172 void (*drop_ns)(void * ) ; 173}; 174#line 22 "include/linux/sysfs.h" 175struct kobject; 176#line 23 177struct module; 178#line 24 179enum kobj_ns_type; 180#line 26 "include/linux/sysfs.h" 181struct attribute { 182 char const *name ; 183 umode_t mode ; 184}; 185#line 112 "include/linux/sysfs.h" 186struct sysfs_ops { 187 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ; 188 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ; 189 void const *(*namespace)(struct kobject * , struct attribute const * ) ; 190}; 191#line 118 192struct sysfs_dirent; 193#line 118 194struct sysfs_dirent; 195#line 22 "include/linux/kref.h" 196struct kref { 197 atomic_t refcount ; 198}; 199#line 60 "include/linux/kobject.h" 200struct kset; 201#line 60 202struct kobj_type; 203#line 60 "include/linux/kobject.h" 204struct kobject { 205 char const *name ; 206 struct list_head entry ; 207 struct kobject *parent ; 208 struct kset *kset ; 209 struct kobj_type *ktype ; 210 struct sysfs_dirent *sd ; 211 struct kref kref ; 212 unsigned int state_initialized : 1 ; 213 unsigned int state_in_sysfs : 1 ; 214 unsigned int state_add_uevent_sent : 1 ; 215 unsigned int state_remove_uevent_sent : 1 ; 216 unsigned int uevent_suppress : 1 ; 217}; 218#line 108 "include/linux/kobject.h" 219struct kobj_type { 220 void (*release)(struct kobject *kobj ) ; 221 struct sysfs_ops const *sysfs_ops ; 222 struct attribute **default_attrs ; 223 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ; 224 void const *(*namespace)(struct kobject *kobj ) ; 225}; 226#line 116 "include/linux/kobject.h" 227struct kobj_uevent_env { 228 char *envp[32] ; 229 int envp_idx ; 230 char buf[2048] ; 231 int buflen ; 232}; 233#line 123 "include/linux/kobject.h" 234struct kset_uevent_ops { 235 int (* const filter)(struct kset *kset , struct kobject *kobj ) ; 236 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ; 237 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ; 238}; 239#line 140 240struct sock; 241#line 159 "include/linux/kobject.h" 242struct kset { 243 struct list_head list ; 244 spinlock_t list_lock ; 245 struct kobject kobj ; 246 struct kset_uevent_ops const *uevent_ops ; 247}; 248#line 39 "include/linux/moduleparam.h" 249struct kernel_param; 250#line 39 251struct kernel_param; 252#line 41 "include/linux/moduleparam.h" 253struct kernel_param_ops { 254 int (*set)(char const *val , struct kernel_param const *kp ) ; 255 int (*get)(char *buffer , struct kernel_param const *kp ) ; 256 void (*free)(void *arg ) ; 257}; 258#line 50 259struct kparam_string; 260#line 50 261struct kparam_array; 262#line 50 "include/linux/moduleparam.h" 263union __anonunion____missing_field_name_199 { 264 void *arg ; 265 struct kparam_string const *str ; 266 struct kparam_array const *arr ; 267}; 268#line 50 "include/linux/moduleparam.h" 269struct kernel_param { 270 char const *name ; 271 struct kernel_param_ops const *ops ; 272 u16 perm ; 273 s16 level ; 274 union __anonunion____missing_field_name_199 __annonCompField32 ; 275}; 276#line 63 "include/linux/moduleparam.h" 277struct kparam_string { 278 unsigned int maxlen ; 279 char *string ; 280}; 281#line 69 "include/linux/moduleparam.h" 282struct kparam_array { 283 unsigned int max ; 284 unsigned int elemsize ; 285 unsigned int *num ; 286 struct kernel_param_ops const *ops ; 287 void *elem ; 288}; 289#line 445 290struct module; 291#line 80 "include/linux/jump_label.h" 292struct module; 293#line 143 "include/linux/jump_label.h" 294struct static_key { 295 atomic_t enabled ; 296}; 297#line 22 "include/linux/tracepoint.h" 298struct module; 299#line 23 300struct tracepoint; 301#line 23 302struct tracepoint; 303#line 25 "include/linux/tracepoint.h" 304struct tracepoint_func { 305 void *func ; 306 void *data ; 307}; 308#line 30 "include/linux/tracepoint.h" 309struct tracepoint { 310 char const *name ; 311 struct static_key key ; 312 void (*regfunc)(void) ; 313 void (*unregfunc)(void) ; 314 struct tracepoint_func *funcs ; 315}; 316#line 19 "include/linux/export.h" 317struct kernel_symbol { 318 unsigned long value ; 319 char const *name ; 320}; 321#line 8 "include/asm-generic/module.h" 322struct mod_arch_specific { 323 324}; 325#line 35 "include/linux/module.h" 326struct module; 327#line 37 328struct module_param_attrs; 329#line 37 "include/linux/module.h" 330struct module_kobject { 331 struct kobject kobj ; 332 struct module *mod ; 333 struct kobject *drivers_dir ; 334 struct module_param_attrs *mp ; 335}; 336#line 44 "include/linux/module.h" 337struct module_attribute { 338 struct attribute attr ; 339 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ; 340 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * , 341 size_t count ) ; 342 void (*setup)(struct module * , char const * ) ; 343 int (*test)(struct module * ) ; 344 void (*free)(struct module * ) ; 345}; 346#line 71 347struct exception_table_entry; 348#line 71 349struct exception_table_entry; 350#line 199 351enum module_state { 352 MODULE_STATE_LIVE = 0, 353 MODULE_STATE_COMING = 1, 354 MODULE_STATE_GOING = 2 355} ; 356#line 215 "include/linux/module.h" 357struct module_ref { 358 unsigned long incs ; 359 unsigned long decs ; 360} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ; 361#line 220 362struct module_sect_attrs; 363#line 220 364struct module_notes_attrs; 365#line 220 366struct ftrace_event_call; 367#line 220 "include/linux/module.h" 368struct module { 369 enum module_state state ; 370 struct list_head list ; 371 char name[64UL - sizeof(unsigned long )] ; 372 struct module_kobject mkobj ; 373 struct module_attribute *modinfo_attrs ; 374 char const *version ; 375 char const *srcversion ; 376 struct kobject *holders_dir ; 377 struct kernel_symbol const *syms ; 378 unsigned long const *crcs ; 379 unsigned int num_syms ; 380 struct kernel_param *kp ; 381 unsigned int num_kp ; 382 unsigned int num_gpl_syms ; 383 struct kernel_symbol const *gpl_syms ; 384 unsigned long const *gpl_crcs ; 385 struct kernel_symbol const *unused_syms ; 386 unsigned long const *unused_crcs ; 387 unsigned int num_unused_syms ; 388 unsigned int num_unused_gpl_syms ; 389 struct kernel_symbol const *unused_gpl_syms ; 390 unsigned long const *unused_gpl_crcs ; 391 struct kernel_symbol const *gpl_future_syms ; 392 unsigned long const *gpl_future_crcs ; 393 unsigned int num_gpl_future_syms ; 394 unsigned int num_exentries ; 395 struct exception_table_entry *extable ; 396 int (*init)(void) ; 397 void *module_init ; 398 void *module_core ; 399 unsigned int init_size ; 400 unsigned int core_size ; 401 unsigned int init_text_size ; 402 unsigned int core_text_size ; 403 unsigned int init_ro_size ; 404 unsigned int core_ro_size ; 405 struct mod_arch_specific arch ; 406 unsigned int taints ; 407 unsigned int num_bugs ; 408 struct list_head bug_list ; 409 struct bug_entry *bug_table ; 410 Elf64_Sym *symtab ; 411 Elf64_Sym *core_symtab ; 412 unsigned int num_symtab ; 413 unsigned int core_num_syms ; 414 char *strtab ; 415 char *core_strtab ; 416 struct module_sect_attrs *sect_attrs ; 417 struct module_notes_attrs *notes_attrs ; 418 char *args ; 419 void *percpu ; 420 unsigned int percpu_size ; 421 unsigned int num_tracepoints ; 422 struct tracepoint * const *tracepoints_ptrs ; 423 unsigned int num_trace_bprintk_fmt ; 424 char const **trace_bprintk_fmt_start ; 425 struct ftrace_event_call **trace_events ; 426 unsigned int num_trace_events ; 427 struct list_head source_list ; 428 struct list_head target_list ; 429 struct task_struct *waiter ; 430 void (*exit)(void) ; 431 struct module_ref *refptr ; 432 ctor_fn_t *ctors ; 433 unsigned int num_ctors ; 434}; 435#line 36 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h" 436struct pi_protocol; 437#line 36 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h" 438struct pi_adapter { 439 struct pi_protocol *proto ; 440 int port ; 441 int mode ; 442 int delay ; 443 int devtype ; 444 char *device ; 445 int unit ; 446 int saved_r0 ; 447 int saved_r2 ; 448 int reserved ; 449 unsigned long private ; 450 wait_queue_head_t parq ; 451 void *pardev ; 452 char *parname ; 453 int claimed ; 454 void (*claim_cont)(void) ; 455}; 456#line 57 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h" 457typedef struct pi_adapter PIA; 458#line 135 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h" 459struct pi_protocol { 460 char name[8] ; 461 int index ; 462 int max_mode ; 463 int epp_first ; 464 int default_delay ; 465 int max_units ; 466 void (*write_regr)(PIA * , int , int , int ) ; 467 int (*read_regr)(PIA * , int , int ) ; 468 void (*write_block)(PIA * , char * , int ) ; 469 void (*read_block)(PIA * , char * , int ) ; 470 void (*connect)(PIA * ) ; 471 void (*disconnect)(PIA * ) ; 472 int (*test_port)(PIA * ) ; 473 int (*probe_unit)(PIA * ) ; 474 int (*test_proto)(PIA * , char * , int ) ; 475 void (*log_adapter)(PIA * , char * , int ) ; 476 int (*init_proto)(PIA * ) ; 477 void (*release_proto)(PIA * ) ; 478 struct module *owner ; 479}; 480#line 164 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h" 481typedef struct pi_protocol PIP; 482#line 1 "<compiler builtins>" 483long __builtin_expect(long val , long res ) ; 484#line 100 "include/linux/printk.h" 485extern int ( /* format attribute */ printk)(char const *fmt , ...) ; 486#line 152 "include/linux/mutex.h" 487void mutex_lock(struct mutex *lock ) ; 488#line 153 489int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ; 490#line 154 491int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ; 492#line 168 493int mutex_trylock(struct mutex *lock ) ; 494#line 169 495void mutex_unlock(struct mutex *lock ) ; 496#line 170 497int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ; 498#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h" 499__inline static void outb(unsigned char value , int port ) __attribute__((__no_instrument_function__)) ; 500#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h" 501__inline static void outb(unsigned char value , int port ) 502{ 503 504 { 505#line 308 506 __asm__ volatile ("out" 507 "b" 508 " %" 509 "b" 510 "0, %w1": : "a" (value), "Nd" (port)); 511#line 308 512 return; 513} 514} 515#line 308 516__inline static unsigned char inb(int port ) __attribute__((__no_instrument_function__)) ; 517#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h" 518__inline static unsigned char inb(int port ) 519{ unsigned char value ; 520 521 { 522#line 308 523 __asm__ volatile ("in" 524 "b" 525 " %w1, %" 526 "b" 527 "0": "=a" (value): "Nd" (port)); 528#line 308 529 return (value); 530} 531} 532#line 26 "include/linux/export.h" 533extern struct module __this_module ; 534#line 67 "include/linux/module.h" 535int init_module(void) ; 536#line 68 537void cleanup_module(void) ; 538#line 8 "include/asm-generic/delay.h" 539extern void __udelay(unsigned long usecs ) ; 540#line 166 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/block/paride/paride.h" 541extern int paride_register(PIP * ) ; 542#line 167 543extern void paride_unregister(PIP * ) ; 544#line 37 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 545static int cont_map[2] = { 8, 32}; 546#line 39 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 547static void aten_write_regr(PIA *pi , int cont , int regr , int val ) 548{ int r ; 549 unsigned long __cil_tmp6 ; 550 unsigned long __cil_tmp7 ; 551 int __cil_tmp8 ; 552 int __cil_tmp9 ; 553 unsigned char __cil_tmp10 ; 554 unsigned long __cil_tmp11 ; 555 unsigned long __cil_tmp12 ; 556 int __cil_tmp13 ; 557 unsigned long __cil_tmp14 ; 558 unsigned long __cil_tmp15 ; 559 unsigned long __cil_tmp16 ; 560 unsigned long __cil_tmp17 ; 561 int __cil_tmp18 ; 562 unsigned long __cil_tmp19 ; 563 unsigned long __cil_tmp20 ; 564 unsigned long __cil_tmp21 ; 565 int __cil_tmp22 ; 566 int __cil_tmp23 ; 567 unsigned long __cil_tmp24 ; 568 unsigned long __cil_tmp25 ; 569 unsigned long __cil_tmp26 ; 570 unsigned long __cil_tmp27 ; 571 int __cil_tmp28 ; 572 unsigned long __cil_tmp29 ; 573 unsigned long __cil_tmp30 ; 574 unsigned long __cil_tmp31 ; 575 int __cil_tmp32 ; 576 int __cil_tmp33 ; 577 unsigned long __cil_tmp34 ; 578 unsigned long __cil_tmp35 ; 579 unsigned long __cil_tmp36 ; 580 unsigned long __cil_tmp37 ; 581 int __cil_tmp38 ; 582 unsigned long __cil_tmp39 ; 583 unsigned char __cil_tmp40 ; 584 unsigned long __cil_tmp41 ; 585 unsigned long __cil_tmp42 ; 586 int __cil_tmp43 ; 587 unsigned long __cil_tmp44 ; 588 unsigned long __cil_tmp45 ; 589 unsigned long __cil_tmp46 ; 590 unsigned long __cil_tmp47 ; 591 int __cil_tmp48 ; 592 unsigned long __cil_tmp49 ; 593 unsigned long __cil_tmp50 ; 594 unsigned long __cil_tmp51 ; 595 int __cil_tmp52 ; 596 int __cil_tmp53 ; 597 unsigned long __cil_tmp54 ; 598 unsigned long __cil_tmp55 ; 599 unsigned long __cil_tmp56 ; 600 unsigned long __cil_tmp57 ; 601 int __cil_tmp58 ; 602 unsigned long __cil_tmp59 ; 603 unsigned long __cil_tmp60 ; 604 unsigned long __cil_tmp61 ; 605 int __cil_tmp62 ; 606 int __cil_tmp63 ; 607 unsigned long __cil_tmp64 ; 608 unsigned long __cil_tmp65 ; 609 unsigned long __cil_tmp66 ; 610 unsigned long __cil_tmp67 ; 611 int __cil_tmp68 ; 612 unsigned long __cil_tmp69 ; 613 unsigned long __cil_tmp70 ; 614 unsigned long __cil_tmp71 ; 615 int __cil_tmp72 ; 616 int __cil_tmp73 ; 617 unsigned long __cil_tmp74 ; 618 unsigned long __cil_tmp75 ; 619 unsigned long __cil_tmp76 ; 620 unsigned long __cil_tmp77 ; 621 int __cil_tmp78 ; 622 unsigned long __cil_tmp79 ; 623 624 { 625 { 626#line 43 627 __cil_tmp6 = cont * 4UL; 628#line 43 629 __cil_tmp7 = (unsigned long )(cont_map) + __cil_tmp6; 630#line 43 631 __cil_tmp8 = *((int *)__cil_tmp7); 632#line 43 633 __cil_tmp9 = regr + __cil_tmp8; 634#line 43 635 r = __cil_tmp9 + 128; 636#line 45 637 __cil_tmp10 = (unsigned char )r; 638#line 45 639 __cil_tmp11 = (unsigned long )pi; 640#line 45 641 __cil_tmp12 = __cil_tmp11 + 8; 642#line 45 643 __cil_tmp13 = *((int *)__cil_tmp12); 644#line 45 645 outb(__cil_tmp10, __cil_tmp13); 646 } 647 { 648#line 45 649 __cil_tmp14 = (unsigned long )pi; 650#line 45 651 __cil_tmp15 = __cil_tmp14 + 16; 652#line 45 653 if (*((int *)__cil_tmp15)) { 654 { 655#line 45 656 __cil_tmp16 = (unsigned long )pi; 657#line 45 658 __cil_tmp17 = __cil_tmp16 + 16; 659#line 45 660 __cil_tmp18 = *((int *)__cil_tmp17); 661#line 45 662 __cil_tmp19 = (unsigned long )__cil_tmp18; 663#line 45 664 __udelay(__cil_tmp19); 665 } 666 } else { 667 668 } 669 } 670 { 671#line 45 672 __cil_tmp20 = (unsigned long )pi; 673#line 45 674 __cil_tmp21 = __cil_tmp20 + 8; 675#line 45 676 __cil_tmp22 = *((int *)__cil_tmp21); 677#line 45 678 __cil_tmp23 = __cil_tmp22 + 2; 679#line 45 680 outb((unsigned char)14, __cil_tmp23); 681 } 682 { 683#line 45 684 __cil_tmp24 = (unsigned long )pi; 685#line 45 686 __cil_tmp25 = __cil_tmp24 + 16; 687#line 45 688 if (*((int *)__cil_tmp25)) { 689 { 690#line 45 691 __cil_tmp26 = (unsigned long )pi; 692#line 45 693 __cil_tmp27 = __cil_tmp26 + 16; 694#line 45 695 __cil_tmp28 = *((int *)__cil_tmp27); 696#line 45 697 __cil_tmp29 = (unsigned long )__cil_tmp28; 698#line 45 699 __udelay(__cil_tmp29); 700 } 701 } else { 702 703 } 704 } 705 { 706#line 45 707 __cil_tmp30 = (unsigned long )pi; 708#line 45 709 __cil_tmp31 = __cil_tmp30 + 8; 710#line 45 711 __cil_tmp32 = *((int *)__cil_tmp31); 712#line 45 713 __cil_tmp33 = __cil_tmp32 + 2; 714#line 45 715 outb((unsigned char)6, __cil_tmp33); 716 } 717 { 718#line 45 719 __cil_tmp34 = (unsigned long )pi; 720#line 45 721 __cil_tmp35 = __cil_tmp34 + 16; 722#line 45 723 if (*((int *)__cil_tmp35)) { 724 { 725#line 45 726 __cil_tmp36 = (unsigned long )pi; 727#line 45 728 __cil_tmp37 = __cil_tmp36 + 16; 729#line 45 730 __cil_tmp38 = *((int *)__cil_tmp37); 731#line 45 732 __cil_tmp39 = (unsigned long )__cil_tmp38; 733#line 45 734 __udelay(__cil_tmp39); 735 } 736 } else { 737 738 } 739 } 740 { 741#line 45 742 __cil_tmp40 = (unsigned char )val; 743#line 45 744 __cil_tmp41 = (unsigned long )pi; 745#line 45 746 __cil_tmp42 = __cil_tmp41 + 8; 747#line 45 748 __cil_tmp43 = *((int *)__cil_tmp42); 749#line 45 750 outb(__cil_tmp40, __cil_tmp43); 751 } 752 { 753#line 45 754 __cil_tmp44 = (unsigned long )pi; 755#line 45 756 __cil_tmp45 = __cil_tmp44 + 16; 757#line 45 758 if (*((int *)__cil_tmp45)) { 759 { 760#line 45 761 __cil_tmp46 = (unsigned long )pi; 762#line 45 763 __cil_tmp47 = __cil_tmp46 + 16; 764#line 45 765 __cil_tmp48 = *((int *)__cil_tmp47); 766#line 45 767 __cil_tmp49 = (unsigned long )__cil_tmp48; 768#line 45 769 __udelay(__cil_tmp49); 770 } 771 } else { 772 773 } 774 } 775 { 776#line 45 777 __cil_tmp50 = (unsigned long )pi; 778#line 45 779 __cil_tmp51 = __cil_tmp50 + 8; 780#line 45 781 __cil_tmp52 = *((int *)__cil_tmp51); 782#line 45 783 __cil_tmp53 = __cil_tmp52 + 2; 784#line 45 785 outb((unsigned char)7, __cil_tmp53); 786 } 787 { 788#line 45 789 __cil_tmp54 = (unsigned long )pi; 790#line 45 791 __cil_tmp55 = __cil_tmp54 + 16; 792#line 45 793 if (*((int *)__cil_tmp55)) { 794 { 795#line 45 796 __cil_tmp56 = (unsigned long )pi; 797#line 45 798 __cil_tmp57 = __cil_tmp56 + 16; 799#line 45 800 __cil_tmp58 = *((int *)__cil_tmp57); 801#line 45 802 __cil_tmp59 = (unsigned long )__cil_tmp58; 803#line 45 804 __udelay(__cil_tmp59); 805 } 806 } else { 807 808 } 809 } 810 { 811#line 45 812 __cil_tmp60 = (unsigned long )pi; 813#line 45 814 __cil_tmp61 = __cil_tmp60 + 8; 815#line 45 816 __cil_tmp62 = *((int *)__cil_tmp61); 817#line 45 818 __cil_tmp63 = __cil_tmp62 + 2; 819#line 45 820 outb((unsigned char)6, __cil_tmp63); 821 } 822 { 823#line 45 824 __cil_tmp64 = (unsigned long )pi; 825#line 45 826 __cil_tmp65 = __cil_tmp64 + 16; 827#line 45 828 if (*((int *)__cil_tmp65)) { 829 { 830#line 45 831 __cil_tmp66 = (unsigned long )pi; 832#line 45 833 __cil_tmp67 = __cil_tmp66 + 16; 834#line 45 835 __cil_tmp68 = *((int *)__cil_tmp67); 836#line 45 837 __cil_tmp69 = (unsigned long )__cil_tmp68; 838#line 45 839 __udelay(__cil_tmp69); 840 } 841 } else { 842 843 } 844 } 845 { 846#line 45 847 __cil_tmp70 = (unsigned long )pi; 848#line 45 849 __cil_tmp71 = __cil_tmp70 + 8; 850#line 45 851 __cil_tmp72 = *((int *)__cil_tmp71); 852#line 45 853 __cil_tmp73 = __cil_tmp72 + 2; 854#line 45 855 outb((unsigned char)12, __cil_tmp73); 856 } 857 { 858#line 45 859 __cil_tmp74 = (unsigned long )pi; 860#line 45 861 __cil_tmp75 = __cil_tmp74 + 16; 862#line 45 863 if (*((int *)__cil_tmp75)) { 864 { 865#line 45 866 __cil_tmp76 = (unsigned long )pi; 867#line 45 868 __cil_tmp77 = __cil_tmp76 + 16; 869#line 45 870 __cil_tmp78 = *((int *)__cil_tmp77); 871#line 45 872 __cil_tmp79 = (unsigned long )__cil_tmp78; 873#line 45 874 __udelay(__cil_tmp79); 875 } 876 } else { 877 878 } 879 } 880#line 46 881 return; 882} 883} 884#line 48 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 885static int aten_read_regr(PIA *pi , int cont , int regr ) 886{ int a ; 887 int b ; 888 int r ; 889 unsigned char tmp ; 890 unsigned char tmp___0 ; 891 unsigned char tmp___1 ; 892 unsigned long __cil_tmp10 ; 893 unsigned long __cil_tmp11 ; 894 int __cil_tmp12 ; 895 int __cil_tmp13 ; 896 unsigned long __cil_tmp14 ; 897 unsigned long __cil_tmp15 ; 898 unsigned char __cil_tmp16 ; 899 unsigned long __cil_tmp17 ; 900 unsigned long __cil_tmp18 ; 901 int __cil_tmp19 ; 902 unsigned long __cil_tmp20 ; 903 unsigned long __cil_tmp21 ; 904 unsigned long __cil_tmp22 ; 905 unsigned long __cil_tmp23 ; 906 int __cil_tmp24 ; 907 unsigned long __cil_tmp25 ; 908 unsigned long __cil_tmp26 ; 909 unsigned long __cil_tmp27 ; 910 int __cil_tmp28 ; 911 int __cil_tmp29 ; 912 unsigned long __cil_tmp30 ; 913 unsigned long __cil_tmp31 ; 914 unsigned long __cil_tmp32 ; 915 unsigned long __cil_tmp33 ; 916 int __cil_tmp34 ; 917 unsigned long __cil_tmp35 ; 918 unsigned long __cil_tmp36 ; 919 unsigned long __cil_tmp37 ; 920 int __cil_tmp38 ; 921 int __cil_tmp39 ; 922 unsigned long __cil_tmp40 ; 923 unsigned long __cil_tmp41 ; 924 unsigned long __cil_tmp42 ; 925 unsigned long __cil_tmp43 ; 926 int __cil_tmp44 ; 927 unsigned long __cil_tmp45 ; 928 unsigned long __cil_tmp46 ; 929 unsigned long __cil_tmp47 ; 930 int __cil_tmp48 ; 931 int __cil_tmp49 ; 932 unsigned long __cil_tmp50 ; 933 unsigned long __cil_tmp51 ; 934 unsigned long __cil_tmp52 ; 935 unsigned long __cil_tmp53 ; 936 int __cil_tmp54 ; 937 unsigned long __cil_tmp55 ; 938 unsigned long __cil_tmp56 ; 939 unsigned long __cil_tmp57 ; 940 int __cil_tmp58 ; 941 int __cil_tmp59 ; 942 unsigned long __cil_tmp60 ; 943 unsigned long __cil_tmp61 ; 944 unsigned long __cil_tmp62 ; 945 unsigned long __cil_tmp63 ; 946 int __cil_tmp64 ; 947 unsigned long __cil_tmp65 ; 948 unsigned long __cil_tmp66 ; 949 unsigned long __cil_tmp67 ; 950 int __cil_tmp68 ; 951 int __cil_tmp69 ; 952 unsigned long __cil_tmp70 ; 953 unsigned long __cil_tmp71 ; 954 unsigned long __cil_tmp72 ; 955 unsigned long __cil_tmp73 ; 956 int __cil_tmp74 ; 957 unsigned long __cil_tmp75 ; 958 unsigned long __cil_tmp76 ; 959 unsigned long __cil_tmp77 ; 960 unsigned long __cil_tmp78 ; 961 unsigned long __cil_tmp79 ; 962 int __cil_tmp80 ; 963 unsigned long __cil_tmp81 ; 964 unsigned long __cil_tmp82 ; 965 unsigned long __cil_tmp83 ; 966 int __cil_tmp84 ; 967 int __cil_tmp85 ; 968 int __cil_tmp86 ; 969 unsigned long __cil_tmp87 ; 970 unsigned long __cil_tmp88 ; 971 int __cil_tmp89 ; 972 unsigned long __cil_tmp90 ; 973 unsigned long __cil_tmp91 ; 974 unsigned long __cil_tmp92 ; 975 unsigned long __cil_tmp93 ; 976 int __cil_tmp94 ; 977 unsigned long __cil_tmp95 ; 978 unsigned long __cil_tmp96 ; 979 unsigned long __cil_tmp97 ; 980 unsigned long __cil_tmp98 ; 981 unsigned long __cil_tmp99 ; 982 int __cil_tmp100 ; 983 unsigned long __cil_tmp101 ; 984 unsigned long __cil_tmp102 ; 985 unsigned long __cil_tmp103 ; 986 int __cil_tmp104 ; 987 int __cil_tmp105 ; 988 int __cil_tmp106 ; 989 unsigned long __cil_tmp107 ; 990 unsigned long __cil_tmp108 ; 991 int __cil_tmp109 ; 992 int __cil_tmp110 ; 993 unsigned long __cil_tmp111 ; 994 unsigned long __cil_tmp112 ; 995 unsigned long __cil_tmp113 ; 996 unsigned long __cil_tmp114 ; 997 int __cil_tmp115 ; 998 unsigned long __cil_tmp116 ; 999 int __cil_tmp117 ; 1000 int __cil_tmp118 ; 1001 int __cil_tmp119 ; 1002 int __cil_tmp120 ; 1003 unsigned char __cil_tmp121 ; 1004 unsigned long __cil_tmp122 ; 1005 unsigned long __cil_tmp123 ; 1006 int __cil_tmp124 ; 1007 unsigned long __cil_tmp125 ; 1008 unsigned long __cil_tmp126 ; 1009 unsigned long __cil_tmp127 ; 1010 unsigned long __cil_tmp128 ; 1011 int __cil_tmp129 ; 1012 unsigned long __cil_tmp130 ; 1013 unsigned long __cil_tmp131 ; 1014 unsigned long __cil_tmp132 ; 1015 int __cil_tmp133 ; 1016 int __cil_tmp134 ; 1017 unsigned long __cil_tmp135 ; 1018 unsigned long __cil_tmp136 ; 1019 unsigned long __cil_tmp137 ; 1020 unsigned long __cil_tmp138 ; 1021 int __cil_tmp139 ; 1022 unsigned long __cil_tmp140 ; 1023 unsigned long __cil_tmp141 ; 1024 unsigned long __cil_tmp142 ; 1025 int __cil_tmp143 ; 1026 int __cil_tmp144 ; 1027 unsigned long __cil_tmp145 ; 1028 unsigned long __cil_tmp146 ; 1029 unsigned long __cil_tmp147 ; 1030 unsigned long __cil_tmp148 ; 1031 int __cil_tmp149 ; 1032 unsigned long __cil_tmp150 ; 1033 unsigned long __cil_tmp151 ; 1034 unsigned long __cil_tmp152 ; 1035 int __cil_tmp153 ; 1036 unsigned long __cil_tmp154 ; 1037 unsigned long __cil_tmp155 ; 1038 unsigned long __cil_tmp156 ; 1039 unsigned long __cil_tmp157 ; 1040 int __cil_tmp158 ; 1041 unsigned long __cil_tmp159 ; 1042 unsigned long __cil_tmp160 ; 1043 unsigned long __cil_tmp161 ; 1044 int __cil_tmp162 ; 1045 int __cil_tmp163 ; 1046 unsigned long __cil_tmp164 ; 1047 unsigned long __cil_tmp165 ; 1048 unsigned long __cil_tmp166 ; 1049 unsigned long __cil_tmp167 ; 1050 int __cil_tmp168 ; 1051 unsigned long __cil_tmp169 ; 1052 unsigned long __cil_tmp170 ; 1053 unsigned long __cil_tmp171 ; 1054 int __cil_tmp172 ; 1055 int __cil_tmp173 ; 1056 unsigned long __cil_tmp174 ; 1057 unsigned long __cil_tmp175 ; 1058 unsigned long __cil_tmp176 ; 1059 unsigned long __cil_tmp177 ; 1060 int __cil_tmp178 ; 1061 unsigned long __cil_tmp179 ; 1062 unsigned long __cil_tmp180 ; 1063 unsigned long __cil_tmp181 ; 1064 int __cil_tmp182 ; 1065 int __cil_tmp183 ; 1066 unsigned long __cil_tmp184 ; 1067 unsigned long __cil_tmp185 ; 1068 unsigned long __cil_tmp186 ; 1069 unsigned long __cil_tmp187 ; 1070 int __cil_tmp188 ; 1071 unsigned long __cil_tmp189 ; 1072 unsigned long __cil_tmp190 ; 1073 unsigned long __cil_tmp191 ; 1074 unsigned long __cil_tmp192 ; 1075 unsigned long __cil_tmp193 ; 1076 int __cil_tmp194 ; 1077 unsigned long __cil_tmp195 ; 1078 unsigned long __cil_tmp196 ; 1079 unsigned long __cil_tmp197 ; 1080 int __cil_tmp198 ; 1081 int __cil_tmp199 ; 1082 unsigned long __cil_tmp200 ; 1083 unsigned long __cil_tmp201 ; 1084 int __cil_tmp202 ; 1085 int __cil_tmp203 ; 1086 unsigned long __cil_tmp204 ; 1087 unsigned long __cil_tmp205 ; 1088 unsigned long __cil_tmp206 ; 1089 unsigned long __cil_tmp207 ; 1090 int __cil_tmp208 ; 1091 unsigned long __cil_tmp209 ; 1092 unsigned long __cil_tmp210 ; 1093 unsigned long __cil_tmp211 ; 1094 int __cil_tmp212 ; 1095 int __cil_tmp213 ; 1096 unsigned long __cil_tmp214 ; 1097 unsigned long __cil_tmp215 ; 1098 unsigned long __cil_tmp216 ; 1099 unsigned long __cil_tmp217 ; 1100 int __cil_tmp218 ; 1101 unsigned long __cil_tmp219 ; 1102 1103 { 1104#line 52 1105 __cil_tmp10 = cont * 4UL; 1106#line 52 1107 __cil_tmp11 = (unsigned long )(cont_map) + __cil_tmp10; 1108#line 52 1109 __cil_tmp12 = *((int *)__cil_tmp11); 1110#line 52 1111 __cil_tmp13 = regr + __cil_tmp12; 1112#line 52 1113 r = __cil_tmp13 + 64; 1114 { 1115#line 54 1116 __cil_tmp14 = (unsigned long )pi; 1117#line 54 1118 __cil_tmp15 = __cil_tmp14 + 12; 1119#line 56 1120 if (*((int *)__cil_tmp15) == 0) { 1121#line 56 1122 goto case_0; 1123 } else 1124#line 61 1125 if (*((int *)__cil_tmp15) == 1) { 1126#line 61 1127 goto case_1; 1128 } else 1129#line 54 1130 if (0) { 1131 case_0: /* CIL Label */ 1132 { 1133#line 56 1134 __cil_tmp16 = (unsigned char )r; 1135#line 56 1136 __cil_tmp17 = (unsigned long )pi; 1137#line 56 1138 __cil_tmp18 = __cil_tmp17 + 8; 1139#line 56 1140 __cil_tmp19 = *((int *)__cil_tmp18); 1141#line 56 1142 outb(__cil_tmp16, __cil_tmp19); 1143 } 1144 { 1145#line 56 1146 __cil_tmp20 = (unsigned long )pi; 1147#line 56 1148 __cil_tmp21 = __cil_tmp20 + 16; 1149#line 56 1150 if (*((int *)__cil_tmp21)) { 1151 { 1152#line 56 1153 __cil_tmp22 = (unsigned long )pi; 1154#line 56 1155 __cil_tmp23 = __cil_tmp22 + 16; 1156#line 56 1157 __cil_tmp24 = *((int *)__cil_tmp23); 1158#line 56 1159 __cil_tmp25 = (unsigned long )__cil_tmp24; 1160#line 56 1161 __udelay(__cil_tmp25); 1162 } 1163 } else { 1164 1165 } 1166 } 1167 { 1168#line 56 1169 __cil_tmp26 = (unsigned long )pi; 1170#line 56 1171 __cil_tmp27 = __cil_tmp26 + 8; 1172#line 56 1173 __cil_tmp28 = *((int *)__cil_tmp27); 1174#line 56 1175 __cil_tmp29 = __cil_tmp28 + 2; 1176#line 56 1177 outb((unsigned char)14, __cil_tmp29); 1178 } 1179 { 1180#line 56 1181 __cil_tmp30 = (unsigned long )pi; 1182#line 56 1183 __cil_tmp31 = __cil_tmp30 + 16; 1184#line 56 1185 if (*((int *)__cil_tmp31)) { 1186 { 1187#line 56 1188 __cil_tmp32 = (unsigned long )pi; 1189#line 56 1190 __cil_tmp33 = __cil_tmp32 + 16; 1191#line 56 1192 __cil_tmp34 = *((int *)__cil_tmp33); 1193#line 56 1194 __cil_tmp35 = (unsigned long )__cil_tmp34; 1195#line 56 1196 __udelay(__cil_tmp35); 1197 } 1198 } else { 1199 1200 } 1201 } 1202 { 1203#line 56 1204 __cil_tmp36 = (unsigned long )pi; 1205#line 56 1206 __cil_tmp37 = __cil_tmp36 + 8; 1207#line 56 1208 __cil_tmp38 = *((int *)__cil_tmp37); 1209#line 56 1210 __cil_tmp39 = __cil_tmp38 + 2; 1211#line 56 1212 outb((unsigned char)6, __cil_tmp39); 1213 } 1214 { 1215#line 56 1216 __cil_tmp40 = (unsigned long )pi; 1217#line 56 1218 __cil_tmp41 = __cil_tmp40 + 16; 1219#line 56 1220 if (*((int *)__cil_tmp41)) { 1221 { 1222#line 56 1223 __cil_tmp42 = (unsigned long )pi; 1224#line 56 1225 __cil_tmp43 = __cil_tmp42 + 16; 1226#line 56 1227 __cil_tmp44 = *((int *)__cil_tmp43); 1228#line 56 1229 __cil_tmp45 = (unsigned long )__cil_tmp44; 1230#line 56 1231 __udelay(__cil_tmp45); 1232 } 1233 } else { 1234 1235 } 1236 } 1237 { 1238#line 57 1239 __cil_tmp46 = (unsigned long )pi; 1240#line 57 1241 __cil_tmp47 = __cil_tmp46 + 8; 1242#line 57 1243 __cil_tmp48 = *((int *)__cil_tmp47); 1244#line 57 1245 __cil_tmp49 = __cil_tmp48 + 2; 1246#line 57 1247 outb((unsigned char)7, __cil_tmp49); 1248 } 1249 { 1250#line 57 1251 __cil_tmp50 = (unsigned long )pi; 1252#line 57 1253 __cil_tmp51 = __cil_tmp50 + 16; 1254#line 57 1255 if (*((int *)__cil_tmp51)) { 1256 { 1257#line 57 1258 __cil_tmp52 = (unsigned long )pi; 1259#line 57 1260 __cil_tmp53 = __cil_tmp52 + 16; 1261#line 57 1262 __cil_tmp54 = *((int *)__cil_tmp53); 1263#line 57 1264 __cil_tmp55 = (unsigned long )__cil_tmp54; 1265#line 57 1266 __udelay(__cil_tmp55); 1267 } 1268 } else { 1269 1270 } 1271 } 1272 { 1273#line 57 1274 __cil_tmp56 = (unsigned long )pi; 1275#line 57 1276 __cil_tmp57 = __cil_tmp56 + 8; 1277#line 57 1278 __cil_tmp58 = *((int *)__cil_tmp57); 1279#line 57 1280 __cil_tmp59 = __cil_tmp58 + 2; 1281#line 57 1282 outb((unsigned char)6, __cil_tmp59); 1283 } 1284 { 1285#line 57 1286 __cil_tmp60 = (unsigned long )pi; 1287#line 57 1288 __cil_tmp61 = __cil_tmp60 + 16; 1289#line 57 1290 if (*((int *)__cil_tmp61)) { 1291 { 1292#line 57 1293 __cil_tmp62 = (unsigned long )pi; 1294#line 57 1295 __cil_tmp63 = __cil_tmp62 + 16; 1296#line 57 1297 __cil_tmp64 = *((int *)__cil_tmp63); 1298#line 57 1299 __cil_tmp65 = (unsigned long )__cil_tmp64; 1300#line 57 1301 __udelay(__cil_tmp65); 1302 } 1303 } else { 1304 1305 } 1306 } 1307 { 1308#line 57 1309 __cil_tmp66 = (unsigned long )pi; 1310#line 57 1311 __cil_tmp67 = __cil_tmp66 + 8; 1312#line 57 1313 __cil_tmp68 = *((int *)__cil_tmp67); 1314#line 57 1315 __cil_tmp69 = __cil_tmp68 + 2; 1316#line 57 1317 outb((unsigned char)0, __cil_tmp69); 1318 } 1319 { 1320#line 57 1321 __cil_tmp70 = (unsigned long )pi; 1322#line 57 1323 __cil_tmp71 = __cil_tmp70 + 16; 1324#line 57 1325 if (*((int *)__cil_tmp71)) { 1326 { 1327#line 57 1328 __cil_tmp72 = (unsigned long )pi; 1329#line 57 1330 __cil_tmp73 = __cil_tmp72 + 16; 1331#line 57 1332 __cil_tmp74 = *((int *)__cil_tmp73); 1333#line 57 1334 __cil_tmp75 = (unsigned long )__cil_tmp74; 1335#line 57 1336 __udelay(__cil_tmp75); 1337 } 1338 } else { 1339 1340 } 1341 } 1342 { 1343#line 58 1344 __cil_tmp76 = (unsigned long )pi; 1345#line 58 1346 __cil_tmp77 = __cil_tmp76 + 16; 1347#line 58 1348 if (*((int *)__cil_tmp77)) { 1349 { 1350#line 58 1351 __cil_tmp78 = (unsigned long )pi; 1352#line 58 1353 __cil_tmp79 = __cil_tmp78 + 16; 1354#line 58 1355 __cil_tmp80 = *((int *)__cil_tmp79); 1356#line 58 1357 __cil_tmp81 = (unsigned long )__cil_tmp80; 1358#line 58 1359 __udelay(__cil_tmp81); 1360 } 1361 } else { 1362 1363 } 1364 } 1365 { 1366#line 58 1367 __cil_tmp82 = (unsigned long )pi; 1368#line 58 1369 __cil_tmp83 = __cil_tmp82 + 8; 1370#line 58 1371 __cil_tmp84 = *((int *)__cil_tmp83); 1372#line 58 1373 __cil_tmp85 = __cil_tmp84 + 1; 1374#line 58 1375 tmp = inb(__cil_tmp85); 1376#line 58 1377 __cil_tmp86 = (int )tmp; 1378#line 58 1379 a = __cil_tmp86 & 255; 1380#line 58 1381 __cil_tmp87 = (unsigned long )pi; 1382#line 58 1383 __cil_tmp88 = __cil_tmp87 + 8; 1384#line 58 1385 __cil_tmp89 = *((int *)__cil_tmp88); 1386#line 58 1387 outb((unsigned char)16, __cil_tmp89); 1388 } 1389 { 1390#line 58 1391 __cil_tmp90 = (unsigned long )pi; 1392#line 58 1393 __cil_tmp91 = __cil_tmp90 + 16; 1394#line 58 1395 if (*((int *)__cil_tmp91)) { 1396 { 1397#line 58 1398 __cil_tmp92 = (unsigned long )pi; 1399#line 58 1400 __cil_tmp93 = __cil_tmp92 + 16; 1401#line 58 1402 __cil_tmp94 = *((int *)__cil_tmp93); 1403#line 58 1404 __cil_tmp95 = (unsigned long )__cil_tmp94; 1405#line 58 1406 __udelay(__cil_tmp95); 1407 } 1408 } else { 1409 1410 } 1411 } 1412 { 1413#line 58 1414 __cil_tmp96 = (unsigned long )pi; 1415#line 58 1416 __cil_tmp97 = __cil_tmp96 + 16; 1417#line 58 1418 if (*((int *)__cil_tmp97)) { 1419 { 1420#line 58 1421 __cil_tmp98 = (unsigned long )pi; 1422#line 58 1423 __cil_tmp99 = __cil_tmp98 + 16; 1424#line 58 1425 __cil_tmp100 = *((int *)__cil_tmp99); 1426#line 58 1427 __cil_tmp101 = (unsigned long )__cil_tmp100; 1428#line 58 1429 __udelay(__cil_tmp101); 1430 } 1431 } else { 1432 1433 } 1434 } 1435 { 1436#line 58 1437 __cil_tmp102 = (unsigned long )pi; 1438#line 58 1439 __cil_tmp103 = __cil_tmp102 + 8; 1440#line 58 1441 __cil_tmp104 = *((int *)__cil_tmp103); 1442#line 58 1443 __cil_tmp105 = __cil_tmp104 + 1; 1444#line 58 1445 tmp___0 = inb(__cil_tmp105); 1446#line 58 1447 __cil_tmp106 = (int )tmp___0; 1448#line 58 1449 b = __cil_tmp106 & 255; 1450#line 58 1451 __cil_tmp107 = (unsigned long )pi; 1452#line 58 1453 __cil_tmp108 = __cil_tmp107 + 8; 1454#line 58 1455 __cil_tmp109 = *((int *)__cil_tmp108); 1456#line 58 1457 __cil_tmp110 = __cil_tmp109 + 2; 1458#line 58 1459 outb((unsigned char)12, __cil_tmp110); 1460 } 1461 { 1462#line 58 1463 __cil_tmp111 = (unsigned long )pi; 1464#line 58 1465 __cil_tmp112 = __cil_tmp111 + 16; 1466#line 58 1467 if (*((int *)__cil_tmp112)) { 1468 { 1469#line 58 1470 __cil_tmp113 = (unsigned long )pi; 1471#line 58 1472 __cil_tmp114 = __cil_tmp113 + 16; 1473#line 58 1474 __cil_tmp115 = *((int *)__cil_tmp114); 1475#line 58 1476 __cil_tmp116 = (unsigned long )__cil_tmp115; 1477#line 58 1478 __udelay(__cil_tmp116); 1479 } 1480 } else { 1481 1482 } 1483 } 1484 { 1485#line 59 1486 __cil_tmp117 = b & 240; 1487#line 59 1488 __cil_tmp118 = a >> 4; 1489#line 59 1490 __cil_tmp119 = __cil_tmp118 & 15; 1491#line 59 1492 __cil_tmp120 = __cil_tmp119 | __cil_tmp117; 1493#line 59 1494 return (__cil_tmp120 ^ 136); 1495 } 1496 case_1: /* CIL Label */ 1497 { 1498#line 61 1499 r = r | 16; 1500#line 62 1501 __cil_tmp121 = (unsigned char )r; 1502#line 62 1503 __cil_tmp122 = (unsigned long )pi; 1504#line 62 1505 __cil_tmp123 = __cil_tmp122 + 8; 1506#line 62 1507 __cil_tmp124 = *((int *)__cil_tmp123); 1508#line 62 1509 outb(__cil_tmp121, __cil_tmp124); 1510 } 1511 { 1512#line 62 1513 __cil_tmp125 = (unsigned long )pi; 1514#line 62 1515 __cil_tmp126 = __cil_tmp125 + 16; 1516#line 62 1517 if (*((int *)__cil_tmp126)) { 1518 { 1519#line 62 1520 __cil_tmp127 = (unsigned long )pi; 1521#line 62 1522 __cil_tmp128 = __cil_tmp127 + 16; 1523#line 62 1524 __cil_tmp129 = *((int *)__cil_tmp128); 1525#line 62 1526 __cil_tmp130 = (unsigned long )__cil_tmp129; 1527#line 62 1528 __udelay(__cil_tmp130); 1529 } 1530 } else { 1531 1532 } 1533 } 1534 { 1535#line 62 1536 __cil_tmp131 = (unsigned long )pi; 1537#line 62 1538 __cil_tmp132 = __cil_tmp131 + 8; 1539#line 62 1540 __cil_tmp133 = *((int *)__cil_tmp132); 1541#line 62 1542 __cil_tmp134 = __cil_tmp133 + 2; 1543#line 62 1544 outb((unsigned char)14, __cil_tmp134); 1545 } 1546 { 1547#line 62 1548 __cil_tmp135 = (unsigned long )pi; 1549#line 62 1550 __cil_tmp136 = __cil_tmp135 + 16; 1551#line 62 1552 if (*((int *)__cil_tmp136)) { 1553 { 1554#line 62 1555 __cil_tmp137 = (unsigned long )pi; 1556#line 62 1557 __cil_tmp138 = __cil_tmp137 + 16; 1558#line 62 1559 __cil_tmp139 = *((int *)__cil_tmp138); 1560#line 62 1561 __cil_tmp140 = (unsigned long )__cil_tmp139; 1562#line 62 1563 __udelay(__cil_tmp140); 1564 } 1565 } else { 1566 1567 } 1568 } 1569 { 1570#line 62 1571 __cil_tmp141 = (unsigned long )pi; 1572#line 62 1573 __cil_tmp142 = __cil_tmp141 + 8; 1574#line 62 1575 __cil_tmp143 = *((int *)__cil_tmp142); 1576#line 62 1577 __cil_tmp144 = __cil_tmp143 + 2; 1578#line 62 1579 outb((unsigned char)6, __cil_tmp144); 1580 } 1581 { 1582#line 62 1583 __cil_tmp145 = (unsigned long )pi; 1584#line 62 1585 __cil_tmp146 = __cil_tmp145 + 16; 1586#line 62 1587 if (*((int *)__cil_tmp146)) { 1588 { 1589#line 62 1590 __cil_tmp147 = (unsigned long )pi; 1591#line 62 1592 __cil_tmp148 = __cil_tmp147 + 16; 1593#line 62 1594 __cil_tmp149 = *((int *)__cil_tmp148); 1595#line 62 1596 __cil_tmp150 = (unsigned long )__cil_tmp149; 1597#line 62 1598 __udelay(__cil_tmp150); 1599 } 1600 } else { 1601 1602 } 1603 } 1604 { 1605#line 62 1606 __cil_tmp151 = (unsigned long )pi; 1607#line 62 1608 __cil_tmp152 = __cil_tmp151 + 8; 1609#line 62 1610 __cil_tmp153 = *((int *)__cil_tmp152); 1611#line 62 1612 outb((unsigned char)255, __cil_tmp153); 1613 } 1614 { 1615#line 62 1616 __cil_tmp154 = (unsigned long )pi; 1617#line 62 1618 __cil_tmp155 = __cil_tmp154 + 16; 1619#line 62 1620 if (*((int *)__cil_tmp155)) { 1621 { 1622#line 62 1623 __cil_tmp156 = (unsigned long )pi; 1624#line 62 1625 __cil_tmp157 = __cil_tmp156 + 16; 1626#line 62 1627 __cil_tmp158 = *((int *)__cil_tmp157); 1628#line 62 1629 __cil_tmp159 = (unsigned long )__cil_tmp158; 1630#line 62 1631 __udelay(__cil_tmp159); 1632 } 1633 } else { 1634 1635 } 1636 } 1637 { 1638#line 63 1639 __cil_tmp160 = (unsigned long )pi; 1640#line 63 1641 __cil_tmp161 = __cil_tmp160 + 8; 1642#line 63 1643 __cil_tmp162 = *((int *)__cil_tmp161); 1644#line 63 1645 __cil_tmp163 = __cil_tmp162 + 2; 1646#line 63 1647 outb((unsigned char)39, __cil_tmp163); 1648 } 1649 { 1650#line 63 1651 __cil_tmp164 = (unsigned long )pi; 1652#line 63 1653 __cil_tmp165 = __cil_tmp164 + 16; 1654#line 63 1655 if (*((int *)__cil_tmp165)) { 1656 { 1657#line 63 1658 __cil_tmp166 = (unsigned long )pi; 1659#line 63 1660 __cil_tmp167 = __cil_tmp166 + 16; 1661#line 63 1662 __cil_tmp168 = *((int *)__cil_tmp167); 1663#line 63 1664 __cil_tmp169 = (unsigned long )__cil_tmp168; 1665#line 63 1666 __udelay(__cil_tmp169); 1667 } 1668 } else { 1669 1670 } 1671 } 1672 { 1673#line 63 1674 __cil_tmp170 = (unsigned long )pi; 1675#line 63 1676 __cil_tmp171 = __cil_tmp170 + 8; 1677#line 63 1678 __cil_tmp172 = *((int *)__cil_tmp171); 1679#line 63 1680 __cil_tmp173 = __cil_tmp172 + 2; 1681#line 63 1682 outb((unsigned char)38, __cil_tmp173); 1683 } 1684 { 1685#line 63 1686 __cil_tmp174 = (unsigned long )pi; 1687#line 63 1688 __cil_tmp175 = __cil_tmp174 + 16; 1689#line 63 1690 if (*((int *)__cil_tmp175)) { 1691 { 1692#line 63 1693 __cil_tmp176 = (unsigned long )pi; 1694#line 63 1695 __cil_tmp177 = __cil_tmp176 + 16; 1696#line 63 1697 __cil_tmp178 = *((int *)__cil_tmp177); 1698#line 63 1699 __cil_tmp179 = (unsigned long )__cil_tmp178; 1700#line 63 1701 __udelay(__cil_tmp179); 1702 } 1703 } else { 1704 1705 } 1706 } 1707 { 1708#line 63 1709 __cil_tmp180 = (unsigned long )pi; 1710#line 63 1711 __cil_tmp181 = __cil_tmp180 + 8; 1712#line 63 1713 __cil_tmp182 = *((int *)__cil_tmp181); 1714#line 63 1715 __cil_tmp183 = __cil_tmp182 + 2; 1716#line 63 1717 outb((unsigned char)32, __cil_tmp183); 1718 } 1719 { 1720#line 63 1721 __cil_tmp184 = (unsigned long )pi; 1722#line 63 1723 __cil_tmp185 = __cil_tmp184 + 16; 1724#line 63 1725 if (*((int *)__cil_tmp185)) { 1726 { 1727#line 63 1728 __cil_tmp186 = (unsigned long )pi; 1729#line 63 1730 __cil_tmp187 = __cil_tmp186 + 16; 1731#line 63 1732 __cil_tmp188 = *((int *)__cil_tmp187); 1733#line 63 1734 __cil_tmp189 = (unsigned long )__cil_tmp188; 1735#line 63 1736 __udelay(__cil_tmp189); 1737 } 1738 } else { 1739 1740 } 1741 } 1742 { 1743#line 64 1744 __cil_tmp190 = (unsigned long )pi; 1745#line 64 1746 __cil_tmp191 = __cil_tmp190 + 16; 1747#line 64 1748 if (*((int *)__cil_tmp191)) { 1749 { 1750#line 64 1751 __cil_tmp192 = (unsigned long )pi; 1752#line 64 1753 __cil_tmp193 = __cil_tmp192 + 16; 1754#line 64 1755 __cil_tmp194 = *((int *)__cil_tmp193); 1756#line 64 1757 __cil_tmp195 = (unsigned long )__cil_tmp194; 1758#line 64 1759 __udelay(__cil_tmp195); 1760 } 1761 } else { 1762 1763 } 1764 } 1765 { 1766#line 64 1767 __cil_tmp196 = (unsigned long )pi; 1768#line 64 1769 __cil_tmp197 = __cil_tmp196 + 8; 1770#line 64 1771 __cil_tmp198 = *((int *)__cil_tmp197); 1772#line 64 1773 tmp___1 = inb(__cil_tmp198); 1774#line 64 1775 __cil_tmp199 = (int )tmp___1; 1776#line 64 1777 a = __cil_tmp199 & 255; 1778#line 65 1779 __cil_tmp200 = (unsigned long )pi; 1780#line 65 1781 __cil_tmp201 = __cil_tmp200 + 8; 1782#line 65 1783 __cil_tmp202 = *((int *)__cil_tmp201); 1784#line 65 1785 __cil_tmp203 = __cil_tmp202 + 2; 1786#line 65 1787 outb((unsigned char)38, __cil_tmp203); 1788 } 1789 { 1790#line 65 1791 __cil_tmp204 = (unsigned long )pi; 1792#line 65 1793 __cil_tmp205 = __cil_tmp204 + 16; 1794#line 65 1795 if (*((int *)__cil_tmp205)) { 1796 { 1797#line 65 1798 __cil_tmp206 = (unsigned long )pi; 1799#line 65 1800 __cil_tmp207 = __cil_tmp206 + 16; 1801#line 65 1802 __cil_tmp208 = *((int *)__cil_tmp207); 1803#line 65 1804 __cil_tmp209 = (unsigned long )__cil_tmp208; 1805#line 65 1806 __udelay(__cil_tmp209); 1807 } 1808 } else { 1809 1810 } 1811 } 1812 { 1813#line 65 1814 __cil_tmp210 = (unsigned long )pi; 1815#line 65 1816 __cil_tmp211 = __cil_tmp210 + 8; 1817#line 65 1818 __cil_tmp212 = *((int *)__cil_tmp211); 1819#line 65 1820 __cil_tmp213 = __cil_tmp212 + 2; 1821#line 65 1822 outb((unsigned char)12, __cil_tmp213); 1823 } 1824 { 1825#line 65 1826 __cil_tmp214 = (unsigned long )pi; 1827#line 65 1828 __cil_tmp215 = __cil_tmp214 + 16; 1829#line 65 1830 if (*((int *)__cil_tmp215)) { 1831 { 1832#line 65 1833 __cil_tmp216 = (unsigned long )pi; 1834#line 65 1835 __cil_tmp217 = __cil_tmp216 + 16; 1836#line 65 1837 __cil_tmp218 = *((int *)__cil_tmp217); 1838#line 65 1839 __cil_tmp219 = (unsigned long )__cil_tmp218; 1840#line 65 1841 __udelay(__cil_tmp219); 1842 } 1843 } else { 1844 1845 } 1846 } 1847#line 66 1848 return (a); 1849 } else { 1850 switch_break: /* CIL Label */ ; 1851 } 1852 } 1853#line 68 1854 return (-1); 1855} 1856} 1857#line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 1858static void aten_read_block(PIA *pi , char *buf , int count ) 1859{ int k ; 1860 int a ; 1861 int b ; 1862 int c ; 1863 int d ; 1864 unsigned char tmp ; 1865 unsigned char tmp___0 ; 1866 unsigned char tmp___1 ; 1867 unsigned char tmp___2 ; 1868 unsigned char tmp___3 ; 1869 unsigned char tmp___4 ; 1870 unsigned long __cil_tmp15 ; 1871 unsigned long __cil_tmp16 ; 1872 unsigned long __cil_tmp17 ; 1873 unsigned long __cil_tmp18 ; 1874 int __cil_tmp19 ; 1875 unsigned long __cil_tmp20 ; 1876 unsigned long __cil_tmp21 ; 1877 unsigned long __cil_tmp22 ; 1878 unsigned long __cil_tmp23 ; 1879 int __cil_tmp24 ; 1880 unsigned long __cil_tmp25 ; 1881 unsigned long __cil_tmp26 ; 1882 unsigned long __cil_tmp27 ; 1883 int __cil_tmp28 ; 1884 int __cil_tmp29 ; 1885 unsigned long __cil_tmp30 ; 1886 unsigned long __cil_tmp31 ; 1887 unsigned long __cil_tmp32 ; 1888 unsigned long __cil_tmp33 ; 1889 int __cil_tmp34 ; 1890 unsigned long __cil_tmp35 ; 1891 unsigned long __cil_tmp36 ; 1892 unsigned long __cil_tmp37 ; 1893 int __cil_tmp38 ; 1894 int __cil_tmp39 ; 1895 unsigned long __cil_tmp40 ; 1896 unsigned long __cil_tmp41 ; 1897 unsigned long __cil_tmp42 ; 1898 unsigned long __cil_tmp43 ; 1899 int __cil_tmp44 ; 1900 unsigned long __cil_tmp45 ; 1901 int __cil_tmp46 ; 1902 unsigned long __cil_tmp47 ; 1903 unsigned long __cil_tmp48 ; 1904 int __cil_tmp49 ; 1905 int __cil_tmp50 ; 1906 unsigned long __cil_tmp51 ; 1907 unsigned long __cil_tmp52 ; 1908 unsigned long __cil_tmp53 ; 1909 unsigned long __cil_tmp54 ; 1910 int __cil_tmp55 ; 1911 unsigned long __cil_tmp56 ; 1912 unsigned long __cil_tmp57 ; 1913 unsigned long __cil_tmp58 ; 1914 int __cil_tmp59 ; 1915 int __cil_tmp60 ; 1916 unsigned long __cil_tmp61 ; 1917 unsigned long __cil_tmp62 ; 1918 unsigned long __cil_tmp63 ; 1919 unsigned long __cil_tmp64 ; 1920 int __cil_tmp65 ; 1921 unsigned long __cil_tmp66 ; 1922 unsigned long __cil_tmp67 ; 1923 unsigned long __cil_tmp68 ; 1924 int __cil_tmp69 ; 1925 int __cil_tmp70 ; 1926 unsigned long __cil_tmp71 ; 1927 unsigned long __cil_tmp72 ; 1928 unsigned long __cil_tmp73 ; 1929 unsigned long __cil_tmp74 ; 1930 int __cil_tmp75 ; 1931 unsigned long __cil_tmp76 ; 1932 unsigned long __cil_tmp77 ; 1933 unsigned long __cil_tmp78 ; 1934 unsigned long __cil_tmp79 ; 1935 unsigned long __cil_tmp80 ; 1936 int __cil_tmp81 ; 1937 unsigned long __cil_tmp82 ; 1938 unsigned long __cil_tmp83 ; 1939 unsigned long __cil_tmp84 ; 1940 int __cil_tmp85 ; 1941 int __cil_tmp86 ; 1942 int __cil_tmp87 ; 1943 unsigned long __cil_tmp88 ; 1944 unsigned long __cil_tmp89 ; 1945 int __cil_tmp90 ; 1946 unsigned long __cil_tmp91 ; 1947 unsigned long __cil_tmp92 ; 1948 unsigned long __cil_tmp93 ; 1949 unsigned long __cil_tmp94 ; 1950 int __cil_tmp95 ; 1951 unsigned long __cil_tmp96 ; 1952 unsigned long __cil_tmp97 ; 1953 unsigned long __cil_tmp98 ; 1954 unsigned long __cil_tmp99 ; 1955 unsigned long __cil_tmp100 ; 1956 int __cil_tmp101 ; 1957 unsigned long __cil_tmp102 ; 1958 unsigned long __cil_tmp103 ; 1959 unsigned long __cil_tmp104 ; 1960 int __cil_tmp105 ; 1961 int __cil_tmp106 ; 1962 int __cil_tmp107 ; 1963 unsigned long __cil_tmp108 ; 1964 unsigned long __cil_tmp109 ; 1965 int __cil_tmp110 ; 1966 int __cil_tmp111 ; 1967 unsigned long __cil_tmp112 ; 1968 unsigned long __cil_tmp113 ; 1969 unsigned long __cil_tmp114 ; 1970 unsigned long __cil_tmp115 ; 1971 int __cil_tmp116 ; 1972 unsigned long __cil_tmp117 ; 1973 unsigned long __cil_tmp118 ; 1974 unsigned long __cil_tmp119 ; 1975 unsigned long __cil_tmp120 ; 1976 unsigned long __cil_tmp121 ; 1977 int __cil_tmp122 ; 1978 unsigned long __cil_tmp123 ; 1979 unsigned long __cil_tmp124 ; 1980 unsigned long __cil_tmp125 ; 1981 int __cil_tmp126 ; 1982 int __cil_tmp127 ; 1983 int __cil_tmp128 ; 1984 unsigned long __cil_tmp129 ; 1985 unsigned long __cil_tmp130 ; 1986 int __cil_tmp131 ; 1987 unsigned long __cil_tmp132 ; 1988 unsigned long __cil_tmp133 ; 1989 unsigned long __cil_tmp134 ; 1990 unsigned long __cil_tmp135 ; 1991 int __cil_tmp136 ; 1992 unsigned long __cil_tmp137 ; 1993 unsigned long __cil_tmp138 ; 1994 unsigned long __cil_tmp139 ; 1995 unsigned long __cil_tmp140 ; 1996 unsigned long __cil_tmp141 ; 1997 int __cil_tmp142 ; 1998 unsigned long __cil_tmp143 ; 1999 unsigned long __cil_tmp144 ; 2000 unsigned long __cil_tmp145 ; 2001 int __cil_tmp146 ; 2002 int __cil_tmp147 ; 2003 int __cil_tmp148 ; 2004 int __cil_tmp149 ; 2005 char *__cil_tmp150 ; 2006 int __cil_tmp151 ; 2007 int __cil_tmp152 ; 2008 int __cil_tmp153 ; 2009 int __cil_tmp154 ; 2010 int __cil_tmp155 ; 2011 int __cil_tmp156 ; 2012 int __cil_tmp157 ; 2013 char *__cil_tmp158 ; 2014 int __cil_tmp159 ; 2015 int __cil_tmp160 ; 2016 int __cil_tmp161 ; 2017 int __cil_tmp162 ; 2018 int __cil_tmp163 ; 2019 unsigned long __cil_tmp164 ; 2020 unsigned long __cil_tmp165 ; 2021 int __cil_tmp166 ; 2022 int __cil_tmp167 ; 2023 unsigned long __cil_tmp168 ; 2024 unsigned long __cil_tmp169 ; 2025 unsigned long __cil_tmp170 ; 2026 unsigned long __cil_tmp171 ; 2027 int __cil_tmp172 ; 2028 unsigned long __cil_tmp173 ; 2029 unsigned long __cil_tmp174 ; 2030 unsigned long __cil_tmp175 ; 2031 int __cil_tmp176 ; 2032 unsigned long __cil_tmp177 ; 2033 unsigned long __cil_tmp178 ; 2034 unsigned long __cil_tmp179 ; 2035 unsigned long __cil_tmp180 ; 2036 int __cil_tmp181 ; 2037 unsigned long __cil_tmp182 ; 2038 unsigned long __cil_tmp183 ; 2039 unsigned long __cil_tmp184 ; 2040 int __cil_tmp185 ; 2041 int __cil_tmp186 ; 2042 unsigned long __cil_tmp187 ; 2043 unsigned long __cil_tmp188 ; 2044 unsigned long __cil_tmp189 ; 2045 unsigned long __cil_tmp190 ; 2046 int __cil_tmp191 ; 2047 unsigned long __cil_tmp192 ; 2048 unsigned long __cil_tmp193 ; 2049 unsigned long __cil_tmp194 ; 2050 int __cil_tmp195 ; 2051 int __cil_tmp196 ; 2052 unsigned long __cil_tmp197 ; 2053 unsigned long __cil_tmp198 ; 2054 unsigned long __cil_tmp199 ; 2055 unsigned long __cil_tmp200 ; 2056 int __cil_tmp201 ; 2057 unsigned long __cil_tmp202 ; 2058 int __cil_tmp203 ; 2059 unsigned long __cil_tmp204 ; 2060 unsigned long __cil_tmp205 ; 2061 int __cil_tmp206 ; 2062 int __cil_tmp207 ; 2063 unsigned long __cil_tmp208 ; 2064 unsigned long __cil_tmp209 ; 2065 unsigned long __cil_tmp210 ; 2066 unsigned long __cil_tmp211 ; 2067 int __cil_tmp212 ; 2068 unsigned long __cil_tmp213 ; 2069 unsigned long __cil_tmp214 ; 2070 unsigned long __cil_tmp215 ; 2071 int __cil_tmp216 ; 2072 int __cil_tmp217 ; 2073 unsigned long __cil_tmp218 ; 2074 unsigned long __cil_tmp219 ; 2075 unsigned long __cil_tmp220 ; 2076 unsigned long __cil_tmp221 ; 2077 int __cil_tmp222 ; 2078 unsigned long __cil_tmp223 ; 2079 unsigned long __cil_tmp224 ; 2080 unsigned long __cil_tmp225 ; 2081 int __cil_tmp226 ; 2082 int __cil_tmp227 ; 2083 unsigned long __cil_tmp228 ; 2084 unsigned long __cil_tmp229 ; 2085 unsigned long __cil_tmp230 ; 2086 unsigned long __cil_tmp231 ; 2087 int __cil_tmp232 ; 2088 unsigned long __cil_tmp233 ; 2089 unsigned long __cil_tmp234 ; 2090 unsigned long __cil_tmp235 ; 2091 unsigned long __cil_tmp236 ; 2092 unsigned long __cil_tmp237 ; 2093 int __cil_tmp238 ; 2094 unsigned long __cil_tmp239 ; 2095 unsigned long __cil_tmp240 ; 2096 unsigned long __cil_tmp241 ; 2097 int __cil_tmp242 ; 2098 int __cil_tmp243 ; 2099 unsigned long __cil_tmp244 ; 2100 unsigned long __cil_tmp245 ; 2101 int __cil_tmp246 ; 2102 int __cil_tmp247 ; 2103 unsigned long __cil_tmp248 ; 2104 unsigned long __cil_tmp249 ; 2105 unsigned long __cil_tmp250 ; 2106 unsigned long __cil_tmp251 ; 2107 int __cil_tmp252 ; 2108 unsigned long __cil_tmp253 ; 2109 unsigned long __cil_tmp254 ; 2110 unsigned long __cil_tmp255 ; 2111 unsigned long __cil_tmp256 ; 2112 unsigned long __cil_tmp257 ; 2113 int __cil_tmp258 ; 2114 unsigned long __cil_tmp259 ; 2115 unsigned long __cil_tmp260 ; 2116 unsigned long __cil_tmp261 ; 2117 int __cil_tmp262 ; 2118 int __cil_tmp263 ; 2119 int __cil_tmp264 ; 2120 char *__cil_tmp265 ; 2121 int __cil_tmp266 ; 2122 int __cil_tmp267 ; 2123 char *__cil_tmp268 ; 2124 unsigned long __cil_tmp269 ; 2125 unsigned long __cil_tmp270 ; 2126 int __cil_tmp271 ; 2127 int __cil_tmp272 ; 2128 unsigned long __cil_tmp273 ; 2129 unsigned long __cil_tmp274 ; 2130 unsigned long __cil_tmp275 ; 2131 unsigned long __cil_tmp276 ; 2132 int __cil_tmp277 ; 2133 unsigned long __cil_tmp278 ; 2134 unsigned long __cil_tmp279 ; 2135 unsigned long __cil_tmp280 ; 2136 int __cil_tmp281 ; 2137 int __cil_tmp282 ; 2138 unsigned long __cil_tmp283 ; 2139 unsigned long __cil_tmp284 ; 2140 unsigned long __cil_tmp285 ; 2141 unsigned long __cil_tmp286 ; 2142 int __cil_tmp287 ; 2143 unsigned long __cil_tmp288 ; 2144 2145 { 2146 { 2147#line 75 2148 __cil_tmp15 = (unsigned long )pi; 2149#line 75 2150 __cil_tmp16 = __cil_tmp15 + 12; 2151#line 77 2152 if (*((int *)__cil_tmp16) == 0) { 2153#line 77 2154 goto case_0; 2155 } else 2156#line 88 2157 if (*((int *)__cil_tmp16) == 1) { 2158#line 88 2159 goto case_1; 2160 } else 2161#line 75 2162 if (0) { 2163 case_0: /* CIL Label */ 2164 { 2165#line 77 2166 __cil_tmp17 = (unsigned long )pi; 2167#line 77 2168 __cil_tmp18 = __cil_tmp17 + 8; 2169#line 77 2170 __cil_tmp19 = *((int *)__cil_tmp18); 2171#line 77 2172 outb((unsigned char)72, __cil_tmp19); 2173 } 2174 { 2175#line 77 2176 __cil_tmp20 = (unsigned long )pi; 2177#line 77 2178 __cil_tmp21 = __cil_tmp20 + 16; 2179#line 77 2180 if (*((int *)__cil_tmp21)) { 2181 { 2182#line 77 2183 __cil_tmp22 = (unsigned long )pi; 2184#line 77 2185 __cil_tmp23 = __cil_tmp22 + 16; 2186#line 77 2187 __cil_tmp24 = *((int *)__cil_tmp23); 2188#line 77 2189 __cil_tmp25 = (unsigned long )__cil_tmp24; 2190#line 77 2191 __udelay(__cil_tmp25); 2192 } 2193 } else { 2194 2195 } 2196 } 2197 { 2198#line 77 2199 __cil_tmp26 = (unsigned long )pi; 2200#line 77 2201 __cil_tmp27 = __cil_tmp26 + 8; 2202#line 77 2203 __cil_tmp28 = *((int *)__cil_tmp27); 2204#line 77 2205 __cil_tmp29 = __cil_tmp28 + 2; 2206#line 77 2207 outb((unsigned char)14, __cil_tmp29); 2208 } 2209 { 2210#line 77 2211 __cil_tmp30 = (unsigned long )pi; 2212#line 77 2213 __cil_tmp31 = __cil_tmp30 + 16; 2214#line 77 2215 if (*((int *)__cil_tmp31)) { 2216 { 2217#line 77 2218 __cil_tmp32 = (unsigned long )pi; 2219#line 77 2220 __cil_tmp33 = __cil_tmp32 + 16; 2221#line 77 2222 __cil_tmp34 = *((int *)__cil_tmp33); 2223#line 77 2224 __cil_tmp35 = (unsigned long )__cil_tmp34; 2225#line 77 2226 __udelay(__cil_tmp35); 2227 } 2228 } else { 2229 2230 } 2231 } 2232 { 2233#line 77 2234 __cil_tmp36 = (unsigned long )pi; 2235#line 77 2236 __cil_tmp37 = __cil_tmp36 + 8; 2237#line 77 2238 __cil_tmp38 = *((int *)__cil_tmp37); 2239#line 77 2240 __cil_tmp39 = __cil_tmp38 + 2; 2241#line 77 2242 outb((unsigned char)6, __cil_tmp39); 2243 } 2244 { 2245#line 77 2246 __cil_tmp40 = (unsigned long )pi; 2247#line 77 2248 __cil_tmp41 = __cil_tmp40 + 16; 2249#line 77 2250 if (*((int *)__cil_tmp41)) { 2251 { 2252#line 77 2253 __cil_tmp42 = (unsigned long )pi; 2254#line 77 2255 __cil_tmp43 = __cil_tmp42 + 16; 2256#line 77 2257 __cil_tmp44 = *((int *)__cil_tmp43); 2258#line 77 2259 __cil_tmp45 = (unsigned long )__cil_tmp44; 2260#line 77 2261 __udelay(__cil_tmp45); 2262 } 2263 } else { 2264 2265 } 2266 } 2267#line 78 2268 k = 0; 2269 { 2270#line 78 2271 while (1) { 2272 while_continue: /* CIL Label */ ; 2273 { 2274#line 78 2275 __cil_tmp46 = count / 2; 2276#line 78 2277 if (k < __cil_tmp46) { 2278 2279 } else { 2280#line 78 2281 goto while_break; 2282 } 2283 } 2284 { 2285#line 79 2286 __cil_tmp47 = (unsigned long )pi; 2287#line 79 2288 __cil_tmp48 = __cil_tmp47 + 8; 2289#line 79 2290 __cil_tmp49 = *((int *)__cil_tmp48); 2291#line 79 2292 __cil_tmp50 = __cil_tmp49 + 2; 2293#line 79 2294 outb((unsigned char)7, __cil_tmp50); 2295 } 2296 { 2297#line 79 2298 __cil_tmp51 = (unsigned long )pi; 2299#line 79 2300 __cil_tmp52 = __cil_tmp51 + 16; 2301#line 79 2302 if (*((int *)__cil_tmp52)) { 2303 { 2304#line 79 2305 __cil_tmp53 = (unsigned long )pi; 2306#line 79 2307 __cil_tmp54 = __cil_tmp53 + 16; 2308#line 79 2309 __cil_tmp55 = *((int *)__cil_tmp54); 2310#line 79 2311 __cil_tmp56 = (unsigned long )__cil_tmp55; 2312#line 79 2313 __udelay(__cil_tmp56); 2314 } 2315 } else { 2316 2317 } 2318 } 2319 { 2320#line 79 2321 __cil_tmp57 = (unsigned long )pi; 2322#line 79 2323 __cil_tmp58 = __cil_tmp57 + 8; 2324#line 79 2325 __cil_tmp59 = *((int *)__cil_tmp58); 2326#line 79 2327 __cil_tmp60 = __cil_tmp59 + 2; 2328#line 79 2329 outb((unsigned char)6, __cil_tmp60); 2330 } 2331 { 2332#line 79 2333 __cil_tmp61 = (unsigned long )pi; 2334#line 79 2335 __cil_tmp62 = __cil_tmp61 + 16; 2336#line 79 2337 if (*((int *)__cil_tmp62)) { 2338 { 2339#line 79 2340 __cil_tmp63 = (unsigned long )pi; 2341#line 79 2342 __cil_tmp64 = __cil_tmp63 + 16; 2343#line 79 2344 __cil_tmp65 = *((int *)__cil_tmp64); 2345#line 79 2346 __cil_tmp66 = (unsigned long )__cil_tmp65; 2347#line 79 2348 __udelay(__cil_tmp66); 2349 } 2350 } else { 2351 2352 } 2353 } 2354 { 2355#line 79 2356 __cil_tmp67 = (unsigned long )pi; 2357#line 79 2358 __cil_tmp68 = __cil_tmp67 + 8; 2359#line 79 2360 __cil_tmp69 = *((int *)__cil_tmp68); 2361#line 79 2362 __cil_tmp70 = __cil_tmp69 + 2; 2363#line 79 2364 outb((unsigned char)2, __cil_tmp70); 2365 } 2366 { 2367#line 79 2368 __cil_tmp71 = (unsigned long )pi; 2369#line 79 2370 __cil_tmp72 = __cil_tmp71 + 16; 2371#line 79 2372 if (*((int *)__cil_tmp72)) { 2373 { 2374#line 79 2375 __cil_tmp73 = (unsigned long )pi; 2376#line 79 2377 __cil_tmp74 = __cil_tmp73 + 16; 2378#line 79 2379 __cil_tmp75 = *((int *)__cil_tmp74); 2380#line 79 2381 __cil_tmp76 = (unsigned long )__cil_tmp75; 2382#line 79 2383 __udelay(__cil_tmp76); 2384 } 2385 } else { 2386 2387 } 2388 } 2389 { 2390#line 80 2391 __cil_tmp77 = (unsigned long )pi; 2392#line 80 2393 __cil_tmp78 = __cil_tmp77 + 16; 2394#line 80 2395 if (*((int *)__cil_tmp78)) { 2396 { 2397#line 80 2398 __cil_tmp79 = (unsigned long )pi; 2399#line 80 2400 __cil_tmp80 = __cil_tmp79 + 16; 2401#line 80 2402 __cil_tmp81 = *((int *)__cil_tmp80); 2403#line 80 2404 __cil_tmp82 = (unsigned long )__cil_tmp81; 2405#line 80 2406 __udelay(__cil_tmp82); 2407 } 2408 } else { 2409 2410 } 2411 } 2412 { 2413#line 80 2414 __cil_tmp83 = (unsigned long )pi; 2415#line 80 2416 __cil_tmp84 = __cil_tmp83 + 8; 2417#line 80 2418 __cil_tmp85 = *((int *)__cil_tmp84); 2419#line 80 2420 __cil_tmp86 = __cil_tmp85 + 1; 2421#line 80 2422 tmp = inb(__cil_tmp86); 2423#line 80 2424 __cil_tmp87 = (int )tmp; 2425#line 80 2426 a = __cil_tmp87 & 255; 2427#line 80 2428 __cil_tmp88 = (unsigned long )pi; 2429#line 80 2430 __cil_tmp89 = __cil_tmp88 + 8; 2431#line 80 2432 __cil_tmp90 = *((int *)__cil_tmp89); 2433#line 80 2434 outb((unsigned char)88, __cil_tmp90); 2435 } 2436 { 2437#line 80 2438 __cil_tmp91 = (unsigned long )pi; 2439#line 80 2440 __cil_tmp92 = __cil_tmp91 + 16; 2441#line 80 2442 if (*((int *)__cil_tmp92)) { 2443 { 2444#line 80 2445 __cil_tmp93 = (unsigned long )pi; 2446#line 80 2447 __cil_tmp94 = __cil_tmp93 + 16; 2448#line 80 2449 __cil_tmp95 = *((int *)__cil_tmp94); 2450#line 80 2451 __cil_tmp96 = (unsigned long )__cil_tmp95; 2452#line 80 2453 __udelay(__cil_tmp96); 2454 } 2455 } else { 2456 2457 } 2458 } 2459 { 2460#line 80 2461 __cil_tmp97 = (unsigned long )pi; 2462#line 80 2463 __cil_tmp98 = __cil_tmp97 + 16; 2464#line 80 2465 if (*((int *)__cil_tmp98)) { 2466 { 2467#line 80 2468 __cil_tmp99 = (unsigned long )pi; 2469#line 80 2470 __cil_tmp100 = __cil_tmp99 + 16; 2471#line 80 2472 __cil_tmp101 = *((int *)__cil_tmp100); 2473#line 80 2474 __cil_tmp102 = (unsigned long )__cil_tmp101; 2475#line 80 2476 __udelay(__cil_tmp102); 2477 } 2478 } else { 2479 2480 } 2481 } 2482 { 2483#line 80 2484 __cil_tmp103 = (unsigned long )pi; 2485#line 80 2486 __cil_tmp104 = __cil_tmp103 + 8; 2487#line 80 2488 __cil_tmp105 = *((int *)__cil_tmp104); 2489#line 80 2490 __cil_tmp106 = __cil_tmp105 + 1; 2491#line 80 2492 tmp___0 = inb(__cil_tmp106); 2493#line 80 2494 __cil_tmp107 = (int )tmp___0; 2495#line 80 2496 b = __cil_tmp107 & 255; 2497#line 81 2498 __cil_tmp108 = (unsigned long )pi; 2499#line 81 2500 __cil_tmp109 = __cil_tmp108 + 8; 2501#line 81 2502 __cil_tmp110 = *((int *)__cil_tmp109); 2503#line 81 2504 __cil_tmp111 = __cil_tmp110 + 2; 2505#line 81 2506 outb((unsigned char)0, __cil_tmp111); 2507 } 2508 { 2509#line 81 2510 __cil_tmp112 = (unsigned long )pi; 2511#line 81 2512 __cil_tmp113 = __cil_tmp112 + 16; 2513#line 81 2514 if (*((int *)__cil_tmp113)) { 2515 { 2516#line 81 2517 __cil_tmp114 = (unsigned long )pi; 2518#line 81 2519 __cil_tmp115 = __cil_tmp114 + 16; 2520#line 81 2521 __cil_tmp116 = *((int *)__cil_tmp115); 2522#line 81 2523 __cil_tmp117 = (unsigned long )__cil_tmp116; 2524#line 81 2525 __udelay(__cil_tmp117); 2526 } 2527 } else { 2528 2529 } 2530 } 2531 { 2532#line 81 2533 __cil_tmp118 = (unsigned long )pi; 2534#line 81 2535 __cil_tmp119 = __cil_tmp118 + 16; 2536#line 81 2537 if (*((int *)__cil_tmp119)) { 2538 { 2539#line 81 2540 __cil_tmp120 = (unsigned long )pi; 2541#line 81 2542 __cil_tmp121 = __cil_tmp120 + 16; 2543#line 81 2544 __cil_tmp122 = *((int *)__cil_tmp121); 2545#line 81 2546 __cil_tmp123 = (unsigned long )__cil_tmp122; 2547#line 81 2548 __udelay(__cil_tmp123); 2549 } 2550 } else { 2551 2552 } 2553 } 2554 { 2555#line 81 2556 __cil_tmp124 = (unsigned long )pi; 2557#line 81 2558 __cil_tmp125 = __cil_tmp124 + 8; 2559#line 81 2560 __cil_tmp126 = *((int *)__cil_tmp125); 2561#line 81 2562 __cil_tmp127 = __cil_tmp126 + 1; 2563#line 81 2564 tmp___1 = inb(__cil_tmp127); 2565#line 81 2566 __cil_tmp128 = (int )tmp___1; 2567#line 81 2568 d = __cil_tmp128 & 255; 2569#line 81 2570 __cil_tmp129 = (unsigned long )pi; 2571#line 81 2572 __cil_tmp130 = __cil_tmp129 + 8; 2573#line 81 2574 __cil_tmp131 = *((int *)__cil_tmp130); 2575#line 81 2576 outb((unsigned char)72, __cil_tmp131); 2577 } 2578 { 2579#line 81 2580 __cil_tmp132 = (unsigned long )pi; 2581#line 81 2582 __cil_tmp133 = __cil_tmp132 + 16; 2583#line 81 2584 if (*((int *)__cil_tmp133)) { 2585 { 2586#line 81 2587 __cil_tmp134 = (unsigned long )pi; 2588#line 81 2589 __cil_tmp135 = __cil_tmp134 + 16; 2590#line 81 2591 __cil_tmp136 = *((int *)__cil_tmp135); 2592#line 81 2593 __cil_tmp137 = (unsigned long )__cil_tmp136; 2594#line 81 2595 __udelay(__cil_tmp137); 2596 } 2597 } else { 2598 2599 } 2600 } 2601 { 2602#line 81 2603 __cil_tmp138 = (unsigned long )pi; 2604#line 81 2605 __cil_tmp139 = __cil_tmp138 + 16; 2606#line 81 2607 if (*((int *)__cil_tmp139)) { 2608 { 2609#line 81 2610 __cil_tmp140 = (unsigned long )pi; 2611#line 81 2612 __cil_tmp141 = __cil_tmp140 + 16; 2613#line 81 2614 __cil_tmp142 = *((int *)__cil_tmp141); 2615#line 81 2616 __cil_tmp143 = (unsigned long )__cil_tmp142; 2617#line 81 2618 __udelay(__cil_tmp143); 2619 } 2620 } else { 2621 2622 } 2623 } 2624 { 2625#line 81 2626 __cil_tmp144 = (unsigned long )pi; 2627#line 81 2628 __cil_tmp145 = __cil_tmp144 + 8; 2629#line 81 2630 __cil_tmp146 = *((int *)__cil_tmp145); 2631#line 81 2632 __cil_tmp147 = __cil_tmp146 + 1; 2633#line 81 2634 tmp___2 = inb(__cil_tmp147); 2635#line 81 2636 __cil_tmp148 = (int )tmp___2; 2637#line 81 2638 c = __cil_tmp148 & 255; 2639#line 82 2640 __cil_tmp149 = 2 * k; 2641#line 82 2642 __cil_tmp150 = buf + __cil_tmp149; 2643#line 82 2644 __cil_tmp151 = d & 240; 2645#line 82 2646 __cil_tmp152 = c >> 4; 2647#line 82 2648 __cil_tmp153 = __cil_tmp152 & 15; 2649#line 82 2650 __cil_tmp154 = __cil_tmp153 | __cil_tmp151; 2651#line 82 2652 __cil_tmp155 = __cil_tmp154 ^ 136; 2653#line 82 2654 *__cil_tmp150 = (char )__cil_tmp155; 2655#line 83 2656 __cil_tmp156 = 2 * k; 2657#line 83 2658 __cil_tmp157 = __cil_tmp156 + 1; 2659#line 83 2660 __cil_tmp158 = buf + __cil_tmp157; 2661#line 83 2662 __cil_tmp159 = b & 240; 2663#line 83 2664 __cil_tmp160 = a >> 4; 2665#line 83 2666 __cil_tmp161 = __cil_tmp160 & 15; 2667#line 83 2668 __cil_tmp162 = __cil_tmp161 | __cil_tmp159; 2669#line 83 2670 __cil_tmp163 = __cil_tmp162 ^ 136; 2671#line 83 2672 *__cil_tmp158 = (char )__cil_tmp163; 2673#line 78 2674 k = k + 1; 2675 } 2676 } 2677 while_break: /* CIL Label */ ; 2678 } 2679 { 2680#line 85 2681 __cil_tmp164 = (unsigned long )pi; 2682#line 85 2683 __cil_tmp165 = __cil_tmp164 + 8; 2684#line 85 2685 __cil_tmp166 = *((int *)__cil_tmp165); 2686#line 85 2687 __cil_tmp167 = __cil_tmp166 + 2; 2688#line 85 2689 outb((unsigned char)12, __cil_tmp167); 2690 } 2691 { 2692#line 85 2693 __cil_tmp168 = (unsigned long )pi; 2694#line 85 2695 __cil_tmp169 = __cil_tmp168 + 16; 2696#line 85 2697 if (*((int *)__cil_tmp169)) { 2698 { 2699#line 85 2700 __cil_tmp170 = (unsigned long )pi; 2701#line 85 2702 __cil_tmp171 = __cil_tmp170 + 16; 2703#line 85 2704 __cil_tmp172 = *((int *)__cil_tmp171); 2705#line 85 2706 __cil_tmp173 = (unsigned long )__cil_tmp172; 2707#line 85 2708 __udelay(__cil_tmp173); 2709 } 2710 } else { 2711 2712 } 2713 } 2714#line 86 2715 goto switch_break; 2716 case_1: /* CIL Label */ 2717 { 2718#line 88 2719 __cil_tmp174 = (unsigned long )pi; 2720#line 88 2721 __cil_tmp175 = __cil_tmp174 + 8; 2722#line 88 2723 __cil_tmp176 = *((int *)__cil_tmp175); 2724#line 88 2725 outb((unsigned char)88, __cil_tmp176); 2726 } 2727 { 2728#line 88 2729 __cil_tmp177 = (unsigned long )pi; 2730#line 88 2731 __cil_tmp178 = __cil_tmp177 + 16; 2732#line 88 2733 if (*((int *)__cil_tmp178)) { 2734 { 2735#line 88 2736 __cil_tmp179 = (unsigned long )pi; 2737#line 88 2738 __cil_tmp180 = __cil_tmp179 + 16; 2739#line 88 2740 __cil_tmp181 = *((int *)__cil_tmp180); 2741#line 88 2742 __cil_tmp182 = (unsigned long )__cil_tmp181; 2743#line 88 2744 __udelay(__cil_tmp182); 2745 } 2746 } else { 2747 2748 } 2749 } 2750 { 2751#line 88 2752 __cil_tmp183 = (unsigned long )pi; 2753#line 88 2754 __cil_tmp184 = __cil_tmp183 + 8; 2755#line 88 2756 __cil_tmp185 = *((int *)__cil_tmp184); 2757#line 88 2758 __cil_tmp186 = __cil_tmp185 + 2; 2759#line 88 2760 outb((unsigned char)14, __cil_tmp186); 2761 } 2762 { 2763#line 88 2764 __cil_tmp187 = (unsigned long )pi; 2765#line 88 2766 __cil_tmp188 = __cil_tmp187 + 16; 2767#line 88 2768 if (*((int *)__cil_tmp188)) { 2769 { 2770#line 88 2771 __cil_tmp189 = (unsigned long )pi; 2772#line 88 2773 __cil_tmp190 = __cil_tmp189 + 16; 2774#line 88 2775 __cil_tmp191 = *((int *)__cil_tmp190); 2776#line 88 2777 __cil_tmp192 = (unsigned long )__cil_tmp191; 2778#line 88 2779 __udelay(__cil_tmp192); 2780 } 2781 } else { 2782 2783 } 2784 } 2785 { 2786#line 88 2787 __cil_tmp193 = (unsigned long )pi; 2788#line 88 2789 __cil_tmp194 = __cil_tmp193 + 8; 2790#line 88 2791 __cil_tmp195 = *((int *)__cil_tmp194); 2792#line 88 2793 __cil_tmp196 = __cil_tmp195 + 2; 2794#line 88 2795 outb((unsigned char)6, __cil_tmp196); 2796 } 2797 { 2798#line 88 2799 __cil_tmp197 = (unsigned long )pi; 2800#line 88 2801 __cil_tmp198 = __cil_tmp197 + 16; 2802#line 88 2803 if (*((int *)__cil_tmp198)) { 2804 { 2805#line 88 2806 __cil_tmp199 = (unsigned long )pi; 2807#line 88 2808 __cil_tmp200 = __cil_tmp199 + 16; 2809#line 88 2810 __cil_tmp201 = *((int *)__cil_tmp200); 2811#line 88 2812 __cil_tmp202 = (unsigned long )__cil_tmp201; 2813#line 88 2814 __udelay(__cil_tmp202); 2815 } 2816 } else { 2817 2818 } 2819 } 2820#line 89 2821 k = 0; 2822 { 2823#line 89 2824 while (1) { 2825 while_continue___0: /* CIL Label */ ; 2826 { 2827#line 89 2828 __cil_tmp203 = count / 2; 2829#line 89 2830 if (k < __cil_tmp203) { 2831 2832 } else { 2833#line 89 2834 goto while_break___0; 2835 } 2836 } 2837 { 2838#line 90 2839 __cil_tmp204 = (unsigned long )pi; 2840#line 90 2841 __cil_tmp205 = __cil_tmp204 + 8; 2842#line 90 2843 __cil_tmp206 = *((int *)__cil_tmp205); 2844#line 90 2845 __cil_tmp207 = __cil_tmp206 + 2; 2846#line 90 2847 outb((unsigned char)39, __cil_tmp207); 2848 } 2849 { 2850#line 90 2851 __cil_tmp208 = (unsigned long )pi; 2852#line 90 2853 __cil_tmp209 = __cil_tmp208 + 16; 2854#line 90 2855 if (*((int *)__cil_tmp209)) { 2856 { 2857#line 90 2858 __cil_tmp210 = (unsigned long )pi; 2859#line 90 2860 __cil_tmp211 = __cil_tmp210 + 16; 2861#line 90 2862 __cil_tmp212 = *((int *)__cil_tmp211); 2863#line 90 2864 __cil_tmp213 = (unsigned long )__cil_tmp212; 2865#line 90 2866 __udelay(__cil_tmp213); 2867 } 2868 } else { 2869 2870 } 2871 } 2872 { 2873#line 90 2874 __cil_tmp214 = (unsigned long )pi; 2875#line 90 2876 __cil_tmp215 = __cil_tmp214 + 8; 2877#line 90 2878 __cil_tmp216 = *((int *)__cil_tmp215); 2879#line 90 2880 __cil_tmp217 = __cil_tmp216 + 2; 2881#line 90 2882 outb((unsigned char)38, __cil_tmp217); 2883 } 2884 { 2885#line 90 2886 __cil_tmp218 = (unsigned long )pi; 2887#line 90 2888 __cil_tmp219 = __cil_tmp218 + 16; 2889#line 90 2890 if (*((int *)__cil_tmp219)) { 2891 { 2892#line 90 2893 __cil_tmp220 = (unsigned long )pi; 2894#line 90 2895 __cil_tmp221 = __cil_tmp220 + 16; 2896#line 90 2897 __cil_tmp222 = *((int *)__cil_tmp221); 2898#line 90 2899 __cil_tmp223 = (unsigned long )__cil_tmp222; 2900#line 90 2901 __udelay(__cil_tmp223); 2902 } 2903 } else { 2904 2905 } 2906 } 2907 { 2908#line 90 2909 __cil_tmp224 = (unsigned long )pi; 2910#line 90 2911 __cil_tmp225 = __cil_tmp224 + 8; 2912#line 90 2913 __cil_tmp226 = *((int *)__cil_tmp225); 2914#line 90 2915 __cil_tmp227 = __cil_tmp226 + 2; 2916#line 90 2917 outb((unsigned char)34, __cil_tmp227); 2918 } 2919 { 2920#line 90 2921 __cil_tmp228 = (unsigned long )pi; 2922#line 90 2923 __cil_tmp229 = __cil_tmp228 + 16; 2924#line 90 2925 if (*((int *)__cil_tmp229)) { 2926 { 2927#line 90 2928 __cil_tmp230 = (unsigned long )pi; 2929#line 90 2930 __cil_tmp231 = __cil_tmp230 + 16; 2931#line 90 2932 __cil_tmp232 = *((int *)__cil_tmp231); 2933#line 90 2934 __cil_tmp233 = (unsigned long )__cil_tmp232; 2935#line 90 2936 __udelay(__cil_tmp233); 2937 } 2938 } else { 2939 2940 } 2941 } 2942 { 2943#line 91 2944 __cil_tmp234 = (unsigned long )pi; 2945#line 91 2946 __cil_tmp235 = __cil_tmp234 + 16; 2947#line 91 2948 if (*((int *)__cil_tmp235)) { 2949 { 2950#line 91 2951 __cil_tmp236 = (unsigned long )pi; 2952#line 91 2953 __cil_tmp237 = __cil_tmp236 + 16; 2954#line 91 2955 __cil_tmp238 = *((int *)__cil_tmp237); 2956#line 91 2957 __cil_tmp239 = (unsigned long )__cil_tmp238; 2958#line 91 2959 __udelay(__cil_tmp239); 2960 } 2961 } else { 2962 2963 } 2964 } 2965 { 2966#line 91 2967 __cil_tmp240 = (unsigned long )pi; 2968#line 91 2969 __cil_tmp241 = __cil_tmp240 + 8; 2970#line 91 2971 __cil_tmp242 = *((int *)__cil_tmp241); 2972#line 91 2973 tmp___3 = inb(__cil_tmp242); 2974#line 91 2975 __cil_tmp243 = (int )tmp___3; 2976#line 91 2977 a = __cil_tmp243 & 255; 2978#line 91 2979 __cil_tmp244 = (unsigned long )pi; 2980#line 91 2981 __cil_tmp245 = __cil_tmp244 + 8; 2982#line 91 2983 __cil_tmp246 = *((int *)__cil_tmp245); 2984#line 91 2985 __cil_tmp247 = __cil_tmp246 + 2; 2986#line 91 2987 outb((unsigned char)32, __cil_tmp247); 2988 } 2989 { 2990#line 91 2991 __cil_tmp248 = (unsigned long )pi; 2992#line 91 2993 __cil_tmp249 = __cil_tmp248 + 16; 2994#line 91 2995 if (*((int *)__cil_tmp249)) { 2996 { 2997#line 91 2998 __cil_tmp250 = (unsigned long )pi; 2999#line 91 3000 __cil_tmp251 = __cil_tmp250 + 16; 3001#line 91 3002 __cil_tmp252 = *((int *)__cil_tmp251); 3003#line 91 3004 __cil_tmp253 = (unsigned long )__cil_tmp252; 3005#line 91 3006 __udelay(__cil_tmp253); 3007 } 3008 } else { 3009 3010 } 3011 } 3012 { 3013#line 91 3014 __cil_tmp254 = (unsigned long )pi; 3015#line 91 3016 __cil_tmp255 = __cil_tmp254 + 16; 3017#line 91 3018 if (*((int *)__cil_tmp255)) { 3019 { 3020#line 91 3021 __cil_tmp256 = (unsigned long )pi; 3022#line 91 3023 __cil_tmp257 = __cil_tmp256 + 16; 3024#line 91 3025 __cil_tmp258 = *((int *)__cil_tmp257); 3026#line 91 3027 __cil_tmp259 = (unsigned long )__cil_tmp258; 3028#line 91 3029 __udelay(__cil_tmp259); 3030 } 3031 } else { 3032 3033 } 3034 } 3035 { 3036#line 91 3037 __cil_tmp260 = (unsigned long )pi; 3038#line 91 3039 __cil_tmp261 = __cil_tmp260 + 8; 3040#line 91 3041 __cil_tmp262 = *((int *)__cil_tmp261); 3042#line 91 3043 tmp___4 = inb(__cil_tmp262); 3044#line 91 3045 __cil_tmp263 = (int )tmp___4; 3046#line 91 3047 b = __cil_tmp263 & 255; 3048#line 92 3049 __cil_tmp264 = 2 * k; 3050#line 92 3051 __cil_tmp265 = buf + __cil_tmp264; 3052#line 92 3053 *__cil_tmp265 = (char )b; 3054#line 92 3055 __cil_tmp266 = 2 * k; 3056#line 92 3057 __cil_tmp267 = __cil_tmp266 + 1; 3058#line 92 3059 __cil_tmp268 = buf + __cil_tmp267; 3060#line 92 3061 *__cil_tmp268 = (char )a; 3062#line 89 3063 k = k + 1; 3064 } 3065 } 3066 while_break___0: /* CIL Label */ ; 3067 } 3068 { 3069#line 94 3070 __cil_tmp269 = (unsigned long )pi; 3071#line 94 3072 __cil_tmp270 = __cil_tmp269 + 8; 3073#line 94 3074 __cil_tmp271 = *((int *)__cil_tmp270); 3075#line 94 3076 __cil_tmp272 = __cil_tmp271 + 2; 3077#line 94 3078 outb((unsigned char)38, __cil_tmp272); 3079 } 3080 { 3081#line 94 3082 __cil_tmp273 = (unsigned long )pi; 3083#line 94 3084 __cil_tmp274 = __cil_tmp273 + 16; 3085#line 94 3086 if (*((int *)__cil_tmp274)) { 3087 { 3088#line 94 3089 __cil_tmp275 = (unsigned long )pi; 3090#line 94 3091 __cil_tmp276 = __cil_tmp275 + 16; 3092#line 94 3093 __cil_tmp277 = *((int *)__cil_tmp276); 3094#line 94 3095 __cil_tmp278 = (unsigned long )__cil_tmp277; 3096#line 94 3097 __udelay(__cil_tmp278); 3098 } 3099 } else { 3100 3101 } 3102 } 3103 { 3104#line 94 3105 __cil_tmp279 = (unsigned long )pi; 3106#line 94 3107 __cil_tmp280 = __cil_tmp279 + 8; 3108#line 94 3109 __cil_tmp281 = *((int *)__cil_tmp280); 3110#line 94 3111 __cil_tmp282 = __cil_tmp281 + 2; 3112#line 94 3113 outb((unsigned char)12, __cil_tmp282); 3114 } 3115 { 3116#line 94 3117 __cil_tmp283 = (unsigned long )pi; 3118#line 94 3119 __cil_tmp284 = __cil_tmp283 + 16; 3120#line 94 3121 if (*((int *)__cil_tmp284)) { 3122 { 3123#line 94 3124 __cil_tmp285 = (unsigned long )pi; 3125#line 94 3126 __cil_tmp286 = __cil_tmp285 + 16; 3127#line 94 3128 __cil_tmp287 = *((int *)__cil_tmp286); 3129#line 94 3130 __cil_tmp288 = (unsigned long )__cil_tmp287; 3131#line 94 3132 __udelay(__cil_tmp288); 3133 } 3134 } else { 3135 3136 } 3137 } 3138#line 95 3139 goto switch_break; 3140 } else { 3141 switch_break: /* CIL Label */ ; 3142 } 3143 } 3144#line 97 3145 return; 3146} 3147} 3148#line 99 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 3149static void aten_write_block(PIA *pi , char *buf , int count ) 3150{ int k ; 3151 unsigned long __cil_tmp5 ; 3152 unsigned long __cil_tmp6 ; 3153 int __cil_tmp7 ; 3154 unsigned long __cil_tmp8 ; 3155 unsigned long __cil_tmp9 ; 3156 unsigned long __cil_tmp10 ; 3157 unsigned long __cil_tmp11 ; 3158 int __cil_tmp12 ; 3159 unsigned long __cil_tmp13 ; 3160 unsigned long __cil_tmp14 ; 3161 unsigned long __cil_tmp15 ; 3162 int __cil_tmp16 ; 3163 int __cil_tmp17 ; 3164 unsigned long __cil_tmp18 ; 3165 unsigned long __cil_tmp19 ; 3166 unsigned long __cil_tmp20 ; 3167 unsigned long __cil_tmp21 ; 3168 int __cil_tmp22 ; 3169 unsigned long __cil_tmp23 ; 3170 unsigned long __cil_tmp24 ; 3171 unsigned long __cil_tmp25 ; 3172 int __cil_tmp26 ; 3173 int __cil_tmp27 ; 3174 unsigned long __cil_tmp28 ; 3175 unsigned long __cil_tmp29 ; 3176 unsigned long __cil_tmp30 ; 3177 unsigned long __cil_tmp31 ; 3178 int __cil_tmp32 ; 3179 unsigned long __cil_tmp33 ; 3180 int __cil_tmp34 ; 3181 int __cil_tmp35 ; 3182 int __cil_tmp36 ; 3183 char *__cil_tmp37 ; 3184 char __cil_tmp38 ; 3185 unsigned char __cil_tmp39 ; 3186 unsigned long __cil_tmp40 ; 3187 unsigned long __cil_tmp41 ; 3188 int __cil_tmp42 ; 3189 unsigned long __cil_tmp43 ; 3190 unsigned long __cil_tmp44 ; 3191 unsigned long __cil_tmp45 ; 3192 unsigned long __cil_tmp46 ; 3193 int __cil_tmp47 ; 3194 unsigned long __cil_tmp48 ; 3195 unsigned long __cil_tmp49 ; 3196 unsigned long __cil_tmp50 ; 3197 int __cil_tmp51 ; 3198 int __cil_tmp52 ; 3199 unsigned long __cil_tmp53 ; 3200 unsigned long __cil_tmp54 ; 3201 unsigned long __cil_tmp55 ; 3202 unsigned long __cil_tmp56 ; 3203 int __cil_tmp57 ; 3204 unsigned long __cil_tmp58 ; 3205 unsigned long __cil_tmp59 ; 3206 unsigned long __cil_tmp60 ; 3207 int __cil_tmp61 ; 3208 int __cil_tmp62 ; 3209 unsigned long __cil_tmp63 ; 3210 unsigned long __cil_tmp64 ; 3211 unsigned long __cil_tmp65 ; 3212 unsigned long __cil_tmp66 ; 3213 int __cil_tmp67 ; 3214 unsigned long __cil_tmp68 ; 3215 int __cil_tmp69 ; 3216 char *__cil_tmp70 ; 3217 char __cil_tmp71 ; 3218 unsigned char __cil_tmp72 ; 3219 unsigned long __cil_tmp73 ; 3220 unsigned long __cil_tmp74 ; 3221 int __cil_tmp75 ; 3222 unsigned long __cil_tmp76 ; 3223 unsigned long __cil_tmp77 ; 3224 unsigned long __cil_tmp78 ; 3225 unsigned long __cil_tmp79 ; 3226 int __cil_tmp80 ; 3227 unsigned long __cil_tmp81 ; 3228 unsigned long __cil_tmp82 ; 3229 unsigned long __cil_tmp83 ; 3230 int __cil_tmp84 ; 3231 int __cil_tmp85 ; 3232 unsigned long __cil_tmp86 ; 3233 unsigned long __cil_tmp87 ; 3234 unsigned long __cil_tmp88 ; 3235 unsigned long __cil_tmp89 ; 3236 int __cil_tmp90 ; 3237 unsigned long __cil_tmp91 ; 3238 unsigned long __cil_tmp92 ; 3239 unsigned long __cil_tmp93 ; 3240 int __cil_tmp94 ; 3241 int __cil_tmp95 ; 3242 unsigned long __cil_tmp96 ; 3243 unsigned long __cil_tmp97 ; 3244 unsigned long __cil_tmp98 ; 3245 unsigned long __cil_tmp99 ; 3246 int __cil_tmp100 ; 3247 unsigned long __cil_tmp101 ; 3248 unsigned long __cil_tmp102 ; 3249 unsigned long __cil_tmp103 ; 3250 int __cil_tmp104 ; 3251 int __cil_tmp105 ; 3252 unsigned long __cil_tmp106 ; 3253 unsigned long __cil_tmp107 ; 3254 unsigned long __cil_tmp108 ; 3255 unsigned long __cil_tmp109 ; 3256 int __cil_tmp110 ; 3257 unsigned long __cil_tmp111 ; 3258 3259 { 3260 { 3261#line 103 3262 __cil_tmp5 = (unsigned long )pi; 3263#line 103 3264 __cil_tmp6 = __cil_tmp5 + 8; 3265#line 103 3266 __cil_tmp7 = *((int *)__cil_tmp6); 3267#line 103 3268 outb((unsigned char)136, __cil_tmp7); 3269 } 3270 { 3271#line 103 3272 __cil_tmp8 = (unsigned long )pi; 3273#line 103 3274 __cil_tmp9 = __cil_tmp8 + 16; 3275#line 103 3276 if (*((int *)__cil_tmp9)) { 3277 { 3278#line 103 3279 __cil_tmp10 = (unsigned long )pi; 3280#line 103 3281 __cil_tmp11 = __cil_tmp10 + 16; 3282#line 103 3283 __cil_tmp12 = *((int *)__cil_tmp11); 3284#line 103 3285 __cil_tmp13 = (unsigned long )__cil_tmp12; 3286#line 103 3287 __udelay(__cil_tmp13); 3288 } 3289 } else { 3290 3291 } 3292 } 3293 { 3294#line 103 3295 __cil_tmp14 = (unsigned long )pi; 3296#line 103 3297 __cil_tmp15 = __cil_tmp14 + 8; 3298#line 103 3299 __cil_tmp16 = *((int *)__cil_tmp15); 3300#line 103 3301 __cil_tmp17 = __cil_tmp16 + 2; 3302#line 103 3303 outb((unsigned char)14, __cil_tmp17); 3304 } 3305 { 3306#line 103 3307 __cil_tmp18 = (unsigned long )pi; 3308#line 103 3309 __cil_tmp19 = __cil_tmp18 + 16; 3310#line 103 3311 if (*((int *)__cil_tmp19)) { 3312 { 3313#line 103 3314 __cil_tmp20 = (unsigned long )pi; 3315#line 103 3316 __cil_tmp21 = __cil_tmp20 + 16; 3317#line 103 3318 __cil_tmp22 = *((int *)__cil_tmp21); 3319#line 103 3320 __cil_tmp23 = (unsigned long )__cil_tmp22; 3321#line 103 3322 __udelay(__cil_tmp23); 3323 } 3324 } else { 3325 3326 } 3327 } 3328 { 3329#line 103 3330 __cil_tmp24 = (unsigned long )pi; 3331#line 103 3332 __cil_tmp25 = __cil_tmp24 + 8; 3333#line 103 3334 __cil_tmp26 = *((int *)__cil_tmp25); 3335#line 103 3336 __cil_tmp27 = __cil_tmp26 + 2; 3337#line 103 3338 outb((unsigned char)6, __cil_tmp27); 3339 } 3340 { 3341#line 103 3342 __cil_tmp28 = (unsigned long )pi; 3343#line 103 3344 __cil_tmp29 = __cil_tmp28 + 16; 3345#line 103 3346 if (*((int *)__cil_tmp29)) { 3347 { 3348#line 103 3349 __cil_tmp30 = (unsigned long )pi; 3350#line 103 3351 __cil_tmp31 = __cil_tmp30 + 16; 3352#line 103 3353 __cil_tmp32 = *((int *)__cil_tmp31); 3354#line 103 3355 __cil_tmp33 = (unsigned long )__cil_tmp32; 3356#line 103 3357 __udelay(__cil_tmp33); 3358 } 3359 } else { 3360 3361 } 3362 } 3363#line 104 3364 k = 0; 3365 { 3366#line 104 3367 while (1) { 3368 while_continue: /* CIL Label */ ; 3369 { 3370#line 104 3371 __cil_tmp34 = count / 2; 3372#line 104 3373 if (k < __cil_tmp34) { 3374 3375 } else { 3376#line 104 3377 goto while_break; 3378 } 3379 } 3380 { 3381#line 105 3382 __cil_tmp35 = 2 * k; 3383#line 105 3384 __cil_tmp36 = __cil_tmp35 + 1; 3385#line 105 3386 __cil_tmp37 = buf + __cil_tmp36; 3387#line 105 3388 __cil_tmp38 = *__cil_tmp37; 3389#line 105 3390 __cil_tmp39 = (unsigned char )__cil_tmp38; 3391#line 105 3392 __cil_tmp40 = (unsigned long )pi; 3393#line 105 3394 __cil_tmp41 = __cil_tmp40 + 8; 3395#line 105 3396 __cil_tmp42 = *((int *)__cil_tmp41); 3397#line 105 3398 outb(__cil_tmp39, __cil_tmp42); 3399 } 3400 { 3401#line 105 3402 __cil_tmp43 = (unsigned long )pi; 3403#line 105 3404 __cil_tmp44 = __cil_tmp43 + 16; 3405#line 105 3406 if (*((int *)__cil_tmp44)) { 3407 { 3408#line 105 3409 __cil_tmp45 = (unsigned long )pi; 3410#line 105 3411 __cil_tmp46 = __cil_tmp45 + 16; 3412#line 105 3413 __cil_tmp47 = *((int *)__cil_tmp46); 3414#line 105 3415 __cil_tmp48 = (unsigned long )__cil_tmp47; 3416#line 105 3417 __udelay(__cil_tmp48); 3418 } 3419 } else { 3420 3421 } 3422 } 3423 { 3424#line 105 3425 __cil_tmp49 = (unsigned long )pi; 3426#line 105 3427 __cil_tmp50 = __cil_tmp49 + 8; 3428#line 105 3429 __cil_tmp51 = *((int *)__cil_tmp50); 3430#line 105 3431 __cil_tmp52 = __cil_tmp51 + 2; 3432#line 105 3433 outb((unsigned char)14, __cil_tmp52); 3434 } 3435 { 3436#line 105 3437 __cil_tmp53 = (unsigned long )pi; 3438#line 105 3439 __cil_tmp54 = __cil_tmp53 + 16; 3440#line 105 3441 if (*((int *)__cil_tmp54)) { 3442 { 3443#line 105 3444 __cil_tmp55 = (unsigned long )pi; 3445#line 105 3446 __cil_tmp56 = __cil_tmp55 + 16; 3447#line 105 3448 __cil_tmp57 = *((int *)__cil_tmp56); 3449#line 105 3450 __cil_tmp58 = (unsigned long )__cil_tmp57; 3451#line 105 3452 __udelay(__cil_tmp58); 3453 } 3454 } else { 3455 3456 } 3457 } 3458 { 3459#line 105 3460 __cil_tmp59 = (unsigned long )pi; 3461#line 105 3462 __cil_tmp60 = __cil_tmp59 + 8; 3463#line 105 3464 __cil_tmp61 = *((int *)__cil_tmp60); 3465#line 105 3466 __cil_tmp62 = __cil_tmp61 + 2; 3467#line 105 3468 outb((unsigned char)6, __cil_tmp62); 3469 } 3470 { 3471#line 105 3472 __cil_tmp63 = (unsigned long )pi; 3473#line 105 3474 __cil_tmp64 = __cil_tmp63 + 16; 3475#line 105 3476 if (*((int *)__cil_tmp64)) { 3477 { 3478#line 105 3479 __cil_tmp65 = (unsigned long )pi; 3480#line 105 3481 __cil_tmp66 = __cil_tmp65 + 16; 3482#line 105 3483 __cil_tmp67 = *((int *)__cil_tmp66); 3484#line 105 3485 __cil_tmp68 = (unsigned long )__cil_tmp67; 3486#line 105 3487 __udelay(__cil_tmp68); 3488 } 3489 } else { 3490 3491 } 3492 } 3493 { 3494#line 106 3495 __cil_tmp69 = 2 * k; 3496#line 106 3497 __cil_tmp70 = buf + __cil_tmp69; 3498#line 106 3499 __cil_tmp71 = *__cil_tmp70; 3500#line 106 3501 __cil_tmp72 = (unsigned char )__cil_tmp71; 3502#line 106 3503 __cil_tmp73 = (unsigned long )pi; 3504#line 106 3505 __cil_tmp74 = __cil_tmp73 + 8; 3506#line 106 3507 __cil_tmp75 = *((int *)__cil_tmp74); 3508#line 106 3509 outb(__cil_tmp72, __cil_tmp75); 3510 } 3511 { 3512#line 106 3513 __cil_tmp76 = (unsigned long )pi; 3514#line 106 3515 __cil_tmp77 = __cil_tmp76 + 16; 3516#line 106 3517 if (*((int *)__cil_tmp77)) { 3518 { 3519#line 106 3520 __cil_tmp78 = (unsigned long )pi; 3521#line 106 3522 __cil_tmp79 = __cil_tmp78 + 16; 3523#line 106 3524 __cil_tmp80 = *((int *)__cil_tmp79); 3525#line 106 3526 __cil_tmp81 = (unsigned long )__cil_tmp80; 3527#line 106 3528 __udelay(__cil_tmp81); 3529 } 3530 } else { 3531 3532 } 3533 } 3534 { 3535#line 106 3536 __cil_tmp82 = (unsigned long )pi; 3537#line 106 3538 __cil_tmp83 = __cil_tmp82 + 8; 3539#line 106 3540 __cil_tmp84 = *((int *)__cil_tmp83); 3541#line 106 3542 __cil_tmp85 = __cil_tmp84 + 2; 3543#line 106 3544 outb((unsigned char)7, __cil_tmp85); 3545 } 3546 { 3547#line 106 3548 __cil_tmp86 = (unsigned long )pi; 3549#line 106 3550 __cil_tmp87 = __cil_tmp86 + 16; 3551#line 106 3552 if (*((int *)__cil_tmp87)) { 3553 { 3554#line 106 3555 __cil_tmp88 = (unsigned long )pi; 3556#line 106 3557 __cil_tmp89 = __cil_tmp88 + 16; 3558#line 106 3559 __cil_tmp90 = *((int *)__cil_tmp89); 3560#line 106 3561 __cil_tmp91 = (unsigned long )__cil_tmp90; 3562#line 106 3563 __udelay(__cil_tmp91); 3564 } 3565 } else { 3566 3567 } 3568 } 3569 { 3570#line 106 3571 __cil_tmp92 = (unsigned long )pi; 3572#line 106 3573 __cil_tmp93 = __cil_tmp92 + 8; 3574#line 106 3575 __cil_tmp94 = *((int *)__cil_tmp93); 3576#line 106 3577 __cil_tmp95 = __cil_tmp94 + 2; 3578#line 106 3579 outb((unsigned char)6, __cil_tmp95); 3580 } 3581 { 3582#line 106 3583 __cil_tmp96 = (unsigned long )pi; 3584#line 106 3585 __cil_tmp97 = __cil_tmp96 + 16; 3586#line 106 3587 if (*((int *)__cil_tmp97)) { 3588 { 3589#line 106 3590 __cil_tmp98 = (unsigned long )pi; 3591#line 106 3592 __cil_tmp99 = __cil_tmp98 + 16; 3593#line 106 3594 __cil_tmp100 = *((int *)__cil_tmp99); 3595#line 106 3596 __cil_tmp101 = (unsigned long )__cil_tmp100; 3597#line 106 3598 __udelay(__cil_tmp101); 3599 } 3600 } else { 3601 3602 } 3603 } 3604#line 104 3605 k = k + 1; 3606 } 3607 while_break: /* CIL Label */ ; 3608 } 3609 { 3610#line 108 3611 __cil_tmp102 = (unsigned long )pi; 3612#line 108 3613 __cil_tmp103 = __cil_tmp102 + 8; 3614#line 108 3615 __cil_tmp104 = *((int *)__cil_tmp103); 3616#line 108 3617 __cil_tmp105 = __cil_tmp104 + 2; 3618#line 108 3619 outb((unsigned char)12, __cil_tmp105); 3620 } 3621 { 3622#line 108 3623 __cil_tmp106 = (unsigned long )pi; 3624#line 108 3625 __cil_tmp107 = __cil_tmp106 + 16; 3626#line 108 3627 if (*((int *)__cil_tmp107)) { 3628 { 3629#line 108 3630 __cil_tmp108 = (unsigned long )pi; 3631#line 108 3632 __cil_tmp109 = __cil_tmp108 + 16; 3633#line 108 3634 __cil_tmp110 = *((int *)__cil_tmp109); 3635#line 108 3636 __cil_tmp111 = (unsigned long )__cil_tmp110; 3637#line 108 3638 __udelay(__cil_tmp111); 3639 } 3640 } else { 3641 3642 } 3643 } 3644#line 109 3645 return; 3646} 3647} 3648#line 111 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 3649static void aten_connect(PIA *pi ) 3650{ unsigned char tmp ; 3651 unsigned char tmp___0 ; 3652 unsigned long __cil_tmp4 ; 3653 unsigned long __cil_tmp5 ; 3654 unsigned long __cil_tmp6 ; 3655 unsigned long __cil_tmp7 ; 3656 int __cil_tmp8 ; 3657 unsigned long __cil_tmp9 ; 3658 unsigned long __cil_tmp10 ; 3659 unsigned long __cil_tmp11 ; 3660 int __cil_tmp12 ; 3661 unsigned long __cil_tmp13 ; 3662 unsigned long __cil_tmp14 ; 3663 int __cil_tmp15 ; 3664 unsigned long __cil_tmp16 ; 3665 unsigned long __cil_tmp17 ; 3666 unsigned long __cil_tmp18 ; 3667 unsigned long __cil_tmp19 ; 3668 int __cil_tmp20 ; 3669 unsigned long __cil_tmp21 ; 3670 unsigned long __cil_tmp22 ; 3671 unsigned long __cil_tmp23 ; 3672 int __cil_tmp24 ; 3673 int __cil_tmp25 ; 3674 unsigned long __cil_tmp26 ; 3675 unsigned long __cil_tmp27 ; 3676 int __cil_tmp28 ; 3677 unsigned long __cil_tmp29 ; 3678 unsigned long __cil_tmp30 ; 3679 int __cil_tmp31 ; 3680 int __cil_tmp32 ; 3681 unsigned long __cil_tmp33 ; 3682 unsigned long __cil_tmp34 ; 3683 unsigned long __cil_tmp35 ; 3684 unsigned long __cil_tmp36 ; 3685 int __cil_tmp37 ; 3686 unsigned long __cil_tmp38 ; 3687 3688 { 3689 { 3690#line 113 3691 __cil_tmp4 = (unsigned long )pi; 3692#line 113 3693 __cil_tmp5 = __cil_tmp4 + 16; 3694#line 113 3695 if (*((int *)__cil_tmp5)) { 3696 { 3697#line 113 3698 __cil_tmp6 = (unsigned long )pi; 3699#line 113 3700 __cil_tmp7 = __cil_tmp6 + 16; 3701#line 113 3702 __cil_tmp8 = *((int *)__cil_tmp7); 3703#line 113 3704 __cil_tmp9 = (unsigned long )__cil_tmp8; 3705#line 113 3706 __udelay(__cil_tmp9); 3707 } 3708 } else { 3709 3710 } 3711 } 3712 { 3713#line 113 3714 __cil_tmp10 = (unsigned long )pi; 3715#line 113 3716 __cil_tmp11 = __cil_tmp10 + 8; 3717#line 113 3718 __cil_tmp12 = *((int *)__cil_tmp11); 3719#line 113 3720 tmp = inb(__cil_tmp12); 3721#line 113 3722 __cil_tmp13 = (unsigned long )pi; 3723#line 113 3724 __cil_tmp14 = __cil_tmp13 + 36; 3725#line 113 3726 __cil_tmp15 = (int )tmp; 3727#line 113 3728 *((int *)__cil_tmp14) = __cil_tmp15 & 255; 3729 } 3730 { 3731#line 114 3732 __cil_tmp16 = (unsigned long )pi; 3733#line 114 3734 __cil_tmp17 = __cil_tmp16 + 16; 3735#line 114 3736 if (*((int *)__cil_tmp17)) { 3737 { 3738#line 114 3739 __cil_tmp18 = (unsigned long )pi; 3740#line 114 3741 __cil_tmp19 = __cil_tmp18 + 16; 3742#line 114 3743 __cil_tmp20 = *((int *)__cil_tmp19); 3744#line 114 3745 __cil_tmp21 = (unsigned long )__cil_tmp20; 3746#line 114 3747 __udelay(__cil_tmp21); 3748 } 3749 } else { 3750 3751 } 3752 } 3753 { 3754#line 114 3755 __cil_tmp22 = (unsigned long )pi; 3756#line 114 3757 __cil_tmp23 = __cil_tmp22 + 8; 3758#line 114 3759 __cil_tmp24 = *((int *)__cil_tmp23); 3760#line 114 3761 __cil_tmp25 = __cil_tmp24 + 2; 3762#line 114 3763 tmp___0 = inb(__cil_tmp25); 3764#line 114 3765 __cil_tmp26 = (unsigned long )pi; 3766#line 114 3767 __cil_tmp27 = __cil_tmp26 + 40; 3768#line 114 3769 __cil_tmp28 = (int )tmp___0; 3770#line 114 3771 *((int *)__cil_tmp27) = __cil_tmp28 & 255; 3772#line 115 3773 __cil_tmp29 = (unsigned long )pi; 3774#line 115 3775 __cil_tmp30 = __cil_tmp29 + 8; 3776#line 115 3777 __cil_tmp31 = *((int *)__cil_tmp30); 3778#line 115 3779 __cil_tmp32 = __cil_tmp31 + 2; 3780#line 115 3781 outb((unsigned char)12, __cil_tmp32); 3782 } 3783 { 3784#line 115 3785 __cil_tmp33 = (unsigned long )pi; 3786#line 115 3787 __cil_tmp34 = __cil_tmp33 + 16; 3788#line 115 3789 if (*((int *)__cil_tmp34)) { 3790 { 3791#line 115 3792 __cil_tmp35 = (unsigned long )pi; 3793#line 115 3794 __cil_tmp36 = __cil_tmp35 + 16; 3795#line 115 3796 __cil_tmp37 = *((int *)__cil_tmp36); 3797#line 115 3798 __cil_tmp38 = (unsigned long )__cil_tmp37; 3799#line 115 3800 __udelay(__cil_tmp38); 3801 } 3802 } else { 3803 3804 } 3805 } 3806#line 116 3807 return; 3808} 3809} 3810#line 118 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 3811static void aten_disconnect(PIA *pi ) 3812{ unsigned long __cil_tmp2 ; 3813 unsigned long __cil_tmp3 ; 3814 int __cil_tmp4 ; 3815 unsigned char __cil_tmp5 ; 3816 unsigned long __cil_tmp6 ; 3817 unsigned long __cil_tmp7 ; 3818 int __cil_tmp8 ; 3819 unsigned long __cil_tmp9 ; 3820 unsigned long __cil_tmp10 ; 3821 unsigned long __cil_tmp11 ; 3822 unsigned long __cil_tmp12 ; 3823 int __cil_tmp13 ; 3824 unsigned long __cil_tmp14 ; 3825 unsigned long __cil_tmp15 ; 3826 unsigned long __cil_tmp16 ; 3827 int __cil_tmp17 ; 3828 unsigned char __cil_tmp18 ; 3829 unsigned long __cil_tmp19 ; 3830 unsigned long __cil_tmp20 ; 3831 int __cil_tmp21 ; 3832 int __cil_tmp22 ; 3833 unsigned long __cil_tmp23 ; 3834 unsigned long __cil_tmp24 ; 3835 unsigned long __cil_tmp25 ; 3836 unsigned long __cil_tmp26 ; 3837 int __cil_tmp27 ; 3838 unsigned long __cil_tmp28 ; 3839 3840 { 3841 { 3842#line 120 3843 __cil_tmp2 = (unsigned long )pi; 3844#line 120 3845 __cil_tmp3 = __cil_tmp2 + 36; 3846#line 120 3847 __cil_tmp4 = *((int *)__cil_tmp3); 3848#line 120 3849 __cil_tmp5 = (unsigned char )__cil_tmp4; 3850#line 120 3851 __cil_tmp6 = (unsigned long )pi; 3852#line 120 3853 __cil_tmp7 = __cil_tmp6 + 8; 3854#line 120 3855 __cil_tmp8 = *((int *)__cil_tmp7); 3856#line 120 3857 outb(__cil_tmp5, __cil_tmp8); 3858 } 3859 { 3860#line 120 3861 __cil_tmp9 = (unsigned long )pi; 3862#line 120 3863 __cil_tmp10 = __cil_tmp9 + 16; 3864#line 120 3865 if (*((int *)__cil_tmp10)) { 3866 { 3867#line 120 3868 __cil_tmp11 = (unsigned long )pi; 3869#line 120 3870 __cil_tmp12 = __cil_tmp11 + 16; 3871#line 120 3872 __cil_tmp13 = *((int *)__cil_tmp12); 3873#line 120 3874 __cil_tmp14 = (unsigned long )__cil_tmp13; 3875#line 120 3876 __udelay(__cil_tmp14); 3877 } 3878 } else { 3879 3880 } 3881 } 3882 { 3883#line 121 3884 __cil_tmp15 = (unsigned long )pi; 3885#line 121 3886 __cil_tmp16 = __cil_tmp15 + 40; 3887#line 121 3888 __cil_tmp17 = *((int *)__cil_tmp16); 3889#line 121 3890 __cil_tmp18 = (unsigned char )__cil_tmp17; 3891#line 121 3892 __cil_tmp19 = (unsigned long )pi; 3893#line 121 3894 __cil_tmp20 = __cil_tmp19 + 8; 3895#line 121 3896 __cil_tmp21 = *((int *)__cil_tmp20); 3897#line 121 3898 __cil_tmp22 = __cil_tmp21 + 2; 3899#line 121 3900 outb(__cil_tmp18, __cil_tmp22); 3901 } 3902 { 3903#line 121 3904 __cil_tmp23 = (unsigned long )pi; 3905#line 121 3906 __cil_tmp24 = __cil_tmp23 + 16; 3907#line 121 3908 if (*((int *)__cil_tmp24)) { 3909 { 3910#line 121 3911 __cil_tmp25 = (unsigned long )pi; 3912#line 121 3913 __cil_tmp26 = __cil_tmp25 + 16; 3914#line 121 3915 __cil_tmp27 = *((int *)__cil_tmp26); 3916#line 121 3917 __cil_tmp28 = (unsigned long )__cil_tmp27; 3918#line 121 3919 __udelay(__cil_tmp28); 3920 } 3921 } else { 3922 3923 } 3924 } 3925#line 122 3926 return; 3927} 3928} 3929#line 124 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 3930static void aten_log_adapter(PIA *pi , char *scratch , int verbose ) 3931{ char *mode_string[2] ; 3932 unsigned long __cil_tmp5 ; 3933 unsigned long __cil_tmp6 ; 3934 unsigned long __cil_tmp7 ; 3935 unsigned long __cil_tmp8 ; 3936 unsigned long __cil_tmp9 ; 3937 unsigned long __cil_tmp10 ; 3938 char *__cil_tmp11 ; 3939 unsigned long __cil_tmp12 ; 3940 unsigned long __cil_tmp13 ; 3941 int __cil_tmp14 ; 3942 unsigned long __cil_tmp15 ; 3943 unsigned long __cil_tmp16 ; 3944 int __cil_tmp17 ; 3945 unsigned long __cil_tmp18 ; 3946 unsigned long __cil_tmp19 ; 3947 int __cil_tmp20 ; 3948 unsigned long __cil_tmp21 ; 3949 unsigned long __cil_tmp22 ; 3950 char *__cil_tmp23 ; 3951 unsigned long __cil_tmp24 ; 3952 unsigned long __cil_tmp25 ; 3953 int __cil_tmp26 ; 3954 3955 { 3956 { 3957#line 126 3958 __cil_tmp5 = 0 * 8UL; 3959#line 126 3960 __cil_tmp6 = (unsigned long )(mode_string) + __cil_tmp5; 3961#line 126 3962 *((char **)__cil_tmp6) = (char *)"4-bit"; 3963#line 126 3964 __cil_tmp7 = 1 * 8UL; 3965#line 126 3966 __cil_tmp8 = (unsigned long )(mode_string) + __cil_tmp7; 3967#line 126 3968 *((char **)__cil_tmp8) = (char *)"8-bit"; 3969#line 128 3970 __cil_tmp9 = (unsigned long )pi; 3971#line 128 3972 __cil_tmp10 = __cil_tmp9 + 24; 3973#line 128 3974 __cil_tmp11 = *((char **)__cil_tmp10); 3975#line 128 3976 __cil_tmp12 = (unsigned long )pi; 3977#line 128 3978 __cil_tmp13 = __cil_tmp12 + 8; 3979#line 128 3980 __cil_tmp14 = *((int *)__cil_tmp13); 3981#line 128 3982 printk("%s: aten %s, ATEN EH-100 at 0x%x, ", __cil_tmp11, "1.01", __cil_tmp14); 3983#line 130 3984 __cil_tmp15 = (unsigned long )pi; 3985#line 130 3986 __cil_tmp16 = __cil_tmp15 + 12; 3987#line 130 3988 __cil_tmp17 = *((int *)__cil_tmp16); 3989#line 130 3990 __cil_tmp18 = (unsigned long )pi; 3991#line 130 3992 __cil_tmp19 = __cil_tmp18 + 12; 3993#line 130 3994 __cil_tmp20 = *((int *)__cil_tmp19); 3995#line 130 3996 __cil_tmp21 = __cil_tmp20 * 8UL; 3997#line 130 3998 __cil_tmp22 = (unsigned long )(mode_string) + __cil_tmp21; 3999#line 130 4000 __cil_tmp23 = *((char **)__cil_tmp22); 4001#line 130 4002 __cil_tmp24 = (unsigned long )pi; 4003#line 130 4004 __cil_tmp25 = __cil_tmp24 + 16; 4005#line 130 4006 __cil_tmp26 = *((int *)__cil_tmp25); 4007#line 130 4008 printk("mode %d (%s), delay %d\n", __cil_tmp17, __cil_tmp23, __cil_tmp26); 4009 } 4010#line 133 4011 return; 4012} 4013} 4014#line 135 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 4015static struct pi_protocol aten = 4016#line 135 4017 {{(char )'a', (char )'t', (char )'e', (char )'n', (char )'\000', (char)0, (char)0, 4018 (char)0}, 0, 2, 2, 1, 1, & aten_write_regr, & aten_read_regr, & aten_write_block, 4019 & aten_read_block, & aten_connect, & aten_disconnect, (int (*)(PIA * ))0, (int (*)(PIA * ))0, 4020 (int (*)(PIA * , char * , int ))0, & aten_log_adapter, (int (*)(PIA * ))0, (void (*)(PIA * ))0, 4021 & __this_module}; 4022#line 151 4023static int aten_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ; 4024#line 151 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 4025static int aten_init(void) 4026{ int tmp ; 4027 4028 { 4029 { 4030#line 153 4031 tmp = paride_register(& aten); 4032 } 4033#line 153 4034 return (tmp); 4035} 4036} 4037#line 156 4038static void aten_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ; 4039#line 156 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 4040static void aten_exit(void) 4041{ 4042 4043 { 4044 { 4045#line 158 4046 paride_unregister(& aten); 4047 } 4048#line 159 4049 return; 4050} 4051} 4052#line 161 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 4053static char const __mod_license161[12] __attribute__((__used__, __unused__, __section__(".modinfo"), 4054__aligned__(1))) = 4055#line 161 4056 { (char const )'l', (char const )'i', (char const )'c', (char const )'e', 4057 (char const )'n', (char const )'s', (char const )'e', (char const )'=', 4058 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'}; 4059#line 162 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 4060int init_module(void) 4061{ int tmp ; 4062 4063 { 4064 { 4065#line 162 4066 tmp = aten_init(); 4067 } 4068#line 162 4069 return (tmp); 4070} 4071} 4072#line 163 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 4073void cleanup_module(void) 4074{ 4075 4076 { 4077 { 4078#line 163 4079 aten_exit(); 4080 } 4081#line 163 4082 return; 4083} 4084} 4085#line 181 4086void ldv_check_final_state(void) ; 4087#line 187 4088extern void ldv_initialize(void) ; 4089#line 190 4090extern int __VERIFIER_nondet_int(void) ; 4091#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 4092int LDV_IN_INTERRUPT ; 4093#line 196 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 4094void main(void) 4095{ PIA *var_aten_write_regr_0_p0 ; 4096 int var_aten_write_regr_0_p1 ; 4097 int var_aten_write_regr_0_p2 ; 4098 int var_aten_write_regr_0_p3 ; 4099 PIA *var_aten_read_regr_1_p0 ; 4100 int var_aten_read_regr_1_p1 ; 4101 int var_aten_read_regr_1_p2 ; 4102 PIA *var_aten_write_block_3_p0 ; 4103 char *var_aten_write_block_3_p1 ; 4104 int var_aten_write_block_3_p2 ; 4105 PIA *var_aten_read_block_2_p0 ; 4106 char *var_aten_read_block_2_p1 ; 4107 int var_aten_read_block_2_p2 ; 4108 PIA *var_aten_connect_4_p0 ; 4109 PIA *var_aten_disconnect_5_p0 ; 4110 PIA *var_aten_log_adapter_6_p0 ; 4111 char *var_aten_log_adapter_6_p1 ; 4112 int var_aten_log_adapter_6_p2 ; 4113 int tmp ; 4114 int ldv_s_aten_pi_protocol ; 4115 int tmp___0 ; 4116 int tmp___1 ; 4117 int __cil_tmp23 ; 4118 4119 { 4120 { 4121#line 281 4122 LDV_IN_INTERRUPT = 1; 4123#line 290 4124 ldv_initialize(); 4125#line 299 4126 tmp = aten_init(); 4127 } 4128#line 299 4129 if (tmp) { 4130#line 300 4131 goto ldv_final; 4132 } else { 4133 4134 } 4135#line 301 4136 ldv_s_aten_pi_protocol = 0; 4137 { 4138#line 305 4139 while (1) { 4140 while_continue: /* CIL Label */ ; 4141 { 4142#line 305 4143 tmp___1 = __VERIFIER_nondet_int(); 4144 } 4145#line 305 4146 if (tmp___1) { 4147 4148 } else { 4149 { 4150#line 305 4151 __cil_tmp23 = ldv_s_aten_pi_protocol == 0; 4152#line 305 4153 if (! __cil_tmp23) { 4154 4155 } else { 4156#line 305 4157 goto while_break; 4158 } 4159 } 4160 } 4161 { 4162#line 309 4163 tmp___0 = __VERIFIER_nondet_int(); 4164 } 4165#line 311 4166 if (tmp___0 == 0) { 4167#line 311 4168 goto case_0; 4169 } else 4170#line 330 4171 if (tmp___0 == 1) { 4172#line 330 4173 goto case_1; 4174 } else 4175#line 349 4176 if (tmp___0 == 2) { 4177#line 349 4178 goto case_2; 4179 } else 4180#line 368 4181 if (tmp___0 == 3) { 4182#line 368 4183 goto case_3; 4184 } else 4185#line 387 4186 if (tmp___0 == 4) { 4187#line 387 4188 goto case_4; 4189 } else 4190#line 406 4191 if (tmp___0 == 5) { 4192#line 406 4193 goto case_5; 4194 } else 4195#line 425 4196 if (tmp___0 == 6) { 4197#line 425 4198 goto case_6; 4199 } else { 4200 { 4201#line 444 4202 goto switch_default; 4203#line 309 4204 if (0) { 4205 case_0: /* CIL Label */ 4206#line 314 4207 if (ldv_s_aten_pi_protocol == 0) { 4208 { 4209#line 322 4210 aten_connect(var_aten_connect_4_p0); 4211#line 323 4212 ldv_s_aten_pi_protocol = ldv_s_aten_pi_protocol + 1; 4213 } 4214 } else { 4215 4216 } 4217#line 329 4218 goto switch_break; 4219 case_1: /* CIL Label */ 4220#line 333 4221 if (ldv_s_aten_pi_protocol == 1) { 4222 { 4223#line 341 4224 aten_disconnect(var_aten_disconnect_5_p0); 4225#line 342 4226 ldv_s_aten_pi_protocol = 0; 4227 } 4228 } else { 4229 4230 } 4231#line 348 4232 goto switch_break; 4233 case_2: /* CIL Label */ 4234 { 4235#line 360 4236 aten_write_regr(var_aten_write_regr_0_p0, var_aten_write_regr_0_p1, var_aten_write_regr_0_p2, 4237 var_aten_write_regr_0_p3); 4238 } 4239#line 367 4240 goto switch_break; 4241 case_3: /* CIL Label */ 4242 { 4243#line 379 4244 aten_read_regr(var_aten_read_regr_1_p0, var_aten_read_regr_1_p1, var_aten_read_regr_1_p2); 4245 } 4246#line 386 4247 goto switch_break; 4248 case_4: /* CIL Label */ 4249 { 4250#line 398 4251 aten_write_block(var_aten_write_block_3_p0, var_aten_write_block_3_p1, var_aten_write_block_3_p2); 4252 } 4253#line 405 4254 goto switch_break; 4255 case_5: /* CIL Label */ 4256 { 4257#line 417 4258 aten_read_block(var_aten_read_block_2_p0, var_aten_read_block_2_p1, var_aten_read_block_2_p2); 4259 } 4260#line 424 4261 goto switch_break; 4262 case_6: /* CIL Label */ 4263 { 4264#line 436 4265 aten_log_adapter(var_aten_log_adapter_6_p0, var_aten_log_adapter_6_p1, var_aten_log_adapter_6_p2); 4266 } 4267#line 443 4268 goto switch_break; 4269 switch_default: /* CIL Label */ 4270#line 444 4271 goto switch_break; 4272 } else { 4273 switch_break: /* CIL Label */ ; 4274 } 4275 } 4276 } 4277 } 4278 while_break: /* CIL Label */ ; 4279 } 4280 { 4281#line 459 4282 aten_exit(); 4283 } 4284 ldv_final: 4285 { 4286#line 462 4287 ldv_check_final_state(); 4288 } 4289#line 465 4290 return; 4291} 4292} 4293#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h" 4294void ldv_blast_assert(void) 4295{ 4296 4297 { 4298 ERROR: 4299#line 6 4300 goto ERROR; 4301} 4302} 4303#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h" 4304extern int __VERIFIER_nondet_int(void) ; 4305#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4306int ldv_mutex = 1; 4307#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4308int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) 4309{ int nondetermined ; 4310 4311 { 4312#line 29 4313 if (ldv_mutex == 1) { 4314 4315 } else { 4316 { 4317#line 29 4318 ldv_blast_assert(); 4319 } 4320 } 4321 { 4322#line 32 4323 nondetermined = __VERIFIER_nondet_int(); 4324 } 4325#line 35 4326 if (nondetermined) { 4327#line 38 4328 ldv_mutex = 2; 4329#line 40 4330 return (0); 4331 } else { 4332#line 45 4333 return (-4); 4334 } 4335} 4336} 4337#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4338int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) 4339{ int nondetermined ; 4340 4341 { 4342#line 57 4343 if (ldv_mutex == 1) { 4344 4345 } else { 4346 { 4347#line 57 4348 ldv_blast_assert(); 4349 } 4350 } 4351 { 4352#line 60 4353 nondetermined = __VERIFIER_nondet_int(); 4354 } 4355#line 63 4356 if (nondetermined) { 4357#line 66 4358 ldv_mutex = 2; 4359#line 68 4360 return (0); 4361 } else { 4362#line 73 4363 return (-4); 4364 } 4365} 4366} 4367#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4368int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 4369{ int atomic_value_after_dec ; 4370 4371 { 4372#line 83 4373 if (ldv_mutex == 1) { 4374 4375 } else { 4376 { 4377#line 83 4378 ldv_blast_assert(); 4379 } 4380 } 4381 { 4382#line 86 4383 atomic_value_after_dec = __VERIFIER_nondet_int(); 4384 } 4385#line 89 4386 if (atomic_value_after_dec == 0) { 4387#line 92 4388 ldv_mutex = 2; 4389#line 94 4390 return (1); 4391 } else { 4392 4393 } 4394#line 98 4395 return (0); 4396} 4397} 4398#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4399void mutex_lock(struct mutex *lock ) 4400{ 4401 4402 { 4403#line 108 4404 if (ldv_mutex == 1) { 4405 4406 } else { 4407 { 4408#line 108 4409 ldv_blast_assert(); 4410 } 4411 } 4412#line 110 4413 ldv_mutex = 2; 4414#line 111 4415 return; 4416} 4417} 4418#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4419int mutex_trylock(struct mutex *lock ) 4420{ int nondetermined ; 4421 4422 { 4423#line 121 4424 if (ldv_mutex == 1) { 4425 4426 } else { 4427 { 4428#line 121 4429 ldv_blast_assert(); 4430 } 4431 } 4432 { 4433#line 124 4434 nondetermined = __VERIFIER_nondet_int(); 4435 } 4436#line 127 4437 if (nondetermined) { 4438#line 130 4439 ldv_mutex = 2; 4440#line 132 4441 return (1); 4442 } else { 4443#line 137 4444 return (0); 4445 } 4446} 4447} 4448#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4449void mutex_unlock(struct mutex *lock ) 4450{ 4451 4452 { 4453#line 147 4454 if (ldv_mutex == 2) { 4455 4456 } else { 4457 { 4458#line 147 4459 ldv_blast_assert(); 4460 } 4461 } 4462#line 149 4463 ldv_mutex = 1; 4464#line 150 4465 return; 4466} 4467} 4468#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4469void ldv_check_final_state(void) 4470{ 4471 4472 { 4473#line 156 4474 if (ldv_mutex == 1) { 4475 4476 } else { 4477 { 4478#line 156 4479 ldv_blast_assert(); 4480 } 4481 } 4482#line 157 4483 return; 4484} 4485} 4486#line 474 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16796/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/aten.c.common.c" 4487long s__builtin_expect(long val , long res ) 4488{ 4489 4490 { 4491#line 475 4492 return (val); 4493} 4494}

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

ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 176

Source: