8397 goto switch_break;
8398 switch_default:
8399#line 743
8400 goto switch_break;
8401 } else {
8402 switch_break: ;
8403 }
8404 }
8405 }
8406 }
8407 while_break: ;
8408 }
8409 {
8410#line 764
8411 qlogicfas408_exit();
8412 }
8413 ldv_final:
8414 {
8415#line 767
8416 ldv_check_final_state();
8417 }
8418#line 770
8419 return;
8420}
8421}
8422#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/969/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
8423void ldv_blast_assert(void)
8424{
8425
8426 {
8427 ERROR:
8428#line 6
8429 goto ERROR;
8430}
8431}
8432#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/969/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
8433extern int __VERIFIER_nondet_int(void) ;
8434#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/969/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8435int ldv_mutex = 1;
8436#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/969/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8437int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )