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 31 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 545static int cont_map[2] = { 16, 8}; 546#line 33 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 547static void ktti_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 unsigned char __cil_tmp9 ; 553 unsigned long __cil_tmp10 ; 554 unsigned long __cil_tmp11 ; 555 int __cil_tmp12 ; 556 unsigned long __cil_tmp13 ; 557 unsigned long __cil_tmp14 ; 558 unsigned long __cil_tmp15 ; 559 unsigned long __cil_tmp16 ; 560 int __cil_tmp17 ; 561 unsigned long __cil_tmp18 ; 562 unsigned long __cil_tmp19 ; 563 unsigned long __cil_tmp20 ; 564 int __cil_tmp21 ; 565 int __cil_tmp22 ; 566 unsigned long __cil_tmp23 ; 567 unsigned long __cil_tmp24 ; 568 unsigned long __cil_tmp25 ; 569 unsigned long __cil_tmp26 ; 570 int __cil_tmp27 ; 571 unsigned long __cil_tmp28 ; 572 unsigned long __cil_tmp29 ; 573 unsigned long __cil_tmp30 ; 574 int __cil_tmp31 ; 575 int __cil_tmp32 ; 576 unsigned long __cil_tmp33 ; 577 unsigned long __cil_tmp34 ; 578 unsigned long __cil_tmp35 ; 579 unsigned long __cil_tmp36 ; 580 int __cil_tmp37 ; 581 unsigned long __cil_tmp38 ; 582 unsigned long __cil_tmp39 ; 583 unsigned long __cil_tmp40 ; 584 int __cil_tmp41 ; 585 int __cil_tmp42 ; 586 unsigned long __cil_tmp43 ; 587 unsigned long __cil_tmp44 ; 588 unsigned long __cil_tmp45 ; 589 unsigned long __cil_tmp46 ; 590 int __cil_tmp47 ; 591 unsigned long __cil_tmp48 ; 592 unsigned long __cil_tmp49 ; 593 unsigned long __cil_tmp50 ; 594 int __cil_tmp51 ; 595 int __cil_tmp52 ; 596 unsigned long __cil_tmp53 ; 597 unsigned long __cil_tmp54 ; 598 unsigned long __cil_tmp55 ; 599 unsigned long __cil_tmp56 ; 600 int __cil_tmp57 ; 601 unsigned long __cil_tmp58 ; 602 unsigned char __cil_tmp59 ; 603 unsigned long __cil_tmp60 ; 604 unsigned long __cil_tmp61 ; 605 int __cil_tmp62 ; 606 unsigned long __cil_tmp63 ; 607 unsigned long __cil_tmp64 ; 608 unsigned long __cil_tmp65 ; 609 unsigned long __cil_tmp66 ; 610 int __cil_tmp67 ; 611 unsigned long __cil_tmp68 ; 612 unsigned long __cil_tmp69 ; 613 unsigned long __cil_tmp70 ; 614 int __cil_tmp71 ; 615 int __cil_tmp72 ; 616 unsigned long __cil_tmp73 ; 617 unsigned long __cil_tmp74 ; 618 unsigned long __cil_tmp75 ; 619 unsigned long __cil_tmp76 ; 620 int __cil_tmp77 ; 621 unsigned long __cil_tmp78 ; 622 unsigned long __cil_tmp79 ; 623 unsigned long __cil_tmp80 ; 624 int __cil_tmp81 ; 625 unsigned long __cil_tmp82 ; 626 unsigned long __cil_tmp83 ; 627 unsigned long __cil_tmp84 ; 628 unsigned long __cil_tmp85 ; 629 int __cil_tmp86 ; 630 unsigned long __cil_tmp87 ; 631 unsigned long __cil_tmp88 ; 632 unsigned long __cil_tmp89 ; 633 int __cil_tmp90 ; 634 int __cil_tmp91 ; 635 unsigned long __cil_tmp92 ; 636 unsigned long __cil_tmp93 ; 637 unsigned long __cil_tmp94 ; 638 unsigned long __cil_tmp95 ; 639 int __cil_tmp96 ; 640 unsigned long __cil_tmp97 ; 641 unsigned long __cil_tmp98 ; 642 unsigned long __cil_tmp99 ; 643 int __cil_tmp100 ; 644 int __cil_tmp101 ; 645 unsigned long __cil_tmp102 ; 646 unsigned long __cil_tmp103 ; 647 unsigned long __cil_tmp104 ; 648 unsigned long __cil_tmp105 ; 649 int __cil_tmp106 ; 650 unsigned long __cil_tmp107 ; 651 652 { 653 { 654#line 37 655 __cil_tmp6 = cont * 4UL; 656#line 37 657 __cil_tmp7 = (unsigned long )(cont_map) + __cil_tmp6; 658#line 37 659 __cil_tmp8 = *((int *)__cil_tmp7); 660#line 37 661 r = regr + __cil_tmp8; 662#line 39 663 __cil_tmp9 = (unsigned char )r; 664#line 39 665 __cil_tmp10 = (unsigned long )pi; 666#line 39 667 __cil_tmp11 = __cil_tmp10 + 8; 668#line 39 669 __cil_tmp12 = *((int *)__cil_tmp11); 670#line 39 671 outb(__cil_tmp9, __cil_tmp12); 672 } 673 { 674#line 39 675 __cil_tmp13 = (unsigned long )pi; 676#line 39 677 __cil_tmp14 = __cil_tmp13 + 16; 678#line 39 679 if (*((int *)__cil_tmp14)) { 680 { 681#line 39 682 __cil_tmp15 = (unsigned long )pi; 683#line 39 684 __cil_tmp16 = __cil_tmp15 + 16; 685#line 39 686 __cil_tmp17 = *((int *)__cil_tmp16); 687#line 39 688 __cil_tmp18 = (unsigned long )__cil_tmp17; 689#line 39 690 __udelay(__cil_tmp18); 691 } 692 } else { 693 694 } 695 } 696 { 697#line 39 698 __cil_tmp19 = (unsigned long )pi; 699#line 39 700 __cil_tmp20 = __cil_tmp19 + 8; 701#line 39 702 __cil_tmp21 = *((int *)__cil_tmp20); 703#line 39 704 __cil_tmp22 = __cil_tmp21 + 2; 705#line 39 706 outb((unsigned char)11, __cil_tmp22); 707 } 708 { 709#line 39 710 __cil_tmp23 = (unsigned long )pi; 711#line 39 712 __cil_tmp24 = __cil_tmp23 + 16; 713#line 39 714 if (*((int *)__cil_tmp24)) { 715 { 716#line 39 717 __cil_tmp25 = (unsigned long )pi; 718#line 39 719 __cil_tmp26 = __cil_tmp25 + 16; 720#line 39 721 __cil_tmp27 = *((int *)__cil_tmp26); 722#line 39 723 __cil_tmp28 = (unsigned long )__cil_tmp27; 724#line 39 725 __udelay(__cil_tmp28); 726 } 727 } else { 728 729 } 730 } 731 { 732#line 39 733 __cil_tmp29 = (unsigned long )pi; 734#line 39 735 __cil_tmp30 = __cil_tmp29 + 8; 736#line 39 737 __cil_tmp31 = *((int *)__cil_tmp30); 738#line 39 739 __cil_tmp32 = __cil_tmp31 + 2; 740#line 39 741 outb((unsigned char)10, __cil_tmp32); 742 } 743 { 744#line 39 745 __cil_tmp33 = (unsigned long )pi; 746#line 39 747 __cil_tmp34 = __cil_tmp33 + 16; 748#line 39 749 if (*((int *)__cil_tmp34)) { 750 { 751#line 39 752 __cil_tmp35 = (unsigned long )pi; 753#line 39 754 __cil_tmp36 = __cil_tmp35 + 16; 755#line 39 756 __cil_tmp37 = *((int *)__cil_tmp36); 757#line 39 758 __cil_tmp38 = (unsigned long )__cil_tmp37; 759#line 39 760 __udelay(__cil_tmp38); 761 } 762 } else { 763 764 } 765 } 766 { 767#line 39 768 __cil_tmp39 = (unsigned long )pi; 769#line 39 770 __cil_tmp40 = __cil_tmp39 + 8; 771#line 39 772 __cil_tmp41 = *((int *)__cil_tmp40); 773#line 39 774 __cil_tmp42 = __cil_tmp41 + 2; 775#line 39 776 outb((unsigned char)3, __cil_tmp42); 777 } 778 { 779#line 39 780 __cil_tmp43 = (unsigned long )pi; 781#line 39 782 __cil_tmp44 = __cil_tmp43 + 16; 783#line 39 784 if (*((int *)__cil_tmp44)) { 785 { 786#line 39 787 __cil_tmp45 = (unsigned long )pi; 788#line 39 789 __cil_tmp46 = __cil_tmp45 + 16; 790#line 39 791 __cil_tmp47 = *((int *)__cil_tmp46); 792#line 39 793 __cil_tmp48 = (unsigned long )__cil_tmp47; 794#line 39 795 __udelay(__cil_tmp48); 796 } 797 } else { 798 799 } 800 } 801 { 802#line 39 803 __cil_tmp49 = (unsigned long )pi; 804#line 39 805 __cil_tmp50 = __cil_tmp49 + 8; 806#line 39 807 __cil_tmp51 = *((int *)__cil_tmp50); 808#line 39 809 __cil_tmp52 = __cil_tmp51 + 2; 810#line 39 811 outb((unsigned char)6, __cil_tmp52); 812 } 813 { 814#line 39 815 __cil_tmp53 = (unsigned long )pi; 816#line 39 817 __cil_tmp54 = __cil_tmp53 + 16; 818#line 39 819 if (*((int *)__cil_tmp54)) { 820 { 821#line 39 822 __cil_tmp55 = (unsigned long )pi; 823#line 39 824 __cil_tmp56 = __cil_tmp55 + 16; 825#line 39 826 __cil_tmp57 = *((int *)__cil_tmp56); 827#line 39 828 __cil_tmp58 = (unsigned long )__cil_tmp57; 829#line 39 830 __udelay(__cil_tmp58); 831 } 832 } else { 833 834 } 835 } 836 { 837#line 40 838 __cil_tmp59 = (unsigned char )val; 839#line 40 840 __cil_tmp60 = (unsigned long )pi; 841#line 40 842 __cil_tmp61 = __cil_tmp60 + 8; 843#line 40 844 __cil_tmp62 = *((int *)__cil_tmp61); 845#line 40 846 outb(__cil_tmp59, __cil_tmp62); 847 } 848 { 849#line 40 850 __cil_tmp63 = (unsigned long )pi; 851#line 40 852 __cil_tmp64 = __cil_tmp63 + 16; 853#line 40 854 if (*((int *)__cil_tmp64)) { 855 { 856#line 40 857 __cil_tmp65 = (unsigned long )pi; 858#line 40 859 __cil_tmp66 = __cil_tmp65 + 16; 860#line 40 861 __cil_tmp67 = *((int *)__cil_tmp66); 862#line 40 863 __cil_tmp68 = (unsigned long )__cil_tmp67; 864#line 40 865 __udelay(__cil_tmp68); 866 } 867 } else { 868 869 } 870 } 871 { 872#line 40 873 __cil_tmp69 = (unsigned long )pi; 874#line 40 875 __cil_tmp70 = __cil_tmp69 + 8; 876#line 40 877 __cil_tmp71 = *((int *)__cil_tmp70); 878#line 40 879 __cil_tmp72 = __cil_tmp71 + 2; 880#line 40 881 outb((unsigned char)3, __cil_tmp72); 882 } 883 { 884#line 40 885 __cil_tmp73 = (unsigned long )pi; 886#line 40 887 __cil_tmp74 = __cil_tmp73 + 16; 888#line 40 889 if (*((int *)__cil_tmp74)) { 890 { 891#line 40 892 __cil_tmp75 = (unsigned long )pi; 893#line 40 894 __cil_tmp76 = __cil_tmp75 + 16; 895#line 40 896 __cil_tmp77 = *((int *)__cil_tmp76); 897#line 40 898 __cil_tmp78 = (unsigned long )__cil_tmp77; 899#line 40 900 __udelay(__cil_tmp78); 901 } 902 } else { 903 904 } 905 } 906 { 907#line 40 908 __cil_tmp79 = (unsigned long )pi; 909#line 40 910 __cil_tmp80 = __cil_tmp79 + 8; 911#line 40 912 __cil_tmp81 = *((int *)__cil_tmp80); 913#line 40 914 outb((unsigned char)0, __cil_tmp81); 915 } 916 { 917#line 40 918 __cil_tmp82 = (unsigned long )pi; 919#line 40 920 __cil_tmp83 = __cil_tmp82 + 16; 921#line 40 922 if (*((int *)__cil_tmp83)) { 923 { 924#line 40 925 __cil_tmp84 = (unsigned long )pi; 926#line 40 927 __cil_tmp85 = __cil_tmp84 + 16; 928#line 40 929 __cil_tmp86 = *((int *)__cil_tmp85); 930#line 40 931 __cil_tmp87 = (unsigned long )__cil_tmp86; 932#line 40 933 __udelay(__cil_tmp87); 934 } 935 } else { 936 937 } 938 } 939 { 940#line 40 941 __cil_tmp88 = (unsigned long )pi; 942#line 40 943 __cil_tmp89 = __cil_tmp88 + 8; 944#line 40 945 __cil_tmp90 = *((int *)__cil_tmp89); 946#line 40 947 __cil_tmp91 = __cil_tmp90 + 2; 948#line 40 949 outb((unsigned char)6, __cil_tmp91); 950 } 951 { 952#line 40 953 __cil_tmp92 = (unsigned long )pi; 954#line 40 955 __cil_tmp93 = __cil_tmp92 + 16; 956#line 40 957 if (*((int *)__cil_tmp93)) { 958 { 959#line 40 960 __cil_tmp94 = (unsigned long )pi; 961#line 40 962 __cil_tmp95 = __cil_tmp94 + 16; 963#line 40 964 __cil_tmp96 = *((int *)__cil_tmp95); 965#line 40 966 __cil_tmp97 = (unsigned long )__cil_tmp96; 967#line 40 968 __udelay(__cil_tmp97); 969 } 970 } else { 971 972 } 973 } 974 { 975#line 40 976 __cil_tmp98 = (unsigned long )pi; 977#line 40 978 __cil_tmp99 = __cil_tmp98 + 8; 979#line 40 980 __cil_tmp100 = *((int *)__cil_tmp99); 981#line 40 982 __cil_tmp101 = __cil_tmp100 + 2; 983#line 40 984 outb((unsigned char)11, __cil_tmp101); 985 } 986 { 987#line 40 988 __cil_tmp102 = (unsigned long )pi; 989#line 40 990 __cil_tmp103 = __cil_tmp102 + 16; 991#line 40 992 if (*((int *)__cil_tmp103)) { 993 { 994#line 40 995 __cil_tmp104 = (unsigned long )pi; 996#line 40 997 __cil_tmp105 = __cil_tmp104 + 16; 998#line 40 999 __cil_tmp106 = *((int *)__cil_tmp105); 1000#line 40 1001 __cil_tmp107 = (unsigned long )__cil_tmp106; 1002#line 40 1003 __udelay(__cil_tmp107); 1004 } 1005 } else { 1006 1007 } 1008 } 1009#line 41 1010 return; 1011} 1012} 1013#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 1014static int ktti_read_regr(PIA *pi , int cont , int regr ) 1015{ int a ; 1016 int b ; 1017 int r ; 1018 unsigned char tmp ; 1019 unsigned char tmp___0 ; 1020 unsigned long __cil_tmp9 ; 1021 unsigned long __cil_tmp10 ; 1022 int __cil_tmp11 ; 1023 unsigned char __cil_tmp12 ; 1024 unsigned long __cil_tmp13 ; 1025 unsigned long __cil_tmp14 ; 1026 int __cil_tmp15 ; 1027 unsigned long __cil_tmp16 ; 1028 unsigned long __cil_tmp17 ; 1029 unsigned long __cil_tmp18 ; 1030 unsigned long __cil_tmp19 ; 1031 int __cil_tmp20 ; 1032 unsigned long __cil_tmp21 ; 1033 unsigned long __cil_tmp22 ; 1034 unsigned long __cil_tmp23 ; 1035 int __cil_tmp24 ; 1036 int __cil_tmp25 ; 1037 unsigned long __cil_tmp26 ; 1038 unsigned long __cil_tmp27 ; 1039 unsigned long __cil_tmp28 ; 1040 unsigned long __cil_tmp29 ; 1041 int __cil_tmp30 ; 1042 unsigned long __cil_tmp31 ; 1043 unsigned long __cil_tmp32 ; 1044 unsigned long __cil_tmp33 ; 1045 int __cil_tmp34 ; 1046 int __cil_tmp35 ; 1047 unsigned long __cil_tmp36 ; 1048 unsigned long __cil_tmp37 ; 1049 unsigned long __cil_tmp38 ; 1050 unsigned long __cil_tmp39 ; 1051 int __cil_tmp40 ; 1052 unsigned long __cil_tmp41 ; 1053 unsigned long __cil_tmp42 ; 1054 unsigned long __cil_tmp43 ; 1055 int __cil_tmp44 ; 1056 int __cil_tmp45 ; 1057 unsigned long __cil_tmp46 ; 1058 unsigned long __cil_tmp47 ; 1059 unsigned long __cil_tmp48 ; 1060 unsigned long __cil_tmp49 ; 1061 int __cil_tmp50 ; 1062 unsigned long __cil_tmp51 ; 1063 unsigned long __cil_tmp52 ; 1064 unsigned long __cil_tmp53 ; 1065 int __cil_tmp54 ; 1066 int __cil_tmp55 ; 1067 unsigned long __cil_tmp56 ; 1068 unsigned long __cil_tmp57 ; 1069 unsigned long __cil_tmp58 ; 1070 unsigned long __cil_tmp59 ; 1071 int __cil_tmp60 ; 1072 unsigned long __cil_tmp61 ; 1073 unsigned long __cil_tmp62 ; 1074 unsigned long __cil_tmp63 ; 1075 int __cil_tmp64 ; 1076 int __cil_tmp65 ; 1077 unsigned long __cil_tmp66 ; 1078 unsigned long __cil_tmp67 ; 1079 unsigned long __cil_tmp68 ; 1080 unsigned long __cil_tmp69 ; 1081 int __cil_tmp70 ; 1082 unsigned long __cil_tmp71 ; 1083 unsigned long __cil_tmp72 ; 1084 unsigned long __cil_tmp73 ; 1085 unsigned long __cil_tmp74 ; 1086 unsigned long __cil_tmp75 ; 1087 int __cil_tmp76 ; 1088 unsigned long __cil_tmp77 ; 1089 unsigned long __cil_tmp78 ; 1090 unsigned long __cil_tmp79 ; 1091 int __cil_tmp80 ; 1092 int __cil_tmp81 ; 1093 int __cil_tmp82 ; 1094 unsigned long __cil_tmp83 ; 1095 unsigned long __cil_tmp84 ; 1096 int __cil_tmp85 ; 1097 int __cil_tmp86 ; 1098 unsigned long __cil_tmp87 ; 1099 unsigned long __cil_tmp88 ; 1100 unsigned long __cil_tmp89 ; 1101 unsigned long __cil_tmp90 ; 1102 int __cil_tmp91 ; 1103 unsigned long __cil_tmp92 ; 1104 unsigned long __cil_tmp93 ; 1105 unsigned long __cil_tmp94 ; 1106 unsigned long __cil_tmp95 ; 1107 unsigned long __cil_tmp96 ; 1108 int __cil_tmp97 ; 1109 unsigned long __cil_tmp98 ; 1110 unsigned long __cil_tmp99 ; 1111 unsigned long __cil_tmp100 ; 1112 int __cil_tmp101 ; 1113 int __cil_tmp102 ; 1114 int __cil_tmp103 ; 1115 unsigned long __cil_tmp104 ; 1116 unsigned long __cil_tmp105 ; 1117 int __cil_tmp106 ; 1118 int __cil_tmp107 ; 1119 unsigned long __cil_tmp108 ; 1120 unsigned long __cil_tmp109 ; 1121 unsigned long __cil_tmp110 ; 1122 unsigned long __cil_tmp111 ; 1123 int __cil_tmp112 ; 1124 unsigned long __cil_tmp113 ; 1125 unsigned long __cil_tmp114 ; 1126 unsigned long __cil_tmp115 ; 1127 int __cil_tmp116 ; 1128 int __cil_tmp117 ; 1129 unsigned long __cil_tmp118 ; 1130 unsigned long __cil_tmp119 ; 1131 unsigned long __cil_tmp120 ; 1132 unsigned long __cil_tmp121 ; 1133 int __cil_tmp122 ; 1134 unsigned long __cil_tmp123 ; 1135 unsigned long __cil_tmp124 ; 1136 unsigned long __cil_tmp125 ; 1137 int __cil_tmp126 ; 1138 int __cil_tmp127 ; 1139 unsigned long __cil_tmp128 ; 1140 unsigned long __cil_tmp129 ; 1141 unsigned long __cil_tmp130 ; 1142 unsigned long __cil_tmp131 ; 1143 int __cil_tmp132 ; 1144 unsigned long __cil_tmp133 ; 1145 int __cil_tmp134 ; 1146 int __cil_tmp135 ; 1147 int __cil_tmp136 ; 1148 1149 { 1150 { 1151#line 47 1152 __cil_tmp9 = cont * 4UL; 1153#line 47 1154 __cil_tmp10 = (unsigned long )(cont_map) + __cil_tmp9; 1155#line 47 1156 __cil_tmp11 = *((int *)__cil_tmp10); 1157#line 47 1158 r = regr + __cil_tmp11; 1159#line 49 1160 __cil_tmp12 = (unsigned char )r; 1161#line 49 1162 __cil_tmp13 = (unsigned long )pi; 1163#line 49 1164 __cil_tmp14 = __cil_tmp13 + 8; 1165#line 49 1166 __cil_tmp15 = *((int *)__cil_tmp14); 1167#line 49 1168 outb(__cil_tmp12, __cil_tmp15); 1169 } 1170 { 1171#line 49 1172 __cil_tmp16 = (unsigned long )pi; 1173#line 49 1174 __cil_tmp17 = __cil_tmp16 + 16; 1175#line 49 1176 if (*((int *)__cil_tmp17)) { 1177 { 1178#line 49 1179 __cil_tmp18 = (unsigned long )pi; 1180#line 49 1181 __cil_tmp19 = __cil_tmp18 + 16; 1182#line 49 1183 __cil_tmp20 = *((int *)__cil_tmp19); 1184#line 49 1185 __cil_tmp21 = (unsigned long )__cil_tmp20; 1186#line 49 1187 __udelay(__cil_tmp21); 1188 } 1189 } else { 1190 1191 } 1192 } 1193 { 1194#line 49 1195 __cil_tmp22 = (unsigned long )pi; 1196#line 49 1197 __cil_tmp23 = __cil_tmp22 + 8; 1198#line 49 1199 __cil_tmp24 = *((int *)__cil_tmp23); 1200#line 49 1201 __cil_tmp25 = __cil_tmp24 + 2; 1202#line 49 1203 outb((unsigned char)11, __cil_tmp25); 1204 } 1205 { 1206#line 49 1207 __cil_tmp26 = (unsigned long )pi; 1208#line 49 1209 __cil_tmp27 = __cil_tmp26 + 16; 1210#line 49 1211 if (*((int *)__cil_tmp27)) { 1212 { 1213#line 49 1214 __cil_tmp28 = (unsigned long )pi; 1215#line 49 1216 __cil_tmp29 = __cil_tmp28 + 16; 1217#line 49 1218 __cil_tmp30 = *((int *)__cil_tmp29); 1219#line 49 1220 __cil_tmp31 = (unsigned long )__cil_tmp30; 1221#line 49 1222 __udelay(__cil_tmp31); 1223 } 1224 } else { 1225 1226 } 1227 } 1228 { 1229#line 49 1230 __cil_tmp32 = (unsigned long )pi; 1231#line 49 1232 __cil_tmp33 = __cil_tmp32 + 8; 1233#line 49 1234 __cil_tmp34 = *((int *)__cil_tmp33); 1235#line 49 1236 __cil_tmp35 = __cil_tmp34 + 2; 1237#line 49 1238 outb((unsigned char)10, __cil_tmp35); 1239 } 1240 { 1241#line 49 1242 __cil_tmp36 = (unsigned long )pi; 1243#line 49 1244 __cil_tmp37 = __cil_tmp36 + 16; 1245#line 49 1246 if (*((int *)__cil_tmp37)) { 1247 { 1248#line 49 1249 __cil_tmp38 = (unsigned long )pi; 1250#line 49 1251 __cil_tmp39 = __cil_tmp38 + 16; 1252#line 49 1253 __cil_tmp40 = *((int *)__cil_tmp39); 1254#line 49 1255 __cil_tmp41 = (unsigned long )__cil_tmp40; 1256#line 49 1257 __udelay(__cil_tmp41); 1258 } 1259 } else { 1260 1261 } 1262 } 1263 { 1264#line 49 1265 __cil_tmp42 = (unsigned long )pi; 1266#line 49 1267 __cil_tmp43 = __cil_tmp42 + 8; 1268#line 49 1269 __cil_tmp44 = *((int *)__cil_tmp43); 1270#line 49 1271 __cil_tmp45 = __cil_tmp44 + 2; 1272#line 49 1273 outb((unsigned char)9, __cil_tmp45); 1274 } 1275 { 1276#line 49 1277 __cil_tmp46 = (unsigned long )pi; 1278#line 49 1279 __cil_tmp47 = __cil_tmp46 + 16; 1280#line 49 1281 if (*((int *)__cil_tmp47)) { 1282 { 1283#line 49 1284 __cil_tmp48 = (unsigned long )pi; 1285#line 49 1286 __cil_tmp49 = __cil_tmp48 + 16; 1287#line 49 1288 __cil_tmp50 = *((int *)__cil_tmp49); 1289#line 49 1290 __cil_tmp51 = (unsigned long )__cil_tmp50; 1291#line 49 1292 __udelay(__cil_tmp51); 1293 } 1294 } else { 1295 1296 } 1297 } 1298 { 1299#line 49 1300 __cil_tmp52 = (unsigned long )pi; 1301#line 49 1302 __cil_tmp53 = __cil_tmp52 + 8; 1303#line 49 1304 __cil_tmp54 = *((int *)__cil_tmp53); 1305#line 49 1306 __cil_tmp55 = __cil_tmp54 + 2; 1307#line 49 1308 outb((unsigned char)12, __cil_tmp55); 1309 } 1310 { 1311#line 49 1312 __cil_tmp56 = (unsigned long )pi; 1313#line 49 1314 __cil_tmp57 = __cil_tmp56 + 16; 1315#line 49 1316 if (*((int *)__cil_tmp57)) { 1317 { 1318#line 49 1319 __cil_tmp58 = (unsigned long )pi; 1320#line 49 1321 __cil_tmp59 = __cil_tmp58 + 16; 1322#line 49 1323 __cil_tmp60 = *((int *)__cil_tmp59); 1324#line 49 1325 __cil_tmp61 = (unsigned long )__cil_tmp60; 1326#line 49 1327 __udelay(__cil_tmp61); 1328 } 1329 } else { 1330 1331 } 1332 } 1333 { 1334#line 49 1335 __cil_tmp62 = (unsigned long )pi; 1336#line 49 1337 __cil_tmp63 = __cil_tmp62 + 8; 1338#line 49 1339 __cil_tmp64 = *((int *)__cil_tmp63); 1340#line 49 1341 __cil_tmp65 = __cil_tmp64 + 2; 1342#line 49 1343 outb((unsigned char)9, __cil_tmp65); 1344 } 1345 { 1346#line 49 1347 __cil_tmp66 = (unsigned long )pi; 1348#line 49 1349 __cil_tmp67 = __cil_tmp66 + 16; 1350#line 49 1351 if (*((int *)__cil_tmp67)) { 1352 { 1353#line 49 1354 __cil_tmp68 = (unsigned long )pi; 1355#line 49 1356 __cil_tmp69 = __cil_tmp68 + 16; 1357#line 49 1358 __cil_tmp70 = *((int *)__cil_tmp69); 1359#line 49 1360 __cil_tmp71 = (unsigned long )__cil_tmp70; 1361#line 49 1362 __udelay(__cil_tmp71); 1363 } 1364 } else { 1365 1366 } 1367 } 1368 { 1369#line 50 1370 __cil_tmp72 = (unsigned long )pi; 1371#line 50 1372 __cil_tmp73 = __cil_tmp72 + 16; 1373#line 50 1374 if (*((int *)__cil_tmp73)) { 1375 { 1376#line 50 1377 __cil_tmp74 = (unsigned long )pi; 1378#line 50 1379 __cil_tmp75 = __cil_tmp74 + 16; 1380#line 50 1381 __cil_tmp76 = *((int *)__cil_tmp75); 1382#line 50 1383 __cil_tmp77 = (unsigned long )__cil_tmp76; 1384#line 50 1385 __udelay(__cil_tmp77); 1386 } 1387 } else { 1388 1389 } 1390 } 1391 { 1392#line 50 1393 __cil_tmp78 = (unsigned long )pi; 1394#line 50 1395 __cil_tmp79 = __cil_tmp78 + 8; 1396#line 50 1397 __cil_tmp80 = *((int *)__cil_tmp79); 1398#line 50 1399 __cil_tmp81 = __cil_tmp80 + 1; 1400#line 50 1401 tmp = inb(__cil_tmp81); 1402#line 50 1403 __cil_tmp82 = (int )tmp; 1404#line 50 1405 a = __cil_tmp82 & 255; 1406#line 50 1407 __cil_tmp83 = (unsigned long )pi; 1408#line 50 1409 __cil_tmp84 = __cil_tmp83 + 8; 1410#line 50 1411 __cil_tmp85 = *((int *)__cil_tmp84); 1412#line 50 1413 __cil_tmp86 = __cil_tmp85 + 2; 1414#line 50 1415 outb((unsigned char)12, __cil_tmp86); 1416 } 1417 { 1418#line 50 1419 __cil_tmp87 = (unsigned long )pi; 1420#line 50 1421 __cil_tmp88 = __cil_tmp87 + 16; 1422#line 50 1423 if (*((int *)__cil_tmp88)) { 1424 { 1425#line 50 1426 __cil_tmp89 = (unsigned long )pi; 1427#line 50 1428 __cil_tmp90 = __cil_tmp89 + 16; 1429#line 50 1430 __cil_tmp91 = *((int *)__cil_tmp90); 1431#line 50 1432 __cil_tmp92 = (unsigned long )__cil_tmp91; 1433#line 50 1434 __udelay(__cil_tmp92); 1435 } 1436 } else { 1437 1438 } 1439 } 1440 { 1441#line 50 1442 __cil_tmp93 = (unsigned long )pi; 1443#line 50 1444 __cil_tmp94 = __cil_tmp93 + 16; 1445#line 50 1446 if (*((int *)__cil_tmp94)) { 1447 { 1448#line 50 1449 __cil_tmp95 = (unsigned long )pi; 1450#line 50 1451 __cil_tmp96 = __cil_tmp95 + 16; 1452#line 50 1453 __cil_tmp97 = *((int *)__cil_tmp96); 1454#line 50 1455 __cil_tmp98 = (unsigned long )__cil_tmp97; 1456#line 50 1457 __udelay(__cil_tmp98); 1458 } 1459 } else { 1460 1461 } 1462 } 1463 { 1464#line 50 1465 __cil_tmp99 = (unsigned long )pi; 1466#line 50 1467 __cil_tmp100 = __cil_tmp99 + 8; 1468#line 50 1469 __cil_tmp101 = *((int *)__cil_tmp100); 1470#line 50 1471 __cil_tmp102 = __cil_tmp101 + 1; 1472#line 50 1473 tmp___0 = inb(__cil_tmp102); 1474#line 50 1475 __cil_tmp103 = (int )tmp___0; 1476#line 50 1477 b = __cil_tmp103 & 255; 1478#line 50 1479 __cil_tmp104 = (unsigned long )pi; 1480#line 50 1481 __cil_tmp105 = __cil_tmp104 + 8; 1482#line 50 1483 __cil_tmp106 = *((int *)__cil_tmp105); 1484#line 50 1485 __cil_tmp107 = __cil_tmp106 + 2; 1486#line 50 1487 outb((unsigned char)9, __cil_tmp107); 1488 } 1489 { 1490#line 50 1491 __cil_tmp108 = (unsigned long )pi; 1492#line 50 1493 __cil_tmp109 = __cil_tmp108 + 16; 1494#line 50 1495 if (*((int *)__cil_tmp109)) { 1496 { 1497#line 50 1498 __cil_tmp110 = (unsigned long )pi; 1499#line 50 1500 __cil_tmp111 = __cil_tmp110 + 16; 1501#line 50 1502 __cil_tmp112 = *((int *)__cil_tmp111); 1503#line 50 1504 __cil_tmp113 = (unsigned long )__cil_tmp112; 1505#line 50 1506 __udelay(__cil_tmp113); 1507 } 1508 } else { 1509 1510 } 1511 } 1512 { 1513#line 50 1514 __cil_tmp114 = (unsigned long )pi; 1515#line 50 1516 __cil_tmp115 = __cil_tmp114 + 8; 1517#line 50 1518 __cil_tmp116 = *((int *)__cil_tmp115); 1519#line 50 1520 __cil_tmp117 = __cil_tmp116 + 2; 1521#line 50 1522 outb((unsigned char)12, __cil_tmp117); 1523 } 1524 { 1525#line 50 1526 __cil_tmp118 = (unsigned long )pi; 1527#line 50 1528 __cil_tmp119 = __cil_tmp118 + 16; 1529#line 50 1530 if (*((int *)__cil_tmp119)) { 1531 { 1532#line 50 1533 __cil_tmp120 = (unsigned long )pi; 1534#line 50 1535 __cil_tmp121 = __cil_tmp120 + 16; 1536#line 50 1537 __cil_tmp122 = *((int *)__cil_tmp121); 1538#line 50 1539 __cil_tmp123 = (unsigned long )__cil_tmp122; 1540#line 50 1541 __udelay(__cil_tmp123); 1542 } 1543 } else { 1544 1545 } 1546 } 1547 { 1548#line 50 1549 __cil_tmp124 = (unsigned long )pi; 1550#line 50 1551 __cil_tmp125 = __cil_tmp124 + 8; 1552#line 50 1553 __cil_tmp126 = *((int *)__cil_tmp125); 1554#line 50 1555 __cil_tmp127 = __cil_tmp126 + 2; 1556#line 50 1557 outb((unsigned char)9, __cil_tmp127); 1558 } 1559 { 1560#line 50 1561 __cil_tmp128 = (unsigned long )pi; 1562#line 50 1563 __cil_tmp129 = __cil_tmp128 + 16; 1564#line 50 1565 if (*((int *)__cil_tmp129)) { 1566 { 1567#line 50 1568 __cil_tmp130 = (unsigned long )pi; 1569#line 50 1570 __cil_tmp131 = __cil_tmp130 + 16; 1571#line 50 1572 __cil_tmp132 = *((int *)__cil_tmp131); 1573#line 50 1574 __cil_tmp133 = (unsigned long )__cil_tmp132; 1575#line 50 1576 __udelay(__cil_tmp133); 1577 } 1578 } else { 1579 1580 } 1581 } 1582 { 1583#line 51 1584 __cil_tmp134 = b & 240; 1585#line 51 1586 __cil_tmp135 = a >> 4; 1587#line 51 1588 __cil_tmp136 = __cil_tmp135 & 15; 1589#line 51 1590 return (__cil_tmp136 | __cil_tmp134); 1591 } 1592} 1593} 1594#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 1595static void ktti_read_block(PIA *pi , char *buf , int count ) 1596{ int k ; 1597 int a ; 1598 int b ; 1599 unsigned char tmp ; 1600 unsigned char tmp___0 ; 1601 unsigned char tmp___1 ; 1602 unsigned char tmp___2 ; 1603 int __cil_tmp11 ; 1604 unsigned long __cil_tmp12 ; 1605 unsigned long __cil_tmp13 ; 1606 int __cil_tmp14 ; 1607 unsigned long __cil_tmp15 ; 1608 unsigned long __cil_tmp16 ; 1609 unsigned long __cil_tmp17 ; 1610 unsigned long __cil_tmp18 ; 1611 int __cil_tmp19 ; 1612 unsigned long __cil_tmp20 ; 1613 unsigned long __cil_tmp21 ; 1614 unsigned long __cil_tmp22 ; 1615 int __cil_tmp23 ; 1616 int __cil_tmp24 ; 1617 unsigned long __cil_tmp25 ; 1618 unsigned long __cil_tmp26 ; 1619 unsigned long __cil_tmp27 ; 1620 unsigned long __cil_tmp28 ; 1621 int __cil_tmp29 ; 1622 unsigned long __cil_tmp30 ; 1623 unsigned long __cil_tmp31 ; 1624 unsigned long __cil_tmp32 ; 1625 int __cil_tmp33 ; 1626 int __cil_tmp34 ; 1627 unsigned long __cil_tmp35 ; 1628 unsigned long __cil_tmp36 ; 1629 unsigned long __cil_tmp37 ; 1630 unsigned long __cil_tmp38 ; 1631 int __cil_tmp39 ; 1632 unsigned long __cil_tmp40 ; 1633 unsigned long __cil_tmp41 ; 1634 unsigned long __cil_tmp42 ; 1635 int __cil_tmp43 ; 1636 int __cil_tmp44 ; 1637 unsigned long __cil_tmp45 ; 1638 unsigned long __cil_tmp46 ; 1639 unsigned long __cil_tmp47 ; 1640 unsigned long __cil_tmp48 ; 1641 int __cil_tmp49 ; 1642 unsigned long __cil_tmp50 ; 1643 unsigned long __cil_tmp51 ; 1644 unsigned long __cil_tmp52 ; 1645 int __cil_tmp53 ; 1646 int __cil_tmp54 ; 1647 unsigned long __cil_tmp55 ; 1648 unsigned long __cil_tmp56 ; 1649 unsigned long __cil_tmp57 ; 1650 unsigned long __cil_tmp58 ; 1651 int __cil_tmp59 ; 1652 unsigned long __cil_tmp60 ; 1653 unsigned long __cil_tmp61 ; 1654 unsigned long __cil_tmp62 ; 1655 int __cil_tmp63 ; 1656 int __cil_tmp64 ; 1657 unsigned long __cil_tmp65 ; 1658 unsigned long __cil_tmp66 ; 1659 unsigned long __cil_tmp67 ; 1660 unsigned long __cil_tmp68 ; 1661 int __cil_tmp69 ; 1662 unsigned long __cil_tmp70 ; 1663 unsigned long __cil_tmp71 ; 1664 unsigned long __cil_tmp72 ; 1665 unsigned long __cil_tmp73 ; 1666 unsigned long __cil_tmp74 ; 1667 int __cil_tmp75 ; 1668 unsigned long __cil_tmp76 ; 1669 unsigned long __cil_tmp77 ; 1670 unsigned long __cil_tmp78 ; 1671 int __cil_tmp79 ; 1672 int __cil_tmp80 ; 1673 int __cil_tmp81 ; 1674 unsigned long __cil_tmp82 ; 1675 unsigned long __cil_tmp83 ; 1676 int __cil_tmp84 ; 1677 int __cil_tmp85 ; 1678 unsigned long __cil_tmp86 ; 1679 unsigned long __cil_tmp87 ; 1680 unsigned long __cil_tmp88 ; 1681 unsigned long __cil_tmp89 ; 1682 int __cil_tmp90 ; 1683 unsigned long __cil_tmp91 ; 1684 unsigned long __cil_tmp92 ; 1685 unsigned long __cil_tmp93 ; 1686 unsigned long __cil_tmp94 ; 1687 unsigned long __cil_tmp95 ; 1688 int __cil_tmp96 ; 1689 unsigned long __cil_tmp97 ; 1690 unsigned long __cil_tmp98 ; 1691 unsigned long __cil_tmp99 ; 1692 int __cil_tmp100 ; 1693 int __cil_tmp101 ; 1694 int __cil_tmp102 ; 1695 unsigned long __cil_tmp103 ; 1696 unsigned long __cil_tmp104 ; 1697 int __cil_tmp105 ; 1698 int __cil_tmp106 ; 1699 unsigned long __cil_tmp107 ; 1700 unsigned long __cil_tmp108 ; 1701 unsigned long __cil_tmp109 ; 1702 unsigned long __cil_tmp110 ; 1703 int __cil_tmp111 ; 1704 unsigned long __cil_tmp112 ; 1705 int __cil_tmp113 ; 1706 char *__cil_tmp114 ; 1707 int __cil_tmp115 ; 1708 int __cil_tmp116 ; 1709 int __cil_tmp117 ; 1710 int __cil_tmp118 ; 1711 unsigned long __cil_tmp119 ; 1712 unsigned long __cil_tmp120 ; 1713 unsigned long __cil_tmp121 ; 1714 unsigned long __cil_tmp122 ; 1715 int __cil_tmp123 ; 1716 unsigned long __cil_tmp124 ; 1717 unsigned long __cil_tmp125 ; 1718 unsigned long __cil_tmp126 ; 1719 int __cil_tmp127 ; 1720 int __cil_tmp128 ; 1721 int __cil_tmp129 ; 1722 unsigned long __cil_tmp130 ; 1723 unsigned long __cil_tmp131 ; 1724 int __cil_tmp132 ; 1725 int __cil_tmp133 ; 1726 unsigned long __cil_tmp134 ; 1727 unsigned long __cil_tmp135 ; 1728 unsigned long __cil_tmp136 ; 1729 unsigned long __cil_tmp137 ; 1730 int __cil_tmp138 ; 1731 unsigned long __cil_tmp139 ; 1732 unsigned long __cil_tmp140 ; 1733 unsigned long __cil_tmp141 ; 1734 unsigned long __cil_tmp142 ; 1735 unsigned long __cil_tmp143 ; 1736 int __cil_tmp144 ; 1737 unsigned long __cil_tmp145 ; 1738 unsigned long __cil_tmp146 ; 1739 unsigned long __cil_tmp147 ; 1740 int __cil_tmp148 ; 1741 int __cil_tmp149 ; 1742 int __cil_tmp150 ; 1743 unsigned long __cil_tmp151 ; 1744 unsigned long __cil_tmp152 ; 1745 int __cil_tmp153 ; 1746 int __cil_tmp154 ; 1747 unsigned long __cil_tmp155 ; 1748 unsigned long __cil_tmp156 ; 1749 unsigned long __cil_tmp157 ; 1750 unsigned long __cil_tmp158 ; 1751 int __cil_tmp159 ; 1752 unsigned long __cil_tmp160 ; 1753 int __cil_tmp161 ; 1754 int __cil_tmp162 ; 1755 char *__cil_tmp163 ; 1756 int __cil_tmp164 ; 1757 int __cil_tmp165 ; 1758 int __cil_tmp166 ; 1759 int __cil_tmp167 ; 1760 1761 { 1762#line 59 1763 k = 0; 1764 { 1765#line 59 1766 while (1) { 1767 while_continue: /* CIL Label */ ; 1768 { 1769#line 59 1770 __cil_tmp11 = count / 2; 1771#line 59 1772 if (k < __cil_tmp11) { 1773 1774 } else { 1775#line 59 1776 goto while_break; 1777 } 1778 } 1779 { 1780#line 60 1781 __cil_tmp12 = (unsigned long )pi; 1782#line 60 1783 __cil_tmp13 = __cil_tmp12 + 8; 1784#line 60 1785 __cil_tmp14 = *((int *)__cil_tmp13); 1786#line 60 1787 outb((unsigned char)16, __cil_tmp14); 1788 } 1789 { 1790#line 60 1791 __cil_tmp15 = (unsigned long )pi; 1792#line 60 1793 __cil_tmp16 = __cil_tmp15 + 16; 1794#line 60 1795 if (*((int *)__cil_tmp16)) { 1796 { 1797#line 60 1798 __cil_tmp17 = (unsigned long )pi; 1799#line 60 1800 __cil_tmp18 = __cil_tmp17 + 16; 1801#line 60 1802 __cil_tmp19 = *((int *)__cil_tmp18); 1803#line 60 1804 __cil_tmp20 = (unsigned long )__cil_tmp19; 1805#line 60 1806 __udelay(__cil_tmp20); 1807 } 1808 } else { 1809 1810 } 1811 } 1812 { 1813#line 60 1814 __cil_tmp21 = (unsigned long )pi; 1815#line 60 1816 __cil_tmp22 = __cil_tmp21 + 8; 1817#line 60 1818 __cil_tmp23 = *((int *)__cil_tmp22); 1819#line 60 1820 __cil_tmp24 = __cil_tmp23 + 2; 1821#line 60 1822 outb((unsigned char)11, __cil_tmp24); 1823 } 1824 { 1825#line 60 1826 __cil_tmp25 = (unsigned long )pi; 1827#line 60 1828 __cil_tmp26 = __cil_tmp25 + 16; 1829#line 60 1830 if (*((int *)__cil_tmp26)) { 1831 { 1832#line 60 1833 __cil_tmp27 = (unsigned long )pi; 1834#line 60 1835 __cil_tmp28 = __cil_tmp27 + 16; 1836#line 60 1837 __cil_tmp29 = *((int *)__cil_tmp28); 1838#line 60 1839 __cil_tmp30 = (unsigned long )__cil_tmp29; 1840#line 60 1841 __udelay(__cil_tmp30); 1842 } 1843 } else { 1844 1845 } 1846 } 1847 { 1848#line 60 1849 __cil_tmp31 = (unsigned long )pi; 1850#line 60 1851 __cil_tmp32 = __cil_tmp31 + 8; 1852#line 60 1853 __cil_tmp33 = *((int *)__cil_tmp32); 1854#line 60 1855 __cil_tmp34 = __cil_tmp33 + 2; 1856#line 60 1857 outb((unsigned char)10, __cil_tmp34); 1858 } 1859 { 1860#line 60 1861 __cil_tmp35 = (unsigned long )pi; 1862#line 60 1863 __cil_tmp36 = __cil_tmp35 + 16; 1864#line 60 1865 if (*((int *)__cil_tmp36)) { 1866 { 1867#line 60 1868 __cil_tmp37 = (unsigned long )pi; 1869#line 60 1870 __cil_tmp38 = __cil_tmp37 + 16; 1871#line 60 1872 __cil_tmp39 = *((int *)__cil_tmp38); 1873#line 60 1874 __cil_tmp40 = (unsigned long )__cil_tmp39; 1875#line 60 1876 __udelay(__cil_tmp40); 1877 } 1878 } else { 1879 1880 } 1881 } 1882 { 1883#line 60 1884 __cil_tmp41 = (unsigned long )pi; 1885#line 60 1886 __cil_tmp42 = __cil_tmp41 + 8; 1887#line 60 1888 __cil_tmp43 = *((int *)__cil_tmp42); 1889#line 60 1890 __cil_tmp44 = __cil_tmp43 + 2; 1891#line 60 1892 outb((unsigned char)9, __cil_tmp44); 1893 } 1894 { 1895#line 60 1896 __cil_tmp45 = (unsigned long )pi; 1897#line 60 1898 __cil_tmp46 = __cil_tmp45 + 16; 1899#line 60 1900 if (*((int *)__cil_tmp46)) { 1901 { 1902#line 60 1903 __cil_tmp47 = (unsigned long )pi; 1904#line 60 1905 __cil_tmp48 = __cil_tmp47 + 16; 1906#line 60 1907 __cil_tmp49 = *((int *)__cil_tmp48); 1908#line 60 1909 __cil_tmp50 = (unsigned long )__cil_tmp49; 1910#line 60 1911 __udelay(__cil_tmp50); 1912 } 1913 } else { 1914 1915 } 1916 } 1917 { 1918#line 60 1919 __cil_tmp51 = (unsigned long )pi; 1920#line 60 1921 __cil_tmp52 = __cil_tmp51 + 8; 1922#line 60 1923 __cil_tmp53 = *((int *)__cil_tmp52); 1924#line 60 1925 __cil_tmp54 = __cil_tmp53 + 2; 1926#line 60 1927 outb((unsigned char)12, __cil_tmp54); 1928 } 1929 { 1930#line 60 1931 __cil_tmp55 = (unsigned long )pi; 1932#line 60 1933 __cil_tmp56 = __cil_tmp55 + 16; 1934#line 60 1935 if (*((int *)__cil_tmp56)) { 1936 { 1937#line 60 1938 __cil_tmp57 = (unsigned long )pi; 1939#line 60 1940 __cil_tmp58 = __cil_tmp57 + 16; 1941#line 60 1942 __cil_tmp59 = *((int *)__cil_tmp58); 1943#line 60 1944 __cil_tmp60 = (unsigned long )__cil_tmp59; 1945#line 60 1946 __udelay(__cil_tmp60); 1947 } 1948 } else { 1949 1950 } 1951 } 1952 { 1953#line 60 1954 __cil_tmp61 = (unsigned long )pi; 1955#line 60 1956 __cil_tmp62 = __cil_tmp61 + 8; 1957#line 60 1958 __cil_tmp63 = *((int *)__cil_tmp62); 1959#line 60 1960 __cil_tmp64 = __cil_tmp63 + 2; 1961#line 60 1962 outb((unsigned char)9, __cil_tmp64); 1963 } 1964 { 1965#line 60 1966 __cil_tmp65 = (unsigned long )pi; 1967#line 60 1968 __cil_tmp66 = __cil_tmp65 + 16; 1969#line 60 1970 if (*((int *)__cil_tmp66)) { 1971 { 1972#line 60 1973 __cil_tmp67 = (unsigned long )pi; 1974#line 60 1975 __cil_tmp68 = __cil_tmp67 + 16; 1976#line 60 1977 __cil_tmp69 = *((int *)__cil_tmp68); 1978#line 60 1979 __cil_tmp70 = (unsigned long )__cil_tmp69; 1980#line 60 1981 __udelay(__cil_tmp70); 1982 } 1983 } else { 1984 1985 } 1986 } 1987 { 1988#line 61 1989 __cil_tmp71 = (unsigned long )pi; 1990#line 61 1991 __cil_tmp72 = __cil_tmp71 + 16; 1992#line 61 1993 if (*((int *)__cil_tmp72)) { 1994 { 1995#line 61 1996 __cil_tmp73 = (unsigned long )pi; 1997#line 61 1998 __cil_tmp74 = __cil_tmp73 + 16; 1999#line 61 2000 __cil_tmp75 = *((int *)__cil_tmp74); 2001#line 61 2002 __cil_tmp76 = (unsigned long )__cil_tmp75; 2003#line 61 2004 __udelay(__cil_tmp76); 2005 } 2006 } else { 2007 2008 } 2009 } 2010 { 2011#line 61 2012 __cil_tmp77 = (unsigned long )pi; 2013#line 61 2014 __cil_tmp78 = __cil_tmp77 + 8; 2015#line 61 2016 __cil_tmp79 = *((int *)__cil_tmp78); 2017#line 61 2018 __cil_tmp80 = __cil_tmp79 + 1; 2019#line 61 2020 tmp = inb(__cil_tmp80); 2021#line 61 2022 __cil_tmp81 = (int )tmp; 2023#line 61 2024 a = __cil_tmp81 & 255; 2025#line 61 2026 __cil_tmp82 = (unsigned long )pi; 2027#line 61 2028 __cil_tmp83 = __cil_tmp82 + 8; 2029#line 61 2030 __cil_tmp84 = *((int *)__cil_tmp83); 2031#line 61 2032 __cil_tmp85 = __cil_tmp84 + 2; 2033#line 61 2034 outb((unsigned char)12, __cil_tmp85); 2035 } 2036 { 2037#line 61 2038 __cil_tmp86 = (unsigned long )pi; 2039#line 61 2040 __cil_tmp87 = __cil_tmp86 + 16; 2041#line 61 2042 if (*((int *)__cil_tmp87)) { 2043 { 2044#line 61 2045 __cil_tmp88 = (unsigned long )pi; 2046#line 61 2047 __cil_tmp89 = __cil_tmp88 + 16; 2048#line 61 2049 __cil_tmp90 = *((int *)__cil_tmp89); 2050#line 61 2051 __cil_tmp91 = (unsigned long )__cil_tmp90; 2052#line 61 2053 __udelay(__cil_tmp91); 2054 } 2055 } else { 2056 2057 } 2058 } 2059 { 2060#line 61 2061 __cil_tmp92 = (unsigned long )pi; 2062#line 61 2063 __cil_tmp93 = __cil_tmp92 + 16; 2064#line 61 2065 if (*((int *)__cil_tmp93)) { 2066 { 2067#line 61 2068 __cil_tmp94 = (unsigned long )pi; 2069#line 61 2070 __cil_tmp95 = __cil_tmp94 + 16; 2071#line 61 2072 __cil_tmp96 = *((int *)__cil_tmp95); 2073#line 61 2074 __cil_tmp97 = (unsigned long )__cil_tmp96; 2075#line 61 2076 __udelay(__cil_tmp97); 2077 } 2078 } else { 2079 2080 } 2081 } 2082 { 2083#line 61 2084 __cil_tmp98 = (unsigned long )pi; 2085#line 61 2086 __cil_tmp99 = __cil_tmp98 + 8; 2087#line 61 2088 __cil_tmp100 = *((int *)__cil_tmp99); 2089#line 61 2090 __cil_tmp101 = __cil_tmp100 + 1; 2091#line 61 2092 tmp___0 = inb(__cil_tmp101); 2093#line 61 2094 __cil_tmp102 = (int )tmp___0; 2095#line 61 2096 b = __cil_tmp102 & 255; 2097#line 61 2098 __cil_tmp103 = (unsigned long )pi; 2099#line 61 2100 __cil_tmp104 = __cil_tmp103 + 8; 2101#line 61 2102 __cil_tmp105 = *((int *)__cil_tmp104); 2103#line 61 2104 __cil_tmp106 = __cil_tmp105 + 2; 2105#line 61 2106 outb((unsigned char)9, __cil_tmp106); 2107 } 2108 { 2109#line 61 2110 __cil_tmp107 = (unsigned long )pi; 2111#line 61 2112 __cil_tmp108 = __cil_tmp107 + 16; 2113#line 61 2114 if (*((int *)__cil_tmp108)) { 2115 { 2116#line 61 2117 __cil_tmp109 = (unsigned long )pi; 2118#line 61 2119 __cil_tmp110 = __cil_tmp109 + 16; 2120#line 61 2121 __cil_tmp111 = *((int *)__cil_tmp110); 2122#line 61 2123 __cil_tmp112 = (unsigned long )__cil_tmp111; 2124#line 61 2125 __udelay(__cil_tmp112); 2126 } 2127 } else { 2128 2129 } 2130 } 2131#line 62 2132 __cil_tmp113 = 2 * k; 2133#line 62 2134 __cil_tmp114 = buf + __cil_tmp113; 2135#line 62 2136 __cil_tmp115 = b & 240; 2137#line 62 2138 __cil_tmp116 = a >> 4; 2139#line 62 2140 __cil_tmp117 = __cil_tmp116 & 15; 2141#line 62 2142 __cil_tmp118 = __cil_tmp117 | __cil_tmp115; 2143#line 62 2144 *__cil_tmp114 = (char )__cil_tmp118; 2145 { 2146#line 63 2147 __cil_tmp119 = (unsigned long )pi; 2148#line 63 2149 __cil_tmp120 = __cil_tmp119 + 16; 2150#line 63 2151 if (*((int *)__cil_tmp120)) { 2152 { 2153#line 63 2154 __cil_tmp121 = (unsigned long )pi; 2155#line 63 2156 __cil_tmp122 = __cil_tmp121 + 16; 2157#line 63 2158 __cil_tmp123 = *((int *)__cil_tmp122); 2159#line 63 2160 __cil_tmp124 = (unsigned long )__cil_tmp123; 2161#line 63 2162 __udelay(__cil_tmp124); 2163 } 2164 } else { 2165 2166 } 2167 } 2168 { 2169#line 63 2170 __cil_tmp125 = (unsigned long )pi; 2171#line 63 2172 __cil_tmp126 = __cil_tmp125 + 8; 2173#line 63 2174 __cil_tmp127 = *((int *)__cil_tmp126); 2175#line 63 2176 __cil_tmp128 = __cil_tmp127 + 1; 2177#line 63 2178 tmp___1 = inb(__cil_tmp128); 2179#line 63 2180 __cil_tmp129 = (int )tmp___1; 2181#line 63 2182 a = __cil_tmp129 & 255; 2183#line 63 2184 __cil_tmp130 = (unsigned long )pi; 2185#line 63 2186 __cil_tmp131 = __cil_tmp130 + 8; 2187#line 63 2188 __cil_tmp132 = *((int *)__cil_tmp131); 2189#line 63 2190 __cil_tmp133 = __cil_tmp132 + 2; 2191#line 63 2192 outb((unsigned char)12, __cil_tmp133); 2193 } 2194 { 2195#line 63 2196 __cil_tmp134 = (unsigned long )pi; 2197#line 63 2198 __cil_tmp135 = __cil_tmp134 + 16; 2199#line 63 2200 if (*((int *)__cil_tmp135)) { 2201 { 2202#line 63 2203 __cil_tmp136 = (unsigned long )pi; 2204#line 63 2205 __cil_tmp137 = __cil_tmp136 + 16; 2206#line 63 2207 __cil_tmp138 = *((int *)__cil_tmp137); 2208#line 63 2209 __cil_tmp139 = (unsigned long )__cil_tmp138; 2210#line 63 2211 __udelay(__cil_tmp139); 2212 } 2213 } else { 2214 2215 } 2216 } 2217 { 2218#line 63 2219 __cil_tmp140 = (unsigned long )pi; 2220#line 63 2221 __cil_tmp141 = __cil_tmp140 + 16; 2222#line 63 2223 if (*((int *)__cil_tmp141)) { 2224 { 2225#line 63 2226 __cil_tmp142 = (unsigned long )pi; 2227#line 63 2228 __cil_tmp143 = __cil_tmp142 + 16; 2229#line 63 2230 __cil_tmp144 = *((int *)__cil_tmp143); 2231#line 63 2232 __cil_tmp145 = (unsigned long )__cil_tmp144; 2233#line 63 2234 __udelay(__cil_tmp145); 2235 } 2236 } else { 2237 2238 } 2239 } 2240 { 2241#line 63 2242 __cil_tmp146 = (unsigned long )pi; 2243#line 63 2244 __cil_tmp147 = __cil_tmp146 + 8; 2245#line 63 2246 __cil_tmp148 = *((int *)__cil_tmp147); 2247#line 63 2248 __cil_tmp149 = __cil_tmp148 + 1; 2249#line 63 2250 tmp___2 = inb(__cil_tmp149); 2251#line 63 2252 __cil_tmp150 = (int )tmp___2; 2253#line 63 2254 b = __cil_tmp150 & 255; 2255#line 63 2256 __cil_tmp151 = (unsigned long )pi; 2257#line 63 2258 __cil_tmp152 = __cil_tmp151 + 8; 2259#line 63 2260 __cil_tmp153 = *((int *)__cil_tmp152); 2261#line 63 2262 __cil_tmp154 = __cil_tmp153 + 2; 2263#line 63 2264 outb((unsigned char)9, __cil_tmp154); 2265 } 2266 { 2267#line 63 2268 __cil_tmp155 = (unsigned long )pi; 2269#line 63 2270 __cil_tmp156 = __cil_tmp155 + 16; 2271#line 63 2272 if (*((int *)__cil_tmp156)) { 2273 { 2274#line 63 2275 __cil_tmp157 = (unsigned long )pi; 2276#line 63 2277 __cil_tmp158 = __cil_tmp157 + 16; 2278#line 63 2279 __cil_tmp159 = *((int *)__cil_tmp158); 2280#line 63 2281 __cil_tmp160 = (unsigned long )__cil_tmp159; 2282#line 63 2283 __udelay(__cil_tmp160); 2284 } 2285 } else { 2286 2287 } 2288 } 2289#line 64 2290 __cil_tmp161 = 2 * k; 2291#line 64 2292 __cil_tmp162 = __cil_tmp161 + 1; 2293#line 64 2294 __cil_tmp163 = buf + __cil_tmp162; 2295#line 64 2296 __cil_tmp164 = b & 240; 2297#line 64 2298 __cil_tmp165 = a >> 4; 2299#line 64 2300 __cil_tmp166 = __cil_tmp165 & 15; 2301#line 64 2302 __cil_tmp167 = __cil_tmp166 | __cil_tmp164; 2303#line 64 2304 *__cil_tmp163 = (char )__cil_tmp167; 2305#line 59 2306 k = k + 1; 2307 } 2308 while_break: /* CIL Label */ ; 2309 } 2310#line 66 2311 return; 2312} 2313} 2314#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 2315static void ktti_write_block(PIA *pi , char *buf , int count ) 2316{ int k ; 2317 int __cil_tmp5 ; 2318 unsigned long __cil_tmp6 ; 2319 unsigned long __cil_tmp7 ; 2320 int __cil_tmp8 ; 2321 unsigned long __cil_tmp9 ; 2322 unsigned long __cil_tmp10 ; 2323 unsigned long __cil_tmp11 ; 2324 unsigned long __cil_tmp12 ; 2325 int __cil_tmp13 ; 2326 unsigned long __cil_tmp14 ; 2327 unsigned long __cil_tmp15 ; 2328 unsigned long __cil_tmp16 ; 2329 int __cil_tmp17 ; 2330 int __cil_tmp18 ; 2331 unsigned long __cil_tmp19 ; 2332 unsigned long __cil_tmp20 ; 2333 unsigned long __cil_tmp21 ; 2334 unsigned long __cil_tmp22 ; 2335 int __cil_tmp23 ; 2336 unsigned long __cil_tmp24 ; 2337 unsigned long __cil_tmp25 ; 2338 unsigned long __cil_tmp26 ; 2339 int __cil_tmp27 ; 2340 int __cil_tmp28 ; 2341 unsigned long __cil_tmp29 ; 2342 unsigned long __cil_tmp30 ; 2343 unsigned long __cil_tmp31 ; 2344 unsigned long __cil_tmp32 ; 2345 int __cil_tmp33 ; 2346 unsigned long __cil_tmp34 ; 2347 unsigned long __cil_tmp35 ; 2348 unsigned long __cil_tmp36 ; 2349 int __cil_tmp37 ; 2350 int __cil_tmp38 ; 2351 unsigned long __cil_tmp39 ; 2352 unsigned long __cil_tmp40 ; 2353 unsigned long __cil_tmp41 ; 2354 unsigned long __cil_tmp42 ; 2355 int __cil_tmp43 ; 2356 unsigned long __cil_tmp44 ; 2357 unsigned long __cil_tmp45 ; 2358 unsigned long __cil_tmp46 ; 2359 int __cil_tmp47 ; 2360 int __cil_tmp48 ; 2361 unsigned long __cil_tmp49 ; 2362 unsigned long __cil_tmp50 ; 2363 unsigned long __cil_tmp51 ; 2364 unsigned long __cil_tmp52 ; 2365 int __cil_tmp53 ; 2366 unsigned long __cil_tmp54 ; 2367 int __cil_tmp55 ; 2368 char *__cil_tmp56 ; 2369 char __cil_tmp57 ; 2370 unsigned char __cil_tmp58 ; 2371 unsigned long __cil_tmp59 ; 2372 unsigned long __cil_tmp60 ; 2373 int __cil_tmp61 ; 2374 unsigned long __cil_tmp62 ; 2375 unsigned long __cil_tmp63 ; 2376 unsigned long __cil_tmp64 ; 2377 unsigned long __cil_tmp65 ; 2378 int __cil_tmp66 ; 2379 unsigned long __cil_tmp67 ; 2380 unsigned long __cil_tmp68 ; 2381 unsigned long __cil_tmp69 ; 2382 int __cil_tmp70 ; 2383 int __cil_tmp71 ; 2384 unsigned long __cil_tmp72 ; 2385 unsigned long __cil_tmp73 ; 2386 unsigned long __cil_tmp74 ; 2387 unsigned long __cil_tmp75 ; 2388 int __cil_tmp76 ; 2389 unsigned long __cil_tmp77 ; 2390 int __cil_tmp78 ; 2391 int __cil_tmp79 ; 2392 char *__cil_tmp80 ; 2393 char __cil_tmp81 ; 2394 unsigned char __cil_tmp82 ; 2395 unsigned long __cil_tmp83 ; 2396 unsigned long __cil_tmp84 ; 2397 int __cil_tmp85 ; 2398 unsigned long __cil_tmp86 ; 2399 unsigned long __cil_tmp87 ; 2400 unsigned long __cil_tmp88 ; 2401 unsigned long __cil_tmp89 ; 2402 int __cil_tmp90 ; 2403 unsigned long __cil_tmp91 ; 2404 unsigned long __cil_tmp92 ; 2405 unsigned long __cil_tmp93 ; 2406 int __cil_tmp94 ; 2407 int __cil_tmp95 ; 2408 unsigned long __cil_tmp96 ; 2409 unsigned long __cil_tmp97 ; 2410 unsigned long __cil_tmp98 ; 2411 unsigned long __cil_tmp99 ; 2412 int __cil_tmp100 ; 2413 unsigned long __cil_tmp101 ; 2414 unsigned long __cil_tmp102 ; 2415 unsigned long __cil_tmp103 ; 2416 int __cil_tmp104 ; 2417 int __cil_tmp105 ; 2418 unsigned long __cil_tmp106 ; 2419 unsigned long __cil_tmp107 ; 2420 unsigned long __cil_tmp108 ; 2421 unsigned long __cil_tmp109 ; 2422 int __cil_tmp110 ; 2423 unsigned long __cil_tmp111 ; 2424 2425 { 2426#line 72 2427 k = 0; 2428 { 2429#line 72 2430 while (1) { 2431 while_continue: /* CIL Label */ ; 2432 { 2433#line 72 2434 __cil_tmp5 = count / 2; 2435#line 72 2436 if (k < __cil_tmp5) { 2437 2438 } else { 2439#line 72 2440 goto while_break; 2441 } 2442 } 2443 { 2444#line 73 2445 __cil_tmp6 = (unsigned long )pi; 2446#line 73 2447 __cil_tmp7 = __cil_tmp6 + 8; 2448#line 73 2449 __cil_tmp8 = *((int *)__cil_tmp7); 2450#line 73 2451 outb((unsigned char)16, __cil_tmp8); 2452 } 2453 { 2454#line 73 2455 __cil_tmp9 = (unsigned long )pi; 2456#line 73 2457 __cil_tmp10 = __cil_tmp9 + 16; 2458#line 73 2459 if (*((int *)__cil_tmp10)) { 2460 { 2461#line 73 2462 __cil_tmp11 = (unsigned long )pi; 2463#line 73 2464 __cil_tmp12 = __cil_tmp11 + 16; 2465#line 73 2466 __cil_tmp13 = *((int *)__cil_tmp12); 2467#line 73 2468 __cil_tmp14 = (unsigned long )__cil_tmp13; 2469#line 73 2470 __udelay(__cil_tmp14); 2471 } 2472 } else { 2473 2474 } 2475 } 2476 { 2477#line 73 2478 __cil_tmp15 = (unsigned long )pi; 2479#line 73 2480 __cil_tmp16 = __cil_tmp15 + 8; 2481#line 73 2482 __cil_tmp17 = *((int *)__cil_tmp16); 2483#line 73 2484 __cil_tmp18 = __cil_tmp17 + 2; 2485#line 73 2486 outb((unsigned char)11, __cil_tmp18); 2487 } 2488 { 2489#line 73 2490 __cil_tmp19 = (unsigned long )pi; 2491#line 73 2492 __cil_tmp20 = __cil_tmp19 + 16; 2493#line 73 2494 if (*((int *)__cil_tmp20)) { 2495 { 2496#line 73 2497 __cil_tmp21 = (unsigned long )pi; 2498#line 73 2499 __cil_tmp22 = __cil_tmp21 + 16; 2500#line 73 2501 __cil_tmp23 = *((int *)__cil_tmp22); 2502#line 73 2503 __cil_tmp24 = (unsigned long )__cil_tmp23; 2504#line 73 2505 __udelay(__cil_tmp24); 2506 } 2507 } else { 2508 2509 } 2510 } 2511 { 2512#line 73 2513 __cil_tmp25 = (unsigned long )pi; 2514#line 73 2515 __cil_tmp26 = __cil_tmp25 + 8; 2516#line 73 2517 __cil_tmp27 = *((int *)__cil_tmp26); 2518#line 73 2519 __cil_tmp28 = __cil_tmp27 + 2; 2520#line 73 2521 outb((unsigned char)10, __cil_tmp28); 2522 } 2523 { 2524#line 73 2525 __cil_tmp29 = (unsigned long )pi; 2526#line 73 2527 __cil_tmp30 = __cil_tmp29 + 16; 2528#line 73 2529 if (*((int *)__cil_tmp30)) { 2530 { 2531#line 73 2532 __cil_tmp31 = (unsigned long )pi; 2533#line 73 2534 __cil_tmp32 = __cil_tmp31 + 16; 2535#line 73 2536 __cil_tmp33 = *((int *)__cil_tmp32); 2537#line 73 2538 __cil_tmp34 = (unsigned long )__cil_tmp33; 2539#line 73 2540 __udelay(__cil_tmp34); 2541 } 2542 } else { 2543 2544 } 2545 } 2546 { 2547#line 73 2548 __cil_tmp35 = (unsigned long )pi; 2549#line 73 2550 __cil_tmp36 = __cil_tmp35 + 8; 2551#line 73 2552 __cil_tmp37 = *((int *)__cil_tmp36); 2553#line 73 2554 __cil_tmp38 = __cil_tmp37 + 2; 2555#line 73 2556 outb((unsigned char)3, __cil_tmp38); 2557 } 2558 { 2559#line 73 2560 __cil_tmp39 = (unsigned long )pi; 2561#line 73 2562 __cil_tmp40 = __cil_tmp39 + 16; 2563#line 73 2564 if (*((int *)__cil_tmp40)) { 2565 { 2566#line 73 2567 __cil_tmp41 = (unsigned long )pi; 2568#line 73 2569 __cil_tmp42 = __cil_tmp41 + 16; 2570#line 73 2571 __cil_tmp43 = *((int *)__cil_tmp42); 2572#line 73 2573 __cil_tmp44 = (unsigned long )__cil_tmp43; 2574#line 73 2575 __udelay(__cil_tmp44); 2576 } 2577 } else { 2578 2579 } 2580 } 2581 { 2582#line 73 2583 __cil_tmp45 = (unsigned long )pi; 2584#line 73 2585 __cil_tmp46 = __cil_tmp45 + 8; 2586#line 73 2587 __cil_tmp47 = *((int *)__cil_tmp46); 2588#line 73 2589 __cil_tmp48 = __cil_tmp47 + 2; 2590#line 73 2591 outb((unsigned char)6, __cil_tmp48); 2592 } 2593 { 2594#line 73 2595 __cil_tmp49 = (unsigned long )pi; 2596#line 73 2597 __cil_tmp50 = __cil_tmp49 + 16; 2598#line 73 2599 if (*((int *)__cil_tmp50)) { 2600 { 2601#line 73 2602 __cil_tmp51 = (unsigned long )pi; 2603#line 73 2604 __cil_tmp52 = __cil_tmp51 + 16; 2605#line 73 2606 __cil_tmp53 = *((int *)__cil_tmp52); 2607#line 73 2608 __cil_tmp54 = (unsigned long )__cil_tmp53; 2609#line 73 2610 __udelay(__cil_tmp54); 2611 } 2612 } else { 2613 2614 } 2615 } 2616 { 2617#line 74 2618 __cil_tmp55 = 2 * k; 2619#line 74 2620 __cil_tmp56 = buf + __cil_tmp55; 2621#line 74 2622 __cil_tmp57 = *__cil_tmp56; 2623#line 74 2624 __cil_tmp58 = (unsigned char )__cil_tmp57; 2625#line 74 2626 __cil_tmp59 = (unsigned long )pi; 2627#line 74 2628 __cil_tmp60 = __cil_tmp59 + 8; 2629#line 74 2630 __cil_tmp61 = *((int *)__cil_tmp60); 2631#line 74 2632 outb(__cil_tmp58, __cil_tmp61); 2633 } 2634 { 2635#line 74 2636 __cil_tmp62 = (unsigned long )pi; 2637#line 74 2638 __cil_tmp63 = __cil_tmp62 + 16; 2639#line 74 2640 if (*((int *)__cil_tmp63)) { 2641 { 2642#line 74 2643 __cil_tmp64 = (unsigned long )pi; 2644#line 74 2645 __cil_tmp65 = __cil_tmp64 + 16; 2646#line 74 2647 __cil_tmp66 = *((int *)__cil_tmp65); 2648#line 74 2649 __cil_tmp67 = (unsigned long )__cil_tmp66; 2650#line 74 2651 __udelay(__cil_tmp67); 2652 } 2653 } else { 2654 2655 } 2656 } 2657 { 2658#line 74 2659 __cil_tmp68 = (unsigned long )pi; 2660#line 74 2661 __cil_tmp69 = __cil_tmp68 + 8; 2662#line 74 2663 __cil_tmp70 = *((int *)__cil_tmp69); 2664#line 74 2665 __cil_tmp71 = __cil_tmp70 + 2; 2666#line 74 2667 outb((unsigned char)3, __cil_tmp71); 2668 } 2669 { 2670#line 74 2671 __cil_tmp72 = (unsigned long )pi; 2672#line 74 2673 __cil_tmp73 = __cil_tmp72 + 16; 2674#line 74 2675 if (*((int *)__cil_tmp73)) { 2676 { 2677#line 74 2678 __cil_tmp74 = (unsigned long )pi; 2679#line 74 2680 __cil_tmp75 = __cil_tmp74 + 16; 2681#line 74 2682 __cil_tmp76 = *((int *)__cil_tmp75); 2683#line 74 2684 __cil_tmp77 = (unsigned long )__cil_tmp76; 2685#line 74 2686 __udelay(__cil_tmp77); 2687 } 2688 } else { 2689 2690 } 2691 } 2692 { 2693#line 75 2694 __cil_tmp78 = 2 * k; 2695#line 75 2696 __cil_tmp79 = __cil_tmp78 + 1; 2697#line 75 2698 __cil_tmp80 = buf + __cil_tmp79; 2699#line 75 2700 __cil_tmp81 = *__cil_tmp80; 2701#line 75 2702 __cil_tmp82 = (unsigned char )__cil_tmp81; 2703#line 75 2704 __cil_tmp83 = (unsigned long )pi; 2705#line 75 2706 __cil_tmp84 = __cil_tmp83 + 8; 2707#line 75 2708 __cil_tmp85 = *((int *)__cil_tmp84); 2709#line 75 2710 outb(__cil_tmp82, __cil_tmp85); 2711 } 2712 { 2713#line 75 2714 __cil_tmp86 = (unsigned long )pi; 2715#line 75 2716 __cil_tmp87 = __cil_tmp86 + 16; 2717#line 75 2718 if (*((int *)__cil_tmp87)) { 2719 { 2720#line 75 2721 __cil_tmp88 = (unsigned long )pi; 2722#line 75 2723 __cil_tmp89 = __cil_tmp88 + 16; 2724#line 75 2725 __cil_tmp90 = *((int *)__cil_tmp89); 2726#line 75 2727 __cil_tmp91 = (unsigned long )__cil_tmp90; 2728#line 75 2729 __udelay(__cil_tmp91); 2730 } 2731 } else { 2732 2733 } 2734 } 2735 { 2736#line 75 2737 __cil_tmp92 = (unsigned long )pi; 2738#line 75 2739 __cil_tmp93 = __cil_tmp92 + 8; 2740#line 75 2741 __cil_tmp94 = *((int *)__cil_tmp93); 2742#line 75 2743 __cil_tmp95 = __cil_tmp94 + 2; 2744#line 75 2745 outb((unsigned char)6, __cil_tmp95); 2746 } 2747 { 2748#line 75 2749 __cil_tmp96 = (unsigned long )pi; 2750#line 75 2751 __cil_tmp97 = __cil_tmp96 + 16; 2752#line 75 2753 if (*((int *)__cil_tmp97)) { 2754 { 2755#line 75 2756 __cil_tmp98 = (unsigned long )pi; 2757#line 75 2758 __cil_tmp99 = __cil_tmp98 + 16; 2759#line 75 2760 __cil_tmp100 = *((int *)__cil_tmp99); 2761#line 75 2762 __cil_tmp101 = (unsigned long )__cil_tmp100; 2763#line 75 2764 __udelay(__cil_tmp101); 2765 } 2766 } else { 2767 2768 } 2769 } 2770 { 2771#line 76 2772 __cil_tmp102 = (unsigned long )pi; 2773#line 76 2774 __cil_tmp103 = __cil_tmp102 + 8; 2775#line 76 2776 __cil_tmp104 = *((int *)__cil_tmp103); 2777#line 76 2778 __cil_tmp105 = __cil_tmp104 + 2; 2779#line 76 2780 outb((unsigned char)11, __cil_tmp105); 2781 } 2782 { 2783#line 76 2784 __cil_tmp106 = (unsigned long )pi; 2785#line 76 2786 __cil_tmp107 = __cil_tmp106 + 16; 2787#line 76 2788 if (*((int *)__cil_tmp107)) { 2789 { 2790#line 76 2791 __cil_tmp108 = (unsigned long )pi; 2792#line 76 2793 __cil_tmp109 = __cil_tmp108 + 16; 2794#line 76 2795 __cil_tmp110 = *((int *)__cil_tmp109); 2796#line 76 2797 __cil_tmp111 = (unsigned long )__cil_tmp110; 2798#line 76 2799 __udelay(__cil_tmp111); 2800 } 2801 } else { 2802 2803 } 2804 } 2805#line 72 2806 k = k + 1; 2807 } 2808 while_break: /* CIL Label */ ; 2809 } 2810#line 78 2811 return; 2812} 2813} 2814#line 80 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 2815static void ktti_connect(PIA *pi ) 2816{ unsigned char tmp ; 2817 unsigned char tmp___0 ; 2818 unsigned long __cil_tmp4 ; 2819 unsigned long __cil_tmp5 ; 2820 unsigned long __cil_tmp6 ; 2821 unsigned long __cil_tmp7 ; 2822 int __cil_tmp8 ; 2823 unsigned long __cil_tmp9 ; 2824 unsigned long __cil_tmp10 ; 2825 unsigned long __cil_tmp11 ; 2826 int __cil_tmp12 ; 2827 unsigned long __cil_tmp13 ; 2828 unsigned long __cil_tmp14 ; 2829 int __cil_tmp15 ; 2830 unsigned long __cil_tmp16 ; 2831 unsigned long __cil_tmp17 ; 2832 unsigned long __cil_tmp18 ; 2833 unsigned long __cil_tmp19 ; 2834 int __cil_tmp20 ; 2835 unsigned long __cil_tmp21 ; 2836 unsigned long __cil_tmp22 ; 2837 unsigned long __cil_tmp23 ; 2838 int __cil_tmp24 ; 2839 int __cil_tmp25 ; 2840 unsigned long __cil_tmp26 ; 2841 unsigned long __cil_tmp27 ; 2842 int __cil_tmp28 ; 2843 unsigned long __cil_tmp29 ; 2844 unsigned long __cil_tmp30 ; 2845 int __cil_tmp31 ; 2846 int __cil_tmp32 ; 2847 unsigned long __cil_tmp33 ; 2848 unsigned long __cil_tmp34 ; 2849 unsigned long __cil_tmp35 ; 2850 unsigned long __cil_tmp36 ; 2851 int __cil_tmp37 ; 2852 unsigned long __cil_tmp38 ; 2853 unsigned long __cil_tmp39 ; 2854 unsigned long __cil_tmp40 ; 2855 int __cil_tmp41 ; 2856 int __cil_tmp42 ; 2857 unsigned long __cil_tmp43 ; 2858 unsigned long __cil_tmp44 ; 2859 unsigned long __cil_tmp45 ; 2860 unsigned long __cil_tmp46 ; 2861 int __cil_tmp47 ; 2862 unsigned long __cil_tmp48 ; 2863 unsigned long __cil_tmp49 ; 2864 unsigned long __cil_tmp50 ; 2865 int __cil_tmp51 ; 2866 unsigned long __cil_tmp52 ; 2867 unsigned long __cil_tmp53 ; 2868 unsigned long __cil_tmp54 ; 2869 unsigned long __cil_tmp55 ; 2870 int __cil_tmp56 ; 2871 unsigned long __cil_tmp57 ; 2872 unsigned long __cil_tmp58 ; 2873 unsigned long __cil_tmp59 ; 2874 int __cil_tmp60 ; 2875 int __cil_tmp61 ; 2876 unsigned long __cil_tmp62 ; 2877 unsigned long __cil_tmp63 ; 2878 unsigned long __cil_tmp64 ; 2879 unsigned long __cil_tmp65 ; 2880 int __cil_tmp66 ; 2881 unsigned long __cil_tmp67 ; 2882 unsigned long __cil_tmp68 ; 2883 unsigned long __cil_tmp69 ; 2884 int __cil_tmp70 ; 2885 int __cil_tmp71 ; 2886 unsigned long __cil_tmp72 ; 2887 unsigned long __cil_tmp73 ; 2888 unsigned long __cil_tmp74 ; 2889 unsigned long __cil_tmp75 ; 2890 int __cil_tmp76 ; 2891 unsigned long __cil_tmp77 ; 2892 2893 { 2894 { 2895#line 82 2896 __cil_tmp4 = (unsigned long )pi; 2897#line 82 2898 __cil_tmp5 = __cil_tmp4 + 16; 2899#line 82 2900 if (*((int *)__cil_tmp5)) { 2901 { 2902#line 82 2903 __cil_tmp6 = (unsigned long )pi; 2904#line 82 2905 __cil_tmp7 = __cil_tmp6 + 16; 2906#line 82 2907 __cil_tmp8 = *((int *)__cil_tmp7); 2908#line 82 2909 __cil_tmp9 = (unsigned long )__cil_tmp8; 2910#line 82 2911 __udelay(__cil_tmp9); 2912 } 2913 } else { 2914 2915 } 2916 } 2917 { 2918#line 82 2919 __cil_tmp10 = (unsigned long )pi; 2920#line 82 2921 __cil_tmp11 = __cil_tmp10 + 8; 2922#line 82 2923 __cil_tmp12 = *((int *)__cil_tmp11); 2924#line 82 2925 tmp = inb(__cil_tmp12); 2926#line 82 2927 __cil_tmp13 = (unsigned long )pi; 2928#line 82 2929 __cil_tmp14 = __cil_tmp13 + 36; 2930#line 82 2931 __cil_tmp15 = (int )tmp; 2932#line 82 2933 *((int *)__cil_tmp14) = __cil_tmp15 & 255; 2934 } 2935 { 2936#line 83 2937 __cil_tmp16 = (unsigned long )pi; 2938#line 83 2939 __cil_tmp17 = __cil_tmp16 + 16; 2940#line 83 2941 if (*((int *)__cil_tmp17)) { 2942 { 2943#line 83 2944 __cil_tmp18 = (unsigned long )pi; 2945#line 83 2946 __cil_tmp19 = __cil_tmp18 + 16; 2947#line 83 2948 __cil_tmp20 = *((int *)__cil_tmp19); 2949#line 83 2950 __cil_tmp21 = (unsigned long )__cil_tmp20; 2951#line 83 2952 __udelay(__cil_tmp21); 2953 } 2954 } else { 2955 2956 } 2957 } 2958 { 2959#line 83 2960 __cil_tmp22 = (unsigned long )pi; 2961#line 83 2962 __cil_tmp23 = __cil_tmp22 + 8; 2963#line 83 2964 __cil_tmp24 = *((int *)__cil_tmp23); 2965#line 83 2966 __cil_tmp25 = __cil_tmp24 + 2; 2967#line 83 2968 tmp___0 = inb(__cil_tmp25); 2969#line 83 2970 __cil_tmp26 = (unsigned long )pi; 2971#line 83 2972 __cil_tmp27 = __cil_tmp26 + 40; 2973#line 83 2974 __cil_tmp28 = (int )tmp___0; 2975#line 83 2976 *((int *)__cil_tmp27) = __cil_tmp28 & 255; 2977#line 84 2978 __cil_tmp29 = (unsigned long )pi; 2979#line 84 2980 __cil_tmp30 = __cil_tmp29 + 8; 2981#line 84 2982 __cil_tmp31 = *((int *)__cil_tmp30); 2983#line 84 2984 __cil_tmp32 = __cil_tmp31 + 2; 2985#line 84 2986 outb((unsigned char)11, __cil_tmp32); 2987 } 2988 { 2989#line 84 2990 __cil_tmp33 = (unsigned long )pi; 2991#line 84 2992 __cil_tmp34 = __cil_tmp33 + 16; 2993#line 84 2994 if (*((int *)__cil_tmp34)) { 2995 { 2996#line 84 2997 __cil_tmp35 = (unsigned long )pi; 2998#line 84 2999 __cil_tmp36 = __cil_tmp35 + 16; 3000#line 84 3001 __cil_tmp37 = *((int *)__cil_tmp36); 3002#line 84 3003 __cil_tmp38 = (unsigned long )__cil_tmp37; 3004#line 84 3005 __udelay(__cil_tmp38); 3006 } 3007 } else { 3008 3009 } 3010 } 3011 { 3012#line 84 3013 __cil_tmp39 = (unsigned long )pi; 3014#line 84 3015 __cil_tmp40 = __cil_tmp39 + 8; 3016#line 84 3017 __cil_tmp41 = *((int *)__cil_tmp40); 3018#line 84 3019 __cil_tmp42 = __cil_tmp41 + 2; 3020#line 84 3021 outb((unsigned char)10, __cil_tmp42); 3022 } 3023 { 3024#line 84 3025 __cil_tmp43 = (unsigned long )pi; 3026#line 84 3027 __cil_tmp44 = __cil_tmp43 + 16; 3028#line 84 3029 if (*((int *)__cil_tmp44)) { 3030 { 3031#line 84 3032 __cil_tmp45 = (unsigned long )pi; 3033#line 84 3034 __cil_tmp46 = __cil_tmp45 + 16; 3035#line 84 3036 __cil_tmp47 = *((int *)__cil_tmp46); 3037#line 84 3038 __cil_tmp48 = (unsigned long )__cil_tmp47; 3039#line 84 3040 __udelay(__cil_tmp48); 3041 } 3042 } else { 3043 3044 } 3045 } 3046 { 3047#line 84 3048 __cil_tmp49 = (unsigned long )pi; 3049#line 84 3050 __cil_tmp50 = __cil_tmp49 + 8; 3051#line 84 3052 __cil_tmp51 = *((int *)__cil_tmp50); 3053#line 84 3054 outb((unsigned char)0, __cil_tmp51); 3055 } 3056 { 3057#line 84 3058 __cil_tmp52 = (unsigned long )pi; 3059#line 84 3060 __cil_tmp53 = __cil_tmp52 + 16; 3061#line 84 3062 if (*((int *)__cil_tmp53)) { 3063 { 3064#line 84 3065 __cil_tmp54 = (unsigned long )pi; 3066#line 84 3067 __cil_tmp55 = __cil_tmp54 + 16; 3068#line 84 3069 __cil_tmp56 = *((int *)__cil_tmp55); 3070#line 84 3071 __cil_tmp57 = (unsigned long )__cil_tmp56; 3072#line 84 3073 __udelay(__cil_tmp57); 3074 } 3075 } else { 3076 3077 } 3078 } 3079 { 3080#line 84 3081 __cil_tmp58 = (unsigned long )pi; 3082#line 84 3083 __cil_tmp59 = __cil_tmp58 + 8; 3084#line 84 3085 __cil_tmp60 = *((int *)__cil_tmp59); 3086#line 84 3087 __cil_tmp61 = __cil_tmp60 + 2; 3088#line 84 3089 outb((unsigned char)3, __cil_tmp61); 3090 } 3091 { 3092#line 84 3093 __cil_tmp62 = (unsigned long )pi; 3094#line 84 3095 __cil_tmp63 = __cil_tmp62 + 16; 3096#line 84 3097 if (*((int *)__cil_tmp63)) { 3098 { 3099#line 84 3100 __cil_tmp64 = (unsigned long )pi; 3101#line 84 3102 __cil_tmp65 = __cil_tmp64 + 16; 3103#line 84 3104 __cil_tmp66 = *((int *)__cil_tmp65); 3105#line 84 3106 __cil_tmp67 = (unsigned long )__cil_tmp66; 3107#line 84 3108 __udelay(__cil_tmp67); 3109 } 3110 } else { 3111 3112 } 3113 } 3114 { 3115#line 84 3116 __cil_tmp68 = (unsigned long )pi; 3117#line 84 3118 __cil_tmp69 = __cil_tmp68 + 8; 3119#line 84 3120 __cil_tmp70 = *((int *)__cil_tmp69); 3121#line 84 3122 __cil_tmp71 = __cil_tmp70 + 2; 3123#line 84 3124 outb((unsigned char)6, __cil_tmp71); 3125 } 3126 { 3127#line 84 3128 __cil_tmp72 = (unsigned long )pi; 3129#line 84 3130 __cil_tmp73 = __cil_tmp72 + 16; 3131#line 84 3132 if (*((int *)__cil_tmp73)) { 3133 { 3134#line 84 3135 __cil_tmp74 = (unsigned long )pi; 3136#line 84 3137 __cil_tmp75 = __cil_tmp74 + 16; 3138#line 84 3139 __cil_tmp76 = *((int *)__cil_tmp75); 3140#line 84 3141 __cil_tmp77 = (unsigned long )__cil_tmp76; 3142#line 84 3143 __udelay(__cil_tmp77); 3144 } 3145 } else { 3146 3147 } 3148 } 3149#line 85 3150 return; 3151} 3152} 3153#line 87 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 3154static void ktti_disconnect(PIA *pi ) 3155{ unsigned long __cil_tmp2 ; 3156 unsigned long __cil_tmp3 ; 3157 int __cil_tmp4 ; 3158 int __cil_tmp5 ; 3159 unsigned long __cil_tmp6 ; 3160 unsigned long __cil_tmp7 ; 3161 unsigned long __cil_tmp8 ; 3162 unsigned long __cil_tmp9 ; 3163 int __cil_tmp10 ; 3164 unsigned long __cil_tmp11 ; 3165 unsigned long __cil_tmp12 ; 3166 unsigned long __cil_tmp13 ; 3167 int __cil_tmp14 ; 3168 int __cil_tmp15 ; 3169 unsigned long __cil_tmp16 ; 3170 unsigned long __cil_tmp17 ; 3171 unsigned long __cil_tmp18 ; 3172 unsigned long __cil_tmp19 ; 3173 int __cil_tmp20 ; 3174 unsigned long __cil_tmp21 ; 3175 unsigned long __cil_tmp22 ; 3176 unsigned long __cil_tmp23 ; 3177 int __cil_tmp24 ; 3178 unsigned long __cil_tmp25 ; 3179 unsigned long __cil_tmp26 ; 3180 unsigned long __cil_tmp27 ; 3181 unsigned long __cil_tmp28 ; 3182 int __cil_tmp29 ; 3183 unsigned long __cil_tmp30 ; 3184 unsigned long __cil_tmp31 ; 3185 unsigned long __cil_tmp32 ; 3186 int __cil_tmp33 ; 3187 int __cil_tmp34 ; 3188 unsigned long __cil_tmp35 ; 3189 unsigned long __cil_tmp36 ; 3190 unsigned long __cil_tmp37 ; 3191 unsigned long __cil_tmp38 ; 3192 int __cil_tmp39 ; 3193 unsigned long __cil_tmp40 ; 3194 unsigned long __cil_tmp41 ; 3195 unsigned long __cil_tmp42 ; 3196 int __cil_tmp43 ; 3197 int __cil_tmp44 ; 3198 unsigned long __cil_tmp45 ; 3199 unsigned long __cil_tmp46 ; 3200 unsigned long __cil_tmp47 ; 3201 unsigned long __cil_tmp48 ; 3202 int __cil_tmp49 ; 3203 unsigned long __cil_tmp50 ; 3204 unsigned long __cil_tmp51 ; 3205 unsigned long __cil_tmp52 ; 3206 int __cil_tmp53 ; 3207 unsigned char __cil_tmp54 ; 3208 unsigned long __cil_tmp55 ; 3209 unsigned long __cil_tmp56 ; 3210 int __cil_tmp57 ; 3211 unsigned long __cil_tmp58 ; 3212 unsigned long __cil_tmp59 ; 3213 unsigned long __cil_tmp60 ; 3214 unsigned long __cil_tmp61 ; 3215 int __cil_tmp62 ; 3216 unsigned long __cil_tmp63 ; 3217 unsigned long __cil_tmp64 ; 3218 unsigned long __cil_tmp65 ; 3219 int __cil_tmp66 ; 3220 unsigned char __cil_tmp67 ; 3221 unsigned long __cil_tmp68 ; 3222 unsigned long __cil_tmp69 ; 3223 int __cil_tmp70 ; 3224 int __cil_tmp71 ; 3225 unsigned long __cil_tmp72 ; 3226 unsigned long __cil_tmp73 ; 3227 unsigned long __cil_tmp74 ; 3228 unsigned long __cil_tmp75 ; 3229 int __cil_tmp76 ; 3230 unsigned long __cil_tmp77 ; 3231 3232 { 3233 { 3234#line 89 3235 __cil_tmp2 = (unsigned long )pi; 3236#line 89 3237 __cil_tmp3 = __cil_tmp2 + 8; 3238#line 89 3239 __cil_tmp4 = *((int *)__cil_tmp3); 3240#line 89 3241 __cil_tmp5 = __cil_tmp4 + 2; 3242#line 89 3243 outb((unsigned char)11, __cil_tmp5); 3244 } 3245 { 3246#line 89 3247 __cil_tmp6 = (unsigned long )pi; 3248#line 89 3249 __cil_tmp7 = __cil_tmp6 + 16; 3250#line 89 3251 if (*((int *)__cil_tmp7)) { 3252 { 3253#line 89 3254 __cil_tmp8 = (unsigned long )pi; 3255#line 89 3256 __cil_tmp9 = __cil_tmp8 + 16; 3257#line 89 3258 __cil_tmp10 = *((int *)__cil_tmp9); 3259#line 89 3260 __cil_tmp11 = (unsigned long )__cil_tmp10; 3261#line 89 3262 __udelay(__cil_tmp11); 3263 } 3264 } else { 3265 3266 } 3267 } 3268 { 3269#line 89 3270 __cil_tmp12 = (unsigned long )pi; 3271#line 89 3272 __cil_tmp13 = __cil_tmp12 + 8; 3273#line 89 3274 __cil_tmp14 = *((int *)__cil_tmp13); 3275#line 89 3276 __cil_tmp15 = __cil_tmp14 + 2; 3277#line 89 3278 outb((unsigned char)10, __cil_tmp15); 3279 } 3280 { 3281#line 89 3282 __cil_tmp16 = (unsigned long )pi; 3283#line 89 3284 __cil_tmp17 = __cil_tmp16 + 16; 3285#line 89 3286 if (*((int *)__cil_tmp17)) { 3287 { 3288#line 89 3289 __cil_tmp18 = (unsigned long )pi; 3290#line 89 3291 __cil_tmp19 = __cil_tmp18 + 16; 3292#line 89 3293 __cil_tmp20 = *((int *)__cil_tmp19); 3294#line 89 3295 __cil_tmp21 = (unsigned long )__cil_tmp20; 3296#line 89 3297 __udelay(__cil_tmp21); 3298 } 3299 } else { 3300 3301 } 3302 } 3303 { 3304#line 89 3305 __cil_tmp22 = (unsigned long )pi; 3306#line 89 3307 __cil_tmp23 = __cil_tmp22 + 8; 3308#line 89 3309 __cil_tmp24 = *((int *)__cil_tmp23); 3310#line 89 3311 outb((unsigned char)160, __cil_tmp24); 3312 } 3313 { 3314#line 89 3315 __cil_tmp25 = (unsigned long )pi; 3316#line 89 3317 __cil_tmp26 = __cil_tmp25 + 16; 3318#line 89 3319 if (*((int *)__cil_tmp26)) { 3320 { 3321#line 89 3322 __cil_tmp27 = (unsigned long )pi; 3323#line 89 3324 __cil_tmp28 = __cil_tmp27 + 16; 3325#line 89 3326 __cil_tmp29 = *((int *)__cil_tmp28); 3327#line 89 3328 __cil_tmp30 = (unsigned long )__cil_tmp29; 3329#line 89 3330 __udelay(__cil_tmp30); 3331 } 3332 } else { 3333 3334 } 3335 } 3336 { 3337#line 89 3338 __cil_tmp31 = (unsigned long )pi; 3339#line 89 3340 __cil_tmp32 = __cil_tmp31 + 8; 3341#line 89 3342 __cil_tmp33 = *((int *)__cil_tmp32); 3343#line 89 3344 __cil_tmp34 = __cil_tmp33 + 2; 3345#line 89 3346 outb((unsigned char)3, __cil_tmp34); 3347 } 3348 { 3349#line 89 3350 __cil_tmp35 = (unsigned long )pi; 3351#line 89 3352 __cil_tmp36 = __cil_tmp35 + 16; 3353#line 89 3354 if (*((int *)__cil_tmp36)) { 3355 { 3356#line 89 3357 __cil_tmp37 = (unsigned long )pi; 3358#line 89 3359 __cil_tmp38 = __cil_tmp37 + 16; 3360#line 89 3361 __cil_tmp39 = *((int *)__cil_tmp38); 3362#line 89 3363 __cil_tmp40 = (unsigned long )__cil_tmp39; 3364#line 89 3365 __udelay(__cil_tmp40); 3366 } 3367 } else { 3368 3369 } 3370 } 3371 { 3372#line 89 3373 __cil_tmp41 = (unsigned long )pi; 3374#line 89 3375 __cil_tmp42 = __cil_tmp41 + 8; 3376#line 89 3377 __cil_tmp43 = *((int *)__cil_tmp42); 3378#line 89 3379 __cil_tmp44 = __cil_tmp43 + 2; 3380#line 89 3381 outb((unsigned char)4, __cil_tmp44); 3382 } 3383 { 3384#line 89 3385 __cil_tmp45 = (unsigned long )pi; 3386#line 89 3387 __cil_tmp46 = __cil_tmp45 + 16; 3388#line 89 3389 if (*((int *)__cil_tmp46)) { 3390 { 3391#line 89 3392 __cil_tmp47 = (unsigned long )pi; 3393#line 89 3394 __cil_tmp48 = __cil_tmp47 + 16; 3395#line 89 3396 __cil_tmp49 = *((int *)__cil_tmp48); 3397#line 89 3398 __cil_tmp50 = (unsigned long )__cil_tmp49; 3399#line 89 3400 __udelay(__cil_tmp50); 3401 } 3402 } else { 3403 3404 } 3405 } 3406 { 3407#line 90 3408 __cil_tmp51 = (unsigned long )pi; 3409#line 90 3410 __cil_tmp52 = __cil_tmp51 + 36; 3411#line 90 3412 __cil_tmp53 = *((int *)__cil_tmp52); 3413#line 90 3414 __cil_tmp54 = (unsigned char )__cil_tmp53; 3415#line 90 3416 __cil_tmp55 = (unsigned long )pi; 3417#line 90 3418 __cil_tmp56 = __cil_tmp55 + 8; 3419#line 90 3420 __cil_tmp57 = *((int *)__cil_tmp56); 3421#line 90 3422 outb(__cil_tmp54, __cil_tmp57); 3423 } 3424 { 3425#line 90 3426 __cil_tmp58 = (unsigned long )pi; 3427#line 90 3428 __cil_tmp59 = __cil_tmp58 + 16; 3429#line 90 3430 if (*((int *)__cil_tmp59)) { 3431 { 3432#line 90 3433 __cil_tmp60 = (unsigned long )pi; 3434#line 90 3435 __cil_tmp61 = __cil_tmp60 + 16; 3436#line 90 3437 __cil_tmp62 = *((int *)__cil_tmp61); 3438#line 90 3439 __cil_tmp63 = (unsigned long )__cil_tmp62; 3440#line 90 3441 __udelay(__cil_tmp63); 3442 } 3443 } else { 3444 3445 } 3446 } 3447 { 3448#line 91 3449 __cil_tmp64 = (unsigned long )pi; 3450#line 91 3451 __cil_tmp65 = __cil_tmp64 + 40; 3452#line 91 3453 __cil_tmp66 = *((int *)__cil_tmp65); 3454#line 91 3455 __cil_tmp67 = (unsigned char )__cil_tmp66; 3456#line 91 3457 __cil_tmp68 = (unsigned long )pi; 3458#line 91 3459 __cil_tmp69 = __cil_tmp68 + 8; 3460#line 91 3461 __cil_tmp70 = *((int *)__cil_tmp69); 3462#line 91 3463 __cil_tmp71 = __cil_tmp70 + 2; 3464#line 91 3465 outb(__cil_tmp67, __cil_tmp71); 3466 } 3467 { 3468#line 91 3469 __cil_tmp72 = (unsigned long )pi; 3470#line 91 3471 __cil_tmp73 = __cil_tmp72 + 16; 3472#line 91 3473 if (*((int *)__cil_tmp73)) { 3474 { 3475#line 91 3476 __cil_tmp74 = (unsigned long )pi; 3477#line 91 3478 __cil_tmp75 = __cil_tmp74 + 16; 3479#line 91 3480 __cil_tmp76 = *((int *)__cil_tmp75); 3481#line 91 3482 __cil_tmp77 = (unsigned long )__cil_tmp76; 3483#line 91 3484 __udelay(__cil_tmp77); 3485 } 3486 } else { 3487 3488 } 3489 } 3490#line 92 3491 return; 3492} 3493} 3494#line 94 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 3495static void ktti_log_adapter(PIA *pi , char *scratch , int verbose ) 3496{ unsigned long __cil_tmp4 ; 3497 unsigned long __cil_tmp5 ; 3498 char *__cil_tmp6 ; 3499 unsigned long __cil_tmp7 ; 3500 unsigned long __cil_tmp8 ; 3501 int __cil_tmp9 ; 3502 unsigned long __cil_tmp10 ; 3503 unsigned long __cil_tmp11 ; 3504 int __cil_tmp12 ; 3505 3506 { 3507 { 3508#line 96 3509 __cil_tmp4 = (unsigned long )pi; 3510#line 96 3511 __cil_tmp5 = __cil_tmp4 + 24; 3512#line 96 3513 __cil_tmp6 = *((char **)__cil_tmp5); 3514#line 96 3515 __cil_tmp7 = (unsigned long )pi; 3516#line 96 3517 __cil_tmp8 = __cil_tmp7 + 8; 3518#line 96 3519 __cil_tmp9 = *((int *)__cil_tmp8); 3520#line 96 3521 __cil_tmp10 = (unsigned long )pi; 3522#line 96 3523 __cil_tmp11 = __cil_tmp10 + 16; 3524#line 96 3525 __cil_tmp12 = *((int *)__cil_tmp11); 3526#line 96 3527 printk("%s: ktti %s, KT adapter at 0x%x, delay %d\n", __cil_tmp6, "1.0", __cil_tmp9, 3528 __cil_tmp12); 3529 } 3530#line 99 3531 return; 3532} 3533} 3534#line 101 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 3535static struct pi_protocol ktti = 3536#line 101 3537 {{(char )'k', (char )'t', (char )'t', (char )'i', (char )'\000', (char)0, (char)0, 3538 (char)0}, 0, 1, 2, 1, 1, & ktti_write_regr, & ktti_read_regr, & ktti_write_block, 3539 & ktti_read_block, & ktti_connect, & ktti_disconnect, (int (*)(PIA * ))0, (int (*)(PIA * ))0, 3540 (int (*)(PIA * , char * , int ))0, & ktti_log_adapter, (int (*)(PIA * ))0, (void (*)(PIA * ))0, 3541 & __this_module}; 3542#line 117 3543static int ktti_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ; 3544#line 117 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 3545static int ktti_init(void) 3546{ int tmp ; 3547 3548 { 3549 { 3550#line 119 3551 tmp = paride_register(& ktti); 3552 } 3553#line 119 3554 return (tmp); 3555} 3556} 3557#line 122 3558static void ktti_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ; 3559#line 122 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 3560static void ktti_exit(void) 3561{ 3562 3563 { 3564 { 3565#line 124 3566 paride_unregister(& ktti); 3567 } 3568#line 125 3569 return; 3570} 3571} 3572#line 127 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 3573static char const __mod_license127[12] __attribute__((__used__, __unused__, __section__(".modinfo"), 3574__aligned__(1))) = 3575#line 127 3576 { (char const )'l', (char const )'i', (char const )'c', (char const )'e', 3577 (char const )'n', (char const )'s', (char const )'e', (char const )'=', 3578 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'}; 3579#line 128 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 3580int init_module(void) 3581{ int tmp ; 3582 3583 { 3584 { 3585#line 128 3586 tmp = ktti_init(); 3587 } 3588#line 128 3589 return (tmp); 3590} 3591} 3592#line 129 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 3593void cleanup_module(void) 3594{ 3595 3596 { 3597 { 3598#line 129 3599 ktti_exit(); 3600 } 3601#line 129 3602 return; 3603} 3604} 3605#line 147 3606void ldv_check_final_state(void) ; 3607#line 153 3608extern void ldv_initialize(void) ; 3609#line 156 3610extern int __VERIFIER_nondet_int(void) ; 3611#line 159 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 3612int LDV_IN_INTERRUPT ; 3613#line 162 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 3614void main(void) 3615{ PIA *var_ktti_write_regr_0_p0 ; 3616 int var_ktti_write_regr_0_p1 ; 3617 int var_ktti_write_regr_0_p2 ; 3618 int var_ktti_write_regr_0_p3 ; 3619 PIA *var_ktti_read_regr_1_p0 ; 3620 int var_ktti_read_regr_1_p1 ; 3621 int var_ktti_read_regr_1_p2 ; 3622 PIA *var_ktti_write_block_3_p0 ; 3623 char *var_ktti_write_block_3_p1 ; 3624 int var_ktti_write_block_3_p2 ; 3625 PIA *var_ktti_read_block_2_p0 ; 3626 char *var_ktti_read_block_2_p1 ; 3627 int var_ktti_read_block_2_p2 ; 3628 PIA *var_ktti_connect_4_p0 ; 3629 PIA *var_ktti_disconnect_5_p0 ; 3630 PIA *var_ktti_log_adapter_6_p0 ; 3631 char *var_ktti_log_adapter_6_p1 ; 3632 int var_ktti_log_adapter_6_p2 ; 3633 int tmp ; 3634 int ldv_s_ktti_pi_protocol ; 3635 int tmp___0 ; 3636 int tmp___1 ; 3637 int __cil_tmp23 ; 3638 3639 { 3640 { 3641#line 247 3642 LDV_IN_INTERRUPT = 1; 3643#line 256 3644 ldv_initialize(); 3645#line 265 3646 tmp = ktti_init(); 3647 } 3648#line 265 3649 if (tmp) { 3650#line 266 3651 goto ldv_final; 3652 } else { 3653 3654 } 3655#line 267 3656 ldv_s_ktti_pi_protocol = 0; 3657 { 3658#line 271 3659 while (1) { 3660 while_continue: /* CIL Label */ ; 3661 { 3662#line 271 3663 tmp___1 = __VERIFIER_nondet_int(); 3664 } 3665#line 271 3666 if (tmp___1) { 3667 3668 } else { 3669 { 3670#line 271 3671 __cil_tmp23 = ldv_s_ktti_pi_protocol == 0; 3672#line 271 3673 if (! __cil_tmp23) { 3674 3675 } else { 3676#line 271 3677 goto while_break; 3678 } 3679 } 3680 } 3681 { 3682#line 275 3683 tmp___0 = __VERIFIER_nondet_int(); 3684 } 3685#line 277 3686 if (tmp___0 == 0) { 3687#line 277 3688 goto case_0; 3689 } else 3690#line 296 3691 if (tmp___0 == 1) { 3692#line 296 3693 goto case_1; 3694 } else 3695#line 315 3696 if (tmp___0 == 2) { 3697#line 315 3698 goto case_2; 3699 } else 3700#line 334 3701 if (tmp___0 == 3) { 3702#line 334 3703 goto case_3; 3704 } else 3705#line 353 3706 if (tmp___0 == 4) { 3707#line 353 3708 goto case_4; 3709 } else 3710#line 372 3711 if (tmp___0 == 5) { 3712#line 372 3713 goto case_5; 3714 } else 3715#line 391 3716 if (tmp___0 == 6) { 3717#line 391 3718 goto case_6; 3719 } else { 3720 { 3721#line 410 3722 goto switch_default; 3723#line 275 3724 if (0) { 3725 case_0: /* CIL Label */ 3726#line 280 3727 if (ldv_s_ktti_pi_protocol == 0) { 3728 { 3729#line 288 3730 ktti_connect(var_ktti_connect_4_p0); 3731#line 289 3732 ldv_s_ktti_pi_protocol = ldv_s_ktti_pi_protocol + 1; 3733 } 3734 } else { 3735 3736 } 3737#line 295 3738 goto switch_break; 3739 case_1: /* CIL Label */ 3740#line 299 3741 if (ldv_s_ktti_pi_protocol == 1) { 3742 { 3743#line 307 3744 ktti_disconnect(var_ktti_disconnect_5_p0); 3745#line 308 3746 ldv_s_ktti_pi_protocol = 0; 3747 } 3748 } else { 3749 3750 } 3751#line 314 3752 goto switch_break; 3753 case_2: /* CIL Label */ 3754 { 3755#line 326 3756 ktti_write_regr(var_ktti_write_regr_0_p0, var_ktti_write_regr_0_p1, var_ktti_write_regr_0_p2, 3757 var_ktti_write_regr_0_p3); 3758 } 3759#line 333 3760 goto switch_break; 3761 case_3: /* CIL Label */ 3762 { 3763#line 345 3764 ktti_read_regr(var_ktti_read_regr_1_p0, var_ktti_read_regr_1_p1, var_ktti_read_regr_1_p2); 3765 } 3766#line 352 3767 goto switch_break; 3768 case_4: /* CIL Label */ 3769 { 3770#line 364 3771 ktti_write_block(var_ktti_write_block_3_p0, var_ktti_write_block_3_p1, var_ktti_write_block_3_p2); 3772 } 3773#line 371 3774 goto switch_break; 3775 case_5: /* CIL Label */ 3776 { 3777#line 383 3778 ktti_read_block(var_ktti_read_block_2_p0, var_ktti_read_block_2_p1, var_ktti_read_block_2_p2); 3779 } 3780#line 390 3781 goto switch_break; 3782 case_6: /* CIL Label */ 3783 { 3784#line 402 3785 ktti_log_adapter(var_ktti_log_adapter_6_p0, var_ktti_log_adapter_6_p1, var_ktti_log_adapter_6_p2); 3786 } 3787#line 409 3788 goto switch_break; 3789 switch_default: /* CIL Label */ 3790#line 410 3791 goto switch_break; 3792 } else { 3793 switch_break: /* CIL Label */ ; 3794 } 3795 } 3796 } 3797 } 3798 while_break: /* CIL Label */ ; 3799 } 3800 { 3801#line 425 3802 ktti_exit(); 3803 } 3804 ldv_final: 3805 { 3806#line 428 3807 ldv_check_final_state(); 3808 } 3809#line 431 3810 return; 3811} 3812} 3813#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h" 3814void ldv_blast_assert(void) 3815{ 3816 3817 { 3818 ERROR: 3819#line 6 3820 goto ERROR; 3821} 3822} 3823#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h" 3824extern int __VERIFIER_nondet_int(void) ; 3825#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3826int ldv_mutex = 1; 3827#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3828int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) 3829{ int nondetermined ; 3830 3831 { 3832#line 29 3833 if (ldv_mutex == 1) { 3834 3835 } else { 3836 { 3837#line 29 3838 ldv_blast_assert(); 3839 } 3840 } 3841 { 3842#line 32 3843 nondetermined = __VERIFIER_nondet_int(); 3844 } 3845#line 35 3846 if (nondetermined) { 3847#line 38 3848 ldv_mutex = 2; 3849#line 40 3850 return (0); 3851 } else { 3852#line 45 3853 return (-4); 3854 } 3855} 3856} 3857#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3858int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) 3859{ int nondetermined ; 3860 3861 { 3862#line 57 3863 if (ldv_mutex == 1) { 3864 3865 } else { 3866 { 3867#line 57 3868 ldv_blast_assert(); 3869 } 3870 } 3871 { 3872#line 60 3873 nondetermined = __VERIFIER_nondet_int(); 3874 } 3875#line 63 3876 if (nondetermined) { 3877#line 66 3878 ldv_mutex = 2; 3879#line 68 3880 return (0); 3881 } else { 3882#line 73 3883 return (-4); 3884 } 3885} 3886} 3887#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3888int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 3889{ int atomic_value_after_dec ; 3890 3891 { 3892#line 83 3893 if (ldv_mutex == 1) { 3894 3895 } else { 3896 { 3897#line 83 3898 ldv_blast_assert(); 3899 } 3900 } 3901 { 3902#line 86 3903 atomic_value_after_dec = __VERIFIER_nondet_int(); 3904 } 3905#line 89 3906 if (atomic_value_after_dec == 0) { 3907#line 92 3908 ldv_mutex = 2; 3909#line 94 3910 return (1); 3911 } else { 3912 3913 } 3914#line 98 3915 return (0); 3916} 3917} 3918#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3919void mutex_lock(struct mutex *lock ) 3920{ 3921 3922 { 3923#line 108 3924 if (ldv_mutex == 1) { 3925 3926 } else { 3927 { 3928#line 108 3929 ldv_blast_assert(); 3930 } 3931 } 3932#line 110 3933 ldv_mutex = 2; 3934#line 111 3935 return; 3936} 3937} 3938#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3939int mutex_trylock(struct mutex *lock ) 3940{ int nondetermined ; 3941 3942 { 3943#line 121 3944 if (ldv_mutex == 1) { 3945 3946 } else { 3947 { 3948#line 121 3949 ldv_blast_assert(); 3950 } 3951 } 3952 { 3953#line 124 3954 nondetermined = __VERIFIER_nondet_int(); 3955 } 3956#line 127 3957 if (nondetermined) { 3958#line 130 3959 ldv_mutex = 2; 3960#line 132 3961 return (1); 3962 } else { 3963#line 137 3964 return (0); 3965 } 3966} 3967} 3968#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3969void mutex_unlock(struct mutex *lock ) 3970{ 3971 3972 { 3973#line 147 3974 if (ldv_mutex == 2) { 3975 3976 } else { 3977 { 3978#line 147 3979 ldv_blast_assert(); 3980 } 3981 } 3982#line 149 3983 ldv_mutex = 1; 3984#line 150 3985 return; 3986} 3987} 3988#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3989void ldv_check_final_state(void) 3990{ 3991 3992 { 3993#line 156 3994 if (ldv_mutex == 1) { 3995 3996 } else { 3997 { 3998#line 156 3999 ldv_blast_assert(); 4000 } 4001 } 4002#line 157 4003 return; 4004} 4005} 4006#line 440 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16807/dscv_tempdir/dscv/ri/32_1/drivers/block/paride/ktti.c.common.c" 4007long s__builtin_expect(long val , long res ) 4008{ 4009 4010 { 4011#line 441 4012 return (val); 4013} 4014}

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--ktti.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file:	3818
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 187

Source: