Showing error 855

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

Source: 

4899#line 485
4900  tmp___1 = __VERIFIER_nondet_int();
4901  }
4902#line 485
4903  if (tmp___1 != 0) {
4904#line 486
4905    goto ldv_26643;
4906  } else {
4907#line 488
4908    goto ldv_26645;
4909  }
4910  ldv_26645: ;
4911  {
4912#line 522
4913  xenkbd_cleanup();
4914  }
4915  ldv_final: 
4916  {
4917#line 525
4918  ldv_check_final_state();
4919  }
4920#line 528
4921  return;
4922}
4923}
4924#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3040/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4925void ldv_blast_assert(void) 
4926{ 
4927
4928  {
4929  ERROR: ;
4930#line 6
4931  goto ERROR;
4932}
4933}
4934#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3040/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4935extern int __VERIFIER_nondet_int(void) ;
4936#line 549 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3040/dscv_tempdir/dscv/ri/43_1a/drivers/input/misc/xen-kbdfront.c.p"
4937int ldv_spin  =    0;
4938#line 553 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3040/dscv_tempdir/dscv/ri/43_1a/drivers/input/misc/xen-kbdfront.c.p"
4939void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑