19023 goto ldv_23141;
19024 } else
19025#line 7327
19026 if (ldv_s_pch_udc_driver_pci_driver != 0) {
19027#line 7329
19028 goto ldv_23141;
19029 } else {
19030#line 7331
19031 goto ldv_23143;
19032 }
19033 ldv_23143: ;
19034 ldv_module_exit:
19035 {
19036#line 11552
19037 pch_udc_pci_exit();
19038 }
19039 ldv_final:
19040 {
19041#line 11555
19042 ldv_check_final_state();
19043 }
19044#line 11558
19045 return;
19046}
19047}
19048#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1983/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
19049void ldv_blast_assert(void)
19050{
19051
19052 {
19053 ERROR: ;
19054#line 6
19055 goto ERROR;
19056}
19057}
19058#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1983/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
19059extern int __VERIFIER_nondet_int(void) ;
19060#line 11579 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1983/dscv_tempdir/dscv/ri/43_1a/drivers/usb/gadget/pch_udc.c.p"
19061int ldv_spin = 0;
19062#line 11583 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1983/dscv_tempdir/dscv/ri/43_1a/drivers/usb/gadget/pch_udc.c.p"
19063void ldv_check_alloc_flags(gfp_t flags )