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_inb_p_safe.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 |
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 )