Showing error 900

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

Source: 

2470#line 349
2471  tmp___1 = __VERIFIER_nondet_int();
2472  }
2473#line 349
2474  if (tmp___1 != 0) {
2475#line 350
2476    goto ldv_17201;
2477  } else {
2478#line 352
2479    goto ldv_17203;
2480  }
2481  ldv_17203: ;
2482  {
2483#line 414
2484  gpio_trig_exit();
2485  }
2486  ldv_final: 
2487  {
2488#line 417
2489  ldv_check_final_state();
2490  }
2491#line 420
2492  return;
2493}
2494}
2495#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12460/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2496void ldv_blast_assert(void) 
2497{ 
2498
2499  {
2500  ERROR: ;
2501#line 6
2502  goto ERROR;
2503}
2504}
2505#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12460/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2506extern int __VERIFIER_nondet_int(void) ;
2507#line 441 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12460/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-gpio.c.p"
2508int ldv_spin  =    0;
2509#line 445 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12460/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-gpio.c.p"
2510void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑