Showing error 17

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.c
Line in file: 220
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

  1int get_exit_nondet()
  2{
  3    int retval;
  4    return (retval);
  5}
  6
  7int main()
  8{
  9    int p1;  // condition variable
 10    int lk1; // lock variable
 11
 12    int p2;  // condition variable
 13    int lk2; // lock variable
 14
 15    int p3;  // condition variable
 16    int lk3; // lock variable
 17
 18    int p4;  // condition variable
 19    int lk4; // lock variable
 20
 21    int p5;  // condition variable
 22    int lk5; // lock variable
 23
 24    int p6;  // condition variable
 25    int lk6; // lock variable
 26
 27    int p7;  // condition variable
 28    int lk7; // lock variable
 29
 30    int p8;  // condition variable
 31    int lk8; // lock variable
 32
 33    int p9;  // condition variable
 34    int lk9; // lock variable
 35
 36    int p10;  // condition variable
 37    int lk10; // lock variable
 38
 39    int p11;  // condition variable
 40    int lk11; // lock variable
 41
 42    int p12;  // condition variable
 43    int lk12; // lock variable
 44
 45    int p13;  // condition variable
 46    int lk13; // lock variable
 47
 48    int p14;  // condition variable
 49    int lk14; // lock variable
 50
 51
 52    int cond;
 53
 54    while(1) {
 55        cond = get_exit_nondet();
 56        if (cond == 0) {
 57            goto out;
 58        } else {}
 59        lk1 = 0; // initially lock is open
 60
 61        lk2 = 0; // initially lock is open
 62
 63        lk3 = 0; // initially lock is open
 64
 65        lk4 = 0; // initially lock is open
 66
 67        lk5 = 0; // initially lock is open
 68
 69        lk6 = 0; // initially lock is open
 70
 71        lk7 = 0; // initially lock is open
 72
 73        lk8 = 0; // initially lock is open
 74
 75        lk9 = 0; // initially lock is open
 76
 77        lk10 = 0; // initially lock is open
 78
 79        lk11 = 0; // initially lock is open
 80
 81        lk12 = 0; // initially lock is open
 82
 83        lk13 = 0; // initially lock is open
 84
 85        lk14 = 0; // initially lock is open
 86
 87
 88    // lock phase
 89        if (p1 != 0) {
 90            lk1 = 1; // acquire lock
 91        } else {}
 92
 93        if (p2 != 0) {
 94            lk2 = 1; // acquire lock
 95        } else {}
 96
 97        if (p3 != 0) {
 98            lk3 = 1; // acquire lock
 99        } else {}
100
101        if (p4 != 0) {
102            lk4 = 1; // acquire lock
103        } else {}
104
105        if (p5 != 0) {
106            lk5 = 1; // acquire lock
107        } else {}
108
109        if (p6 != 0) {
110            lk6 = 1; // acquire lock
111        } else {}
112
113        if (p7 != 0) {
114            lk7 = 1; // acquire lock
115        } else {}
116
117        if (p8 != 0) {
118            lk8 = 1; // acquire lock
119        } else {}
120
121        if (p9 != 0) {
122            lk9 = 1; // acquire lock
123        } else {}
124
125        if (p10 != 0) {
126            lk10 = 1; // acquire lock
127        } else {}
128
129        if (p11 != 0) {
130            lk11 = 1; // acquire lock
131        } else {}
132
133        if (p12 != 0) {
134            lk12 = 1; // acquire lock
135        } else {}
136
137        if (p13 != 0) {
138            lk13 = 1; // acquire lock
139        } else {}
140
141        if (p14 != 0) {
142            lk14 = 1; // acquire lock
143        } else {}
144
145
146    // unlock phase
147        if (p1 != 0) {
148            if (lk1 != 1) goto ERROR; // assertion failure
149            lk1 = 0;
150        } else {}
151
152        if (p2 != 0) {
153            if (lk2 != 1) goto ERROR; // assertion failure
154            lk2 = 0;
155        } else {}
156
157        if (p3 != 0) {
158            if (lk3 != 1) goto ERROR; // assertion failure
159            lk3 = 0;
160        } else {}
161
162        if (p4 != 0) {
163            if (lk4 != 1) goto ERROR; // assertion failure
164            lk4 = 0;
165        } else {}
166
167        if (p5 != 0) {
168            if (lk5 != 1) goto ERROR; // assertion failure
169            lk5 = 0;
170        } else {}
171
172        if (p6 != 0) {
173            if (lk6 != 1) goto ERROR; // assertion failure
174            lk6 = 0;
175        } else {}
176
177        if (p7 != 0) {
178            if (lk7 != 1) goto ERROR; // assertion failure
179            lk7 = 0;
180        } else {}
181
182        if (p8 != 0) {
183            if (lk8 != 1) goto ERROR; // assertion failure
184            lk8 = 0;
185        } else {}
186
187        if (p9 != 0) {
188            if (lk9 != 1) goto ERROR; // assertion failure
189            lk9 = 0;
190        } else {}
191
192        if (p10 != 0) {
193            if (lk10 != 1) goto ERROR; // assertion failure
194            lk10 = 0;
195        } else {}
196
197        if (p11 != 0) {
198            if (lk11 != 1) goto ERROR; // assertion failure
199            lk11 = 0;
200        } else {}
201
202        if (p12 != 0) {
203            if (lk12 != 1) goto ERROR; // assertion failure
204            lk12 = 0;
205        } else {}
206
207        if (p13 != 0) {
208            if (lk13 != 1) goto ERROR; // assertion failure
209            lk13 = 0;
210        } else {}
211
212        if (p14 != 0) {
213            if (lk14 != 1) goto ERROR; // assertion failure
214            lk14 = 0;
215        } else {}
216
217    }
218  out:
219    return 0;
220  ERROR:
221    return 0;  
222}
223
↑