6731 switch_default:
6732#line 490
6733 goto switch_break;
6734 } else {
6735 switch_break: ;
6736 }
6737 }
6738 }
6739 }
6740 while_break: ;
6741 }
6742 ldv_module_exit:
6743 {
6744#line 509
6745 mcp2120_sir_cleanup();
6746 }
6747 ldv_final:
6748 {
6749#line 517
6750 ldv_check_final_state();
6751 }
6752#line 520
6753 return;
6754}
6755}
6756#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9306/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6757void ldv_blast_assert(void)
6758{
6759
6760 {
6761 ERROR:
6762#line 6
6763 goto ERROR;
6764}
6765}
6766#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9306/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6767extern int __VERIFIER_nondet_int(void) ;
6768#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9306/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6769int ldv_mutex = 1;
6770#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9306/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6771int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )