Showing error 130

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-safe_1.cil.c
Line in file: 13
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

 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  {
Show full sources
↑