9548 goto ldv_24323;
9549 } else
9550#line 1306
9551 if (ldv_s_mdc800_usb_driver_usb_driver != 0) {
9552#line 1309
9553 goto ldv_24323;
9554 } else {
9555#line 1311
9556 goto ldv_24325;
9557 }
9558 ldv_24325: ;
9559 ldv_module_exit:
9560 {
9561#line 1524
9562 usb_mdc800_cleanup();
9563 }
9564 ldv_final:
9565 {
9566#line 1527
9567 ldv_check_final_state();
9568 }
9569#line 1530
9570 return;
9571}
9572}
9573#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2028/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
9574void ldv_blast_assert(void)
9575{
9576
9577 {
9578 ERROR: ;
9579#line 6
9580 goto ERROR;
9581}
9582}
9583#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2028/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
9584extern int __VERIFIER_nondet_int(void) ;
9585#line 1551 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2028/dscv_tempdir/dscv/ri/43_1a/drivers/usb/image/mdc800.c.p"
9586int ldv_spin = 0;
9587#line 1555 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2028/dscv_tempdir/dscv/ri/43_1a/drivers/usb/image/mdc800.c.p"
9588void ldv_check_alloc_flags(gfp_t flags )