4915 tmp___0 = __VERIFIER_nondet_int();
4916 }
4917#line 405
4918 if (tmp___0 != 0) {
4919#line 407
4920 goto ldv_26155;
4921 } else
4922#line 405
4923 if (ldv_s_vgg2432a4_driver_spi_driver != 0) {
4924#line 407
4925 goto ldv_26155;
4926 } else {
4927#line 409
4928 goto ldv_26157;
4929 }
4930 ldv_26157: ;
4931 ldv_module_exit: ;
4932 {
4933#line 538
4934 ldv_check_final_state();
4935 }
4936#line 541
4937 return;
4938}
4939}
4940#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1342/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4941void ldv_blast_assert(void)
4942{
4943
4944 {
4945 ERROR: ;
4946#line 6
4947 goto ERROR;
4948}
4949}
4950#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1342/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4951extern int __VERIFIER_nondet_int(void) ;
4952#line 562 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1342/dscv_tempdir/dscv/ri/43_1a/drivers/video/backlight/vgg2432a4.c.p"
4953int ldv_spin = 0;
4954#line 566 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1342/dscv_tempdir/dscv/ri/43_1a/drivers/video/backlight/vgg2432a4.c.p"
4955void ldv_check_alloc_flags(gfp_t flags )