3432 goto ldv_18183;
3433 } else
3434#line 478
3435 if (ldv_s_wafwdt_fops_file_operations != 0) {
3436#line 480
3437 goto ldv_18183;
3438 } else {
3439#line 482
3440 goto ldv_18185;
3441 }
3442 ldv_18185: ;
3443 ldv_module_exit:
3444 {
3445#line 612
3446 wafwdt_exit();
3447 }
3448 ldv_final:
3449 {
3450#line 615
3451 ldv_check_final_state();
3452 }
3453#line 618
3454 return;
3455}
3456}
3457#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17372/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3458void ldv_blast_assert(void)
3459{
3460
3461 {
3462 ERROR: ;
3463#line 6
3464 goto ERROR;
3465}
3466}
3467#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17372/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3468extern int __VERIFIER_nondet_int(void) ;
3469#line 639 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17372/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wafer5823wdt.c.p"
3470int ldv_spin = 0;
3471#line 643 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17372/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/wafer5823wdt.c.p"
3472void ldv_check_alloc_flags(gfp_t flags )