15473 goto ldv_41057;
15474 } else
15475#line 1206
15476 if (ldv_s_driver_bttv_sub_driver != 0) {
15477#line 1208
15478 goto ldv_41057;
15479 } else {
15480#line 1210
15481 goto ldv_41059;
15482 }
15483 ldv_41059: ;
15484 ldv_module_exit:
15485 {
15486#line 1477
15487 dvb_bt8xx_exit();
15488 }
15489 ldv_final:
15490 {
15491#line 1480
15492 ldv_check_final_state();
15493 }
15494#line 1483
15495 return;
15496}
15497}
15498#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8632/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
15499void ldv_blast_assert(void)
15500{
15501
15502 {
15503 ERROR: ;
15504#line 6
15505 goto ERROR;
15506}
15507}
15508#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8632/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
15509extern int __VERIFIER_nondet_int(void) ;
15510#line 1504 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8632/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/bt8xx/dvb-bt8xx.c.p"
15511int ldv_spin = 0;
15512#line 1508 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8632/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/bt8xx/dvb-bt8xx.c.p"
15513void ldv_check_alloc_flags(gfp_t flags )