Showing error 737

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_7_cilled_unsafe_const_ok_linux-32_1-drivers--gpu--drm--vmwgfx--vmwgfx.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 14600
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

14570#line 1374
14571  tmp___11 = __builtin_expect(__cil_tmp51, 0L);
14572  }
14573#line 1374
14574  if (tmp___11) {
14575#line 1375
14576    goto out_unlock;
14577  } else {
14578
14579  }
14580  {
14581#line 1377
14582  vmw_kms_cursor_post_execbuf(dev_priv);
14583  }
14584  out_unlock: 
14585  {
14586#line 1380
14587  __cil_tmp52 = (struct ttm_lock *)vmaster;
14588#line 1380
14589  ttm_read_unlock(__cil_tmp52);
14590  }
14591#line 1381
14592  return (ret);
14593}
14594}
14595#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6447/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
14596void ldv_blast_assert(void) 
14597{ 
14598
14599  {
14600  ERROR: 
14601#line 6
14602  goto ERROR;
14603}
14604}
14605#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6447/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
14606extern int __VERIFIER_nondet_int(void) ;
14607#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6447/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14608int ldv_mutex  =    1;
14609#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6447/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14610int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock )
Show full sources
↑