Showing error 118

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.c
Line in file: 5971
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

5941}
5942#line 1633 "concatenated.c"
5943void __VERIFIER_assume(int phi ) 
5944{ 
5945
5946  {
5947  {
5948#line 1633
5949  while (1) {
5950    while_18_continue: /* CIL Label */ ;
5951#line 1633
5952    if (! phi) {
5953
5954    } else {
5955      goto while_18_break;
5956    }
5957  }
5958  while_18_break: /* CIL Label */ ;
5959  }
5960#line 1633
5961  return;
5962}
5963}
5964#line 1634 "concatenated.c"
5965void __VERIFIER_assert(int phi , char *txt ) 
5966{ 
5967
5968  {
5969#line 1634
5970  if (! phi) {
5971    ERROR:assert(0); 
5972    goto ERROR;
5973  } else {
5974
5975  }
5976#line 1634
5977  return;
5978}
5979}
5980#line 1636 "concatenated.c"
5981int nonseekable_open(struct inode *inode , struct file *filp )
Show full sources
↑