2210#line 332
2211 tmp___1 = __VERIFIER_nondet_int();
2212 }
2213#line 332
2214 if (tmp___1 != 0) {
2215#line 333
2216 goto ldv_15478;
2217 } else {
2218#line 335
2219 goto ldv_15480;
2220 }
2221 ldv_15480: ;
2222 {
2223#line 353
2224 ramoops_exit();
2225 }
2226 ldv_final:
2227 {
2228#line 356
2229 ldv_check_final_state();
2230 }
2231#line 359
2232 return;
2233}
2234}
2235#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2236void ldv_blast_assert(void)
2237{
2238
2239 {
2240 ERROR: ;
2241#line 6
2242 goto ERROR;
2243}
2244}
2245#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2246extern int __VERIFIER_nondet_int(void) ;
2247#line 380 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2248int ldv_spin = 0;
2249#line 384 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2250void ldv_check_alloc_flags(gfp_t flags )