Showing error 1459

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_12_safe.c
Line in file: 187
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    int p11 = __VERIFIER_nondet_int();  // condition variable
 35    int lk11; // lock variable
 36
 37    int p12 = __VERIFIER_nondet_int();  // condition variable
 38    int lk12; // lock variable
 39
 40
 41    int cond;
 42
 43    while(1) {
 44        cond = __VERIFIER_nondet_int();
 45        if (cond == 0) {
 46            goto out;
 47        } else {}
 48        lk1 = 0; // initially lock is open
 49
 50        lk2 = 0; // initially lock is open
 51
 52        lk3 = 0; // initially lock is open
 53
 54        lk4 = 0; // initially lock is open
 55
 56        lk5 = 0; // initially lock is open
 57
 58        lk6 = 0; // initially lock is open
 59
 60        lk7 = 0; // initially lock is open
 61
 62        lk8 = 0; // initially lock is open
 63
 64        lk9 = 0; // initially lock is open
 65
 66        lk10 = 0; // initially lock is open
 67
 68        lk11 = 0; // initially lock is open
 69
 70        lk12 = 0; // initially lock is open
 71
 72
 73    // lock phase
 74        if (p1 != 0) {
 75            lk1 = 1; // acquire lock
 76        } else {}
 77
 78        if (p2 != 0) {
 79            lk2 = 1; // acquire lock
 80        } else {}
 81
 82        if (p3 != 0) {
 83            lk3 = 1; // acquire lock
 84        } else {}
 85
 86        if (p4 != 0) {
 87            lk4 = 1; // acquire lock
 88        } else {}
 89
 90        if (p5 != 0) {
 91            lk5 = 1; // acquire lock
 92        } else {}
 93
 94        if (p6 != 0) {
 95            lk6 = 1; // acquire lock
 96        } else {}
 97
 98        if (p7 != 0) {
 99            lk7 = 1; // acquire lock
100        } else {}
101
102        if (p8 != 0) {
103            lk8 = 1; // acquire lock
104        } else {}
105
106        if (p9 != 0) {
107            lk9 = 1; // acquire lock
108        } else {}
109
110        if (p10 != 0) {
111            lk10 = 1; // acquire lock
112        } else {}
113
114        if (p11 != 0) {
115            lk11 = 1; // acquire lock
116        } else {}
117
118        if (p12 != 0) {
119            lk12 = 1; // acquire lock
120        } else {}
121
122
123    // unlock phase
124        if (p1 != 0) {
125            if (lk1 != 1) goto ERROR; // assertion failure
126            lk1 = 0;
127        } else {}
128
129        if (p2 != 0) {
130            if (lk2 != 1) goto ERROR; // assertion failure
131            lk2 = 0;
132        } else {}
133
134        if (p3 != 0) {
135            if (lk3 != 1) goto ERROR; // assertion failure
136            lk3 = 0;
137        } else {}
138
139        if (p4 != 0) {
140            if (lk4 != 1) goto ERROR; // assertion failure
141            lk4 = 0;
142        } else {}
143
144        if (p5 != 0) {
145            if (lk5 != 1) goto ERROR; // assertion failure
146            lk5 = 0;
147        } else {}
148
149        if (p6 != 0) {
150            if (lk6 != 1) goto ERROR; // assertion failure
151            lk6 = 0;
152        } else {}
153
154        if (p7 != 0) {
155            if (lk7 != 1) goto ERROR; // assertion failure
156            lk7 = 0;
157        } else {}
158
159        if (p8 != 0) {
160            if (lk8 != 1) goto ERROR; // assertion failure
161            lk8 = 0;
162        } else {}
163
164        if (p9 != 0) {
165            if (lk9 != 1) goto ERROR; // assertion failure
166            lk9 = 0;
167        } else {}
168
169        if (p10 != 0) {
170            if (lk10 != 1) goto ERROR; // assertion failure
171            lk10 = 0;
172        } else {}
173
174        if (p11 != 0) {
175            if (lk11 != 1) goto ERROR; // assertion failure
176            lk11 = 0;
177        } else {}
178
179        if (p12 != 0) {
180            if (lk12 != 1) goto ERROR; // assertion failure
181            lk12 = 0;
182        } else {}
183
184    }
185  out:
186    return 0;
187  ERROR:
188    return 0;  
189}
190
↑