Showing error 848

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

Source: 

4471  tmp___0 = __VERIFIER_nondet_int();
4472  }
4473#line 356
4474  if (tmp___0 != 0) {
4475#line 358
4476    goto ldv_22622;
4477  } else
4478#line 356
4479  if (ldv_s_mma8450_driver_i2c_driver != 0) {
4480#line 358
4481    goto ldv_22622;
4482  } else {
4483#line 360
4484    goto ldv_22624;
4485  }
4486  ldv_22624: ;
4487  ldv_module_exit: ;
4488  {
4489#line 409
4490  ldv_check_final_state();
4491  }
4492#line 412
4493  return;
4494}
4495}
4496#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3030/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4497void ldv_blast_assert(void) 
4498{ 
4499
4500  {
4501  ERROR: ;
4502#line 6
4503  goto ERROR;
4504}
4505}
4506#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3030/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4507extern int __VERIFIER_nondet_int(void) ;
4508#line 433 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3030/dscv_tempdir/dscv/ri/43_1a/drivers/input/misc/mma8450.c.p"
4509int ldv_spin  =    0;
4510#line 437 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3030/dscv_tempdir/dscv/ri/43_1a/drivers/input/misc/mma8450.c.p"
4511void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑