5756 switch_default:
5757#line 918
5758 goto switch_break;
5759 } else {
5760 switch_break: ;
5761 }
5762 }
5763 }
5764 }
5765 while_break: ;
5766 }
5767 ldv_module_exit:
5768 {
5769#line 947
5770 ab8500_usb_exit();
5771 }
5772 ldv_final:
5773 {
5774#line 950
5775 ldv_check_final_state();
5776 }
5777#line 953
5778 return;
5779}
5780}
5781#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7763/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5782void ldv_blast_assert(void)
5783{
5784
5785 {
5786 ERROR:
5787#line 6
5788 goto ERROR;
5789}
5790}
5791#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7763/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5792extern int __VERIFIER_nondet_int(void) ;
5793#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7763/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5794int ldv_mutex = 1;
5795#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7763/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5796int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )