7270 switch_default:
7271#line 367
7272 goto switch_break;
7273 } else {
7274 switch_break: ;
7275 }
7276 }
7277 }
7278 }
7279 while_break: ;
7280 }
7281 ldv_module_exit:
7282 {
7283#line 385
7284 orinoco_tmd_exit();
7285 }
7286 ldv_final:
7287 {
7288#line 388
7289 ldv_check_final_state();
7290 }
7291#line 391
7292 return;
7293}
7294}
7295#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10310/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7296void ldv_blast_assert(void)
7297{
7298
7299 {
7300 ERROR:
7301#line 6
7302 goto ERROR;
7303}
7304}
7305#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10310/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7306extern int __VERIFIER_nondet_int(void) ;
7307#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10310/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7308int ldv_mutex = 1;
7309#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10310/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7310int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )