3592 goto ldv_19024;
3593 } else
3594#line 266
3595 if (ldv_s_gen_74x164_driver_spi_driver != 0) {
3596#line 268
3597 goto ldv_19024;
3598 } else {
3599#line 270
3600 goto ldv_19026;
3601 }
3602 ldv_19026: ;
3603 ldv_module_exit:
3604 {
3605#line 303
3606 gen_74x164_exit();
3607 }
3608 ldv_final:
3609 {
3610#line 306
3611 ldv_check_final_state();
3612 }
3613#line 309
3614 return;
3615}
3616}
3617#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2747/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3618void ldv_blast_assert(void)
3619{
3620
3621 {
3622 ERROR: ;
3623#line 6
3624 goto ERROR;
3625}
3626}
3627#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2747/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3628extern int __VERIFIER_nondet_int(void) ;
3629#line 330 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2747/dscv_tempdir/dscv/ri/43_1a/drivers/gpio/gpio-74x164.c.p"
3630int ldv_spin = 0;
3631#line 334 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2747/dscv_tempdir/dscv/ri/43_1a/drivers/gpio/gpio-74x164.c.p"
3632void ldv_check_alloc_flags(gfp_t flags )