Showing error 14

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