Showing error 1461

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