2621 goto ldv_21747;
2622 } else
2623#line 357
2624 if (ldv_s_matrox_w1_pci_driver_pci_driver != 0) {
2625#line 359
2626 goto ldv_21747;
2627 } else {
2628#line 361
2629 goto ldv_21749;
2630 }
2631 ldv_21749: ;
2632 ldv_module_exit:
2633 {
2634#line 414
2635 matrox_w1_fini();
2636 }
2637 ldv_final:
2638 {
2639#line 417
2640 ldv_check_final_state();
2641 }
2642#line 420
2643 return;
2644}
2645}
2646#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2647void ldv_blast_assert(void)
2648{
2649
2650 {
2651 ERROR: ;
2652#line 6
2653 goto ERROR;
2654}
2655}
2656#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2657extern int __VERIFIER_nondet_int(void) ;
2658#line 441 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/43_1a/drivers/w1/masters/matrox_w1.c.p"
2659int ldv_spin = 0;
2660#line 445 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/43_1a/drivers/w1/masters/matrox_w1.c.p"
2661void ldv_check_alloc_flags(gfp_t flags )