Showing error 15

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_13.c
Line in file: 206
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
 49    int cond;
 50
 51    while(1) {
 52        cond = get_exit_nondet();
 53        if (cond == 0) {
 54            goto out;
 55        } else {}
 56        lk1 = 0; // initially lock is open
 57
 58        lk2 = 0; // initially lock is open
 59
 60        lk3 = 0; // initially lock is open
 61
 62        lk4 = 0; // initially lock is open
 63
 64        lk5 = 0; // initially lock is open
 65
 66        lk6 = 0; // initially lock is open
 67
 68        lk7 = 0; // initially lock is open
 69
 70        lk8 = 0; // initially lock is open
 71
 72        lk9 = 0; // initially lock is open
 73
 74        lk10 = 0; // initially lock is open
 75
 76        lk11 = 0; // initially lock is open
 77
 78        lk12 = 0; // initially lock is open
 79
 80        lk13 = 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
137    // unlock phase
138        if (p1 != 0) {
139            if (lk1 != 1) goto ERROR; // assertion failure
140            lk1 = 0;
141        } else {}
142
143        if (p2 != 0) {
144            if (lk2 != 1) goto ERROR; // assertion failure
145            lk2 = 0;
146        } else {}
147
148        if (p3 != 0) {
149            if (lk3 != 1) goto ERROR; // assertion failure
150            lk3 = 0;
151        } else {}
152
153        if (p4 != 0) {
154            if (lk4 != 1) goto ERROR; // assertion failure
155            lk4 = 0;
156        } else {}
157
158        if (p5 != 0) {
159            if (lk5 != 1) goto ERROR; // assertion failure
160            lk5 = 0;
161        } else {}
162
163        if (p6 != 0) {
164            if (lk6 != 1) goto ERROR; // assertion failure
165            lk6 = 0;
166        } else {}
167
168        if (p7 != 0) {
169            if (lk7 != 1) goto ERROR; // assertion failure
170            lk7 = 0;
171        } else {}
172
173        if (p8 != 0) {
174            if (lk8 != 1) goto ERROR; // assertion failure
175            lk8 = 0;
176        } else {}
177
178        if (p9 != 0) {
179            if (lk9 != 1) goto ERROR; // assertion failure
180            lk9 = 0;
181        } else {}
182
183        if (p10 != 0) {
184            if (lk10 != 1) goto ERROR; // assertion failure
185            lk10 = 0;
186        } else {}
187
188        if (p11 != 0) {
189            if (lk11 != 1) goto ERROR; // assertion failure
190            lk11 = 0;
191        } else {}
192
193        if (p12 != 0) {
194            if (lk12 != 1) goto ERROR; // assertion failure
195            lk12 = 0;
196        } else {}
197
198        if (p13 != 0) {
199            if (lk13 != 1) goto ERROR; // assertion failure
200            lk13 = 0;
201        } else {}
202
203    }
204  out:
205    return 0;
206  ERROR:
207    return 0;  
208}
209
↑