927#line 408
928 LDV_IN_INTERRUPT = 1;
929 }
930#line 414
931 goto switch_break;
932 switch_default:
933#line 415
934 goto switch_break;
935 } else {
936 switch_break: ;
937 }
938 }
939 }
940 }
941 while_break: ;
942 }
943 ldv_module_exit:
944 {
945#line 424
946 ldv_check_final_state();
947 }
948#line 427
949 return;
950}
951}
952#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/53/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
953void ldv_blast_assert(void)
954{
955
956 {
957 ERROR:
958#line 6
959 goto ERROR;
960}
961}
962#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/53/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
963extern int __VERIFIER_nondet_int(void) ;
964#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/53/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
965int ldv_mutex = 1;
966#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/53/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
967int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )