5784 goto ldv_24864;
5785 } else
5786#line 1307
5787 if (ldv_s_altera_jtaguart_platform_driver_platform_driver != 0) {
5788#line 1309
5789 goto ldv_24864;
5790 } else {
5791#line 1311
5792 goto ldv_24866;
5793 }
5794 ldv_24866: ;
5795 ldv_module_exit:
5796 {
5797#line 2276
5798 altera_jtaguart_exit();
5799 }
5800 ldv_final:
5801 {
5802#line 2279
5803 ldv_check_final_state();
5804 }
5805#line 2282
5806 return;
5807}
5808}
5809#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17422/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5810void ldv_blast_assert(void)
5811{
5812
5813 {
5814 ERROR: ;
5815#line 6
5816 goto ERROR;
5817}
5818}
5819#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17422/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5820extern int __VERIFIER_nondet_int(void) ;
5821#line 2303 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17422/dscv_tempdir/dscv/ri/43_1a/drivers/tty/serial/altera_jtaguart.c.p"
5822int ldv_spin = 0;
5823#line 2307 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17422/dscv_tempdir/dscv/ri/43_1a/drivers/tty/serial/altera_jtaguart.c.p"
5824void ldv_check_alloc_flags(gfp_t flags )