1821 goto ldv_20099;
1822 } else
1823#line 216
1824 if (ldv_s_rdc321x_sb_driver_pci_driver != 0) {
1825#line 218
1826 goto ldv_20099;
1827 } else {
1828#line 220
1829 goto ldv_20101;
1830 }
1831 ldv_20101: ;
1832 ldv_module_exit:
1833 {
1834#line 253
1835 rdc321x_sb_exit();
1836 }
1837 ldv_final:
1838 {
1839#line 256
1840 ldv_check_final_state();
1841 }
1842#line 259
1843 return;
1844}
1845}
1846#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1847void ldv_blast_assert(void)
1848{
1849
1850 {
1851 ERROR: ;
1852#line 6
1853 goto ERROR;
1854}
1855}
1856#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1857extern int __VERIFIER_nondet_int(void) ;
1858#line 280 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1859int ldv_spin = 0;
1860#line 284 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5001/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/rdc321x-southbridge.c.p"
1861void ldv_check_alloc_flags(gfp_t flags )