5900 goto ldv_25744;
5901 } else
5902#line 515
5903 if (ldv_s_sd_desc_sd_desc != 0) {
5904#line 518
5905 goto ldv_25744;
5906 } else
5907#line 515
5908 if (ldv_s_sd_driver_usb_driver != 0) {
5909#line 518
5910 goto ldv_25744;
5911 } else {
5912#line 520
5913 goto ldv_25746;
5914 }
5915 ldv_25746: ;
5916 ldv_module_exit: ;
5917 {
5918#line 696
5919 ldv_check_final_state();
5920 }
5921#line 699
5922 return;
5923}
5924}
5925#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7660/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5926void ldv_blast_assert(void)
5927{
5928
5929 {
5930 ERROR: ;
5931#line 6
5932 goto ERROR;
5933}
5934}
5935#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7660/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5936extern int __VERIFIER_nondet_int(void) ;
5937#line 720 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7660/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/gspca/stv0680.c.p"
5938int ldv_spin = 0;
5939#line 724 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7660/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/gspca/stv0680.c.p"
5940void ldv_check_alloc_flags(gfp_t flags )