Showing error 12

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_10.c
Line in file: 164
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
 40    int cond;
 41
 42    while(1) {
 43        cond = get_exit_nondet();
 44        if (cond == 0) {
 45            goto out;
 46        } else {}
 47        lk1 = 0; // initially lock is open
 48
 49        lk2 = 0; // initially lock is open
 50
 51        lk3 = 0; // initially lock is open
 52
 53        lk4 = 0; // initially lock is open
 54
 55        lk5 = 0; // initially lock is open
 56
 57        lk6 = 0; // initially lock is open
 58
 59        lk7 = 0; // initially lock is open
 60
 61        lk8 = 0; // initially lock is open
 62
 63        lk9 = 0; // initially lock is open
 64
 65        lk10 = 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
110    // unlock phase
111        if (p1 != 0) {
112            if (lk1 != 1) goto ERROR; // assertion failure
113            lk1 = 0;
114        } else {}
115
116        if (p2 != 0) {
117            if (lk2 != 1) goto ERROR; // assertion failure
118            lk2 = 0;
119        } else {}
120
121        if (p3 != 0) {
122            if (lk3 != 1) goto ERROR; // assertion failure
123            lk3 = 0;
124        } else {}
125
126        if (p4 != 0) {
127            if (lk4 != 1) goto ERROR; // assertion failure
128            lk4 = 0;
129        } else {}
130
131        if (p5 != 0) {
132            if (lk5 != 1) goto ERROR; // assertion failure
133            lk5 = 0;
134        } else {}
135
136        if (p6 != 0) {
137            if (lk6 != 1) goto ERROR; // assertion failure
138            lk6 = 0;
139        } else {}
140
141        if (p7 != 0) {
142            if (lk7 != 1) goto ERROR; // assertion failure
143            lk7 = 0;
144        } else {}
145
146        if (p8 != 0) {
147            if (lk8 != 1) goto ERROR; // assertion failure
148            lk8 = 0;
149        } else {}
150
151        if (p9 != 0) {
152            if (lk9 != 1) goto ERROR; // assertion failure
153            lk9 = 0;
154        } else {}
155
156        if (p10 != 0) {
157            if (lk10 != 1) goto ERROR; // assertion failure
158            lk10 = 0;
159        } else {}
160
161    }
162  out:
163    return 0;
164  ERROR:
165    return 0;  
166}
167
↑