Showing error 111

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-drivers/module_get_put-drivers-scsi-megaraid.ko_safe.cil.out.i.pp.cil.c
Line in file: 22665
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

22635    goto ldv_32904;
22636  } else
22637#line 5758
22638  if (ldv_s_megaraid_pci_driver_pci_driver != 0) {
22639#line 5761
22640    goto ldv_32904;
22641  } else {
22642#line 5763
22643    goto ldv_32906;
22644  }
22645  ldv_32906: ;
22646  ldv_module_exit: 
22647  {
22648#line 6479
22649  megaraid_exit();
22650  }
22651  ldv_final: 
22652  {
22653#line 6482
22654  ldv_check_final_state();
22655  }
22656#line 6485
22657  return;
22658}
22659}
22660#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/scsi/megaraid.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
22661void ldv_blast_assert(void) 
22662{ 
22663
22664  {
22665  ERROR: ;
22666#line 6
22667  goto ERROR;
22668}
22669}
22670#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/scsi/megaraid.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
22671extern int ldv_undefined_int(void) ;
22672#line 6502 "/anthill/stuff/tacas-comp/work/current--X--drivers/scsi/megaraid.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/scsi/megaraid.c.p"
22673int ldv_module_refcounter  =    1;
22674#line 6505 "/anthill/stuff/tacas-comp/work/current--X--drivers/scsi/megaraid.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/scsi/megaraid.c.p"
22675void ldv_module_get(struct module *module ) 
Show full sources