User: | Jiri Slaby |
Error type: | Reachable Error Location |
Error type description: | A specified error location is reachable in some program path |
File location: | ldv-regression/mutex_lock_struct.c-unsafe.cil.c |
Line in file: | 13 |
Project: | SV-COMP 2012 |
Tools: |
Manual Work
|
Entered: | 2012-11-19 13:47:39 UTC |
1/* Generated by CIL v. 1.3.7 */ 2/* print_CIL_Input is true */ 3 4#line 12 "files/mutex_lock_struct.c" 5struct mutex { 6 int is_locked ; 7}; 8#line 9 "files/mutex_lock_struct.c" 9void err(void) 10{ 11 12 { 13 ERROR:assert(0); 14#line 10 15 goto ERROR; 16} 17} 18#line 16 "files/mutex_lock_struct.c" 19void mutex_lock(struct mutex *a ) 20{ int __cil_tmp2 ; 21 22 { 23 {