Showing error 13

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_11.c
Line in file: 178
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
 43    int cond;
 44
 45    while(1) {
 46        cond = get_exit_nondet();
 47        if (cond == 0) {
 48            goto out;
 49        } else {}
 50        lk1 = 0; // initially lock is open
 51
 52        lk2 = 0; // initially lock is open
 53
 54        lk3 = 0; // initially lock is open
 55
 56        lk4 = 0; // initially lock is open
 57
 58        lk5 = 0; // initially lock is open
 59
 60        lk6 = 0; // initially lock is open
 61
 62        lk7 = 0; // initially lock is open
 63
 64        lk8 = 0; // initially lock is open
 65
 66        lk9 = 0; // initially lock is open
 67
 68        lk10 = 0; // initially lock is open
 69
 70        lk11 = 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
119    // unlock phase
120        if (p1 != 0) {
121            if (lk1 != 1) goto ERROR; // assertion failure
122            lk1 = 0;
123        } else {}
124
125        if (p2 != 0) {
126            if (lk2 != 1) goto ERROR; // assertion failure
127            lk2 = 0;
128        } else {}
129
130        if (p3 != 0) {
131            if (lk3 != 1) goto ERROR; // assertion failure
132            lk3 = 0;
133        } else {}
134
135        if (p4 != 0) {
136            if (lk4 != 1) goto ERROR; // assertion failure
137            lk4 = 0;
138        } else {}
139
140        if (p5 != 0) {
141            if (lk5 != 1) goto ERROR; // assertion failure
142            lk5 = 0;
143        } else {}
144
145        if (p6 != 0) {
146            if (lk6 != 1) goto ERROR; // assertion failure
147            lk6 = 0;
148        } else {}
149
150        if (p7 != 0) {
151            if (lk7 != 1) goto ERROR; // assertion failure
152            lk7 = 0;
153        } else {}
154
155        if (p8 != 0) {
156            if (lk8 != 1) goto ERROR; // assertion failure
157            lk8 = 0;
158        } else {}
159
160        if (p9 != 0) {
161            if (lk9 != 1) goto ERROR; // assertion failure
162            lk9 = 0;
163        } else {}
164
165        if (p10 != 0) {
166            if (lk10 != 1) goto ERROR; // assertion failure
167            lk10 = 0;
168        } else {}
169
170        if (p11 != 0) {
171            if (lk11 != 1) goto ERROR; // assertion failure
172            lk11 = 0;
173        } else {}
174
175    }
176  out:
177    return 0;
178  ERROR:
179    return 0;  
180}
181
↑