2810 goto ldv_21785;
2811 } else
2812#line 407
2813 if (ldv_s_cmodio_pci_driver_pci_driver != 0) {
2814#line 409
2815 goto ldv_21785;
2816 } else {
2817#line 411
2818 goto ldv_21787;
2819 }
2820 ldv_21787: ;
2821 ldv_module_exit:
2822 {
2823#line 456
2824 cmodio_exit();
2825 }
2826 ldv_final:
2827 {
2828#line 459
2829 ldv_check_final_state();
2830 }
2831#line 462
2832 return;
2833}
2834}
2835#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4996/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2836void ldv_blast_assert(void)
2837{
2838
2839 {
2840 ERROR: ;
2841#line 6
2842 goto ERROR;
2843}
2844}
2845#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4996/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2846extern int __VERIFIER_nondet_int(void) ;
2847#line 483 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4996/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/janz-cmodio.c.p"
2848int ldv_spin = 0;
2849#line 487 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4996/dscv_tempdir/dscv/ri/43_1a/drivers/mfd/janz-cmodio.c.p"
2850void ldv_check_alloc_flags(gfp_t flags )