Showing error 1055

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/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--media--video--cx231xx--cx231xx-dvb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 13739
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

13709#line 914
13710  tmp___1 = __VERIFIER_nondet_int();
13711  }
13712#line 914
13713  if (tmp___1 != 0) {
13714#line 915
13715    goto ldv_42563;
13716  } else {
13717#line 917
13718    goto ldv_42565;
13719  }
13720  ldv_42565: ;
13721  {
13722#line 993
13723  cx231xx_dvb_unregister();
13724  }
13725  ldv_final: 
13726  {
13727#line 996
13728  ldv_check_final_state();
13729  }
13730#line 999
13731  return;
13732}
13733}
13734#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7454/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
13735void ldv_blast_assert(void) 
13736{ 
13737
13738  {
13739  ERROR: ;
13740#line 6
13741  goto ERROR;
13742}
13743}
13744#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7454/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
13745extern int __VERIFIER_nondet_int(void) ;
13746#line 1020 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7454/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/cx231xx/cx231xx-dvb.c.p"
13747int ldv_spin  =    0;
13748#line 1024 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7454/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/cx231xx/cx231xx-dvb.c.p"
13749void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑