Showing error 282

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

Source: 

3395        switch_default: /* CIL Label */ 
3396#line 367
3397        goto switch_break;
3398      } else {
3399        switch_break: /* CIL Label */ ;
3400      }
3401      }
3402    }
3403  }
3404  while_break: /* CIL Label */ ;
3405  }
3406  ldv_module_exit: 
3407  {
3408#line 382
3409  gunze_exit();
3410  }
3411  ldv_final: 
3412  {
3413#line 385
3414  ldv_check_final_state();
3415  }
3416#line 388
3417  return;
3418}
3419}
3420#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3421void ldv_blast_assert(void) 
3422{ 
3423
3424  {
3425  ERROR: 
3426#line 6
3427  goto ERROR;
3428}
3429}
3430#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3431extern int __VERIFIER_nondet_int(void) ;
3432#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3433int ldv_mutex  =    1;
3434#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3435int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock )
Show full sources
↑