6917 goto ldv_28179;
6918 } else
6919#line 824
6920 if (ldv_s_vfb_driver_platform_driver != 0) {
6921#line 826
6922 goto ldv_28179;
6923 } else {
6924#line 828
6925 goto ldv_28181;
6926 }
6927 ldv_28181: ;
6928 ldv_module_exit:
6929 {
6930#line 1048
6931 vfb_exit();
6932 }
6933 ldv_final:
6934 {
6935#line 1054
6936 ldv_check_final_state();
6937 }
6938#line 1057
6939 return;
6940}
6941}
6942#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1638/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6943void ldv_blast_assert(void)
6944{
6945
6946 {
6947 ERROR: ;
6948#line 6
6949 goto ERROR;
6950}
6951}
6952#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1638/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6953extern int __VERIFIER_nondet_int(void) ;
6954#line 1078 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1638/dscv_tempdir/dscv/ri/43_1a/drivers/video/vfb.c.p"
6955int ldv_spin = 0;
6956#line 1082 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1638/dscv_tempdir/dscv/ri/43_1a/drivers/video/vfb.c.p"
6957void ldv_check_alloc_flags(gfp_t flags )