3973 switch_default:
3974#line 458
3975 goto switch_break;
3976 } else {
3977 switch_break: ;
3978 }
3979 }
3980 }
3981 }
3982 while_break: ;
3983 }
3984 ldv_module_exit:
3985 {
3986#line 473
3987 zc_exit();
3988 }
3989 ldv_final:
3990 {
3991#line 476
3992 ldv_check_final_state();
3993 }
3994#line 479
3995 return;
3996}
3997}
3998#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/238/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3999void ldv_blast_assert(void)
4000{
4001
4002 {
4003 ERROR:
4004#line 6
4005 goto ERROR;
4006}
4007}
4008#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/238/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4009extern int __VERIFIER_nondet_int(void) ;
4010#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/238/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4011int ldv_mutex = 1;
4012#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/238/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4013int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )