Showing error 263

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

Source: 

4161        } else {
4162
4163        }
4164#line 393
4165        goto switch_break;
4166        switch_default: /* CIL Label */ 
4167#line 394
4168        goto switch_break;
4169      } else {
4170        switch_break: /* CIL Label */ ;
4171      }
4172      }
4173    }
4174  }
4175  while_break: /* CIL Label */ ;
4176  }
4177  ldv_module_exit: 
4178  {
4179#line 403
4180  ldv_check_final_state();
4181  }
4182#line 406
4183  return;
4184}
4185}
4186#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4007/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4187void ldv_blast_assert(void) 
4188{ 
4189
4190  {
4191  ERROR: 
4192#line 6
4193  goto ERROR;
4194}
4195}
4196#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4007/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4197extern int __VERIFIER_nondet_int(void) ;
4198#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4007/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4199int ldv_mutex  =    1;
4200#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4007/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4201int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock )
Show full sources
↑