Showing error 859

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

Source: 

2989#line 299
2990  tmp___1 = __VERIFIER_nondet_int();
2991  }
2992#line 299
2993  if (tmp___1 != 0) {
2994#line 300
2995    goto ldv_20968;
2996  } else {
2997#line 302
2998    goto ldv_20970;
2999  }
3000  ldv_20970: ;
3001  {
3002#line 319
3003  parkbd_exit();
3004  }
3005  ldv_final: 
3006  {
3007#line 322
3008  ldv_check_final_state();
3009  }
3010#line 325
3011  return;
3012}
3013}
3014#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2972/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3015void ldv_blast_assert(void) 
3016{ 
3017
3018  {
3019  ERROR: ;
3020#line 6
3021  goto ERROR;
3022}
3023}
3024#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2972/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3025extern int __VERIFIER_nondet_int(void) ;
3026#line 346 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2972/dscv_tempdir/dscv/ri/43_1a/drivers/input/serio/parkbd.c.p"
3027int ldv_spin  =    0;
3028#line 350 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2972/dscv_tempdir/dscv/ri/43_1a/drivers/input/serio/parkbd.c.p"
3029void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑