Showing error 128

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_int.c-safe_1.cil.c
Line in file: 9
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 10 "files/mutex_lock_int.c"
 5void err(void) 
 6{ 
 7
 8  {
 9  ERROR:assert(0); 
10#line 11
11  goto ERROR;
12}
13}
14#line 13 "files/mutex_lock_int.c"
15void mutex_lock(int *a ) 
16{ int __cil_tmp2 ;
17
18  {
19  {
20#line 15
21  __cil_tmp2 = *a;
22#line 15
23  if (__cil_tmp2 == 1) {
24    {
25#line 15
26    err();
27    }
28  } else {
29
30  }
31  }
32#line 16
33  *a = 1;
34#line 17
35  return;
36}
37}
38#line 19 "files/mutex_lock_int.c"
39void mutex_unlock(int *b ) 
40{ int __cil_tmp2 ;
41
42  {
43  {
44#line 21
45  __cil_tmp2 = *b;
46#line 21
47  if (__cil_tmp2 != 1) {
48    {
49#line 21
50    err();
51    }
52  } else {
53
54  }
55  }
56#line 22
57  *b = 0;
58#line 23
59  return;
60}
61}
62#line 25 "files/mutex_lock_int.c"
63int main(void) 
64{ int m ;
65
66  {
67  {
68#line 28
69  m = 0;
70#line 30
71  mutex_lock(& m);
72#line 32
73  mutex_unlock(& m);
74  }
75#line 37
76  return (0);
77}
78}
↑