Showing error 1457

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: locks/test_locks_10_safe.c
Line in file: 159
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

  1extern int __VERIFIER_nondet_int();
  2int main()
  3{
  4    int p1 = __VERIFIER_nondet_int();  // condition variable
  5    int lk1; // lock variable
  6
  7    int p2 = __VERIFIER_nondet_int();  // condition variable
  8    int lk2; // lock variable
  9
 10    int p3 = __VERIFIER_nondet_int();  // condition variable
 11    int lk3; // lock variable
 12
 13    int p4 = __VERIFIER_nondet_int();  // condition variable
 14    int lk4; // lock variable
 15
 16    int p5 = __VERIFIER_nondet_int();  // condition variable
 17    int lk5; // lock variable
 18
 19    int p6 = __VERIFIER_nondet_int();  // condition variable
 20    int lk6; // lock variable
 21
 22    int p7 = __VERIFIER_nondet_int();  // condition variable
 23    int lk7; // lock variable
 24
 25    int p8 = __VERIFIER_nondet_int();  // condition variable
 26    int lk8; // lock variable
 27
 28    int p9 = __VERIFIER_nondet_int();  // condition variable
 29    int lk9; // lock variable
 30
 31    int p10 = __VERIFIER_nondet_int();  // condition variable
 32    int lk10; // lock variable
 33
 34
 35    int cond;
 36
 37    while(1) {
 38        cond = __VERIFIER_nondet_int();
 39        if (cond == 0) {
 40            goto out;
 41        } else {}
 42        lk1 = 0; // initially lock is open
 43
 44        lk2 = 0; // initially lock is open
 45
 46        lk3 = 0; // initially lock is open
 47
 48        lk4 = 0; // initially lock is open
 49
 50        lk5 = 0; // initially lock is open
 51
 52        lk6 = 0; // initially lock is open
 53
 54        lk7 = 0; // initially lock is open
 55
 56        lk8 = 0; // initially lock is open
 57
 58        lk9 = 0; // initially lock is open
 59
 60        lk10 = 0; // initially lock is open
 61
 62
 63    // lock phase
 64        if (p1 != 0) {
 65            lk1 = 1; // acquire lock
 66        } else {}
 67
 68        if (p2 != 0) {
 69            lk2 = 1; // acquire lock
 70        } else {}
 71
 72        if (p3 != 0) {
 73            lk3 = 1; // acquire lock
 74        } else {}
 75
 76        if (p4 != 0) {
 77            lk4 = 1; // acquire lock
 78        } else {}
 79
 80        if (p5 != 0) {
 81            lk5 = 1; // acquire lock
 82        } else {}
 83
 84        if (p6 != 0) {
 85            lk6 = 1; // acquire lock
 86        } else {}
 87
 88        if (p7 != 0) {
 89            lk7 = 1; // acquire lock
 90        } else {}
 91
 92        if (p8 != 0) {
 93            lk8 = 1; // acquire lock
 94        } else {}
 95
 96        if (p9 != 0) {
 97            lk9 = 1; // acquire lock
 98        } else {}
 99
100        if (p10 != 0) {
101            lk10 = 1; // acquire lock
102        } else {}
103
104
105    // unlock phase
106        if (p1 != 0) {
107            if (lk1 != 1) goto ERROR; // assertion failure
108            lk1 = 0;
109        } else {}
110
111        if (p2 != 0) {
112            if (lk2 != 1) goto ERROR; // assertion failure
113            lk2 = 0;
114        } else {}
115
116        if (p3 != 0) {
117            if (lk3 != 1) goto ERROR; // assertion failure
118            lk3 = 0;
119        } else {}
120
121        if (p4 != 0) {
122            if (lk4 != 1) goto ERROR; // assertion failure
123            lk4 = 0;
124        } else {}
125
126        if (p5 != 0) {
127            if (lk5 != 1) goto ERROR; // assertion failure
128            lk5 = 0;
129        } else {}
130
131        if (p6 != 0) {
132            if (lk6 != 1) goto ERROR; // assertion failure
133            lk6 = 0;
134        } else {}
135
136        if (p7 != 0) {
137            if (lk7 != 1) goto ERROR; // assertion failure
138            lk7 = 0;
139        } else {}
140
141        if (p8 != 0) {
142            if (lk8 != 1) goto ERROR; // assertion failure
143            lk8 = 0;
144        } else {}
145
146        if (p9 != 0) {
147            if (lk9 != 1) goto ERROR; // assertion failure
148            lk9 = 0;
149        } else {}
150
151        if (p10 != 0) {
152            if (lk10 != 1) goto ERROR; // assertion failure
153            lk10 = 0;
154        } else {}
155
156    }
157  out:
158    return 0;
159  ERROR:
160    return 0;  
161}
162
↑