3222 goto ldv_19180;
3223 } else
3224#line 204
3225 if (ldv_s_max7301_driver_spi_driver != 0) {
3226#line 206
3227 goto ldv_19180;
3228 } else {
3229#line 208
3230 goto ldv_19182;
3231 }
3232 ldv_19182: ;
3233 ldv_module_exit:
3234 {
3235#line 241
3236 max7301_exit();
3237 }
3238 ldv_final:
3239 {
3240#line 244
3241 ldv_check_final_state();
3242 }
3243#line 247
3244 return;
3245}
3246}
3247#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2754/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3248void ldv_blast_assert(void)
3249{
3250
3251 {
3252 ERROR: ;
3253#line 6
3254 goto ERROR;
3255}
3256}
3257#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2754/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3258extern int __VERIFIER_nondet_int(void) ;
3259#line 268 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2754/dscv_tempdir/dscv/ri/43_1a/drivers/gpio/gpio-max7301.c.p"
3260int ldv_spin = 0;
3261#line 272 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2754/dscv_tempdir/dscv/ri/43_1a/drivers/gpio/gpio-max7301.c.p"
3262void ldv_check_alloc_flags(gfp_t flags )