Showing error 741

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_7_cilled_unsafe_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 14798
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

14768        } else {
14769
14770        }
14771#line 1004
14772        goto switch_break;
14773        switch_default: /* CIL Label */ 
14774#line 1005
14775        goto switch_break;
14776      } else {
14777        switch_break: /* CIL Label */ ;
14778      }
14779      }
14780    }
14781  }
14782  while_break: /* CIL Label */ ;
14783  }
14784  ldv_module_exit: 
14785  {
14786#line 1014
14787  ldv_check_final_state();
14788  }
14789#line 1017
14790  return;
14791}
14792}
14793#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13517/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
14794void ldv_blast_assert(void) 
14795{ 
14796
14797  {
14798  ERROR: 
14799#line 6
14800  goto ERROR;
14801}
14802}
14803#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13517/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
14804extern int __VERIFIER_nondet_int(void) ;
14805#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13517/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14806int ldv_mutex  =    1;
14807#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13517/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14808int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock )
Show full sources
↑