Showing error 42

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_inw_unsafe.cil.c
Line in file: 5992
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

5962}
5963#line 1633 "concatenated.c"
5964void __VERIFIER_assume(int phi ) 
5965{ 
5966
5967  {
5968  {
5969#line 1633
5970  while (1) {
5971    while_18_continue: /* CIL Label */ ;
5972#line 1633
5973    if (! phi) {
5974
5975    } else {
5976      goto while_18_break;
5977    }
5978  }
5979  while_18_break: /* CIL Label */ ;
5980  }
5981#line 1633
5982  return;
5983}
5984}
5985#line 1634 "concatenated.c"
5986void __VERIFIER_assert(int phi , char *txt ) 
5987{ 
5988
5989  {
5990#line 1634
5991  if (! phi) {
5992    ERROR: 
5993    goto ERROR;
5994  } else {
5995
5996  }
5997#line 1634
5998  return;
5999}
6000}
6001#line 1636 "concatenated.c"
6002int nonseekable_open(struct inode *inode , struct file *filp )
Show full sources
↑