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