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_BUG.cil.c |
Line in file: | 5993 |
Project: | SV-COMP 2012 |
Tools: |
Manual Work
|
Entered: | 2012-11-19 13:47:39 UTC |
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:assert(0); 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 )