Showing error 1377

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 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 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: 
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  {
24#line 18
25  __cil_tmp2 = a->is_locked;
26#line 18
27  if (__cil_tmp2 == 1) {
28    {
29#line 18
30    err();
31    }
32  } else {
33
34  }
35  }
36#line 19
37  a->is_locked = 1;
38#line 20
39  return;
40}
41}
42#line 22 "files/mutex_lock_struct.c"
43void mutex_unlock(struct mutex *b ) 
44{ int __cil_tmp2 ;
45
46  {
47  {
48#line 24
49  __cil_tmp2 = b->is_locked;
50#line 24
51  if (__cil_tmp2 != 1) {
52    {
53#line 24
54    err();
55    }
56  } else {
57
58  }
59  }
60#line 25
61  b->is_locked = 0;
62#line 26
63  return;
64}
65}
66#line 28 "files/mutex_lock_struct.c"
67int main(void) 
68{ struct mutex m ;
69
70  {
71  {
72#line 31
73  m.is_locked = 0;
74#line 33
75  mutex_lock(& m);
76#line 37
77  mutex_lock(& m);
78  }
79#line 40
80  return (0);
81}
82}