Showing error 1378

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.i
Line in file: 15
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_struct.c"
 2# 1 "<built-in>"
 3# 1 "<command-line>"
 4# 1 "files/mutex_lock_struct.c"
 5
 6
 7
 8
 9
10
11
12
13
14void err()
15{ ERROR: goto ERROR; }
16
17struct mutex {
18 int is_locked;
19};
20
21void mutex_lock(struct mutex *a)
22{
23 if (a->is_locked == 1) err();
24 a->is_locked = 1;
25}
Show full sources
↑