1979 switch_default:
1980#line 345
1981 goto switch_break;
1982 } else {
1983 switch_break: ;
1984 }
1985 }
1986 }
1987 }
1988 while_break: ;
1989 }
1990 ldv_module_exit:
1991 {
1992#line 357
1993 tps65912_gpio_exit();
1994 }
1995 ldv_final:
1996 {
1997#line 360
1998 ldv_check_final_state();
1999 }
2000#line 363
2001 return;
2002}
2003}
2004#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5858/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2005void ldv_blast_assert(void)
2006{
2007
2008 {
2009 ERROR:
2010#line 6
2011 goto ERROR;
2012}
2013}
2014#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5858/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2015extern int __VERIFIER_nondet_int(void) ;
2016#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5858/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2017int ldv_mutex = 1;
2018#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5858/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2019int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )