5451 } else {
5452
5453 }
5454#line 505
5455 goto switch_break;
5456 switch_default:
5457#line 506
5458 goto switch_break;
5459 } else {
5460 switch_break: ;
5461 }
5462 }
5463 }
5464 }
5465 while_break: ;
5466 }
5467 ldv_module_exit:
5468 {
5469#line 515
5470 ldv_check_final_state();
5471 }
5472#line 518
5473 return;
5474}
5475}
5476#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5477void ldv_blast_assert(void)
5478{
5479
5480 {
5481 ERROR:
5482#line 6
5483 goto ERROR;
5484}
5485}
5486#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5487extern int __VERIFIER_nondet_int(void) ;
5488#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5489int ldv_mutex = 1;
5490#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5491int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )