2338 switch_default:
2339#line 314
2340 goto switch_break;
2341 } else {
2342 switch_break: ;
2343 }
2344 }
2345 }
2346 }
2347 while_break: ;
2348 }
2349 ldv_module_exit:
2350 {
2351#line 330
2352 i2o_bus_exit();
2353 }
2354 ldv_final:
2355 {
2356#line 333
2357 ldv_check_final_state();
2358 }
2359#line 336
2360 return;
2361}
2362}
2363#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1072/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2364void ldv_blast_assert(void)
2365{
2366
2367 {
2368 ERROR:
2369#line 6
2370 goto ERROR;
2371}
2372}
2373#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1072/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2374extern int __VERIFIER_nondet_int(void) ;
2375#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1072/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2376int ldv_mutex = 1;
2377#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1072/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2378int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )