Showing error 1458

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