5391 {
5392#line 388
5393 tua6100_get_frequency(var_group1, var_tua6100_get_frequency_3_p1);
5394 }
5395#line 395
5396 goto switch_break;
5397 switch_default:
5398#line 396
5399 goto switch_break;
5400 } else {
5401 switch_break: ;
5402 }
5403 }
5404 }
5405 }
5406 while_break: ;
5407 }
5408 {
5409#line 405
5410 ldv_check_final_state();
5411 }
5412#line 408
5413 return;
5414}
5415}
5416#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5417void ldv_blast_assert(void)
5418{
5419
5420 {
5421 ERROR:
5422#line 6
5423 goto ERROR;
5424}
5425}
5426#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5427extern int __VERIFIER_nondet_int(void) ;
5428#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5429int ldv_mutex = 1;
5430#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5431int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )