3303 goto ldv_18140;
3304 } else
3305#line 469
3306 if (ldv_s_cpu5wdt_fops_file_operations != 0) {
3307#line 471
3308 goto ldv_18140;
3309 } else {
3310#line 473
3311 goto ldv_18142;
3312 }
3313 ldv_18142: ;
3314 ldv_module_exit:
3315 {
3316#line 617
3317 cpu5wdt_exit_module();
3318 }
3319 ldv_final:
3320 {
3321#line 620
3322 ldv_check_final_state();
3323 }
3324#line 623
3325 return;
3326}
3327}
3328#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17339/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3329void ldv_blast_assert(void)
3330{
3331
3332 {
3333 ERROR: ;
3334#line 6
3335 goto ERROR;
3336}
3337}
3338#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17339/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3339extern int __VERIFIER_nondet_int(void) ;
3340#line 644 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17339/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/cpu5wdt.c.p"
3341int ldv_spin = 0;
3342#line 648 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17339/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/cpu5wdt.c.p"
3343void ldv_check_alloc_flags(gfp_t flags )