Showing error 802

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

Source: 

2582#line 160
2583  tmp___1 = __VERIFIER_nondet_int();
2584  }
2585#line 160
2586  if (tmp___1 != 0) {
2587#line 161
2588    goto ldv_19743;
2589  } else {
2590#line 163
2591    goto ldv_19745;
2592  }
2593  ldv_19745: ;
2594  {
2595#line 193
2596  saitek_exit();
2597  }
2598  ldv_final: 
2599  {
2600#line 196
2601  ldv_check_final_state();
2602  }
2603#line 199
2604  return;
2605}
2606}
2607#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4855/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2608void ldv_blast_assert(void) 
2609{ 
2610
2611  {
2612  ERROR: ;
2613#line 6
2614  goto ERROR;
2615}
2616}
2617#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4855/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2618extern int __VERIFIER_nondet_int(void) ;
2619#line 220 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4855/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-saitek.c.p"
2620int ldv_spin  =    0;
2621#line 224 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4855/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-saitek.c.p"
2622void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑