Showing error 189

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/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--block--paride--on26.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 24722
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

24692        goto switch_break;
24693        switch_default: /* CIL Label */ 
24694#line 728
24695        goto switch_break;
24696      } else {
24697        switch_break: /* CIL Label */ ;
24698      }
24699      }
24700    }
24701  }
24702  while_break: /* CIL Label */ ;
24703  }
24704  {
24705#line 748
24706  on26_exit();
24707  }
24708  ldv_final: 
24709  {
24710#line 751
24711  ldv_check_final_state();
24712  }
24713#line 754
24714  return;
24715}
24716}
24717#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16809/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
24718void ldv_blast_assert(void) 
24719{ 
24720
24721  {
24722  ERROR: 
24723#line 6
24724  goto ERROR;
24725}
24726}
24727#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16809/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
24728extern int __VERIFIER_nondet_int(void) ;
24729#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16809/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
24730int ldv_mutex  =    1;
24731#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16809/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
24732int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock )
Show full sources
↑