Showing error 1302

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

Source: 

5700  tmp___0 = __VERIFIER_nondet_int();
5701  }
5702#line 690
5703  if (tmp___0 != 0) {
5704#line 692
5705    goto ldv_26119;
5706  } else
5707#line 690
5708  if (ldv_s_tdo24m_driver_spi_driver != 0) {
5709#line 692
5710    goto ldv_26119;
5711  } else {
5712#line 694
5713    goto ldv_26121;
5714  }
5715  ldv_26121: ;
5716  ldv_module_exit: ;
5717  {
5718#line 937
5719  ldv_check_final_state();
5720  }
5721#line 940
5722  return;
5723}
5724}
5725#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1341/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5726void ldv_blast_assert(void) 
5727{ 
5728
5729  {
5730  ERROR: ;
5731#line 6
5732  goto ERROR;
5733}
5734}
5735#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1341/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5736extern int __VERIFIER_nondet_int(void) ;
5737#line 961 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1341/dscv_tempdir/dscv/ri/43_1a/drivers/video/backlight/tdo24m.c.p"
5738int ldv_spin  =    0;
5739#line 965 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1341/dscv_tempdir/dscv/ri/43_1a/drivers/video/backlight/tdo24m.c.p"
5740void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑