Showing error 1298

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

Source: 

4823  {
4824#line 345
4825  tmp___0 = __VERIFIER_nondet_int();
4826  }
4827#line 345
4828  if (tmp___0 != 0) {
4829#line 346
4830    goto ldv_25808;
4831  } else {
4832#line 348
4833    goto ldv_25810;
4834  }
4835  ldv_25810: ;
4836  {
4837#line 367
4838  lcd_class_exit();
4839  }
4840  {
4841#line 370
4842  ldv_check_final_state();
4843  }
4844#line 373
4845  return;
4846}
4847}
4848#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1331/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4849void ldv_blast_assert(void) 
4850{ 
4851
4852  {
4853  ERROR: ;
4854#line 6
4855  goto ERROR;
4856}
4857}
4858#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1331/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4859extern int __VERIFIER_nondet_int(void) ;
4860#line 394 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1331/dscv_tempdir/dscv/ri/43_1a/drivers/video/backlight/lcd.c.p"
4861int ldv_spin  =    0;
4862#line 398 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1331/dscv_tempdir/dscv/ri/43_1a/drivers/video/backlight/lcd.c.p"
4863void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑