Showing error 21

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_6.c
Line in file: 108
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
 28    int cond;
 29
 30    while(1) {
 31        cond = get_exit_nondet();
 32        if (cond == 0) {
 33            goto out;
 34        } else {}
 35        lk1 = 0; // initially lock is open
 36
 37        lk2 = 0; // initially lock is open
 38
 39        lk3 = 0; // initially lock is open
 40
 41        lk4 = 0; // initially lock is open
 42
 43        lk5 = 0; // initially lock is open
 44
 45        lk6 = 0; // initially lock is open
 46
 47
 48    // lock phase
 49        if (p1 != 0) {
 50            lk1 = 1; // acquire lock
 51        } else {}
 52
 53        if (p2 != 0) {
 54            lk2 = 1; // acquire lock
 55        } else {}
 56
 57        if (p3 != 0) {
 58            lk3 = 1; // acquire lock
 59        } else {}
 60
 61        if (p4 != 0) {
 62            lk4 = 1; // acquire lock
 63        } else {}
 64
 65        if (p5 != 0) {
 66            lk5 = 1; // acquire lock
 67        } else {}
 68
 69        if (p6 != 0) {
 70            lk6 = 1; // acquire lock
 71        } else {}
 72
 73
 74    // unlock phase
 75        if (p1 != 0) {
 76            if (lk1 != 1) goto ERROR; // assertion failure
 77            lk1 = 0;
 78        } else {}
 79
 80        if (p2 != 0) {
 81            if (lk2 != 1) goto ERROR; // assertion failure
 82            lk2 = 0;
 83        } else {}
 84
 85        if (p3 != 0) {
 86            if (lk3 != 1) goto ERROR; // assertion failure
 87            lk3 = 0;
 88        } else {}
 89
 90        if (p4 != 0) {
 91            if (lk4 != 1) goto ERROR; // assertion failure
 92            lk4 = 0;
 93        } else {}
 94
 95        if (p5 != 0) {
 96            if (lk5 != 1) goto ERROR; // assertion failure
 97            lk5 = 0;
 98        } else {}
 99
100        if (p6 != 0) {
101            if (lk6 != 1) goto ERROR; // assertion failure
102            lk6 = 0;
103        } else {}
104
105    }
106  out:
107    return 0;
108  ERROR:
109    return 0;  
110}
111
↑