276#line 109
277 if (0) {
278 switch_default:
279#line 111
280 goto switch_break;
281 } else {
282 switch_break: ;
283 }
284 }
285 }
286 while_break: ;
287 }
288 {
289#line 123
290 exit_rc_map_lirc();
291 }
292 ldv_final:
293 {
294#line 126
295 ldv_check_final_state();
296 }
297#line 129
298 return;
299}
300}
301#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12910/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
302void ldv_blast_assert(void)
303{
304
305 {
306 ERROR:
307#line 6
308 goto ERROR;
309}
310}
311#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12910/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
312extern int __VERIFIER_nondet_int(void) ;
313#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12910/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
314int ldv_mutex = 1;
315#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12910/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
316int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )