Showing error 24

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