Showing error 178

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-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.c
Line in file: 6702
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

6672    goto ldv_24711;
6673  } else
6674#line 729
6675  if (ldv_s_magicmouse_driver_hid_driver != 0) {
6676#line 731
6677    goto ldv_24711;
6678  } else {
6679#line 733
6680    goto ldv_24713;
6681  }
6682  ldv_24713: ;
6683  ldv_module_exit: 
6684  {
6685#line 874
6686  magicmouse_exit();
6687  }
6688  ldv_final: 
6689  {
6690#line 877
6691  ldv_check_final_state();
6692  }
6693#line 880
6694  return;
6695}
6696}
6697#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/hid/hid-magicmouse.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"
6698void ldv_blast_assert(void) 
6699{ 
6700
6701  {
6702  ERROR: ;
6703#line 6
6704  goto ERROR;
6705}
6706}
6707#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/hid/hid-magicmouse.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"
6708extern int ldv_undefined_int(void) ;
6709#line 897 "/anthill/stuff/tacas-comp/work/current--X--drivers/hid/hid-magicmouse.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/hid/hid-magicmouse.c.p"
6710int ldv_module_refcounter  =    1;
6711#line 900 "/anthill/stuff/tacas-comp/work/current--X--drivers/hid/hid-magicmouse.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/hid/hid-magicmouse.c.p"
6712void ldv_module_get(struct module *module ) 
Show full sources