6445 switch_default:
6446#line 305
6447 goto switch_break;
6448 } else {
6449 switch_break: ;
6450 }
6451 }
6452 }
6453 }
6454 while_break: ;
6455 }
6456 ldv_module_exit:
6457 {
6458#line 317
6459 ixj_pcmcia_exit();
6460 }
6461 ldv_final:
6462 {
6463#line 320
6464 ldv_check_final_state();
6465 }
6466#line 323
6467 return;
6468}
6469}
6470#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/2058/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6471void ldv_blast_assert(void)
6472{
6473
6474 {
6475 ERROR:
6476#line 6
6477 goto ERROR;
6478}
6479}
6480#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/2058/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6481extern int __VERIFIER_nondet_int(void) ;
6482#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/2058/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6483int ldv_mutex = 1;
6484#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/2058/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6485int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )