6420 {
6421#line 449
6422 ili9320_set_power(var_group1, var_ili9320_set_power_9_p1);
6423 }
6424#line 460
6425 goto switch_break;
6426 switch_default:
6427#line 461
6428 goto switch_break;
6429 } else {
6430 switch_break: ;
6431 }
6432 }
6433 }
6434 }
6435 while_break: ;
6436 }
6437 {
6438#line 470
6439 ldv_check_final_state();
6440 }
6441#line 473
6442 return;
6443}
6444}
6445#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16918/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6446void ldv_blast_assert(void)
6447{
6448
6449 {
6450 ERROR:
6451#line 6
6452 goto ERROR;
6453}
6454}
6455#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16918/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6456extern int __VERIFIER_nondet_int(void) ;
6457#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16918/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6458int ldv_mutex = 1;
6459#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16918/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6460int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )