4374 goto ldv_18860;
4375 } else
4376#line 437
4377 if (ldv_s_tle62x0_driver_spi_driver != 0) {
4378#line 439
4379 goto ldv_18860;
4380 } else {
4381#line 441
4382 goto ldv_18862;
4383 }
4384 ldv_18862: ;
4385 ldv_module_exit:
4386 {
4387#line 488
4388 tle62x0_exit();
4389 }
4390 ldv_final:
4391 {
4392#line 491
4393 ldv_check_final_state();
4394 }
4395#line 494
4396 return;
4397}
4398}
4399#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2801/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4400void ldv_blast_assert(void)
4401{
4402
4403 {
4404 ERROR: ;
4405#line 6
4406 goto ERROR;
4407}
4408}
4409#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2801/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4410extern int __VERIFIER_nondet_int(void) ;
4411#line 515 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2801/dscv_tempdir/dscv/ri/43_1a/drivers/spi/spi-tle62x0.c.p"
4412int ldv_spin = 0;
4413#line 519 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2801/dscv_tempdir/dscv/ri/43_1a/drivers/spi/spi-tle62x0.c.p"
4414void ldv_check_alloc_flags(gfp_t flags )