6412 switch_default:
6413#line 312
6414 goto switch_break;
6415 } else {
6416 switch_break: ;
6417 }
6418 }
6419 }
6420 }
6421 while_break: ;
6422 }
6423 ldv_module_exit:
6424 {
6425#line 324
6426 old_belkin_sir_cleanup();
6427 }
6428 ldv_final:
6429 {
6430#line 327
6431 ldv_check_final_state();
6432 }
6433#line 330
6434 return;
6435}
6436}
6437#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9309/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6438void ldv_blast_assert(void)
6439{
6440
6441 {
6442 ERROR:
6443#line 6
6444 goto ERROR;
6445}
6446}
6447#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9309/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6448extern int __VERIFIER_nondet_int(void) ;
6449#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9309/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6450int ldv_mutex = 1;
6451#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9309/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6452int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )