13804 switch_default:
13805#line 1107
13806 goto switch_break;
13807 } else {
13808 switch_break: ;
13809 }
13810 }
13811 }
13812 }
13813 while_break: ;
13814 }
13815 ldv_module_exit:
13816 {
13817#line 1119
13818 rtl28xxu_module_exit();
13819 }
13820 ldv_final:
13821 {
13822#line 1122
13823 ldv_check_final_state();
13824 }
13825#line 1125
13826 return;
13827}
13828}
13829#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13538/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
13830void ldv_blast_assert(void)
13831{
13832
13833 {
13834 ERROR:
13835#line 6
13836 goto ERROR;
13837}
13838}
13839#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13538/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
13840extern int __VERIFIER_nondet_int(void) ;
13841#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13538/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
13842int ldv_mutex = 1;
13843#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13538/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
13844int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )