6841 goto ldv_24920;
6842 } else
6843#line 2024
6844 if (ldv_s_altera_uart_platform_driver_platform_driver != 0) {
6845#line 2026
6846 goto ldv_24920;
6847 } else {
6848#line 2028
6849 goto ldv_24922;
6850 }
6851 ldv_24922: ;
6852 ldv_module_exit:
6853 {
6854#line 3591
6855 altera_uart_exit();
6856 }
6857 ldv_final:
6858 {
6859#line 3594
6860 ldv_check_final_state();
6861 }
6862#line 3597
6863 return;
6864}
6865}
6866#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17423/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6867void ldv_blast_assert(void)
6868{
6869
6870 {
6871 ERROR: ;
6872#line 6
6873 goto ERROR;
6874}
6875}
6876#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17423/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6877extern int __VERIFIER_nondet_int(void) ;
6878#line 3618 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17423/dscv_tempdir/dscv/ri/43_1a/drivers/tty/serial/altera_uart.c.p"
6879int ldv_spin = 0;
6880#line 3622 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17423/dscv_tempdir/dscv/ri/43_1a/drivers/tty/serial/altera_uart.c.p"
6881void ldv_check_alloc_flags(gfp_t flags )