Showing error 909

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--common--tuners--mxl5007t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 9343
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

9313  tmp___0 = __VERIFIER_nondet_int();
9314  }
9315#line 1222
9316  if (tmp___0 != 0) {
9317#line 1224
9318    goto ldv_24032;
9319  } else
9320#line 1222
9321  if (ldv_s_mxl5007t_tuner_ops_dvb_tuner_ops != 0) {
9322#line 1224
9323    goto ldv_24032;
9324  } else {
9325#line 1226
9326    goto ldv_24034;
9327  }
9328  ldv_24034: ;
9329
9330  {
9331#line 1557
9332  ldv_check_final_state();
9333  }
9334#line 1560
9335  return;
9336}
9337}
9338#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9525/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
9339void ldv_blast_assert(void) 
9340{ 
9341
9342  {
9343  ERROR: ;
9344#line 6
9345  goto ERROR;
9346}
9347}
9348#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9525/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
9349extern int __VERIFIER_nondet_int(void) ;
9350#line 1581 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9525/dscv_tempdir/dscv/ri/43_1a/drivers/media/common/tuners/mxl5007t.c.p"
9351int ldv_spin  =    0;
9352#line 1585 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9525/dscv_tempdir/dscv/ri/43_1a/drivers/media/common/tuners/mxl5007t.c.p"
9353void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑