Showing error 119

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-video-aty-aty128fb.ko_safe.cil.out.i.pp.cil.c
Line in file: 12495
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

12465    goto ldv_31858;
12466  } else
12467#line 4348
12468  if (ldv_s_aty128fb_driver_pci_driver != 0) {
12469#line 4350
12470    goto ldv_31858;
12471  } else {
12472#line 4352
12473    goto ldv_31860;
12474  }
12475  ldv_31860: ;
12476  ldv_module_exit: 
12477  {
12478#line 6197
12479  aty128fb_exit();
12480  }
12481  ldv_final: 
12482  {
12483#line 6204
12484  ldv_check_final_state();
12485  }
12486#line 6207
12487  return;
12488}
12489}
12490#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/video/aty/aty128fb.ko--X--chewlinux-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"
12491void ldv_blast_assert(void) 
12492{ 
12493
12494  {
12495  ERROR: ;
12496#line 6
12497  goto ERROR;
12498}
12499}
12500#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/video/aty/aty128fb.ko--X--chewlinux-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"
12501extern int ldv_undefined_int(void) ;
12502#line 6224 "/anthill/stuff/tacas-comp/work/current--X--drivers/video/aty/aty128fb.ko--X--chewlinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/video/aty/aty128fb.c.p"
12503int ldv_module_refcounter  =    1;
12504#line 6227 "/anthill/stuff/tacas-comp/work/current--X--drivers/video/aty/aty128fb.ko--X--chewlinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/video/aty/aty128fb.c.p"
12505void ldv_module_get(struct module *module ) 
Show full sources