Showing error 43

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

Source: 

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