Showing error 317

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

Source: 

1226        goto switch_break;
1227        switch_default: /* CIL Label */ 
1228#line 138
1229        goto switch_break;
1230      } else {
1231        switch_break: /* CIL Label */ ;
1232      }
1233      }
1234    }
1235  }
1236  while_break: /* CIL Label */ ;
1237  }
1238  {
1239#line 150
1240  defon_trig_exit();
1241  }
1242  ldv_final: 
1243  {
1244#line 153
1245  ldv_check_final_state();
1246  }
1247#line 156
1248  return;
1249}
1250}
1251#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1252void ldv_blast_assert(void) 
1253{ 
1254
1255  {
1256  ERROR: 
1257#line 6
1258  goto ERROR;
1259}
1260}
1261#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1262extern int __VERIFIER_nondet_int(void) ;
1263#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1264int ldv_mutex  =    1;
1265#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1266int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock )
Show full sources
↑