5380 goto ldv_25745;
5381 } else
5382#line 527
5383 if (ldv_s_sd_desc_sd_desc != 0) {
5384#line 530
5385 goto ldv_25745;
5386 } else
5387#line 527
5388 if (ldv_s_sd_driver_usb_driver != 0) {
5389#line 530
5390 goto ldv_25745;
5391 } else {
5392#line 532
5393 goto ldv_25747;
5394 }
5395 ldv_25747: ;
5396 ldv_module_exit: ;
5397 {
5398#line 712
5399 ldv_check_final_state();
5400 }
5401#line 715
5402 return;
5403}
5404}
5405#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7656/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5406void ldv_blast_assert(void)
5407{
5408
5409 {
5410 ERROR: ;
5411#line 6
5412 goto ERROR;
5413}
5414}
5415#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7656/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5416extern int __VERIFIER_nondet_int(void) ;
5417#line 736 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7656/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/gspca/sq905c.c.p"
5418int ldv_spin = 0;
5419#line 740 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7656/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/gspca/sq905c.c.p"
5420void ldv_check_alloc_flags(gfp_t flags )