Showing error 173

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


Source:

7893    goto ldv_21812;
7894  } else
7895#line 1402
7896  if (ldv_s_pt_fops_file_operations != 0) {
7897#line 1404
7898    goto ldv_21812;
7899  } else {
7900#line 1406
7901    goto ldv_21814;
7902  }
7903  ldv_21814: ;
7904  ldv_module_exit: 
7905  {
7906#line 1785
7907  pt_exit();
7908  }
7909  ldv_final: 
7910  {
7911#line 1788
7912  ldv_check_final_state();
7913  }
7914#line 1791
7915  return;
7916}
7917}
7918#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-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"
7919void ldv_blast_assert(void) 
7920{ 
7921
7922  {
7923  ERROR: ;
7924#line 6
7925  goto ERROR;
7926}
7927}
7928#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-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"
7929extern int ldv_undefined_int(void) ;
7930#line 1808 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
7931int ldv_module_refcounter  =    1;
7932#line 1811 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/paride/pt.ko--X--safelinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/block/paride/pt.c.p"
7933void ldv_module_get(struct module *module ) 
Show full sources