4074 goto ldv_19285;
4075 } else
4076#line 504
4077 if (ldv_s_advwdt_driver_platform_driver != 0) {
4078#line 507
4079 goto ldv_19285;
4080 } else {
4081#line 509
4082 goto ldv_19287;
4083 }
4084 ldv_19287: ;
4085 ldv_module_exit:
4086 {
4087#line 663
4088 advwdt_exit();
4089 }
4090 ldv_final:
4091 {
4092#line 666
4093 ldv_check_final_state();
4094 }
4095#line 669
4096 return;
4097}
4098}
4099#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17336/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4100void ldv_blast_assert(void)
4101{
4102
4103 {
4104 ERROR: ;
4105#line 6
4106 goto ERROR;
4107}
4108}
4109#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17336/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4110extern int __VERIFIER_nondet_int(void) ;
4111#line 690 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17336/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/advantechwdt.c.p"
4112int ldv_spin = 0;
4113#line 694 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17336/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/advantechwdt.c.p"
4114void ldv_check_alloc_flags(gfp_t flags )