2309 goto ldv_18859;
2310 } else
2311#line 263
2312 if (ldv_s_nop_usb_xceiv_driver_platform_driver != 0) {
2313#line 265
2314 goto ldv_18859;
2315 } else {
2316#line 267
2317 goto ldv_18861;
2318 }
2319 ldv_18861: ;
2320 ldv_module_exit:
2321 {
2322#line 300
2323 nop_usb_xceiv_exit();
2324 }
2325 ldv_final:
2326 {
2327#line 303
2328 ldv_check_final_state();
2329 }
2330#line 306
2331 return;
2332}
2333}
2334#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2335void ldv_blast_assert(void)
2336{
2337
2338 {
2339 ERROR: ;
2340#line 6
2341 goto ERROR;
2342}
2343}
2344#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2345extern int __VERIFIER_nondet_int(void) ;
2346#line 327 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2347int ldv_spin = 0;
2348#line 331 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2349void ldv_check_alloc_flags(gfp_t flags )