6108 switch_default:
6109#line 2222
6110 goto switch_break;
6111 } else {
6112 switch_break: ;
6113 }
6114 }
6115 }
6116 }
6117 while_break: ;
6118 }
6119 ldv_module_exit:
6120 {
6121#line 2262
6122 altera_jtaguart_exit();
6123 }
6124 ldv_final:
6125 {
6126#line 2265
6127 ldv_check_final_state();
6128 }
6129#line 2268
6130 return;
6131}
6132}
6133#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16485/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6134void ldv_blast_assert(void)
6135{
6136
6137 {
6138 ERROR:
6139#line 6
6140 goto ERROR;
6141}
6142}
6143#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16485/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6144extern int __VERIFIER_nondet_int(void) ;
6145#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16485/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6146int ldv_mutex = 1;
6147#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16485/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6148int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )