Showing error 798

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

Source: 

2811#line 189
2812  tmp___1 = __VERIFIER_nondet_int();
2813  }
2814#line 189
2815  if (tmp___1 != 0) {
2816#line 190
2817    goto ldv_19763;
2818  } else {
2819#line 192
2820    goto ldv_19765;
2821  }
2822  ldv_19765: ;
2823  {
2824#line 245
2825  mr_exit();
2826  }
2827  ldv_final: 
2828  {
2829#line 248
2830  ldv_check_final_state();
2831  }
2832#line 251
2833  return;
2834}
2835}
2836#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4838/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2837void ldv_blast_assert(void) 
2838{ 
2839
2840  {
2841  ERROR: ;
2842#line 6
2843  goto ERROR;
2844}
2845}
2846#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4838/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2847extern int __VERIFIER_nondet_int(void) ;
2848#line 272 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4838/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-monterey.c.p"
2849int ldv_spin  =    0;
2850#line 276 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4838/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-monterey.c.p"
2851void ldv_check_alloc_flags(gfp_t flags )
Show full sources
↑