Showing error 1346

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_unsafe_ok_linux-43_1a-drivers--misc--sgi-xp--xpc.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 10717
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

10687#line 1475
10688  tmp___1 = __VERIFIER_nondet_int();
10689  }
10690#line 1475
10691  if (tmp___1 != 0) {
10692#line 1476
10693    goto ldv_19506;
10694  } else {
10695#line 1478
10696    goto ldv_19508;
10697  }
10698  ldv_19508: ;
10699  {
10700#line 1575
10701  xpc_exit();
10702  }
10703  ldv_final: 
10704  {
10705#line 1578
10706  ldv_check_final_state();
10707  }
10708#line 1581
10709  return;
10710}
10711}
10712#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12523/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
10713void ldv_blast_assert(void) 
10714{ 
10715
10716  {
10717  ERROR: ;
10718#line 6
10719  goto ERROR;
10720}
10721}
10722#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12523/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
10723extern int __VERIFIER_nondet_int(void) ;
10724#line 1602 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12523/dscv_tempdir/dscv/ri/43_1a/drivers/misc/sgi-xp/xpc_main.c.p"
10725int ldv_spin  =    0;
10726#line 1606 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12523/dscv_tempdir/dscv/ri/43_1a/drivers/misc/sgi-xp/xpc_main.c.p"
10727void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑