4615 goto ldv_28089;
4616 } else
4617#line 293
4618 if (ldv_s_cfag12864bfb_driver_platform_driver != 0) {
4619#line 295
4620 goto ldv_28089;
4621 } else {
4622#line 297
4623 goto ldv_28091;
4624 }
4625 ldv_28091: ;
4626 ldv_module_exit:
4627 {
4628#line 352
4629 cfag12864bfb_exit();
4630 }
4631 ldv_final:
4632 {
4633#line 355
4634 ldv_check_final_state();
4635 }
4636#line 358
4637 return;
4638}
4639}
4640#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17288/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4641void ldv_blast_assert(void)
4642{
4643
4644 {
4645 ERROR: ;
4646#line 6
4647 goto ERROR;
4648}
4649}
4650#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17288/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4651extern int __VERIFIER_nondet_int(void) ;
4652#line 379 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17288/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864bfb.c.p"
4653int ldv_spin = 0;
4654#line 383 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17288/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864bfb.c.p"
4655void ldv_check_alloc_flags(gfp_t flags )