8425 }
8426 ldv_42127: ;
8427 ldv_42133:
8428 {
8429#line 254
8430 tmp___0 = __VERIFIER_nondet_int();
8431 }
8432#line 254
8433 if (tmp___0 != 0) {
8434#line 255
8435 goto ldv_42132;
8436 } else {
8437#line 257
8438 goto ldv_42134;
8439 }
8440 ldv_42134: ;
8441
8442 {
8443#line 332
8444 ldv_check_final_state();
8445 }
8446#line 335
8447 return;
8448}
8449}
8450#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7362/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
8451void ldv_blast_assert(void)
8452{
8453
8454 {
8455 ERROR: ;
8456#line 6
8457 goto ERROR;
8458}
8459}
8460#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7362/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
8461extern int __VERIFIER_nondet_int(void) ;
8462#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7362/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/cx88/cx88-vp3054-i2c.c.p"
8463int ldv_spin = 0;
8464#line 360 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7362/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/cx88/cx88-vp3054-i2c.c.p"
8465void ldv_check_alloc_flags(gfp_t flags )