9544 switch_default:
9545#line 2753
9546 goto switch_break;
9547 } else {
9548 switch_break: ;
9549 }
9550 }
9551 }
9552 }
9553 while_break: ;
9554 }
9555 ldv_module_exit:
9556 {
9557#line 2848
9558 exit_sym53c500_cs();
9559 }
9560 ldv_final:
9561 {
9562#line 2851
9563 ldv_check_final_state();
9564 }
9565#line 2854
9566 return;
9567}
9568}
9569#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/404/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
9570void ldv_blast_assert(void)
9571{
9572
9573 {
9574 ERROR:
9575#line 6
9576 goto ERROR;
9577}
9578}
9579#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/404/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
9580extern int __VERIFIER_nondet_int(void) ;
9581#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/404/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9582int ldv_mutex = 1;
9583#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/404/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9584int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )