6525 __cil_tmp28 = & etdev->eeprom_data;
6526#line 407
6527 __cil_tmp29 = (u8 *)__cil_tmp28;
6528#line 407
6529 __cil_tmp30 = __cil_tmp29 + 1UL;
6530#line 407
6531 eeprom_read(etdev, 113U, __cil_tmp30);
6532 }
6533 {
6534#line 409
6535 __cil_tmp31 = etdev->eeprom_data[0];
6536#line 409
6537 __cil_tmp32 = (unsigned int )__cil_tmp31;
6538#line 409
6539 if (__cil_tmp32 != 205U) {
6540#line 411
6541 etdev->eeprom_data[1] = (u8 )0U;
6542 } else {
6543
6544 }
6545 }
6546#line 413
6547 return (0);
6548}
6549}
6550#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/staging/et131x/et131x.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/19/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
6551void ldv_blast_assert(void)
6552{
6553
6554 {
6555 ERROR: ;
6556#line 6
6557 goto ERROR;
6558}
6559}
6560#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/staging/et131x/et131x.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/19/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
6561extern int ldv_undefined_int(void) ;
6562#line 423 "/anthill/stuff/tacas-comp/work/current--X--drivers/staging/et131x/et131x.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/19/dscv_tempdir/dscv/ri/08_1/drivers/staging/et131x/et1310_eeprom.c.p"
6563void ldv_check_final_state(void) ;
6564#line 426 "/anthill/stuff/tacas-comp/work/current--X--drivers/staging/et131x/et131x.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/19/dscv_tempdir/dscv/ri/08_1/drivers/staging/et131x/et1310_eeprom.c.p"
6565int ldv_module_refcounter = 1;