Showing error 1372

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

Source: 

 1# 1 "files/mutex_lock_int.c"
 2# 1 "<built-in>"
 3# 1 "<command-line>"
 4# 1 "files/mutex_lock_int.c"
 5
 6
 7
 8
 9
10
11
12
13
14
15void err()
16{ ERROR: goto ERROR; }
17
18void mutex_lock(int *a)
19{
20 if (*a == 1) err();
21 *a = 1;
22}
23
24void mutex_unlock(int *b)
25{
26 if (*b != 1) err();
27 *b = 0;
28}
29
30int main()
31{
32 int m;
33 m = 0;
34
35 mutex_lock(&m);
36
37 mutex_unlock(&m);
38
39
40
41
42}
↑