6763 switch_default:
6764#line 733
6765 goto switch_break;
6766 } else {
6767 switch_break: ;
6768 }
6769 }
6770 }
6771 }
6772 while_break: ;
6773 }
6774 ldv_module_exit:
6775 {
6776#line 777
6777 act200l_sir_cleanup();
6778 }
6779 ldv_final:
6780 {
6781#line 784
6782 ldv_check_final_state();
6783 }
6784#line 787
6785 return;
6786}
6787}
6788#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9294/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6789void ldv_blast_assert(void)
6790{
6791
6792 {
6793 ERROR:
6794#line 6
6795 goto ERROR;
6796}
6797}
6798#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9294/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6799extern int __VERIFIER_nondet_int(void) ;
6800#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9294/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6801int ldv_mutex = 1;
6802#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9294/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6803int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )