7745 goto ldv_24883;
7746 } else
7747#line 3075
7748 if (ldv_s_xuartps_platform_driver_platform_driver != 0) {
7749#line 3077
7750 goto ldv_24883;
7751 } else {
7752#line 3079
7753 goto ldv_24885;
7754 }
7755 ldv_24885: ;
7756 ldv_module_exit:
7757 {
7758#line 5237
7759 xuartps_exit();
7760 }
7761 ldv_final:
7762 {
7763#line 5240
7764 ldv_check_final_state();
7765 }
7766#line 5243
7767 return;
7768}
7769}
7770#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17434/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7771void ldv_blast_assert(void)
7772{
7773
7774 {
7775 ERROR: ;
7776#line 6
7777 goto ERROR;
7778}
7779}
7780#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17434/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7781extern int __VERIFIER_nondet_int(void) ;
7782#line 5264 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17434/dscv_tempdir/dscv/ri/43_1a/drivers/tty/serial/xilinx_uartps.c.p"
7783int ldv_spin = 0;
7784#line 5268 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17434/dscv_tempdir/dscv/ri/43_1a/drivers/tty/serial/xilinx_uartps.c.p"
7785void ldv_check_alloc_flags(gfp_t flags )