Showing error 23

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