7206 switch_default:
7207#line 3515
7208 goto switch_break;
7209 } else {
7210 switch_break: ;
7211 }
7212 }
7213 }
7214 }
7215 while_break: ;
7216 }
7217 ldv_module_exit:
7218 {
7219#line 3577
7220 altera_uart_exit();
7221 }
7222 ldv_final:
7223 {
7224#line 3580
7225 ldv_check_final_state();
7226 }
7227#line 3583
7228 return;
7229}
7230}
7231#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16486/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7232void ldv_blast_assert(void)
7233{
7234
7235 {
7236 ERROR:
7237#line 6
7238 goto ERROR;
7239}
7240}
7241#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16486/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7242extern int __VERIFIER_nondet_int(void) ;
7243#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16486/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7244int ldv_mutex = 1;
7245#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16486/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7246int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )